awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) (0 : S) ((algebraMap A S : (a : A) → 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_7 + 1} (α := S') (0 : S') ((algebraMap A S' : (a : A) → S') 0 : S')
Tactic: convert! pb.constr_pow_algebraMap hy 0 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) (0 : S) ((algebraMap A S : (a : A) → S) 0 : S)
have h : Eq.{u_2 + 1} (α := S) 0 0
Tactic: rw [map_zero]
-- 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') (0 : S') ((algebraMap A S' : (a : A) → S') 0 : S')
have h : Eq.{u_7 + 1} (α := S') 0 0
Tactic: rw [map_zero]
-- 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
f : S →ₐ[A] S'
⊢ Eq.{u_7 + 1} (α := S')
    (((aeval ((f : (a : S) → S') pb.gen) : A[X] →ₐ[A] S') : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
have rw : Eq.{u_7 + 1} (α := S') ((f : (a : S) → S') ((aeval pb.gen : (a : A[X]) → S) (minpoly A pb.gen) : S) : S') (0 : S')
Tactic: rw [aeval_algHom_apply, minpoly.aeval, map_zero]
-- 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
f : S →ₐ[A] S'
rw : Eq.{u_7 + 1} (α := S') ((f : (a : S) → S') ((aeval pb.gen : (a : A[X]) → S) (minpoly A pb.gen) : S) : S') (0 : S')
⊢ Eq.{u_7 + 1} (α := S')
    (((aeval ((f : (a : S) → S') pb.gen) : A[X] →ₐ[A] S') : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
have rw₁ : Eq.{u_7 + 1} (α := S') ((f : (a : S) → S') 0 : S') (0 : S')
Tactic: rw [aeval_algHom_apply, minpoly.aeval, map_zero]
-- 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
f : S →ₐ[A] S'
rw : Eq.{u_7 + 1} (α := S') ((f : (a : S) → S') ((aeval pb.gen : (a : A[X]) → S) (minpoly A pb.gen) : S) : S') (0 : S')
rw₁ : Eq.{u_7 + 1} (α := S') ((f : (a : S) → S') 0 : S') (0 : S')
⊢ Eq.{u_7 + 1} (α := S')
    (((aeval ((f : (a : S) → S') pb.gen) : A[X] →ₐ[A] S') : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
have rw₂ : Eq.{u_7 + 1} (α := S') 0 0
Tactic: rw [aeval_algHom_apply, minpoly.aeval, map_zero]
-- 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'
inst_10 : IsDomain B
pb : PowerBasis A S
x : B
⊢ Eq.{u_5 + 1} (α := B) ((aeval x : (a : A[X]) → B) (minpoly A pb.gen) : B) (0 : B) ↔
    Membership.mem (α := B) (aroots (minpoly A pb.gen) B) ((Equiv.refl B : (a : B) → B) x : B)
have rw : Eq.{u_5 + 1} (α := B) ((aeval x : (a : A[X]) → B) (minpoly A pb.gen) : B) (0 : B) ↔
  Eq (α := B) ((aeval x : (a : B[X]) → B) (map (algebraMap A B) (minpoly A pb.gen)) : B) (0 : B)
Tactic: rw [Equiv.refl_apply, mem_roots_iff_aeval_eq_zero]
-- 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'
inst_10 : IsDomain B
pb : PowerBasis A S
x : B
rw :
  Eq.{u_5 + 1} (α := B) ((aeval x : (a : A[X]) → B) (minpoly A pb.gen) : B) (0 : B) ↔
    Eq (α := B) ((aeval x : (a : B[X]) → B) (map (algebraMap A B) (minpoly A pb.gen)) : B) (0 : B)
⊢ Eq.{u_5 + 1} (α := B) ((aeval x : (a : A[X]) → B) (minpoly A pb.gen) : B) (0 : B) ↔
    Membership.mem (α := B) (aroots (minpoly A pb.gen) B) ((Equiv.refl B : (a : B) → B) x : B)
have rw₁ : Ne (α := B[X]) (map (algebraMap A B) (minpoly A pb.gen)) 0
Tactic: rw [Equiv.refl_apply, mem_roots_iff_aeval_eq_zero]
-- 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
pb' : PowerBasis A S'
h₁ : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : A[X]) → S) (minpoly A pb'.gen) : S) (0 : S)
h₂ : Eq.{u_7 + 1} (α := S') ((aeval pb'.gen : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
⊢ (pb.lift pb'.gen h₂).comp (pb'.lift pb.gen h₁) = AlgHom.id A S'
have H : ∀ (x : S'),
  Eq (α := S') (((pb.lift pb'.gen h₂).comp (pb'.lift pb.gen h₁) : (a : S') → S') x : S')
    ((AlgHom.id A S' : (a : S') → S') x : S')
Tactic: ext 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
pb' : PowerBasis A S'
h₁ : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : A[X]) → S) (minpoly A pb'.gen) : S) (0 : S)
h₂ : Eq.{u_7 + 1} (α := S') ((aeval pb'.gen : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
x : S'
⊢ Eq (α := S') (((pb.lift pb'.gen h₂).comp (pb'.lift pb.gen h₁) : (a : S') → S') x : S')
    ((AlgHom.id A S' : (a : S') → S') x : S')
have H : ∀ (f : A[X]),
  Eq (α := S')
    (((pb.lift pb'.gen h₂).comp (pb'.lift pb.gen h₁) : (a : S') → S') ((aeval pb'.gen : (a : A[X]) → S') f : S') : S')
    ((AlgHom.id A S' : (a : S') → S') ((aeval pb'.gen : (a : A[X]) → S') f : S') : S')
Tactic: obtain ⟨f, hf, 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
pb' : PowerBasis A S'
h₁ : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : A[X]) → S) (minpoly A pb'.gen) : S) (0 : S)
h₂ : Eq.{u_7 + 1} (α := S') ((aeval pb'.gen : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
⊢ (pb'.lift pb.gen h₁).comp (pb.lift pb'.gen h₂) = AlgHom.id A S
have H : ∀ (x : S),
  Eq (α := S) (((pb'.lift pb.gen h₁).comp (pb.lift pb'.gen h₂) : (a : S) → S) x : S)
    ((AlgHom.id A S : (a : S) → S) x : S)
Tactic: ext 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
pb' : PowerBasis A S'
h₁ : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : A[X]) → S) (minpoly A pb'.gen) : S) (0 : S)
h₂ : Eq.{u_7 + 1} (α := S') ((aeval pb'.gen : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
x : S
⊢ Eq (α := S) (((pb'.lift pb.gen h₁).comp (pb.lift pb'.gen h₂) : (a : S) → S) x : S)
    ((AlgHom.id A S : (a : S) → S) x : S)
have H : ∀ (f : A[X]),
  Eq (α := S)
    (((pb'.lift pb.gen h₁).comp (pb.lift pb'.gen h₂) : (a : S) → S) ((aeval pb.gen : (a : A[X]) → S) f : S) : S)
    ((AlgHom.id A S : (a : S) → S) ((aeval pb.gen : (a : A[X]) → S) f : S) : S)
Tactic: obtain ⟨f, hf, 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
K : Type u_6
inst_1 : Field K
inst_2 : Algebra K S
x : S
⊢ LinearIndependent.{0, u_6, u_2} K (M := S) fun (i : Fin (natDegree (minpoly K x))) ↦ x ^ (↑i : ℕ)
have pos : ∀ (h : IsIntegral K x),
  LinearIndependent.{0, u_6, u_2} K (M := S) fun (i : Fin (natDegree (minpoly K x))) ↦ x ^ (↑i : ℕ)
Tactic: by_cases h : IsIntegral K x
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
K : Type u_6
inst_1 : Field K
inst_2 : Algebra K S
x : S
pos :
  ∀ (h : IsIntegral K x),
    LinearIndependent.{0, u_6, u_2} K (M := S) fun (i : Fin (natDegree (minpoly K x))) ↦ x ^ (↑i : ℕ)
⊢ LinearIndependent.{0, u_6, u_2} K (M := S) fun (i : Fin (natDegree (minpoly K x))) ↦ x ^ (↑i : ℕ)
have neg : ∀ (h : ¬IsIntegral K x),
  LinearIndependent.{0, u_6, u_2} K (M := S) fun (i : Fin (natDegree (minpoly K x))) ↦ x ^ (↑i : ℕ)
Tactic: by_cases h : IsIntegral K x
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
K : Type u_6
inst_1 : Field K
inst_2 : Algebra K S
x : S
h : ¬IsIntegral K x
⊢ LinearIndependent.{0, u_6, u_2} K (M := S) fun (i : Fin (natDegree (minpoly K x))) ↦ x ^ (↑i : ℕ)
have neg : LinearIndependent.{0, u_6, u_2} K (M := S) fun (i : Fin 0) ↦ x ^ (↑i : ℕ)
Tactic: rw [minpoly.eq_zero h, natDegree_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
K : Type u_6
inst_1 : Field K
inst_2 : Algebra K S
x : S
h : IsIntegral K x
⊢ LinearIndependent.{0, u_6, u_2} K (M := S) fun (i : Fin (natDegree (minpoly K x))) ↦ x ^ (↑i : ℕ)
have pos : ∀ (g : Fin (natDegree (minpoly K x)) → K)
  (hg : Eq.{u_2 + 1} (α := S) (∑ i : Fin (minpoly K x).natDegree, g i • x ^ (↑i : ℕ)) 0)
  (i : Fin (natDegree (minpoly K x))), g i = 0
Tactic: refine Fintype.linearIndependent_iff.2 fun g hg i => ?_
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (hypothesis)
Goal:
S : Type u_2
inst : Ring S
K : Type u_6
inst_1 : Field K
inst_2 : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
hg : Eq.{u_2 + 1} (α := S) (∑ i : Fin (minpoly K x).natDegree, g i • x ^ (↑i : ℕ)) 0
i : Fin (natDegree (minpoly K x))
⊢ g i = 0
have hg₁ : Eq.{u_2 + 1} (α := S)
  ((aeval x : (a : K[X]) → S) (∑ x_1 : Fin (minpoly K x).natDegree, (monomial (↑x_1 : ℕ) : (a : K) → K[X]) (g x_1)) : S)
  (0 : S)
Tactic: simp_rw [Algebra.smul_def, ← aeval_monomial, ← map_sum] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
K : Type u_6
inst_1 : Field K
inst_2 : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
i : Fin (natDegree (minpoly K x))
hg :
  Eq.{u_2 + 1} (α := S)
    ((aeval x : (a : K[X]) → S) (∑ x_1 : Fin (minpoly K x).natDegree, (monomial (↑x_1 : ℕ) : (a : K) → K[X]) (g x_1)) :
      S)
    (0 : S)
⊢ g i = 0
have pos : degree.{u_6} (R := K) (∑ x_1 : Fin (minpoly K x).natDegree, (monomial (↑x_1 : ℕ) : (a : K) → K[X]) (g x_1)) <
  degree (minpoly K x)
Tactic: apply (fun hn0 => (minpoly.degree_le_of_ne_zero K x (mt (fun h0 => ?_) hn0) hg).not_gt).mtr
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
K : Type u_6
inst_1 : Field K
inst_2 : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
i : Fin (natDegree (minpoly K x))
hg :
  Eq.{u_2 + 1} (α := S)
    ((aeval x : (a : K[X]) → S) (∑ x_1 : Fin (minpoly K x).natDegree, (monomial (↑x_1 : ℕ) : (a : K) → K[X]) (g x_1)) :
      S)
    (0 : S)
pos :
  degree.{u_6} (R := K) (∑ x_1 : Fin (minpoly K x).natDegree, (monomial (↑x_1 : ℕ) : (a : K) → K[X]) (g x_1)) <
    degree (minpoly K x)
⊢ g i = 0
have apply : ∀ (hn0 : ¬g i = 0)
  (h0 :
    Eq.{u_6 + 1} (α := K[X]) (∑ x_1 : Fin (minpoly K x).natDegree, (monomial (↑x_1 : ℕ) : (a : K) → K[X]) (g x_1)) 0),
  g i = 0
Tactic: apply (fun hn0 => (minpoly.degree_le_of_ne_zero K x (mt (fun h0 => ?_) hn0) hg).not_gt).mtr
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
K : Type u_6
inst_1 : Field K
inst_2 : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
i : Fin (natDegree (minpoly K x))
hg :
  Eq.{u_2 + 1} (α := S)
    ((aeval x : (a : K[X]) → S) (∑ x_1 : Fin (minpoly K x).natDegree, (monomial (↑x_1 : ℕ) : (a : K) → K[X]) (g x_1)) :
      S)
    (0 : S)
⊢ degree.{u_6} (R := K) (∑ x_1 : Fin (minpoly K x).natDegree, (monomial (↑x_1 : ℕ) : (a : K) → K[X]) (g x_1)) <
    degree (minpoly K x)
have pos : degree.{u_6} (R := K)
    (∑ x_1 : Fin (minpoly K x).natDegree,
      HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (g x_1) : K[X]) (HPow.hPow (α := K[X]) X (↑x_1 : ℕ))) <
  degree (minpoly K x)
Tactic: simp_rw [← C_mul_X_pow_eq_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (hypothesis)
Goal:
S : Type u_2
inst : Ring S
K : Type u_6
inst_1 : Field K
inst_2 : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
i : Fin (natDegree (minpoly K x))
hg :
  Eq.{u_2 + 1} (α := S)
    ((aeval x : (a : K[X]) → S) (∑ x_1 : Fin (minpoly K x).natDegree, (monomial (↑x_1 : ℕ) : (a : K) → K[X]) (g x_1)) :
      S)
    (0 : S)
hn0 : ¬g i = 0
h0 : Eq.{u_6 + 1} (α := K[X]) (∑ x_1 : Fin (minpoly K x).natDegree, (monomial (↑x_1 : ℕ) : (a : K) → K[X]) (g x_1)) 0
⊢ g i = 0
have h0₁ : Eq (α := K)
  ((lcoeff K (↑i : ℕ) : (a : K[X]) → K)
      (∑ x_1 : Fin (minpoly K x).natDegree, (monomial (↑x_1 : ℕ) : (a : K) → K[X]) (g x_1)) :
    K)
  ((lcoeff K (↑i : ℕ) : (a : K[X]) → K) 0 : K)
Tactic: apply_fun lcoeff K i at h0
Cleared hypotheses: h0
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (hypothesis)
Goal:
S : Type u_2
inst : Ring S
K : Type u_6
inst_1 : Field K
inst_2 : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
i : Fin (natDegree (minpoly K x))
hg :
  Eq.{u_2 + 1} (α := S)
    ((aeval x : (a : K[X]) → S) (∑ x_1 : Fin (minpoly K x).natDegree, (monomial (↑x_1 : ℕ) : (a : K) → K[X]) (g x_1)) :
      S)
    (0 : S)
hn0 : ¬g i = 0
h0 :
  Eq (α := K)
    ((lcoeff K (↑i : ℕ) : (a : K[X]) → K)
        (∑ x_1 : Fin (minpoly K x).natDegree, (monomial (↑x_1 : ℕ) : (a : K) → K[X]) (g x_1)) :
      K)
    ((lcoeff K (↑i : ℕ) : (a : K[X]) → K) 0 : K)
⊢ g i = 0
have h0₁ : (if Membership.mem (γ := Finset (Fin (natDegree (minpoly K x)))) Finset.univ i then g i else 0) = coeff 0 (↑i : ℕ)
Tactic: simp_rw [map_sum, lcoeff_apply, coeff_monomial, Fin.val_eq_val, Finset.sum_ite_eq'] at h0
Cleared hypotheses: h0
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial R
x y : S
hx : IsIntegral R x
hy : ∃ (f : R[X]), y = (aeval x : (a : R[X]) → S) f
⊢ Membership.mem (γ := Submodule R S)
    (Submodule.span R (Set.range fun (i : Fin (natDegree (minpoly R x))) ↦ x ^ (↑i : ℕ))) y
have obtain : ∀ (f : R[X]),
  Membership.mem.{u_2, u_2} (α := S) (γ := Submodule R S)
    (Submodule.span R (Set.range fun (i : Fin (natDegree (minpoly R x))) ↦ x ^ (↑i : ℕ)))
    ((aeval x : (a : R[X]) → S) f : S)
Tactic: obtain ⟨f, rfl⟩ := hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
⊢ Membership.mem.{u_2, u_2} (α := S) (γ := Submodule R S)
    (Submodule.span R (Set.range fun (i : Fin (natDegree (minpoly R x))) ↦ x ^ (↑i : ℕ)))
    ((aeval x : (a : R[X]) → S) f : S)
have apply : ∃ (f_1 : R[X]),
  f_1.degree < (↑(natDegree (minpoly R x)) : WithBot ℕ) ∧
    Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) f : S) ((aeval x : (a : R[X]) → S) f_1 : S)
Tactic: apply mem_span_pow'.mpr _
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
⊢ ∃ (f_1 : R[X]),
    f_1.degree < (↑(natDegree (minpoly R x)) : WithBot ℕ) ∧
      Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) f : S) ((aeval x : (a : R[X]) → S) f_1 : S)
have this : Monic (minpoly R x)
Tactic: have := minpoly.monic hx
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
this : Monic (minpoly R x)
⊢ ∃ (f_1 : R[X]),
    f_1.degree < (↑(natDegree (minpoly R x)) : WithBot ℕ) ∧
      Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) f : S) ((aeval x : (a : R[X]) → S) f_1 : S)
have refine : Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) f : S) ((aeval x : (a : R[X]) → S) (f %ₘ minpoly R x) : S)
Tactic: refine ⟨f %ₘ minpoly R x, (degree_modByMonic_lt _ this).trans_le degree_le_natDegree, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
this : Monic (minpoly R x)
| ((aeval x : (a : R[X]) → S) f : S)
have rw : ((aeval x : (a : R[X]) → S) (f %ₘ minpoly R x + minpoly R x * (f /ₘ minpoly R x)) : S)
Tactic: rw [← modByMonic_add_div f (minpoly R x)]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
this : Monic (minpoly R x)
⊢ Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) f : S) ((aeval x : (a : R[X]) → S) (f %ₘ minpoly R x) : S)
have conv_lhs : Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) (f %ₘ minpoly R x + minpoly R x * (f /ₘ minpoly R x)) : S)
  ((aeval x : (a : R[X]) → S) (f %ₘ minpoly R x) : S)
Tactic: conv_lhs => rw [← modByMonic_add_div f (minpoly R 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
S' : Type u_7
inst_7 : CommRing S'
inst_8 : Algebra R S'
pb : PowerBasis R S
e : S ≃ₐ[R] S'
i : Fin pb.dim
⊢ (pb.basis.map (↑e : S ≃ₗ[R] S') : (a : Fin pb.dim) → S') i =
    HPow.hPow (α := S') ((e : (a : S) → S') pb.gen : S') (↑i : ℕ)
have rw : ((↑e : S ≃ₗ[R] S') : (a : S) → S') ((pb.basis : (a : Fin pb.dim) → S) i : S) =
  HPow.hPow (α := S') ((e : (a : S) → S') pb.gen : S') (↑i : ℕ)
Tactic: rw [Basis.map_apply, pb.basis_eq_pow, e.toLinearEquiv_apply, map_pow]
-- 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
S' : Type u_7
inst_7 : CommRing S'
inst_8 : Algebra R S'
pb : PowerBasis R S
e : S ≃ₐ[R] S'
i : Fin pb.dim
rw :
  ((↑e : S ≃ₗ[R] S') : (a : S) → S') ((pb.basis : (a : Fin pb.dim) → S) i : S) =
    HPow.hPow (α := S') ((e : (a : S) → S') pb.gen : S') (↑i : ℕ)
⊢ (pb.basis.map (↑e : S ≃ₗ[R] S') : (a : Fin pb.dim) → S') i =
    HPow.hPow (α := S') ((e : (a : S) → S') pb.gen : S') (↑i : ℕ)
have rw₁ : ((↑e : S ≃ₗ[R] S') : (a : S) → S') (pb.gen ^ (↑i : ℕ)) = HPow.hPow (α := S') ((e : (a : S) → S') pb.gen : S') (↑i : ℕ)
Tactic: rw [Basis.map_apply, pb.basis_eq_pow, e.toLinearEquiv_apply, map_pow]
-- 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
S' : Type u_7
inst_7 : CommRing S'
inst_8 : Algebra R S'
pb : PowerBasis R S
e : S ≃ₐ[R] S'
i : Fin pb.dim
rw :
  ((↑e : S ≃ₗ[R] S') : (a : S) → S') ((pb.basis : (a : Fin pb.dim) → S) i : S) =
    HPow.hPow (α := S') ((e : (a : S) → S') pb.gen : S') (↑i : ℕ)
rw₁ :
  ((↑e : S ≃ₗ[R] S') : (a : S) → S') (pb.gen ^ (↑i : ℕ)) = HPow.hPow (α := S') ((e : (a : S) → S') pb.gen : S') (↑i : ℕ)
⊢ (pb.basis.map (↑e : S ≃ₗ[R] S') : (a : Fin pb.dim) → S') i =
    HPow.hPow (α := S') ((e : (a : S) → S') pb.gen : S') (↑i : ℕ)
have rw₂ : (e : (a : S) → S') (pb.gen ^ (↑i : ℕ)) = HPow.hPow (α := S') ((e : (a : S) → S') pb.gen : S') (↑i : ℕ)
Tactic: rw [Basis.map_apply, pb.basis_eq_pow, e.toLinearEquiv_apply, map_pow]
-- 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
S' : Type u_7
inst_7 : CommRing S'
inst_8 : Algebra R S'
pb : PowerBasis R S
e : S ≃ₐ[R] S'
i : Fin pb.dim
rw :
  ((↑e : S ≃ₗ[R] S') : (a : S) → S') ((pb.basis : (a : Fin pb.dim) → S) i : S) =
    HPow.hPow (α := S') ((e : (a : S) → S') pb.gen : S') (↑i : ℕ)
rw₁ :
  ((↑e : S ≃ₗ[R] S') : (a : S) → S') (pb.gen ^ (↑i : ℕ)) = HPow.hPow (α := S') ((e : (a : S) → S') pb.gen : S') (↑i : ℕ)
rw₂ : (e : (a : S) → S') (pb.gen ^ (↑i : ℕ)) = HPow.hPow (α := S') ((e : (a : S) → S') pb.gen : S') (↑i : ℕ)
⊢ (pb.basis.map (↑e : S ≃ₗ[R] S') : (a : Fin pb.dim) → S') i =
    HPow.hPow (α := S') ((e : (a : S) → S') pb.gen : S') (↑i : ℕ)
have rw₃ : HPow.hPow (α := S') ((e : (a : S) → S') pb.gen : S') (↑i : ℕ) =
  HPow.hPow (α := S') ((e : (a : S) → S') pb.gen : S') (↑i : ℕ)
Tactic: rw [Basis.map_apply, pb.basis_eq_pow, e.toLinearEquiv_apply, map_pow]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
S' : Type u_7
inst_2 : CommRing S'
inst_3 : Algebra A S
inst_4 : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
h₁ : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : A[X]) → S) (minpoly A (pb.map e).gen) : S) (0 : S)
h₂ : Eq.{u_7 + 1} (α := S') ((aeval (pb.map e).gen : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
⊢ pb.equivOfRoot (pb.map e) h₁ h₂ = e
have h : ∀ (x : S), Eq.{u_7 + 1} (α := S') ((pb.equivOfRoot (pb.map e) h₁ h₂ : (a : S) → S') x : S') ((e : (a : S) → S') x : S')
Tactic: ext x