awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.LinearMap (hypothesis)
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Free R M
inst_6 : Module.Finite R M
f g : End R M
h_comm : Commute f g
hf : Eq.{u_3 + 1} (α := Submodule R M) (⨆ (μ : R), f.maxGenEigenspace μ) ⊤
hg :
  ∀ (μ : R),
    Eq.{u_2 + 1} (α := R)
      ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
          (restrict g ⋯) :
        R)
      (0 : R)
hfg : ∀ (μ : R), MapsTo (⇑(g ∘ₗ f) : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
μ : R
hf' : MapsTo (⇑f : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
hg' : MapsTo (⇑g : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
⊢ Eq.{u_2 + 1} (α := R)
    ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
        ((g ∘ₗ f).restrict ⋯) :
      R)
    (0 : R)
have h_comm₁ : Commute (restrict g sorry) (restrict f sorry)
Tactic: replace h_comm : Commute (g.restrict (f.mapsTo_maxGenEigenspace_of_comm h_comm μ))
      (f.restrict (f.mapsTo_maxGenEigenspace_of_comm rfl μ)) :=
    restrict_commute h_comm.symm _ _
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.LinearMap (hypothesis)
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Free R M
inst_6 : Module.Finite R M
f g : End R M
h_comm_1 : Commute f g
hf : Eq.{u_3 + 1} (α := Submodule R M) (⨆ (μ : R), f.maxGenEigenspace μ) ⊤
hg :
  ∀ (μ : R),
    Eq.{u_2 + 1} (α := R)
      ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
          (restrict g ⋯) :
        R)
      (0 : R)
hfg : ∀ (μ : R), MapsTo (⇑(g ∘ₗ f) : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
μ : R
hf' : MapsTo (⇑f : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
hg' : MapsTo (⇑g : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
h_comm : Commute (restrict g ⋯) (restrict f ⋯)
⊢ Eq.{u_2 + 1} (α := R)
    ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
        ((g ∘ₗ f).restrict ⋯) :
      R)
    (0 : R)
have this : IsNilpotent (restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) sorry)
Tactic: have := f.isNilpotent_restrict_maxGenEigenspace_sub_algebraMap μ
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.LinearMap (goal)
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Free R M
inst_6 : Module.Finite R M
f g : End R M
h_comm_1 : Commute f g
hf : Eq.{u_3 + 1} (α := Submodule R M) (⨆ (μ : R), f.maxGenEigenspace μ) ⊤
hg :
  ∀ (μ : R),
    Eq.{u_2 + 1} (α := R)
      ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
          (restrict g ⋯) :
        R)
      (0 : R)
hfg : ∀ (μ : R), MapsTo (⇑(g ∘ₗ f) : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
μ : R
hf' : MapsTo (⇑f : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
hg' : MapsTo (⇑g : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
h_comm : Commute (restrict g ⋯) (restrict f ⋯)
this : IsNilpotent (restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) ⋯)
⊢ Eq.{u_2 + 1} (α := R)
    ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
        ((g ∘ₗ f).restrict ⋯) :
      R)
    (0 : R)
have rw : Eq.{u_2 + 1} (α := R)
  ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
      (restrict g hg' ∘ₗ restrict f hf') :
    R)
  (0 : R)
Tactic: rw [restrict_comp hf' hg', trace_comp_eq_mul_of_commute_of_isNilpotent μ h_comm this,
    hg, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.LinearMap (goal)
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Free R M
inst_6 : Module.Finite R M
f g : End R M
h_comm_1 : Commute f g
hf : Eq.{u_3 + 1} (α := Submodule R M) (⨆ (μ : R), f.maxGenEigenspace μ) ⊤
hg :
  ∀ (μ : R),
    Eq.{u_2 + 1} (α := R)
      ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
          (restrict g ⋯) :
        R)
      (0 : R)
hfg : ∀ (μ : R), MapsTo (⇑(g ∘ₗ f) : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
μ : R
hf' : MapsTo (⇑f : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
hg' : MapsTo (⇑g : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
h_comm : Commute (restrict g ⋯) (restrict f ⋯)
this : IsNilpotent (restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) ⋯)
rw :
  Eq.{u_2 + 1} (α := R)
    ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
        (restrict g hg' ∘ₗ restrict f hf') :
      R)
    (0 : R)
⊢ Eq.{u_2 + 1} (α := R)
    ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
        ((g ∘ₗ f).restrict ⋯) :
      R)
    (0 : R)
have rw₁ : HMul.hMul (β := R) μ
    ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
        (restrict g sorry) :
      R) =
  0
Tactic: rw [restrict_comp hf' hg', trace_comp_eq_mul_of_commute_of_isNilpotent μ h_comm this,
    hg, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.LinearMap (goal)
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Free R M
inst_6 : Module.Finite R M
f g : End R M
h_comm_1 : Commute f g
hf : Eq.{u_3 + 1} (α := Submodule R M) (⨆ (μ : R), f.maxGenEigenspace μ) ⊤
hg :
  ∀ (μ : R),
    Eq.{u_2 + 1} (α := R)
      ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
          (restrict g ⋯) :
        R)
      (0 : R)
hfg : ∀ (μ : R), MapsTo (⇑(g ∘ₗ f) : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
μ : R
hf' : MapsTo (⇑f : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
hg' : MapsTo (⇑g : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
h_comm : Commute (restrict g ⋯) (restrict f ⋯)
this : IsNilpotent (restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) ⋯)
rw :
  Eq.{u_2 + 1} (α := R)
    ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
        (restrict g hg' ∘ₗ restrict f hf') :
      R)
    (0 : R)
rw₁ :
  HMul.hMul (β := R) μ
      ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
          (restrict g ⋯) :
        R) =
    0
⊢ Eq.{u_2 + 1} (α := R)
    ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
        ((g ∘ₗ f).restrict ⋯) :
      R)
    (0 : R)
have rw₂ : μ * 0 = 0
Tactic: rw [restrict_comp hf' hg', trace_comp_eq_mul_of_commute_of_isNilpotent μ h_comm this,
    hg, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.LinearMap (goal)
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Free R M
inst_6 : Module.Finite R M
f g : End R M
h_comm_1 : Commute f g
hf : Eq.{u_3 + 1} (α := Submodule R M) (⨆ (μ : R), f.maxGenEigenspace μ) ⊤
hg :
  ∀ (μ : R),
    Eq.{u_2 + 1} (α := R)
      ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
          (restrict g ⋯) :
        R)
      (0 : R)
hfg : ∀ (μ : R), MapsTo (⇑(g ∘ₗ f) : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
μ : R
hf' : MapsTo (⇑f : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
hg' : MapsTo (⇑g : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
h_comm : Commute (restrict g ⋯) (restrict f ⋯)
this : IsNilpotent (restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) ⋯)
rw :
  Eq.{u_2 + 1} (α := R)
    ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
        (restrict g hg' ∘ₗ restrict f hf') :
      R)
    (0 : R)
rw₁ :
  HMul.hMul (β := R) μ
      ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
          (restrict g ⋯) :
        R) =
    0
rw₂ : μ * 0 = 0
⊢ Eq.{u_2 + 1} (α := R)
    ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
        ((g ∘ₗ f).restrict ⋯) :
      R)
    (0 : R)
have rw₃ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [restrict_comp hf' hg', trace_comp_eq_mul_of_commute_of_isNilpotent μ h_comm this,
    hg, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.LinearMap (hypothesis)
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_4
N : ι → Submodule R M
s : Set ι
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N i) : Set M)
⊢ MapsTo (⇑f : (a : M) → M) (↑(⨆ i ∈ s, N i) : Set M) (↑(⨆ i ∈ s, N i) : Set M)
have hf₁ : ∀ (i : ι), Submodule.map f (N i) ≤ N i
Tactic: replace hf : ∀ i, (N i).map f ≤ N i := fun i ↦ Submodule.map_le_iff_le_comap.mpr (hf i)
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.LinearMap (goal)
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_4
N : ι → Submodule R M
s : Set ι
f : End R M
hf : ∀ (i : ι), Submodule.map f (N i) ≤ N i
⊢ MapsTo (⇑f : (a : M) → M) (↑(⨆ i ∈ s, N i) : Set M) (↑(⨆ i ∈ s, N i) : Set M)
have suffices : Submodule.map f (⨆ i ∈ s, N i) ≤ ⨆ i ∈ s, N i
Tactic: suffices (⨆ i ∈ s, N i).map f ≤ ⨆ i ∈ s, N i from Submodule.map_le_iff_le_comap.mp this
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.LinearMap (hypothesis)
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)
N' : ↥s → Submodule R ↥p := fun (i : ↥s) ↦ Submodule.comap p.subtype (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)
have h₁ : IsInternal N'
Tactic: replace h : IsInternal N' := hp ▸ isInternal_biSup_submodule_of_iSupIndep (s : Set ι) h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.LinearMap (hypothesis)
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 ι
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)
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)
have hf' : ∀ (i : ↥s), MapsTo (⇑(restrict f hp') : (a : ↥p) → ↥p) (↑(N' i) : Set ↥p) (↑(N' i) : Set ↥p)
Tactic: have hf' : ∀ i, MapsTo (restrict f hp') (N' i) (N' i) := fun i x hx' ↦ by simpa using hf i hx'
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.LinearMap (hypothesis)
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 ι
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)
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)
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 ⋯
⊢ 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 _i1 : ∀ (i : ↥s), Module.Finite.{u_2, u_3} R ↥(N' i)
Tactic: have _i1 : ∀ i, Module.Finite R (N' i) := fun i ↦ Module.Finite.equiv (e i).symm
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.LinearMap (hypothesis)
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 ι
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)
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)
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)
⊢ 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 _i2 : ∀ (i : ↥s), Free.{u_2, u_3} R ↥(N' i)
Tactic: have _i2 : ∀ i, Module.Free R (N' i) := fun i ↦ Module.Free.of_equiv (e i).symm
-- 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 ι
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)
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)
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)
⊢ 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 rw : Eq.{u_2 + 1} (α := R) (∑ i : ↥s, (trace R ↥(N' i) : (a : ↥(N' i) →ₗ[R] ↥(N' i)) → R) ((restrict f hp').restrict sorry))
  (∑ i : ↥s, (trace R ↥(N (↑i : ι)) : (a : ↥(N (↑i : ι)) →ₗ[R] ↥(N (↑i : ι))) → R) (restrict f sorry))
Tactic: rw [trace_eq_sum_trace_restrict h hf', ← s.sum_coe_sort]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.LinearMap (hypothesis)
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 ι
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)
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)
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)
⊢ 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 ⋯))
have this : ∀ (i : ↥s),
  Eq (α := ↥(N (↑i : ι)) →ₗ[R] ↥(N (↑i : ι))) (restrict f sorry)
    (((e i).conj : (a : End R ↥(N' i)) → End R ↥(N (↑i : ι))) ((restrict f hp').restrict sorry))
Tactic: have : ∀ i : s, f.restrict (hf i) = (e i).conj ((f.restrict hp').restrict (hf' i)) := fun _ ↦ rfl
-- 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)
⊢ 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'),
  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
-- 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)
⊢ 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)),
  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