awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Ne (α := K⟮X⟯[X]) (Polynomial.map (algebraMap (↥E) K⟮X⟯) (q E)) 0

Tactic:
Polynomial.map_ne_zero (q_ne_zero h)

Premises used: _private.0.RatFunc.Luroth.q_ne_zero, Polynomial.map_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Ne (α := K⟮X⟯[X]) (Polynomial.map (algebraMap (↥E) K⟮X⟯) (q E)) 0

Tactic:
exact Polynomial.map_ne_zero (q_ne_zero h)

Premises used: _private.0.RatFunc.Luroth.q_ne_zero, Polynomial.map_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
rw :
  HMul.hMul (β := K[X][Y]) (Polynomial.map Polynomial.C (g E)) ((Polynomial.C : (a : K[X]) → K[X][Y]) (f E) : K[X][Y]) -
      HMul.hMul (β := K[X][Y]) (Polynomial.map Polynomial.C (f E))
        ((Polynomial.C : (a : K[X]) → K[X][Y]) (g E) : K[X][Y]) =
    -θ E
⊢ (Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (θ E) = -θ E

Tactic:
rw [map_sub, map_mul, map_mul, Bivariate.swap_C, Bivariate.swap_map_C, Bivariate.swap_C,
    Bivariate.swap_map_C]

Premises used: map_sub, Polynomial.Bivariate.swap_map_C, map_mul, Polynomial.Bivariate.swap_C
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
⊢ HMul.hMul (β := K[X][Y]) (Polynomial.map Polynomial.C (g E)) ((Polynomial.C : (a : K[X]) → K[X][Y]) (f E) : K[X][Y]) -
      HMul.hMul (β := K[X][Y]) (Polynomial.map Polynomial.C (f E))
        ((Polynomial.C : (a : K[X]) → K[X][Y]) (g E) : K[X][Y]) =
    -θ E

Tactic:
ring
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (HMul.hMul (α := K[X][Y]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (g E) : K[X][Y])
          (Polynomial.map Polynomial.C (f E)) -
        HMul.hMul (α := K[X][Y]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (f E) : K[X][Y])
          (Polynomial.map Polynomial.C (g E))).natDegree ≤
    max
      (HMul.hMul (α := K[X][Y]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (g E) : K[X][Y])
          (Polynomial.map Polynomial.C (f E))).natDegree
      (HMul.hMul (α := K[X][Y]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (f E) : K[X][Y])
          (Polynomial.map Polynomial.C (g E))).natDegree

Tactic:
natDegree_sub_le _ _

Premises used: Polynomial.natDegree_sub_le
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
h₁ :
  (f E).natDegree =
    (HMul.hMul (α := K[X][Y]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (g E) : K[X][Y])
        (Polynomial.map Polynomial.C (f E))).natDegree
h₂ :
  (g E).natDegree =
    (HMul.hMul (α := K[X][Y]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (f E) : K[X][Y])
        (Polynomial.map Polynomial.C (g E))).natDegree
⊢ (θ E).natDegree ≤ m E

Tactic:
convert! natDegree_sub_le _ _ using 3

Premises used: Polynomial.natDegree_sub_le
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
h₁ :
  (f E).natDegree =
    natDegree.{u_1} (R := K[X]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (generator E).denom) +
      (Polynomial.map Polynomial.C (generator E).num).natDegree
h₂ : (f E).natDegree = 0 + (Polynomial.map Polynomial.C (generator E).num).natDegree
h₃ : (f E).natDegree = (Polynomial.map Polynomial.C (generator E).num).natDegree
h₄ h₅ : (f E).natDegree = (generator E).num.natDegree
⊢ (f E).natDegree =
    (HMul.hMul (α := K[X][Y]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (g E) : K[X][Y])
        (Polynomial.map Polynomial.C (f E))).natDegree

Tactic:
rw [natDegree_mul (C_ne_zero.mpr (generator E).denom_ne_zero)
      (Polynomial.map_ne_zero (num_ne_zero (generator_ne_zero h))), natDegree_C, zero_add,
      natDegree_map]

Premises used: Iff.mpr, Polynomial.natDegree_mul, RatFunc.Luroth.generator_ne_zero, Polynomial.natDegree_map, Polynomial.natDegree_C, RatFunc.num_ne_zero, zero_add, RatFunc.Luroth.generator, Polynomial.map_ne_zero, RatFunc.denom_ne_zero, Polynomial.C_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
h₁ :
  (g E).natDegree =
    natDegree.{u_1} (R := K[X]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (generator E).num) +
      (Polynomial.map Polynomial.C (generator E).denom).natDegree
h₂ : (g E).natDegree = 0 + (Polynomial.map Polynomial.C (generator E).denom).natDegree
h₃ : (g E).natDegree = (Polynomial.map Polynomial.C (generator E).denom).natDegree
h₄ h₅ : (g E).natDegree = (generator E).denom.natDegree
⊢ (g E).natDegree =
    (HMul.hMul (α := K[X][Y]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (f E) : K[X][Y])
        (Polynomial.map Polynomial.C (g E))).natDegree

Tactic:
rw [natDegree_mul (C_ne_zero.mpr (num_ne_zero (generator_ne_zero h)))
      (Polynomial.map_ne_zero (generator E).denom_ne_zero), natDegree_C, zero_add, natDegree_map]

Premises used: Iff.mpr, Polynomial.natDegree_mul, RatFunc.Luroth.generator_ne_zero, Polynomial.natDegree_map, Polynomial.natDegree_C, RatFunc.num_ne_zero, zero_add, RatFunc.Luroth.generator, Polynomial.map_ne_zero, RatFunc.denom_ne_zero, Polynomial.C_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X])
        ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E)) : K⟮X⟯[X])
        (Polynomial.map (algebraMap (↥E) K⟮X⟯) (q E)) *
      Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
rw :
  HMul.hMul (α := K⟮X⟯[X])
      ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X])
          (HDiv.hDiv (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯) (c E)) :
        K⟮X⟯[X])
      (HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X]) ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) (c E) : K⟮X⟯[X])
          (Polynomial.map (algebraMap (↥E) K⟮X⟯) (q E)) *
        Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E)) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
⊢ Q₀ E * Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E) = Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)

Tactic:
rw [← C_c_mul_φ h, mul_assoc, ← mul_assoc _ (Polynomial.C (c E)) _,
      mul_comm _ (Polynomial.C (c E))]

Premises used: Polynomial.C, mul_assoc, _private.0.RatFunc.Luroth.C_c_mul_φ, _private.0.RatFunc.Luroth.c, mul_comm, DFunLike.coe
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X])
        ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E)) : K⟮X⟯[X])
        (Polynomial.map (algebraMap (↥E) K⟮X⟯) (q E)) *
      Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
⊢ HMul.hMul (α := K⟮X⟯[X])
      ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X])
          (HDiv.hDiv (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯) (c E)) :
        K⟮X⟯[X])
      (HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X]) ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) (c E) : K⟮X⟯[X])
          (Polynomial.map (algebraMap (↥E) K⟮X⟯) (q E)) *
        Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E)) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)

Tactic:
simpa only [← mul_assoc, ← C_mul, div_mul_cancel₀ _ (c_ne_zero h)] using this

Premises used: _private.0.RatFunc.Luroth.c_ne_zero, div_mul_cancel₀, mul_assoc, Polynomial.C_mul
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
rw :
  HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X])
        ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E)) : K⟮X⟯[X])
        (Polynomial.map (algebraMap (↥E) K⟮X⟯) (q E)) *
      Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
⊢ Q₀ E * Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E) = Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)

Tactic:
suffices
    Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E)) * (q E).map (algebraMap (↥E) K⟮X⟯) *
       (φ E).map (algebraMap (↥E) K⟮X⟯) = (θ E).map (algebraMap K[X] K⟮X⟯) by
    rw [← C_c_mul_φ h, mul_assoc, ← mul_assoc _ (Polynomial.C (c E)) _,
      mul_comm _ (Polynomial.C (c E))]
    simpa only [← mul_assoc, ← C_mul, div_mul_cancel₀ _ (c_ne_zero h)] using this
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
rw :
  HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X])
        ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E)) : K⟮X⟯[X])
        (Polynomial.map
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥E) K⟮X⟯)
              (↑(inclusion ⋯) : ↥K⟮generator E⟯ →+* ↥E))
            (algebraMap K ↥K⟮generator E⟯))
          (generator E).num) -
      HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X])
        ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X])
            (HMul.hMul (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯)
              (↑(Subtype.mk (p := fun (x : K⟮X⟯) ↦ Membership.mem (γ := Subalgebra K K⟮X⟯) K[generator E] x)
                    (generator E) ⋯) :
                K⟮X⟯)) :
          K⟮X⟯[X])
        (Polynomial.map
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥E) K⟮X⟯)
              (↑(inclusion ⋯) : ↥K⟮generator E⟯ →+* ↥E))
            (algebraMap K ↥K⟮generator E⟯))
          (generator E).denom) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
⊢ HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X])
        ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E)) : K⟮X⟯[X])
        (Polynomial.map (algebraMap (↥E) K⟮X⟯) (q E)) *
      Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)

Tactic:
rw [mul_assoc, ← Polynomial.map_mul, mul_comm (q E) (φ E), φ_mul_q, Polynomial.map_map,
    Polynomial.map_sub, Polynomial.map_mul, map_C, RingHom.coe_comp, Function.comp_apply,
    IntermediateField.algebraMap_apply, Polynomial.map_map, Polynomial.map_map, mul_sub,
    ← mul_assoc, ← map_mul, (inclusion adjoin_generator_le).algebraMap_toAlgebra,
    AlgHom.toRingHom_eq_coe, RingHom.coe_coe, coe_inclusion, coe_algebraMap]

Premises used: _private.0.RatFunc.Luroth.φ_mul_q, Polynomial.map_mul, mul_sub, IntermediateField.coe_inclusion, _private.0.RatFunc.Luroth.φ, RingHom.coe_coe, mul_assoc, IntermediateField.algebraMap_apply, map_mul, AlgHom.toRingHom, AlgHom.toRingHom_eq_coe, RatFunc.Luroth.adjoin_generator_le, mul_comm, Polynomial.map_sub, RingHom.coe_comp, Function.comp_apply, RingHom.algebraMap_toAlgebra, _private.0.RatFunc.Luroth.q, IntermediateField.inclusion, Polynomial.map_C, Polynomial.map_map, IntermediateField.algebraAdjoinAdjoin.coe_algebraMap
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
enter :
  (↑(Subtype.mk (p := fun (x : K⟮X⟯) ↦ Membership.mem (γ := Subalgebra K K⟮X⟯) K[generator E] x) (generator E) ⋯) :
    K⟮X⟯)
| HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X])
        ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E)) : K⟮X⟯[X])
        (Polynomial.map
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥E) K⟮X⟯)
              (↑(inclusion ⋯) : ↥K⟮generator E⟯ →+* ↥E))
            (algebraMap K ↥K⟮generator E⟯))
          (generator E).num) -
      HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X])
        ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X])
            (HMul.hMul (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯)
              (↑(Subtype.mk (p := fun (x : K⟮X⟯) ↦ Membership.mem (γ := Subalgebra K K⟮X⟯) K[generator E] x)
                    (generator E) ⋯) :
                K⟮X⟯)) :
          K⟮X⟯[X])
        (Polynomial.map
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥E) K⟮X⟯)
              (↑(inclusion ⋯) : ↥K⟮generator E⟯ →+* ↥E))
            (algebraMap K ↥K⟮generator E⟯))
          (generator E).denom) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)

Tactic:
enter [1, 2, 1, 2, 2]
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
rw :
  (↑(Subtype.mk (p := fun (x : K⟮X⟯) ↦
        Membership.mem (γ := Subalgebra K K⟮X⟯)
          K[HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (generator E).num : K⟮X⟯)
              ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (generator E).denom : K⟮X⟯)]
          x)
        (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (generator E).num : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (generator E).denom : K⟮X⟯))
        ⋯) :
    K⟮X⟯)
| (↑(Subtype.mk (p := fun (x : K⟮X⟯) ↦ Membership.mem (γ := Subalgebra K K⟮X⟯) K[generator E] x) (generator E) ⋯) :
    K⟮X⟯)

Tactic:
rw [← num_div_denom (generator E)]

Premises used: RatFunc.Luroth.generator, RatFunc.num_div_denom
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
enter :
  (↑(Subtype.mk (p := fun (x : K⟮X⟯) ↦
        Membership.mem (γ := Subalgebra K K⟮X⟯)
          K[HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (generator E).num : K⟮X⟯)
              ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (generator E).denom : K⟮X⟯)]
          x)
        (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (generator E).num : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (generator E).denom : K⟮X⟯))
        ⋯) :
    K⟮X⟯)
| HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X])
        ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E)) : K⟮X⟯[X])
        (Polynomial.map
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥E) K⟮X⟯)
              (↑(inclusion ⋯) : ↥K⟮generator E⟯ →+* ↥E))
            (algebraMap K ↥K⟮generator E⟯))
          (generator E).num) -
      HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X])
        ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X])
            (HMul.hMul (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯)
              (↑(Subtype.mk (p := fun (x : K⟮X⟯) ↦ Membership.mem (γ := Subalgebra K K⟮X⟯) K[generator E] x)
                    (generator E) ⋯) :
                K⟮X⟯)) :
          K⟮X⟯[X])
        (Polynomial.map
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥E) K⟮X⟯)
              (↑(inclusion ⋯) : ↥K⟮generator E⟯ →+* ↥E))
            (algebraMap K ↥K⟮generator E⟯))
          (generator E).denom) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)

Tactic:
enter [1, 2, 1, 2, 2]; rw [← num_div_denom (generator E)]

Premises used: RatFunc.Luroth.generator, RatFunc.num_div_denom
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
conv :
  HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X])
        ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E)) : K⟮X⟯[X])
        (Polynomial.map
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥E) K⟮X⟯)
              (↑(inclusion ⋯) : ↥K⟮generator E⟯ →+* ↥E))
            (algebraMap K ↥K⟮generator E⟯))
          (generator E).num) -
      HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X])
        ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X])
            (HMul.hMul (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯)
              (↑(Subtype.mk (p := fun (x : K⟮X⟯) ↦
                    Membership.mem (γ := Subalgebra K K⟮X⟯)
                      K[HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯)
                          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (generator E).num : K⟮X⟯)
                          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (generator E).denom : K⟮X⟯)]
                      x)
                    (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯)
                      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (generator E).num : K⟮X⟯)
                      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (generator E).denom : K⟮X⟯))
                    ⋯) :
                K⟮X⟯)) :
          K⟮X⟯[X])
        (Polynomial.map
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥E) K⟮X⟯)
              (↑(inclusion ⋯) : ↥K⟮generator E⟯ →+* ↥E))
            (algebraMap K ↥K⟮generator E⟯))
          (generator E).denom) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
⊢ HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X])
        ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E)) : K⟮X⟯[X])
        (Polynomial.map
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥E) K⟮X⟯)
              (↑(inclusion ⋯) : ↥K⟮generator E⟯ →+* ↥E))
            (algebraMap K ↥K⟮generator E⟯))
          (generator E).num) -
      HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X])
        ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X])
            (HMul.hMul (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯)
              (↑(Subtype.mk (p := fun (x : K⟮X⟯) ↦ Membership.mem (γ := Subalgebra K K⟮X⟯) K[generator E] x)
                    (generator E) ⋯) :
                K⟮X⟯)) :
          K⟮X⟯[X])
        (Polynomial.map
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥E) K⟮X⟯)
              (↑(inclusion ⋯) : ↥K⟮generator E⟯ →+* ↥E))
            (algebraMap K ↥K⟮generator E⟯))
          (generator E).denom) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)

Tactic:
conv => enter [1, 2, 1, 2, 2]; rw [← num_div_denom (generator E)]

Premises used: RatFunc.Luroth.generator, RatFunc.num_div_denom
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X])
        ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E)) : K⟮X⟯[X])
        (Polynomial.map
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥E) K⟮X⟯)
              (↑(inclusion ⋯) : ↥K⟮generator E⟯ →+* ↥E))
            (algebraMap K ↥K⟮generator E⟯))
          (generator E).num) -
      HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X])
        ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (generator E).num) : K⟮X⟯[X])
        (Polynomial.map
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥E) K⟮X⟯)
              (↑(inclusion ⋯) : ↥K⟮generator E⟯ →+* ↥E))
            (algebraMap K ↥K⟮generator E⟯))
          (generator E).denom) =
    HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X])
        ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E)) : K⟮X⟯[X])
        (Polynomial.map (RingHom.comp (algebraMap K[X] K⟮X⟯) Polynomial.C) (f E)) -
      HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X])
        ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (f E)) : K⟮X⟯[X])
        (Polynomial.map (RingHom.comp (algebraMap K[X] K⟮X⟯) Polynomial.C) (g E))

Tactic:
rfl
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
apply :
  Membership.mem (γ := Subsemiring K⟮X⟯[X]) (lifts (R := K[X]) (algebraMap K[X] K⟮X⟯))
    (Q₀ E * Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ' E).primPart)
⊢ Membership.mem (γ := Subsemiring K⟮X⟯[X]) (lifts (R := K[X]) (algebraMap K[X] K⟮X⟯)) (Q₀ E)

Tactic:
apply (Φ' E).isPrimitive_primPart.mul_map_mem_lifts_iff.mp

Premises used: _private.0.RatFunc.Luroth.Φ', Polynomial.IsPrimitive.mul_map_mem_lifts_iff, Polynomial.isPrimitive_primPart, Iff.mp
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
rw :
  Membership.mem (γ := Subsemiring K⟮X⟯[X]) (lifts (R := K[X]) (algebraMap K[X] K⟮X⟯))
    (Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E))
⊢ Membership.mem (γ := Subsemiring K⟮X⟯[X]) (lifts (R := K[X]) (algebraMap K[X] K⟮X⟯))
    (Q₀ E * Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ' E).primPart)

Tactic:
rw [Q₀_mul_Φ h]

Premises used: _private.0.RatFunc.Luroth.Q₀_mul_Φ
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Membership.mem (γ := Subsemiring K⟮X⟯[X]) (lifts (R := K[X]) (algebraMap K[X] K⟮X⟯))
    (Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E))

Tactic:
⟨_, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, rfl
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Membership.mem (γ := Subsemiring K⟮X⟯[X]) (lifts (R := K[X]) (algebraMap K[X] K⟮X⟯))
    (Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E))

Tactic:
exact ⟨_, rfl⟩
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
apply :
  Membership.mem (γ := Subsemiring K⟮X⟯[X]) (lifts (R := K[X]) (algebraMap K[X] K⟮X⟯))
    (Q₀ E * Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ' E).primPart)
apply₁ :
  Membership.mem (γ := Subsemiring K⟮X⟯[X]) (lifts (R := K[X]) (algebraMap K[X] K⟮X⟯))
    (Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E))
⊢ Membership.mem (γ := Subsemiring K⟮X⟯[X]) (lifts (R := K[X]) (algebraMap K[X] K⟮X⟯)) (Q₀ E)

Tactic:
classical
  apply (Φ' E).isPrimitive_primPart.mul_map_mem_lifts_iff.mp
  rw [Q₀_mul_Φ h]
  exact ⟨_, rfl⟩

Premises used: _private.0.RatFunc.Luroth.Q₀_mul_Φ
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.map (algebraMap K[X] K⟮X⟯) (Q₁ h) = Q₀ E

Tactic:
(Q₀_mem_lifts h).choose_spec

Premises used: Exists.choose_spec, _private.0.RatFunc.Luroth.Q₀_mem_lifts, Polynomial.map
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
apply_fun :
  Ne (α := K⟮X⟯[X]) (Polynomial.map (algebraMap K[X] K⟮X⟯) (Q₁ h)) (Polynomial.map (R := K[X]) (algebraMap K[X] K⟮X⟯) 0)
⊢ Q₁ h ≠ 0

Tactic:
apply_fun Polynomial.map (algebraMap K[X] K⟮X⟯)

Premises used: Algebra.algebraMap, Polynomial, RatFunc, Polynomial.map
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
rw : Q₀ E ≠ 0
⊢ Ne (α := K⟮X⟯[X]) (Polynomial.map (algebraMap K[X] K⟮X⟯) (Q₁ h)) (Polynomial.map (R := K[X]) (algebraMap K[X] K⟮X⟯) 0)

Tactic:
rw [map_Q₁, Polynomial.map_zero]

Premises used: _private.0.RatFunc.Luroth.map_Q₁, Polynomial.map_zero
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Q₀ E ≠ 0

Tactic:
Q₀_ne_zero h

Premises used: _private.0.RatFunc.Luroth.Q₀_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Q₀ E ≠ 0

Tactic:
exact Q₀_ne_zero h

Premises used: _private.0.RatFunc.Luroth.Q₀_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := K[X][Y]) (β := K⟮X⟯[X]) (Polynomial.map (algebraMap K[X] K⟮X⟯))

Tactic:
Polynomial.map_injective _ (algebraMap_injective K)

Premises used: Polynomial.map_injective, RatFunc.algebraMap_injective