awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
f_ne_zero : f ≠ 0
H : Eq (α := K⟮X⟯) (↑(coeff (f.minpolyX ↥K⟮f⟯) f.num.natDegree) : K⟮X⟯) (↑0 : K⟮X⟯)
⊢ HSub.hSub (α := K⟮X⟯) ((C : (a : K) → K⟮X⟯) f.num.leadingCoeff : K⟮X⟯)
      (HMul.hMul (β := K⟮X⟯) f ((C : (a : K) → K⟮X⟯) (f.denom.coeff f.num.natDegree) : K⟮X⟯)) =
    0

Tactic:
simp only [coeff_sub, coeff_map, coeff_natDegree, coeff_C_mul, AddSubgroupClass.coe_sub,
    SubalgebraClass.coe_algebraMap, algebraMap_eq_C, MulMemClass.coe_mul, coe_algebraMap,
    ZeroMemClass.coe_zero] at H

Premises used: AddSubgroupClass.coe_sub, Polynomial.coeff_map, Polynomial.coeff_natDegree, Polynomial.coeff_C_mul, RatFunc.algebraMap_eq_C, ZeroMemClass.coe_zero, Polynomial.coeff_sub, SubalgebraClass.coe_algebraMap, MulMemClass.coe_mul, IntermediateField.algebraAdjoinAdjoin.coe_algebraMap
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
f_ne_zero : f ≠ 0
H :
  HSub.hSub (α := K⟮X⟯) ((C : (a : K) → K⟮X⟯) f.num.leadingCoeff : K⟮X⟯)
      (HMul.hMul (β := K⟮X⟯) f ((C : (a : K) → K⟮X⟯) (f.denom.coeff f.num.natDegree) : K⟮X⟯)) =
    0
⊢ f = (C : (a : K) → K⟮X⟯) (f.denom.coeff f.num.natDegree / f.num.leadingCoeff)⁻¹

Tactic:
rw [sub_eq_zero, ← mul_right_inj' (inv_ne_zero f_ne_zero), ← mul_assoc, inv_mul_cancel₀ f_ne_zero,
    one_mul, ← eq_div_iff <| (_root_.map_ne_zero C).mpr <| Polynomial.leadingCoeff_ne_zero.mpr
    (num_ne_zero f_ne_zero), ← inv_inj, inv_inv, ← map_div₀, ← map_inv₀] at H

Premises used: Iff.mpr, sub_eq_zero, RatFunc.C, mul_assoc, RatFunc.num_ne_zero, map_inv₀, inv_inj, map_div₀, Polynomial.leadingCoeff_ne_zero, inv_inv, inv_ne_zero, map_ne_zero, mul_right_inj', eq_div_iff, inv_mul_cancel₀, one_mul
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
f_ne_zero : f ≠ 0
H : f = (C : (a : K) → K⟮X⟯) (f.denom.coeff f.num.natDegree / f.num.leadingCoeff)⁻¹
⊢ False

Tactic:
hf ⟨_, H⟩

Premises used: Exists.intro
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
f_ne_zero : f ≠ 0
H : f = (C : (a : K) → K⟮X⟯) (f.denom.coeff f.num.natDegree / f.num.leadingCoeff)⁻¹
⊢ False

Tactic:
exact hf ⟨_, H⟩

Premises used: Exists.intro
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
pos :
  ∀ (hf : ∃ (c : K), f = (C : (a : K) → K⟮X⟯) c),
    natDegree (R := ↥K⟮f⟯) (f.minpolyX ↥K⟮f⟯) = max f.num.natDegree f.denom.natDegree
neg :
  ∀ (hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c),
    natDegree (R := ↥K⟮f⟯) (f.minpolyX ↥K⟮f⟯) = max f.num.natDegree f.denom.natDegree
⊢ natDegree (R := ↥K⟮f⟯) (f.minpolyX ↥K⟮f⟯) = max f.num.natDegree f.denom.natDegree

Tactic:
by_cases hf : ∃ c, f = C c
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
pos :
  ∀ (c : K),
    natDegree.{u_1} (R := ↥K⟮((C : (a : K) → K⟮X⟯) c : K⟮X⟯)⟯)
        (minpolyX (K := K) ((C : (a : K) → K⟮X⟯) c) ↥K⟮((C : (a : K) → K⟮X⟯) c : K⟮X⟯)⟯) =
      max (natDegree.{u_1} (R := K) (num ((C : (a : K) → K⟮X⟯) c)))
        (natDegree.{u_1} (R := K) (denom ((C : (a : K) → K⟮X⟯) c)))
⊢ natDegree (R := ↥K⟮f⟯) (f.minpolyX ↥K⟮f⟯) = max f.num.natDegree f.denom.natDegree

Tactic:
obtain ⟨c, rfl⟩ := hf

Premises used: rfl
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
c : K
⊢ natDegree.{u_1} (R := ↥K⟮((C : (a : K) → K⟮X⟯) c : K⟮X⟯)⟯)
      (minpolyX (K := K) ((C : (a : K) → K⟮X⟯) c) ↥K⟮((C : (a : K) → K⟮X⟯) c : K⟮X⟯)⟯) =
    max (natDegree.{u_1} (R := K) (num ((C : (a : K) → K⟮X⟯) c)))
      (natDegree.{u_1} (R := K) (denom ((C : (a : K) → K⟮X⟯) c)))

Tactic:
simp
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
neg : natDegree (R := ↥K⟮f⟯) (f.minpolyX ↥K⟮f⟯) ≤ max f.num.natDegree f.denom.natDegree
neg₁ : max f.num.natDegree f.denom.natDegree ≤ natDegree (R := ↥K⟮f⟯) (f.minpolyX ↥K⟮f⟯)
⊢ natDegree (R := ↥K⟮f⟯) (f.minpolyX ↥K⟮f⟯) = max f.num.natDegree f.denom.natDegree

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
⊢ natDegree (R := ↥K⟮f⟯) (f.minpolyX ↥K⟮f⟯) ≤
    max (natDegree (R := ↥K⟮f⟯) (Polynomial.map (algebraMap K ↥K⟮f⟯) f.num))
      (HMul.hMul (α := (↥K⟮f⟯)[X]) (β := (↥K⟮f⟯)[X])
          ((Polynomial.C : (a : ↥K⟮f⟯) → (↥K⟮f⟯)[X])
              ((algebraMap ↥K[f] ↥K⟮f⟯ : (a : ↥K[f]) → ↥K⟮f⟯)
                (Subtype.mk (p := fun (x : K⟮X⟯) ↦ Membership.mem (γ := Subalgebra K K⟮X⟯) K[f] x) f ⋯)) :
            (↥K⟮f⟯)[X])
          (Polynomial.map (algebraMap K ↥K⟮f⟯) f.denom)).natDegree

Tactic:
have : (f.minpolyX K⟮f⟯).natDegree ≤ _ := natDegree_sub_le _ _
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
this :
  natDegree (R := ↥K⟮f⟯) (f.minpolyX ↥K⟮f⟯) ≤
    max f.num.natDegree
      (HMul.hMul (α := (↥K⟮f⟯)[X]) (β := (↥K⟮f⟯)[X])
          ((Polynomial.C : (a : ↥K⟮f⟯) → (↥K⟮f⟯)[X])
              ((algebraMap ↥K[f] ↥K⟮f⟯ : (a : ↥K[f]) → ↥K⟮f⟯)
                (Subtype.mk (p := fun (x : K⟮X⟯) ↦ Membership.mem (γ := Subalgebra K K⟮X⟯) K[f] x) f ⋯)) :
            (↥K⟮f⟯)[X])
          (Polynomial.map (algebraMap K ↥K⟮f⟯) f.denom)).natDegree
H :
  Eq (α := ↥K⟮f⟯)
    ((algebraMap ↥K[f] ↥K⟮f⟯ : (a : ↥K[f]) → ↥K⟮f⟯)
        (Subtype.mk (p := fun (x : K⟮X⟯) ↦ Membership.mem (γ := Subalgebra K K⟮X⟯) K[f] x) f ⋯) :
      ↥K⟮f⟯)
    (0 : ↥K⟮f⟯)
⊢ f = (C : (a : K) → K⟮X⟯) 0

Tactic:
simpa [map_zero] using congr($(H).val)

Premises used: map_zero
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
this :
  natDegree (R := ↥K⟮f⟯) (f.minpolyX ↥K⟮f⟯) ≤
    max (natDegree (R := ↥K⟮f⟯) (Polynomial.map (algebraMap K ↥K⟮f⟯) f.num))
      (HMul.hMul (α := (↥K⟮f⟯)[X]) (β := (↥K⟮f⟯)[X])
          ((Polynomial.C : (a : ↥K⟮f⟯) → (↥K⟮f⟯)[X])
              ((algebraMap ↥K[f] ↥K⟮f⟯ : (a : ↥K[f]) → ↥K⟮f⟯)
                (Subtype.mk (p := fun (x : K⟮X⟯) ↦ Membership.mem (γ := Subalgebra K K⟮X⟯) K[f] x) f ⋯)) :
            (↥K⟮f⟯)[X])
          (Polynomial.map (algebraMap K ↥K⟮f⟯) f.denom)).natDegree
⊢ natDegree (R := ↥K⟮f⟯) (f.minpolyX ↥K⟮f⟯) ≤ max f.num.natDegree f.denom.natDegree

Tactic:
rw [natDegree_map, natDegree_C_mul fun H ↦ hf ⟨0, by simpa [map_zero] using congr($(H).val)⟩,
      natDegree_map] at this

Premises used: Polynomial.natDegree_map, Polynomial.natDegree_C_mul, Exists.intro, OfNat.ofNat
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
this : natDegree (R := ↥K⟮f⟯) (f.minpolyX ↥K⟮f⟯) ≤ max f.num.natDegree f.denom.natDegree
⊢ natDegree (R := ↥K⟮f⟯) (f.minpolyX ↥K⟮f⟯) ≤ max f.num.natDegree f.denom.natDegree

Tactic:
this
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
this : natDegree (R := ↥K⟮f⟯) (f.minpolyX ↥K⟮f⟯) ≤ max f.num.natDegree f.denom.natDegree
⊢ natDegree (R := ↥K⟮f⟯) (f.minpolyX ↥K⟮f⟯) ≤ max f.num.natDegree f.denom.natDegree

Tactic:
exact this
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
⊢ max f.num.natDegree f.denom.natDegree ≤ natDegree (R := ↥K⟮f⟯) (f.minpolyX ↥K⟮f⟯)

Tactic:
max_le (natDegree_num_le_natDegree_minpolyX f hf) <| le_natDegree_of_ne_zero
      fun H ↦ hf (f.eq_C_of_minpolyX_coeff_eq_zero congr($(H).val))

Premises used: congrArg, RatFunc.eq_C_of_minpolyX_coeff_eq_zero, id, RatFunc.natDegree_num_le_natDegree_minpolyX, max_le, Polynomial.le_natDegree_of_ne_zero, Subtype.val
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
⊢ max f.num.natDegree f.denom.natDegree ≤ natDegree (R := ↥K⟮f⟯) (f.minpolyX ↥K⟮f⟯)

Tactic:
exact max_le (natDegree_num_le_natDegree_minpolyX f hf) <| le_natDegree_of_ne_zero
      fun H ↦ hf (f.eq_C_of_minpolyX_coeff_eq_zero congr($(H).val))

Premises used: RatFunc.natDegree_num_le_natDegree_minpolyX, max_le
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
H : IsAlgebraic K f
⊢ Algebra.IsAlgebraic K ↥K⟮f⟯

Tactic:
have := isAlgebraic_adjoin_simple H.isIntegral
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
H : IsAlgebraic K f
this : Algebra.IsAlgebraic K ↥K⟮f⟯
⊢ Algebra.Transcendental K K⟮X⟯

Tactic:
infer_instance
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
H : IsAlgebraic K f
this : Algebra.IsAlgebraic K ↥K⟮f⟯
⊢ Algebra.Transcendental K K⟮X⟯

Tactic:
have tr : Algebra.Transcendental K K⟮X⟯ := by infer_instance
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
H : IsAlgebraic K f
this : Algebra.IsAlgebraic K ↥K⟮f⟯
tr : Algebra.Transcendental K K⟮X⟯
⊢ ¬Algebra.IsAlgebraic K K⟮X⟯

Tactic:
rw [Algebra.transcendental_iff_not_isAlgebraic] at tr

Premises used: Algebra.transcendental_iff_not_isAlgebraic
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
H : IsAlgebraic K f
this : Algebra.IsAlgebraic K ↥K⟮f⟯
tr : ¬Algebra.IsAlgebraic K K⟮X⟯
⊢ False

Tactic:
tr <| Algebra.IsAlgebraic.trans _ _ _ (alg := f.isAlgebraic_adjoin_simple_X' hf)

Premises used: Algebra.IsAlgebraic.trans
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
H : IsAlgebraic K f
this : Algebra.IsAlgebraic K ↥K⟮f⟯
tr : ¬Algebra.IsAlgebraic K K⟮X⟯
⊢ False

Tactic:
exact tr <| Algebra.IsAlgebraic.trans _ _ _ (alg := f.isAlgebraic_adjoin_simple_X' hf)

Premises used: Algebra.IsAlgebraic.trans
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
e : K[X] ≃ₐ[K] ↥K[f] := Polynomial.algEquivOfTranscendental K f ⋯
φ : K[X][X] :=
  Polynomial.map (algebraMap K K[X]) f.num -
    HMul.hMul (α := K[X][X]) (β := K[X][X]) ((Polynomial.C : (a : K[X]) → K[X][X]) Polynomial.X : K[X][X])
      (Polynomial.map (algebraMap K K[X]) f.denom)
simp :
  Polynomial.map
        (RingHom.comp
          (↑(aeval (Subtype.mk (p := fun (x : K⟮X⟯) ↦ Membership.mem (γ := Subalgebra K K⟮X⟯) K[f] x) f ⋯)) :
            K[X] →+* ↥K[f])
          Polynomial.C)
        f.num -
      HMul.hMul (α := (↥K[f])[X]) (β := (↥K[f])[X])
        ((Polynomial.C : (a : ↥K[f]) → (↥K[f])[X])
            (Subtype.mk (p := fun (x : K⟮X⟯) ↦ Membership.mem (γ := Subalgebra K K⟮X⟯) K[f] x) f ⋯) :
          (↥K[f])[X])
        (Polynomial.map
          (RingHom.comp
            (↑(aeval (Subtype.mk (p := fun (x : K⟮X⟯) ↦ Membership.mem (γ := Subalgebra K K⟮X⟯) K[f] x) f ⋯)) :
              K[X] →+* ↥K[f])
            Polynomial.C)
          f.denom) =
    f.minpolyX ↥K[f]
⊢ Eq (α := (↥K[f])[X]) ((mapEquiv e.toRingEquiv : (a : K[X][X]) → (↥K[f])[X]) φ : (↥K[f])[X])
    (f.minpolyX ↥K[f] : (↥K[f])[X])

Tactic:
simp only [algebraMap_eq, map_sub, mapEquiv_apply,
      AlgEquiv.toRingEquiv_toRingHom, algEquivOfTranscendental_coe, Polynomial.map_map, map_mul,
      map_C, RingHom.coe_coe, aeval_X, e, φ]

Premises used: AlgEquiv.toRingEquiv_toRingHom, map_sub, RingHom.coe_coe, Polynomial.algEquivOfTranscendental_coe, map_mul, Polynomial.map_C, Polynomial.map_map, Polynomial.mapEquiv_apply, Polynomial.aeval_X, Polynomial.algebraMap_eq
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
e : K[X] ≃ₐ[K] ↥K[f] := Polynomial.algEquivOfTranscendental K f ⋯
φ : K[X][X] :=
  Polynomial.map (algebraMap K K[X]) f.num -
    HMul.hMul (α := K[X][X]) (β := K[X][X]) ((Polynomial.C : (a : K[X]) → K[X][X]) Polynomial.X : K[X][X])
      (Polynomial.map (algebraMap K K[X]) f.denom)
e_a :
  Eq (α := K →+* ↥K[f])
    (RingHom.comp
      (↑(aeval (Subtype.mk (p := fun (x : K⟮X⟯) ↦ Membership.mem (γ := Subalgebra K K⟮X⟯) K[f] x) f ⋯)) :
        K[X] →+* ↥K[f])
      Polynomial.C)
    (algebraMap K ↥K[f])
e_a₁ :
  Eq (α := (↥K[f])[X])
    (Polynomial.map
      (RingHom.comp
        (↑(aeval (Subtype.mk (p := fun (x : K⟮X⟯) ↦ Membership.mem (γ := Subalgebra K K⟮X⟯) K[f] x) f ⋯)) :
          K[X] →+* ↥K[f])
        Polynomial.C)
      f.denom)
    (Polynomial.map (algebraMap K ↥K[f]) f.denom)
⊢ Polynomial.map
        (RingHom.comp
          (↑(aeval (Subtype.mk (p := fun (x : K⟮X⟯) ↦ Membership.mem (γ := Subalgebra K K⟮X⟯) K[f] x) f ⋯)) :
            K[X] →+* ↥K[f])
          Polynomial.C)
        f.num -
      HMul.hMul (α := (↥K[f])[X]) (β := (↥K[f])[X])
        ((Polynomial.C : (a : ↥K[f]) → (↥K[f])[X])
            (Subtype.mk (p := fun (x : K⟮X⟯) ↦ Membership.mem (γ := Subalgebra K K⟮X⟯) K[f] x) f ⋯) :
          (↥K[f])[X])
        (Polynomial.map
          (RingHom.comp
            (↑(aeval (Subtype.mk (p := fun (x : K⟮X⟯) ↦ Membership.mem (γ := Subalgebra K K⟮X⟯) K[f] x) f ⋯)) :
              K[X] →+* ↥K[f])
            Polynomial.C)
          f.denom) =
    f.minpolyX ↥K[f]

Tactic:
congr 2
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
e : K[X] ≃ₐ[K] ↥K[f] := Polynomial.algEquivOfTranscendental K f ⋯
φ : K[X][X] :=
  Polynomial.map (algebraMap K K[X]) f.num -
    HMul.hMul (α := K[X][X]) (β := K[X][X]) ((Polynomial.C : (a : K[X]) → K[X][X]) Polynomial.X : K[X][X])
      (Polynomial.map (algebraMap K K[X]) f.denom)
e_a :
  ∀ (x : K),
    Eq.{u_1 + 1} (α := K⟮X⟯)
      (↑((RingHom.comp
                (↑(aeval (Subtype.mk (p := fun (x : K⟮X⟯) ↦ Membership.mem (γ := Subalgebra K K⟮X⟯) K[f] x) f ⋯)) :
                  K[X] →+* ↥K[f])
                Polynomial.C :
              (a : K) → ↥K[f])
            x) :
        K⟮X⟯)
      (↑((algebraMap K ↥K[f] : (a : K) → ↥K[f]) x) : K⟮X⟯)
⊢ Eq (α := K →+* ↥K[f])
    (RingHom.comp
      (↑(aeval (Subtype.mk (p := fun (x : K⟮X⟯) ↦ Membership.mem (γ := Subalgebra K K⟮X⟯) K[f] x) f ⋯)) :
        K[X] →+* ↥K[f])
      Polynomial.C)
    (algebraMap K ↥K[f])

Tactic:
ext
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
e : K[X] ≃ₐ[K] ↥K[f] := Polynomial.algEquivOfTranscendental K f ⋯
φ : K[X][X] :=
  Polynomial.map (algebraMap K K[X]) f.num -
    HMul.hMul (α := K[X][X]) (β := K[X][X]) ((Polynomial.C : (a : K[X]) → K[X][X]) Polynomial.X : K[X][X])
      (Polynomial.map (algebraMap K K[X]) f.denom)
e_a :
  ∀ (n : ℕ),
    (↑(coeff
            (Polynomial.map
              (RingHom.comp
                (↑(aeval (Subtype.mk (p := fun (x : K⟮X⟯) ↦ Membership.mem (γ := Subalgebra K K⟮X⟯) K[f] x) f ⋯)) :
                  K[X] →+* ↥K[f])
                Polynomial.C)
              f.denom)
            n) :
        K⟮X⟯) =
      (↑(coeff (Polynomial.map (algebraMap K ↥K[f]) f.denom) n) : K⟮X⟯)
⊢ Eq (α := (↥K[f])[X])
    (Polynomial.map
      (RingHom.comp
        (↑(aeval (Subtype.mk (p := fun (x : K⟮X⟯) ↦ Membership.mem (γ := Subalgebra K K⟮X⟯) K[f] x) f ⋯)) :
          K[X] →+* ↥K[f])
        Polynomial.C)
      f.denom)
    (Polynomial.map (algebraMap K ↥K[f]) f.denom)

Tactic:
ext
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
e : K[X] ≃ₐ[K] ↥K[f] := Polynomial.algEquivOfTranscendental K f ⋯
φ : K[X][X] :=
  Polynomial.map (algebraMap K K[X]) f.num -
    HMul.hMul (α := K[X][X]) (β := K[X][X]) ((Polynomial.C : (a : K[X]) → K[X][X]) Polynomial.X : K[X][X])
      (Polynomial.map (algebraMap K K[X]) f.denom)
x : K
⊢ Eq.{u_1 + 1} (α := K⟮X⟯)
    (↑((RingHom.comp
              (↑(aeval (Subtype.mk (p := fun (x : K⟮X⟯) ↦ Membership.mem (γ := Subalgebra K K⟮X⟯) K[f] x) f ⋯)) :
                K[X] →+* ↥K[f])
              Polynomial.C :
            (a : K) → ↥K[f])
          x) :
      K⟮X⟯)
    (↑((algebraMap K ↥K[f] : (a : K) → ↥K[f]) x) : K⟮X⟯)

Tactic:
simp
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
e : K[X] ≃ₐ[K] ↥K[f] := Polynomial.algEquivOfTranscendental K f ⋯
φ : K[X][X] :=
  Polynomial.map (algebraMap K K[X]) f.num -
    HMul.hMul (α := K[X][X]) (β := K[X][X]) ((Polynomial.C : (a : K[X]) → K[X][X]) Polynomial.X : K[X][X])
      (Polynomial.map (algebraMap K K[X]) f.denom)
n : ℕ
⊢ (↑(coeff
          (Polynomial.map
            (RingHom.comp
              (↑(aeval (Subtype.mk (p := fun (x : K⟮X⟯) ↦ Membership.mem (γ := Subalgebra K K⟮X⟯) K[f] x) f ⋯)) :
                K[X] →+* ↥K[f])
              Polynomial.C)
            f.denom)
          n) :
      K⟮X⟯) =
    (↑(coeff (Polynomial.map (algebraMap K ↥K[f]) f.denom) n) : K⟮X⟯)

Tactic:
simp
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
e : K[X] ≃ₐ[K] ↥K[f] := Polynomial.algEquivOfTranscendental K f ⋯
φ : K[X][X] :=
  Polynomial.map (algebraMap K K[X]) f.num -
    HMul.hMul (α := K[X][X]) (β := K[X][X]) ((Polynomial.C : (a : K[X]) → K[X][X]) Polynomial.X : K[X][X])
      (Polynomial.map (algebraMap K K[X]) f.denom)
⊢ Eq (α := (↥K[f])[X]) ((mapEquiv e.toRingEquiv : (a : K[X][X]) → (↥K[f])[X]) φ : (↥K[f])[X])
    (f.minpolyX ↥K[f] : (↥K[f])[X])

Tactic:
have φ_map : φ.mapEquiv e.toRingEquiv = (f.minpolyX K[f]) := by
    simp only [algebraMap_eq, map_sub, mapEquiv_apply,
      AlgEquiv.toRingEquiv_toRingHom, algEquivOfTranscendental_coe, Polynomial.map_map, map_mul,
      map_C, RingHom.coe_coe, aeval_X, e, φ]
    congr 2 <;> ext <;> simp
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
e : K[X] ≃ₐ[K] ↥K[f] := Polynomial.algEquivOfTranscendental K f ⋯
φ : K[X][X] :=
  Polynomial.map (algebraMap K K[X]) f.num -
    HMul.hMul (α := K[X][X]) (β := K[X][X]) ((Polynomial.C : (a : K[X]) → K[X][X]) Polynomial.X : K[X][X])
      (Polynomial.map (algebraMap K K[X]) f.denom)
φ_map :
  Eq (α := (↥K[f])[X]) ((mapEquiv e.toRingEquiv : (a : K[X][X]) → (↥K[f])[X]) φ : (↥K[f])[X])
    (f.minpolyX ↥K[f] : (↥K[f])[X])
rw : Irreducible φ
⊢ Irreducible (M := (↥K[f])[X]) (f.minpolyX ↥K[f])

Tactic:
rw [← φ_map, MulEquiv.irreducible_iff]

Premises used: MulEquiv.irreducible_iff
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
e : K[X] ≃ₐ[K] ↥K[f] := Polynomial.algEquivOfTranscendental K f ⋯
φ : K[X][X] :=
  Polynomial.map (algebraMap K K[X]) f.num -
    HMul.hMul (α := K[X][X]) (β := K[X][X]) ((Polynomial.C : (a : K[X]) → K[X][X]) Polynomial.X : K[X][X])
      (Polynomial.map (algebraMap K K[X]) f.denom)
φ_map :
  Eq (α := (↥K[f])[X]) ((mapEquiv e.toRingEquiv : (a : K[X][X]) → (↥K[f])[X]) φ : (↥K[f])[X])
    (f.minpolyX ↥K[f] : (↥K[f])[X])
simp :
  φ =
    Polynomial.eval Polynomial.X
      (((aeval ((Polynomial.C : (a : K[X][X]) → K[X][X][X]) ((Polynomial.C : (a : K[X]) → K[X][X]) Polynomial.X)) :
            K[X][X] →ₐ[K[X]] K[X][X][X]) :
          (a : K[X][X]) → K[X][X][X])
        (HSub.hSub (α := K[X][X]) ((Polynomial.C : (a : K[X]) → K[X][X]) f.num : K[X][X])
          (HMul.hMul (α := K[X][X]) (β := K[X][X]) ((Polynomial.C : (a : K[X]) → K[X][X]) f.denom : K[X][X])
            Polynomial.X)))
⊢ φ =
    (Bivariate.swap : (a : K[X][X]) → K[X][X])
      (HSub.hSub (α := K[X][X]) ((Polynomial.C : (a : K[X]) → K[X][X]) f.num : K[X][X])
        (HMul.hMul (α := K[X][X]) (β := K[X][X]) Polynomial.X
          ((Polynomial.C : (a : K[X]) → K[X][X]) f.denom : K[X][X])))

Tactic:
simp only [X_mul_C, Bivariate.swap_apply, aevalAeval, aevalAevalEquiv, Equiv.coe_fn_mk,
      AlgHom.coe_comp, AlgHom.coe_restrictScalars', coe_aeval_eq_eval, Function.comp_apply,
      aeval_sub, aeval_C, algebraMap_def, coe_mapRingHom, map_mul, aeval_X, eval_sub,
      eval_map_algebraMap, Polynomial.eval_mul, Polynomial.eval_C]

Premises used: Polynomial.eval_C, Polynomial.aevalAevalEquiv, Polynomial.Bivariate.swap_apply, Polynomial.X_mul_C, Polynomial.algebraMap_def, Polynomial.eval_mul, Polynomial.aevalAeval, map_mul, AlgHom.coe_comp, AlgHom.coe_restrictScalars', Polynomial.coe_mapRingHom, Polynomial.aeval_C, Equiv.coe_fn_mk, Polynomial.eval_map_algebraMap, Function.comp_apply, Polynomial.coe_aeval_eq_eval, Polynomial.eval_sub, Polynomial.aeval_sub, Polynomial.aeval_X
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
e : K[X] ≃ₐ[K] ↥K[f] := Polynomial.algEquivOfTranscendental K f ⋯
φ : K[X][X] :=
  Polynomial.map (algebraMap K K[X]) f.num -
    HMul.hMul (α := K[X][X]) (β := K[X][X]) ((Polynomial.C : (a : K[X]) → K[X][X]) Polynomial.X : K[X][X])
      (Polynomial.map (algebraMap K K[X]) f.denom)
φ_map :
  Eq (α := (↥K[f])[X]) ((mapEquiv e.toRingEquiv : (a : K[X][X]) → (↥K[f])[X]) φ : (↥K[f])[X])
    (f.minpolyX ↥K[f] : (↥K[f])[X])
rw :
  φ =
    Polynomial.eval Polynomial.X
      (((aeval ((Polynomial.C : (a : K[X][X]) → K[X][X][X]) ((Polynomial.C : (a : K[X]) → K[X][X]) Polynomial.X)) :
            K[X][X] →ₐ[K[X]] K[X][X][X]) :
          (a : K[X][X]) → K[X][X][X])
        (HSub.hSub (α := K[X][X]) ((Polynomial.C : (a : K[X]) → K[X][X]) f.num : K[X][X])
          (HMul.hMul (α := K[X][X]) (β := K[X][X]) Polynomial.X
            ((Polynomial.C : (a : K[X]) → K[X][X]) f.denom : K[X][X]))))
⊢ φ =
    Polynomial.eval Polynomial.X
      (((aeval ((Polynomial.C : (a : K[X][X]) → K[X][X][X]) ((Polynomial.C : (a : K[X]) → K[X][X]) Polynomial.X)) :
            K[X][X] →ₐ[K[X]] K[X][X][X]) :
          (a : K[X][X]) → K[X][X][X])
        (HSub.hSub (α := K[X][X]) ((Polynomial.C : (a : K[X]) → K[X][X]) f.num : K[X][X])
          (HMul.hMul (α := K[X][X]) (β := K[X][X]) ((Polynomial.C : (a : K[X]) → K[X][X]) f.denom : K[X][X])
            Polynomial.X)))

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
e : K[X] ≃ₐ[K] ↥K[f] := Polynomial.algEquivOfTranscendental K f ⋯
φ : K[X][X] :=
  Polynomial.map (algebraMap K K[X]) f.num -
    HMul.hMul (α := K[X][X]) (β := K[X][X]) ((Polynomial.C : (a : K[X]) → K[X][X]) Polynomial.X : K[X][X])
      (Polynomial.map (algebraMap K K[X]) f.denom)
φ_map :
  Eq (α := (↥K[f])[X]) ((mapEquiv e.toRingEquiv : (a : K[X][X]) → (↥K[f])[X]) φ : (↥K[f])[X])
    (f.minpolyX ↥K[f] : (↥K[f])[X])
⊢ φ =
    (Bivariate.swap : (a : K[X][X]) → K[X][X])
      (HSub.hSub (α := K[X][X]) ((Polynomial.C : (a : K[X]) → K[X][X]) f.num : K[X][X])
        (HMul.hMul (α := K[X][X]) (β := K[X][X]) Polynomial.X
          ((Polynomial.C : (a : K[X]) → K[X][X]) f.denom : K[X][X])))

Tactic:
have : φ = Bivariate.swap
      (Polynomial.C f.num - Polynomial.X * Polynomial.C f.denom) := by
    simp only [X_mul_C, Bivariate.swap_apply, aevalAeval, aevalAevalEquiv, Equiv.coe_fn_mk,
      AlgHom.coe_comp, AlgHom.coe_restrictScalars', coe_aeval_eq_eval, Function.comp_apply,
      aeval_sub, aeval_C, algebraMap_def, coe_mapRingHom, map_mul, aeval_X, eval_sub,
      eval_map_algebraMap, Polynomial.eval_mul, Polynomial.eval_C]
    rw [mul_comm]
    rfl