awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ 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₁ : ∀ (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)
Tactic: refine Finset.sum_eq_zero fun ⟨i, j⟩ hij ↦ ?_
-- 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_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)
⊢ 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)
have 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
Tactic: rw [LinearMap.smul_apply, this, 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₂ : ℕ∞
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
⊢ 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)
have rw₁ : HSMul.hSMul (β := M) ((l₁ + l₂).choose (i, j).1) 0 = 0
Tactic: rw [LinearMap.smul_apply, this, 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₂ : ℕ∞
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
⊢ 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)
have rw₂ : Eq.{w + 1} (α := M) 0 0
Tactic: rw [LinearMap.smul_apply, this, 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₂ : ℕ∞
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₂)
⊢ 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)
have 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)
Tactic: suffices (((f₁ - μ₁ • 1) ^ i) * ((f₂ - μ₂ • 1) ^ j)) m = 0 by
    rw [LinearMap.smul_apply, this, smul_zero]
-- 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₂ : ℕ∞
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₂)
⊢ 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)
have hij₁ : (i, j).1 + (i, j).2 = l₁ + l₂
Tactic: rw [Finset.mem_antidiagonal] at hij
Cleared hypotheses: hij
-- 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)
x : ℕ × ℕ
i j : ℕ
hij : (i, j).1 + (i, j).2 = l₁ + l₂
⊢ 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)
have 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)
Tactic: obtain hi | hj : l₁ ≤ i ∨ l₂ ≤ j := by lia
-- 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)
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)
⊢ 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)
have 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)
Tactic: obtain hi | hj : l₁ ≤ i ∨ l₂ ≤ j := by lia
-- 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)
x : ℕ × ℕ
i j : ℕ
hij : (i, j).1 + (i, j).2 = l₁ + l₂
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)
have 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)
Tactic: rw [(h.pow_pow i j).eq, Module.End.mul_apply, Module.End.pow_map_zero_of_le hi hl₁, map_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₂ : ℕ∞
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)
⊢ 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)
have 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)
Tactic: rw [(h.pow_pow i j).eq, Module.End.mul_apply, Module.End.pow_map_zero_of_le hi hl₁, map_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₂ : ℕ∞
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)
⊢ 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)
have h₃ : Eq (α := M) (((f₂ - HSMul.hSMul (β := End R M) μ₂ 1) ^ j : (a : M) → M) 0 : 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]
-- 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)
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)
⊢ 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)
have h₄ : Eq.{w + 1} (α := M) 0 0
Tactic: rw [(h.pow_pow i j).eq, Module.End.mul_apply, Module.End.pow_map_zero_of_le hi hl₁, map_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₂ : ℕ∞
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
⊢ 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)
have 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)
Tactic: rw [Module.End.mul_apply, Module.End.pow_map_zero_of_le hj hl₂, map_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₂ : ℕ∞
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)
⊢ 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)
have h₂ : Eq (α := M) (((f₁ - HSMul.hSMul (β := End R M) μ₁ 1) ^ i : (a : M) → M) 0 : M) (0 : M)
Tactic: rw [Module.End.mul_apply, Module.End.pow_map_zero_of_le hj hl₂, map_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₂ : ℕ∞
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)
⊢ 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)
have h₃ : Eq.{w + 1} (α := M) 0 0
Tactic: rw [Module.End.mul_apply, Module.End.pow_map_zero_of_le hj hl₂, map_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
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
L : Type u_1
F : Type u_2
inst_5 : SMul R L
inst_6 : FunLike.{u_2 + 1, u_1 + 1, w + 1} F L (End R M)
inst_7 : MulActionHomClass.{u_2, v, u_1, w} F R L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne :
  Ne.{w + 1} (α := Submodule R M)
    (⨅ (x : L), (genEigenspace ((f : (a : L) → End R M) x) (μ x) : (a : ℕ∞) → Submodule R M) k) ⊥
t : R
x : L
⊢ μ (t • x) = t • μ x
have by_contra : ∀ (contra : ¬μ (t • x) = t • μ x), False
Tactic: by_contra contra
-- 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
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
L : Type u_1
F : Type u_2
inst_5 : SMul R L
inst_6 : FunLike.{u_2 + 1, u_1 + 1, w + 1} F L (End R M)
inst_7 : MulActionHomClass.{u_2, v, u_1, w} F R L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne :
  Ne.{w + 1} (α := Submodule R M)
    (⨅ (x : L), (genEigenspace ((f : (a : L) → End R M) x) (μ x) : (a : ℕ∞) → Submodule R M) k) ⊥
t : R
x : L
contra : ¬μ (t • x) = t • μ x
g : L → Submodule R M := fun (x : L) ↦ (genEigenspace ((f : (a : L) → End R M) x) (μ x) : (a : ℕ∞) → Submodule R M) k
⊢ False
have this : ⨅ (x : L), g x ≤ g x ⊓ g (t • x)
Tactic: have : ⨅ x, g x ≤ g x ⊓ g (t • x) := le_inf_iff.mpr ⟨iInf_le g x, iInf_le g (t • x)⟩
-- 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
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
L : Type u_1
F : Type u_2
inst_5 : SMul R L
inst_6 : FunLike.{u_2 + 1, u_1 + 1, w + 1} F L (End R M)
inst_7 : MulActionHomClass.{u_2, v, u_1, w} F R L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne :
  Ne.{w + 1} (α := Submodule R M)
    (⨅ (x : L), (genEigenspace ((f : (a : L) → End R M) x) (μ x) : (a : ℕ∞) → Submodule R M) k) ⊥
t : R
x : L
contra : ¬μ (t • x) = t • μ x
g : L → Submodule R M := fun (x : L) ↦ (genEigenspace ((f : (a : L) → End R M) x) (μ x) : (a : ℕ∞) → Submodule R M) k
this : ⨅ (x : L), g x ≤ g x ⊓ g (t • x)
⊢ False
have refine : Disjoint (g x) (g (t • x))
Tactic: refine h_ne <| eq_bot_iff.mpr (le_trans this (disjoint_iff_inf_le.mp ?_))
-- 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
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
L : Type u_1
F : Type u_2
inst_5 : SMul R L
inst_6 : FunLike.{u_2 + 1, u_1 + 1, w + 1} F L (End R M)
inst_7 : MulActionHomClass.{u_2, v, u_1, w} F R L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne :
  Ne.{w + 1} (α := Submodule R M)
    (⨅ (x : L), (genEigenspace ((f : (a : L) → End R M) x) (μ x) : (a : ℕ∞) → Submodule R M) k) ⊥
t : R
x : L
contra : ¬μ (t • x) = t • μ x
g : L → Submodule R M := fun (x : L) ↦ (genEigenspace ((f : (a : L) → End R M) x) (μ x) : (a : ℕ∞) → Submodule R M) k
this : ⨅ (x : L), g x ≤ g x ⊓ g (t • x)
⊢ Disjoint (g x) (g (t • x))
have apply : Disjoint
  (((HSMul.hSMul (β := End R M) t ((f : (a : L) → End R M) x : End R M)).genEigenspace (t * μ x) :
      (a : ℕ∞) → Submodule R M)
    k)
  (g (t • x))
Tactic: apply Disjoint.mono_left (genEigenspace_le_smul (f x) (μ x) t k)
-- 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
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
L : Type u_1
F : Type u_2
inst_5 : SMul R L
inst_6 : FunLike.{u_2 + 1, u_1 + 1, w + 1} F L (End R M)
inst_7 : MulActionHomClass.{u_2, v, u_1, w} F R L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne :
  Ne.{w + 1} (α := Submodule R M)
    (⨅ (x : L), (genEigenspace ((f : (a : L) → End R M) x) (μ x) : (a : ℕ∞) → Submodule R M) k) ⊥
t : R
x : L
contra : ¬μ (t • x) = t • μ x
g : L → Submodule R M := fun (x : L) ↦ (genEigenspace ((f : (a : L) → End R M) x) (μ x) : (a : ℕ∞) → Submodule R M) k
this : ⨅ (x : L), g x ≤ g x ⊓ g (t • x)
⊢ Disjoint
    (((HSMul.hSMul (β := End R M) t ((f : (a : L) → End R M) x : End R M)).genEigenspace (t * μ x) :
        (a : ℕ∞) → Submodule R M)
      k)
    (g (t • x))
have simp : Disjoint (α := Submodule R M)
  (((HSMul.hSMul (β := End R M) t ((f : (a : L) → End R M) x : End R M)).genEigenspace (t * μ x) :
        (a : ℕ∞) → Submodule R M)
      k :
    Submodule R M)
  (((HSMul.hSMul (β := End R M) t ((f : (a : L) → End R M) x : End R M)).genEigenspace (μ (t • x)) :
        (a : ℕ∞) → Submodule R M)
      k :
    Submodule R M)
Tactic: simp only [g, map_smul]