-- Module: Mathlib.Algebra.DirectSum.LinearMap
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : ι → Submodule R M
inst_3 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_4 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
s : Finset ι
h : iSupIndep.{u_1 + 1, u_3} (α := Submodule R M) fun (i : ↥s) ↦ N (↑i : ι)
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N i) : Set M)
p : Submodule R M
hp : p = ⨆ i ∈ s, N i
hp' : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
let let₁ let₂ :
  Eq.{u_2 + 1} (α := R) ((trace R ↥p : (a : ↥p →ₗ[R] ↥p) → R) (restrict f hp') : R)
    (∑ i ∈ s, (trace R ↥(N i) : (a : ↥(N i) →ₗ[R] ↥(N i)) → R) (restrict f ⋯) : R)
let₃ :
  let N' : ↥s → Submodule R ↥p := fun (i : ↥s) ↦ Submodule.comap p.subtype (N (↑i : ι));
  ∀ (h : IsInternal N'),
    Eq.{u_2 + 1} (α := R) ((trace R ↥p : (a : ↥p →ₗ[R] ↥p) → R) (restrict f hp') : R)
      (∑ i ∈ s, (trace R ↥(N i) : (a : ↥(N i) →ₗ[R] ↥(N i)) → R) (restrict f ⋯) : R)
let₄ let₅ :
  let N' : ↥s → Submodule R ↥p := fun (i : ↥s) ↦ Submodule.comap p.subtype (N (↑i : ι));
  ∀ (h : IsInternal N')
    (hf' : ∀ (i : ↥s), MapsTo (⇑(restrict f hp') : (a : ↥p) → ↥p) (↑(N' i) : Set ↥p) (↑(N' i) : Set ↥p)),
    Eq.{u_2 + 1} (α := R) ((trace R ↥p : (a : ↥p →ₗ[R] ↥p) → R) (restrict f hp') : R)
      (∑ i ∈ s, (trace R ↥(N i) : (a : ↥(N i) →ₗ[R] ↥(N i)) → R) (restrict f ⋯) : R)
let₆ :
  let N' : ↥s → Submodule R ↥p := fun (i : ↥s) ↦ Submodule.comap p.subtype (N (↑i : ι));
  ∀ (h : IsInternal N')
    (hf' : ∀ (i : ↥s), MapsTo (⇑(restrict f hp') : (a : ↥p) → ↥p) (↑(N' i) : Set ↥p) (↑(N' i) : Set ↥p))
    (_i1 : ∀ (i : ↥s), Module.Finite.{u_2, u_3} R ↥(N' i)),
    Eq.{u_2 + 1} (α := R) ((trace R ↥p : (a : ↥p →ₗ[R] ↥p) → R) (restrict f hp') : R)
      (∑ i ∈ s, (trace R ↥(N i) : (a : ↥(N i) →ₗ[R] ↥(N i)) → R) (restrict f ⋯) : R)
let₇ :
  let N' : ↥s → Submodule R ↥p := fun (i : ↥s) ↦ Submodule.comap p.subtype (N (↑i : ι));
  ∀ (h : IsInternal N')
    (hf' : ∀ (i : ↥s), MapsTo (⇑(restrict f hp') : (a : ↥p) → ↥p) (↑(N' i) : Set ↥p) (↑(N' i) : Set ↥p))
    (_i1 : ∀ (i : ↥s), Module.Finite.{u_2, u_3} R ↥(N' i)) (_i2 : ∀ (i : ↥s), Free.{u_2, u_3} R ↥(N' i)),
    Eq.{u_2 + 1} (α := R) ((trace R ↥p : (a : ↥p →ₗ[R] ↥p) → R) (restrict f hp') : R)
      (∑ i ∈ s, (trace R ↥(N i) : (a : ↥(N i) →ₗ[R] ↥(N i)) → R) (restrict f ⋯) : R)
let₈ :
  let N' : ↥s → Submodule R ↥p := fun (i : ↥s) ↦ Submodule.comap p.subtype (N (↑i : ι));
  ∀ (h : IsInternal N')
    (hf' : ∀ (i : ↥s), MapsTo (⇑(restrict f hp') : (a : ↥p) → ↥p) (↑(N' i) : Set ↥p) (↑(N' i) : Set ↥p))
    (_i1 : ∀ (i : ↥s), Module.Finite.{u_2, u_3} R ↥(N' i)) (_i2 : ∀ (i : ↥s), Free.{u_2, u_3} R ↥(N' i)),
    Eq.{u_2 + 1} (α := R) (∑ i : ↥s, (trace R ↥(N' i) : (a : ↥(N' i) →ₗ[R] ↥(N' i)) → R) ((restrict f hp').restrict ⋯))
      (∑ i : ↥s, (trace R ↥(N (↑i : ι)) : (a : ↥(N (↑i : ι)) →ₗ[R] ↥(N (↑i : ι))) → R) (restrict f ⋯))
let₉ :
  let N' : ↥s → Submodule R ↥p := fun (i : ↥s) ↦ Submodule.comap p.subtype (N (↑i : ι));
  ∀ (h : IsInternal N')
    (hf' : ∀ (i : ↥s), MapsTo (⇑(restrict f hp') : (a : ↥p) → ↥p) (↑(N' i) : Set ↥p) (↑(N' i) : Set ↥p)),
    let e : (i : ↥s) → ↥(N' i) ≃ₗ[R] ↥(N (↑i : ι)) := fun (x : ↥s) ↦
      match (motive := (x : ↥s) → ↥(N' x) ≃ₗ[R] ↥(N (↑x : ι))) x with
      | ⟨i, hi⟩ => Submodule.comapSubtypeEquivOfLe ⋯;
    ∀ (_i1 : ∀ (i : ↥s), Module.Finite.{u_2, u_3} R ↥(N' i)) (_i2 : ∀ (i : ↥s), Free.{u_2, u_3} R ↥(N' i))
      (this :
        ∀ (i : ↥s),
          Eq (α := ↥(N (↑i : ι)) →ₗ[R] ↥(N (↑i : ι))) (restrict f ⋯)
            (((e i).conj : (a : End R ↥(N' i)) → End R ↥(N (↑i : ι))) ((restrict f hp').restrict ⋯))),
      Eq.{u_2 + 1} (α := R)
        (∑ i : ↥s, (trace R ↥(N' i) : (a : ↥(N' i) →ₗ[R] ↥(N' i)) → R) ((restrict f hp').restrict ⋯))
        (∑ i : ↥s, (trace R ↥(N (↑i : ι)) : (a : ↥(N (↑i : ι)) →ₗ[R] ↥(N (↑i : ι))) → R) (restrict f ⋯))
⊢ Eq.{u_2 + 1} (α := R) ((trace R ↥p : (a : ↥p →ₗ[R] ↥p) → R) (restrict f hp') : R)
    (∑ i ∈ s, (trace R ↥(N i) : (a : ↥(N i) →ₗ[R] ↥(N i)) → R) (restrict f ⋯) : R)

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]

Premises used: Finset.sum_coe_sort