awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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
S : IntermediateField F K
inst_7 : Algebra.IsAlgebraic.{u, w} F ↥S
inst_8 : IsPurelyInseparable F E
⊢ Algebra.IsAlgebraic.{u, w} F ↥(adjoin F (↑S : Set K))

Tactic:
have : Algebra.IsAlgebraic F (adjoin F (S : Set K)) := by rwa [adjoin_self]
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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
S : IntermediateField F K
inst_7 : Algebra.IsAlgebraic.{u, w} F ↥S
inst_8 : IsPurelyInseparable F E
this : Algebra.IsAlgebraic.{u, w} F ↥(adjoin F (↑S : Set K))
⊢ sepDegree E ↥(adjoin E (↑S : Set K)) = sepDegree F ↥(adjoin F (↑S : Set K))

Tactic:
have := sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable (F := F) E (S : Set K)
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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
S : IntermediateField F K
inst_7 : Algebra.IsAlgebraic.{u, w} F ↥S
inst_8 : IsPurelyInseparable F E
this_1 : Algebra.IsAlgebraic.{u, w} F ↥(adjoin F (↑S : Set K))
this : sepDegree E ↥(adjoin E (↑S : Set K)) = sepDegree F ↥(adjoin F (↑S : Set K))
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : sepDegree E ↥(adjoin E (↑S : Set K)) = sepDegree F ↥S),
    sepDegree E ↥(adjoin E (↑S : Set K)) = sepDegree F ↥S
⊢ sepDegree E ↥(adjoin E (↑S : Set K)) = sepDegree F ↥S

Tactic:
rwa [adjoin_self] at this

Premises used: IntermediateField.adjoin_self
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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
⊢ IsIntegral F x

Tactic:
have hi := IsSeparable.isIntegral hsep
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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
⊢ IsIntegral E x

Tactic:
have hi' : IsIntegral E x := IsIntegral.tower_top hi
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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
⊢ Eq (α := E[X]) (Polynomial.map (algebraMap F E) (minpoly F x)) (minpoly E x)

Tactic:
eq_of_monic_of_dvd_of_natDegree_le (monic hi') ((monic hi).map (algebraMap F E))
    (dvd_map_of_isScalarTower F E x) (le_of_eq ?_)

Premises used: minpoly.monic, Algebra.algebraMap, minpoly.dvd_map_of_isScalarTower, Polynomial.eq_of_monic_of_dvd_of_natDegree_le, le_of_eq, Polynomial.Monic.map
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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
refine : natDegree (Polynomial.map (algebraMap F E) (minpoly F x)) = natDegree (minpoly E x)
⊢ Eq (α := E[X]) (Polynomial.map (algebraMap F E) (minpoly F x)) (minpoly E x)

Tactic:
refine eq_of_monic_of_dvd_of_natDegree_le (monic hi') ((monic hi).map (algebraMap F E))
    (dvd_map_of_isScalarTower F E x) (le_of_eq ?_)

Premises used: minpoly.monic, Algebra.algebraMap, minpoly.dvd_map_of_isScalarTower, Polynomial.eq_of_monic_of_dvd_of_natDegree_le, le_of_eq, Polynomial.Monic.map
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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
⊢ IsSeparable E x

Tactic:
have hsep' := IsSeparable.tower_top E hsep
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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
⊢ Algebra.IsSeparable.{u, w} F ↥F⟮x⟯

Tactic:
haveI := (isSeparable_adjoin_simple_iff_isSeparable _ _).2 hsep
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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 : Algebra.IsSeparable.{u, w} F ↥F⟮x⟯
⊢ Algebra.IsSeparable.{v, w} E ↥E⟮x⟯

Tactic:
haveI := (isSeparable_adjoin_simple_iff_isSeparable _ _).2 hsep'
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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 : Algebra.IsSeparable.{v, w} E ↥E⟮x⟯
⊢ Algebra.IsAlgebraic.{u, w} F ↥F⟮x⟯

Tactic:
have := Algebra.IsSeparable.isAlgebraic F F⟮x⟯
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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⟯) : ℕ)
rw₇ rw₈ :
  Eq (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{w}) → ℕ) (sepDegree F ↥F⟮x⟯) : ℕ)
    ((Cardinal.toNat : (a : Cardinal.{w}) → ℕ) (sepDegree F ↥F⟮x⟯) : ℕ)
⊢ natDegree (Polynomial.map (algebraMap F E) (minpoly 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]

Premises used: IntermediateField.adjoin.finrank, Polynomial.natDegree_map, Field.finSepDegree_eq_finrank_of_isSeparable, IntermediateField.sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable, Field.finSepDegree_eq
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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
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)
⊢ 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'

Premises used: LT.lt.ne', Irreducible.natDegree_pos, Iff.mp, Polynomial.natDegree_pos_iff_degree_pos, IsAlgClosed.exists_aeval_eq_zero
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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)
⊢ 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
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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
rw₁ rw₂ : Eq (α := F[X]) (minpoly F x) (minpoly F x)
⊢ f * (↑this.unit : F[X]) = minpoly F x

Tactic:
rw [IsUnit.unit_spec, minpoly.eq_of_irreducible hirr hx]

Premises used: minpoly.eq_of_irreducible, IsUnit.unit_spec
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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])
⊢ Associated f (minpoly F x)

Tactic:
exact ⟨this.unit, by rw [IsUnit.unit_spec, minpoly.eq_of_irreducible hirr hx]⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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)

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]⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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)
⊢ 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
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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))
⊢ 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)
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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)
rw : Irreducible (M := E[X]) (minpoly E x)
⊢ Irreducible (M := E[X]) (Polynomial.map (algebraMap F E) f)

Tactic:
rw [ha'.irreducible_iff, heq]

Premises used: Associated.irreducible_iff
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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]) (minpoly E x)

Tactic:
minpoly.irreducible (Algebra.IsIntegral.isIntegral x)

Premises used: Algebra.IsIntegral.isIntegral, minpoly.irreducible
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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]) (minpoly E x)

Tactic:
exact minpoly.irreducible (Algebra.IsIntegral.isIntegral x)

Premises used: Algebra.IsIntegral.isIntegral, minpoly.irreducible
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
⊢ Eq (α := K →+* K⟮X⟯) (algebraMap K K⟮X⟯) C

Tactic:
rfl

Premises used: RatFunc.C, rfl
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
a : K
⊢ Eq (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Polynomial.C : (a : K) → K[X]) a) : K⟮X⟯)
    ((C : (a : K) → K⟮X⟯) a : K⟮X⟯)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
⊢ Eq.{u + 1} (α := K →+* K⟮X⟯) (RingHom.comp (algebraMap K[X] K⟮X⟯) Polynomial.C) C

Tactic:
rfl

Premises used: RatFunc.C, rfl
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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
rw₁ 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
⊢ r • x = HMul.hMul (α := K⟮X⟯) ((C : (a : K) → K⟮X⟯) r : K⟮X⟯) x

Tactic:
rw [Algebra.smul_def, algebraMap_eq_C]

Premises used: RatFunc.algebraMap_eq_C, Algebra.smul_def
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
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]))
⊢ Function.Injective.{u + 1, u + 1} (α := K) (β := K⟮X⟯) (⇑C : (a : K) → K⟮X⟯)

Tactic:
rw [← algebraMap_comp_C, RingHom.coe_comp]

Premises used: RingHom.coe_comp, RatFunc.algebraMap_comp_C
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
⊢ 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:
Function.Injective.comp (algebraMap_injective K) (Polynomial.C_injective)

Premises used: Function.Injective.comp, RatFunc.algebraMap_injective, Polynomial.C_injective
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
⊢ 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:
exact Function.Injective.comp (algebraMap_injective K) (Polynomial.C_injective)

Premises used: Function.Injective.comp, RatFunc.algebraMap_injective, Polynomial.C_injective
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
⊢ Eq.{u + 1} (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) Polynomial.X : K⟮X⟯) (X : K⟮X⟯)

Tactic:
rfl

Premises used: RatFunc.X, rfl
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
n : ℕ
a : K
⊢ (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Polynomial.monomial n : (a : K) → K[X]) a) =
    HMul.hMul (α := K⟮X⟯) ((C : (a : K) → K⟮X⟯) a : K⟮X⟯) (HPow.hPow (α := K⟮X⟯) X n)

Tactic:
simp [← Polynomial.C_mul_X_pow_eq_monomial]

Premises used: Polynomial.C_mul_X_pow_eq_monomial
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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⟯)
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⟯)
⊢ 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⟯)

Tactic:
induction p using Polynomial.induction_on'
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
p q : K[X]
h :
  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⟯)
h_1 :
  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:
simp_all
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
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:
simp_all
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
p : K[X]
⊢ (↑p : K⟮X⟯) = (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p

Tactic:
rfl

Premises used: RatFunc.coePolynomial, rfl
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
L : Type u_1
inst_2 : Field L
φ : RingHom.{u, u_1} K[X] L
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ L⁰)
x : K
⊢ Eq.{u_1 + 1} (α := L) ((liftRingHom φ hφ : (a : K⟮X⟯) → L) ((C : (a : K) → K⟮X⟯) x : K⟮X⟯) : L)
    ((φ : (a : K[X]) → L) ((Polynomial.C : (a : K) → K[X]) x : K[X]) : L)

Tactic:
RatFunc.liftRingHom_algebraMap _ _ _

Premises used: RatFunc.liftRingHom_algebraMap
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
L : Type u_1
inst_2 : Field L
φ : RingHom.{u, u_1} K[X] L
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ L⁰)
⊢ Eq.{u_1 + 1} (α := L) ((liftRingHom φ hφ : (a : K⟮X⟯) → L) X : L) ((φ : (a : K[X]) → L) Polynomial.X : L)

Tactic:
RatFunc.liftRingHom_algebraMap _ _ _

Premises used: RatFunc.X, RatFunc.liftRingHom_algebraMap
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u
inst : Field K
c : K
⊢ Eq.{u + 1} (α := K[X]) (num ((C : (a : K) → K⟮X⟯) c)) ((Polynomial.C : (a : K) → K[X]) c)

Tactic:
num_algebraMap _

Premises used: RatFunc.num_algebraMap
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u
inst : Field K
c : K
⊢ Eq.{u + 1} (α := K[X]) (denom ((C : (a : K) → K⟮X⟯) c)) 1

Tactic:
denom_algebraMap _

Premises used: RatFunc.denom_algebraMap
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u
inst : Field K
⊢ Eq.{u + 1} (α := K[X]) (num X) Polynomial.X

Tactic:
num_algebraMap _

Premises used: RatFunc.X, RatFunc.num_algebraMap
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u
inst : Field K
⊢ Eq.{u + 1} (α := K[X]) (denom X) 1

Tactic:
denom_algebraMap _

Premises used: RatFunc.X, RatFunc.denom_algebraMap
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u
inst : Field K
⊢ Ne.{u + 1} (α := K⟮X⟯) X 0

Tactic:
RatFunc.algebraMap_ne_zero Polynomial.X_ne_zero

Premises used: RatFunc.X, RatFunc.algebraMap_ne_zero, Polynomial.X_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u
inst : Field K
c : K
⊢ Polynomial.natDegree.{u} (R := K) (num ((C : (a : K) → K⟮X⟯) c)) = 0 ∧
    Polynomial.natDegree.{u} (R := K) (denom ((C : (a : K) → K⟮X⟯) c)) = 0

Tactic:
simp
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u
inst : Field K
f : K⟮X⟯
refine : f.num.natDegree = 0 ∧ f.denom.natDegree = 0 → ∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
⊢ (∃ (c : K), f = (C : (a : K) → K⟮X⟯) c) ↔ f.num.natDegree = 0 ∧ f.denom.natDegree = 0

Tactic:
refine ⟨by rintro ⟨c, rfl⟩; simp, ?_⟩
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u
inst : Field K
f : K⟮X⟯
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
⊢ f.num.natDegree = 0 ∧ f.denom.natDegree = 0 → ∃ (c : K), f = (C : (a : K) → K⟮X⟯) c

Tactic:
rw [Polynomial.natDegree_eq_zero, Polynomial.natDegree_eq_zero]

Premises used: Polynomial.natDegree_eq_zero
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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 : f = (C : (a : K) → K⟮X⟯) (a / b)
⊢ ∃ (c : K), f = (C : (a : K) → K⟮X⟯) c

Tactic:
use a / b