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
h : Nontrivial A
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)
⊢ 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:
refine pb.basis.ext fun k => ?_

Premises used: PowerBasis.basis, Module.Basis.ext
-- 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
k : Fin pb.dim
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)
⊢ 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:
simp_rw [Matrix.toLin_self, Matrix.of_apply, pb.basis_eq_pow]

Premises used: Matrix.toLin_self, Matrix.of_apply, PowerBasis.basis_eq_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
k : Fin pb.dim
inr :
  pb.gen ^ ((↑k : ℕ) + 1) =
    ∑ 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 : ℕ)
⊢ 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:
apply (pow_succ' _ _).symm.trans

Premises used: Eq.symm, pow_succ', 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
h : Nontrivial A
k : Fin pb.dim
pos :
  ∀ (h : (↑k : ℕ) + 1 = pb.dim),
    pb.gen ^ ((↑k : ℕ) + 1) = ∑ x : Fin pb.dim, -pb.minpolyGen.coeff (↑x : ℕ) • pb.gen ^ (↑x : ℕ)
neg :
  ∀ (h : ¬(↑k : ℕ) + 1 = pb.dim),
    pb.gen ^ ((↑k : ℕ) + 1) =
      ∑ x : Fin pb.dim,
        HSMul.hSMul.{u_4, u_2, u_2} (α := A) (if (↑x : ℕ) = (↑k : ℕ) + 1 then 1 else 0) (pb.gen ^ (↑x : ℕ))
⊢ pb.gen ^ ((↑k : ℕ) + 1) =
    ∑ 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 : ℕ)

Tactic:
split_ifs with h
-- 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_1 : Nontrivial A
k : Fin pb.dim
h : (↑k : ℕ) + 1 = pb.dim
pos : pb.gen ^ pb.dim + ∑ x : Fin pb.dim, pb.minpolyGen.coeff (↑x : ℕ) • pb.gen ^ (↑x : ℕ) = 0
⊢ pb.gen ^ ((↑k : ℕ) + 1) = ∑ x : Fin pb.dim, -pb.minpolyGen.coeff (↑x : ℕ) • pb.gen ^ (↑x : ℕ)

Tactic:
simp_rw [h, neg_smul, Finset.sum_neg_distrib, eq_neg_iff_add_eq_zero]

Premises used: neg_smul, eq_neg_iff_add_eq_zero, Finset.sum_neg_distrib
-- 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_1 : Nontrivial A
k : Fin pb.dim
h : (↑k : ℕ) + 1 = pb.dim
⊢ Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : A[X]) → S) pb.minpolyGen : S) (0 : S)

Tactic:
pb.aeval_minpolyGen

Premises used: 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
pb : PowerBasis A S
h_1 : Nontrivial A
k : Fin pb.dim
h : (↑k : ℕ) + 1 = pb.dim
h₁ :
  pb.gen ^ pb.dim + ∑ x : Fin pb.dim, pb.minpolyGen.coeff (↑x : ℕ) • pb.gen ^ (↑x : ℕ) =
    (aeval pb.gen : (a : A[X]) → S) pb.minpolyGen
⊢ pb.gen ^ pb.dim + ∑ x : Fin pb.dim, pb.minpolyGen.coeff (↑x : ℕ) • pb.gen ^ (↑x : ℕ) = 0

Tactic:
convert! pb.aeval_minpolyGen

Premises used: 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
pb : PowerBasis A S
h_1 : Nontrivial A
k : Fin pb.dim
h : (↑k : ℕ) + 1 = pb.dim
h₁ :
  ∑ x : Fin pb.dim, pb.minpolyGen.coeff (↑x : ℕ) • pb.gen ^ (↑x : ℕ) + pb.gen ^ pb.dim =
    (aeval pb.gen : (a : A[X]) → S) pb.minpolyGen
h₂ :
  ∑ x : Fin pb.dim, pb.minpolyGen.coeff (↑x : ℕ) • pb.gen ^ (↑x : ℕ) + pb.gen ^ pb.dim =
    ∑ i ∈ Finset.range (pb.minpolyGen.natDegree + 1), pb.minpolyGen.coeff i • pb.gen ^ i
h₃ :
  ∑ x : Fin pb.dim, pb.minpolyGen.coeff (↑x : ℕ) • pb.gen ^ (↑x : ℕ) + pb.gen ^ pb.dim =
    ∑ x ∈ Finset.range pb.minpolyGen.natDegree, pb.minpolyGen.coeff x • pb.gen ^ x +
      pb.minpolyGen.coeff pb.minpolyGen.natDegree • pb.gen ^ pb.minpolyGen.natDegree
h₄ :
  ∑ x : Fin pb.dim, pb.minpolyGen.coeff (↑x : ℕ) • pb.gen ^ (↑x : ℕ) + pb.gen ^ pb.dim =
    ∑ x ∈ Finset.range pb.minpolyGen.natDegree, pb.minpolyGen.coeff x • pb.gen ^ x +
      pb.minpolyGen.leadingCoeff • pb.gen ^ pb.minpolyGen.natDegree
h₅ :
  ∑ x : Fin pb.dim, pb.minpolyGen.coeff (↑x : ℕ) • pb.gen ^ (↑x : ℕ) + pb.gen ^ pb.dim =
    ∑ x ∈ Finset.range pb.minpolyGen.natDegree, pb.minpolyGen.coeff x • pb.gen ^ x +
      HSMul.hSMul.{u_4, u_2, u_2} (α := A) 1 (pb.gen ^ pb.minpolyGen.natDegree)
h₆ :
  ∑ x : Fin pb.dim, pb.minpolyGen.coeff (↑x : ℕ) • pb.gen ^ (↑x : ℕ) + pb.gen ^ pb.dim =
    ∑ x ∈ Finset.range pb.minpolyGen.natDegree, pb.minpolyGen.coeff x • pb.gen ^ x + pb.gen ^ pb.minpolyGen.natDegree
h₇ :
  ∑ x : Fin pb.dim, pb.minpolyGen.coeff (↑x : ℕ) • pb.gen ^ (↑x : ℕ) + pb.gen ^ pb.dim =
    ∑ x ∈ Finset.range pb.dim, pb.minpolyGen.coeff x • pb.gen ^ x + pb.gen ^ pb.dim
h₈ h₉ :
  ∑ x : Fin pb.dim, pb.minpolyGen.coeff (↑x : ℕ) • pb.gen ^ (↑x : ℕ) + pb.gen ^ pb.dim =
    ∑ i : Fin pb.dim, pb.minpolyGen.coeff (↑i : ℕ) • pb.gen ^ (↑i : ℕ) + pb.gen ^ pb.dim
⊢ pb.gen ^ pb.dim + ∑ x : Fin pb.dim, pb.minpolyGen.coeff (↑x : ℕ) • pb.gen ^ (↑x : ℕ) =
    (aeval pb.gen : (a : A[X]) → S) pb.minpolyGen

Tactic:
rw [add_comm, aeval_eq_sum_range, Finset.sum_range_succ, ← leadingCoeff,
      pb.minpolyGen_monic.leadingCoeff, one_smul, natDegree_minpolyGen, Finset.sum_range]

Premises used: PowerBasis.minpolyGen_monic, PowerBasis.natDegree_minpolyGen, Polynomial.leadingCoeff, add_comm, one_smul, Finset.sum_range, Polynomial.aeval_eq_sum_range, Polynomial.Monic.leadingCoeff, Finset.sum_range_succ
-- 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_1 : Nontrivial A
k : Fin pb.dim
h : ¬(↑k : ℕ) + 1 = pb.dim
neg : (↑(⟨(↑k : ℕ) + 1, ⋯⟩ : Fin pb.dim) : ℕ) = (↑k : ℕ) + 1
neg₁ :
  ∀ (x : Fin pb.dim),
    x ≠ ⟨(↑k : ℕ) + 1, ⋯⟩ →
      HSMul.hSMul.{u_4, u_2, u_2} (α := A) (if (↑x : ℕ) = (↑k : ℕ) + 1 then 1 else 0) (pb.gen ^ (↑x : ℕ)) = 0
⊢ pb.gen ^ ((↑k : ℕ) + 1) =
    ∑ x : Fin pb.dim,
      HSMul.hSMul.{u_4, u_2, u_2} (α := A) (if (↑x : ℕ) = (↑k : ℕ) + 1 then 1 else 0) (pb.gen ^ (↑x : ℕ))

Tactic:
rw [Fintype.sum_eq_single (⟨(k : ℕ) + 1, lt_of_le_of_ne k.2 h⟩ : Fin pb.dim), if_pos, one_smul]

Premises used: Fin.isLt, Fin.mk, if_pos, Fin.val, one_smul, HAdd.hAdd, OfNat.ofNat, lt_of_le_of_ne, Fintype.sum_eq_single
-- 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_1 : Nontrivial A
k : Fin pb.dim
h : ¬(↑k : ℕ) + 1 = pb.dim
⊢ (↑(⟨(↑k : ℕ) + 1, ⋯⟩ : Fin pb.dim) : ℕ) = (↑k : ℕ) + 1

Tactic:
rfl
-- 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_1 : Nontrivial A
k : Fin pb.dim
h : ¬(↑k : ℕ) + 1 = pb.dim
x : Fin pb.dim
hx : x ≠ ⟨(↑k : ℕ) + 1, ⋯⟩
neg : ¬(↑x : ℕ) = (↑k : ℕ) + 1
⊢ HSMul.hSMul.{u_4, u_2, u_2} (α := A) (if (↑x : ℕ) = (↑k : ℕ) + 1 then 1 else 0) (pb.gen ^ (↑x : ℕ)) = 0

Tactic:
rw [if_neg, zero_smul]

Premises used: zero_smul, if_neg
-- 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_1 : Nontrivial A
k : Fin pb.dim
h : ¬(↑k : ℕ) + 1 = pb.dim
x : Fin pb.dim
hx : x ≠ ⟨(↑k : ℕ) + 1, ⋯⟩
⊢ ¬(↑x : ℕ) = (↑k : ℕ) + 1

Tactic:
apply mt Fin.ext hx

Premises used: mt, Fin.ext
-- 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
S' : Type u_7
inst_3 : Ring S'
inst_4 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
f : A[X]
inl :
  Subsingleton A →
    Eq.{u_7 + 1} (α := S')
      (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
          ((aeval pb.gen : (a : A[X]) → S) f : S) :
        S')
      ((aeval y : (a : A[X]) → S') f : S')
inr :
  Nontrivial A →
    Eq.{u_7 + 1} (α := S')
      (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
          ((aeval pb.gen : (a : A[X]) → S) f : S) :
        S')
      ((aeval y : (a : A[X]) → S') f : S')
⊢ Eq.{u_7 + 1} (α := S')
    (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
        ((aeval pb.gen : (a : A[X]) → S) f : S) :
      S')
    ((aeval y : (a : A[X]) → S') f : S')

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
S' : Type u_7
inst_3 : Ring S'
inst_4 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
f : A[X]
h : Subsingleton A
inl :
  Eq.{u_7 + 1} (α := S')
    (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
        ((aeval pb.gen : (a : A[X]) → S) 0 : S) :
      S')
    ((aeval y : (a : A[X]) → S') 0 : S')
inl₁ :
  Eq.{u_7 + 1} (α := S')
    (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S') 0 :
      S')
    ((aeval y : (a : A[X]) → S') 0 : S')
inl₂ : Eq.{u_7 + 1} (α := S') (0 : S') ((aeval y : (a : A[X]) → S') 0 : S')
inl₃ inl₄ : Eq.{u_7 + 1} (α := S') 0 0
⊢ Eq.{u_7 + 1} (α := S')
    (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
        ((aeval pb.gen : (a : A[X]) → S) f : S) :
      S')
    ((aeval y : (a : A[X]) → S') f : S')

Tactic:
rw [(Subsingleton.elim _ _ : f = 0), aeval_zero, map_zero, aeval_zero]

Premises used: map_zero, Polynomial.aeval_zero, Subsingleton.elim
-- 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
S' : Type u_7
inst_3 : Ring S'
inst_4 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
f : A[X]
h : Nontrivial A
inr :
  Eq.{u_7 + 1} (α := S')
    (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
        ((aeval pb.gen : (a : A[X]) → S) (f %ₘ minpoly A pb.gen) : S) :
      S')
    ((aeval y : (a : A[X]) → S') (f %ₘ minpoly A pb.gen) : S')
⊢ Eq.{u_7 + 1} (α := S')
    (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
        ((aeval pb.gen : (a : A[X]) → S) f : S) :
      S')
    ((aeval y : (a : A[X]) → S') f : S')

Tactic:
rw [← aeval_modByMonic_eq_self_of_root (minpoly.aeval _ _), ← aeval_modByMonic_eq_self_of_root hy]

Premises used: Polynomial.aeval_modByMonic_eq_self_of_root, minpoly.aeval
-- 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
S' : Type u_7
inst_3 : Ring S'
inst_4 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
f : A[X]
h : Nontrivial A
pos :
  ∀ (hf : f %ₘ minpoly A pb.gen = 0),
    Eq.{u_7 + 1} (α := S')
      (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
          ((aeval pb.gen : (a : A[X]) → S) (f %ₘ minpoly A pb.gen) : S) :
        S')
      ((aeval y : (a : A[X]) → S') (f %ₘ minpoly A pb.gen) : S')
neg :
  ∀ (hf : ¬f %ₘ minpoly A pb.gen = 0),
    Eq.{u_7 + 1} (α := S')
      (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
          ((aeval pb.gen : (a : A[X]) → S) (f %ₘ minpoly A pb.gen) : S) :
        S')
      ((aeval y : (a : A[X]) → S') (f %ₘ minpoly A pb.gen) : S')
⊢ Eq.{u_7 + 1} (α := S')
    (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
        ((aeval pb.gen : (a : A[X]) → S) (f %ₘ minpoly A pb.gen) : S) :
      S')
    ((aeval y : (a : A[X]) → S') (f %ₘ minpoly A pb.gen) : S')

Tactic:
by_cases hf : f %ₘ minpoly A pb.gen = 0

Premises used: PowerBasis.gen, minpoly
-- 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
S' : Type u_7
inst_3 : Ring S'
inst_4 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
f : A[X]
h : Nontrivial A
hf : f %ₘ minpoly A pb.gen = 0
⊢ Eq.{u_7 + 1} (α := S')
    (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
        ((aeval pb.gen : (a : A[X]) → S) (f %ₘ minpoly A pb.gen) : S) :
      S')
    ((aeval y : (a : A[X]) → S') (f %ₘ minpoly A pb.gen) : S')

Tactic:
simp only [hf, map_zero]

Premises used: map_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
S' : Type u_7
inst_3 : Ring S'
inst_4 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
f : A[X]
h : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
rw : (f %ₘ minpoly A pb.gen).natDegree < natDegree (minpoly A pb.gen)
⊢ (f %ₘ minpoly A pb.gen).natDegree < pb.dim

Tactic:
rw [← pb.natDegree_minpoly]

Premises used: PowerBasis.natDegree_minpoly
-- 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
S' : Type u_7
inst_3 : Ring S'
inst_4 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
f : A[X]
h : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
apply : (f %ₘ minpoly A pb.gen).degree < degree (minpoly A pb.gen)
⊢ (f %ₘ minpoly A pb.gen).natDegree < natDegree (minpoly A pb.gen)

Tactic:
apply natDegree_lt_natDegree hf

Premises used: Polynomial.natDegree_lt_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
S' : Type u_7
inst_3 : Ring S'
inst_4 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
f : A[X]
h : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
⊢ (f %ₘ minpoly A pb.gen).degree < degree (minpoly A pb.gen)

Tactic:
degree_modByMonic_lt _ (minpoly.monic pb.isIntegral_gen)

Premises used: minpoly.monic, PowerBasis.isIntegral_gen, Polynomial.degree_modByMonic_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
S' : Type u_7
inst_3 : Ring S'
inst_4 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
f : A[X]
h : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
⊢ (f %ₘ minpoly A pb.gen).degree < degree (minpoly A pb.gen)

Tactic:
exact degree_modByMonic_lt _ (minpoly.monic pb.isIntegral_gen)

Premises used: minpoly.monic, PowerBasis.isIntegral_gen, Polynomial.degree_modByMonic_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
S' : Type u_7
inst_3 : Ring S'
inst_4 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
f : A[X]
h : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
⊢ (f %ₘ minpoly A pb.gen).natDegree < pb.dim

Tactic:
have : (f %ₘ minpoly A pb.gen).natDegree < pb.dim := by
    rw [← pb.natDegree_minpoly]
    apply natDegree_lt_natDegree hf
    exact degree_modByMonic_lt _ (minpoly.monic pb.isIntegral_gen)
-- 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
S' : Type u_7
inst_3 : Ring S'
inst_4 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
f : A[X]
h : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
this : (f %ₘ minpoly A pb.gen).natDegree < pb.dim
neg :
  Eq.{u_7 + 1} (α := S')
    (∑ x ∈ Finset.range pb.dim,
      ((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
        ((f %ₘ minpoly A pb.gen).coeff x • pb.gen ^ x))
    (∑ i ∈ Finset.range pb.dim, (f %ₘ minpoly A pb.gen).coeff i • y ^ i)
⊢ Eq.{u_7 + 1} (α := S')
    (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
        ((aeval pb.gen : (a : A[X]) → S) (f %ₘ minpoly A pb.gen) : S) :
      S')
    ((aeval y : (a : A[X]) → S') (f %ₘ minpoly A pb.gen) : S')

Tactic:
rw [aeval_eq_sum_range' this, aeval_eq_sum_range' this, map_sum]

Premises used: map_sum, 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
S' : Type u_7
inst_3 : Ring S'
inst_4 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
f : A[X]
h : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
this : (f %ₘ minpoly A pb.gen).natDegree < pb.dim
⊢ Eq.{u_7 + 1} (α := S')
    (∑ x ∈ Finset.range pb.dim,
      ((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
        ((f %ₘ minpoly A pb.gen).coeff x • pb.gen ^ x))
    (∑ i ∈ Finset.range pb.dim, (f %ₘ minpoly A pb.gen).coeff i • y ^ i)

Tactic:
Finset.sum_congr rfl fun i (hi : i ∈ Finset.range pb.dim) => ?_

Premises used: Finset.sum_congr, rfl
-- 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
S' : Type u_7
inst_3 : Ring S'
inst_4 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
f : A[X]
h : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
this : (f %ₘ minpoly A pb.gen).natDegree < pb.dim
neg :
  ∀ (i : ℕ) (hi : i ∈ Finset.range pb.dim),
    ((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
        ((f %ₘ minpoly A pb.gen).coeff i • pb.gen ^ i) =
      (f %ₘ minpoly A pb.gen).coeff i • y ^ i
⊢ Eq.{u_7 + 1} (α := S')
    (∑ x ∈ Finset.range pb.dim,
      ((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
        ((f %ₘ minpoly A pb.gen).coeff x • pb.gen ^ x))
    (∑ i ∈ Finset.range pb.dim, (f %ₘ minpoly A pb.gen).coeff i • y ^ i)

Tactic:
refine Finset.sum_congr rfl fun i (hi : i ∈ Finset.range pb.dim) => ?_

Premises used: Finset.sum_congr, rfl
-- 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
S' : Type u_7
inst_3 : Ring S'
inst_4 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
f : A[X]
h : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
this : (f %ₘ minpoly A pb.gen).natDegree < pb.dim
i : ℕ
hi : i ∈ Finset.range pb.dim
⊢ i < pb.dim

Tactic:
rw [Finset.mem_range] at hi

Premises used: Finset.mem_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
S' : Type u_7
inst_3 : Ring S'
inst_4 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
f : A[X]
h : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
this : (f %ₘ minpoly A pb.gen).natDegree < pb.dim
i : ℕ
hi : i < pb.dim
neg :
  HSMul.hSMul (β := S') ((f %ₘ minpoly A pb.gen).coeff i)
      (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
          (pb.gen ^ i) :
        S') =
    (f %ₘ minpoly A pb.gen).coeff i • y ^ i
⊢ ((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
      ((f %ₘ minpoly A pb.gen).coeff i • pb.gen ^ i) =
    (f %ₘ minpoly A pb.gen).coeff i • y ^ i

Tactic:
rw [map_smul]

Premises used: map_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
S' : Type u_7
inst_3 : Ring S'
inst_4 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
f : A[X]
h : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
this : (f %ₘ minpoly A pb.gen).natDegree < pb.dim
i : ℕ
hi : i < pb.dim
neg :
  ((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
      (pb.gen ^ i) =
    y ^ i
⊢ HSMul.hSMul (β := S') ((f %ₘ minpoly A pb.gen).coeff i)
      (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
          (pb.gen ^ i) :
        S') =
    (f %ₘ minpoly A pb.gen).coeff i • y ^ i

Tactic:
congr