awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
h : Nontrivial B
H :
  HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
            (⟨0, ⋯⟩ : Fin pb.dim) :
          A)
        ((pb.basis : (a : Fin pb.dim) → B) (⟨0, ⋯⟩ : Fin pb.dim) : B) +
      ∑ x ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim),
        HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
          ((pb.basis : (a : Fin pb.dim) → B) x : B) =
    b
i : Fin pb.dim
hi : i ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim)
⊢ Membership.mem (γ := Ideal B) (Ideal.span {pb.gen})
    (HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
      ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) i : A)
      ((fun (i : Fin pb.dim) ↦ pb.gen ^ (↑i : ℕ)) i))
have inr : Membership.mem (γ := Ideal B) (Ideal.span {pb.gen})
  (HMul.hMul (α := B) (β := B)
    ((algebraMap A B : (a : A) → B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) i : A) :
      B)
    ((fun (i : Fin pb.dim) ↦ pb.gen ^ (↑i : ℕ)) i : B))
Tactic: rw [Algebra.smul_def']
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
pb : PowerBasis A S
⊢ Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : A[X]) → S) pb.minpolyGen : S) (0 : S)
have simp_rw : pb.gen ^ pb.dim -
    ∑ x : Fin pb.dim,
      HSMul.hSMul.{u_4, u_2, u_2} (α := A)
        ((((pb.basis.repr : (a : S) → Fin pb.dim →₀ A) (pb.gen ^ pb.dim) : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x :
          A)
        (pb.gen ^ (↑x : ℕ)) =
  0
Tactic: simp_rw [minpolyGen, map_sub, map_sum, map_mul, map_pow, aeval_C, ← Algebra.smul_def, aeval_X]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
pb : PowerBasis A S
⊢ pb.gen ^ pb.dim -
      ∑ x : Fin pb.dim,
        HSMul.hSMul.{u_4, u_2, u_2} (α := A)
          ((((pb.basis.repr : (a : S) → Fin pb.dim →₀ A) (pb.gen ^ pb.dim) : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
              x :
            A)
          (pb.gen ^ (↑x : ℕ)) =
    0
have refine : Eq.{u_2 + 1} (α := S)
  ((linearCombination A (⇑pb.basis : (a : Fin pb.dim) → S) : (a : Fin pb.dim →₀ A) → S)
      ((pb.basis.repr : (a : S) → Fin pb.dim →₀ A) (pb.gen ^ pb.dim) : Fin pb.dim →₀ A) :
    S)
  (∑ x : Fin pb.dim,
      HSMul.hSMul.{u_4, u_2, u_2} (α := A)
        ((((pb.basis.repr : (a : S) → Fin pb.dim →₀ A) (pb.gen ^ pb.dim) : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x :
          A)
        (pb.gen ^ (↑x : ℕ)) :
    S)
Tactic: refine sub_eq_zero.mpr ((pb.basis.linearCombination_repr (pb.gen ^ pb.dim)).symm.trans ?_)
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
pb : PowerBasis A S
⊢ Eq.{u_2 + 1} (α := S)
    ((linearCombination A (⇑pb.basis : (a : Fin pb.dim) → S) : (a : Fin pb.dim →₀ A) → S)
        ((pb.basis.repr : (a : S) → Fin pb.dim →₀ A) (pb.gen ^ pb.dim) : Fin pb.dim →₀ A) :
      S)
    (∑ x : Fin pb.dim,
        HSMul.hSMul.{u_4, u_2, u_2} (α := A)
          ((((pb.basis.repr : (a : S) → Fin pb.dim →₀ A) (pb.gen ^ pb.dim) : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
              x :
            A)
          (pb.gen ^ (↑x : ℕ)) :
      S)
have rw : Eq.{u_2 + 1} (α := S)
  (∑ i : Fin pb.dim,
    HSMul.hSMul.{u_4, u_2, u_2} (α := A) (β := S)
      ((((pb.basis.repr : (a : S) → Fin pb.dim →₀ A) (pb.gen ^ pb.dim) : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) i : A)
      ((pb.basis : (a : Fin pb.dim) → S) i : S))
  (∑ x : Fin pb.dim,
    HSMul.hSMul.{u_4, u_2, u_2} (α := A)
      ((((pb.basis.repr : (a : S) → Fin pb.dim →₀ A) (pb.gen ^ pb.dim) : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
      (pb.gen ^ (↑x : ℕ)))
Tactic: rw [Finsupp.linearCombination_apply, Finsupp.sum_fintype]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
pb : PowerBasis A S
rw :
  Eq.{u_2 + 1} (α := S)
    (∑ i : Fin pb.dim,
      HSMul.hSMul.{u_4, u_2, u_2} (α := A) (β := S)
        ((((pb.basis.repr : (a : S) → Fin pb.dim →₀ A) (pb.gen ^ pb.dim) : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) i :
          A)
        ((pb.basis : (a : Fin pb.dim) → S) i : S))
    (∑ x : Fin pb.dim,
      HSMul.hSMul.{u_4, u_2, u_2} (α := A)
        ((((pb.basis.repr : (a : S) → Fin pb.dim →₀ A) (pb.gen ^ pb.dim) : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x :
          A)
        (pb.gen ^ (↑x : ℕ)))
⊢ Eq.{u_2 + 1} (α := S)
    ((linearCombination A (⇑pb.basis : (a : Fin pb.dim) → S) : (a : Fin pb.dim →₀ A) → S)
        ((pb.basis.repr : (a : S) → Fin pb.dim →₀ A) (pb.gen ^ pb.dim) : Fin pb.dim →₀ A) :
      S)
    (∑ x : Fin pb.dim,
        HSMul.hSMul.{u_4, u_2, u_2} (α := A)
          ((((pb.basis.repr : (a : S) → Fin pb.dim →₀ A) (pb.gen ^ pb.dim) : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
              x :
            A)
          (pb.gen ^ (↑x : ℕ)) :
      S)
have h : ∀ (i : Fin pb.dim), HSMul.hSMul.{u_4, u_2, u_2} (α := A) (β := S) 0 ((pb.basis : (a : Fin pb.dim) → S) i : S) = 0
Tactic: rw [Finsupp.linearCombination_apply, Finsupp.sum_fintype]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (hypothesis)
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
pb : PowerBasis A S
⊢ pb.minpolyGen.Monic
have a : Nontrivial A
Tactic: nontriviality A
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
pb : PowerBasis A S
h : Nontrivial A
⊢ pb.minpolyGen.Monic
have apply : degree.{u_4} (R := A)
    (∑ i : Fin pb.dim,
      HMul.hMul (α := A[X])
        ((C : (a : A) → A[X])
            ((((pb.basis.repr : (a : S) → Fin pb.dim →₀ A) (pb.gen ^ pb.dim) : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
              i) :
          A[X])
        (HPow.hPow (α := A[X]) X (↑i : ℕ))) <
  (HPow.hPow (α := A[X]) X pb.dim).degree
Tactic: apply (monic_X_pow _).sub_of_left _
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
pb : PowerBasis A S
h : Nontrivial A
⊢ degree.{u_4} (R := A)
      (∑ i : Fin pb.dim,
        HMul.hMul (α := A[X])
          ((C : (a : A) → A[X])
              ((((pb.basis.repr : (a : S) → Fin pb.dim →₀ A) (pb.gen ^ pb.dim) : Fin pb.dim →₀ A) :
                  (a : Fin pb.dim) → A)
                i) :
            A[X])
          (HPow.hPow (α := A[X]) X (↑i : ℕ))) <
    (HPow.hPow (α := A[X]) X pb.dim).degree
have rw : degree.{u_4} (R := A)
    (∑ i : Fin pb.dim,
      HMul.hMul (α := A[X])
        ((C : (a : A) → A[X])
            ((((pb.basis.repr : (a : S) → Fin pb.dim →₀ A) (pb.gen ^ pb.dim) : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
              i) :
          A[X])
        (HPow.hPow (α := A[X]) X (↑i : ℕ))) <
  (↑pb.dim : WithBot ℕ)
Tactic: rw [degree_X_pow]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : A[X]) → S) p : S) (0 : S)
⊢ pb.dim ≤ p.natDegree
have refine : ∀ (hlt : p.natDegree < pb.dim), p = 0
Tactic: refine le_of_not_gt fun hlt => ne_zero ?_
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : A[X]) → S) p : S) (0 : S)
hlt : p.natDegree < pb.dim
⊢ p = 0
have rw : Eq.{u_4 + 1} (α := A[X]) (∑ i : Fin pb.dim, (monomial (↑i : ℕ) : (a : A) → A[X]) (p.coeff (↑i : ℕ))) 0
Tactic: rw [p.as_sum_range' _ hlt, Finset.sum_range]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : A[X]) → S) p : S) (0 : S)
hlt : p.natDegree < pb.dim
⊢ Eq.{u_4 + 1} (α := A[X]) (∑ i : Fin pb.dim, (monomial (↑i : ℕ) : (a : A) → A[X]) (p.coeff (↑i : ℕ))) 0
have refine : ∀ (i : Fin pb.dim), Eq (α := A[X]) ((monomial (↑i : ℕ) : (a : A) → A[X]) (p.coeff (↑i : ℕ)) : A[X]) (0 : A[X])
Tactic: refine Fintype.sum_eq_zero _ fun i => ?_
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (hypothesis)
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : A[X]) → S) p : S) (0 : S)
hlt : p.natDegree < pb.dim
i : Fin pb.dim
⊢ Eq (α := A[X]) ((monomial (↑i : ℕ) : (a : A) → A[X]) (p.coeff (↑i : ℕ)) : A[X]) (0 : A[X])
have root₁ : Eq.{u_2 + 1} (α := S)
  (∑ x : Fin pb.dim, HSMul.hSMul (β := S) (p.coeff (↑x : ℕ)) ((pb.basis : (a : Fin pb.dim) → S) x : S)) 0
Tactic: simp_rw [aeval_eq_sum_range' hlt, Finset.sum_range, ← pb.basis_eq_pow] at root
Cleared hypotheses: root
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (hypothesis)
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
hlt : p.natDegree < pb.dim
i : Fin pb.dim
root :
  Eq.{u_2 + 1} (α := S)
    (∑ x : Fin pb.dim, HSMul.hSMul (β := S) (p.coeff (↑x : ℕ)) ((pb.basis : (a : Fin pb.dim) → S) x : S)) 0
⊢ Eq (α := A[X]) ((monomial (↑i : ℕ) : (a : A) → A[X]) (p.coeff (↑i : ℕ)) : A[X]) (0 : A[X])
have this : ∀ (i : Fin pb.dim), p.coeff (↑i : ℕ) = 0
Tactic: have := Fintype.linearIndependent_iff.1 pb.basis.linearIndependent _ root
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
hlt : p.natDegree < pb.dim
i : Fin pb.dim
root :
  Eq.{u_2 + 1} (α := S)
    (∑ x : Fin pb.dim, HSMul.hSMul (β := S) (p.coeff (↑x : ℕ)) ((pb.basis : (a : Fin pb.dim) → S) x : S)) 0
this : ∀ (i : Fin pb.dim), p.coeff (↑i : ℕ) = 0
⊢ Eq (α := A[X]) ((monomial (↑i : ℕ) : (a : A) → A[X]) (p.coeff (↑i : ℕ)) : A[X]) (0 : A[X])
have rw : Eq.{u_4 + 1} (α := A[X]) ((monomial (↑i : ℕ) : (a : A) → A[X]) 0) 0
Tactic: rw [this, monomial_zero_right]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
hlt : p.natDegree < pb.dim
i : Fin pb.dim
root :
  Eq.{u_2 + 1} (α := S)
    (∑ x : Fin pb.dim, HSMul.hSMul (β := S) (p.coeff (↑x : ℕ)) ((pb.basis : (a : Fin pb.dim) → S) x : S)) 0
this : ∀ (i : Fin pb.dim), p.coeff (↑i : ℕ) = 0
rw : Eq.{u_4 + 1} (α := A[X]) ((monomial (↑i : ℕ) : (a : A) → A[X]) 0) 0
⊢ Eq (α := A[X]) ((monomial (↑i : ℕ) : (a : A) → A[X]) (p.coeff (↑i : ℕ)) : A[X]) (0 : A[X])
have rw₁ : Eq.{u_4 + 1} (α := A[X]) 0 0
Tactic: rw [this, monomial_zero_right]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
h : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : Eq.{u_2 + 1} (α := S) ((aeval h.gen : (a : A[X]) → S) p : S) (0 : S)
⊢ (↑h.dim : WithBot ℕ) ≤ p.degree
have rw : LE.le (α := WithBot ℕ) (↑h.dim : WithBot ℕ) (↑p.natDegree : WithBot ℕ)
Tactic: rw [degree_eq_natDegree ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
inst_3 : Nontrivial A
pb : PowerBasis A S
⊢ (HPow.hPow (α := A[X]) X pb.dim -
        ∑ i : Fin pb.dim,
          HMul.hMul (α := A[X])
            ((C : (a : A) → A[X])
                ((((pb.basis.repr : (a : S) → Fin pb.dim →₀ A) (pb.gen ^ pb.dim) : Fin pb.dim →₀ A) :
                    (a : Fin pb.dim) → A)
                  i) :
              A[X])
            (HPow.hPow (α := A[X]) X (↑i : ℕ))).degree =
    (↑pb.dim : WithBot ℕ)
have rw : (HPow.hPow (α := A[X]) X pb.dim).degree = (↑pb.dim : WithBot ℕ)
Tactic: rw [degree_sub_eq_left_of_degree_lt]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
inst_3 : Nontrivial A
pb : PowerBasis A S
rw : (HPow.hPow (α := A[X]) X pb.dim).degree = (↑pb.dim : WithBot ℕ)
⊢ (HPow.hPow (α := A[X]) X pb.dim -
        ∑ i : Fin pb.dim,
          HMul.hMul (α := A[X])
            ((C : (a : A) → A[X])
                ((((pb.basis.repr : (a : S) → Fin pb.dim →₀ A) (pb.gen ^ pb.dim) : Fin pb.dim →₀ A) :
                    (a : Fin pb.dim) → A)
                  i) :
              A[X])
            (HPow.hPow (α := A[X]) X (↑i : ℕ))).degree =
    (↑pb.dim : WithBot ℕ)
have rw₁ : degree.{u_4} (R := A)
    (∑ i : Fin pb.dim,
      HMul.hMul (α := A[X])
        ((C : (a : A) → A[X])
            ((((pb.basis.repr : (a : S) → Fin pb.dim →₀ A) (pb.gen ^ pb.dim) : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
              i) :
          A[X])
        (HPow.hPow (α := A[X]) X (↑i : ℕ))) <
  (HPow.hPow (α := A[X]) X pb.dim).degree
Tactic: rw [degree_sub_eq_left_of_degree_lt]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
inst_3 : Nontrivial A
pb : PowerBasis A S
⊢ (HPow.hPow (α := A[X]) X pb.dim).degree = (↑pb.dim : WithBot ℕ)
have rw : Eq (α := WithBot ℕ) (↑pb.dim : WithBot ℕ) (↑pb.dim : WithBot ℕ)
Tactic: rw [degree_X_pow]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
inst_3 : Nontrivial A
pb : PowerBasis A S
⊢ degree.{u_4} (R := A)
      (∑ i : Fin pb.dim,
        HMul.hMul (α := A[X])
          ((C : (a : A) → A[X])
              ((((pb.basis.repr : (a : S) → Fin pb.dim →₀ A) (pb.gen ^ pb.dim) : Fin pb.dim →₀ A) :
                  (a : Fin pb.dim) → A)
                i) :
            A[X])
          (HPow.hPow (α := A[X]) X (↑i : ℕ))) <
    (HPow.hPow (α := A[X]) X pb.dim).degree
have rw : degree.{u_4} (R := A)
    (∑ i : Fin pb.dim,
      HMul.hMul (α := A[X])
        ((C : (a : A) → A[X])
            ((((pb.basis.repr : (a : S) → Fin pb.dim →₀ A) (pb.gen ^ pb.dim) : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
              i) :
          A[X])
        (HPow.hPow (α := A[X]) X (↑i : ℕ))) <
  (↑pb.dim : WithBot ℕ)
Tactic: rw [degree_X_pow]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (hypothesis)
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
pb : PowerBasis A S
⊢ pb.minpolyGen = minpoly A pb.gen
have a : Nontrivial A
Tactic: nontriviality A
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
pb : PowerBasis A S
h : Nontrivial A
⊢ pb.minpolyGen = minpoly A pb.gen
have refine : ∀ (q : A[X]) (hq : q.degree < pb.minpolyGen.degree) (hn0 : ¬q = 0)
  (h0 : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : A[X]) → S) q : S) (0 : S)), False
Tactic: refine minpoly.unique' A _ pb.minpolyGen_monic pb.aeval_minpolyGen fun q hq =>
    or_iff_not_imp_left.2 fun hn0 h0 => ?_
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
inst_3 : Nontrivial A
pb : PowerBasis A S
⊢ degree (minpoly A pb.gen) = (↑pb.dim : WithBot ℕ)
have rw : pb.minpolyGen.degree = (↑pb.dim : WithBot ℕ)
Tactic: rw [← minpolyGen_eq, degree_minpolyGen]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
inst_3 : Nontrivial A
pb : PowerBasis A S
rw : pb.minpolyGen.degree = (↑pb.dim : WithBot ℕ)
⊢ degree (minpoly A pb.gen) = (↑pb.dim : WithBot ℕ)
have rw₁ : Eq (α := WithBot ℕ) (↑pb.dim : WithBot ℕ) (↑pb.dim : WithBot ℕ)
Tactic: rw [← minpolyGen_eq, degree_minpolyGen]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
inst_3 : Nontrivial A
pb : PowerBasis A S
⊢ natDegree (minpoly A pb.gen) = pb.dim
have rw : pb.minpolyGen.natDegree = pb.dim
Tactic: rw [← minpolyGen_eq, natDegree_minpolyGen]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
inst_3 : Nontrivial A
pb : PowerBasis A S
rw : pb.minpolyGen.natDegree = pb.dim
⊢ natDegree (minpoly A pb.gen) = pb.dim
have rw₁ : pb.dim = pb.dim
Tactic: rw [← minpolyGen_eq, natDegree_minpolyGen]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
pb : PowerBasis A S
⊢ Eq (α := Matrix (Fin pb.dim) (Fin pb.dim) A)
    (((Algebra.leftMulMatrix pb.basis : S →ₐ[A] Matrix (Fin pb.dim) (Fin pb.dim) A) :
          (a : S) → Matrix (Fin pb.dim) (Fin pb.dim) A)
        pb.gen :
      Matrix (Fin pb.dim) (Fin pb.dim) A)
    ((Matrix.of : (a : Fin pb.dim → Fin pb.dim → A) → Matrix (Fin pb.dim) (Fin pb.dim) A) fun (i j : Fin pb.dim) ↦
        if (↑j : ℕ) + 1 = pb.dim then -pb.minpolyGen.coeff (↑i : ℕ) else if (↑i : ℕ) = (↑j : ℕ) + 1 then 1 else 0 :
      Matrix (Fin pb.dim) (Fin pb.dim) A)
have inl : Subsingleton A →
  Eq (α := Matrix (Fin pb.dim) (Fin pb.dim) A)
    (((Algebra.leftMulMatrix pb.basis : S →ₐ[A] Matrix (Fin pb.dim) (Fin pb.dim) A) :
          (a : S) → Matrix (Fin pb.dim) (Fin pb.dim) A)
        pb.gen :
      Matrix (Fin pb.dim) (Fin pb.dim) A)
    ((Matrix.of : (a : Fin pb.dim → Fin pb.dim → A) → Matrix (Fin pb.dim) (Fin pb.dim) A) fun (i j : Fin pb.dim) ↦
        if (↑j : ℕ) + 1 = pb.dim then -pb.minpolyGen.coeff (↑i : ℕ) else if (↑i : ℕ) = (↑j : ℕ) + 1 then 1 else 0 :
      Matrix (Fin pb.dim) (Fin pb.dim) A)
Tactic: cases subsingleton_or_nontrivial A
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
pb : PowerBasis A S
inl :
  Subsingleton A →
    Eq (α := Matrix (Fin pb.dim) (Fin pb.dim) A)
      (((Algebra.leftMulMatrix pb.basis : S →ₐ[A] Matrix (Fin pb.dim) (Fin pb.dim) A) :
            (a : S) → Matrix (Fin pb.dim) (Fin pb.dim) A)
          pb.gen :
        Matrix (Fin pb.dim) (Fin pb.dim) A)
      ((Matrix.of : (a : Fin pb.dim → Fin pb.dim → A) → Matrix (Fin pb.dim) (Fin pb.dim) A) fun (i j : Fin pb.dim) ↦
          if (↑j : ℕ) + 1 = pb.dim then -pb.minpolyGen.coeff (↑i : ℕ) else if (↑i : ℕ) = (↑j : ℕ) + 1 then 1 else 0 :
        Matrix (Fin pb.dim) (Fin pb.dim) A)
⊢ Eq (α := Matrix (Fin pb.dim) (Fin pb.dim) A)
    (((Algebra.leftMulMatrix pb.basis : S →ₐ[A] Matrix (Fin pb.dim) (Fin pb.dim) A) :
          (a : S) → Matrix (Fin pb.dim) (Fin pb.dim) A)
        pb.gen :
      Matrix (Fin pb.dim) (Fin pb.dim) A)
    ((Matrix.of : (a : Fin pb.dim → Fin pb.dim → A) → Matrix (Fin pb.dim) (Fin pb.dim) A) fun (i j : Fin pb.dim) ↦
        if (↑j : ℕ) + 1 = pb.dim then -pb.minpolyGen.coeff (↑i : ℕ) else if (↑i : ℕ) = (↑j : ℕ) + 1 then 1 else 0 :
      Matrix (Fin pb.dim) (Fin pb.dim) A)
have inr : Nontrivial A →
  Eq (α := Matrix (Fin pb.dim) (Fin pb.dim) A)
    (((Algebra.leftMulMatrix pb.basis : S →ₐ[A] Matrix (Fin pb.dim) (Fin pb.dim) A) :
          (a : S) → Matrix (Fin pb.dim) (Fin pb.dim) A)
        pb.gen :
      Matrix (Fin pb.dim) (Fin pb.dim) A)
    ((Matrix.of : (a : Fin pb.dim → Fin pb.dim → A) → Matrix (Fin pb.dim) (Fin pb.dim) A) fun (i j : Fin pb.dim) ↦
        if (↑j : ℕ) + 1 = pb.dim then -pb.minpolyGen.coeff (↑i : ℕ) else if (↑i : ℕ) = (↑j : ℕ) + 1 then 1 else 0 :
      Matrix (Fin pb.dim) (Fin pb.dim) A)
Tactic: cases subsingleton_or_nontrivial A
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
pb : PowerBasis A S
h : Nontrivial A
⊢ Eq (α := Matrix (Fin pb.dim) (Fin pb.dim) A)
    (((Algebra.leftMulMatrix pb.basis : S →ₐ[A] Matrix (Fin pb.dim) (Fin pb.dim) A) :
          (a : S) → Matrix (Fin pb.dim) (Fin pb.dim) A)
        pb.gen :
      Matrix (Fin pb.dim) (Fin pb.dim) A)
    ((Matrix.of : (a : Fin pb.dim → Fin pb.dim → A) → Matrix (Fin pb.dim) (Fin pb.dim) A) fun (i j : Fin pb.dim) ↦
        if (↑j : ℕ) + 1 = pb.dim then -pb.minpolyGen.coeff (↑i : ℕ) else if (↑i : ℕ) = (↑j : ℕ) + 1 then 1 else 0 :
      Matrix (Fin pb.dim) (Fin pb.dim) A)
have inr : Eq (α := S →ₗ[A] S) ((Algebra.lmul A S : (a : S) → End A S) pb.gen : End A S)
  ((Matrix.toLin pb.basis pb.basis : (a : Matrix (Fin pb.dim) (Fin pb.dim) A) → S →ₗ[A] S)
      ((Matrix.of : (a : Fin pb.dim → Fin pb.dim → A) → Matrix (Fin pb.dim) (Fin pb.dim) A) fun (i j : Fin pb.dim) ↦
        if (↑j : ℕ) + 1 = pb.dim then -pb.minpolyGen.coeff (↑i : ℕ) else if (↑i : ℕ) = (↑j : ℕ) + 1 then 1 else 0) :
    S →ₗ[A] S)
Tactic: rw [Algebra.leftMulMatrix_apply, ← LinearEquiv.eq_symm_apply, LinearMap.toMatrix_symm]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
pb : PowerBasis A S
h : Nontrivial A
⊢ Eq (α := S →ₗ[A] S) ((Algebra.lmul A S : (a : S) → End A S) pb.gen : End A S)
    ((Matrix.toLin pb.basis pb.basis : (a : Matrix (Fin pb.dim) (Fin pb.dim) A) → S →ₗ[A] S)
        ((Matrix.of : (a : Fin pb.dim → Fin pb.dim → A) → Matrix (Fin pb.dim) (Fin pb.dim) A) fun (i j : Fin pb.dim) ↦
          if (↑j : ℕ) + 1 = pb.dim then -pb.minpolyGen.coeff (↑i : ℕ) else if (↑i : ℕ) = (↑j : ℕ) + 1 then 1 else 0) :
      S →ₗ[A] S)
have inr : ∀ (k : Fin pb.dim),
  Eq (α := S)
    ((((Algebra.lmul A S : (a : S) → End A S) pb.gen : End A S) : (a : S) → S)
        ((pb.basis : (a : Fin pb.dim) → S) k : S) :
      S)
    ((((Matrix.toLin pb.basis pb.basis : (a : Matrix (Fin pb.dim) (Fin pb.dim) A) → S →ₗ[A] S)
              ((Matrix.of : (a : Fin pb.dim → Fin pb.dim → A) → Matrix (Fin pb.dim) (Fin pb.dim) A)
                fun (i j : Fin pb.dim) ↦
                if (↑j : ℕ) + 1 = pb.dim then -pb.minpolyGen.coeff (↑i : ℕ)
                else if (↑i : ℕ) = (↑j : ℕ) + 1 then 1 else 0) :
            S →ₗ[A] S) :
          (a : S) → S)
        ((pb.basis : (a : Fin pb.dim) → S) k : S) :
      S)
Tactic: refine pb.basis.ext fun k => ?_
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
pb : PowerBasis A S
h : Nontrivial A
k : Fin pb.dim
⊢ Eq (α := S)
    ((((Algebra.lmul A S : (a : S) → End A S) pb.gen : End A S) : (a : S) → S)
        ((pb.basis : (a : Fin pb.dim) → S) k : S) :
      S)
    ((((Matrix.toLin pb.basis pb.basis : (a : Matrix (Fin pb.dim) (Fin pb.dim) A) → S →ₗ[A] S)
              ((Matrix.of : (a : Fin pb.dim → Fin pb.dim → A) → Matrix (Fin pb.dim) (Fin pb.dim) A)
                fun (i j : Fin pb.dim) ↦
                if (↑j : ℕ) + 1 = pb.dim then -pb.minpolyGen.coeff (↑i : ℕ)
                else if (↑i : ℕ) = (↑j : ℕ) + 1 then 1 else 0) :
            S →ₗ[A] S) :
          (a : S) → S)
        ((pb.basis : (a : Fin pb.dim) → S) k : S) :
      S)
have inr : Eq (α := S) ((((Algebra.lmul A S : (a : S) → End A S) pb.gen : End A S) : (a : S) → S) (pb.gen ^ (↑k : ℕ)) : S)
  (∑ x : Fin pb.dim,
      (if (↑k : ℕ) + 1 = pb.dim then -pb.minpolyGen.coeff (↑x : ℕ) else if (↑x : ℕ) = (↑k : ℕ) + 1 then 1 else 0) •
        pb.gen ^ (↑x : ℕ) :
    S)
Tactic: simp_rw [Matrix.toLin_self, Matrix.of_apply, pb.basis_eq_pow]