awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
I : Ideal R
h_1 : Nontrivial R
s : Finset M
hs_card : s.card = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤
hs_span : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
this :
  Eq.{u_2 + 1} (α := Submodule R M) (Submodule.span R (Set.range (ι := ↥s) (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) ⊤
A : ↥(isRepresentation R (Subtype.val (p := fun (x : M) ↦ x ∈ s)))
h : ∀ (i j : ↥s), (↑A : Matrix (↥s) (↥s) R) i j ∈ I
hI :
  range (R := R) (M := M) (τ₁₂ := RingHom.id R)
      ((isRepresentation.toEnd R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) this :
          (a : ↥(isRepresentation R Subtype.val)) → Module.End R M)
        A) ≤
    HSMul.hSMul (β := Submodule R M) I ⊤
inr :
  Eq (α := Matrix.{u_2, u_2, u_3} (↥s) (↥s) R)
    ((aeval (↑A : Matrix (↥s) (↥s) R) : (a : R[X]) → Matrix (↥s) (↥s) R) (↑A : Matrix (↥s) (↥s) R).charpoly :
      Matrix.{u_2, u_2, u_3} (↥s) (↥s) R)
    ((↑0 : Matrix.{u_2, u_2, u_3} (↥s) (↥s) R) : Matrix.{u_2, u_2, u_3} (↥s) (↥s) R)
inr₁ : Eq (α := Matrix.{u_2, u_2, u_3} (↥s) (↥s) R) 0 (↑0 : Matrix (↥s) (↥s) R)
⊢ Eq (α := Matrix.{u_2, u_2, u_3} (↥s) (↥s) R)
    (↑((aeval A : (a : R[X]) → ↥(isRepresentation R Subtype.val)) (↑A : Matrix (↥s) (↥s) R).charpoly) :
      Matrix (↥s) (↥s) R)
    (↑0 : Matrix (↥s) (↥s) R)
have inr₂ : Eq (α := Matrix.{u_2, u_2, u_3} (↥s) (↥s) R) 0 0
Tactic: rw [Polynomial.aeval_subalgebra_coe, Matrix.aeval_self_charpoly, Subalgebra.coe_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ HSMul.hSMul (β := Submodule R M) I ⊤
⊢ ∃ (p : R[X]),
    p.Monic ∧
      p.natDegree = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤ ∧
        (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧
          Eq.{u_2 + 1} (α := Module.End R M) ((aeval f : (a : R[X]) → Module.End R M) p : Module.End R M)
            (0 : Module.End R M)
have inl : Subsingleton R →
  ∃ (p : R[X]),
    p.Monic ∧
      p.natDegree = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤ ∧
        (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧
          Eq.{u_2 + 1} (α := Module.End R M) ((aeval f : (a : R[X]) → Module.End R M) p : Module.End R M)
            (0 : Module.End R M)
Tactic: classical
    cases subsingleton_or_nontrivial R
    · exact ⟨0, by simp [nontriviality]⟩
    obtain ⟨s, hs_card, hs_span⟩ :=
      Submodule.FG.exists_span_finset_card_eq_spanFinrank (R := R) (M := M) Module.Finite.fg_top
    have : Submodule.span R (Set.range ((↑) : s → M)) = ⊤ := by simp [hs_span]
    obtain ⟨A, rfl, h⟩ := Matrix.isRepresentation.toEnd_exists_mem_ideal R ((↑) : s → M) this f I hI
    refine ⟨A.1.charpoly, A.1.charpoly_monic, by simp [hs_card],
            by simpa using coeff_charpoly_mem_ideal_pow h, ?_⟩
    rw [Polynomial.aeval_algHom_apply,
      ← map_zero (Matrix.isRepresentation.toEnd R ((↑) : s → M) this)]
    congr 1
    ext1
    rw [Polynomial.aeval_subalgebra_coe, Matrix.aeval_self_charpoly, Subalgebra.coe_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ HSMul.hSMul (β := Submodule R M) I ⊤
inl :
  Subsingleton R →
    ∃ (p : R[X]),
      p.Monic ∧
        p.natDegree = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤ ∧
          (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧
            Eq.{u_2 + 1} (α := Module.End R M) ((aeval f : (a : R[X]) → Module.End R M) p : Module.End R M)
              (0 : Module.End R M)
⊢ ∃ (p : R[X]),
    p.Monic ∧
      p.natDegree = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤ ∧
        (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧
          Eq.{u_2 + 1} (α := Module.End R M) ((aeval f : (a : R[X]) → Module.End R M) p : Module.End R M)
            (0 : Module.End R M)
have inr : Nontrivial R →
  ∃ (p : R[X]),
    p.Monic ∧
      p.natDegree = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤ ∧
        (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧
          Eq.{u_2 + 1} (α := Module.End R M) ((aeval f : (a : R[X]) → Module.End R M) p : Module.End R M)
            (0 : Module.End R M)
Tactic: classical
    cases subsingleton_or_nontrivial R
    · exact ⟨0, by simp [nontriviality]⟩
    obtain ⟨s, hs_card, hs_span⟩ :=
      Submodule.FG.exists_span_finset_card_eq_spanFinrank (R := R) (M := M) Module.Finite.fg_top
    have : Submodule.span R (Set.range ((↑) : s → M)) = ⊤ := by simp [hs_span]
    obtain ⟨A, rfl, h⟩ := Matrix.isRepresentation.toEnd_exists_mem_ideal R ((↑) : s → M) this f I hI
    refine ⟨A.1.charpoly, A.1.charpoly_monic, by simp [hs_card],
            by simpa using coeff_charpoly_mem_ideal_pow h, ?_⟩
    rw [Polynomial.aeval_algHom_apply,
      ← map_zero (Matrix.isRepresentation.toEnd R ((↑) : s → M) this)]
    congr 1
    ext1
    rw [Polynomial.aeval_subalgebra_coe, Matrix.aeval_self_charpoly, Subalgebra.coe_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ HSMul.hSMul (β := Submodule R M) I ⊤
inl :
  Subsingleton R →
    ∃ (p : R[X]),
      p.Monic ∧
        p.natDegree = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤ ∧
          (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧
            Eq.{u_2 + 1} (α := Module.End R M) ((aeval f : (a : R[X]) → Module.End R M) p : Module.End R M)
              (0 : Module.End R M)
inr inr₁ :
  Nontrivial R →
    ∃ (p : R[X]),
      p.Monic ∧
        p.natDegree = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤ ∧
          (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧
            Eq.{u_2 + 1} (α := Module.End R M) ((aeval f : (a : R[X]) → Module.End R M) p : Module.End R M)
              (0 : Module.End R M)
⊢ ∃ (p : R[X]),
    p.Monic ∧
      p.natDegree = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤ ∧
        (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧
          Eq.{u_2 + 1} (α := Module.End R M) ((aeval f : (a : R[X]) → Module.End R M) p : Module.End R M)
            (0 : Module.End R M)
have inr₂ : Nontrivial R →
  ∀ (s : Finset M) (hs_card : s.card = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤)
    (hs_span : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤),
    ∃ (p : R[X]),
      p.Monic ∧
        p.natDegree = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤ ∧
          (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧
            Eq.{u_2 + 1} (α := Module.End R M) ((aeval f : (a : R[X]) → Module.End R M) p : Module.End R M)
              (0 : Module.End R M)
Tactic: classical
    cases subsingleton_or_nontrivial R
    · exact ⟨0, by simp [nontriviality]⟩
    obtain ⟨s, hs_card, hs_span⟩ :=
      Submodule.FG.exists_span_finset_card_eq_spanFinrank (R := R) (M := M) Module.Finite.fg_top
    have : Submodule.span R (Set.range ((↑) : s → M)) = ⊤ := by simp [hs_span]
    obtain ⟨A, rfl, h⟩ := Matrix.isRepresentation.toEnd_exists_mem_ideal R ((↑) : s → M) this f I hI
    refine ⟨A.1.charpoly, A.1.charpoly_monic, by simp [hs_card],
            by simpa using coeff_charpoly_mem_ideal_pow h, ?_⟩
    rw [Polynomial.aeval_algHom_apply,
      ← map_zero (Matrix.isRepresentation.toEnd R ((↑) : s → M) this)]
    congr 1
    ext1
    rw [Polynomial.aeval_subalgebra_coe, Matrix.aeval_self_charpoly, Subalgebra.coe_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ HSMul.hSMul (β := Submodule R M) I ⊤
inl :
  Subsingleton R →
    ∃ (p : R[X]),
      p.Monic ∧
        p.natDegree = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤ ∧
          (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧
            Eq.{u_2 + 1} (α := Module.End R M) ((aeval f : (a : R[X]) → Module.End R M) p : Module.End R M)
              (0 : Module.End R M)
inr inr₁ :
  Nontrivial R →
    ∃ (p : R[X]),
      p.Monic ∧
        p.natDegree = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤ ∧
          (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧
            Eq.{u_2 + 1} (α := Module.End R M) ((aeval f : (a : R[X]) → Module.End R M) p : Module.End R M)
              (0 : Module.End R M)
inr₂ :
  Nontrivial R →
    ∀ (s : Finset M) (hs_card : s.card = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤)
      (hs_span : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤),
      ∃ (p : R[X]),
        p.Monic ∧
          p.natDegree = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤ ∧
            (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧
              Eq.{u_2 + 1} (α := Module.End R M) ((aeval f : (a : R[X]) → Module.End R M) p : Module.End R M)
                (0 : Module.End R M)
⊢ ∃ (p : R[X]),
    p.Monic ∧
      p.natDegree = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤ ∧
        (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧
          Eq.{u_2 + 1} (α := Module.End R M) ((aeval f : (a : R[X]) → Module.End R M) p : Module.End R M)
            (0 : Module.End R M)
have inr₃ : Nontrivial R →
  ∀ (s : Finset M) (hs_card : s.card = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤)
    (hs_span : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤)
    (this :
      Eq.{u_2 + 1} (α := Submodule R M)
        (Submodule.span R (Set.range (ι := ↥s) (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) ⊤),
    ∃ (p : R[X]),
      p.Monic ∧
        p.natDegree = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤ ∧
          (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧
            Eq.{u_2 + 1} (α := Module.End R M) ((aeval f : (a : R[X]) → Module.End R M) p : Module.End R M)
              (0 : Module.End R M)
Tactic: classical
    cases subsingleton_or_nontrivial R
    · exact ⟨0, by simp [nontriviality]⟩
    obtain ⟨s, hs_card, hs_span⟩ :=
      Submodule.FG.exists_span_finset_card_eq_spanFinrank (R := R) (M := M) Module.Finite.fg_top
    have : Submodule.span R (Set.range ((↑) : s → M)) = ⊤ := by simp [hs_span]
    obtain ⟨A, rfl, h⟩ := Matrix.isRepresentation.toEnd_exists_mem_ideal R ((↑) : s → M) this f I hI
    refine ⟨A.1.charpoly, A.1.charpoly_monic, by simp [hs_card],
            by simpa using coeff_charpoly_mem_ideal_pow h, ?_⟩
    rw [Polynomial.aeval_algHom_apply,
      ← map_zero (Matrix.isRepresentation.toEnd R ((↑) : s → M) this)]
    congr 1
    ext1
    rw [Polynomial.aeval_subalgebra_coe, Matrix.aeval_self_charpoly, Subalgebra.coe_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly (goal)
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : Ring S
inst_2 : Algebra R S
h : PowerBasis R S
⊢ Eq (α := R[X])
    (charpoly (n := Fin h.dim)
      (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) : (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
        h.gen))
    (minpoly R h.gen)
have inl : Subsingleton R →
  Eq (α := R[X])
    (charpoly (n := Fin h.dim)
      (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) : (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
        h.gen))
    (minpoly R h.gen)
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly (goal)
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : Ring S
inst_2 : Algebra R S
h : PowerBasis R S
inl :
  Subsingleton R →
    Eq (α := R[X])
      (charpoly (n := Fin h.dim)
        (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) :
            (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
          h.gen))
      (minpoly R h.gen)
⊢ Eq (α := R[X])
    (charpoly (n := Fin h.dim)
      (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) : (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
        h.gen))
    (minpoly R h.gen)
have inr : Nontrivial R →
  Eq (α := R[X])
    (charpoly (n := Fin h.dim)
      (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) : (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
        h.gen))
    (minpoly R h.gen)
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly (goal)
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : Ring S
inst_2 : Algebra R S
h : PowerBasis R S
h_1 : Nontrivial R
⊢ Eq (α := R[X])
    (charpoly (n := Fin h.dim)
      (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) : (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
        h.gen))
    (minpoly R h.gen)
have inr : Eq.{u_1 + 1} (α := S)
  ((aeval h.gen : (a : R[X]) → S)
      (charpoly (n := Fin h.dim)
        (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) :
            (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
          h.gen)) :
    S)
  (0 : S)
Tactic: apply minpoly.unique' R h.gen (charpoly_monic _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly (goal)
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : Ring S
inst_2 : Algebra R S
h : PowerBasis R S
h_1 : Nontrivial R
inr :
  Eq.{u_1 + 1} (α := S)
    ((aeval h.gen : (a : R[X]) → S)
        (charpoly (n := Fin h.dim)
          (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) :
              (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
            h.gen)) :
      S)
    (0 : S)
⊢ Eq (α := R[X])
    (charpoly (n := Fin h.dim)
      (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) : (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
        h.gen))
    (minpoly R h.gen)
have inr₁ : ∀ (q : R[X]),
  q.degree <
      degree.{u} (R := R)
        (charpoly (n := Fin h.dim)
          (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) :
              (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
            h.gen)) →
    q = 0 ∨ Ne.{u_1 + 1} (α := S) ((aeval h.gen : (a : R[X]) → S) q : S) (0 : S)
Tactic: apply minpoly.unique' R h.gen (charpoly_monic _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly (goal)
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : Ring S
inst_2 : Algebra R S
h : PowerBasis R S
h_1 : Nontrivial R
⊢ Eq.{u_1 + 1} (α := S)
    ((aeval h.gen : (a : R[X]) → S)
        (charpoly (n := Fin h.dim)
          (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) :
              (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
            h.gen)) :
      S)
    (0 : S)
have inr : Eq.{u + 1} (α := Matrix (Fin h.dim) (Fin h.dim) R)
  (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) : (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
      ((aeval h.gen : (a : R[X]) → S)
        (charpoly (n := Fin h.dim)
          (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) :
              (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
            h.gen))) :
    Matrix (Fin h.dim) (Fin h.dim) R)
  (0 : Matrix (Fin h.dim) (Fin h.dim) R)
Tactic: apply (injective_iff_map_eq_zero (G := S) (leftMulMatrix _)).mp
      (leftMulMatrix_injective h.basis)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly (goal)
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : Ring S
inst_2 : Algebra R S
h : PowerBasis R S
h_1 : Nontrivial R
⊢ Eq.{u + 1} (α := Matrix (Fin h.dim) (Fin h.dim) R)
    (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) : (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
        ((aeval h.gen : (a : R[X]) → S)
          (charpoly (n := Fin h.dim)
            (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) :
                (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
              h.gen))) :
      Matrix (Fin h.dim) (Fin h.dim) R)
    (0 : Matrix (Fin h.dim) (Fin h.dim) R)
have inr : Eq.{u + 1} (α := Matrix (Fin h.dim) (Fin h.dim) R)
  (((aeval
            (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) :
                (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
              h.gen) :
          R[X] →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) :
        (a : R[X]) → Matrix (Fin h.dim) (Fin h.dim) R)
      (charpoly (n := Fin h.dim)
        (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) :
            (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
          h.gen)) :
    Matrix (Fin h.dim) (Fin h.dim) R)
  (0 : Matrix (Fin h.dim) (Fin h.dim) R)
Tactic: rw [← Polynomial.aeval_algHom_apply, aeval_self_charpoly]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly (goal)
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : Ring S
inst_2 : Algebra R S
h : PowerBasis R S
h_1 : Nontrivial R
inr :
  Eq.{u + 1} (α := Matrix (Fin h.dim) (Fin h.dim) R)
    (((aeval
              (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) :
                  (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
                h.gen) :
            R[X] →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) :
          (a : R[X]) → Matrix (Fin h.dim) (Fin h.dim) R)
        (charpoly (n := Fin h.dim)
          (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) :
              (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
            h.gen)) :
      Matrix (Fin h.dim) (Fin h.dim) R)
    (0 : Matrix (Fin h.dim) (Fin h.dim) R)
⊢ Eq.{u + 1} (α := Matrix (Fin h.dim) (Fin h.dim) R)
    (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) : (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
        ((aeval h.gen : (a : R[X]) → S)
          (charpoly (n := Fin h.dim)
            (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) :
                (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
              h.gen))) :
      Matrix (Fin h.dim) (Fin h.dim) R)
    (0 : Matrix (Fin h.dim) (Fin h.dim) R)
have inr₁ : Eq.{u + 1} (α := Matrix (Fin h.dim) (Fin h.dim) R) 0 0
Tactic: rw [← Polynomial.aeval_algHom_apply, aeval_self_charpoly]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly (goal)
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : Ring S
inst_2 : Algebra R S
h : PowerBasis R S
h_1 : Nontrivial R
⊢ ∀ (q : R[X]),
    q.degree <
        degree.{u} (R := R)
          (charpoly (n := Fin h.dim)
            (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) :
                (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
              h.gen)) →
      q = 0 ∨ Ne.{u_1 + 1} (α := S) ((aeval h.gen : (a : R[X]) → S) q : S) (0 : S)
have inr : ∀ (q : R[X])
  (hq :
    q.degree <
      degree.{u} (R := R)
        (charpoly (n := Fin h.dim)
          (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) :
              (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
            h.gen)))
  (h0 : ¬q = 0), Ne.{u_1 + 1} (α := S) ((aeval h.gen : (a : R[X]) → S) q : S) (0 : S)
Tactic: refine fun q hq => or_iff_not_imp_left.2 fun h0 => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly (hypothesis)
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : Ring S
inst_2 : Algebra R S
h : PowerBasis R S
h_1 : Nontrivial R
q : R[X]
hq :
  q.degree <
    degree.{u} (R := R)
      (charpoly (n := Fin h.dim)
        (((leftMulMatrix h.basis : S →ₐ[R] Matrix (Fin h.dim) (Fin h.dim) R) :
            (a : S) → Matrix (Fin h.dim) (Fin h.dim) R)
          h.gen))
h0 : ¬q = 0
⊢ Ne.{u_1 + 1} (α := S) ((aeval h.gen : (a : R[X]) → S) q : S) (0 : S)
have hq₁ : q.degree < (↑h.dim : WithBot ℕ)
Tactic: rw [Matrix.charpoly_degree_eq_dim, Fintype.card_fin] at hq
Cleared hypotheses: hq, h0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly (goal)
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : Ring S
inst_2 : Algebra R S
h : PowerBasis R S
h_1 : Nontrivial R
q : R[X]
hq : q.degree < (↑h.dim : WithBot ℕ)
h0 : ¬q = 0
⊢ Ne.{u_1 + 1} (α := S) ((aeval h.gen : (a : R[X]) → S) q : S) (0 : S)
have inr : ∀ (hq : Eq.{u_1 + 1} (α := S) ((aeval h.gen : (a : R[X]) → S) q : S) (0 : S)), (↑h.dim : WithBot ℕ) ≤ q.degree
Tactic: contrapose! hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Univ (goal)
Goal:
R : Type u_1
S : Type u_2
n : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fintype n
inst_3 : DecidableEq n
f : R →+* S
M : n × n → S
⊢ Polynomial.map (eval₂Hom f M) (univ R n) =
    charpoly.{u_2, u_3} (n := n) ((of : (a : n → n → S) → Matrix n n S) (Function.curry M))
have rw : Eq (α := Polynomial S) (map (mvPolynomialX n n R) (eval₂ f M)).charpoly
  (map (mvPolynomialX n n R)
      (eval₂ f fun (p : n × n) ↦ (of : (a : n → n → S) → Matrix n n S) (Function.curry M) p.1 p.2)).charpoly
Tactic: rw [univ, ← charpoly_map, coe_eval₂Hom, ← mvPolynomialX_map_eval₂ f (Matrix.of M.curry)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Univ (goal)
Goal:
R : Type u_1
S : Type u_2
n : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fintype n
inst_3 : DecidableEq n
f : R →+* S
⊢ Polynomial.map (MvPolynomial.map f) (univ R n) = univ S n
have rw : Eq (α := Polynomial (MvPolynomial.{u_3, u_2} (n × n) S))
  (charpoly (n := n)
    ((of : (a : n → n → MvPolynomial (n × n) S) → Matrix n n (MvPolynomial (n × n) S)) (Function.curry MvPolynomial.X)))
  (univ S n)
Tactic: rw [MvPolynomial.map_eq_eval₂Hom_C_comp, univ_map_eval₂Hom]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Univ (goal)
Goal:
R : Type u_1
S : Type u_2
n : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fintype n
inst_3 : DecidableEq n
f : R →+* S
M : n × n → S
i : ℕ
⊢ Eq.{u_2 + 1} (α := S)
    ((MvPolynomial.eval₂Hom f M : (a : MvPolynomial (n × n) R) → S) (Polynomial.coeff (univ R n) i) : S)
    (Polynomial.coeff (charpoly.{u_2, u_3} (n := n) ((of : (a : n → n → S) → Matrix n n S) (Function.curry M))) i : S)
have rw : (MvPolynomial.eval₂Hom f M : (a : MvPolynomial (n × n) R) → S) (Polynomial.coeff (univ R n) i) =
  (Polynomial.map (MvPolynomial.eval₂Hom f M) (univ R n)).coeff i
Tactic: rw [← univ_map_eval₂Hom n f M, Polynomial.coeff_map]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Univ (goal)
Goal:
R : Type u_1
S : Type u_2
n : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fintype n
inst_3 : DecidableEq n
f : R →+* S
M : n × n → S
i : ℕ
rw :
  (MvPolynomial.eval₂Hom f M : (a : MvPolynomial (n × n) R) → S) (Polynomial.coeff (univ R n) i) =
    (Polynomial.map (MvPolynomial.eval₂Hom f M) (univ R n)).coeff i
⊢ Eq.{u_2 + 1} (α := S)
    ((MvPolynomial.eval₂Hom f M : (a : MvPolynomial (n × n) R) → S) (Polynomial.coeff (univ R n) i) : S)
    (Polynomial.coeff (charpoly.{u_2, u_3} (n := n) ((of : (a : n → n → S) → Matrix n n S) (Function.curry M))) i : S)
have rw₁ : Eq.{u_2 + 1} (α := S)
  ((MvPolynomial.eval₂Hom f M : (a : MvPolynomial (n × n) R) → S) (Polynomial.coeff (univ R n) i) : S)
  ((MvPolynomial.eval₂Hom f M : (a : MvPolynomial (n × n) R) → S) (Polynomial.coeff (univ R n) i) : S)
Tactic: rw [← univ_map_eval₂Hom n f M, Polynomial.coeff_map]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Univ (goal)
Goal:
R : Type u_1
n : Type u_3
inst : CommRing R
inst_1 : Fintype n
inst_2 : DecidableEq n
this : Eq (α := MvPolynomial (n × n) ℤ) (Polynomial.coeff (univ ℤ n) (Fintype.card n)) 1
⊢ Eq (α := MvPolynomial.{u_3, u_1} (n × n) R) (Polynomial.coeff (univ R n) (Fintype.card n)) 1
have rw : Eq (α := MvPolynomial.{u_3, u_1} (n × n) R)
  (Polynomial.coeff (Polynomial.map (R := MvPolynomial (n × n) ℤ) (MvPolynomial.map (Int.castRingHom R)) (univ ℤ n))
    (Fintype.card n))
  1
Tactic: rw [← univ_map_map n (Int.castRingHom R), Polynomial.coeff_map, this, map_one]