awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
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])
⊢ Ne (α := F) ((aeval α : (a : K[X]) → F) (f E) : F) (0 : F) ∧
    Ne (α := F) ((aeval α : (a : K[X]) → F) (g E) : F) (0 : F)
have inl : ∀ (H : Ne (α := F) ((aeval α : (a : K[X]) → F) (generator E).num : 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: obtain (H | H) := aeval_ne_zero_of_isCoprime (generator E).isCoprime_num_denom α
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
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])
inl :
  ∀ (H : Ne (α := F) ((aeval α : (a : K[X]) → F) (generator E).num : 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)
⊢ Ne (α := F) ((aeval α : (a : K[X]) → F) (f E) : F) (0 : F) ∧
    Ne (α := F) ((aeval α : (a : K[X]) → F) (g E) : F) (0 : F)
have inr : ∀ (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: obtain (H | H) := aeval_ne_zero_of_isCoprime (generator E).isCoprime_num_denom α
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
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)
⊢ Ne (α := F) ((aeval α : (a : K[X]) → F) (f E) : F) (0 : F) ∧
    Ne (α := F) ((aeval α : (a : K[X]) → F) (g E) : F) (0 : F)
have 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])
Tactic: refine ⟨H, Polynomial.C_injective.ne_iff.mp ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
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)
⊢ 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])
have 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
Tactic: rw [map_zero, ← mul_ne_zero_iff_left <| Polynomial.map_ne_zero <|
        num_ne_zero (generator_ne_zero h)]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
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
⊢ 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])
have rw : K →+* F
Tactic: rw [map_zero, ← mul_ne_zero_iff_left <| Polynomial.map_ne_zero <|
        num_ne_zero (generator_ne_zero h)]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
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)
have 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])
Tactic: refine ⟨Polynomial.C_injective.ne_iff.mp ?_, H⟩
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
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[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])
have 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
Tactic: rw [map_zero, ← mul_ne_zero_iff_left <| Polynomial.map_ne_zero (generator E).denom_ne_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
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
⊢ 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])
have rw : K →+* F
Tactic: rw [map_zero, ← mul_ne_zero_iff_left <| Polynomial.map_ne_zero (generator E).denom_ne_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (hypothesis)
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])
⊢ (generator E).num.natDegree = 0 ∧ (generator E).denom.natDegree = 0
have isUnit₁ : 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
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (hypothesis)
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])
⊢ (generator E).num.natDegree = 0 ∧ (generator E).denom.natDegree = 0
have isUnit₂ : 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
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (hypothesis)
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])
⊢ (generator E).num.natDegree = 0 ∧ (generator E).denom.natDegree = 0
have 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])
Tactic: have isCoprime := IsCoprime.map (generator E).isCoprime_num_denom <|
    Polynomial.mapRingHom (algebraMap K F)
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
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])
have 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]))
Tactic: rw [← associated_mul_isUnit_left_iff isUnit₂, Associated.comm]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (hypothesis)
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])
⊢ (generator E).num.natDegree = 0 ∧ (generator E).denom.natDegree = 0
have 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])
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⟩
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (hypothesis)
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])
⊢ (generator E).num.natDegree = 0 ∧ (generator E).denom.natDegree = 0
have 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])
Tactic: have := isCoprime.isUnit_of_associated this
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.map Polynomial.C ((Polynomial.C : (a : K) → K[X]) (Q₃ h)) * Φ E = θ E
have rw : Polynomial.map Polynomial.C (Q₂ h) * Φ E = θ E
Tactic: rw [Q₃_map h, Q₂_mul_Φ h]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
rw : Polynomial.map Polynomial.C (Q₂ h) * Φ E = θ E
⊢ Polynomial.map Polynomial.C ((Polynomial.C : (a : K) → K[X]) (Q₃ h)) * Φ E = θ E
have rw₁ : θ E = θ E
Tactic: rw [Q₃_map h, Q₂_mul_Φ h]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (hypothesis)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (Φ E).natDegree = (θ E).natDegree
have this : (Polynomial.map Polynomial.C (Q₂ h) * Φ E).natDegree = (θ E).natDegree
Tactic: have := congr($(Q₂_mul_Φ h).natDegree)
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this : (Polynomial.map Polynomial.C (Q₂ h) * Φ E).natDegree = (θ E).natDegree
⊢ (Φ E).natDegree = (θ E).natDegree
have rwa : ∀ (this : (Polynomial.map Polynomial.C (Q₂ h)).natDegree + (Φ E).natDegree = (θ E).natDegree),
  (Φ E).natDegree = (θ E).natDegree
Tactic: rwa [natDegree_mul (Polynomial.map_ne_zero (Q₂_ne_zero h)) (Φ_ne_zero h), natDegree_map,
    Q₂_natDegree h, zero_add] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this : (Polynomial.map Polynomial.C (Q₂ h) * Φ E).natDegree = (θ E).natDegree
rwa :
  ∀ (this : (Polynomial.map Polynomial.C (Q₂ h)).natDegree + (Φ E).natDegree = (θ E).natDegree),
    (Φ E).natDegree = (θ E).natDegree
⊢ (Φ E).natDegree = (θ E).natDegree
have rwa₁ : ∀ (this : (Q₂ h).natDegree + (Φ E).natDegree = (θ E).natDegree), (Φ E).natDegree = (θ E).natDegree
Tactic: rwa [natDegree_mul (Polynomial.map_ne_zero (Q₂_ne_zero h)) (Φ_ne_zero h), natDegree_map,
    Q₂_natDegree h, zero_add] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this : (Polynomial.map Polynomial.C (Q₂ h) * Φ E).natDegree = (θ E).natDegree
rwa :
  ∀ (this : (Polynomial.map Polynomial.C (Q₂ h)).natDegree + (Φ E).natDegree = (θ E).natDegree),
    (Φ E).natDegree = (θ E).natDegree
rwa₁ : ∀ (this : (Q₂ h).natDegree + (Φ E).natDegree = (θ E).natDegree), (Φ E).natDegree = (θ E).natDegree
⊢ (Φ E).natDegree = (θ E).natDegree
have rwa₂ : ∀ (this : 0 + (Φ E).natDegree = (θ E).natDegree), (Φ E).natDegree = (θ E).natDegree
Tactic: rwa [natDegree_mul (Polynomial.map_ne_zero (Q₂_ne_zero h)) (Φ_ne_zero h), natDegree_map,
    Q₂_natDegree h, zero_add] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this : (Polynomial.map Polynomial.C (Q₂ h) * Φ E).natDegree = (θ E).natDegree
rwa :
  ∀ (this : (Polynomial.map Polynomial.C (Q₂ h)).natDegree + (Φ E).natDegree = (θ E).natDegree),
    (Φ E).natDegree = (θ E).natDegree
rwa₁ : ∀ (this : (Q₂ h).natDegree + (Φ E).natDegree = (θ E).natDegree), (Φ E).natDegree = (θ E).natDegree
rwa₂ : ∀ (this : 0 + (Φ E).natDegree = (θ E).natDegree), (Φ E).natDegree = (θ E).natDegree
⊢ (Φ E).natDegree = (θ E).natDegree
have rwa₃ : ∀ (this : (Φ E).natDegree = (θ E).natDegree), (Φ E).natDegree = (θ E).natDegree
Tactic: rwa [natDegree_mul (Polynomial.map_ne_zero (Q₂_ne_zero h)) (Φ_ne_zero h), natDegree_map,
    Q₂_natDegree h, zero_add] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (hypothesis)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Φ E)) = (θ E).natDegree
have this : natDegree.{u_1} (R := K[X])
    ((Bivariate.swap : (a : K[X][Y]) → K[X][Y])
      (Polynomial.map Polynomial.C ((Polynomial.C : (a : K) → K[X]) (Q₃ h)) * Φ E)) =
  natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (θ E))
Tactic: have := congr((Bivariate.swap $(Q₃_mul_Φ h)).natDegree)