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 ≠ ⊥
⊢ 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)
have 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 sorry) : ↥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⟯))
                  sorry) :
              K⟮X⟯)) :
        K⟮X⟯[X])
      (Polynomial.map
        (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥E) K⟮X⟯)
            (↑(inclusion sorry) : ↥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)]
-- 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 ≠ ⊥
⊢ Membership.mem (γ := Subsemiring K⟮X⟯[X]) (lifts (R := K[X]) (algebraMap K[X] K⟮X⟯)) (Q₀ E)
have 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)
Tactic: apply (Φ' E).isPrimitive_primPart.mul_map_mem_lifts_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 ≠ ⊥
⊢ 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)
have rw : Membership.mem (γ := Subsemiring K⟮X⟯[X]) (lifts (R := K[X]) (algebraMap K[X] K⟮X⟯))
  (Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E))
Tactic: rw [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 ≠ ⊥
⊢ Membership.mem (γ := Subsemiring K⟮X⟯[X]) (lifts (R := K[X]) (algebraMap K[X] K⟮X⟯)) (Q₀ E)
have 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)
Tactic: classical
  apply (Φ' E).isPrimitive_primPart.mul_map_mem_lifts_iff.mp
  rw [Q₀_mul_Φ h]
  exact ⟨_, rfl⟩
-- 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 ≠ ⊥
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)
have apply₁ : Membership.mem (γ := Subsemiring K⟮X⟯[X]) (lifts (R := K[X]) (algebraMap K[X] K⟮X⟯))
  (Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E))
Tactic: classical
  apply (Φ' E).isPrimitive_primPart.mul_map_mem_lifts_iff.mp
  rw [Q₀_mul_Φ h]
  exact ⟨_, rfl⟩
-- 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 ≠ ⊥
⊢ Q₁ h ≠ 0
have 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)
Tactic: apply_fun Polynomial.map (algebraMap K[X] K⟮X⟯)
-- 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 ≠ ⊥
⊢ Ne (α := K⟮X⟯[X]) (Polynomial.map (algebraMap K[X] K⟮X⟯) (Q₁ h)) (Polynomial.map (R := K[X]) (algebraMap K[X] K⟮X⟯) 0)
have rw : Q₀ E ≠ 0
Tactic: rw [map_Q₁, Polynomial.map_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 ≠ ⊥
⊢ Q₁ h * Φ E = θ E
have apply_fun : Eq (α := K⟮X⟯[X]) (Polynomial.map (algebraMap K[X] K⟮X⟯) (Q₁ h * Φ E)) (Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E))
Tactic: apply_fun Polynomial.map (algebraMap K[X] K⟮X⟯) using
    Polynomial.map_injective _ (algebraMap_injective K)
-- 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 ≠ ⊥
⊢ Eq (α := K⟮X⟯[X]) (Polynomial.map (algebraMap K[X] K⟮X⟯) (Q₁ h * Φ E)) (Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E))
have rw : HMul.hMul (α := K⟮X⟯[X]) (Polynomial.map (algebraMap K[X] K⟮X⟯) (Q₁ h)) (Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)) =
  Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
Tactic: rw [Polynomial.map_mul, map_Q₁, 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 :
  HMul.hMul (α := K⟮X⟯[X]) (Polynomial.map (algebraMap K[X] K⟮X⟯) (Q₁ h))
      (Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
⊢ Eq (α := K⟮X⟯[X]) (Polynomial.map (algebraMap K[X] K⟮X⟯) (Q₁ h * Φ E)) (Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E))
have rw₁ : Q₀ E * Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E) = Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
Tactic: rw [Polynomial.map_mul, map_Q₁, 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 :
  HMul.hMul (α := K⟮X⟯[X]) (Polynomial.map (algebraMap K[X] K⟮X⟯) (Q₁ h))
      (Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
rw₁ : Q₀ E * Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E) = Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
⊢ Eq (α := K⟮X⟯[X]) (Polynomial.map (algebraMap K[X] K⟮X⟯) (Q₁ h * Φ E)) (Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E))
have rw₂ : Eq (α := K⟮X⟯[X]) (Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)) (Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E))
Tactic: rw [Polynomial.map_mul, map_Q₁, 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 ≠ ⊥
⊢ natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Q₁ h)) = 0
have this : Q₁ h * Φ E = θ E
Tactic: have : Q₁ h * Φ E = θ E := 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 ≠ ⊥
this : Q₁ h * Φ E = θ E
⊢ natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Q₁ h)) = 0
have this₁ : Eq (α := K[X][Y]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Q₁ h * Φ E) : K[X][Y])
  ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (θ E) : K[X][Y])
Tactic: apply_fun Bivariate.swap 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 ≠ ⊥
this :
  Eq (α := K[X][Y]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Q₁ h * Φ E) : K[X][Y])
    ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (θ E) : K[X][Y])
⊢ natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Q₁ h)) = 0
have this₁ : HMul.hMul (α := K[X][Y]) (β := K[X][Y]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Q₁ h) : K[X][Y])
    ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Φ E) : K[X][Y]) =
  (Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (θ E)
Tactic: rw [map_mul] 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 ≠ ⊥
this :
  HMul.hMul (α := K[X][Y]) (β := K[X][Y]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Q₁ h) : K[X][Y])
      ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Φ E) : K[X][Y]) =
    (Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (θ E)
⊢ natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Q₁ h)) = 0
have this₁ : (HMul.hMul (α := K[X][Y]) (β := K[X][Y]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Q₁ h) : K[X][Y])
      ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Φ E) : K[X][Y])).natDegree =
  natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (θ E))
Tactic: apply_fun natDegree 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 ≠ ⊥
this :
  (HMul.hMul (α := K[X][Y]) (β := K[X][Y]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Q₁ h) : K[X][Y])
        ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Φ E) : K[X][Y])).natDegree =
    natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (θ E))
⊢ natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Q₁ h)) = 0
have this₁ : natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Q₁ h)) +
    natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Φ E)) =
  natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (θ E))
Tactic: rw [natDegree_mul
    ((map_ne_zero_iff _ Bivariate.swap.injective).mpr (Q₁_ne_zero h))
    ((map_ne_zero_iff _ Bivariate.swap.injective).mpr (Φ_ne_zero h))] 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 :
  natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Q₁ h)) +
      natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Φ E)) =
    natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (θ E))
⊢ natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (θ E)) ≤ m E
have rw : (θ E).natDegree ≤ m E
Tactic: rw [swap_θ, natDegree_neg]
-- 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 ≠ ⊥
this :
  natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Q₁ h)) +
      natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Φ E)) =
    natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (θ E))
⊢ natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Q₁ h)) = 0
have h₁ : natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (θ E)) ≤ m E
Tactic: have h₁ : (Bivariate.swap (θ E)).natDegree ≤ m E := by
    rw [swap_θ, natDegree_neg]
    exact θ_natDegree_le 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 ≠ ⊥
this :
  Eq (α := K[X][Y]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Q₁ h) : K[X][Y])
    ((Polynomial.C : (a : K[X]) → K[X][Y]) (coeff ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Q₁ h)) 0) : K[X][Y])
⊢ Polynomial.map Polynomial.C (Q₂ h) = Q₁ h
have this₁ : Eq (α := K[X][Y])
  ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Q₁ h)) : K[X][Y])
  ((Bivariate.swap : (a : K[X][Y]) → K[X][Y])
      ((Polynomial.C : (a : K[X]) → K[X][Y]) (coeff ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Q₁ h)) 0)) :
    K[X][Y])
Tactic: apply_fun Bivariate.swap 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 ≠ ⊥
this :
  Eq (α := K[X][Y])
    ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Q₁ h)) : K[X][Y])
    ((Bivariate.swap : (a : K[X][Y]) → K[X][Y])
        ((Polynomial.C : (a : K[X]) → K[X][Y]) (coeff ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Q₁ h)) 0)) :
      K[X][Y])
⊢ Polynomial.map Polynomial.C (Q₂ h) = Q₁ h
have this₁ : Q₁ h = Polynomial.map Polynomial.C (coeff ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Q₁ h)) 0)
Tactic: rw [Bivariate.swap_swap_apply, Bivariate.swap_C] 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 ≠ ⊥
⊢ Q₂ h ≠ 0
have apply_fun : Polynomial.map Polynomial.C (Q₂ h) ≠ Polynomial.map Polynomial.C 0
Tactic: apply_fun Polynomial.map Polynomial.C
-- 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 (Q₂ h) ≠ Polynomial.map Polynomial.C 0
have rw : Q₁ h ≠ 0
Tactic: rw [Polynomial.map_zero, Q₂_map]
-- 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 (Q₂ h) * Φ E = θ E
have rw : 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 : Q₁ h * Φ E = θ E
⊢ Polynomial.map Polynomial.C (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 (goal)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (Q₂ h).natDegree = 0
have by_contra : ∀ (H : ¬(Q₂ h).natDegree = 0), False
Tactic: by_contra 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 ≠ ⊥
H : ¬(Q₂ h).natDegree = 0
⊢ False
have apply : (generator E).num.natDegree = 0 ∧ (generator E).denom.natDegree = 0
Tactic: apply (generator E).eq_C_iff.not.mp (generator_ne_C 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 ≠ ⊥
H : ¬(Q₂ h).natDegree = 0
F : Type u_1 := AlgebraicClosure K
⊢ (generator E).num.natDegree = 0 ∧ (generator E).denom.natDegree = 0
have H₁ : let F := AlgebraicClosure K;
¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
Tactic: rw [natDegree_eq_zero_iff_degree_le_zero.not, ← degree_map _ (algebraMap K F)] at H
Cleared hypotheses: H, 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
⊢ (generator E).num.natDegree = 0 ∧ (generator E).denom.natDegree = 0
have obtain : ∀ (α : F) (hα : (Polynomial.map (algebraMap K F) (Q₂ h)).IsRoot α),
  (generator E).num.natDegree = 0 ∧ (generator E).denom.natDegree = 0
Tactic: obtain ⟨α, hα⟩ := IsAlgClosed.exists_root ((Q₂ h).map (algebraMap K F)) (ne_of_not_ge H).symm
-- 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α : (Polynomial.map (algebraMap K F) (Q₂ h)).IsRoot α
⊢ (generator E).num.natDegree = 0 ∧ (generator E).denom.natDegree = 0
have hα₁ : Eq (α := F) ((aeval α : (a : K[X]) → F) (Q₂ h) : F) (0 : F)
Tactic: rw [IsRoot.def, eval_map_algebraMap] at hα
Cleared hypotheses: 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)
⊢ 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])
have this : Eq (α := F[X])
  (((aeval ((Polynomial.C : (a : F) → F[X]) α) : K[X][Y] →ₐ[K[X]] F[X]) : (a : K[X][Y]) → F[X]) (θ E) : F[X])
  (((aeval ((Polynomial.C : (a : F) → F[X]) α) : K[X][Y] →ₐ[K[X]] F[X]) : (a : K[X][Y]) → F[X])
      (Polynomial.map Polynomial.C (Q₂ h) * Φ E) :
    F[X])
Tactic: have := congr(aeval (Polynomial.C α) $(Q₂_mul_Φ h)).symm
-- 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)
this :
  ((aeval ((Polynomial.C : (a : F) → F[X]) α) : K[X][Y] →ₐ[K[X]] F[X]) : (a : K[X][Y]) → F[X]) (θ E) =
    HMul.hMul (α := F[X]) (β := F[X])
      (((aeval ((Polynomial.C : (a : F) → F[X]) α) : K[X][Y] →ₐ[K[X]] F[X]) : (a : K[X][Y]) → F[X])
          (Polynomial.map Polynomial.C (Q₂ h)) :
        F[X])
      (((aeval ((Polynomial.C : (a : F) → F[X]) α) : K[X][Y] →ₐ[K[X]] F[X]) : (a : K[X][Y]) → F[X]) (Φ E) : F[X])
⊢ Eq (α := K →+* F[X]) (RingHom.comp (algebraMap K[X] F[X]) Polynomial.C) (RingHom.comp Polynomial.C (algebraMap K F))
have a : ∀ (x : K) (n : ℕ),
  Eq.{u_1 + 1} (α := F) (coeff ((RingHom.comp (algebraMap K[X] F[X]) Polynomial.C : (a : K) → F[X]) x) n)
    (coeff ((RingHom.comp Polynomial.C (algebraMap K F) : (a : K) → F[X]) x) n)
Tactic: ext
-- 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)
this :
  HMul.hMul (α := F[X]) (β := F[X]) ((algebraMap K[X] F[X] : (a : K[X]) → F[X]) (g E) : F[X])
        (((aeval ((Polynomial.C : (a : F) → F[X]) α) : K[X][Y] →ₐ[K[X]] F[X]) : (a : K[X][Y]) → F[X])
            (Polynomial.map Polynomial.C (f E)) :
          F[X]) -
      HMul.hMul (α := F[X]) (β := F[X]) ((algebraMap K[X] F[X] : (a : K[X]) → F[X]) (f E) : F[X])
        (((aeval ((Polynomial.C : (a : F) → F[X]) α) : K[X][Y] →ₐ[K[X]] F[X]) : (a : K[X][Y]) → F[X])
            (Polynomial.map Polynomial.C (g E)) :
          F[X]) =
    0
⊢ Eq (α := K →+* F[X]) (RingHom.comp (algebraMap K[X] F[X]) Polynomial.C) (RingHom.comp Polynomial.C (algebraMap K F))
have a : ∀ (x : K) (n : ℕ),
  Eq.{u_1 + 1} (α := F) (coeff ((RingHom.comp (algebraMap K[X] F[X]) Polynomial.C : (a : K) → F[X]) x) n)
    (coeff ((RingHom.comp Polynomial.C (algebraMap K F) : (a : K) → F[X]) x) n)
Tactic: ext
-- 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)
this :
  HMul.hMul (α := F[X]) (β := F[X]) ((algebraMap K[X] F[X] : (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]) ((algebraMap K[X] F[X] : (a : K[X]) → F[X]) (f E) : F[X])
        (((aeval ((Polynomial.C : (a : F) → F[X]) α) : K[X][Y] →ₐ[K[X]] F[X]) : (a : K[X][Y]) → F[X])
            (Polynomial.map Polynomial.C (g E)) :
          F[X]) =
    0
⊢ Eq (α := K →+* F[X]) (RingHom.comp (algebraMap K[X] F[X]) Polynomial.C) (RingHom.comp Polynomial.C (algebraMap K F))
have a : ∀ (x : K) (n : ℕ),
  Eq.{u_1 + 1} (α := F) (coeff ((RingHom.comp (algebraMap K[X] F[X]) Polynomial.C : (a : K) → F[X]) x) n)
    (coeff ((RingHom.comp Polynomial.C (algebraMap K F) : (a : K) → F[X]) x) n)
Tactic: ext
-- 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)
⊢ (generator E).num.natDegree = 0 ∧ (generator E).denom.natDegree = 0
have 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])
Tactic: have eq :
      (Polynomial.mapRingHom (algebraMap K F)) (g E) * Polynomial.C ((aeval α) (f E)) =
      (Polynomial.mapRingHom (algebraMap K F)) (f E) * Polynomial.C ((aeval α) (g E)) := by
    have := congr(aeval (Polynomial.C α) $(Q₂_mul_Φ h)).symm
    rwa [aeval_mul, ← map_aeval_eq_aeval_map (by ext; simp), hα, map_zero, zero_mul, aeval_sub,
      aeval_mul, aeval_mul, aeval_C, aeval_C, ← map_aeval_eq_aeval_map (by ext; simp),
      ← map_aeval_eq_aeval_map (by ext; simp), algebraMap_def, coe_mapRingHom, sub_eq_zero,
      ← Polynomial.coe_mapRingHom] at 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 ≠ ⊥
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]) ∧
    IsUnit (M := F[X]) ((Polynomial.C : (a : F) → F[X]) ((aeval α : (a : K[X]) → F) (g E)) : F[X])
have rw : 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: rw [Polynomial.isUnit_C, isUnit_iff_ne_zero, Polynomial.isUnit_C, isUnit_iff_ne_zero]