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
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])))
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])))
⊢ Irreducible φ

Tactic:
rw [this, 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])
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
    (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:
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

Premises used: Iff.mpr, RatFunc.isCoprime_num_denom, IsCoprime.symm, IsCoprime.neg_right_iff, IsCoprime.isRelPrime, neg_ne_zero, Polynomial.irreducible_C_mul_X_add_C, RatFunc.denom_ne_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
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])))
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])
⊢ 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:
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

Premises used: Iff.mpr, RatFunc.isCoprime_num_denom, IsCoprime.symm, IsCoprime.neg_right_iff, IsCoprime.isRelPrime, neg_ne_zero, Polynomial.irreducible_C_mul_X_add_C, RatFunc.denom_ne_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
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])))
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)
⊢ 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:
rw [add_comm, X_mul_C, map_neg, neg_mul]

Premises used: Polynomial.X_mul_C, map_neg, add_comm, neg_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
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.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:
sub_eq_add_neg (Polynomial.C f.num) (Polynomial.C f.denom * Polynomial.X)

Premises used: Polynomial.C, RatFunc.denom, HMul.hMul, sub_eq_add_neg, RatFunc.num, Polynomial.X, DFunLike.coe
-- 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])
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.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:
exact sub_eq_add_neg (Polynomial.C f.num) (Polynomial.C f.denom * Polynomial.X)

Premises used: Polynomial.C, RatFunc.denom, HMul.hMul, sub_eq_add_neg, RatFunc.num, Polynomial.X, DFunLike.coe
-- 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
⊢ UniqueFactorizationMonoid.{u_1} ↥K[f]

Tactic:
haveI : UniqueFactorizationMonoid K[f] :=
    (f.transcendental_of_ne_C hf).uniqueFactorizationMonoid_adjoin
-- 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 : UniqueFactorizationMonoid.{u_1} ↥K[f]
rw : Irreducible (M := (↥K[f])[X]) (f.minpolyX ↥K[f])
rw₁ : IsPrimitive (R := ↥K[f]) (f.minpolyX ↥K[f])
⊢ 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]

Premises used: RatFunc.minpolyX_map, Algebra.adjoin, Polynomial.IsPrimitive.irreducible_iff_irreducible_map_fraction_map, Membership.mem, Subtype, IntermediateField.adjoin, Singleton.singleton
-- 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 : UniqueFactorizationMonoid.{u_1} ↥K[f]
⊢ Irreducible (M := (↥K[f])[X]) (f.minpolyX ↥K[f])

Tactic:
f.irreducible_minpolyX' hf

Premises used: RatFunc.irreducible_minpolyX'
-- 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 : UniqueFactorizationMonoid.{u_1} ↥K[f]
⊢ Irreducible (M := (↥K[f])[X]) (f.minpolyX ↥K[f])

Tactic:
exact f.irreducible_minpolyX' hf

Premises used: RatFunc.irreducible_minpolyX'
-- 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 : UniqueFactorizationMonoid.{u_1} ↥K[f]
apply : natDegree (R := ↥K[f]) (f.minpolyX ↥K[f]) ≠ 0
⊢ IsPrimitive (R := ↥K[f]) (f.minpolyX ↥K[f])

Tactic:
apply (f.irreducible_minpolyX' hf).isPrimitive

Premises used: Irreducible.isPrimitive, RatFunc.irreducible_minpolyX'
-- 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 : UniqueFactorizationMonoid.{u_1} ↥K[f]
H : natDegree (R := ↥K[f]) (f.minpolyX ↥K[f]) = 0
⊢ 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])
-- 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_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])
⊢ ∃ (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

Premises used: RatFunc.minpolyX_map, Algebra.adjoin, Membership.mem, Subtype, RatFunc.natDegree_minpolyX, Nat.max_eq_zero_iff, IntermediateField.adjoin, RatFunc.eq_C_iff, Singleton.singleton, nonpos_iff_eq_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_1 : UniqueFactorizationMonoid.{u_1} ↥K[f]
H : natDegree (R := ↥K[f]) (f.minpolyX ↥K[f]) = 0
this : ∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
⊢ False

Tactic:
hf 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_1 : UniqueFactorizationMonoid.{u_1} ↥K[f]
H : natDegree (R := ↥K[f]) (f.minpolyX ↥K[f]) = 0
this : ∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
⊢ False

Tactic:
exact hf this
-- 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),
    Module.finrank.{u_1, u_1} (↥K⟮f⟯) K⟮X⟯ = max f.num.natDegree f.denom.natDegree
neg :
  ∀ (hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c),
    Module.finrank.{u_1, u_1} (↥K⟮f⟯) K⟮X⟯ = max f.num.natDegree f.denom.natDegree
⊢ Module.finrank.{u_1, u_1} (↥K⟮f⟯) K⟮X⟯ = 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),
    Module.finrank.{u_1, u_1} (↥K⟮((C : (a : K) → K⟮X⟯) c : K⟮X⟯)⟯) 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)))
⊢ Module.finrank.{u_1, u_1} (↥K⟮f⟯) K⟮X⟯ = 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
pos :
  0 =
    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)))
⊢ Module.finrank.{u_1, u_1} (↥K⟮((C : (a : K) → K⟮X⟯) c : K⟮X⟯)⟯) 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:
rw [adjoin_simple_eq_bot_iff.mpr (show C c ∈ ⊥ from ⟨c, rfl⟩), finrank_bot',
      Module.finrank_of_not_finite fun H ↦ Algebra.transcendental_iff_not_isAlgebraic.mp
      transcendental <| Algebra.IsAlgebraic.of_finite K K⟮X⟯]

Premises used: Iff.mpr, Algebra.IsAlgebraic.of_finite, Algebra.transcendental_iff_not_isAlgebraic, RatFunc, IntermediateField.adjoin_simple_eq_bot_iff, Exists.intro, Iff.mp, Module.finrank_of_not_finite, RatFunc.transcendental, IntermediateField.finrank_bot', rfl
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
c : K
⊢ 0 =
    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 : Module.finrank.{u_1, u_1} ↥K⟮f⟯ ↥(↥K⟮f⟯)⟮ X⟯ = max f.num.natDegree f.denom.natDegree
neg₁ : natDegree.{u_1} (R := ↥K⟮f⟯) (minpoly ↥K⟮f⟯ (B := K⟮X⟯) X) = max f.num.natDegree f.denom.natDegree
neg₂ :
  (HMul.hMul (α := (↥K⟮f⟯)[X]) (f.minpolyX ↥K⟮f⟯)
        ((Polynomial.C : (a : ↥K⟮f⟯) → (↥K⟮f⟯)[X]) (leadingCoeff (f.minpolyX ↥K⟮f⟯))⁻¹)).natDegree =
    max f.num.natDegree f.denom.natDegree
neg₃ :
  (HMul.hMul (α := (↥K⟮f⟯)[X]) ((Polynomial.C : (a : ↥K⟮f⟯) → (↥K⟮f⟯)[X]) (leadingCoeff (f.minpolyX ↥K⟮f⟯))⁻¹)
        (f.minpolyX ↥K⟮f⟯)).natDegree =
    max f.num.natDegree f.denom.natDegree
neg₄ : natDegree (R := ↥K⟮f⟯) (f.minpolyX ↥K⟮f⟯) = max f.num.natDegree f.denom.natDegree
neg₅ neg₆ : max f.num.natDegree f.denom.natDegree = max f.num.natDegree f.denom.natDegree
⊢ Module.finrank.{u_1, u_1} (↥K⟮f⟯) K⟮X⟯ = max f.num.natDegree f.denom.natDegree

Tactic:
rw [← (IntermediateField.adjoinXEquiv K⟮f⟯).toLinearEquiv.finrank_eq,
    adjoin.finrank (f.isAlgebraic_adjoin_simple_X hf).isIntegral,
    ← minpoly.eq_of_irreducible (f.irreducible_minpolyX hf) f.minpolyX_aeval_X, mul_comm,
    natDegree_C_mul <| inv_ne_zero <| leadingCoeff_ne_zero.mpr fun H ↦
    hf ((minpolyX_eq_zero_iff f).mp H), natDegree_minpolyX]

Premises used: Iff.mpr, IntermediateField.adjoin.finrank, minpoly.eq_of_irreducible, LinearEquiv.finrank_eq, Polynomial.natDegree_C_mul, RatFunc.minpolyX_aeval_X, RatFunc.irreducible_minpolyX, RatFunc.natDegree_minpolyX, RatFunc.minpolyX_eq_zero_iff, Polynomial.leadingCoeff_ne_zero, IntermediateField.adjoin, IsAlgebraic.isIntegral, AlgEquiv.toLinearEquiv, Iff.mp, mul_comm, inv_ne_zero, RatFunc.IntermediateField.adjoinXEquiv, Singleton.singleton, RatFunc.isAlgebraic_adjoin_simple_X
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
hE : E ≠ ⊥
⊢ ∃ x ∈ E, x ∉ ⊥

Tactic:
rw [ne_eq, ← le_bot_iff, SetLike.not_le_iff_exists] at hE

Premises used: le_bot_iff, ne_eq, SetLike.not_le_iff_exists
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
hE : ∃ x ∈ E, x ∉ ⊥
obtain : ∀ (f : K⟮X⟯) (hf₁ : f ∈ E) (hf₂ : f ∉ ⊥), IsAlgebraic.{u_1, u_1} ↥E (A := K⟮X⟯) X
⊢ IsAlgebraic.{u_1, u_1} ↥E (A := K⟮X⟯) X

Tactic:
obtain ⟨f, hf₁, hf₂⟩ := hE
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
c : K
hf₁ : Membership.mem (α := K⟮X⟯) E ((C : (a : K) → K⟮X⟯) c : K⟮X⟯)
hf₂ : ((C : (a : K) → K⟮X⟯) c : K⟮X⟯) ∉ ⊥
⊢ False

Tactic:
hf₂ ⟨c, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
c : K
hf₁ : Membership.mem (α := K⟮X⟯) E ((C : (a : K) → K⟮X⟯) c : K⟮X⟯)
hf₂ : ((C : (a : K) → K⟮X⟯) c : K⟮X⟯) ∉ ⊥
⊢ False

Tactic:
exact hf₂ ⟨c, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
f : K⟮X⟯
hf₁ : f ∈ E
hf₂ : f ∉ ⊥
⊢ IsAlgebraic.{u_1, u_1} ↥E (A := K⟮X⟯) X

Tactic:
exact IsAlgebraic.tower_top_of_subalgebra_le (adjoin_simple_le_iff.mpr hf₁) <|
    f.isAlgebraic_adjoin_simple_X (by rintro ⟨c, rfl⟩; exact hf₂ ⟨c, rfl⟩)

Premises used: Iff.mpr, IsAlgebraic.tower_top_of_subalgebra_le, IntermediateField.adjoin_simple_le_iff, RatFunc.isAlgebraic_adjoin_simple_X
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ φ E ≠ 0

Tactic:
minpoly.ne_zero (IntermediateField.isAlgebraic_X h).isIntegral

Premises used: Set.Mem, RatFunc.IntermediateField.isAlgebraic_X, IsAlgebraic.isIntegral, minpoly.ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (φ E).Monic

Tactic:
minpoly.monic (IntermediateField.isAlgebraic_X h).isIntegral

Premises used: minpoly.monic, Set.Mem, RatFunc.IntermediateField.isAlgebraic_X, IsAlgebraic.isIntegral
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
rw : (φ E).natDegree = Module.finrank.{u_1, u_1} ↥E ↥(↥E)⟮ X⟯
rw₁ rw₂ : (φ E).natDegree = natDegree.{u_1} (R := ↥E) (minpoly ↥E (B := K⟮X⟯) X)
⊢ (φ E).natDegree = Module.finrank.{u_1, u_1} (↥E) K⟮X⟯

Tactic:
rw [← (IntermediateField.adjoinXEquiv E).toLinearEquiv.finrank_eq,
    adjoin.finrank (IntermediateField.isAlgebraic_X h).isIntegral]

Premises used: IntermediateField.adjoin.finrank, RatFunc.IntermediateField.isAlgebraic_X, LinearEquiv.finrank_eq, IsAlgebraic.isIntegral, AlgEquiv.toLinearEquiv, RatFunc.IntermediateField.adjoinXEquiv
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
rw : φ E ∉ RingHom.range (R := K[X]) (Polynomial.mapRingHom (algebraMap K ↥E))
⊢ ∃ (i : ℕ), (φ E).coeff i ∉ RingHom.range (R := K) (algebraMap K ↥E)

Tactic:
rw [← notMem_map_range]

Premises used: Polynomial.notMem_map_range
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
f : K[X]
hf : ((Polynomial.mapRingHom (algebraMap K ↥E) : K[X] →+* (↥E)[X]) : (a : K[X]) → (↥E)[X]) f = φ E
⊢ Polynomial.map (algebraMap K ↥E) f = φ E

Tactic:
rw [coe_mapRingHom] at hf

Premises used: Polynomial.coe_mapRingHom
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
f : K[X]
hf : Polynomial.map (algebraMap K ↥E) f = φ E
⊢ False

Tactic:
transcendental_X ⟨f, ?_, ?_⟩

Premises used: RatFunc.transcendental_X, And.intro, Exists.intro
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
f : K[X]
hf : Polynomial.map (algebraMap K ↥E) f = φ E
refine_1 : f ≠ 0
refine_2 : Eq (α := K⟮X⟯) ((aeval X : (a : K[X]) → K⟮X⟯) f : K⟮X⟯) (0 : K⟮X⟯)
⊢ False

Tactic:
refine transcendental_X ⟨f, ?_, ?_⟩

Premises used: RatFunc.transcendental_X, And.intro, Exists.intro
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
f : K[X]
hf : Polynomial.map (algebraMap K ↥E) f = φ E
refine_1 : Ne (α := (↥E)[X]) (Polynomial.map (algebraMap K ↥E) f) 0
⊢ f ≠ 0

Tactic:
apply (Polynomial.map_ne_zero_iff (FaithfulSMul.algebraMap_injective K E)).mp

Premises used: Membership.mem, Subtype, FaithfulSMul.algebraMap_injective, Iff.mp, Polynomial.map_ne_zero_iff
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
f : K[X]
hf : Polynomial.map (algebraMap K ↥E) f = φ E
⊢ Ne (α := (↥E)[X]) (Polynomial.map (algebraMap K ↥E) f) 0

Tactic:
hf ▸ φ_ne_zero h

Premises used: Eq.rec, Eq.symm, _private.0.RatFunc.Luroth.φ_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
f : K[X]
hf : Polynomial.map (algebraMap K ↥E) f = φ E
⊢ Ne (α := (↥E)[X]) (Polynomial.map (algebraMap K ↥E) f) 0

Tactic:
exact hf ▸ φ_ne_zero h
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
f : K[X]
hf : Polynomial.map (algebraMap K ↥E) f = φ E
⊢ Eq (α := K⟮X⟯) ((aeval X : (a : K[X]) → K⟮X⟯) f : K⟮X⟯) (0 : K⟮X⟯)

Tactic:
simpa using congr(aeval (X : K⟮X⟯) $(hf))
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E = ⊥
⊢ generator E = 0

Tactic:
dif_pos h

Premises used: dif_pos, RatFunc.Luroth.generator
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ generator E = (↑((φ E).coeff (generatorIndex h)) : K⟮X⟯)

Tactic:
dif_neg h

Premises used: Set.Mem, dif_neg, RatFunc.Luroth.generator
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
pos : ∀ (h : E = ⊥), generator E ∈ E
neg : ∀ (h : ¬E = ⊥), generator E ∈ E
⊢ generator E ∈ E

Tactic:
by_cases h : E = ⊥
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E = ⊥
pos : 0 ∈ E
⊢ generator E ∈ E

Tactic:
rw [generator_eq_zero h]

Premises used: RatFunc.Luroth.generator_eq_zero
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E = ⊥
⊢ 0 ∈ E

Tactic:
E.zero_mem

Premises used: Set.Mem, IntermediateField.zero_mem
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E = ⊥
⊢ 0 ∈ E

Tactic:
exact E.zero_mem

Premises used: IntermediateField.zero_mem
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : ¬E = ⊥
neg : (↑((φ E).coeff (generatorIndex h)) : K⟮X⟯) ∈ E
⊢ generator E ∈ E

Tactic:
rw [generator_eq_coeff h]

Premises used: _private.0.RatFunc.Luroth.generator_eq_coeff