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 ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H_1 : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : Eq (α := F) ((aeval α : (a : K[X]) → F) (Q₂ h) : F) (0 : F)
eq :
  HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (g E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (f E)) : F[X]) =
    HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (f E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X])
H : Ne (α := F) ((aeval α : (a : K[X]) → F) (generator E).num : F) (0 : F)
inl :
  Ne (α := F[X]) ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X])
    ((Polynomial.C : (a : F) → F[X]) 0 : F[X])
⊢ Ne (α := F) ((aeval α : (a : K[X]) → F) (f E) : F) (0 : F) ∧
    Ne (α := F) ((aeval α : (a : K[X]) → F) (g E) : F) (0 : F)

Tactic:
refine ⟨H, Polynomial.C_injective.ne_iff.mp ?_⟩
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H_1 : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : Eq (α := F) ((aeval α : (a : K[X]) → F) (Q₂ h) : F) (0 : F)
eq :
  HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (g E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (f E)) : F[X]) =
    HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (f E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X])
H : Ne (α := F) ((aeval α : (a : K[X]) → F) (generator E).num : F) (0 : F)
inl :
  HMul.hMul (β := F[X]) (Polynomial.map (algebraMap K F) (generator E).num)
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X]) ≠
    0
rw : K →+* F
⊢ Ne (α := F[X]) ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X])
    ((Polynomial.C : (a : F) → F[X]) 0 : F[X])

Tactic:
rw [map_zero, ← mul_ne_zero_iff_left <| Polynomial.map_ne_zero <|
        num_ne_zero (generator_ne_zero h)]

Premises used: RatFunc.Luroth.generator_ne_zero, RatFunc.num_ne_zero, map_zero, mul_ne_zero_iff_left, Polynomial.map_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H_1 : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : Eq (α := F) ((aeval α : (a : K[X]) → F) (Q₂ h) : F) (0 : F)
eq :
  HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (g E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (f E)) : F[X]) =
    HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (f E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X])
H : Ne (α := F) ((aeval α : (a : K[X]) → F) (generator E).denom : F) (0 : F)
⊢ Ne (α := F) ((aeval α : (a : K[X]) → F) (f E) : F) (0 : F) ∧
    Ne (α := F) ((aeval α : (a : K[X]) → F) (g E) : F) (0 : F)

Tactic:
⟨Polynomial.C_injective.ne_iff.mp ?_, H⟩

Premises used: Function.Injective.ne_iff, And.intro, Iff.mp, Polynomial.C_injective
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H_1 : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : Eq (α := F) ((aeval α : (a : K[X]) → F) (Q₂ h) : F) (0 : F)
eq :
  HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (g E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (f E)) : F[X]) =
    HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (f E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X])
H : Ne (α := F) ((aeval α : (a : K[X]) → F) (generator E).denom : F) (0 : F)
inr :
  Ne (α := F[X]) ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (f E)) : F[X])
    ((Polynomial.C : (a : F) → F[X]) 0 : F[X])
⊢ Ne (α := F) ((aeval α : (a : K[X]) → F) (f E) : F) (0 : F) ∧
    Ne (α := F) ((aeval α : (a : K[X]) → F) (g E) : F) (0 : F)

Tactic:
refine ⟨Polynomial.C_injective.ne_iff.mp ?_, H⟩
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H_1 : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : Eq (α := F) ((aeval α : (a : K[X]) → F) (Q₂ h) : F) (0 : F)
eq :
  HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (g E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (f E)) : F[X]) =
    HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (f E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X])
H : Ne (α := F) ((aeval α : (a : K[X]) → F) (generator E).denom : F) (0 : F)
inr :
  HMul.hMul (β := F[X]) (Polynomial.map (algebraMap K F) (generator E).denom)
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (f E)) : F[X]) ≠
    0
rw : K →+* F
⊢ Ne (α := F[X]) ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (f E)) : F[X])
    ((Polynomial.C : (a : F) → F[X]) 0 : F[X])

Tactic:
rw [map_zero, ← mul_ne_zero_iff_left <| Polynomial.map_ne_zero (generator E).denom_ne_zero]

Premises used: map_zero, mul_ne_zero_iff_left, RatFunc.Luroth.generator, Polynomial.map_ne_zero, RatFunc.denom_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : Eq (α := F) ((aeval α : (a : K[X]) → F) (Q₂ h) : F) (0 : F)
eq :
  HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (g E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (f E)) : F[X]) =
    HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (f E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X])
⊢ IsUnit (M := F[X]) ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (f E)) : F[X])

Tactic:
obtain ⟨isUnit₁, isUnit₂⟩ :
      IsUnit (Polynomial.C <| aeval α (f E)) ∧ IsUnit (Polynomial.C <| aeval α (g E)) := by
    rw [Polynomial.isUnit_C, isUnit_iff_ne_zero, Polynomial.isUnit_C, isUnit_iff_ne_zero]
    obtain (H | H) := aeval_ne_zero_of_isCoprime (generator E).isCoprime_num_denom α
    · refine ⟨H, Polynomial.C_injective.ne_iff.mp ?_⟩
      rw [map_zero, ← mul_ne_zero_iff_left <| Polynomial.map_ne_zero <|
        num_ne_zero (generator_ne_zero h)]
      exact eq ▸ mul_ne_zero (Polynomial.map_ne_zero (generator E).denom_ne_zero) <|
        Polynomial.C_ne_zero.mpr H
    · refine ⟨Polynomial.C_injective.ne_iff.mp ?_, H⟩
      rw [map_zero, ← mul_ne_zero_iff_left <| Polynomial.map_ne_zero (generator E).denom_ne_zero]
      exact eq ▸ mul_ne_zero (Polynomial.map_ne_zero (num_ne_zero (generator_ne_zero h))) <|
        Polynomial.C_ne_zero.mpr H

Premises used: Polynomial.C, IsUnit, _private.0.RatFunc.Luroth.g, _private.0.RatFunc.Luroth.f, Polynomial.aeval, DFunLike.coe
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : Eq (α := F) ((aeval α : (a : K[X]) → F) (Q₂ h) : F) (0 : F)
eq :
  HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (g E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (f E)) : F[X]) =
    HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (f E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X])
isUnit₁ : IsUnit (M := F[X]) ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (f E)) : F[X])
⊢ IsUnit (M := F[X]) ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X])

Tactic:
obtain ⟨isUnit₁, isUnit₂⟩ :
      IsUnit (Polynomial.C <| aeval α (f E)) ∧ IsUnit (Polynomial.C <| aeval α (g E)) := by
    rw [Polynomial.isUnit_C, isUnit_iff_ne_zero, Polynomial.isUnit_C, isUnit_iff_ne_zero]
    obtain (H | H) := aeval_ne_zero_of_isCoprime (generator E).isCoprime_num_denom α
    · refine ⟨H, Polynomial.C_injective.ne_iff.mp ?_⟩
      rw [map_zero, ← mul_ne_zero_iff_left <| Polynomial.map_ne_zero <|
        num_ne_zero (generator_ne_zero h)]
      exact eq ▸ mul_ne_zero (Polynomial.map_ne_zero (generator E).denom_ne_zero) <|
        Polynomial.C_ne_zero.mpr H
    · refine ⟨Polynomial.C_injective.ne_iff.mp ?_, H⟩
      rw [map_zero, ← mul_ne_zero_iff_left <| Polynomial.map_ne_zero (generator E).denom_ne_zero]
      exact eq ▸ mul_ne_zero (Polynomial.map_ne_zero (num_ne_zero (generator_ne_zero h))) <|
        Polynomial.C_ne_zero.mpr H

Premises used: Polynomial.C, IsUnit, _private.0.RatFunc.Luroth.g, _private.0.RatFunc.Luroth.f, Polynomial.aeval, DFunLike.coe
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : Eq (α := F) ((aeval α : (a : K[X]) → F) (Q₂ h) : F) (0 : F)
eq :
  HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (g E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (f E)) : F[X]) =
    HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (f E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X])
isUnit₁ : IsUnit (M := F[X]) ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (f E)) : F[X])
isUnit₂ : IsUnit (M := F[X]) ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X])
⊢ IsCoprime (R := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (generator E).num : F[X])
    ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (generator E).denom : F[X])

Tactic:
have isCoprime := IsCoprime.map (generator E).isCoprime_num_denom <|
    Polynomial.mapRingHom (algebraMap K F)
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : Eq (α := F) ((aeval α : (a : K[X]) → F) (Q₂ h) : F) (0 : F)
eq :
  HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (g E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (f E)) : F[X]) =
    HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (f E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X])
isUnit₁ : IsUnit (M := F[X]) ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (f E)) : F[X])
isUnit₂ : IsUnit (M := F[X]) ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X])
isCoprime :
  IsCoprime (R := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (generator E).num : F[X])
    ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (generator E).denom : F[X])
rw :
  Associated ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (g E))
    (HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (f E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X]))
⊢ Associated (M := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (f E) : F[X])
    ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (g E) : F[X])

Tactic:
rw [← associated_mul_isUnit_left_iff isUnit₂, Associated.comm]

Premises used: Associated.comm, associated_mul_isUnit_left_iff
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : Eq (α := F) ((aeval α : (a : K[X]) → F) (Q₂ h) : F) (0 : F)
eq :
  HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (g E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (f E)) : F[X]) =
    HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (f E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X])
isUnit₁ : IsUnit (M := F[X]) ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (f E)) : F[X])
isUnit₂ : IsUnit (M := F[X]) ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X])
isCoprime :
  IsCoprime (R := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (generator E).num : F[X])
    ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (generator E).denom : F[X])
⊢ HMul.hMul (α := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (g E) : F[X])
      (↑isUnit₁.unit : F[X]) =
    HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (f E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X])

Tactic:
simpa
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : Eq (α := F) ((aeval α : (a : K[X]) → F) (Q₂ h) : F) (0 : F)
eq :
  HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (g E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (f E)) : F[X]) =
    HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (f E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X])
isUnit₁ : IsUnit (M := F[X]) ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (f E)) : F[X])
isUnit₂ : IsUnit (M := F[X]) ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X])
isCoprime :
  IsCoprime (R := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (generator E).num : F[X])
    ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (generator E).denom : F[X])
⊢ Associated ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (g E))
    (HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (f E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X]))

Tactic:
exact ⟨isUnit₁.unit, by simpa⟩
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : Eq (α := F) ((aeval α : (a : K[X]) → F) (Q₂ h) : F) (0 : F)
eq :
  HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (g E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (f E)) : F[X]) =
    HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (f E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X])
isUnit₁ : IsUnit (M := F[X]) ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (f E)) : F[X])
isUnit₂ : IsUnit (M := F[X]) ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X])
isCoprime :
  IsCoprime (R := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (generator E).num : F[X])
    ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (generator E).denom : F[X])
⊢ Associated (M := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (f E) : F[X])
    ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (g E) : F[X])

Tactic:
have : Associated ((f E).mapRingHom (algebraMap K F)) ((g E).mapRingHom (algebraMap K F)) := by
    rw [← associated_mul_isUnit_left_iff isUnit₂, Associated.comm]
    exact ⟨isUnit₁.unit, by simpa⟩
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : Eq (α := F) ((aeval α : (a : K[X]) → F) (Q₂ h) : F) (0 : F)
eq :
  HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (g E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (f E)) : F[X]) =
    HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (f E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X])
isUnit₁ : IsUnit (M := F[X]) ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (f E)) : F[X])
isUnit₂ : IsUnit (M := F[X]) ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X])
isCoprime :
  IsCoprime (R := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (generator E).num : F[X])
    ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (generator E).denom : F[X])
this :
  Associated (M := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (f E) : F[X])
    ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (g E) : F[X])
⊢ IsUnit (M := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (generator E).num : F[X]) ∧
    IsUnit (M := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (generator E).denom : F[X])

Tactic:
have := isCoprime.isUnit_of_associated this
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : Eq (α := F) ((aeval α : (a : K[X]) → F) (Q₂ h) : F) (0 : F)
eq :
  HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (g E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (f E)) : F[X]) =
    HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (f E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X])
isUnit₁ : IsUnit (M := F[X]) ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (f E)) : F[X])
isUnit₂ : IsUnit (M := F[X]) ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X])
isCoprime :
  IsCoprime (R := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (generator E).num : F[X])
    ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (generator E).denom : F[X])
this_1 :
  Associated (M := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (f E) : F[X])
    ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (g E) : F[X])
this :
  IsUnit (M := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (generator E).num : F[X]) ∧
    IsUnit (M := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (generator E).denom : F[X])
⊢ (generator E).num.natDegree = 0

Tactic:
simpa using (natDegree_eq_zero_of_isUnit this.1)

Premises used: And.left, Polynomial.natDegree_eq_zero_of_isUnit
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : Eq (α := F) ((aeval α : (a : K[X]) → F) (Q₂ h) : F) (0 : F)
eq :
  HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (g E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (f E)) : F[X]) =
    HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (f E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X])
isUnit₁ : IsUnit (M := F[X]) ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (f E)) : F[X])
isUnit₂ : IsUnit (M := F[X]) ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X])
isCoprime :
  IsCoprime (R := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (generator E).num : F[X])
    ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (generator E).denom : F[X])
this_1 :
  Associated (M := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (f E) : F[X])
    ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (g E) : F[X])
this :
  IsUnit (M := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (generator E).num : F[X]) ∧
    IsUnit (M := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (generator E).denom : F[X])
⊢ (generator E).denom.natDegree = 0

Tactic:
simpa using (natDegree_eq_zero_of_isUnit this.2)

Premises used: And.right, Polynomial.natDegree_eq_zero_of_isUnit
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : Eq (α := F) ((aeval α : (a : K[X]) → F) (Q₂ h) : F) (0 : F)
eq :
  HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (g E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (f E)) : F[X]) =
    HMul.hMul (α := F[X]) (β := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (f E) : F[X])
      ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X])
isUnit₁ : IsUnit (M := F[X]) ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (f E)) : F[X])
isUnit₂ : IsUnit (M := F[X]) ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X])
isCoprime :
  IsCoprime (R := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (generator E).num : F[X])
    ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (generator E).denom : F[X])
this_1 :
  Associated (M := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (f E) : F[X])
    ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (g E) : F[X])
this :
  IsUnit (M := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (generator E).num : F[X]) ∧
    IsUnit (M := F[X]) ((Polynomial.mapRingHom (algebraMap K F) : (a : K[X]) → F[X]) (generator E).denom : F[X])
⊢ (generator E).num.natDegree = 0 ∧ (generator E).denom.natDegree = 0

Tactic:
exact ⟨by simpa using (natDegree_eq_zero_of_isUnit this.1),
    by simpa using (natDegree_eq_zero_of_isUnit this.2)⟩
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (Polynomial.C : (a : K) → K[X]) (Q₃ h) = Q₂ h

Tactic:
(eq_C_of_natDegree_eq_zero (Q₂_natDegree h)).symm

Premises used: Polynomial.eq_C_of_natDegree_eq_zero, _private.0.RatFunc.Luroth.Q₂_natDegree, Eq.symm
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
rw : Polynomial.map Polynomial.C (Q₂ h) * Φ E = θ E
rw₁ rw₂ : θ E = θ E
⊢ Polynomial.map Polynomial.C ((Polynomial.C : (a : K) → K[X]) (Q₃ h)) * Φ E = θ E

Tactic:
rw [Q₃_map h, Q₂_mul_Φ h]

Premises used: _private.0.RatFunc.Luroth.Q₂_mul_Φ, _private.0.RatFunc.Luroth.Q₃_map
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (Polynomial.map Polynomial.C (Q₂ h) * Φ E).natDegree = (θ E).natDegree

Tactic:
have := congr($(Q₂_mul_Φ h).natDegree)