awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
x : K
hsep : IsSeparable F x
inst_7 : IsPurelyInseparable F E
hi : IsIntegral F x
hi' : IsIntegral E x
hsep' : IsSeparable E x
this_1 : Algebra.IsSeparable.{u, w} F ↥F⟮x⟯
this_2 : Algebra.IsSeparable.{v, w} E ↥E⟮x⟯
this : Algebra.IsAlgebraic.{u, w} F ↥F⟮x⟯
rw : natDegree (minpoly F x) = natDegree (minpoly E x)
⊢ natDegree (Polynomial.map (algebraMap F E) (minpoly F x)) = natDegree (minpoly E x)
have rw₁ : Module.finrank.{u, w} F ↥F⟮x⟯ = natDegree (minpoly E x)
Tactic: rw [Polynomial.natDegree_map, ← adjoin.finrank hi, ← adjoin.finrank hi',
    ← finSepDegree_eq_finrank_of_isSeparable F _, ← finSepDegree_eq_finrank_of_isSeparable E _,
    finSepDegree_eq, finSepDegree_eq,
    sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable (F := F) E]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
x : K
hsep : IsSeparable F x
inst_7 : IsPurelyInseparable F E
hi : IsIntegral F x
hi' : IsIntegral E x
hsep' : IsSeparable E x
this_1 : Algebra.IsSeparable.{u, w} F ↥F⟮x⟯
this_2 : Algebra.IsSeparable.{v, w} E ↥E⟮x⟯
this : Algebra.IsAlgebraic.{u, w} F ↥F⟮x⟯
rw : natDegree (minpoly F x) = natDegree (minpoly E x)
rw₁ : Module.finrank.{u, w} F ↥F⟮x⟯ = natDegree (minpoly E x)
⊢ natDegree (Polynomial.map (algebraMap F E) (minpoly F x)) = natDegree (minpoly E x)
have rw₂ : Module.finrank.{u, w} F ↥F⟮x⟯ = Module.finrank.{v, w} E ↥E⟮x⟯
Tactic: rw [Polynomial.natDegree_map, ← adjoin.finrank hi, ← adjoin.finrank hi',
    ← finSepDegree_eq_finrank_of_isSeparable F _, ← finSepDegree_eq_finrank_of_isSeparable E _,
    finSepDegree_eq, finSepDegree_eq,
    sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable (F := F) E]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
x : K
hsep : IsSeparable F x
inst_7 : IsPurelyInseparable F E
hi : IsIntegral F x
hi' : IsIntegral E x
hsep' : IsSeparable E x
this_1 : Algebra.IsSeparable.{u, w} F ↥F⟮x⟯
this_2 : Algebra.IsSeparable.{v, w} E ↥E⟮x⟯
this : Algebra.IsAlgebraic.{u, w} F ↥F⟮x⟯
rw : natDegree (minpoly F x) = natDegree (minpoly E x)
rw₁ : Module.finrank.{u, w} F ↥F⟮x⟯ = natDegree (minpoly E x)
rw₂ : Module.finrank.{u, w} F ↥F⟮x⟯ = Module.finrank.{v, w} E ↥E⟮x⟯
⊢ natDegree (Polynomial.map (algebraMap F E) (minpoly F x)) = natDegree (minpoly E x)
have rw₃ : finSepDegree.{u, w} F ↥F⟮x⟯ = Module.finrank.{v, w} E ↥E⟮x⟯
Tactic: rw [Polynomial.natDegree_map, ← adjoin.finrank hi, ← adjoin.finrank hi',
    ← finSepDegree_eq_finrank_of_isSeparable F _, ← finSepDegree_eq_finrank_of_isSeparable E _,
    finSepDegree_eq, finSepDegree_eq,
    sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable (F := F) E]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
x : K
hsep : IsSeparable F x
inst_7 : IsPurelyInseparable F E
hi : IsIntegral F x
hi' : IsIntegral E x
hsep' : IsSeparable E x
this_1 : Algebra.IsSeparable.{u, w} F ↥F⟮x⟯
this_2 : Algebra.IsSeparable.{v, w} E ↥E⟮x⟯
this : Algebra.IsAlgebraic.{u, w} F ↥F⟮x⟯
rw : natDegree (minpoly F x) = natDegree (minpoly E x)
rw₁ : Module.finrank.{u, w} F ↥F⟮x⟯ = natDegree (minpoly E x)
rw₂ : Module.finrank.{u, w} F ↥F⟮x⟯ = Module.finrank.{v, w} E ↥E⟮x⟯
rw₃ : finSepDegree.{u, w} F ↥F⟮x⟯ = Module.finrank.{v, w} E ↥E⟮x⟯
⊢ natDegree (Polynomial.map (algebraMap F E) (minpoly F x)) = natDegree (minpoly E x)
have rw₄ : finSepDegree.{u, w} F ↥F⟮x⟯ = finSepDegree.{v, w} E ↥E⟮x⟯
Tactic: rw [Polynomial.natDegree_map, ← adjoin.finrank hi, ← adjoin.finrank hi',
    ← finSepDegree_eq_finrank_of_isSeparable F _, ← finSepDegree_eq_finrank_of_isSeparable E _,
    finSepDegree_eq, finSepDegree_eq,
    sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable (F := F) E]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
x : K
hsep : IsSeparable F x
inst_7 : IsPurelyInseparable F E
hi : IsIntegral F x
hi' : IsIntegral E x
hsep' : IsSeparable E x
this_1 : Algebra.IsSeparable.{u, w} F ↥F⟮x⟯
this_2 : Algebra.IsSeparable.{v, w} E ↥E⟮x⟯
this : Algebra.IsAlgebraic.{u, w} F ↥F⟮x⟯
rw : natDegree (minpoly F x) = natDegree (minpoly E x)
rw₁ : Module.finrank.{u, w} F ↥F⟮x⟯ = natDegree (minpoly E x)
rw₂ : Module.finrank.{u, w} F ↥F⟮x⟯ = Module.finrank.{v, w} E ↥E⟮x⟯
rw₃ : finSepDegree.{u, w} F ↥F⟮x⟯ = Module.finrank.{v, w} E ↥E⟮x⟯
rw₄ : finSepDegree.{u, w} F ↥F⟮x⟯ = finSepDegree.{v, w} E ↥E⟮x⟯
⊢ natDegree (Polynomial.map (algebraMap F E) (minpoly F x)) = natDegree (minpoly E x)
have rw₅ : (Cardinal.toNat : (a : Cardinal.{w}) → ℕ) (sepDegree F ↥F⟮x⟯) = finSepDegree.{v, w} E ↥E⟮x⟯
Tactic: rw [Polynomial.natDegree_map, ← adjoin.finrank hi, ← adjoin.finrank hi',
    ← finSepDegree_eq_finrank_of_isSeparable F _, ← finSepDegree_eq_finrank_of_isSeparable E _,
    finSepDegree_eq, finSepDegree_eq,
    sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable (F := F) E]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
x : K
hsep : IsSeparable F x
inst_7 : IsPurelyInseparable F E
hi : IsIntegral F x
hi' : IsIntegral E x
hsep' : IsSeparable E x
this_1 : Algebra.IsSeparable.{u, w} F ↥F⟮x⟯
this_2 : Algebra.IsSeparable.{v, w} E ↥E⟮x⟯
this : Algebra.IsAlgebraic.{u, w} F ↥F⟮x⟯
rw : natDegree (minpoly F x) = natDegree (minpoly E x)
rw₁ : Module.finrank.{u, w} F ↥F⟮x⟯ = natDegree (minpoly E x)
rw₂ : Module.finrank.{u, w} F ↥F⟮x⟯ = Module.finrank.{v, w} E ↥E⟮x⟯
rw₃ : finSepDegree.{u, w} F ↥F⟮x⟯ = Module.finrank.{v, w} E ↥E⟮x⟯
rw₄ : finSepDegree.{u, w} F ↥F⟮x⟯ = finSepDegree.{v, w} E ↥E⟮x⟯
rw₅ : (Cardinal.toNat : (a : Cardinal.{w}) → ℕ) (sepDegree F ↥F⟮x⟯) = finSepDegree.{v, w} E ↥E⟮x⟯
⊢ natDegree (Polynomial.map (algebraMap F E) (minpoly F x)) = natDegree (minpoly E x)
have rw₆ : Eq (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{w}) → ℕ) (sepDegree F ↥F⟮x⟯) : ℕ)
  ((Cardinal.toNat : (a : Cardinal.{w}) → ℕ) (sepDegree E ↥E⟮x⟯) : ℕ)
Tactic: rw [Polynomial.natDegree_map, ← adjoin.finrank hi, ← adjoin.finrank hi',
    ← finSepDegree_eq_finrank_of_isSeparable F _, ← finSepDegree_eq_finrank_of_isSeparable E _,
    finSepDegree_eq, finSepDegree_eq,
    sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable (F := F) E]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
x : K
hsep : IsSeparable F x
inst_7 : IsPurelyInseparable F E
hi : IsIntegral F x
hi' : IsIntegral E x
hsep' : IsSeparable E x
this_1 : Algebra.IsSeparable.{u, w} F ↥F⟮x⟯
this_2 : Algebra.IsSeparable.{v, w} E ↥E⟮x⟯
this : Algebra.IsAlgebraic.{u, w} F ↥F⟮x⟯
rw : natDegree (minpoly F x) = natDegree (minpoly E x)
rw₁ : Module.finrank.{u, w} F ↥F⟮x⟯ = natDegree (minpoly E x)
rw₂ : Module.finrank.{u, w} F ↥F⟮x⟯ = Module.finrank.{v, w} E ↥E⟮x⟯
rw₃ : finSepDegree.{u, w} F ↥F⟮x⟯ = Module.finrank.{v, w} E ↥E⟮x⟯
rw₄ : finSepDegree.{u, w} F ↥F⟮x⟯ = finSepDegree.{v, w} E ↥E⟮x⟯
rw₅ : (Cardinal.toNat : (a : Cardinal.{w}) → ℕ) (sepDegree F ↥F⟮x⟯) = finSepDegree.{v, w} E ↥E⟮x⟯
rw₆ :
  Eq (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{w}) → ℕ) (sepDegree F ↥F⟮x⟯) : ℕ)
    ((Cardinal.toNat : (a : Cardinal.{w}) → ℕ) (sepDegree E ↥E⟮x⟯) : ℕ)
⊢ natDegree (Polynomial.map (algebraMap F E) (minpoly F x)) = natDegree (minpoly E x)
have rw₇ : Eq (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{w}) → ℕ) (sepDegree F ↥F⟮x⟯) : ℕ)
  ((Cardinal.toNat : (a : Cardinal.{w}) → ℕ) (sepDegree F ↥F⟮x⟯) : ℕ)
Tactic: rw [Polynomial.natDegree_map, ← adjoin.finrank hi, ← adjoin.finrank hi',
    ← finSepDegree_eq_finrank_of_isSeparable F _, ← finSepDegree_eq_finrank_of_isSeparable E _,
    finSepDegree_eq, finSepDegree_eq,
    sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable (F := F) E]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst_3 : IsPurelyInseparable F E
K : Type v := AlgebraicClosure E
⊢ Irreducible (M := E[X]) (Polynomial.map (algebraMap F E) f)
have obtain : ∀ (x : K) (hx : Eq.{v + 1} (α := K) ((aeval x : (a : F[X]) → K) f : K) (0 : K)),
  Irreducible (M := E[X]) (Polynomial.map (algebraMap F E) f)
Tactic: obtain ⟨x, hx⟩ := IsAlgClosed.exists_aeval_eq_zero K f
    (natDegree_pos_iff_degree_pos.1 hirr.natDegree_pos).ne'
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst_3 : IsPurelyInseparable F E
K : Type v := AlgebraicClosure E
x : K
hx : Eq.{v + 1} (α := K) ((aeval x : (a : F[X]) → K) f : K) (0 : K)
⊢ Associated f (minpoly F x)
have this : IsUnit (M := F[X]) ((C : (a : F) → F[X]) f.leadingCoeff⁻¹ : F[X])
Tactic: have := isUnit_C.2 (leadingCoeff_ne_zero.2 hirr.ne_zero).isUnit.inv
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst_3 : IsPurelyInseparable F E
K : Type v := AlgebraicClosure E
x : K
hx : Eq.{v + 1} (α := K) ((aeval x : (a : F[X]) → K) f : K) (0 : K)
this : IsUnit (M := F[X]) ((C : (a : F) → F[X]) f.leadingCoeff⁻¹ : F[X])
⊢ f * (↑this.unit : F[X]) = minpoly F x
have rw : HMul.hMul (β := F[X]) f ((C : (a : F) → F[X]) f.leadingCoeff⁻¹ : F[X]) = minpoly F x
Tactic: rw [IsUnit.unit_spec, minpoly.eq_of_irreducible hirr hx]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst_3 : IsPurelyInseparable F E
K : Type v := AlgebraicClosure E
x : K
hx : Eq.{v + 1} (α := K) ((aeval x : (a : F[X]) → K) f : K) (0 : K)
this : IsUnit (M := F[X]) ((C : (a : F) → F[X]) f.leadingCoeff⁻¹ : F[X])
rw : HMul.hMul (β := F[X]) f ((C : (a : F) → F[X]) f.leadingCoeff⁻¹ : F[X]) = minpoly F x
⊢ f * (↑this.unit : F[X]) = minpoly F x
have rw₁ : Eq (α := F[X]) (minpoly F x) (minpoly F x)
Tactic: rw [IsUnit.unit_spec, minpoly.eq_of_irreducible hirr hx]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst_3 : IsPurelyInseparable F E
K : Type v := AlgebraicClosure E
x : K
hx : Eq.{v + 1} (α := K) ((aeval x : (a : F[X]) → K) f : K) (0 : K)
⊢ Irreducible (M := E[X]) (Polynomial.map (algebraMap F E) f)
have ha : Associated f (minpoly F x)
Tactic: have ha : Associated f (minpoly F x) := by
    have := isUnit_C.2 (leadingCoeff_ne_zero.2 hirr.ne_zero).isUnit.inv
    exact ⟨this.unit, by rw [IsUnit.unit_spec, minpoly.eq_of_irreducible hirr hx]⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst_3 : IsPurelyInseparable F E
K : Type v := AlgebraicClosure E
x : K
hx : Eq.{v + 1} (α := K) ((aeval x : (a : F[X]) → K) f : K) (0 : K)
ha : Associated f (minpoly F x)
⊢ Irreducible (M := E[X]) (Polynomial.map (algebraMap F E) f)
have ha' : Associated (M := E[X]) (Polynomial.map (algebraMap F E) f) (Polynomial.map (algebraMap F E) (minpoly F x))
Tactic: have ha' : Associated (f.map (algebraMap F E)) ((minpoly F x).map (algebraMap F E)) :=
    ha.map (mapRingHom (algebraMap F E)).toMonoidHom
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst_3 : IsPurelyInseparable F E
K : Type v := AlgebraicClosure E
x : K
hx : Eq.{v + 1} (α := K) ((aeval x : (a : F[X]) → K) f : K) (0 : K)
ha : Associated f (minpoly F x)
ha' : Associated (M := E[X]) (Polynomial.map (algebraMap F E) f) (Polynomial.map (algebraMap F E) (minpoly F x))
⊢ Irreducible (M := E[X]) (Polynomial.map (algebraMap F E) f)
have heq : Eq (α := E[X]) (Polynomial.map (algebraMap F E) (minpoly F x)) (minpoly E x)
Tactic: have heq := minpoly.map_eq_of_isSeparable_of_isPurelyInseparable E x (ha.separable hsep)
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst_3 : IsPurelyInseparable F E
K : Type v := AlgebraicClosure E
x : K
hx : Eq.{v + 1} (α := K) ((aeval x : (a : F[X]) → K) f : K) (0 : K)
ha : Associated f (minpoly F x)
ha' : Associated (M := E[X]) (Polynomial.map (algebraMap F E) f) (Polynomial.map (algebraMap F E) (minpoly F x))
heq : Eq (α := E[X]) (Polynomial.map (algebraMap F E) (minpoly F x)) (minpoly E x)
⊢ Irreducible (M := E[X]) (Polynomial.map (algebraMap F E) f)
have rw : Irreducible (M := E[X]) (minpoly E x)
Tactic: rw [ha'.irreducible_iff, heq]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
r : K
x : K⟮X⟯
⊢ r • x = HMul.hMul (α := K⟮X⟯) ((C : (a : K) → K⟮X⟯) r : K⟮X⟯) x
have rw : HMul.hMul (α := K⟮X⟯) ((algebraMap K K⟮X⟯ : (a : K) → K⟮X⟯) r : K⟮X⟯) x =
  HMul.hMul (α := K⟮X⟯) ((C : (a : K) → K⟮X⟯) r : K⟮X⟯) x
Tactic: rw [Algebra.smul_def, algebraMap_eq_C]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
r : K
x : K⟮X⟯
rw :
  HMul.hMul (α := K⟮X⟯) ((algebraMap K K⟮X⟯ : (a : K) → K⟮X⟯) r : K⟮X⟯) x =
    HMul.hMul (α := K⟮X⟯) ((C : (a : K) → K⟮X⟯) r : K⟮X⟯) x
⊢ r • x = HMul.hMul (α := K⟮X⟯) ((C : (a : K) → K⟮X⟯) r : K⟮X⟯) x
have rw₁ : HMul.hMul (α := K⟮X⟯) ((C : (a : K) → K⟮X⟯) r : K⟮X⟯) x = HMul.hMul (α := K⟮X⟯) ((C : (a : K) → K⟮X⟯) r : K⟮X⟯) x
Tactic: rw [Algebra.smul_def, algebraMap_eq_C]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
⊢ Function.Injective.{u + 1, u + 1} (α := K) (β := K⟮X⟯) (⇑C : (a : K) → K⟮X⟯)
have rw : Function.Injective.{u + 1, u + 1} (α := K) (β := K⟮X⟯)
  (Function.comp (β := K[X]) (⇑(algebraMap K[X] K⟮X⟯) : (a : K[X]) → K⟮X⟯) (⇑Polynomial.C : (a : K) → K[X]))
Tactic: rw [← algebraMap_comp_C, RingHom.coe_comp]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
p : K[X]
⊢ Eq (α := K⟮X⟯) ((Polynomial.aeval X : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
    ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
have add : ∀ (p q : K[X]),
  Eq (α := K⟮X⟯) ((Polynomial.aeval X : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯) →
    Eq (α := K⟮X⟯) ((Polynomial.aeval X : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) →
      Eq (α := K⟮X⟯) ((Polynomial.aeval X : (a : K[X]) → K⟮X⟯) (p + q) : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (p + q) : K⟮X⟯)
Tactic: induction p using Polynomial.induction_on'
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
p : K[X]
add :
  ∀ (p q : K[X]),
    Eq (α := K⟮X⟯) ((Polynomial.aeval X : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯) →
      Eq (α := K⟮X⟯) ((Polynomial.aeval X : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) →
        Eq (α := K⟮X⟯) ((Polynomial.aeval X : (a : K[X]) → K⟮X⟯) (p + q) : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (p + q) : K⟮X⟯)
⊢ Eq (α := K⟮X⟯) ((Polynomial.aeval X : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
    ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
have monomial : ∀ (n : ℕ) (a : K),
  Eq (α := K⟮X⟯) ((Polynomial.aeval X : (a : K[X]) → K⟮X⟯) ((Polynomial.monomial n : (a : K) → K[X]) a) : K⟮X⟯)
    ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Polynomial.monomial n : (a : K) → K[X]) a) : K⟮X⟯)
Tactic: induction p using Polynomial.induction_on'
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : Field K
f : K⟮X⟯
⊢ (∃ (c : K), f = (C : (a : K) → K⟮X⟯) c) ↔ f.num.natDegree = 0 ∧ f.denom.natDegree = 0
have refine : f.num.natDegree = 0 ∧ f.denom.natDegree = 0 → ∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
Tactic: refine ⟨by rintro ⟨c, rfl⟩; simp, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : Field K
f : K⟮X⟯
⊢ f.num.natDegree = 0 ∧ f.denom.natDegree = 0 → ∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
have rw : ((∃ (x : K), (Polynomial.C : (a : K) → K[X]) x = f.num) ∧ ∃ (x : K), (Polynomial.C : (a : K) → K[X]) x = f.denom) →
  ∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
Tactic: rw [Polynomial.natDegree_eq_zero, Polynomial.natDegree_eq_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : Field K
f : K⟮X⟯
a : K
ha : (Polynomial.C : (a : K) → K[X]) a = f.num
b : K
hb : (Polynomial.C : (a : K) → K[X]) b = f.denom
⊢ ∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
have h : f = (C : (a : K) → K⟮X⟯) (a / b)
Tactic: use a / b
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : Field K
f : K⟮X⟯
a : K
ha : (Polynomial.C : (a : K) → K[X]) a = f.num
b : K
hb : (Polynomial.C : (a : K) → K[X]) b = f.denom
⊢ f = (C : (a : K) → K⟮X⟯) (a / b)
have h : HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.num : K⟮X⟯)
    ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.denom : K⟮X⟯) =
  (C : (a : K) → K⟮X⟯) (a / b)
Tactic: rw [← num_div_denom f, ← ha, ← hb, algebraMap_C, algebraMap_C, map_div₀]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : Field K
f : K⟮X⟯
a : K
ha : (Polynomial.C : (a : K) → K[X]) a = f.num
b : K
hb : (Polynomial.C : (a : K) → K[X]) b = f.denom
h :
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.num : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.denom : K⟮X⟯) =
    (C : (a : K) → K⟮X⟯) (a / b)
⊢ f = (C : (a : K) → K⟮X⟯) (a / b)
have h₁ : HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯)
    ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Polynomial.C : (a : K) → K[X]) a) : K⟮X⟯)
    ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.denom : K⟮X⟯) =
  (C : (a : K) → K⟮X⟯) (a / b)
Tactic: rw [← num_div_denom f, ← ha, ← hb, algebraMap_C, algebraMap_C, map_div₀]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : Field K
f : K⟮X⟯
a : K
ha : (Polynomial.C : (a : K) → K[X]) a = f.num
b : K
hb : (Polynomial.C : (a : K) → K[X]) b = f.denom
h :
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.num : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.denom : K⟮X⟯) =
    (C : (a : K) → K⟮X⟯) (a / b)
h₁ :
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Polynomial.C : (a : K) → K[X]) a) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.denom : K⟮X⟯) =
    (C : (a : K) → K⟮X⟯) (a / b)
⊢ f = (C : (a : K) → K⟮X⟯) (a / b)
have h₂ : HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯)
    ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Polynomial.C : (a : K) → K[X]) a) : K⟮X⟯)
    ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Polynomial.C : (a : K) → K[X]) b) : K⟮X⟯) =
  (C : (a : K) → K⟮X⟯) (a / b)
Tactic: rw [← num_div_denom f, ← ha, ← hb, algebraMap_C, algebraMap_C, map_div₀]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : Field K
f : K⟮X⟯
a : K
ha : (Polynomial.C : (a : K) → K[X]) a = f.num
b : K
hb : (Polynomial.C : (a : K) → K[X]) b = f.denom
h :
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.num : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.denom : K⟮X⟯) =
    (C : (a : K) → K⟮X⟯) (a / b)
h₁ :
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Polynomial.C : (a : K) → K[X]) a) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.denom : K⟮X⟯) =
    (C : (a : K) → K⟮X⟯) (a / b)
h₂ :
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Polynomial.C : (a : K) → K[X]) a) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Polynomial.C : (a : K) → K[X]) b) : K⟮X⟯) =
    (C : (a : K) → K⟮X⟯) (a / b)
⊢ f = (C : (a : K) → K⟮X⟯) (a / b)
have h₃ : HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((C : (a : K) → K⟮X⟯) a : K⟮X⟯)
    ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Polynomial.C : (a : K) → K[X]) b) : K⟮X⟯) =
  (C : (a : K) → K⟮X⟯) (a / b)
Tactic: rw [← num_div_denom f, ← ha, ← hb, algebraMap_C, algebraMap_C, map_div₀]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : Field K
f : K⟮X⟯
a : K
ha : (Polynomial.C : (a : K) → K[X]) a = f.num
b : K
hb : (Polynomial.C : (a : K) → K[X]) b = f.denom
h :
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.num : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.denom : K⟮X⟯) =
    (C : (a : K) → K⟮X⟯) (a / b)
h₁ :
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Polynomial.C : (a : K) → K[X]) a) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.denom : K⟮X⟯) =
    (C : (a : K) → K⟮X⟯) (a / b)
h₂ :
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Polynomial.C : (a : K) → K[X]) a) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Polynomial.C : (a : K) → K[X]) b) : K⟮X⟯) =
    (C : (a : K) → K⟮X⟯) (a / b)
h₃ :
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((C : (a : K) → K⟮X⟯) a : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Polynomial.C : (a : K) → K[X]) b) : K⟮X⟯) =
    (C : (a : K) → K⟮X⟯) (a / b)
⊢ f = (C : (a : K) → K⟮X⟯) (a / b)
have h₄ : HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((C : (a : K) → K⟮X⟯) a : K⟮X⟯) ((C : (a : K) → K⟮X⟯) b : K⟮X⟯) =
  (C : (a : K) → K⟮X⟯) (a / b)
Tactic: rw [← num_div_denom f, ← ha, ← hb, algebraMap_C, algebraMap_C, map_div₀]