awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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
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)
⊢ Membership.mem (γ := Submodule R M) (((t • f).genEigenspace (t * μ) : (a : ℕ∞) → Submodule R M) k : Submodule R M) m

Tactic:
simp_rw [mem_genEigenspace, ← exists_prop, LinearMap.mem_ker] at hm ⊢

Premises used: exists_prop, LinearMap.mem_ker, Module.End.mem_genEigenspace
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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)
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)
⊢ ∃ (l : ℕ) (_ : (↑l : ℕ∞) ≤ k),
    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
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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
h₅ h₆ : Eq.{w + 1} (α := M) 0 0
⊢ Eq (α := M) (((t • f - HSMul.hSMul (β := End R M) (t * μ) 1) ^ l : (a : M) → M) m : M) (0 : M)

Tactic:
rw [mul_smul, ← smul_sub, smul_pow, LinearMap.smul_apply, hl, smul_zero]

Premises used: LinearMap.smul_apply, smul_zero, smul_sub, smul_pow, SemigroupAction.mul_smul
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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
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)
⊢ Membership.mem (γ := Submodule R M)
    (((f₁ + f₂).genEigenspace (μ₁ + μ₂) : (a : ℕ∞) → Submodule R M) (k₁ + k₂) : Submodule R M) m

Tactic:
simp only [Submodule.mem_inf, mem_genEigenspace, LinearMap.mem_ker] at hm ⊢

Premises used: Submodule.mem_inf, LinearMap.mem_ker, Module.End.mem_genEigenspace
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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)
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)
⊢ ∃ (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
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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)
h₁ :
  (↑(l₁ + l₂) : ℕ∞) ≤ k₁ + k₂ ∧
    Eq (α := M) (((f₁ + f₂ - HSMul.hSMul (β := End R M) (μ₁ + μ₂) 1) ^ (l₁ + 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:
use l₁ + l₂
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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)
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)
⊢ f₁ + f₂ - HSMul.hSMul (β := End R M) (μ₁ + μ₂) 1 =
    f₁ - HSMul.hSMul (β := End R M) μ₁ 1 + (f₂ - HSMul.hSMul (β := End R M) μ₂ 1)

Tactic:
rw [add_smul]

Premises used: add_smul
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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 + HSMul.hSMul (β := End R M) μ₂ 1) =
    f₁ - HSMul.hSMul (β := End R M) μ₁ 1 + (f₂ - HSMul.hSMul (β := End R M) μ₂ 1)

Tactic:
add_sub_add_comm f₁ f₂ (μ₁ • 1) (μ₂ • 1)

Premises used: add_sub_add_comm, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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 + HSMul.hSMul (β := End R M) μ₂ 1) =
    f₁ - HSMul.hSMul (β := End R M) μ₁ 1 + (f₂ - HSMul.hSMul (β := End R M) μ₂ 1)

Tactic:
exact add_sub_add_comm f₁ f₂ (μ₁ • 1) (μ₂ • 1)

Premises used: add_sub_add_comm, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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)

Tactic:
have : f₁ + f₂ - (μ₁ + μ₂) • 1 = (f₁ - μ₁ • 1) + (f₂ - μ₂ • 1) := by
    rw [add_smul]; exact add_sub_add_comm f₁ f₂ (μ₁ • 1) (μ₂ • 1)
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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)
⊢ 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 μ₁ _)
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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₂ ∧
    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
⊢ (↑(l₁ + l₂) : ℕ∞) ≤ k₁ + k₂ ∧
    Eq (α := M) (((f₁ + f₂ - HSMul.hSMul (β := End R M) (μ₁ + μ₂) 1) ^ (l₁ + l₂) : (a : M) → M) m : M) (0 : M)

Tactic:
rw [this, h.add_pow', LinearMap.coe_sum, Finset.sum_apply]

Premises used: Finset.sum_apply, LinearMap.coe_sum, Commute.add_pow'
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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₂
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
⊢ (↑(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:
constructor
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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₂

Tactic:
simpa only [Nat.cast_add] using add_le_add hlk₁ hlk₂

Premises used: add_le_add, Nat.cast_add
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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)
⊢ 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:
Finset.sum_eq_zero fun ⟨i, j⟩ hij ↦ ?_

Premises used: Nat.choose, HMul.hMul, Finset.sum_eq_zero, HSub.hSub, Prod.fst, HPow.hPow, HAdd.hAdd, HSMul.hSMul, _private.0.Module.End.genEigenspace_inf_le_add.match_1, OfNat.ofNat, Eq, Prod.snd, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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₁ :
  ∀ (x : ℕ × ℕ) (i j : ℕ) (hij : (i, j) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (l₁ + l₂)),
    Eq (α := M)
      (((l₁ + l₂).choose (i, j).1 •
              ((f₁ - HSMul.hSMul (β := End R M) μ₁ 1) ^ (i, j).1 * (f₂ - HSMul.hSMul (β := End R M) μ₂ 1) ^ (i, j).2) :
            (a : M) → M)
          m :
        M)
      (0 : M)
⊢ 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:
refine Finset.sum_eq_zero fun ⟨i, j⟩ hij ↦ ?_

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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_1 :
  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)
x : ℕ × ℕ
i j : ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (l₁ + l₂)
this :
  Eq (α := M)
    (((f₁ - HSMul.hSMul (β := End R M) μ₁ 1) ^ i * (f₂ - HSMul.hSMul (β := End R M) μ₂ 1) ^ j : (a : M) → M) m : M)
    (0 : M)
rw :
  HSMul.hSMul (β := M) ((l₁ + l₂).choose (i, j).1)
      (((f₁ - HSMul.hSMul (β := End R M) μ₁ 1) ^ (i, j).1 * (f₂ - HSMul.hSMul (β := End R M) μ₂ 1) ^ (i, j).2 :
            (a : M) → M)
          m :
        M) =
    0
rw₁ : HSMul.hSMul (β := M) ((l₁ + l₂).choose (i, j).1) 0 = 0
rw₂ rw₃ : Eq.{w + 1} (α := M) 0 0
⊢ Eq (α := M)
    (((l₁ + l₂).choose (i, j).1 •
            ((f₁ - HSMul.hSMul (β := End R M) μ₁ 1) ^ (i, j).1 * (f₂ - HSMul.hSMul (β := End R M) μ₂ 1) ^ (i, j).2) :
          (a : M) → M)
        m :
      M)
    (0 : M)

Tactic:
rw [LinearMap.smul_apply, this, smul_zero]

Premises used: LinearMap.smul_apply, smul_zero
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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)
x : ℕ × ℕ
i j : ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (l₁ + l₂)
h₁ :
  Eq (α := M)
    (((f₁ - HSMul.hSMul (β := End R M) μ₁ 1) ^ i * (f₂ - HSMul.hSMul (β := End R M) μ₂ 1) ^ j : (a : M) → M) m : M)
    (0 : M)
⊢ Eq (α := M)
    (((l₁ + l₂).choose (i, j).1 •
            ((f₁ - HSMul.hSMul (β := End R M) μ₁ 1) ^ (i, j).1 * (f₂ - HSMul.hSMul (β := End R M) μ₂ 1) ^ (i, j).2) :
          (a : M) → M)
        m :
      M)
    (0 : M)

Tactic:
suffices (((f₁ - μ₁ • 1) ^ i) * ((f₂ - μ₂ • 1) ^ j)) m = 0 by
    rw [LinearMap.smul_apply, this, smul_zero]
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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)
x : ℕ × ℕ
i j : ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (l₁ + l₂)
⊢ (i, j).1 + (i, j).2 = l₁ + l₂

Tactic:
rw [Finset.mem_antidiagonal] at hij

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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)
x : ℕ × ℕ
i j : ℕ
hij : (i, j).1 + (i, j).2 = l₁ + l₂
⊢ l₁ ≤ i ∨ l₂ ≤ j

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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)
x : ℕ × ℕ
i j : ℕ
hij : (i, j).1 + (i, j).2 = l₁ + l₂
h₁ :
  ∀ (hi : l₁ ≤ i),
    Eq (α := M)
      (((f₁ - HSMul.hSMul (β := End R M) μ₁ 1) ^ i * (f₂ - HSMul.hSMul (β := End R M) μ₂ 1) ^ j : (a : M) → M) m : M)
      (0 : M)
h₂ :
  ∀ (hj : l₂ ≤ j),
    Eq (α := M)
      (((f₁ - HSMul.hSMul (β := End R M) μ₁ 1) ^ i * (f₂ - HSMul.hSMul (β := End R M) μ₂ 1) ^ j : (a : M) → M) m : M)
      (0 : M)
⊢ Eq (α := M)
    (((f₁ - HSMul.hSMul (β := End R M) μ₁ 1) ^ i * (f₂ - HSMul.hSMul (β := End R M) μ₂ 1) ^ j : (a : M) → M) m : M)
    (0 : M)

Tactic:
obtain hi | hj : l₁ ≤ i ∨ l₂ ≤ j := by lia
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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)
x : ℕ × ℕ
i j : ℕ
hij : (i, j).1 + (i, j).2 = l₁ + l₂
hi : l₁ ≤ i
h₁ :
  Eq (α := M)
    (((f₂ - HSMul.hSMul (β := End R M) μ₂ 1) ^ j * (f₁ - HSMul.hSMul (β := End R M) μ₁ 1) ^ i : (a : M) → M) m : M)
    (0 : M)
h₂ :
  Eq (α := M)
    (((f₂ - HSMul.hSMul (β := End R M) μ₂ 1) ^ j : (a : M) → M)
        (((f₁ - HSMul.hSMul (β := End R M) μ₁ 1) ^ i : (a : M) → M) m : M) :
      M)
    (0 : M)
h₃ : Eq (α := M) (((f₂ - HSMul.hSMul (β := End R M) μ₂ 1) ^ j : (a : M) → M) 0 : M) (0 : M)
h₄ h₅ : Eq.{w + 1} (α := M) 0 0
⊢ Eq (α := M)
    (((f₁ - HSMul.hSMul (β := End R M) μ₁ 1) ^ i * (f₂ - HSMul.hSMul (β := End R M) μ₂ 1) ^ j : (a : M) → M) m : M)
    (0 : M)

Tactic:
rw [(h.pow_pow i j).eq, Module.End.mul_apply, Module.End.pow_map_zero_of_le hi hl₁, map_zero]

Premises used: Commute.pow_pow, map_zero, Module.End.pow_map_zero_of_le, Module.End.mul_apply, Commute.eq
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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)
x : ℕ × ℕ
i j : ℕ
hij : (i, j).1 + (i, j).2 = l₁ + l₂
hj : l₂ ≤ j
h₁ :
  Eq (α := M)
    (((f₁ - HSMul.hSMul (β := End R M) μ₁ 1) ^ i : (a : M) → M)
        (((f₂ - HSMul.hSMul (β := End R M) μ₂ 1) ^ j : (a : M) → M) m : M) :
      M)
    (0 : M)
h₂ : Eq (α := M) (((f₁ - HSMul.hSMul (β := End R M) μ₁ 1) ^ i : (a : M) → M) 0 : M) (0 : M)
h₃ h₄ : Eq.{w + 1} (α := M) 0 0
⊢ Eq (α := M)
    (((f₁ - HSMul.hSMul (β := End R M) μ₁ 1) ^ i * (f₂ - HSMul.hSMul (β := End R M) μ₂ 1) ^ j : (a : M) → M) m : M)
    (0 : M)

Tactic:
rw [Module.End.mul_apply, Module.End.pow_map_zero_of_le hj hl₂, map_zero]

Premises used: map_zero, Module.End.pow_map_zero_of_le, Module.End.mul_apply