awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : DecidableEq ι
inst_4 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_5 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
h : IsInternal N
inst_6 : Fintype ι
f : M →ₗ[R] M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N i) : Set M)
b : (i : ι) → Basis.{u_3, u_2, u_3} (Free.ChooseBasisIndex R ↥(N i)) R ↥(N i) := fun (i : ι) ↦ Free.chooseBasis R ↥(N i)
simp_rw :
  Eq.{u_2 + 1} (α := R)
    (Matrix.trace (n := (i : ι) × Free.ChooseBasisIndex R ↥(N i))
      ((toMatrix (h.collectedBasis (α := fun (i : ι) ↦ Free.ChooseBasisIndex R ↥(N i)) b)
            (h.collectedBasis (α := fun (i : ι) ↦ Free.ChooseBasisIndex R ↥(N i)) b) :
          (a : M →ₗ[R] M) →
            Matrix ((i : ι) × Free.ChooseBasisIndex R ↥(N i)) ((i : ι) × Free.ChooseBasisIndex R ↥(N i)) R)
        f))
    (∑ i : ι, (trace R ↥(N i) : (a : ↥(N i) →ₗ[R] ↥(N i)) → R) (f.restrict ⋯))
simp_rw₁ :
  Eq.{u_2 + 1} (α := R)
    (Matrix.trace (n := (i : ι) × Free.ChooseBasisIndex R ↥(N i))
      (Matrix.blockDiagonal' (m' := fun (i : ι) ↦ Free.ChooseBasisIndex R ↥(N i)) (n' := fun (i : ι) ↦
        Free.ChooseBasisIndex R ↥(N i)) fun (i : ι) ↦
        (toMatrix (b i) (b i) :
            (a : ↥(N i) →ₗ[R] ↥(N i)) → Matrix (Free.ChooseBasisIndex R ↥(N i)) (Free.ChooseBasisIndex R ↥(N i)) R)
          (f.restrict ⋯)))
    (∑ i : ι, (trace R ↥(N i) : (a : ↥(N i) →ₗ[R] ↥(N i)) → R) (f.restrict ⋯))
⊢ Eq.{u_2 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R)
    (∑ i : ι, (trace R ↥(N i) : (a : ↥(N i) →ₗ[R] ↥(N i)) → R) (f.restrict ⋯) : R)
have simp_rw₂ : Eq.{u_2 + 1} (α := R)
  (∑ i : ι,
    Matrix.trace.{u_3, u_2} (n := Free.ChooseBasisIndex R ↥(N i))
      ((toMatrix (b i) (b i) :
          (a : ↥(N i) →ₗ[R] ↥(N i)) → Matrix (Free.ChooseBasisIndex R ↥(N i)) (Free.ChooseBasisIndex R ↥(N i)) R)
        (f.restrict sorry)))
  (∑ i : ι, (trace R ↥(N i) : (a : ↥(N i) →ₗ[R] ↥(N i)) → R) (f.restrict sorry))
Tactic: simp_rw [trace_eq_matrix_trace R (h.collectedBasis b),
    toMatrix_directSum_collectedBasis_eq_blockDiagonal' h h b b hf, Matrix.trace_blockDiagonal',
    ← trace_eq_matrix_trace]
-- 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 : DecidableEq ι
inst_4 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_5 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
h : IsInternal N
hN : Set.Finite.{u_1} (α := ι) {i : ι | N i ≠ ⊥}
f : M →ₗ[R] M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N i) : Set M)
x : Fintype { i : ι // N i ≠ ⊥ } := hN.fintype (s := {i : ι | N i ≠ ⊥})
x_1 : Fintype (↑{i : ι | N i ≠ ⊥} : Type u_1) := hN.fintype (s := {i : ι | N i ≠ ⊥})
⊢ Eq.{u_2 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R)
    (∑ i ∈ hN.toFinset (s := {i : ι | N i ≠ ⊥}), (trace R ↥(N i) : (a : ↥(N i) →ₗ[R] ↥(N i)) → R) (f.restrict ⋯) : R)
have rw : Eq.{u_2 + 1} (α := R)
  (∑ i : { i : ι // N i ≠ ⊥ }, (trace R ↥(N (↑i : ι)) : (a : ↥(N (↑i : ι)) →ₗ[R] ↥(N (↑i : ι))) → R) (f.restrict sorry))
  (∑ i : ↥hN.toFinset, (trace R ↥(N (↑i : ι)) : (a : ↥(N (↑i : ι)) →ₗ[R] ↥(N (↑i : ι))) → R) (f.restrict sorry))
Tactic: rw [← Finset.sum_coe_sort, trace_eq_sum_trace_restrict (isInternal_ne_bot_iff.mpr h) (hf ·)]
-- 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 : DecidableEq ι
inst_4 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_5 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
h : IsInternal N
inst_6 : IsNoetherian R M
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N (σ i)) : Set M)
⊢ Eq.{u_2 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R) (0 : R)
have hN : Set.Finite.{u_1} (α := ι) {i : ι | N i ≠ ⊥}
Tactic: have hN : {i | N i ≠ ⊥}.Finite := WellFoundedGT.finite_ne_bot_of_iSupIndep
    h.submodule_iSupIndep
-- 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 : DecidableEq ι
inst_4 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_5 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
h : IsInternal N
inst_6 : IsNoetherian R M
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N (σ i)) : Set M)
hN : Set.Finite.{u_1} (α := ι) {i : ι | N i ≠ ⊥}
s : Finset ι := hN.toFinset (s := {i : ι | N i ≠ ⊥})
κ : (i : ι) → Type u_3 := fun (i : ι) ↦ Free.ChooseBasisIndex R ↥(N i)
b : (i : ↥s) → Basis.{u_3, u_2, u_3} (κ (↑i : ι)) R ↥(N (↑i : ι)) := fun (i : ↥s) ↦ Free.chooseBasis R ↥(N (↑i : ι))
⊢ IsInternal (S := Submodule R M) fun (i : ↥s) ↦ N (↑i : ι)
have h₁ : ∀ (x : ι), x ∈ s ↔ N x ≠ ⊥
Tactic: convert! DirectSum.isInternal_ne_bot_iff.mpr 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 : DecidableEq ι
inst_4 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_5 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
h : IsInternal N
inst_6 : IsNoetherian R M
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N (σ i)) : Set M)
hN : Set.Finite.{u_1} (α := ι) {i : ι | N i ≠ ⊥}
s : Finset ι := hN.toFinset (s := {i : ι | N i ≠ ⊥})
κ : (i : ι) → Type u_3 := fun (i : ι) ↦ Free.ChooseBasisIndex R ↥(N i)
b : (i : ↥s) → Basis.{u_3, u_2, u_3} (κ (↑i : ι)) R ↥(N (↑i : ι)) := fun (i : ↥s) ↦ Free.chooseBasis R ↥(N (↑i : ι))
h₁ : ∀ (x : ι), x ∈ s ↔ N x ≠ ⊥
⊢ IsInternal (S := Submodule R M) fun (i : ↥s) ↦ N (↑i : ι)
have h₂ : ↥s = { i : ι // N i ≠ ⊥ } → ∀ (a : ↥s) (a' : { i : ι // N i ≠ ⊥ }), a ≍ a' → ∀ (x : ι), x ∈ s ↔ N x ≠ ⊥
Tactic: convert! DirectSum.isInternal_ne_bot_iff.mpr 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 : DecidableEq ι
inst_4 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_5 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
h : IsInternal N
inst_6 : IsNoetherian R M
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N (σ i)) : Set M)
hN : Set.Finite.{u_1} (α := ι) {i : ι | N i ≠ ⊥}
s : Finset ι := hN.toFinset (s := {i : ι | N i ≠ ⊥})
κ : (i : ι) → Type u_3 := fun (i : ι) ↦ Free.ChooseBasisIndex R ↥(N i)
b : (i : ↥s) → Basis.{u_3, u_2, u_3} (κ (↑i : ι)) R ↥(N (↑i : ι)) := fun (i : ↥s) ↦ Free.chooseBasis R ↥(N (↑i : ι))
⊢ Eq.{u_2 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R) (0 : R)
have h₁ : IsInternal (S := Submodule R M) fun (i : ↥s) ↦ N (↑i : ι)
Tactic: replace h : IsInternal fun i : s ↦ N i := by
    convert! DirectSum.isInternal_ne_bot_iff.mpr h <;> simp [s]
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 : DecidableEq ι
inst_4 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_5 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
inst_6 : IsNoetherian R M
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N (σ i)) : Set M)
hN : Set.Finite.{u_1} (α := ι) {i : ι | N i ≠ ⊥}
s : Finset ι := hN.toFinset (s := {i : ι | N i ≠ ⊥})
κ : (i : ι) → Type u_3 := fun (i : ι) ↦ Free.ChooseBasisIndex R ↥(N i)
b : (i : ↥s) → Basis.{u_3, u_2, u_3} (κ (↑i : ι)) R ↥(N (↑i : ι)) := fun (i : ↥s) ↦ Free.chooseBasis R ↥(N (↑i : ι))
h : IsInternal (S := Submodule R M) fun (i : ↥s) ↦ N (↑i : ι)
⊢ Eq.{u_2 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R) (0 : R)
have simp_rw : Eq.{u_2 + 1} (α := R)
  (Matrix.trace (n := (i : ↥s) × κ (↑i : ι))
    ((toMatrix (h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b)
          (h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b) :
        (a : M →ₗ[R] M) → Matrix ((i : ↥s) × κ (↑i : ι)) ((i : ↥s) × κ (↑i : ι)) R)
      f))
  0
Tactic: simp_rw [trace_eq_matrix_trace R (h.collectedBasis b), Matrix.trace,
    diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_ne h b σ hσ hf (by simp [s]),
    Pi.zero_apply, Finset.sum_const_zero]
-- 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 : DecidableEq ι
inst_4 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_5 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
inst_6 : IsNoetherian R M
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N (σ i)) : Set M)
hN : Set.Finite.{u_1} (α := ι) {i : ι | N i ≠ ⊥}
s : Finset ι := hN.toFinset (s := {i : ι | N i ≠ ⊥})
κ : (i : ι) → Type u_3 := fun (i : ι) ↦ Free.ChooseBasisIndex R ↥(N i)
b : (i : ↥s) → Basis.{u_3, u_2, u_3} (κ (↑i : ι)) R ↥(N (↑i : ι)) := fun (i : ↥s) ↦ Free.chooseBasis R ↥(N (↑i : ι))
h : IsInternal (S := Submodule R M) fun (i : ↥s) ↦ N (↑i : ι)
simp_rw :
  Eq.{u_2 + 1} (α := R)
    (Matrix.trace (n := (i : ↥s) × κ (↑i : ι))
      ((toMatrix (h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b)
            (h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b) :
          (a : M →ₗ[R] M) → Matrix ((i : ↥s) × κ (↑i : ι)) ((i : ↥s) × κ (↑i : ι)) R)
        f))
    0
⊢ Eq.{u_2 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R) (0 : R)
have simp_rw₁ : Eq.{u_2 + 1} (α := R)
  (∑ i : (i : ↥s) × κ (↑i : ι),
    Matrix.diag
      ((toMatrix (h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b)
            (h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b) :
          (a : M →ₗ[R] M) → Matrix ((i : ↥s) × κ (↑i : ι)) ((i : ↥s) × κ (↑i : ι)) R)
        f)
      i)
  0
Tactic: simp_rw [trace_eq_matrix_trace R (h.collectedBasis b), Matrix.trace,
    diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_ne h b σ hσ hf (by simp [s]),
    Pi.zero_apply, Finset.sum_const_zero]
-- 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 : DecidableEq ι
inst_4 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_5 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
inst_6 : IsNoetherian R M
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N (σ i)) : Set M)
hN : Set.Finite.{u_1} (α := ι) {i : ι | N i ≠ ⊥}
s : Finset ι := hN.toFinset (s := {i : ι | N i ≠ ⊥})
κ : (i : ι) → Type u_3 := fun (i : ι) ↦ Free.ChooseBasisIndex R ↥(N i)
b : (i : ↥s) → Basis.{u_3, u_2, u_3} (κ (↑i : ι)) R ↥(N (↑i : ι)) := fun (i : ↥s) ↦ Free.chooseBasis R ↥(N (↑i : ι))
h : IsInternal (S := Submodule R M) fun (i : ↥s) ↦ N (↑i : ι)
simp_rw :
  Eq.{u_2 + 1} (α := R)
    (Matrix.trace (n := (i : ↥s) × κ (↑i : ι))
      ((toMatrix (h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b)
            (h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b) :
          (a : M →ₗ[R] M) → Matrix ((i : ↥s) × κ (↑i : ι)) ((i : ↥s) × κ (↑i : ι)) R)
        f))
    0
simp_rw₁ :
  Eq.{u_2 + 1} (α := R)
    (∑ i : (i : ↥s) × κ (↑i : ι),
      Matrix.diag
        ((toMatrix (h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b)
              (h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b) :
            (a : M →ₗ[R] M) → Matrix ((i : ↥s) × κ (↑i : ι)) ((i : ↥s) × κ (↑i : ι)) R)
          f)
        i)
    0
⊢ Eq.{u_2 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R) (0 : R)
have simp_rw₂ : Eq.{u_2 + 1} (α := R) (∑ x : (i : ↥s) × κ (↑i : ι), 0 x) 0
Tactic: simp_rw [trace_eq_matrix_trace R (h.collectedBasis b), Matrix.trace,
    diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_ne h b σ hσ hf (by simp [s]),
    Pi.zero_apply, Finset.sum_const_zero]
-- 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 : DecidableEq ι
inst_4 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_5 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
inst_6 : IsNoetherian R M
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N (σ i)) : Set M)
hN : Set.Finite.{u_1} (α := ι) {i : ι | N i ≠ ⊥}
s : Finset ι := hN.toFinset (s := {i : ι | N i ≠ ⊥})
κ : (i : ι) → Type u_3 := fun (i : ι) ↦ Free.ChooseBasisIndex R ↥(N i)
b : (i : ↥s) → Basis.{u_3, u_2, u_3} (κ (↑i : ι)) R ↥(N (↑i : ι)) := fun (i : ↥s) ↦ Free.chooseBasis R ↥(N (↑i : ι))
h : IsInternal (S := Submodule R M) fun (i : ↥s) ↦ N (↑i : ι)
simp_rw :
  Eq.{u_2 + 1} (α := R)
    (Matrix.trace (n := (i : ↥s) × κ (↑i : ι))
      ((toMatrix (h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b)
            (h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b) :
          (a : M →ₗ[R] M) → Matrix ((i : ↥s) × κ (↑i : ι)) ((i : ↥s) × κ (↑i : ι)) R)
        f))
    0
simp_rw₁ :
  Eq.{u_2 + 1} (α := R)
    (∑ i : (i : ↥s) × κ (↑i : ι),
      Matrix.diag
        ((toMatrix (h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b)
              (h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b) :
            (a : M →ₗ[R] M) → Matrix ((i : ↥s) × κ (↑i : ι)) ((i : ↥s) × κ (↑i : ι)) R)
          f)
        i)
    0
simp_rw₂ : Eq.{u_2 + 1} (α := R) (∑ x : (i : ↥s) × κ (↑i : ι), 0 x) 0
⊢ Eq.{u_2 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R) (0 : R)
have simp_rw₃ : Eq.{u_2 + 1} (α := R) (∑ x : (i : ↥s) × κ (↑i : ι), 0) 0
Tactic: simp_rw [trace_eq_matrix_trace R (h.collectedBasis b), Matrix.trace,
    diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_ne h b σ hσ hf (by simp [s]),
    Pi.zero_apply, Finset.sum_const_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
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)
⊢ Eq.{u_2 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (g ∘ₗ f) : R) (0 : R)
have hfg : ∀ (μ : R), MapsTo (⇑(g ∘ₗ f) : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
Tactic: have hfg : ∀ μ,
      MapsTo (g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ) :=
    fun μ ↦ (f.mapsTo_maxGenEigenspace_of_comm h_comm μ).comp
      (f.mapsTo_maxGenEigenspace_of_comm rfl μ)
-- 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)
this :
  ∀ (μ : R),
    Eq.{u_2 + 1} (α := R)
      ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
          ((g ∘ₗ f).restrict ⋯) :
        R)
      (0 : R)
⊢ Eq.{u_2 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (g ∘ₗ f) : R) (0 : R)
have hds : IsInternal f.maxGenEigenspace
Tactic: have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top
      f.independent_maxGenEigenspace hf
-- 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)
this :
  ∀ (μ : R),
    Eq.{u_2 + 1} (α := R)
      ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
          ((g ∘ₗ f).restrict ⋯) :
        R)
      (0 : R)
hds : IsInternal f.maxGenEigenspace
⊢ Eq.{u_2 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (g ∘ₗ f) : R) (0 : R)
have h_fin : Set.Finite.{u_2} (α := R) {μ : R | f.maxGenEigenspace μ ≠ ⊥}
Tactic: have h_fin : {μ | f.maxGenEigenspace μ ≠ ⊥}.Finite :=
      WellFoundedGT.finite_ne_bot_of_iSupIndep f.independent_maxGenEigenspace
-- 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 : 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)
this :
  ∀ (μ : R),
    Eq.{u_2 + 1} (α := R)
      ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
          ((g ∘ₗ f).restrict ⋯) :
        R)
      (0 : R)
⊢ Eq.{u_2 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (g ∘ₗ f) : R) (0 : R)
have have : ∀ (hds : IsInternal f.maxGenEigenspace), Eq.{u_2 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (g ∘ₗ f) : R) (0 : R)
Tactic: classical
    have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top
      f.independent_maxGenEigenspace hf
    have h_fin : {μ | f.maxGenEigenspace μ ≠ ⊥}.Finite :=
      WellFoundedGT.finite_ne_bot_of_iSupIndep f.independent_maxGenEigenspace
    simp [trace_eq_sum_trace_restrict' hds h_fin hfg, this]
-- 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 : 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)
this :
  ∀ (μ : R),
    Eq.{u_2 + 1} (α := R)
      ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
          ((g ∘ₗ f).restrict ⋯) :
        R)
      (0 : R)
have have₁ have₂ :
  ∀ (hds : IsInternal f.maxGenEigenspace),
    Eq.{u_2 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (g ∘ₗ f) : R) (0 : R)
⊢ Eq.{u_2 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (g ∘ₗ f) : R) (0 : R)
have have₃ : ∀ (hds : IsInternal f.maxGenEigenspace) (h_fin : Set.Finite.{u_2} (α := R) {μ : R | f.maxGenEigenspace μ ≠ ⊥}),
  Eq.{u_2 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (g ∘ₗ f) : R) (0 : R)
Tactic: classical
    have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top
      f.independent_maxGenEigenspace hf
    have h_fin : {μ | f.maxGenEigenspace μ ≠ ⊥}.Finite :=
      WellFoundedGT.finite_ne_bot_of_iSupIndep f.independent_maxGenEigenspace
    simp [trace_eq_sum_trace_restrict' hds h_fin hfg, this]
-- 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 : 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)
⊢ Eq.{u_2 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (g ∘ₗ f) : R) (0 : R)
have suffices : ∀ (μ : R),
  Eq.{u_2 + 1} (α := R)
    ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
        ((g ∘ₗ f).restrict sorry) :
      R)
    (0 : R)
Tactic: suffices ∀ μ, trace R _ ((g ∘ₗ f).restrict (hfg μ)) = 0 by
    classical
    have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top
      f.independent_maxGenEigenspace hf
    have h_fin : {μ | f.maxGenEigenspace μ ≠ ⊥}.Finite :=
      WellFoundedGT.finite_ne_bot_of_iSupIndep f.independent_maxGenEigenspace
    simp [trace_eq_sum_trace_restrict' hds h_fin hfg, this]
-- 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
⊢ Eq.{u_2 + 1} (α := R)
    ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
        ((g ∘ₗ f).restrict ⋯) :
      R)
    (0 : R)
have hf' : MapsTo (⇑f : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
Tactic: have hf' := f.mapsTo_maxGenEigenspace_of_comm (Commute.refl _) μ
-- 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)
⊢ Eq.{u_2 + 1} (α := R)
    ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
        ((g ∘ₗ f).restrict ⋯) :
      R)
    (0 : R)
have hg' : MapsTo (⇑g : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
Tactic: have hg' := f.mapsTo_maxGenEigenspace_of_comm h_comm μ