awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
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
⊢ natDegree (R := ↥K⟮f⟯) (f.minpolyX ↥K⟮f⟯) = max f.num.natDegree f.denom.natDegree
have 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
Tactic: by_cases hf : ∃ c, f = C c
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
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 f.num.natDegree f.denom.natDegree
have 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)))
Tactic: obtain ⟨c, rfl⟩ := hf
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
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 f.num.natDegree f.denom.natDegree
have neg : natDegree (R := ↥K⟮f⟯) (f.minpolyX ↥K⟮f⟯) ≤ max f.num.natDegree f.denom.natDegree
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
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
⊢ natDegree (R := ↥K⟮f⟯) (f.minpolyX ↥K⟮f⟯) = max f.num.natDegree f.denom.natDegree
have neg₁ : max f.num.natDegree f.denom.natDegree ≤ natDegree (R := ↥K⟮f⟯) (f.minpolyX ↥K⟮f⟯)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (hypothesis)
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 f.num.natDegree f.denom.natDegree
have 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 sorry)) :
          (↥K⟮f⟯)[X])
        (Polynomial.map (algebraMap K ↥K⟮f⟯) f.denom)).natDegree
Tactic: have : (f.minpolyX K⟮f⟯).natDegree ≤ _ := natDegree_sub_le _ _
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (hypothesis)
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
⊢ False
have this : Algebra.IsAlgebraic K ↥K⟮f⟯
Tactic: have := isAlgebraic_adjoin_simple H.isIntegral
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (hypothesis)
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⟯
⊢ False
have tr : Algebra.Transcendental K K⟮X⟯
Tactic: have tr : Algebra.Transcendental K K⟮X⟯ := by infer_instance
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (hypothesis)
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⟯
⊢ False
have tr₁ : ¬Algebra.IsAlgebraic K K⟮X⟯
Tactic: rw [Algebra.transcendental_iff_not_isAlgebraic] at tr
Cleared hypotheses: tr
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
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])
have simp : Polynomial.map
      (RingHom.comp
        (↑(aeval (Subtype.mk (p := fun (x : K⟮X⟯) ↦ Membership.mem (γ := Subalgebra K K⟮X⟯) K[f] x) f sorry)) :
          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 sorry) :
        (↥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 sorry)) :
            K[X] →+* ↥K[f])
          Polynomial.C)
        f.denom) =
  f.minpolyX ↥K[f]
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, φ]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
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)
⊢ 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]
have 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 sorry)) : K[X] →+* ↥K[f])
    Polynomial.C)
  (algebraMap K ↥K[f])
Tactic: congr 2
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
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])
⊢ 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]
have 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 sorry)) :
        K[X] →+* ↥K[f])
      Polynomial.C)
    f.denom)
  (Polynomial.map (algebraMap K ↥K[f]) f.denom)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
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 →+* ↥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])
have 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 sorry)) :
                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: ext
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
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])
    (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)
have 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 sorry)) :
                K[X] →+* ↥K[f])
              Polynomial.C)
            f.denom)
          n) :
      K⟮X⟯) =
    (↑(coeff (Polynomial.map (algebraMap K ↥K[f]) f.denom) n) : K⟮X⟯)
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (hypothesis)
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)
⊢ Irreducible (M := (↥K[f])[X]) (f.minpolyX ↥K[f])
have φ_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])
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
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
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])
⊢ Irreducible (M := (↥K[f])[X]) (f.minpolyX ↥K[f])
have rw : Irreducible φ
Tactic: rw [← φ_map, MulEquiv.irreducible_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
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])))
have 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)))
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]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
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])
⊢ φ =
    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)))
have 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]))))
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (hypothesis)
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])
⊢ Irreducible φ
have this : φ =
  (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
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
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])
this :
  φ =
    (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])))
⊢ Irreducible φ
have rw : Irreducible
  (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: rw [this, MulEquiv.irreducible_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
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])
this :
  φ =
    (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])))
⊢ Irreducible
    (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])))
have h : 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])) =
  HAdd.hAdd (β := 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)
    ((Polynomial.C : (a : K[X]) → K[X][X]) f.num : K[X][X])
Tactic: convert!
    irreducible_C_mul_X_add_C (neg_ne_zero.mpr f.denom_ne_zero)
      ((IsCoprime.neg_right_iff _ _).mpr f.isCoprime_num_denom).symm.isRelPrime using 1
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
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])
this :
  φ =
    (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])))
⊢ 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])) =
    HAdd.hAdd (β := 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)
      ((Polynomial.C : (a : K[X]) → K[X][X]) f.num : K[X][X])
have h : 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) =
  HAdd.hAdd (α := 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 [add_comm, X_mul_C, map_neg, neg_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (hypothesis)
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
⊢ Irreducible (M := (↥K⟮f⟯)[X]) (f.minpolyX ↥K⟮f⟯)
have this : UniqueFactorizationMonoid.{u_1} ↥K[f]
Tactic: haveI : UniqueFactorizationMonoid K[f] :=
    (f.transcendental_of_ne_C hf).uniqueFactorizationMonoid_adjoin
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
this : UniqueFactorizationMonoid.{u_1} ↥K[f]
⊢ Irreducible (M := (↥K⟮f⟯)[X]) (f.minpolyX ↥K⟮f⟯)
have rw : Irreducible (M := (↥K[f])[X]) (f.minpolyX ↥K[f])
Tactic: rw [← f.minpolyX_map K[f] K⟮f⟯,
    ← IsPrimitive.irreducible_iff_irreducible_map_fraction_map]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
this : UniqueFactorizationMonoid.{u_1} ↥K[f]
rw : Irreducible (M := (↥K[f])[X]) (f.minpolyX ↥K[f])
⊢ Irreducible (M := (↥K⟮f⟯)[X]) (f.minpolyX ↥K⟮f⟯)
have rw₁ : IsPrimitive (R := ↥K[f]) (f.minpolyX ↥K[f])
Tactic: rw [← f.minpolyX_map K[f] K⟮f⟯,
    ← IsPrimitive.irreducible_iff_irreducible_map_fraction_map]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
this : UniqueFactorizationMonoid.{u_1} ↥K[f]
⊢ IsPrimitive (R := ↥K[f]) (f.minpolyX ↥K[f])
have apply : natDegree (R := ↥K[f]) (f.minpolyX ↥K[f]) ≠ 0
Tactic: apply (f.irreducible_minpolyX' hf).isPrimitive
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (hypothesis)
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
this : UniqueFactorizationMonoid.{u_1} ↥K[f]
H : natDegree (R := ↥K[f]) (f.minpolyX ↥K[f]) = 0
⊢ False
have this₁ : natDegree (R := ↥K⟮f⟯) (Polynomial.map (R := ↥K[f]) (algebraMap ↥K[f] ↥K⟮f⟯) (f.minpolyX ↥K[f])) ≤
  natDegree (R := ↥K[f]) (f.minpolyX ↥K[f])
Tactic: have := natDegree_map_le (f := algebraMap K[f] K⟮f⟯) (p := f.minpolyX K[f])
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (hypothesis)
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
this_1 : UniqueFactorizationMonoid.{u_1} ↥K[f]
H : natDegree (R := ↥K[f]) (f.minpolyX ↥K[f]) = 0
this :
  natDegree (R := ↥K⟮f⟯) (Polynomial.map (R := ↥K[f]) (algebraMap ↥K[f] ↥K⟮f⟯) (f.minpolyX ↥K[f])) ≤
    natDegree (R := ↥K[f]) (f.minpolyX ↥K[f])
⊢ False
have this₁ : ∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
Tactic: rw [f.minpolyX_map K[f] K⟮f⟯, H, nonpos_iff_eq_zero, f.natDegree_minpolyX,
      Nat.max_eq_zero_iff, ← f.eq_C_iff] at this
Cleared hypotheses: this