awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
μ : K
⊢ Submodule.comap ((f - HSMul.hSMul (β := End K V) μ 1) ^ finrank K V)
      ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞)) =
    (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ finrank K V *
        HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ finrank K V).ker
have rw : (((f - HSMul.hSMul (β := End K V) μ 1) ^ finrank K V) ∘ₗ (f - HSMul.hSMul (β := End K V) μ 1) ^ finrank K V).ker =
  (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ finrank K V *
      HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ finrank K V).ker
Tactic: rw [genEigenspace_nat, ← LinearMap.ker_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
μ : K
⊢ (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ finrank K V *
        HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ finrank K V).ker =
    (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V + finrank K V) : ℕ∞)
have simp_rw : LinearMap.ker
    (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^
      (finrank K V + finrank K V)) =
  ((f - HSMul.hSMul (β := End K V) μ 1) ^ (finrank K V + finrank K V)).ker
Tactic: simp_rw [← pow_add, genEigenspace_nat]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
μ : K
⊢ Eq (α := Submodule K V)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V + finrank K V) : ℕ∞) : Submodule K V)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞) : Submodule K V)
have hk : finrank K V ≤ finrank K V + finrank K V
Tactic: rw [genEigenspace_eq_genEigenspace_finrank_of_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (hypothesis)
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
μ : K
⊢ Disjoint (f.genEigenrange μ (↑(finrank K V) : ℕ∞))
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞))
have h : Submodule.comap ((f - HSMul.hSMul (β := End K V) μ 1) ^ finrank K V)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞)) =
  (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞)
Tactic: have h :=
    calc
      Submodule.comap ((f - μ • 1) ^ finrank K V)
        (f.genEigenspace μ (finrank K V)) =
          LinearMap.ker ((f - algebraMap _ _ μ) ^ finrank K V *
            (f - algebraMap K (End K V) μ) ^ finrank K V) := by
              rw [genEigenspace_nat, ← LinearMap.ker_comp]; rfl
      _ = f.genEigenspace μ (finrank K V + finrank K V : ℕ) := by
              simp_rw [← pow_add, genEigenspace_nat]; rfl
      _ = f.genEigenspace μ (finrank K V) := by
              rw [genEigenspace_eq_genEigenspace_finrank_of_le]; lia
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
μ : K
h :
  Submodule.comap ((f - HSMul.hSMul (β := End K V) μ 1) ^ finrank K V)
      ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞)) =
    (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞)
⊢ Disjoint (f.genEigenrange μ (↑(finrank K V) : ℕ∞))
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞))
have rw : Submodule.map ((f - HSMul.hSMul (β := End K V) μ 1) ^ finrank K V)
    ((f - HSMul.hSMul (β := End K V) μ 1) ^ finrank K V).ker ≤
  ⊥
Tactic: rw [disjoint_iff_inf_le, genEigenrange_nat, LinearMap.range_eq_map,
    Submodule.map_inf_eq_map_inf_comap, top_inf_eq, h, genEigenspace_nat]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
p : Submodule R M
hfp : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
μ : R
hμp : Disjoint (f.eigenspace μ) p
⊢ eigenspace (LinearMap.restrict f hfp) μ = ⊥
have rw : eigenspace (LinearMap.restrict f hfp) μ ≤ ⊥
Tactic: rw [eq_bot_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
k : ℕ
μ : K
hx : f.HasEigenvalue μ
hk : 0 < k
⊢ 0 = finrank.{v, w} K ↥⊥
have rw : Eq (α := ℕ) 0 0
Tactic: rw [finrank_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
μ : K
n : ℕ
⊢ Submodule.map f (f.genEigenrange μ (↑n : ℕ∞)) =
    (f * HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ n).range
have rw : Submodule.map f ((f - HSMul.hSMul (β := End K V) μ 1) ^ n).range =
  (f * HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ n).range
Tactic: rw [genEigenrange_nat]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
μ : K
n : ℕ
⊢ (f * HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ n).range =
    (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ n * f).range
have rw : LinearMap.range (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ n * f) =
  (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ n * f).range
Tactic: rw [Algebra.mul_sub_algebraMap_pow_commutes]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
μ : K
n : ℕ
⊢ Submodule.map (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ n)
      (LinearMap.range f) ≤
    f.genEigenrange μ (↑n : ℕ∞)
have rw : Submodule.map (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ n)
    (LinearMap.range f) ≤
  ((f - HSMul.hSMul (β := End K V) μ 1) ^ n).range
Tactic: rw [genEigenrange_nat]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ t : R
k : ℕ∞
m : M
hm : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) m
⊢ Membership.mem (γ := Submodule R M) (((t • f).genEigenspace (t * μ) : (a : ℕ∞) → Submodule R M) k : Submodule R M) m
have simp_rw : ∀
  (hm :
    ∃ (l : ℕ) (_ : (↑l : ℕ∞) ≤ k),
      Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) m : M) (0 : M)),
  ∃ (l : ℕ) (_ : (↑l : ℕ∞) ≤ k),
    Eq (α := M) (((t • f - HSMul.hSMul (β := End R M) (t * μ) 1) ^ l : (a : M) → M) m : M) (0 : M)
Tactic: simp_rw [mem_genEigenspace, ← exists_prop, LinearMap.mem_ker] at hm ⊢
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ t : R
k : ℕ∞
m : M
hm : ∃ (l : ℕ) (_ : (↑l : ℕ∞) ≤ k), Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) m : M) (0 : M)
⊢ ∃ (l : ℕ) (_ : (↑l : ℕ∞) ≤ k),
    Eq (α := M) (((t • f - HSMul.hSMul (β := End R M) (t * μ) 1) ^ l : (a : M) → M) m : M) (0 : M)
have h : ∀ (l : ℕ) (hlk : (↑l : ℕ∞) ≤ k)
  (hl : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) m : M) (0 : M)),
  Eq (α := M) (((t • f - HSMul.hSMul (β := End R M) (t * μ) 1) ^ l : (a : M) → M) m : M) (0 : M)
Tactic: peel hm with l hlk hl
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ t : R
k : ℕ∞
m : M
hm : ∃ (l : ℕ) (_ : (↑l : ℕ∞) ≤ k), Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) m : M) (0 : M)
l : ℕ
hlk : (↑l : ℕ∞) ≤ k
hl : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) m : M) (0 : M)
⊢ Eq (α := M) (((t • f - HSMul.hSMul (β := End R M) (t * μ) 1) ^ l : (a : M) → M) m : M) (0 : M)
have h : Eq (α := M) (((t • f - t • HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) m : M) (0 : M)
Tactic: rw [mul_smul, ← smul_sub, smul_pow, LinearMap.smul_apply, hl, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ t : R
k : ℕ∞
m : M
hm : ∃ (l : ℕ) (_ : (↑l : ℕ∞) ≤ k), Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) m : M) (0 : M)
l : ℕ
hlk : (↑l : ℕ∞) ≤ k
hl : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) m : M) (0 : M)
h : Eq (α := M) (((t • f - t • HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) m : M) (0 : M)
⊢ Eq (α := M) (((t • f - HSMul.hSMul (β := End R M) (t * μ) 1) ^ l : (a : M) → M) m : M) (0 : M)
have h₁ : Eq (α := M) (((t • (f - HSMul.hSMul (β := End R M) μ 1)) ^ l : (a : M) → M) m : M) (0 : M)
Tactic: rw [mul_smul, ← smul_sub, smul_pow, LinearMap.smul_apply, hl, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ t : R
k : ℕ∞
m : M
hm : ∃ (l : ℕ) (_ : (↑l : ℕ∞) ≤ k), Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) m : M) (0 : M)
l : ℕ
hlk : (↑l : ℕ∞) ≤ k
hl : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) m : M) (0 : M)
h : Eq (α := M) (((t • f - t • HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) m : M) (0 : M)
h₁ : Eq (α := M) (((t • (f - HSMul.hSMul (β := End R M) μ 1)) ^ l : (a : M) → M) m : M) (0 : M)
⊢ Eq (α := M) (((t • f - HSMul.hSMul (β := End R M) (t * μ) 1) ^ l : (a : M) → M) m : M) (0 : M)
have h₂ : Eq (α := M) ((t ^ l • (f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) m : M) (0 : M)
Tactic: rw [mul_smul, ← smul_sub, smul_pow, LinearMap.smul_apply, hl, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ t : R
k : ℕ∞
m : M
hm : ∃ (l : ℕ) (_ : (↑l : ℕ∞) ≤ k), Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) m : M) (0 : M)
l : ℕ
hlk : (↑l : ℕ∞) ≤ k
hl : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) m : M) (0 : M)
h : Eq (α := M) (((t • f - t • HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) m : M) (0 : M)
h₁ : Eq (α := M) (((t • (f - HSMul.hSMul (β := End R M) μ 1)) ^ l : (a : M) → M) m : M) (0 : M)
h₂ : Eq (α := M) ((t ^ l • (f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) m : M) (0 : M)
⊢ Eq (α := M) (((t • f - HSMul.hSMul (β := End R M) (t * μ) 1) ^ l : (a : M) → M) m : M) (0 : M)
have h₃ : HSMul.hSMul (β := M) (t ^ l) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) m : M) = 0
Tactic: rw [mul_smul, ← smul_sub, smul_pow, LinearMap.smul_apply, hl, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ t : R
k : ℕ∞
m : M
hm : ∃ (l : ℕ) (_ : (↑l : ℕ∞) ≤ k), Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) m : M) (0 : M)
l : ℕ
hlk : (↑l : ℕ∞) ≤ k
hl : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) m : M) (0 : M)
h : Eq (α := M) (((t • f - t • HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) m : M) (0 : M)
h₁ : Eq (α := M) (((t • (f - HSMul.hSMul (β := End R M) μ 1)) ^ l : (a : M) → M) m : M) (0 : M)
h₂ : Eq (α := M) ((t ^ l • (f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) m : M) (0 : M)
h₃ : HSMul.hSMul (β := M) (t ^ l) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) m : M) = 0
⊢ Eq (α := M) (((t • f - HSMul.hSMul (β := End R M) (t * μ) 1) ^ l : (a : M) → M) m : M) (0 : M)
have h₄ : HSMul.hSMul (β := M) (t ^ l) 0 = 0
Tactic: rw [mul_smul, ← smul_sub, smul_pow, LinearMap.smul_apply, hl, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ t : R
k : ℕ∞
m : M
hm : ∃ (l : ℕ) (_ : (↑l : ℕ∞) ≤ k), Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) m : M) (0 : M)
l : ℕ
hlk : (↑l : ℕ∞) ≤ k
hl : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) m : M) (0 : M)
h : Eq (α := M) (((t • f - t • HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) m : M) (0 : M)
h₁ : Eq (α := M) (((t • (f - HSMul.hSMul (β := End R M) μ 1)) ^ l : (a : M) → M) m : M) (0 : M)
h₂ : Eq (α := M) ((t ^ l • (f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) m : M) (0 : M)
h₃ : HSMul.hSMul (β := M) (t ^ l) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) m : M) = 0
h₄ : HSMul.hSMul (β := M) (t ^ l) 0 = 0
⊢ Eq (α := M) (((t • f - HSMul.hSMul (β := End R M) (t * μ) 1) ^ l : (a : M) → M) m : M) (0 : M)
have h₅ : Eq.{w + 1} (α := M) 0 0
Tactic: rw [mul_smul, ← smul_sub, smul_pow, LinearMap.smul_apply, hl, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
h : Commute f₁ f₂
m : M
hm :
  Membership.mem (γ := Submodule R M)
    ((f₁.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k₁ ⊓ (f₂.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) k₂ :
      Submodule R M)
    m
⊢ Membership.mem (γ := Submodule R M)
    (((f₁ + f₂).genEigenspace (μ₁ + μ₂) : (a : ℕ∞) → Submodule R M) (k₁ + k₂) : Submodule R M) m
have simp : ∀
  (hm :
    (∃ (l : ℕ),
        (↑l : ℕ∞) ≤ k₁ ∧ Eq (α := M) (((f₁ - HSMul.hSMul (β := End R M) μ₁ 1) ^ l : (a : M) → M) m : M) (0 : M)) ∧
      ∃ (l : ℕ),
        (↑l : ℕ∞) ≤ k₂ ∧ Eq (α := M) (((f₂ - HSMul.hSMul (β := End R M) μ₂ 1) ^ l : (a : M) → M) m : M) (0 : M)),
  ∃ (l : ℕ),
    (↑l : ℕ∞) ≤ k₁ + k₂ ∧
      Eq (α := M) (((f₁ + f₂ - HSMul.hSMul (β := End R M) (μ₁ + μ₂) 1) ^ l : (a : M) → M) m : M) (0 : M)
Tactic: simp only [Submodule.mem_inf, mem_genEigenspace, LinearMap.mem_ker] at hm ⊢
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
h : Commute f₁ f₂
m : M
hm :
  (∃ (l : ℕ), (↑l : ℕ∞) ≤ k₁ ∧ Eq (α := M) (((f₁ - HSMul.hSMul (β := End R M) μ₁ 1) ^ l : (a : M) → M) m : M) (0 : M)) ∧
    ∃ (l : ℕ), (↑l : ℕ∞) ≤ k₂ ∧ Eq (α := M) (((f₂ - HSMul.hSMul (β := End R M) μ₂ 1) ^ l : (a : M) → M) m : M) (0 : M)
⊢ ∃ (l : ℕ),
    (↑l : ℕ∞) ≤ k₁ + k₂ ∧
      Eq (α := M) (((f₁ + f₂ - HSMul.hSMul (β := End R M) (μ₁ + μ₂) 1) ^ l : (a : M) → M) m : M) (0 : M)
have obtain : ∀ (l₁ : ℕ) (hlk₁ : (↑l₁ : ℕ∞) ≤ k₁)
  (hl₁ : Eq (α := M) (((f₁ - HSMul.hSMul (β := End R M) μ₁ 1) ^ l₁ : (a : M) → M) m : M) (0 : M)) (l₂ : ℕ)
  (hlk₂ : (↑l₂ : ℕ∞) ≤ k₂)
  (hl₂ : Eq (α := M) (((f₂ - HSMul.hSMul (β := End R M) μ₂ 1) ^ l₂ : (a : M) → M) m : M) (0 : M)),
  ∃ (l : ℕ),
    (↑l : ℕ∞) ≤ k₁ + k₂ ∧
      Eq (α := M) (((f₁ + f₂ - HSMul.hSMul (β := End R M) (μ₁ + μ₂) 1) ^ l : (a : M) → M) m : M) (0 : M)
Tactic: obtain ⟨⟨l₁, hlk₁, hl₁⟩, ⟨l₂, hlk₂, hl₂⟩⟩ := hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
h : Commute f₁ f₂
m : M
l₁ : ℕ
hlk₁ : (↑l₁ : ℕ∞) ≤ k₁
hl₁ : Eq (α := M) (((f₁ - HSMul.hSMul (β := End R M) μ₁ 1) ^ l₁ : (a : M) → M) m : M) (0 : M)
l₂ : ℕ
hlk₂ : (↑l₂ : ℕ∞) ≤ k₂
hl₂ : Eq (α := M) (((f₂ - HSMul.hSMul (β := End R M) μ₂ 1) ^ l₂ : (a : M) → M) m : M) (0 : M)
⊢ ∃ (l : ℕ),
    (↑l : ℕ∞) ≤ k₁ + k₂ ∧
      Eq (α := M) (((f₁ + f₂ - HSMul.hSMul (β := End R M) (μ₁ + μ₂) 1) ^ l : (a : M) → M) m : M) (0 : M)
have h₁ : (↑(l₁ + l₂) : ℕ∞) ≤ k₁ + k₂ ∧
  Eq (α := M) (((f₁ + f₂ - HSMul.hSMul (β := End R M) (μ₁ + μ₂) 1) ^ (l₁ + l₂) : (a : M) → M) m : M) (0 : M)
Tactic: use l₁ + l₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
h : Commute f₁ f₂
m : M
l₁ : ℕ
hlk₁ : (↑l₁ : ℕ∞) ≤ k₁
hl₁ : Eq (α := M) (((f₁ - HSMul.hSMul (β := End R M) μ₁ 1) ^ l₁ : (a : M) → M) m : M) (0 : M)
l₂ : ℕ
hlk₂ : (↑l₂ : ℕ∞) ≤ k₂
hl₂ : Eq (α := M) (((f₂ - HSMul.hSMul (β := End R M) μ₂ 1) ^ l₂ : (a : M) → M) m : M) (0 : M)
⊢ f₁ + f₂ - HSMul.hSMul (β := End R M) (μ₁ + μ₂) 1 =
    f₁ - HSMul.hSMul (β := End R M) μ₁ 1 + (f₂ - HSMul.hSMul (β := End R M) μ₂ 1)
have rw : f₁ + f₂ - (HSMul.hSMul (β := End R M) μ₁ 1 + HSMul.hSMul (β := End R M) μ₂ 1) =
  f₁ - HSMul.hSMul (β := End R M) μ₁ 1 + (f₂ - HSMul.hSMul (β := End R M) μ₂ 1)
Tactic: rw [add_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (hypothesis)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
h : Commute f₁ f₂
m : M
l₁ : ℕ
hlk₁ : (↑l₁ : ℕ∞) ≤ k₁
hl₁ : Eq (α := M) (((f₁ - HSMul.hSMul (β := End R M) μ₁ 1) ^ l₁ : (a : M) → M) m : M) (0 : M)
l₂ : ℕ
hlk₂ : (↑l₂ : ℕ∞) ≤ k₂
hl₂ : Eq (α := M) (((f₂ - HSMul.hSMul (β := End R M) μ₂ 1) ^ l₂ : (a : M) → M) m : M) (0 : M)
⊢ (↑(l₁ + l₂) : ℕ∞) ≤ k₁ + k₂ ∧
    Eq (α := M) (((f₁ + f₂ - HSMul.hSMul (β := End R M) (μ₁ + μ₂) 1) ^ (l₁ + l₂) : (a : M) → M) m : M) (0 : M)
have this : f₁ + f₂ - HSMul.hSMul (β := End R M) (μ₁ + μ₂) 1 =
  f₁ - HSMul.hSMul (β := End R M) μ₁ 1 + (f₂ - HSMul.hSMul (β := End R M) μ₂ 1)
Tactic: have : f₁ + f₂ - (μ₁ + μ₂) • 1 = (f₁ - μ₁ • 1) + (f₂ - μ₂ • 1) := by
    rw [add_smul]; exact add_sub_add_comm f₁ f₂ (μ₁ • 1) (μ₂ • 1)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (hypothesis)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
h : Commute f₁ f₂
m : M
l₁ : ℕ
hlk₁ : (↑l₁ : ℕ∞) ≤ k₁
hl₁ : Eq (α := M) (((f₁ - HSMul.hSMul (β := End R M) μ₁ 1) ^ l₁ : (a : M) → M) m : M) (0 : M)
l₂ : ℕ
hlk₂ : (↑l₂ : ℕ∞) ≤ k₂
hl₂ : Eq (α := M) (((f₂ - HSMul.hSMul (β := End R M) μ₂ 1) ^ l₂ : (a : M) → M) m : M) (0 : M)
this :
  f₁ + f₂ - HSMul.hSMul (β := End R M) (μ₁ + μ₂) 1 =
    f₁ - HSMul.hSMul (β := End R M) μ₁ 1 + (f₂ - HSMul.hSMul (β := End R M) μ₂ 1)
⊢ (↑(l₁ + l₂) : ℕ∞) ≤ k₁ + k₂ ∧
    Eq (α := M) (((f₁ + f₂ - HSMul.hSMul (β := End R M) (μ₁ + μ₂) 1) ^ (l₁ + l₂) : (a : M) → M) m : M) (0 : M)
have h₁ : Commute (f₁ - HSMul.hSMul (β := End R M) μ₁ 1) (f₂ - HSMul.hSMul (β := End R M) μ₂ 1)
Tactic: replace h : Commute (f₁ - μ₁ • 1) (f₂ - μ₂ • 1) :=
    (h.sub_right <| Algebra.commute_algebraMap_right μ₂ f₁).sub_left
      (Algebra.commute_algebraMap_left μ₁ _)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
m : M
l₁ : ℕ
hlk₁ : (↑l₁ : ℕ∞) ≤ k₁
hl₁ : Eq (α := M) (((f₁ - HSMul.hSMul (β := End R M) μ₁ 1) ^ l₁ : (a : M) → M) m : M) (0 : M)
l₂ : ℕ
hlk₂ : (↑l₂ : ℕ∞) ≤ k₂
hl₂ : Eq (α := M) (((f₂ - HSMul.hSMul (β := End R M) μ₂ 1) ^ l₂ : (a : M) → M) m : M) (0 : M)
this :
  f₁ + f₂ - HSMul.hSMul (β := End R M) (μ₁ + μ₂) 1 =
    f₁ - HSMul.hSMul (β := End R M) μ₁ 1 + (f₂ - HSMul.hSMul (β := End R M) μ₂ 1)
h : Commute (f₁ - HSMul.hSMul (β := End R M) μ₁ 1) (f₂ - HSMul.hSMul (β := End R M) μ₂ 1)
⊢ (↑(l₁ + l₂) : ℕ∞) ≤ k₁ + k₂ ∧
    Eq (α := M) (((f₁ + f₂ - HSMul.hSMul (β := End R M) (μ₁ + μ₂) 1) ^ (l₁ + l₂) : (a : M) → M) m : M) (0 : M)
have h₁ : (↑(l₁ + l₂) : ℕ∞) ≤ k₁ + k₂ ∧
  Eq.{w + 1} (α := M)
    (∑ c ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (l₁ + l₂),
      ((l₁ + l₂).choose c.1 •
            ((f₁ - HSMul.hSMul (β := End R M) μ₁ 1) ^ c.1 * (f₂ - HSMul.hSMul (β := End R M) μ₂ 1) ^ c.2) :
          (a : M) → M)
        m)
    0
Tactic: rw [this, h.add_pow', LinearMap.coe_sum, Finset.sum_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
m : M
l₁ : ℕ
hlk₁ : (↑l₁ : ℕ∞) ≤ k₁
hl₁ : Eq (α := M) (((f₁ - HSMul.hSMul (β := End R M) μ₁ 1) ^ l₁ : (a : M) → M) m : M) (0 : M)
l₂ : ℕ
hlk₂ : (↑l₂ : ℕ∞) ≤ k₂
hl₂ : Eq (α := M) (((f₂ - HSMul.hSMul (β := End R M) μ₂ 1) ^ l₂ : (a : M) → M) m : M) (0 : M)
this :
  f₁ + f₂ - HSMul.hSMul (β := End R M) (μ₁ + μ₂) 1 =
    f₁ - HSMul.hSMul (β := End R M) μ₁ 1 + (f₂ - HSMul.hSMul (β := End R M) μ₂ 1)
h : Commute (f₁ - HSMul.hSMul (β := End R M) μ₁ 1) (f₂ - HSMul.hSMul (β := End R M) μ₂ 1)
⊢ (↑(l₁ + l₂) : ℕ∞) ≤ k₁ + k₂ ∧
    Eq.{w + 1} (α := M)
      (∑ c ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (l₁ + l₂),
        ((l₁ + l₂).choose c.1 •
              ((f₁ - HSMul.hSMul (β := End R M) μ₁ 1) ^ c.1 * (f₂ - HSMul.hSMul (β := End R M) μ₂ 1) ^ c.2) :
            (a : M) → M)
          m)
      0
have h₁ : (↑(l₁ + l₂) : ℕ∞) ≤ k₁ + k₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
m : M
l₁ : ℕ
hlk₁ : (↑l₁ : ℕ∞) ≤ k₁
hl₁ : Eq (α := M) (((f₁ - HSMul.hSMul (β := End R M) μ₁ 1) ^ l₁ : (a : M) → M) m : M) (0 : M)
l₂ : ℕ
hlk₂ : (↑l₂ : ℕ∞) ≤ k₂
hl₂ : Eq (α := M) (((f₂ - HSMul.hSMul (β := End R M) μ₂ 1) ^ l₂ : (a : M) → M) m : M) (0 : M)
this :
  f₁ + f₂ - HSMul.hSMul (β := End R M) (μ₁ + μ₂) 1 =
    f₁ - HSMul.hSMul (β := End R M) μ₁ 1 + (f₂ - HSMul.hSMul (β := End R M) μ₂ 1)
h : Commute (f₁ - HSMul.hSMul (β := End R M) μ₁ 1) (f₂ - HSMul.hSMul (β := End R M) μ₂ 1)
h₁ : (↑(l₁ + l₂) : ℕ∞) ≤ k₁ + k₂
⊢ (↑(l₁ + l₂) : ℕ∞) ≤ k₁ + k₂ ∧
    Eq.{w + 1} (α := M)
      (∑ c ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (l₁ + l₂),
        ((l₁ + l₂).choose c.1 •
              ((f₁ - HSMul.hSMul (β := End R M) μ₁ 1) ^ c.1 * (f₂ - HSMul.hSMul (β := End R M) μ₂ 1) ^ c.2) :
            (a : M) → M)
          m)
      0
have h₂ : Eq.{w + 1} (α := M)
  (∑ c ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (l₁ + l₂),
    ((l₁ + l₂).choose c.1 •
          ((f₁ - HSMul.hSMul (β := End R M) μ₁ 1) ^ c.1 * (f₂ - HSMul.hSMul (β := End R M) μ₂ 1) ^ c.2) :
        (a : M) → M)
      m)
  0
Tactic: constructor