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
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 %ₘ minpoly A pb.gen) : S) :
      S')
    ((aeval y : (a : A[X]) → S') (f %ₘ minpoly A pb.gen) : S')
have 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')
Tactic: by_cases hf : f %ₘ minpoly A pb.gen = 0
-- 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
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')
⊢ 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')
have 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')
Tactic: by_cases hf : f %ₘ minpoly A pb.gen = 0
-- 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
hf : ¬f %ₘ minpoly A pb.gen = 0
⊢ (f %ₘ minpoly A pb.gen).natDegree < pb.dim
have rw : (f %ₘ minpoly A pb.gen).natDegree < natDegree (minpoly A pb.gen)
Tactic: rw [← pb.natDegree_minpoly]
-- 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
hf : ¬f %ₘ minpoly A pb.gen = 0
⊢ (f %ₘ minpoly A pb.gen).natDegree < natDegree (minpoly A pb.gen)
have apply : (f %ₘ minpoly A pb.gen).degree < degree (minpoly A pb.gen)
Tactic: apply natDegree_lt_natDegree hf
-- 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
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')
have this : (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)
-- 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
hf : ¬f %ₘ minpoly A pb.gen = 0
this : (f %ₘ minpoly A pb.gen).natDegree < pb.dim
⊢ 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')
have 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)
Tactic: rw [aeval_eq_sum_range' this, aeval_eq_sum_range' this, map_sum]
-- 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
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)
have 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
Tactic: refine Finset.sum_congr rfl fun i (hi : i ∈ Finset.range pb.dim) => ?_
-- 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
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
⊢ ((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
have hi₁ : i < pb.dim
Tactic: rw [Finset.mem_range] at hi
Cleared hypotheses: hi
-- 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
hf : ¬f %ₘ minpoly A pb.gen = 0
this : (f %ₘ minpoly A pb.gen).natDegree < pb.dim
i : ℕ
hi : i < 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
have 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
Tactic: rw [map_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]
h : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
this : (f %ₘ minpoly A pb.gen).natDegree < pb.dim
i : ℕ
hi : i < pb.dim
⊢ 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
have 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
Tactic: congr
-- 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
hf : ¬f %ₘ minpoly A pb.gen = 0
this : (f %ₘ minpoly A pb.gen).natDegree < pb.dim
i : ℕ
hi : i < pb.dim
⊢ ((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
have 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, hi⟩ : Fin pb.dim) : ℕ)) =
  y ^ (↑(⟨i, hi⟩ : Fin pb.dim) : ℕ)
Tactic: rw [← Fin.val_mk hi, ← pb.basis_eq_pow ⟨i, hi⟩, Basis.constr_basis]
-- 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
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, hi⟩ : Fin pb.dim) : ℕ)) =
    y ^ (↑(⟨i, hi⟩ : Fin pb.dim) : ℕ)
⊢ ((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
have neg₁ : ((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
    ((pb.basis : (a : Fin pb.dim) → S) (⟨i, hi⟩ : Fin pb.dim) : S) =
  y ^ (↑(⟨i, hi⟩ : Fin pb.dim) : ℕ)
Tactic: rw [← Fin.val_mk hi, ← pb.basis_eq_pow ⟨i, hi⟩, Basis.constr_basis]
-- 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
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, hi⟩ : Fin pb.dim) : ℕ)) =
    y ^ (↑(⟨i, hi⟩ : Fin 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.basis : (a : Fin pb.dim) → S) (⟨i, hi⟩ : Fin pb.dim) : S) =
    y ^ (↑(⟨i, hi⟩ : Fin pb.dim) : ℕ)
⊢ ((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
have neg₂ : y ^ (↑(⟨i, hi⟩ : Fin pb.dim) : ℕ) = y ^ (↑(⟨i, hi⟩ : Fin pb.dim) : ℕ)
Tactic: rw [← Fin.val_mk hi, ← pb.basis_eq_pow ⟨i, hi⟩, Basis.constr_basis]
-- 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')
⊢ ((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S') pb.gen =
    y
have h : pb.gen = (aeval pb.gen : (a : A[X]) → S) X
Tactic: convert! pb.constr_pow_aeval hy 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
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')
h : pb.gen = (aeval pb.gen : (a : A[X]) → S) X
⊢ ((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S') pb.gen =
    y
have h₁ : y = (aeval y : (a : A[X]) → S') X
Tactic: convert! pb.constr_pow_aeval hy 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
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')
⊢ pb.gen = (aeval pb.gen : (a : A[X]) → S) X
have h : pb.gen = pb.gen
Tactic: rw [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
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')
⊢ y = (aeval y : (a : A[X]) → S') X
have h : y = y
Tactic: rw [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
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')
x : 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')
        ((algebraMap A S : (a : A) → S) x : S) :
      S')
    ((algebraMap A S' : (a : A) → S') x : S')
have h : Eq.{u_2 + 1} (α := S) ((algebraMap A S : (a : A) → S) x : S)
  ((aeval pb.gen : (a : A[X]) → S) ((C : (a : A) → A[X]) x : A[X]) : S)
Tactic: convert! pb.constr_pow_aeval hy (C 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
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')
x : A
h :
  Eq.{u_2 + 1} (α := S) ((algebraMap A S : (a : A) → S) x : S)
    ((aeval pb.gen : (a : A[X]) → S) ((C : (a : A) → A[X]) x : A[X]) : 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')
        ((algebraMap A S : (a : A) → S) x : S) :
      S')
    ((algebraMap A S' : (a : A) → S') x : S')
have h₁ : Eq.{u_7 + 1} (α := S') ((algebraMap A S' : (a : A) → S') x : S')
  ((aeval y : (a : A[X]) → S') ((C : (a : A) → A[X]) x : A[X]) : S')
Tactic: convert! pb.constr_pow_aeval hy (C 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
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')
x : A
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap A S : (a : A) → S) x : S)
    ((aeval pb.gen : (a : A[X]) → S) ((C : (a : A) → A[X]) x : A[X]) : S)
have h : Eq.{u_2 + 1} (α := S) ((algebraMap A S : (a : A) → S) x : S) ((algebraMap A S : (a : A) → S) x : S)
Tactic: rw [aeval_C]
-- 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')
x : A
⊢ Eq.{u_7 + 1} (α := S') ((algebraMap A S' : (a : A) → S') x : S')
    ((aeval y : (a : A[X]) → S') ((C : (a : A) → A[X]) x : A[X]) : S')
have h : Eq.{u_7 + 1} (α := S') ((algebraMap A S' : (a : A) → S') x : S') ((algebraMap A S' : (a : A) → S') x : S')
Tactic: rw [aeval_C]
-- 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')
x x' : S
⊢ ((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
      (x * x') =
    HMul.hMul (α := S') (β := S')
      (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S') x :
        S')
      (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
          x' :
        S')
have obtain : ∀ (f : A[X]),
  ((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
      (HMul.hMul (α := S) ((aeval pb.gen : (a : A[X]) → S) f : S) x') =
    HMul.hMul (α := S') (β := 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')
      (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
          x' :
        S')
Tactic: obtain ⟨f, rfl⟩ := pb.exists_eq_aeval' x
Cleared hypotheses: 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
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')
x' : S
f : A[X]
⊢ ((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
      (HMul.hMul (α := S) ((aeval pb.gen : (a : A[X]) → S) f : S) x') =
    HMul.hMul (α := S') (β := 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')
      (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
          x' :
        S')
have obtain : ∀ (g : A[X]),
  ((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
      (HMul.hMul (α := S) (β := S) ((aeval pb.gen : (a : A[X]) → S) f : S) ((aeval pb.gen : (a : A[X]) → S) g : S)) =
    HMul.hMul (α := S') (β := 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')
      (((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) g : S) :
        S')
Tactic: obtain ⟨g, rfl⟩ := pb.exists_eq_aeval' x'
Cleared hypotheses: x'
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra A B
K : Type u_6
inst_6 : Field K
inst_7 : Algebra A S
S' : Type u_7
inst_8 : Ring S'
inst_9 : 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')
⊢ Eq.{u_7 + 1} (α := S')
    (AddHom.toFun.{u_2, u_7} (M := S)
      (LinearMap.toAddHom.{u_4, u_4, u_2, u_7} (R := A) (S := A) (σ := RingHom.id A)
        ((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ)))
      1)
    1
have h : Eq.{u_2 + 1} (α := S) (1 : S) ((algebraMap A S : (a : A) → S) 1 : S)
Tactic: convert! pb.constr_pow_algebraMap hy 1 using 2
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra A B
K : Type u_6
inst_6 : Field K
inst_7 : Algebra A S
S' : Type u_7
inst_8 : Ring S'
inst_9 : 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')
h : Eq.{u_2 + 1} (α := S) (1 : S) ((algebraMap A S : (a : A) → S) 1 : S)
⊢ Eq.{u_7 + 1} (α := S')
    (AddHom.toFun.{u_2, u_7} (M := S)
      (LinearMap.toAddHom.{u_4, u_4, u_2, u_7} (R := A) (S := A) (σ := RingHom.id A)
        ((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ)))
      1)
    1
have h₁ : Eq.{u_7 + 1} (α := S') (1 : S') ((algebraMap A S' : (a : A) → S') 1 : S')
Tactic: convert! pb.constr_pow_algebraMap hy 1 using 2
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra A B
K : Type u_6
inst_6 : Field K
inst_7 : Algebra A S
S' : Type u_7
inst_8 : Ring S'
inst_9 : 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')
⊢ Eq.{u_2 + 1} (α := S) (1 : S) ((algebraMap A S : (a : A) → S) 1 : S)
have h : Eq.{u_2 + 1} (α := S) 1 1
Tactic: rw [map_one]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra A B
K : Type u_6
inst_6 : Field K
inst_7 : Algebra A S
S' : Type u_7
inst_8 : Ring S'
inst_9 : 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')
⊢ Eq.{u_7 + 1} (α := S') (1 : S') ((algebraMap A S' : (a : A) → S') 1 : S')
have h : Eq.{u_7 + 1} (α := S') 1 1
Tactic: rw [map_one]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra A B
K : Type u_6
inst_6 : Field K
inst_7 : Algebra A S
S' : Type u_7
inst_8 : Ring S'
inst_9 : 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')
⊢ Eq.{u_7 + 1} (α := S')
    (AddHom.toFun.{u_2, u_7} (M := S)
      (LinearMap.toAddHom.{u_4, u_4, u_2, u_7} (R := A) (S := A) (σ := RingHom.id A)
        ((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ)))
      0)
    0
have h : Eq.{u_2 + 1} (α := S) (0 : S) ((algebraMap A S : (a : A) → S) 0 : S)
Tactic: convert! pb.constr_pow_algebraMap hy 0 using 2