-- Mathlib/Algebra/DirectSum/LinearMap.lean
/-- The trace of an endomorphism of a direct sum is the sum of the traces on each component.

Note that it is important the statement gives the user definitional control over `p` since the
_type_ of the term `trace R p (f.restrict hp')` depends on `p`. -/
lemma trace_eq_sum_trace_restrict_of_eq_biSup
    [∀ i, Module.Finite R (N i)] [∀ i, Module.Free R (N i)]
    (s : Finset ι) (h : iSupIndep <| fun i : s ↦ N i)
    {f : Module.End R M} (hf : ∀ i, MapsTo f (N i) (N i))
    (p : Submodule R M) (hp : p = ⨆ i ∈ s, N i)
    (hp' : MapsTo f p p := hp ▸ mapsTo_biSup_of_mapsTo (s : Set ι) hf) :
    trace R p (f.restrict hp') = ∑ i ∈ s, trace R (N i) (f.restrict (hf i))

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : ι → Submodule R M
inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝ : ∀ (i : ι), Module.Free R ↥(N i)
s : Finset ι
f : Module.End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
p : Submodule R M
hp : p = ⨆ i ∈ s, N i
hp' : optParam (MapsTo ⇑f ↑p ↑p) ⋯
N' : { x // x ∈ s } → Submodule R ↥p := fun i => Submodule.comap p.subtype (N ↑i)
h : IsInternal N'
hf' : ∀ (i : { x // x ∈ s }), MapsTo ⇑(restrict f hp') ↑(N' i) ↑(N' i)
e : (i : { x // x ∈ s }) → ↥(N' i) ≃ₗ[R] ↥(N ↑i) :=
  fun x =>
    match x with
    | ⟨i, hi⟩ => Submodule.comapSubtypeEquivOfLe ⋯
_i1 : ∀ (i : { x // x ∈ s }), Module.Finite R ↥(N' i)
_i2 : ∀ (i : { x // x ∈ s }), Module.Free R ↥(N' i)
⊢ ∑ i : { x // x ∈ s }, (trace R ↥(N' i)) ((restrict f hp').restrict ⋯) =
    ∑ i : { x // x ∈ s }, (trace R ↥(N ↑i)) (restrict f ⋯)

Tactic:
have : ∀ i : s, f.restrict (hf i) = (e i).conj ((f.restrict hp').restrict (hf' i)) := fun _ ↦ rfl

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : ι → Submodule R M
inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝ : ∀ (i : ι), Module.Free R ↥(N i)
s : Finset ι
f : Module.End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
p : Submodule R M
hp : p = ⨆ i ∈ s, N i
hp' : optParam (MapsTo ⇑f ↑p ↑p) ⋯
N' : { x // x ∈ s } → Submodule R ↥p := fun i => Submodule.comap p.subtype (N ↑i)
h : IsInternal N'
hf' : ∀ (i : { x // x ∈ s }), MapsTo ⇑(restrict f hp') ↑(N' i) ↑(N' i)
e : (i : { x // x ∈ s }) → ↥(N' i) ≃ₗ[R] ↥(N ↑i) :=
  fun x =>
    match x with
    | ⟨i, hi⟩ => Submodule.comapSubtypeEquivOfLe ⋯
_i1 : ∀ (i : { x // x ∈ s }), Module.Finite R ↥(N' i)
_i2 : ∀ (i : { x // x ∈ s }), Module.Free R ↥(N' i)
this : ∀ (i : { x // x ∈ s }), restrict f ⋯ = (e i).conj ((restrict f hp').restrict ⋯)
⊢ ∑ i : { x // x ∈ s }, (trace R ↥(N' i)) ((restrict f hp').restrict ⋯) =
    ∑ i : { x // x ∈ s }, (trace R ↥(N ↑i)) (restrict f ⋯)

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : ι → Submodule R M
inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝ : ∀ (i : ι), Module.Free R ↥(N i)
s : Finset ι
f : Module.End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
p : Submodule R M
hp : p = ⨆ i ∈ s, N i
hp' : optParam (MapsTo ⇑f ↑p ↑p) ⋯
N' : { x // x ∈ s } → Submodule R ↥p := fun i => Submodule.comap p.subtype (N ↑i)
h : IsInternal N'
hf' : ∀ (i : { x // x ∈ s }), MapsTo ⇑(restrict f hp') ↑(N' i) ↑(N' i)
e : (i : { x // x ∈ s }) → ↥(N' i) ≃ₗ[R] ↥(N ↑i) :=
  fun x =>
    match x with
    | ⟨i, hi⟩ => Submodule.comapSubtypeEquivOfLe ⋯
_i1 : ∀ (i : { x // x ∈ s }), Module.Finite R ↥(N' i)
⊢ (trace R ↥p) (restrict f hp') = ∑ i ∈ s, (trace R ↥(N i)) (restrict f ⋯)

Tactic:
have _i2 : ∀ i, Module.Free R (N' i) := fun i ↦ Module.Free.of_equiv (e i).symm

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : ι → Submodule R M
inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝ : ∀ (i : ι), Module.Free R ↥(N i)
s : Finset ι
f : Module.End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
p : Submodule R M
hp : p = ⨆ i ∈ s, N i
hp' : optParam (MapsTo ⇑f ↑p ↑p) ⋯
N' : { x // x ∈ s } → Submodule R ↥p := fun i => Submodule.comap p.subtype (N ↑i)
h : IsInternal N'
hf' : ∀ (i : { x // x ∈ s }), MapsTo ⇑(restrict f hp') ↑(N' i) ↑(N' i)
e : (i : { x // x ∈ s }) → ↥(N' i) ≃ₗ[R] ↥(N ↑i) :=
  fun x =>
    match x with
    | ⟨i, hi⟩ => Submodule.comapSubtypeEquivOfLe ⋯
_i1 : ∀ (i : { x // x ∈ s }), Module.Finite R ↥(N' i)
_i2 : ∀ (i : { x // x ∈ s }), Module.Free R ↥(N' i)
⊢ (trace R ↥p) (restrict f hp') = ∑ i ∈ s, (trace R ↥(N i)) (restrict f ⋯)

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : ι → Submodule R M
inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝ : ∀ (i : ι), Module.Free R ↥(N i)
s : Finset ι
h : iSupIndep fun i => N ↑i
f : Module.End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
p : Submodule R M
hp : p = ⨆ i ∈ s, N i
hp' : optParam (MapsTo ⇑f ↑p ↑p) ⋯
⊢ (trace R ↥p) (restrict f hp') = ∑ i ∈ s, (trace R ↥(N i)) (restrict f ⋯)

Tactic:
classical
let N' : s → Submodule R p := fun i ↦ (N i).comap p.subtype
replace h : IsInternal N' := hp ▸ isInternal_biSup_submodule_of_iSupIndep (s : Set ι) h
have hf' : ∀ i, MapsTo (restrict f hp') (N' i) (N' i) := fun i x hx' ↦ by simpa using hf i hx'
let e : (i : s) → N' i ≃ₗ[R] N i := fun ⟨i, hi⟩ ↦ (N i).comapSubtypeEquivOfLe (hp ▸ le_biSup N hi)
have _i1 : ∀ i, Module.Finite R (N' i) := fun i ↦ Module.Finite.equiv (e i).symm
have _i2 : ∀ i, Module.Free R (N' i) := fun i ↦ Module.Free.of_equiv (e i).symm
rw [trace_eq_sum_trace_restrict h hf', ← s.sum_coe_sort]
have : ∀ i : s, f.restrict (hf i) = (e i).conj ((f.restrict hp').restrict (hf' i)) := fun _ ↦ rfl
simp [this]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : ι → Submodule R M
inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝ : ∀ (i : ι), Module.Free R ↥(N i)
s : Finset ι
f : Module.End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
p : Submodule R M
hp : p = ⨆ i ∈ s, N i
hp' : optParam (MapsTo ⇑f ↑p ↑p) ⋯
N' : { x // x ∈ s } → Submodule R ↥p := fun i => Submodule.comap p.subtype (N ↑i)
h : IsInternal N'
hf' : ∀ (i : { x // x ∈ s }), MapsTo ⇑(restrict f hp') ↑(N' i) ↑(N' i)
e : (i : { x // x ∈ s }) → ↥(N' i) ≃ₗ[R] ↥(N ↑i) :=
  fun x =>
    match x with
    | ⟨i, hi⟩ => Submodule.comapSubtypeEquivOfLe ⋯
_i1 : ∀ (i : { x // x ∈ s }), Module.Finite R ↥(N' i)
_i2 : ∀ (i : { x // x ∈ s }), Module.Free R ↥(N' i)
this : ∀ (i : { x // x ∈ s }), restrict f ⋯ = (e i).conj ((restrict f hp').restrict ⋯)
⊢ ∑ i : { x // x ∈ s }, (trace R ↥(N' i)) ((restrict f hp').restrict ⋯) =
    ∑ i : { x // x ∈ s }, (trace R ↥(N ↑i)) (restrict f ⋯)

Tactic:
simp [this]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : ι → Submodule R M
inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝ : ∀ (i : ι), Module.Free R ↥(N i)
s : Finset ι
f : Module.End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
p : Submodule R M
hp : p = ⨆ i ∈ s, N i
hp' : optParam (MapsTo ⇑f ↑p ↑p) ⋯
N' : { x // x ∈ s } → Submodule R ↥p := fun i => Submodule.comap p.subtype (N ↑i)
h : IsInternal N'
⊢ (trace R ↥p) (restrict f hp') = ∑ i ∈ s, (trace R ↥(N i)) (restrict f ⋯)

Tactic:
have hf' : ∀ i, MapsTo (restrict f hp') (N' i) (N' i) := fun i x hx' ↦ by simpa using hf i hx'

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : ι → Submodule R M
inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝ : ∀ (i : ι), Module.Free R ↥(N i)
s : Finset ι
f : Module.End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
p : Submodule R M
hp : p = ⨆ i ∈ s, N i
hp' : optParam (MapsTo ⇑f ↑p ↑p) ⋯
N' : { x // x ∈ s } → Submodule R ↥p := fun i => Submodule.comap p.subtype (N ↑i)
h : IsInternal N'
hf' : ∀ (i : { x // x ∈ s }), MapsTo ⇑(restrict f hp') ↑(N' i) ↑(N' i)
⊢ (trace R ↥p) (restrict f hp') = ∑ i ∈ s, (trace R ↥(N i)) (restrict f ⋯)