awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Matrix (hypothesis)
Goal:
R : Type u_1
n : Type u_2
M : Type u_3
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : Nontrivial R
inst_4 : AddCommGroup M
inst_5 : Module R M
d : n → R
μ : R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
b : Basis n R M
this_1 : ∀ (i : n), HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ
h_iSup :
  Eq.{u_3 + 1} (α := Submodule R M)
    (⨆ μ ∈ Set.range d, eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) ⊤
hμ_notMem : μ ∉ Set.range d
this :
  Disjoint.{u_3} (α := Submodule R M) (eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ)
    (⨆ i ∈ Set.range d, eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) i)
⊢ False
have this₁ : Eq.{u_3 + 1} (α := Submodule R M) (eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) ⊥
Tactic: rw [h_iSup, disjoint_top] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Matrix (goal)
Goal:
R : Type u_1
n : Type u_2
M : Type u_3
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
d : n → R
b : Basis n R M
⊢ Eq.{u_3 + 1} (α := Submodule R M)
    (⨆ (μ : R), eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) ⊤
have refine : ∀ (j : n),
  Membership.mem.{u_3, u_3} (α := M) (γ := Submodule R M)
    (⨆ (μ : R), eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) ((b : (a : n) → M) j : M)
Tactic: refine (Submodule.eq_top_iff_forall_basis_mem b).mpr fun j ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Matrix (goal)
Goal:
R : Type u_1
n : Type u_2
M : Type u_3
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
d : n → R
μ : R
b : Basis n R M
inst_5 : IsDomain R
⊢ Eq.{u_3 + 1} (α := Submodule R M) (maxGenEigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ)
    (eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ)
have refine : ∀ (x : M)
  (hx :
    Membership.mem (γ := Submodule R M) (maxGenEigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ)
      x),
  Membership.mem (γ := Submodule R M) (eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) x
Tactic: refine le_antisymm (fun x hx ↦ ?_) eigenspace_le_maxGenEigenspace
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Matrix (goal)
Goal:
R : Type u_1
n : Type u_2
M : Type u_3
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
d : n → R
μ : R
b : Basis n R M
inst_5 : IsDomain R
x : M
hx :
  Membership.mem (γ := Submodule R M) (maxGenEigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) x
⊢ Membership.mem (γ := Submodule R M) (eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) x
have obtain : ∀ (k : ℕ)
  (hk :
    Eq (α := M)
      ((HSub.hSub (α := End R M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d) : M →ₗ[R] M)
                (HSMul.hSMul (β := End R M) μ 1) ^
              k :
            (a : M) → M)
          x :
        M)
      (0 : M)),
  Membership.mem (γ := Submodule R M) (eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) x
Tactic: obtain ⟨k, hk⟩ := (mem_maxGenEigenspace _ _ _).mp hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Matrix (goal)
Goal:
R : Type u_1
n : Type u_2
M : Type u_3
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
d : n → R
μ : R
b : Basis n R M
inst_5 : IsDomain R
x : M
hx :
  Membership.mem (γ := Submodule R M) (maxGenEigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) x
k : ℕ
hk :
  Eq (α := M)
    ((HSub.hSub (α := End R M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d) : M →ₗ[R] M)
              (HSMul.hSMul (β := End R M) μ 1) ^
            k :
          (a : M) → M)
        x :
      M)
    (0 : M)
j : n
⊢ HSub.hSub (α := M →ₗ[R] M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d) : M →ₗ[R] M)
      (HSMul.hSMul (β := M →ₗ[R] M) μ 1) =
    (toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal (d - HSMul.hSMul (β := n → R) μ 1))
have rw : HSub.hSub (α := M →ₗ[R] M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d) : M →ₗ[R] M)
    (HSMul.hSMul (β := M →ₗ[R] M) μ 1) =
  (toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d - diagonal (HSMul.hSMul (β := n → R) μ 1))
Tactic: rw [Pi.sub_def, ← diagonal_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Matrix (hypothesis)
Goal:
R : Type u_1
n : Type u_2
M : Type u_3
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
d : n → R
μ : R
b : Basis n R M
inst_5 : IsDomain R
x : M
hx :
  Membership.mem (γ := Submodule R M) (maxGenEigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) x
k : ℕ
hk :
  Eq (α := M)
    ((HSub.hSub (α := End R M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d) : M →ₗ[R] M)
              (HSMul.hSMul (β := End R M) μ 1) ^
            k :
          (a : M) → M)
        x :
      M)
    (0 : M)
j : n
⊢ Eq.{u_1 + 1} (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (0 : R) ∨ d j = μ ∧ k ≠ 0
have aux : HSub.hSub (α := M →ₗ[R] M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d) : M →ₗ[R] M)
    (HSMul.hSMul (β := M →ₗ[R] M) μ 1) =
  (toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal (d - HSMul.hSMul (β := n → R) μ 1))
Tactic: have aux : (diagonal d).toLin b b - μ • 1 = (diagonal (d - μ • 1)).toLin b b := by
      rw [Pi.sub_def, ← diagonal_sub]; simp [one_eq_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Matrix (goal)
Goal:
R : Type u_1
n : Type u_2
M : Type u_3
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
d : n → R
μ : R
b : Basis n R M
inst_5 : IsDomain R
x : M
hx :
  Membership.mem (γ := Submodule R M) (maxGenEigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) x
k : ℕ
hk :
  Eq (α := M)
    ((HSub.hSub (α := End R M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d) : M →ₗ[R] M)
              (HSMul.hSMul (β := End R M) μ 1) ^
            k :
          (a : M) → M)
        x :
      M)
    (0 : M)
j : n
aux :
  HSub.hSub (α := M →ₗ[R] M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d) : M →ₗ[R] M)
      (HSMul.hSMul (β := M →ₗ[R] M) μ 1) =
    (toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal (d - HSMul.hSMul (β := n → R) μ 1))
⊢ Eq.{u_1 + 1} (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (0 : R) ∨ d j = μ ∧ k ≠ 0
have rw : ∀
  (hk :
    ∀ (j : n),
      (diagonal ((d - HSMul.hSMul (β := n → R) μ 1) ^ k) *ᵥ (⇑((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R))
          j =
        0)
  (j : n)
  (aux :
    HSub.hSub (α := M →ₗ[R] M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d) : M →ₗ[R] M)
        (HSMul.hSMul (β := M →ₗ[R] M) μ 1) =
      (toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal (d - HSMul.hSMul (β := n → R) μ 1))),
  Eq.{u_1 + 1} (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (0 : R) ∨ d j = μ ∧ k ≠ 0
Tactic: rw [aux, ← toLin_pow, diagonal_pow, toLin_apply_eq_zero_iff] at hk
Cleared hypotheses: hk, j, aux
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Matrix (hypothesis)
Goal:
R : Type u_1
n : Type u_2
M : Type u_3
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
d : n → R
μ : R
b : Basis n R M
inst_5 : IsDomain R
x : M
hx :
  Membership.mem (γ := Submodule R M) (maxGenEigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) x
k : ℕ
hk :
  Eq (α := M)
    ((HSub.hSub (α := End R M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d) : M →ₗ[R] M)
              (HSMul.hSMul (β := End R M) μ 1) ^
            k :
          (a : M) → M)
        x :
      M)
    (0 : M)
⊢ Membership.mem (γ := Submodule R M) (eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) x
have hk₁ : ∀ (j : n),
  Eq.{u_1 + 1} (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (0 : R) ∨ d j = μ ∧ k ≠ 0
Tactic: replace hk (j : n) : b.repr x j = 0 ∨ d j = μ ∧ k ≠ 0 := by
    have aux : (diagonal d).toLin b b - μ • 1 = (diagonal (d - μ • 1)).toLin b b := by
      rw [Pi.sub_def, ← diagonal_sub]; simp [one_eq_id]
    rw [aux, ← toLin_pow, diagonal_pow, toLin_apply_eq_zero_iff] at hk
    simpa [mulVec_eq_sum, diagonal_apply, sub_eq_zero] using hk j
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Matrix (goal)
Goal:
R : Type u_1
n : Type u_2
M : Type u_3
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
d : n → R
μ : R
b : Basis n R M
inst_5 : IsDomain R
x : M
hx :
  Membership.mem (γ := Submodule R M) (maxGenEigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) x
k : ℕ
hk :
  ∀ (j : n),
    Eq.{u_1 + 1} (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (0 : R) ∨ d j = μ ∧ k ≠ 0
j : n
⊢ HSMul.hSMul (β := M) (HMul.hMul (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (d j))
      ((b : (a : n) → M) j : M) =
    μ •
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R)
        ((b : (a : n) → M) j : M)
have inl : ∀ (hj : Eq.{u_1 + 1} (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (0 : R)),
  HSMul.hSMul (β := M) (HMul.hMul (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (d j))
      ((b : (a : n) → M) j : M) =
    μ •
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R)
        ((b : (a : n) → M) j : M)
Tactic: rcases hk j with hj | hj
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Matrix (goal)
Goal:
R : Type u_1
n : Type u_2
M : Type u_3
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
d : n → R
μ : R
b : Basis n R M
inst_5 : IsDomain R
x : M
hx :
  Membership.mem (γ := Submodule R M) (maxGenEigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) x
k : ℕ
hk :
  ∀ (j : n),
    Eq.{u_1 + 1} (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (0 : R) ∨ d j = μ ∧ k ≠ 0
j : n
inl :
  ∀ (hj : Eq.{u_1 + 1} (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (0 : R)),
    HSMul.hSMul (β := M) (HMul.hMul (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (d j))
        ((b : (a : n) → M) j : M) =
      μ •
        HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R)
          ((b : (a : n) → M) j : M)
⊢ HSMul.hSMul (β := M) (HMul.hMul (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (d j))
      ((b : (a : n) → M) j : M) =
    μ •
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R)
        ((b : (a : n) → M) j : M)
have inr : ∀ (hj : d j = μ ∧ k ≠ 0),
  HSMul.hSMul (β := M) (HMul.hMul (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (d j))
      ((b : (a : n) → M) j : M) =
    μ •
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R)
        ((b : (a : n) → M) j : M)
Tactic: rcases hk j with hj | hj
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Matrix (goal)
Goal:
R : Type u_1
n : Type u_2
M : Type u_3
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
d : n → R
μ : R
b : Basis n R M
inst_5 : IsDomain R
x : M
hx :
  Membership.mem (γ := Submodule R M) (maxGenEigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) x
k : ℕ
hk :
  ∀ (j : n),
    Eq.{u_1 + 1} (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (0 : R) ∨ d j = μ ∧ k ≠ 0
j : n
hj : d j = μ ∧ k ≠ 0
⊢ HSMul.hSMul (β := M) (HMul.hMul (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (d j))
      ((b : (a : n) → M) j : M) =
    μ •
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R)
        ((b : (a : n) → M) j : M)
have inr : HSMul.hSMul (β := M) (HMul.hMul (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (d j))
    ((b : (a : n) → M) j : M) =
  d j •
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R)
      ((b : (a : n) → M) j : M)
Tactic: rw [← hj.1, mul_comm, mul_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Matrix (goal)
Goal:
R : Type u_1
n : Type u_2
M : Type u_3
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
d : n → R
μ : R
b : Basis n R M
inst_5 : IsDomain R
x : M
hx :
  Membership.mem (γ := Submodule R M) (maxGenEigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) x
k : ℕ
hk :
  ∀ (j : n),
    Eq.{u_1 + 1} (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (0 : R) ∨ d j = μ ∧ k ≠ 0
j : n
hj : d j = μ ∧ k ≠ 0
inr :
  HSMul.hSMul (β := M) (HMul.hMul (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (d j))
      ((b : (a : n) → M) j : M) =
    d j •
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R)
        ((b : (a : n) → M) j : M)
⊢ HSMul.hSMul (β := M) (HMul.hMul (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (d j))
      ((b : (a : n) → M) j : M) =
    μ •
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R)
        ((b : (a : n) → M) j : M)
have inr₁ : HSMul.hSMul (β := M) (HMul.hMul (β := R) (d j) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R))
    ((b : (a : n) → M) j : M) =
  d j •
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R)
      ((b : (a : n) → M) j : M)
Tactic: rw [← hj.1, mul_comm, mul_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Matrix (goal)
Goal:
R : Type u_1
n : Type u_2
M : Type u_3
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
d : n → R
μ : R
b : Basis n R M
inst_5 : IsDomain R
x : M
hx :
  Membership.mem (γ := Submodule R M) (maxGenEigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) x
k : ℕ
hk :
  ∀ (j : n),
    Eq.{u_1 + 1} (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (0 : R) ∨ d j = μ ∧ k ≠ 0
j : n
hj : d j = μ ∧ k ≠ 0
inr :
  HSMul.hSMul (β := M) (HMul.hMul (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (d j))
      ((b : (a : n) → M) j : M) =
    d j •
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R)
        ((b : (a : n) → M) j : M)
inr₁ :
  HSMul.hSMul (β := M) (HMul.hMul (β := R) (d j) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R))
      ((b : (a : n) → M) j : M) =
    d j •
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R)
        ((b : (a : n) → M) j : M)
⊢ HSMul.hSMul (β := M) (HMul.hMul (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (d j))
      ((b : (a : n) → M) j : M) =
    μ •
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R)
        ((b : (a : n) → M) j : M)
have inr₂ : d j •
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R)
      ((b : (a : n) → M) j : M) =
  d j •
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R)
      ((b : (a : n) → M) j : M)
Tactic: rw [← hj.1, mul_comm, mul_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Matrix (hypothesis)
Goal:
R : Type u_1
n : Type u_2
M : Type u_3
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
d : n → R
μ : R
b : Basis n R M
inst_5 : IsDomain R
x : M
hx :
  Membership.mem (γ := Submodule R M) (maxGenEigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) x
k : ℕ
hk :
  ∀ (j : n),
    Eq.{u_1 + 1} (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (0 : R) ∨ d j = μ ∧ k ≠ 0
⊢ Membership.mem (γ := Submodule R M) (eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) x
have aux : ∀ (j : n),
  HSMul.hSMul (β := M) (HMul.hMul (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (d j))
      ((b : (a : n) → M) j : M) =
    μ •
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R)
        ((b : (a : n) → M) j : M)
Tactic: have aux (j : n) : (b.repr x j * d j) • b j = μ • (b.repr x j • b j) := by
    rcases hk j with hj | hj
    · simp [hj]
    · rw [← hj.1, mul_comm, mul_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Matrix (goal)
Goal:
R : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Field R
d : n → R
⊢ spectrum R (diagonal d) = Set.range d
have h : ∀ (μ : R), μ ∈ spectrum R (diagonal d) ↔ μ ∈ Set.range d
Tactic: ext μ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Matrix (goal)
Goal:
R : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Field R
d : n → R
μ : R
⊢ μ ∈ spectrum R (diagonal d) ↔ μ ∈ Set.range d
have h : HasEigenvalue (M := n → R) ((toLinAlgEquiv (Pi.basisFun R n) : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (diagonal d))
    μ ↔
  μ ∈ Set.range d
Tactic: rw [← AlgEquiv.spectrum_eq (toLinAlgEquiv <| Pi.basisFun R n), ← hasEigenvalue_iff_mem_spectrum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Minpoly (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
x : M
p : R[X]
h : f.HasEigenvector μ x
⊢ (((aeval f : (a : R[X]) → End R M) p : End R M) : (a : M) → M) x = eval μ p • x
have refine_1 : ∀ (a : R),
  (((aeval f : (a : R[X]) → End R M) ((C : (a : R) → R[X]) a) : End R M) : (a : M) → M) x =
    eval μ ((C : (a : R) → R[X]) a) • x
Tactic: refine p.induction_on ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Minpoly (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
x : M
p : R[X]
h : f.HasEigenvector μ x
refine_1 :
  ∀ (a : R),
    (((aeval f : (a : R[X]) → End R M) ((C : (a : R) → R[X]) a) : End R M) : (a : M) → M) x =
      eval μ ((C : (a : R) → R[X]) a) • x
⊢ (((aeval f : (a : R[X]) → End R M) p : End R M) : (a : M) → M) x = eval μ p • x
have refine_2 : ∀ (p q : R[X]),
  (((aeval f : (a : R[X]) → End R M) p : End R M) : (a : M) → M) x = eval μ p • x →
    (((aeval f : (a : R[X]) → End R M) q : End R M) : (a : M) → M) x = eval μ q • x →
      (((aeval f : (a : R[X]) → End R M) (p + q) : End R M) : (a : M) → M) x = eval μ (p + q) • x
Tactic: refine p.induction_on ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Minpoly (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
x : M
p : R[X]
h : f.HasEigenvector μ x
refine_1 :
  ∀ (a : R),
    (((aeval f : (a : R[X]) → End R M) ((C : (a : R) → R[X]) a) : End R M) : (a : M) → M) x =
      eval μ ((C : (a : R) → R[X]) a) • x
refine_2 :
  ∀ (p q : R[X]),
    (((aeval f : (a : R[X]) → End R M) p : End R M) : (a : M) → M) x = eval μ p • x →
      (((aeval f : (a : R[X]) → End R M) q : End R M) : (a : M) → M) x = eval μ q • x →
        (((aeval f : (a : R[X]) → End R M) (p + q) : End R M) : (a : M) → M) x = eval μ (p + q) • x
⊢ (((aeval f : (a : R[X]) → End R M) p : End R M) : (a : M) → M) x = eval μ p • x
have refine_3 : ∀ (n : ℕ) (a : R),
  (((aeval f : (a : R[X]) → End R M)
              (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) :
            End R M) :
          (a : M) → M)
        x =
      eval μ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) • x →
    (((aeval f : (a : R[X]) → End R M)
              (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) :
            End R M) :
          (a : M) → M)
        x =
      eval μ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) • x
Tactic: refine p.induction_on ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Minpoly (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
x : M
p : R[X]
h : f.HasEigenvector μ x
n : ℕ
a : R
hna :
  (((aeval f : (a : R[X]) → End R M)
            (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) :
          End R M) :
        (a : M) → M)
      x =
    eval μ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) • x
⊢ (((aeval f : (a : R[X]) → End R M)
            (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) :
          End R M) :
        (a : M) → M)
      x =
    eval μ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) • x
have refine_3 : (((aeval f : (a : R[X]) → End R M) X : End R M) : (a : M) → M)
    (eval μ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) • x) =
  eval μ (X * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) • x
Tactic: rw [mul_comm, pow_succ', mul_assoc, map_mul, Module.End.mul_apply, mul_comm, hna]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Minpoly (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
x : M
p : R[X]
hx : (f : (a : M) → M) x = μ • x
⊢ (((aeval f : (a : R[X]) → End R M) p : End R M) : (a : M) → M) x = eval μ p • x
have inl : ∀ (hx : (f : (a : M) → M) 0 = HSMul.hSMul (β := M) μ 0),
  (((aeval f : (a : R[X]) → End R M) p : End R M) : (a : M) → M) 0 = HSMul.hSMul (β := M) (eval μ p) 0
Tactic: rcases eq_or_ne x 0 with rfl | hne
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Minpoly (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
x : M
p : R[X]
hx : (f : (a : M) → M) x = μ • x
inl :
  ∀ (hx : (f : (a : M) → M) 0 = HSMul.hSMul (β := M) μ 0),
    (((aeval f : (a : R[X]) → End R M) p : End R M) : (a : M) → M) 0 = HSMul.hSMul (β := M) (eval μ p) 0
⊢ (((aeval f : (a : R[X]) → End R M) p : End R M) : (a : M) → M) x = eval μ p • x
have inr : ∀ (hne : x ≠ 0), (((aeval f : (a : R[X]) → End R M) p : End R M) : (a : M) → M) x = eval μ p • x
Tactic: rcases eq_or_ne x 0 with rfl | hne
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Minpoly (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
f : End R M
μ : R
h : f.HasEigenvalue μ
⊢ IsRoot (minpoly R f) μ
have rcases : ∀ (w : M) (H : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) 1 : Submodule R M) w)
  (ne0 : w ≠ 0), IsRoot (minpoly R f) μ
Tactic: rcases (Submodule.ne_bot_iff _).1 h with ⟨w, ⟨H, ne0⟩⟩