awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.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)
have 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 : ℕ)
Tactic: apply (pow_succ' _ _).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
h : Nontrivial A
k : Fin pb.dim
⊢ 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 : ℕ)
have pos : ∀ (h : (↑k : ℕ) + 1 = pb.dim),
  pb.gen ^ ((↑k : ℕ) + 1) = ∑ x : Fin pb.dim, -pb.minpolyGen.coeff (↑x : ℕ) • pb.gen ^ (↑x : ℕ)
Tactic: split_ifs with h
-- 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
pos :
  ∀ (h : (↑k : ℕ) + 1 = pb.dim),
    pb.gen ^ ((↑k : ℕ) + 1) = ∑ x : Fin pb.dim, -pb.minpolyGen.coeff (↑x : ℕ) • 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 : ℕ)
have 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 : ℕ))
Tactic: split_ifs with h
-- 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_1 : Nontrivial A
k : Fin pb.dim
h : (↑k : ℕ) + 1 = pb.dim
⊢ pb.gen ^ ((↑k : ℕ) + 1) = ∑ x : Fin pb.dim, -pb.minpolyGen.coeff (↑x : ℕ) • pb.gen ^ (↑x : ℕ)
have pos : pb.gen ^ pb.dim + ∑ x : Fin pb.dim, pb.minpolyGen.coeff (↑x : ℕ) • pb.gen ^ (↑x : ℕ) = 0
Tactic: simp_rw [h, neg_smul, Finset.sum_neg_distrib, eq_neg_iff_add_eq_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
h_1 : Nontrivial A
k : Fin pb.dim
h : (↑k : ℕ) + 1 = pb.dim
⊢ pb.gen ^ pb.dim + ∑ x : Fin pb.dim, pb.minpolyGen.coeff (↑x : ℕ) • pb.gen ^ (↑x : ℕ) = 0
have 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
Tactic: convert! pb.aeval_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
h_1 : Nontrivial A
k : Fin pb.dim
h : (↑k : ℕ) + 1 = 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
have 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
Tactic: rw [add_comm, aeval_eq_sum_range, Finset.sum_range_succ, ← leadingCoeff,
      pb.minpolyGen_monic.leadingCoeff, one_smul, natDegree_minpolyGen, 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
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
⊢ pb.gen ^ pb.dim + ∑ x : Fin pb.dim, pb.minpolyGen.coeff (↑x : ℕ) • pb.gen ^ (↑x : ℕ) =
    (aeval pb.gen : (a : A[X]) → S) pb.minpolyGen
have 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
Tactic: rw [add_comm, aeval_eq_sum_range, Finset.sum_range_succ, ← leadingCoeff,
      pb.minpolyGen_monic.leadingCoeff, one_smul, natDegree_minpolyGen, 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
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
⊢ pb.gen ^ pb.dim + ∑ x : Fin pb.dim, pb.minpolyGen.coeff (↑x : ℕ) • pb.gen ^ (↑x : ℕ) =
    (aeval pb.gen : (a : A[X]) → S) pb.minpolyGen
have 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
Tactic: rw [add_comm, aeval_eq_sum_range, Finset.sum_range_succ, ← leadingCoeff,
      pb.minpolyGen_monic.leadingCoeff, one_smul, natDegree_minpolyGen, 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
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
⊢ pb.gen ^ pb.dim + ∑ x : Fin pb.dim, pb.minpolyGen.coeff (↑x : ℕ) • pb.gen ^ (↑x : ℕ) =
    (aeval pb.gen : (a : A[X]) → S) pb.minpolyGen
have 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
Tactic: rw [add_comm, aeval_eq_sum_range, Finset.sum_range_succ, ← leadingCoeff,
      pb.minpolyGen_monic.leadingCoeff, one_smul, natDegree_minpolyGen, 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
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
⊢ pb.gen ^ pb.dim + ∑ x : Fin pb.dim, pb.minpolyGen.coeff (↑x : ℕ) • pb.gen ^ (↑x : ℕ) =
    (aeval pb.gen : (a : A[X]) → S) pb.minpolyGen
have 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)
Tactic: rw [add_comm, aeval_eq_sum_range, Finset.sum_range_succ, ← leadingCoeff,
      pb.minpolyGen_monic.leadingCoeff, one_smul, natDegree_minpolyGen, 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
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)
⊢ pb.gen ^ pb.dim + ∑ x : Fin pb.dim, pb.minpolyGen.coeff (↑x : ℕ) • pb.gen ^ (↑x : ℕ) =
    (aeval pb.gen : (a : A[X]) → S) pb.minpolyGen
have 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
Tactic: rw [add_comm, aeval_eq_sum_range, Finset.sum_range_succ, ← leadingCoeff,
      pb.minpolyGen_monic.leadingCoeff, one_smul, natDegree_minpolyGen, 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
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
⊢ pb.gen ^ pb.dim + ∑ x : Fin pb.dim, pb.minpolyGen.coeff (↑x : ℕ) • pb.gen ^ (↑x : ℕ) =
    (aeval pb.gen : (a : A[X]) → S) pb.minpolyGen
have 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
Tactic: rw [add_comm, aeval_eq_sum_range, Finset.sum_range_succ, ← leadingCoeff,
      pb.minpolyGen_monic.leadingCoeff, one_smul, natDegree_minpolyGen, 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
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
⊢ pb.gen ^ pb.dim + ∑ x : Fin pb.dim, pb.minpolyGen.coeff (↑x : ℕ) • pb.gen ^ (↑x : ℕ) =
    (aeval pb.gen : (a : A[X]) → S) pb.minpolyGen
have 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
Tactic: rw [add_comm, aeval_eq_sum_range, Finset.sum_range_succ, ← leadingCoeff,
      pb.minpolyGen_monic.leadingCoeff, one_smul, natDegree_minpolyGen, 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
h_1 : Nontrivial A
k : Fin pb.dim
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 : ℕ))
have neg : (↑(⟨(↑k : ℕ) + 1, sorry⟩ : Fin pb.dim) : ℕ) = (↑k : ℕ) + 1
Tactic: rw [Fintype.sum_eq_single (⟨(k : ℕ) + 1, lt_of_le_of_ne k.2 h⟩ : Fin pb.dim), if_pos, one_smul]
-- 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_1 : Nontrivial A
k : Fin pb.dim
h : ¬(↑k : ℕ) + 1 = pb.dim
neg : (↑(⟨(↑k : ℕ) + 1, ⋯⟩ : Fin pb.dim) : ℕ) = (↑k : ℕ) + 1
⊢ 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 : ℕ))
have neg₁ : ∀ (x : Fin pb.dim),
  x ≠ ⟨(↑k : ℕ) + 1, sorry⟩ →
    HSMul.hSMul.{u_4, u_2, u_2} (α := A) (if (↑x : ℕ) = (↑k : ℕ) + 1 then 1 else 0) (pb.gen ^ (↑x : ℕ)) = 0
Tactic: rw [Fintype.sum_eq_single (⟨(k : ℕ) + 1, lt_of_le_of_ne k.2 h⟩ : Fin pb.dim), if_pos, one_smul]
-- 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_1 : Nontrivial A
k : Fin pb.dim
h : ¬(↑k : ℕ) + 1 = pb.dim
x : Fin pb.dim
hx : x ≠ ⟨(↑k : ℕ) + 1, ⋯⟩
⊢ HSMul.hSMul.{u_4, u_2, u_2} (α := A) (if (↑x : ℕ) = (↑k : ℕ) + 1 then 1 else 0) (pb.gen ^ (↑x : ℕ)) = 0
have neg : ¬(↑x : ℕ) = (↑k : ℕ) + 1
Tactic: rw [if_neg, zero_smul]
-- 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
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]
⊢ 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')
have 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')
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
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')
⊢ 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')
have 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')
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
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
⊢ 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')
have 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')
Tactic: rw [(Subsingleton.elim _ _ : f = 0), aeval_zero, map_zero, aeval_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
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')
⊢ 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')
have 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')
Tactic: rw [(Subsingleton.elim _ _ : f = 0), aeval_zero, map_zero, aeval_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
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')
⊢ 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')
have inl₂ : Eq.{u_7 + 1} (α := S') (0 : S') ((aeval y : (a : A[X]) → S') 0 : S')
Tactic: rw [(Subsingleton.elim _ _ : f = 0), aeval_zero, map_zero, aeval_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
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')
⊢ 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')
have inl₃ : Eq.{u_7 + 1} (α := S') 0 0
Tactic: rw [(Subsingleton.elim _ _ : f = 0), aeval_zero, map_zero, aeval_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
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
⊢ 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')
have 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')
Tactic: rw [← aeval_modByMonic_eq_self_of_root (minpoly.aeval _ _), ← aeval_modByMonic_eq_self_of_root hy]