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 ≠ ⊥
apply_fun :
  Eq (α := K⟮X⟯[X]) (Polynomial.map (algebraMap K[X] K⟮X⟯) (Q₁ h * Φ E)) (Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E))
⊢ Q₁ h * Φ E = θ E

Tactic:
apply_fun Polynomial.map (algebraMap K[X] K⟮X⟯) using
    Polynomial.map_injective _ (algebraMap_injective K)

Premises used: Algebra.algebraMap, Polynomial.map_injective, Polynomial, RatFunc, RatFunc.algebraMap_injective, Polynomial.map
-- 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]) (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)
rw₂ rw₃ : Eq (α := K⟮X⟯[X]) (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))

Tactic:
rw [Polynomial.map_mul, map_Q₁, Q₀_mul_Φ h]

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

Tactic:
have : Q₁ h * Φ E = θ E := Q₁_mul_Φ h
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this : Q₁ h * Φ E = θ E
⊢ 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

Premises used: Polynomial.Bivariate.swap
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
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])
⊢ 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

Premises used: map_mul
-- 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][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)
⊢ (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

Premises used: Polynomial.natDegree
-- 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][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)) +
      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

Premises used: Iff.mpr, Polynomial.natDegree_mul, _private.0.RatFunc.Luroth.Q₁_ne_zero, Polynomial.Bivariate.swap, AlgEquiv.injective, map_ne_zero_iff, _private.0.RatFunc.Luroth.Φ_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
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))
rw : (θ E).natDegree ≤ m E
⊢ natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (θ E)) ≤ m E

Tactic:
rw [swap_θ, natDegree_neg]

Premises used: Polynomial.natDegree_neg, _private.0.RatFunc.Luroth.swap_θ
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
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))
⊢ (θ E).natDegree ≤ m E

Tactic:
θ_natDegree_le h

Premises used: _private.0.RatFunc.Luroth.θ_natDegree_le
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
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))
⊢ (θ E).natDegree ≤ m E

Tactic:
exact θ_natDegree_le h

Premises used: _private.0.RatFunc.Luroth.θ_natDegree_le
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
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

Tactic:
have h₁ : (Bivariate.swap (θ E)).natDegree ≤ m E := by
    rw [swap_θ, natDegree_neg]
    exact θ_natDegree_le h
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
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))
h₁ : natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (θ E)) ≤ m E
⊢ natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Q₁ h)) = 0

Tactic:
grind [m_le_swap_Φ_natDegree h]

Premises used: _private.0.RatFunc.Luroth.m_le_swap_Φ_natDegree
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
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])
⊢ 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

Premises used: Polynomial.Bivariate.swap
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
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])
⊢ 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

Premises used: Polynomial.Bivariate.swap_swap_apply, Polynomial.Bivariate.swap_C
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this : Q₁ h = Polynomial.map Polynomial.C (coeff ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Q₁ h)) 0)
⊢ Polynomial.map Polynomial.C (Q₂ h) = Q₁ h

Tactic:
this.symm

Premises used: Eq.symm
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this : Q₁ h = Polynomial.map Polynomial.C (coeff ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Q₁ h)) 0)
⊢ Polynomial.map Polynomial.C (Q₂ h) = Q₁ h

Tactic:
exact this.symm

Premises used: Eq.symm
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
apply_fun : Polynomial.map Polynomial.C (Q₂ h) ≠ Polynomial.map Polynomial.C 0
⊢ Q₂ h ≠ 0

Tactic:
apply_fun Polynomial.map Polynomial.C

Premises used: Polynomial.C, Polynomial.map
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
rw : Q₁ h ≠ 0
⊢ Polynomial.map Polynomial.C (Q₂ h) ≠ Polynomial.map Polynomial.C 0

Tactic:
rw [Polynomial.map_zero, Q₂_map]

Premises used: _private.0.RatFunc.Luroth.Q₂_map, Polynomial.map_zero
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Q₁ h ≠ 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₁ h ≠ 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 ≠ ⊥
rw : Q₁ h * Φ E = θ E
rw₁ rw₂ : θ E = θ E
⊢ Polynomial.map Polynomial.C (Q₂ h) * Φ E = θ E

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

Premises used: _private.0.RatFunc.Luroth.Q₂_map, _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 ≠ ⊥
by_contra : ∀ (H : ¬(Q₂ h).natDegree = 0), False
⊢ (Q₂ h).natDegree = 0

Tactic:
by_contra H
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
H : ¬(Q₂ h).natDegree = 0
apply : (generator E).num.natDegree = 0 ∧ (generator E).denom.natDegree = 0
⊢ False

Tactic:
apply (generator E).eq_C_iff.not.mp (generator_ne_C h)

Premises used: Iff.not, RatFunc.Luroth.generator_ne_C, Iff.mp, RatFunc.Luroth.generator, RatFunc.eq_C_iff
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
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
⊢ 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

Premises used: Algebra.algebraMap, Iff.not, Polynomial.natDegree_eq_zero_iff_degree_le_zero, Polynomial.degree_map
-- 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
obtain :
  ∀ (α : F) (hα : (Polynomial.map (algebraMap K F) (Q₂ h)).IsRoot α),
    (generator E).num.natDegree = 0 ∧ (generator E).denom.natDegree = 0
⊢ (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

Premises used: Algebra.algebraMap, Ne.symm, _private.0.RatFunc.Luroth.Q₂, IsAlgClosed.exists_root, Polynomial.map, ne_of_not_ge
-- 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α : (Polynomial.map (algebraMap K F) (Q₂ h)).IsRoot α
⊢ Eq (α := F) ((aeval α : (a : K[X]) → F) (Q₂ h) : F) (0 : F)

Tactic:
rw [IsRoot.def, eval_map_algebraMap] at hα

Premises used: Polynomial.IsRoot.def, Polynomial.eval_map_algebraMap
-- 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 (α := 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
-- 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)
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])
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)
⊢ Eq (α := K →+* F[X]) (RingHom.comp (algebraMap K[X] F[X]) Polynomial.C) (RingHom.comp Polynomial.C (algebraMap K F))

Tactic:
ext
-- 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)
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])
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:
simp
-- 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)
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
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)
⊢ Eq (α := K →+* F[X]) (RingHom.comp (algebraMap K[X] F[X]) Polynomial.C) (RingHom.comp Polynomial.C (algebraMap K F))

Tactic:
ext
-- 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)
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
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:
simp
-- 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)
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
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)
⊢ Eq (α := K →+* F[X]) (RingHom.comp (algebraMap K[X] F[X]) Polynomial.C) (RingHom.comp Polynomial.C (algebraMap K F))

Tactic:
ext
-- 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)
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
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:
simp
-- 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)
⊢ 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
-- 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])
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)
⊢ 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:
rw [Polynomial.isUnit_C, isUnit_iff_ne_zero, Polynomial.isUnit_C, isUnit_iff_ne_zero]

Premises used: Polynomial.isUnit_C, isUnit_iff_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])
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)
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)
⊢ 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 α

Premises used: RatFunc.isCoprime_num_denom, Polynomial.aeval_ne_zero_of_isCoprime, RatFunc.Luroth.generator
-- 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)
⊢ 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:
⟨H, Polynomial.C_injective.ne_iff.mp ?_⟩

Premises used: Function.Injective.ne_iff, And.intro, Iff.mp, Polynomial.C_injective