-- Lean 4 proof step from Mathlib.Algebra.DirectSum.LinearMap (goal)
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)
⊢ 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)
have 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 sorry) : 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]
Cleared hypotheses: h