awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (hypothesis)
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
φ : End K M
this :
  [¬φ.HasEigenvalue 0, ¬IsRoot (minpoly K φ) 0, Ne (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K),
      Ne.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K), ¬⊥ < ker φ,
      ∀ (m : M) (_ : m ≠ 0), Ne (α := M) ((φ : (a : M) → M) m : M) (0 : M)].TFAE
⊢ [¬φ.HasEigenvalue 0, ¬IsRoot (minpoly K φ) 0, Ne (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K),
      Ne.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K), ker φ = ⊥,
      ∀ (m : M), Eq (α := M) ((φ : (a : M) → M) m : M) (0 : M) → m = 0].TFAE
have aux₁ : ∀ (m : M), m ≠ 0 → Ne (α := M) ((φ : (a : M) → M) m : M) (0 : M) ↔ Eq (α := M) ((φ : (a : M) → M) m : M) (0 : M) → m = 0
Tactic: have aux₁ : ∀ m, (m ≠ 0 → φ m ≠ 0) ↔ (φ m = 0 → m = 0) := by intro m; apply not_imp_not
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
φ : End K M
this :
  [¬φ.HasEigenvalue 0, ¬IsRoot (minpoly K φ) 0, Ne (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K),
      Ne.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K), ¬⊥ < ker φ,
      ∀ (m : M) (_ : m ≠ 0), Ne (α := M) ((φ : (a : M) → M) m : M) (0 : M)].TFAE
aux₁ :
  ∀ (m : M),
    m ≠ 0 → Ne (α := M) ((φ : (a : M) → M) m : M) (0 : M) ↔ Eq (α := M) ((φ : (a : M) → M) m : M) (0 : M) → m = 0
⊢ ker φ = ⊥ ↔ ¬⊥ < ker φ
have rw : ker φ = ⊥ ↔ ¬ker φ ≠ ⊥
Tactic: rw [bot_lt_iff_ne_bot, not_not]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
φ : End K M
this :
  [¬φ.HasEigenvalue 0, ¬IsRoot (minpoly K φ) 0, Ne (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K),
      Ne.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K), ¬⊥ < ker φ,
      ∀ (m : M) (_ : m ≠ 0), Ne (α := M) ((φ : (a : M) → M) m : M) (0 : M)].TFAE
aux₁ :
  ∀ (m : M),
    m ≠ 0 → Ne (α := M) ((φ : (a : M) → M) m : M) (0 : M) ↔ Eq (α := M) ((φ : (a : M) → M) m : M) (0 : M) → m = 0
rw : ker φ = ⊥ ↔ ¬ker φ ≠ ⊥
⊢ ker φ = ⊥ ↔ ¬⊥ < ker φ
have rw₁ : ker φ = ⊥ ↔ ker φ = ⊥
Tactic: rw [bot_lt_iff_ne_bot, not_not]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (hypothesis)
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
φ : End K M
this :
  [¬φ.HasEigenvalue 0, ¬IsRoot (minpoly K φ) 0, Ne (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K),
      Ne.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K), ¬⊥ < ker φ,
      ∀ (m : M) (_ : m ≠ 0), Ne (α := M) ((φ : (a : M) → M) m : M) (0 : M)].TFAE
aux₁ :
  ∀ (m : M),
    m ≠ 0 → Ne (α := M) ((φ : (a : M) → M) m : M) (0 : M) ↔ Eq (α := M) ((φ : (a : M) → M) m : M) (0 : M) → m = 0
⊢ [¬φ.HasEigenvalue 0, ¬IsRoot (minpoly K φ) 0, Ne (α := K) ((constantCoeff : (a : K[X]) → K) (charpoly φ) : K) (0 : K),
      Ne.{u_2 + 1} (α := K) ((LinearMap.det : (a : M →ₗ[K] M) → K) φ : K) (0 : K), ker φ = ⊥,
      ∀ (m : M), Eq (α := M) ((φ : (a : M) → M) m : M) (0 : M) → m = 0].TFAE
have aux₂ : ker φ = ⊥ ↔ ¬⊥ < ker φ
Tactic: have aux₂ : ker φ = ⊥ ↔ ¬ ⊥ < ker φ := by rw [bot_lt_iff_ne_bot, not_not]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (hypothesis)
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
⊢ finrank.{u_2, u_3} K ↥V = (charpoly φ).natTrailingDegree
have hV : V = ⨆ (n : ℕ), ker (φ ^ n)
Tactic: have hV : V = ⨆ (n : ℕ), ker (φ ^ n) := by
    simp [V, ← Module.End.iSup_genEigenspace_eq, Module.End.genEigenspace_nat]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ (n : ℕ), ker (φ ^ n)
W : Submodule K M := ⨅ (n : ℕ), range (φ ^ n)
⊢ IsCompl V W
have rw : IsCompl (⨆ (n : ℕ), ker (φ ^ n)) W
Tactic: rw [hV]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (hypothesis)
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ (n : ℕ), ker (φ ^ n)
W : Submodule K M := ⨅ (n : ℕ), range (φ ^ n)
⊢ finrank.{u_2, u_3} K ↥V = (charpoly φ).natTrailingDegree
have hVW : IsCompl V W
Tactic: have hVW : IsCompl V W := by
    rw [hV]
    exact LinearMap.isCompl_iSup_ker_pow_iInf_range_pow φ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ (n : ℕ), ker (φ ^ n)
W : Submodule K M := ⨅ (n : ℕ), range (φ ^ n)
hVW : IsCompl V W
⊢ ∀ x ∈ V, Membership.mem (α := M) V ((φ : (a : M) → M) x : M)
have simp : ∀ (x : M) (x_1 : ℕ) (h : Eq (α := M) ((φ ^ x_1 : (a : M) → M) x : M) (0 : M)),
  ∃ (k : ℕ), Eq (α := M) ((φ ^ k : (a : M) → M) ((φ : (a : M) → M) x : M) : M) (0 : M)
Tactic: simp only [V, Module.End.mem_maxGenEigenspace, zero_smul, sub_zero,
      forall_exists_index]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ (n : ℕ), ker (φ ^ n)
W : Submodule K M := ⨅ (n : ℕ), range (φ ^ n)
hVW : IsCompl V W
x : M
n : ℕ
hx : Eq (α := M) ((φ ^ n : (a : M) → M) x : M) (0 : M)
⊢ ∃ (k : ℕ), Eq (α := M) ((φ ^ k : (a : M) → M) ((φ : (a : M) → M) x : M) : M) (0 : M)
have h : Eq (α := M) ((φ ^ n : (a : M) → M) ((φ : (a : M) → M) x : M) : M) (0 : M)
Tactic: use n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ (n : ℕ), ker (φ ^ n)
W : Submodule K M := ⨅ (n : ℕ), range (φ ^ n)
hVW : IsCompl V W
x : M
n : ℕ
hx : Eq (α := M) ((φ ^ n : (a : M) → M) x : M) (0 : M)
⊢ Eq (α := M) ((φ ^ n : (a : M) → M) ((φ : (a : M) → M) x : M) : M) (0 : M)
have h : Eq (α := M) ((φ ^ n * φ : (a : M) → M) x : M) (0 : M)
Tactic: rw [← Module.End.mul_apply, ← pow_succ, pow_succ', Module.End.mul_apply, hx, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ (n : ℕ), ker (φ ^ n)
W : Submodule K M := ⨅ (n : ℕ), range (φ ^ n)
hVW : IsCompl V W
x : M
n : ℕ
hx : Eq (α := M) ((φ ^ n : (a : M) → M) x : M) (0 : M)
h : Eq (α := M) ((φ ^ n * φ : (a : M) → M) x : M) (0 : M)
⊢ Eq (α := M) ((φ ^ n : (a : M) → M) ((φ : (a : M) → M) x : M) : M) (0 : M)
have h₁ : Eq (α := M) ((φ ^ (n + 1) : (a : M) → M) x : M) (0 : M)
Tactic: rw [← Module.End.mul_apply, ← pow_succ, pow_succ', Module.End.mul_apply, hx, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ (n : ℕ), ker (φ ^ n)
W : Submodule K M := ⨅ (n : ℕ), range (φ ^ n)
hVW : IsCompl V W
x : M
n : ℕ
hx : Eq (α := M) ((φ ^ n : (a : M) → M) x : M) (0 : M)
h : Eq (α := M) ((φ ^ n * φ : (a : M) → M) x : M) (0 : M)
h₁ : Eq (α := M) ((φ ^ (n + 1) : (a : M) → M) x : M) (0 : M)
⊢ Eq (α := M) ((φ ^ n : (a : M) → M) ((φ : (a : M) → M) x : M) : M) (0 : M)
have h₂ : Eq (α := M) ((φ * φ ^ n : (a : M) → M) x : M) (0 : M)
Tactic: rw [← Module.End.mul_apply, ← pow_succ, pow_succ', Module.End.mul_apply, hx, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ (n : ℕ), ker (φ ^ n)
W : Submodule K M := ⨅ (n : ℕ), range (φ ^ n)
hVW : IsCompl V W
x : M
n : ℕ
hx : Eq (α := M) ((φ ^ n : (a : M) → M) x : M) (0 : M)
h : Eq (α := M) ((φ ^ n * φ : (a : M) → M) x : M) (0 : M)
h₁ : Eq (α := M) ((φ ^ (n + 1) : (a : M) → M) x : M) (0 : M)
h₂ : Eq (α := M) ((φ * φ ^ n : (a : M) → M) x : M) (0 : M)
⊢ Eq (α := M) ((φ ^ n : (a : M) → M) ((φ : (a : M) → M) x : M) : M) (0 : M)
have h₃ : Eq (α := M) ((φ : (a : M) → M) ((φ ^ n : (a : M) → M) x : M) : M) (0 : M)
Tactic: rw [← Module.End.mul_apply, ← pow_succ, pow_succ', Module.End.mul_apply, hx, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ (n : ℕ), ker (φ ^ n)
W : Submodule K M := ⨅ (n : ℕ), range (φ ^ n)
hVW : IsCompl V W
x : M
n : ℕ
hx : Eq (α := M) ((φ ^ n : (a : M) → M) x : M) (0 : M)
h : Eq (α := M) ((φ ^ n * φ : (a : M) → M) x : M) (0 : M)
h₁ : Eq (α := M) ((φ ^ (n + 1) : (a : M) → M) x : M) (0 : M)
h₂ : Eq (α := M) ((φ * φ ^ n : (a : M) → M) x : M) (0 : M)
h₃ : Eq (α := M) ((φ : (a : M) → M) ((φ ^ n : (a : M) → M) x : M) : M) (0 : M)
⊢ Eq (α := M) ((φ ^ n : (a : M) → M) ((φ : (a : M) → M) x : M) : M) (0 : M)
have h₄ : Eq (α := M) ((φ : (a : M) → M) 0 : M) (0 : M)
Tactic: rw [← Module.End.mul_apply, ← pow_succ, pow_succ', Module.End.mul_apply, hx, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ (n : ℕ), ker (φ ^ n)
W : Submodule K M := ⨅ (n : ℕ), range (φ ^ n)
hVW : IsCompl V W
x : M
n : ℕ
hx : Eq (α := M) ((φ ^ n : (a : M) → M) x : M) (0 : M)
h : Eq (α := M) ((φ ^ n * φ : (a : M) → M) x : M) (0 : M)
h₁ : Eq (α := M) ((φ ^ (n + 1) : (a : M) → M) x : M) (0 : M)
h₂ : Eq (α := M) ((φ * φ ^ n : (a : M) → M) x : M) (0 : M)
h₃ : Eq (α := M) ((φ : (a : M) → M) ((φ ^ n : (a : M) → M) x : M) : M) (0 : M)
h₄ : Eq (α := M) ((φ : (a : M) → M) 0 : M) (0 : M)
⊢ Eq (α := M) ((φ ^ n : (a : M) → M) ((φ : (a : M) → M) x : M) : M) (0 : M)
have h₅ : Eq.{u_3 + 1} (α := M) 0 0
Tactic: rw [← Module.End.mul_apply, ← pow_succ, pow_succ', Module.End.mul_apply, hx, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (hypothesis)
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ (n : ℕ), ker (φ ^ n)
W : Submodule K M := ⨅ (n : ℕ), range (φ ^ n)
hVW : IsCompl V W
⊢ finrank.{u_2, u_3} K ↥V = (charpoly φ).natTrailingDegree
have hφV : ∀ x ∈ V, Membership.mem (α := M) V ((φ : (a : M) → M) x : M)
Tactic: have hφV : ∀ x ∈ V, φ x ∈ V := by
    simp only [V, Module.End.mem_maxGenEigenspace, zero_smul, sub_zero,
      forall_exists_index]
    intro x n hx
    use n
    rw [← Module.End.mul_apply, ← pow_succ, pow_succ', Module.End.mul_apply, hx, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ (n : ℕ), ker (φ ^ n)
W : Submodule K M := ⨅ (n : ℕ), range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, Membership.mem (α := M) V ((φ : (a : M) → M) x : M)
⊢ ∀ x ∈ W, Membership.mem (α := M) W ((φ : (a : M) → M) x : M)
have simp : ∀ (x : M),
  (∀ (i : ℕ), ∃ (y : M), (φ ^ i : (a : M) → M) y = x) →
    ∀ (i : ℕ), ∃ (y : M), Eq (α := M) ((φ ^ i : (a : M) → M) y : M) ((φ : (a : M) → M) x : M)
Tactic: simp only [W, Submodule.mem_iInf, mem_range]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ (n : ℕ), ker (φ ^ n)
W : Submodule K M := ⨅ (n : ℕ), range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, Membership.mem (α := M) V ((φ : (a : M) → M) x : M)
x : M
H : ∀ (i : ℕ), ∃ (y : M), (φ ^ i : (a : M) → M) y = x
n : ℕ
⊢ ∃ (y : M), Eq (α := M) ((φ ^ n : (a : M) → M) y : M) ((φ : (a : M) → M) x : M)
have obtain : ∀ (y : M) (H : ∀ (i : ℕ), ∃ (y_1 : M), Eq (α := M) ((φ ^ i : (a : M) → M) y_1 : M) ((φ ^ n : (a : M) → M) y : M)),
  ∃ (y_1 : M), Eq (α := M) ((φ ^ n : (a : M) → M) y_1 : M) ((φ : (a : M) → M) ((φ ^ n : (a : M) → M) y : M) : M)
Tactic: obtain ⟨y, rfl⟩ := H n
Cleared hypotheses: x, H
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ (n : ℕ), ker (φ ^ n)
W : Submodule K M := ⨅ (n : ℕ), range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, Membership.mem (α := M) V ((φ : (a : M) → M) x : M)
n : ℕ
y : M
H : ∀ (i : ℕ), ∃ (y_1 : M), Eq (α := M) ((φ ^ i : (a : M) → M) y_1 : M) ((φ ^ n : (a : M) → M) y : M)
⊢ ∃ (y_1 : M), Eq (α := M) ((φ ^ n : (a : M) → M) y_1 : M) ((φ : (a : M) → M) ((φ ^ n : (a : M) → M) y : M) : M)
have h : Eq (α := M) ((φ ^ n : (a : M) → M) ((φ : (a : M) → M) y : M) : M) ((φ : (a : M) → M) ((φ ^ n : (a : M) → M) y : M) : M)
Tactic: use φ y
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ (n : ℕ), ker (φ ^ n)
W : Submodule K M := ⨅ (n : ℕ), range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, Membership.mem (α := M) V ((φ : (a : M) → M) x : M)
n : ℕ
y : M
H : ∀ (i : ℕ), ∃ (y_1 : M), Eq (α := M) ((φ ^ i : (a : M) → M) y_1 : M) ((φ ^ n : (a : M) → M) y : M)
⊢ Eq (α := M) ((φ ^ n : (a : M) → M) ((φ : (a : M) → M) y : M) : M)
    ((φ : (a : M) → M) ((φ ^ n : (a : M) → M) y : M) : M)
have h : Eq (α := M) ((φ ^ n * φ : (a : M) → M) y : M) ((φ : (a : M) → M) ((φ ^ n : (a : M) → M) y : M) : M)
Tactic: rw [← Module.End.mul_apply, ← pow_succ, pow_succ', Module.End.mul_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ (n : ℕ), ker (φ ^ n)
W : Submodule K M := ⨅ (n : ℕ), range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, Membership.mem (α := M) V ((φ : (a : M) → M) x : M)
n : ℕ
y : M
H : ∀ (i : ℕ), ∃ (y_1 : M), Eq (α := M) ((φ ^ i : (a : M) → M) y_1 : M) ((φ ^ n : (a : M) → M) y : M)
h : Eq (α := M) ((φ ^ n * φ : (a : M) → M) y : M) ((φ : (a : M) → M) ((φ ^ n : (a : M) → M) y : M) : M)
⊢ Eq (α := M) ((φ ^ n : (a : M) → M) ((φ : (a : M) → M) y : M) : M)
    ((φ : (a : M) → M) ((φ ^ n : (a : M) → M) y : M) : M)
have h₁ : Eq (α := M) ((φ ^ (n + 1) : (a : M) → M) y : M) ((φ : (a : M) → M) ((φ ^ n : (a : M) → M) y : M) : M)
Tactic: rw [← Module.End.mul_apply, ← pow_succ, pow_succ', Module.End.mul_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ (n : ℕ), ker (φ ^ n)
W : Submodule K M := ⨅ (n : ℕ), range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, Membership.mem (α := M) V ((φ : (a : M) → M) x : M)
n : ℕ
y : M
H : ∀ (i : ℕ), ∃ (y_1 : M), Eq (α := M) ((φ ^ i : (a : M) → M) y_1 : M) ((φ ^ n : (a : M) → M) y : M)
h : Eq (α := M) ((φ ^ n * φ : (a : M) → M) y : M) ((φ : (a : M) → M) ((φ ^ n : (a : M) → M) y : M) : M)
h₁ : Eq (α := M) ((φ ^ (n + 1) : (a : M) → M) y : M) ((φ : (a : M) → M) ((φ ^ n : (a : M) → M) y : M) : M)
⊢ Eq (α := M) ((φ ^ n : (a : M) → M) ((φ : (a : M) → M) y : M) : M)
    ((φ : (a : M) → M) ((φ ^ n : (a : M) → M) y : M) : M)
have h₂ : Eq (α := M) ((φ * φ ^ n : (a : M) → M) y : M) ((φ : (a : M) → M) ((φ ^ n : (a : M) → M) y : M) : M)
Tactic: rw [← Module.End.mul_apply, ← pow_succ, pow_succ', Module.End.mul_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ (n : ℕ), ker (φ ^ n)
W : Submodule K M := ⨅ (n : ℕ), range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, Membership.mem (α := M) V ((φ : (a : M) → M) x : M)
n : ℕ
y : M
H : ∀ (i : ℕ), ∃ (y_1 : M), Eq (α := M) ((φ ^ i : (a : M) → M) y_1 : M) ((φ ^ n : (a : M) → M) y : M)
h : Eq (α := M) ((φ ^ n * φ : (a : M) → M) y : M) ((φ : (a : M) → M) ((φ ^ n : (a : M) → M) y : M) : M)
h₁ : Eq (α := M) ((φ ^ (n + 1) : (a : M) → M) y : M) ((φ : (a : M) → M) ((φ ^ n : (a : M) → M) y : M) : M)
h₂ : Eq (α := M) ((φ * φ ^ n : (a : M) → M) y : M) ((φ : (a : M) → M) ((φ ^ n : (a : M) → M) y : M) : M)
⊢ Eq (α := M) ((φ ^ n : (a : M) → M) ((φ : (a : M) → M) y : M) : M)
    ((φ : (a : M) → M) ((φ ^ n : (a : M) → M) y : M) : M)
have h₃ : Eq (α := M) ((φ : (a : M) → M) ((φ ^ n : (a : M) → M) y : M) : M) ((φ : (a : M) → M) ((φ ^ n : (a : M) → M) y : M) : M)
Tactic: rw [← Module.End.mul_apply, ← pow_succ, pow_succ', Module.End.mul_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (hypothesis)
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ (n : ℕ), ker (φ ^ n)
W : Submodule K M := ⨅ (n : ℕ), range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, Membership.mem (α := M) V ((φ : (a : M) → M) x : M)
⊢ finrank.{u_2, u_3} K ↥V = (charpoly φ).natTrailingDegree
have hφW : ∀ x ∈ W, Membership.mem (α := M) W ((φ : (a : M) → M) x : M)
Tactic: have hφW : ∀ x ∈ W, φ x ∈ W := by
    simp only [W, Submodule.mem_iInf, mem_range]
    intro x H n
    obtain ⟨y, rfl⟩ := H n
    use φ y
    rw [← Module.End.mul_apply, ← pow_succ, pow_succ', Module.End.mul_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ (n : ℕ), ker (φ ^ n)
W : Submodule K M := ⨅ (n : ℕ), range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, Membership.mem (α := M) V ((φ : (a : M) → M) x : M)
hφW : ∀ x ∈ W, Membership.mem (α := M) W ((φ : (a : M) → M) x : M)
F : ↥V →ₗ[K] ↥V := restrict φ hφV
G : ↥W →ₗ[K] ↥W := restrict φ hφW
ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G
e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW
bV : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
⊢ ψ =
    ((LinearEquiv.conj.{u_2, u_2, u_3, u_3} (R₁' := K) (R₂' := K) (M₁' := M) (M₂' := ↥V × ↥W) (σ₁'₂' := RingHom.id K)
            (σ₂'₁' := RingHom.id K) e.symm :
          End K M ≃ₗ[K] End K (↥V × ↥W)) :
        (a : End K M) → End K (↥V × ↥W))
      φ
have apply : ∀ (i : ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W),
  Eq (α := ↥V × ↥W)
    ((ψ : (a : ↥V × ↥W) → ↥V × ↥W) ((b : (a : ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) → ↥V × ↥W) i : ↥V × ↥W) :
      ↥V × ↥W)
    (((((LinearEquiv.conj.{u_2, u_2, u_3, u_3} (R₁' := K) (R₂' := K) (M₁' := M) (M₂' := ↥V × ↥W) (σ₁'₂' := RingHom.id K)
                    (σ₂'₁' := RingHom.id K) e.symm :
                  End K M ≃ₗ[K] End K (↥V × ↥W)) :
                (a : End K M) → End K (↥V × ↥W))
              φ :
            End K (↥V × ↥W)) :
          (a : ↥V × ↥W) → ↥V × ↥W)
        ((b : (a : ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) → ↥V × ↥W) i : ↥V × ↥W) :
      ↥V × ↥W)
Tactic: apply b.ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (hypothesis)
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ (n : ℕ), ker (φ ^ n)
W : Submodule K M := ⨅ (n : ℕ), range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, Membership.mem (α := M) V ((φ : (a : M) → M) x : M)
hφW : ∀ x ∈ W, Membership.mem (α := M) W ((φ : (a : M) → M) x : M)
F : ↥V →ₗ[K] ↥V := restrict φ hφV
G : ↥W →ₗ[K] ↥W := restrict φ hφW
ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G
e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW
bV : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
⊢ finrank.{u_2, u_3} K ↥V = (charpoly φ).natTrailingDegree
have hψ : ψ =
  ((LinearEquiv.conj.{u_2, u_2, u_3, u_3} (R₁' := K) (R₂' := K) (M₁' := M) (M₂' := ↥V × ↥W) (σ₁'₂' := RingHom.id K)
          (σ₂'₁' := RingHom.id K) e.symm :
        End K M ≃ₗ[K] End K (↥V × ↥W)) :
      (a : End K M) → End K (↥V × ↥W))
    φ
Tactic: have hψ : ψ = e.symm.conj φ := by
    apply b.ext
    simp only [Basis.prod_apply, coe_inl, coe_inr, prodMap_apply, LinearEquiv.conj_apply,
      LinearEquiv.symm_symm, Submodule.coe_prodEquivOfIsCompl, coe_comp, LinearEquiv.coe_coe,
      Function.comp_apply, coprod_apply, Submodule.coe_subtype, map_add, Sum.forall, Sum.elim_inl,
      map_zero, ZeroMemClass.coe_zero, add_zero, LinearEquiv.eq_symm_apply, and_self,
      Submodule.coe_prodEquivOfIsCompl', coe_restrict_apply, implies_true, Sum.elim_inr, zero_add,
      e, V, W, ψ, F, G, b]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ (n : ℕ), ker (φ ^ n)
W : Submodule K M := ⨅ (n : ℕ), range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, Membership.mem (α := M) V ((φ : (a : M) → M) x : M)
hφW : ∀ x ∈ W, Membership.mem (α := M) W ((φ : (a : M) → M) x : M)
F : ↥V →ₗ[K] ↥V := restrict φ hφV
G : ↥W →ₗ[K] ↥W := restrict φ hφW
ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G
e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW
bV : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ :
  ψ =
    ((LinearEquiv.conj.{u_2, u_2, u_3, u_3} (R₁' := K) (R₂' := K) (M₁' := M) (M₂' := ↥V × ↥W) (σ₁'₂' := RingHom.id K)
            (σ₂'₁' := RingHom.id K) e.symm :
          End K M ≃ₗ[K] End K (↥V × ↥W)) :
        (a : End K M) → End K (↥V × ↥W))
      φ
⊢ finrank.{u_2, u_3} K ↥V = (charpoly φ).natTrailingDegree
have rw : finrank.{u_2, u_3} K ↥V = F.charpoly.natTrailingDegree + G.charpoly.natTrailingDegree
Tactic: rw [← e.symm.charpoly_conj φ, ← hψ, charpoly_prodMap,
    natTrailingDegree_mul (charpoly_monic _).ne_zero (charpoly_monic _).ne_zero]