awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerBasis
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
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)
⊢ 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:
refine sub_eq_zero.mpr ((pb.basis.linearCombination_repr (pb.gen ^ pb.dim)).symm.trans ?_)

Premises used: Iff.mpr, PowerBasis.dim, sub_eq_zero, PowerBasis.gen, PowerBasis.basis, HPow.hPow, Module.Basis.linearCombination_repr, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.PowerBasis
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 : ℕ)))
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
⊢ 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:
rw [Finsupp.linearCombination_apply, Finsupp.sum_fintype]

Premises used: Finsupp.sum_fintype, Finsupp.linearCombination_apply
-- Module: Mathlib.RingTheory.PowerBasis
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)
    (∑ 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:
simp only [pb.coe_basis, zero_smul, imp_true_iff]

Premises used: PowerBasis.coe_basis, imp_true_iff, zero_smul
-- Module: Mathlib.RingTheory.PowerBasis
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
⊢ ∀ (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:
simp only [pb.coe_basis, zero_smul, imp_true_iff]

Premises used: PowerBasis.coe_basis, imp_true_iff, zero_smul
-- Module: Mathlib.RingTheory.PowerBasis
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
⊢ Nontrivial A

Tactic:
nontriviality A
-- Module: Mathlib.RingTheory.PowerBasis
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
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
⊢ pb.minpolyGen.Monic

Tactic:
apply (monic_X_pow _).sub_of_left _

Premises used: Polynomial.monic_X_pow, Polynomial.Monic.sub_of_left
-- Module: Mathlib.RingTheory.PowerBasis
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
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 ℕ)
⊢ 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_X_pow]

Premises used: Polynomial.degree_X_pow
-- Module: Mathlib.RingTheory.PowerBasis
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 : ℕ))) <
    (↑pb.dim : WithBot ℕ)

Tactic:
degree_sum_fin_lt _

Premises used: Polynomial.degree_sum_fin_lt
-- Module: Mathlib.RingTheory.PowerBasis
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 : ℕ))) <
    (↑pb.dim : WithBot ℕ)

Tactic:
exact degree_sum_fin_lt _

Premises used: Polynomial.degree_sum_fin_lt
-- Module: Mathlib.RingTheory.PowerBasis
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

Tactic:
le_of_not_gt fun hlt => ne_zero ?_

Premises used: le_of_not_gt
-- Module: Mathlib.RingTheory.PowerBasis
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)
refine : ∀ (hlt : p.natDegree < pb.dim), p = 0
⊢ pb.dim ≤ p.natDegree

Tactic:
refine le_of_not_gt fun hlt => ne_zero ?_

Premises used: le_of_not_gt
-- Module: Mathlib.RingTheory.PowerBasis
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
rw : Eq.{u_4 + 1} (α := A[X]) (∑ i : Fin pb.dim, (monomial (↑i : ℕ) : (a : A) → A[X]) (p.coeff (↑i : ℕ))) 0
⊢ p = 0

Tactic:
rw [p.as_sum_range' _ hlt, Finset.sum_range]

Premises used: Finset.sum_range, Polynomial.as_sum_range'
-- Module: Mathlib.RingTheory.PowerBasis
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

Tactic:
Fintype.sum_eq_zero _ fun i => ?_

Premises used: Fintype.sum_eq_zero
-- Module: Mathlib.RingTheory.PowerBasis
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
refine : ∀ (i : Fin pb.dim), Eq (α := A[X]) ((monomial (↑i : ℕ) : (a : A) → A[X]) (p.coeff (↑i : ℕ)) : A[X]) (0 : A[X])
⊢ Eq.{u_4 + 1} (α := A[X]) (∑ i : Fin pb.dim, (monomial (↑i : ℕ) : (a : A) → A[X]) (p.coeff (↑i : ℕ))) 0

Tactic:
refine Fintype.sum_eq_zero _ fun i => ?_

Premises used: Fintype.sum_eq_zero
-- Module: Mathlib.RingTheory.PowerBasis
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.{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

Premises used: PowerBasis.basis_eq_pow, Finset.sum_range, Polynomial.aeval_eq_sum_range'
-- Module: Mathlib.RingTheory.PowerBasis
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
⊢ ∀ (i : Fin pb.dim), p.coeff (↑i : ℕ) = 0

Tactic:
have := Fintype.linearIndependent_iff.1 pb.basis.linearIndependent _ root
-- Module: Mathlib.RingTheory.PowerBasis
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
rw₁ rw₂ : Eq.{u_4 + 1} (α := A[X]) 0 0
⊢ Eq (α := A[X]) ((monomial (↑i : ℕ) : (a : A) → A[X]) (p.coeff (↑i : ℕ)) : A[X]) (0 : A[X])

Tactic:
rw [this, monomial_zero_right]

Premises used: Polynomial.monomial_zero_right
-- Module: Mathlib.RingTheory.PowerBasis
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)
rw : LE.le (α := WithBot ℕ) (↑h.dim : WithBot ℕ) (↑p.natDegree : WithBot ℕ)
⊢ (↑h.dim : WithBot ℕ) ≤ p.degree

Tactic:
rw [degree_eq_natDegree ne_zero]

Premises used: Polynomial.degree_eq_natDegree
-- Module: Mathlib.RingTheory.PowerBasis
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)
⊢ LE.le (α := WithBot ℕ) (↑h.dim : WithBot ℕ) (↑p.natDegree : WithBot ℕ)

Tactic:
WithBot.coe_le_coe.2 (h.dim_le_natDegree_of_root ne_zero root)

Premises used: Iff.mpr, WithBot.coe_le_coe, PowerBasis.dim_le_natDegree_of_root
-- Module: Mathlib.RingTheory.PowerBasis
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)
⊢ LE.le (α := WithBot ℕ) (↑h.dim : WithBot ℕ) (↑p.natDegree : WithBot ℕ)

Tactic:
exact WithBot.coe_le_coe.2 (h.dim_le_natDegree_of_root ne_zero root)

Premises used: Iff.mpr, WithBot.coe_le_coe, PowerBasis.dim_le_natDegree_of_root
-- Module: Mathlib.RingTheory.PowerBasis
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 ℕ)
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
⊢ (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 ℕ)

Tactic:
rw [degree_sub_eq_left_of_degree_lt]

Premises used: Polynomial.degree_sub_eq_left_of_degree_lt
-- Module: Mathlib.RingTheory.PowerBasis
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 rw₁ : Eq (α := WithBot ℕ) (↑pb.dim : WithBot ℕ) (↑pb.dim : WithBot ℕ)
⊢ (HPow.hPow (α := A[X]) X pb.dim).degree = (↑pb.dim : WithBot ℕ)

Tactic:
rw [degree_X_pow]

Premises used: Polynomial.degree_X_pow
-- Module: Mathlib.RingTheory.PowerBasis
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 :
  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 ℕ)
⊢ 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_X_pow]

Premises used: Polynomial.degree_X_pow
-- Module: Mathlib.RingTheory.PowerBasis
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 : ℕ))) <
    (↑pb.dim : WithBot ℕ)

Tactic:
apply degree_sum_fin_lt

Premises used: Polynomial.degree_sum_fin_lt
-- Module: Mathlib.RingTheory.PowerBasis
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
⊢ pb.minpolyGen.natDegree = pb.dim

Tactic:
natDegree_eq_of_degree_eq_some pb.degree_minpolyGen

Premises used: Polynomial.natDegree_eq_of_degree_eq_some, PowerBasis.degree_minpolyGen
-- Module: Mathlib.RingTheory.PowerBasis
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

Tactic:
minpoly.unique' A _ pb.minpolyGen_monic pb.aeval_minpolyGen fun q hq =>
    or_iff_not_imp_left.2 fun hn0 h0 => ?_

Premises used: Iff.mpr, PowerBasis.minpolyGen_monic, Classical.or_iff_not_imp_left, PowerBasis.aeval_minpolyGen, minpoly.unique'
-- Module: Mathlib.RingTheory.PowerBasis
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
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
⊢ pb.minpolyGen = minpoly A pb.gen

Tactic:
refine minpoly.unique' A _ pb.minpolyGen_monic pb.aeval_minpolyGen fun q hq =>
    or_iff_not_imp_left.2 fun hn0 h0 => ?_

Premises used: Iff.mpr, PowerBasis.minpolyGen_monic, Classical.or_iff_not_imp_left, PowerBasis.aeval_minpolyGen, minpoly.unique'
-- Module: Mathlib.RingTheory.PowerBasis
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
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:
(pb.dim_le_degree_of_root hn0 h0).not_gt (pb.degree_minpolyGen ▸ hq)

Premises used: Eq.rec, LE.le.not_gt, PowerBasis.degree_minpolyGen, PowerBasis.dim_le_degree_of_root
-- Module: Mathlib.RingTheory.PowerBasis
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
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:
exact (pb.dim_le_degree_of_root hn0 h0).not_gt (pb.degree_minpolyGen ▸ hq)

Premises used: Eq.rec, LE.le.not_gt, PowerBasis.degree_minpolyGen, PowerBasis.dim_le_degree_of_root
-- Module: Mathlib.RingTheory.PowerBasis
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
⊢ IsIntegral A pb.gen

Tactic:
⟨minpolyGen pb, minpolyGen_monic pb, aeval_minpolyGen pb⟩

Premises used: PowerBasis.minpolyGen_monic, PowerBasis.minpolyGen, RingHom.IsIntegralElem, IsIntegral, And.intro, Exists.intro, PowerBasis.aeval_minpolyGen
-- Module: Mathlib.RingTheory.PowerBasis
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 ℕ)
rw₁ rw₂ : Eq (α := WithBot ℕ) (↑pb.dim : WithBot ℕ) (↑pb.dim : WithBot ℕ)
⊢ degree (minpoly A pb.gen) = (↑pb.dim : WithBot ℕ)

Tactic:
rw [← minpolyGen_eq, degree_minpolyGen]

Premises used: PowerBasis.minpolyGen_eq, PowerBasis.degree_minpolyGen
-- Module: Mathlib.RingTheory.PowerBasis
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
rw₁ rw₂ : pb.dim = pb.dim
⊢ natDegree (minpoly A pb.gen) = pb.dim

Tactic:
rw [← minpolyGen_eq, natDegree_minpolyGen]

Premises used: PowerBasis.natDegree_minpolyGen, PowerBasis.minpolyGen_eq
-- Module: Mathlib.RingTheory.PowerBasis
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)
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)
⊢ 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

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.PowerBasis
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 : 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:
subsingleton
-- Module: Mathlib.RingTheory.PowerBasis
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
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)
⊢ 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:
rw [Algebra.leftMulMatrix_apply, ← LinearEquiv.eq_symm_apply, LinearMap.toMatrix_symm]

Premises used: LinearMap.toMatrix_symm, LinearEquiv.eq_symm_apply, Algebra.leftMulMatrix_apply
-- Module: Mathlib.RingTheory.PowerBasis
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)

Tactic:
pb.basis.ext fun k => ?_

Premises used: PowerBasis.basis, Module.Basis.ext