awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
      φ
hG : G.charpoly.natTrailingDegree = 0
x : M
n : ℕ
hx : Eq (α := M) ((φ ^ n : (a : M) → M) x : M) (0 : M)
⊢ Eq (α := ↥(φ.maxGenEigenspace 0))
    ((restrict φ hφV ^ n : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
        (Subtype.mk (p := fun (a : M) ↦ a ∈ φ.maxGenEigenspace 0) x ⋯) :
      ↥(φ.maxGenEigenspace 0))
    (0 : ↥V)
have h : Eq.{u_3 + 1} (α := M)
  (↑((restrict φ hφV ^ n : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
        (Subtype.mk (p := fun (a : M) ↦ a ∈ φ.maxGenEigenspace 0) x sorry)) :
    M)
  (↑0 : M)
Tactic: apply Subtype.ext
-- 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))
      φ
hG : G.charpoly.natTrailingDegree = 0
x : M
n : ℕ
hx : Eq (α := M) ((φ ^ n : (a : M) → M) x : M) (0 : M)
⊢ Eq.{u_3 + 1} (α := M)
    (↑((restrict φ hφV ^ n : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
          (Subtype.mk (p := fun (a : M) ↦ a ∈ φ.maxGenEigenspace 0) x ⋯)) :
      M)
    (↑0 : M)
have h : Eq.{u_3 + 1} (α := M)
  (↑((restrict φ hφV ^ n : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
        (Subtype.mk (p := fun (a : M) ↦ a ∈ φ.maxGenEigenspace 0) x sorry)) :
    M)
  0
Tactic: rw [ZeroMemClass.coe_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)
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))
      φ
hG : G.charpoly.natTrailingDegree = 0
x : M
n : ℕ
hx : Eq (α := M) ((φ ^ n : (a : M) → M) x : M) (0 : M)
⊢ Eq.{u_3 + 1} (α := M)
    (↑((restrict φ hφV ^ n : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
          (Subtype.mk (p := fun (a : M) ↦ a ∈ φ.maxGenEigenspace 0) x ⋯)) :
      M)
    0
have h : Eq (α := M)
  ((↑((restrict φ hφV ^ n : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
          (Subtype.mk (p := fun (a : M) ↦ a ∈ φ.maxGenEigenspace 0) x sorry)) :
      M) :
    M)
  ((φ ^ n : (a : M) → M) x : M)
Tactic: refine .trans ?_ hx
-- 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))
      φ
hG : G.charpoly.natTrailingDegree = 0
x : M
n : ℕ
hx : Eq (α := M) ((φ ^ n : (a : M) → M) x : M) (0 : M)
⊢ Eq (α := M)
    ((↑((restrict φ hφV ^ n : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
            (Subtype.mk (p := fun (a : M) ↦ a ∈ φ.maxGenEigenspace 0) x ⋯)) :
        M) :
      M)
    ((φ ^ n : (a : M) → M) x : M)
have h : ∀ (h' : x ∈ φ.maxGenEigenspace 0),
  Eq (α := M)
    ((↑((restrict φ hφV ^ n : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
            (Subtype.mk (p := fun (x : M) ↦ x ∈ φ.maxGenEigenspace 0) x h')) :
        M) :
      M)
    ((φ ^ n : (a : M) → M) x : M)
Tactic: generalize_proofs 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)
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))
      φ
hG : G.charpoly.natTrailingDegree = 0
x : M
n : ℕ
h' : x ∈ φ.maxGenEigenspace 0
⊢ Eq (α := M)
    ((↑((restrict φ hφV ^ n : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
            (Subtype.mk (p := fun (x : M) ↦ x ∈ φ.maxGenEigenspace 0) x h')) :
        M) :
      M)
    ((φ ^ n : (a : M) → M) x : M)
have h : Eq (α := M)
  ((↑((HPow.hPow (β := ℕ) (restrict φ hφV) 0 : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
          (Subtype.mk (p := fun (x : M) ↦ x ∈ φ.maxGenEigenspace 0) x h')) :
      M) :
    M)
  ((HPow.hPow (β := ℕ) φ 0 : (a : M) → M) x : M)
Tactic: induction n
Cleared hypotheses: 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
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))
      φ
hG : G.charpoly.natTrailingDegree = 0
x : M
n : ℕ
h' : x ∈ φ.maxGenEigenspace 0
h :
  Eq (α := M)
    ((↑((HPow.hPow (β := ℕ) (restrict φ hφV) 0 : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
            (Subtype.mk (p := fun (x : M) ↦ x ∈ φ.maxGenEigenspace 0) x h')) :
        M) :
      M)
    ((HPow.hPow (β := ℕ) φ 0 : (a : M) → M) x : M)
⊢ Eq (α := M)
    ((↑((restrict φ hφV ^ n : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
            (Subtype.mk (p := fun (x : M) ↦ x ∈ φ.maxGenEigenspace 0) x h')) :
        M) :
      M)
    ((φ ^ n : (a : M) → M) x : M)
have h₁ : ∀ (n : ℕ),
  Eq (α := M)
      ((↑((restrict φ hφV ^ n : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
              (Subtype.mk (p := fun (x : M) ↦ x ∈ φ.maxGenEigenspace 0) x h')) :
          M) :
        M)
      ((φ ^ n : (a : M) → M) x : M) →
    Eq (α := M)
      ((↑((restrict φ hφV ^ (n + 1) : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
              (Subtype.mk (p := fun (x : M) ↦ x ∈ φ.maxGenEigenspace 0) x h')) :
          M) :
        M)
      ((φ ^ (n + 1) : (a : M) → M) x : M)
Tactic: induction n
Cleared hypotheses: 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
μ : K
⊢ finrank.{u_2, u_3} K ↥(φ.maxGenEigenspace μ) = rootMultiplicity μ (charpoly φ)
have rw : finrank.{u_2, u_3} K ↥((φ - HSMul.hSMul (β := End K M) μ 1).maxGenEigenspace 0) = rootMultiplicity μ (charpoly φ)
Tactic: rw [φ.maxGenEigenspace_eq_maxGenEigenspace_zero, finrank_maxGenEigenspace_zero_eq,
    Polynomial.rootMultiplicity_eq_natTrailingDegree, LinearMap.charpoly_sub_smul]
-- 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
μ : K
rw : finrank.{u_2, u_3} K ↥((φ - HSMul.hSMul (β := End K M) μ 1).maxGenEigenspace 0) = rootMultiplicity μ (charpoly φ)
⊢ finrank.{u_2, u_3} K ↥(φ.maxGenEigenspace μ) = rootMultiplicity μ (charpoly φ)
have rw₁ : (charpoly (φ - HSMul.hSMul (β := End K M) μ 1)).natTrailingDegree = rootMultiplicity μ (charpoly φ)
Tactic: rw [φ.maxGenEigenspace_eq_maxGenEigenspace_zero, finrank_maxGenEigenspace_zero_eq,
    Polynomial.rootMultiplicity_eq_natTrailingDegree, LinearMap.charpoly_sub_smul]
-- 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
μ : K
rw : finrank.{u_2, u_3} K ↥((φ - HSMul.hSMul (β := End K M) μ 1).maxGenEigenspace 0) = rootMultiplicity μ (charpoly φ)
rw₁ : (charpoly (φ - HSMul.hSMul (β := End K M) μ 1)).natTrailingDegree = rootMultiplicity μ (charpoly φ)
⊢ finrank.{u_2, u_3} K ↥(φ.maxGenEigenspace μ) = rootMultiplicity μ (charpoly φ)
have rw₂ : (charpoly (φ - HSMul.hSMul (β := End K M) μ 1)).natTrailingDegree =
  ((charpoly φ).comp (HAdd.hAdd (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]))).natTrailingDegree
Tactic: rw [φ.maxGenEigenspace_eq_maxGenEigenspace_zero, finrank_maxGenEigenspace_zero_eq,
    Polynomial.rootMultiplicity_eq_natTrailingDegree, LinearMap.charpoly_sub_smul]
-- 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
μ : K
rw : finrank.{u_2, u_3} K ↥((φ - HSMul.hSMul (β := End K M) μ 1).maxGenEigenspace 0) = rootMultiplicity μ (charpoly φ)
rw₁ : (charpoly (φ - HSMul.hSMul (β := End K M) μ 1)).natTrailingDegree = rootMultiplicity μ (charpoly φ)
rw₂ :
  (charpoly (φ - HSMul.hSMul (β := End K M) μ 1)).natTrailingDegree =
    ((charpoly φ).comp (HAdd.hAdd (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]))).natTrailingDegree
⊢ finrank.{u_2, u_3} K ↥(φ.maxGenEigenspace μ) = rootMultiplicity μ (charpoly φ)
have rw₃ : ((charpoly φ).comp (HAdd.hAdd (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]))).natTrailingDegree =
  ((charpoly φ).comp (HAdd.hAdd (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]))).natTrailingDegree
Tactic: rw [φ.maxGenEigenspace_eq_maxGenEigenspace_zero, finrank_maxGenEigenspace_zero_eq,
    Polynomial.rootMultiplicity_eq_natTrailingDegree, LinearMap.charpoly_sub_smul]
-- 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
μ : K
k : ℕ
⊢ finrank.{u_2, u_3} K ↥((φ.genEigenspace μ : (a : ℕ∞) → Submodule K M) (↑k : ℕ∞) : Submodule K M) ≤
    rootMultiplicity μ (charpoly φ)
have grw : finrank.{u_2, u_3} K ↥(φ.maxGenEigenspace μ) ≤ rootMultiplicity μ (charpoly φ)
Tactic: grw [Submodule.finrank_mono (φ.genEigenspace_le_maximal μ k), finrank_maxGenEigenspace_eq]
-- 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
μ : K
k : ℕ
grw : finrank.{u_2, u_3} K ↥(φ.maxGenEigenspace μ) ≤ rootMultiplicity μ (charpoly φ)
⊢ finrank.{u_2, u_3} K ↥((φ.genEigenspace μ : (a : ℕ∞) → Submodule K M) (↑k : ℕ∞) : Submodule K M) ≤
    rootMultiplicity μ (charpoly φ)
have grw₁ : rootMultiplicity μ (charpoly φ) ≤ rootMultiplicity μ (charpoly φ)
Tactic: grw [Submodule.finrank_mono (φ.genEigenspace_le_maximal μ k), finrank_maxGenEigenspace_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
A : Type u_1
inst_3 : Semiring A
inst_4 : Algebra R A
g : ExteriorAlgebra R M →ₐ[R] A
m : M
⊢ HMul.hMul (α := A) (β := A)
      ((g : (a : ExteriorAlgebra R M) → A) ((ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M) : A)
      ((g : (a : ExteriorAlgebra R M) → A) ((ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M) : A) =
    0
have rw : Eq.{u_1 + 1} (α := A)
  ((g : (a : ExteriorAlgebra R M) → A)
      (HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
        ((ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M)
        ((ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M)) :
    A)
  (0 : A)
Tactic: rw [← map_mul, ι_sq_zero, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
A : Type u_1
inst_3 : Semiring A
inst_4 : Algebra R A
g : ExteriorAlgebra R M →ₐ[R] A
m : M
rw :
  Eq.{u_1 + 1} (α := A)
    ((g : (a : ExteriorAlgebra R M) → A)
        (HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
          ((ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M)
          ((ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M)) :
      A)
    (0 : A)
⊢ HMul.hMul (α := A) (β := A)
      ((g : (a : ExteriorAlgebra R M) → A) ((ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M) : A)
      ((g : (a : ExteriorAlgebra R M) → A) ((ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M) : A) =
    0
have rw₁ : Eq.{u_1 + 1} (α := A) ((g : (a : ExteriorAlgebra R M) → A) 0 : A) (0 : A)
Tactic: rw [← map_mul, ι_sq_zero, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
A : Type u_1
inst_3 : Semiring A
inst_4 : Algebra R A
g : ExteriorAlgebra R M →ₐ[R] A
m : M
rw :
  Eq.{u_1 + 1} (α := A)
    ((g : (a : ExteriorAlgebra R M) → A)
        (HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
          ((ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M)
          ((ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M)) :
      A)
    (0 : A)
rw₁ : Eq.{u_1 + 1} (α := A) ((g : (a : ExteriorAlgebra R M) → A) 0 : A) (0 : A)
⊢ HMul.hMul (α := A) (β := A)
      ((g : (a : ExteriorAlgebra R M) → A) ((ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M) : A)
      ((g : (a : ExteriorAlgebra R M) → A) ((ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M) : A) =
    0
have rw₂ : Eq.{u_1 + 1} (α := A) 0 0
Tactic: rw [← map_mul, ι_sq_zero, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (hypothesis)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
A : Type u_1
inst_3 : Semiring A
inst_4 : Algebra R A
this : Module.{u1, u2} Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) ⋯)
⊢ ExteriorAlgebra R M →ₗ[R] M
have this₁ : IsCentralScalar R M
Tactic: haveI : IsCentralScalar R M := ⟨fun r m => rfl⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
⊢ Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
      (0 : ExteriorAlgebra R M) ↔
    x = 0
have rw : Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
    (0 : ExteriorAlgebra R M) ↔
  Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
    ((ι R : (a : M) → ExteriorAlgebra R M) 0 : ExteriorAlgebra R M)
Tactic: rw [← ι_inj R x 0, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
rw :
  Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
      (0 : ExteriorAlgebra R M) ↔
    Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
      ((ι R : (a : M) → ExteriorAlgebra R M) 0 : ExteriorAlgebra R M)
⊢ Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
      (0 : ExteriorAlgebra R M) ↔
    x = 0
have rw₁ : Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
    (0 : ExteriorAlgebra R M) ↔
  Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
    (0 : ExteriorAlgebra R M)
Tactic: rw [← ι_inj R x 0, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
r : R
⊢ Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
      ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M) ↔
    x = 0 ∧ r = 0
have refine_1 : ∀
  (h :
    Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
      ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M)),
  x = 0 ∧ r = 0
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
r : R
refine_1 :
  ∀
    (h :
      Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
        ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M)),
    x = 0 ∧ r = 0
⊢ Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
      ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M) ↔
    x = 0 ∧ r = 0
have refine_2 : x = 0 ∧ r = 0 →
  Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
    ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M)
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (hypothesis)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
r : R
h :
  Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
    ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M)
this : Module.{u1, u2} Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) ⋯)
⊢ x = 0 ∧ r = 0
have this₁ : IsCentralScalar R M
Tactic: haveI : IsCentralScalar R M := ⟨fun r m => rfl⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (hypothesis)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
r : R
h :
  Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
    ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M)
this_1 : Module.{u1, u2} Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) ⋯)
this : IsCentralScalar R M
⊢ x = 0 ∧ r = 0
have hf0 : Eq (α := TrivSqZeroExt R M)
  ((toTrivSqZeroExt : (a : ExteriorAlgebra R M) → TrivSqZeroExt R M) ((ι R : (a : M) → ExteriorAlgebra R M) x) :
    TrivSqZeroExt R M)
  ((0, x) : R × M)
Tactic: have hf0 : toTrivSqZeroExt (ι R x) = (0, x) := toTrivSqZeroExt_ι _
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (hypothesis)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
r : R
h :
  Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
    ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M)
this_1 : Module.{u1, u2} Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) ⋯)
this : IsCentralScalar R M
hf0 :
  Eq (α := TrivSqZeroExt R M)
    ((toTrivSqZeroExt : (a : ExteriorAlgebra R M) → TrivSqZeroExt R M) ((ι R : (a : M) → ExteriorAlgebra R M) x) :
      TrivSqZeroExt R M)
    ((0, x) : R × M)
⊢ x = 0 ∧ r = 0
have hf0₁ : Eq (α := TrivSqZeroExt R M) ((algebraMap R (TrivSqZeroExt R M) : (a : R) → TrivSqZeroExt R M) r : TrivSqZeroExt R M)
  ((0, x) : R × M)
Tactic: rw [h, AlgHom.commutes] at hf0
Cleared hypotheses: hf0