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 :
  Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (generatorIndex h)) : K⟮X⟯)
    ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) 0 : K⟮X⟯)
⊢ (Φ E).coeff (generatorIndex h) ≠ 0

Tactic:
apply_fun algebraMap K[X] K⟮X⟯

Premises used: Algebra.algebraMap, Polynomial, RatFunc
-- 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⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮X⟯) (generator E) ≠ 0
⊢ Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (generatorIndex h)) : K⟮X⟯)
    ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) 0 : K⟮X⟯)

Tactic:
rw [map_zero, Φ_coeff_generatorIndex h]

Premises used: map_zero, _private.0.RatFunc.Luroth.Φ_coeff_generatorIndex
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ HMul.hMul (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮X⟯) (generator E) ≠ 0

Tactic:
mul_ne_zero_iff.mpr ⟨algebraMap_ne_zero (num_ne_zero (c_ne_zero h)), generator_ne_zero h⟩

Premises used: Iff.mpr, _private.0.RatFunc.Luroth.c_ne_zero, RatFunc.Luroth.generator_ne_zero, RatFunc.algebraMap_ne_zero, RatFunc.num_ne_zero, And.intro, mul_ne_zero_iff
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ HMul.hMul (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮X⟯) (generator E) ≠ 0

Tactic:
exact mul_ne_zero_iff.mpr ⟨algebraMap_ne_zero (num_ne_zero (c_ne_zero h)), generator_ne_zero h⟩

Premises used: Iff.mpr, _private.0.RatFunc.Luroth.c_ne_zero, RatFunc.Luroth.generator_ne_zero, RatFunc.algebraMap_ne_zero, RatFunc.num_ne_zero, And.intro, mul_ne_zero_iff
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
rw :
  ∃ (p : K[X]),
    generator E =
      HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮X⟯)
⊢ g E ∣ (c E).num

Tactic:
rw [denom_dvd (num_ne_zero (c_ne_zero h))]

Premises used: _private.0.RatFunc.Luroth.c_ne_zero, RatFunc.num_ne_zero, RatFunc.denom_dvd
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
h₁ :
  generator E =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (generatorIndex h)) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮X⟯)
⊢ ∃ (p : K[X]),
    generator E =
      HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮X⟯)

Tactic:
use (Φ E).coeff (generatorIndex h)

Premises used: Polynomial.coeff, _private.0.RatFunc.Luroth.generatorIndex, _private.0.RatFunc.Luroth.Φ
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
h₁ :
  generator E =
    HDiv.hDiv (β := K⟮X⟯)
      (HMul.hMul (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮X⟯) (generator E))
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮X⟯)
h₂ h₃ : generator E = generator E
⊢ generator E =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (generatorIndex h)) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮X⟯)

Tactic:
rw [Φ_coeff_generatorIndex h,
    mul_div_cancel_left₀ _ (algebraMap_ne_zero (num_ne_zero (c_ne_zero h)))]

Premises used: _private.0.RatFunc.Luroth.c_ne_zero, RatFunc.algebraMap_ne_zero, RatFunc.num_ne_zero, mul_div_cancel_left₀, _private.0.RatFunc.Luroth.Φ_coeff_generatorIndex
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
H : Φ E = 0
⊢ (c E).num = coeff 0 (φ E).natDegree

Tactic:
have := Φ_coeff_φ_natDegree' h ▸ congr($(H).coeff (φ E).natDegree)
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
H : Φ E = 0
this : (c E).num = coeff 0 (φ E).natDegree
⊢ (c E).num = 0

Tactic:
rw [coeff_zero] at this

Premises used: Polynomial.coeff_zero
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
H : Φ E = 0
this : (c E).num = 0
⊢ False

Tactic:
num_ne_zero (c_ne_zero h) this

Premises used: _private.0.RatFunc.Luroth.c_ne_zero, RatFunc.num_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
H : Φ E = 0
this : (c E).num = 0
⊢ False

Tactic:
exact num_ne_zero (c_ne_zero h) this

Premises used: _private.0.RatFunc.Luroth.c_ne_zero, RatFunc.num_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ HMul.hMul (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (generatorIndex h)) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯) =
    HMul.hMul (β := K⟮X⟯)
      (HMul.hMul (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮X⟯) (generator E))
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯)

Tactic:
have := congr($(Φ_coeff_generatorIndex h) * algebraMap K[X] K⟮X⟯ (g E))
-- 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⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (generatorIndex h)) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯) =
    HMul.hMul (β := K⟮X⟯)
      (HMul.hMul (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮X⟯) (generator E))
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯)
enter : generator E
| HMul.hMul (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (generatorIndex h)) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯) =
    HMul.hMul (β := K⟮X⟯)
      (HMul.hMul (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮X⟯) (generator E))
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯)

Tactic:
enter [2, 1, 2]
-- 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⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (generatorIndex h)) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯) =
    HMul.hMul (β := K⟮X⟯)
      (HMul.hMul (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮X⟯) (generator E))
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯)
rw :
  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⟯)
| generator E

Tactic:
rw [← num_div_denom (generator E)]

Premises used: RatFunc.Luroth.generator, RatFunc.num_div_denom
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  HMul.hMul (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (generatorIndex h)) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯) =
    HMul.hMul (β := K⟮X⟯)
      (HMul.hMul (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮X⟯) (generator E))
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯)
enter :
  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⟯)
| HMul.hMul (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (generatorIndex h)) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯) =
    HMul.hMul (β := K⟮X⟯)
      (HMul.hMul (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮X⟯) (generator E))
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯)

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

Premises used: RatFunc.Luroth.generator, RatFunc.num_div_denom
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  HMul.hMul (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (generatorIndex h)) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯) =
    HMul.hMul (β := K⟮X⟯)
      (HMul.hMul (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮X⟯) (generator E))
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯)
⊢ HMul.hMul (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (generatorIndex h)) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯) =
    HMul.hMul (β := K⟮X⟯)
      (HMul.hMul (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮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⟯)))
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯)

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

Premises used: RatFunc.Luroth.generator, RatFunc.num_div_denom
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  HMul.hMul (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (generatorIndex h)) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯) =
    HMul.hMul (β := K⟮X⟯)
      (HMul.hMul (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮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⟯)))
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯)
⊢ Eq (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (generatorIndex h) * g E) : K⟮X⟯)
    ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((c E).num * (generator E).num) : K⟮X⟯)

Tactic:
rw [mul_assoc, div_mul_cancel₀ _ (algebraMap_ne_zero (generator E).denom_ne_zero),
    ← map_mul, ← map_mul] at this

Premises used: div_mul_cancel₀, mul_assoc, RatFunc.algebraMap_ne_zero, map_mul, RatFunc.Luroth.generator, RatFunc.denom_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  Eq (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (generatorIndex h) * g E) : K⟮X⟯)
    ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((c E).num * (generator E).num) : K⟮X⟯)
⊢ ((Φ E).coeff (generatorIndex h) * g E).natDegree = ((c E).num * (generator E).num).natDegree

Tactic:
replace this := congr($(algebraMap_injective K this).natDegree)
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this : ((Φ E).coeff (generatorIndex h) * g E).natDegree = ((c E).num * (generator E).num).natDegree
⊢ ((Φ E).coeff (generatorIndex h)).natDegree + (generator E).denom.natDegree =
    (c E).num.natDegree + (generator E).num.natDegree

Tactic:
rw [natDegree_mul (Φ_coeff_generatorIndex_ne_zero h) (generator E).denom_ne_zero,
    natDegree_mul (num_ne_zero (c_ne_zero h)) (num_ne_zero (generator_ne_zero h))] at this

Premises used: _private.0.RatFunc.Luroth.c_ne_zero, Polynomial.natDegree_mul, RatFunc.Luroth.generator_ne_zero, RatFunc.num_ne_zero, _private.0.RatFunc.Luroth.Φ_coeff_generatorIndex_ne_zero, RatFunc.Luroth.generator, RatFunc.denom_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  ((Φ E).coeff (generatorIndex h)).natDegree + (generator E).denom.natDegree =
    (c E).num.natDegree + (generator E).num.natDegree
⊢ (f E).natDegree ≤ ((Φ E).coeff (generatorIndex h)).natDegree

Tactic:
grind [natDegree_le_of_dvd (generator_denom_dvd_c_num h) (num_ne_zero (c_ne_zero h))]

Premises used: _private.0.RatFunc.Luroth.c_ne_zero, _private.0.RatFunc.Luroth.generator_denom_dvd_c_num, RatFunc.num_ne_zero, Polynomial.natDegree_le_of_dvd
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
rw : (g E).natDegree ≤ (c E).num.natDegree
⊢ (g E).natDegree ≤ ((Φ E).coeff (φ E).natDegree).natDegree

Tactic:
rw [Φ_coeff_φ_natDegree' h]

Premises used: _private.0.RatFunc.Luroth.Φ_coeff_φ_natDegree'
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (g E).natDegree ≤ (c E).num.natDegree

Tactic:
natDegree_le_of_dvd (generator_denom_dvd_c_num h) (num_ne_zero (c_ne_zero h))

Premises used: _private.0.RatFunc.Luroth.c_ne_zero, _private.0.RatFunc.Luroth.generator_denom_dvd_c_num, RatFunc.num_ne_zero, Polynomial.natDegree_le_of_dvd
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (g E).natDegree ≤ (c E).num.natDegree

Tactic:
exact natDegree_le_of_dvd (generator_denom_dvd_c_num h) (num_ne_zero (c_ne_zero h))

Premises used: _private.0.RatFunc.Luroth.c_ne_zero, _private.0.RatFunc.Luroth.generator_denom_dvd_c_num, RatFunc.num_ne_zero, Polynomial.natDegree_le_of_dvd
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
rw :
  m E ≤
    natDegree.{u_1} (R := K[X])
      (∑ x ∈ (Φ E).support,
        (Bivariate.swap : (a : K[X][Y]) → K[X][Y]) ((monomial x : (a : K[X]) → K[X][Y]) ((Φ E).coeff x)))
⊢ m E ≤ natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Φ E))

Tactic:
rw [← sum_monomial_eq (Φ E), sum_def, map_sum]

Premises used: Polynomial.sum_monomial_eq, map_sum, Polynomial.sum_def, _private.0.RatFunc.Luroth.Φ
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
h₁ : ∀ (x : ℕ), (Bivariate.swap : (a : K[X][Y]) → K[X][Y]) ((monomial x : (a : K[X]) → K[X][Y]) ((Φ E).coeff x))
| fun (x : ℕ) ↦ (Bivariate.swap : (a : K[X][Y]) → K[X][Y]) ((monomial x : (a : K[X]) → K[X][Y]) ((Φ E).coeff x))

Tactic:
ext
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
x : ℕ
h₁ :
  HSMul.hSMul (α := K[X]) (β := K[X][Y]) ((monomial x : (a : K) → K[X]) 1)
    (Polynomial.map (algebraMap K K[X]) ((Φ E).coeff x))
| (Bivariate.swap : (a : K[X][Y]) → K[X][Y]) ((monomial x : (a : K[X]) → K[X][Y]) ((Φ E).coeff x))

Tactic:
rw [Bivariate.swap_monomial, mul_comm, ← Polynomial.smul_eq_C_mul,
      ← monomial_one_right_eq_X_pow, ← Polynomial.algebraMap_eq]

Premises used: Polynomial.smul_eq_C_mul, Polynomial.Bivariate.swap_monomial, mul_comm, Polynomial.monomial_one_right_eq_X_pow, Polynomial.algebraMap_eq
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
h₁ :
  ∀ (x : ℕ),
    HSMul.hSMul (α := K[X]) (β := K[X][Y]) ((monomial x : (a : K) → K[X]) 1)
      (Polynomial.map (algebraMap K K[X]) ((Φ E).coeff x))
| fun (x : ℕ) ↦ (Bivariate.swap : (a : K[X][Y]) → K[X][Y]) ((monomial x : (a : K[X]) → K[X][Y]) ((Φ E).coeff x))

Tactic:
ext
    rw [Bivariate.swap_monomial, mul_comm, ← Polynomial.smul_eq_C_mul,
      ← monomial_one_right_eq_X_pow, ← Polynomial.algebraMap_eq]

Premises used: Polynomial.smul_eq_C_mul, Polynomial.Bivariate.swap_monomial, mul_comm, Polynomial.monomial_one_right_eq_X_pow, Polynomial.algebraMap_eq
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
conv :
  m E ≤
    natDegree.{u_1} (R := K[X])
      (∑ x ∈ (Φ E).support,
        HSMul.hSMul (α := K[X]) (β := K[X][Y]) ((monomial x : (a : K) → K[X]) 1)
          (Polynomial.map (algebraMap K K[X]) ((Φ E).coeff x)))
⊢ m E ≤
    natDegree.{u_1} (R := K[X])
      (∑ x ∈ (Φ E).support,
        (Bivariate.swap : (a : K[X][Y]) → K[X][Y]) ((monomial x : (a : K[X]) → K[X][Y]) ((Φ E).coeff x)))

Tactic:
conv in (fun _ ↦ _) =>
    ext
    rw [Bivariate.swap_monomial, mul_comm, ← Polynomial.smul_eq_C_mul,
      ← monomial_one_right_eq_X_pow, ← Polynomial.algebraMap_eq]

Premises used: Polynomial.smul_eq_C_mul, Polynomial.Bivariate.swap_monomial, mul_comm, Polynomial.monomial_one_right_eq_X_pow, Polynomial.algebraMap_eq
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
rw : m E ≤ (Φ E).support.sup fun (i : ℕ) ↦ ((Φ E).coeff i).natDegree
⊢ m E ≤
    natDegree.{u_1} (R := K[X])
      (∑ x ∈ (Φ E).support,
        HSMul.hSMul (α := K[X]) (β := K[X][Y]) ((monomial x : (a : K) → K[X]) 1)
          (Polynomial.map (algebraMap K K[X]) ((Φ E).coeff x)))

Tactic:
rw [natDegree_sum_eq_of_linearIndepOn _
    (coe_basisMonomials K ▸ (basisMonomials K).linearIndepOn (Φ E).support)]

Premises used: Polynomial.natDegree_sum_eq_of_linearIndepOn
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
h₁ : (f E).natDegree ≤ (Φ E).support.sup fun (i : ℕ) ↦ ((Φ E).coeff i).natDegree
h₂ : (g E).natDegree ≤ (Φ E).support.sup fun (i : ℕ) ↦ ((Φ E).coeff i).natDegree
⊢ m E ≤ (Φ E).support.sup fun (i : ℕ) ↦ ((Φ E).coeff i).natDegree

Tactic:
apply max_le

Premises used: max_le
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (f E).natDegree ≤ (Φ E).support.sup fun (i : ℕ) ↦ ((Φ E).coeff i).natDegree

Tactic:
(le_Φ_coeff_generatorIndex_natDegree h).trans <|
      Finset.le_sup (f := fun i ↦ ((Φ E).coeff i).natDegree) <|
      mem_support_iff.mpr (Φ_coeff_generatorIndex_ne_zero h)

Premises used: Iff.mpr, Polynomial.mem_support_iff, _private.0.RatFunc.Luroth.le_Φ_coeff_generatorIndex_natDegree, _private.0.RatFunc.Luroth.Φ_coeff_generatorIndex_ne_zero, LE.le.trans, Finset.le_sup
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (f E).natDegree ≤ (Φ E).support.sup fun (i : ℕ) ↦ ((Φ E).coeff i).natDegree

Tactic:
exact (le_Φ_coeff_generatorIndex_natDegree h).trans <|
      Finset.le_sup (f := fun i ↦ ((Φ E).coeff i).natDegree) <|
      mem_support_iff.mpr (Φ_coeff_generatorIndex_ne_zero h)

Premises used: Iff.mpr, Polynomial.mem_support_iff, _private.0.RatFunc.Luroth.le_Φ_coeff_generatorIndex_natDegree, _private.0.RatFunc.Luroth.Φ_coeff_generatorIndex_ne_zero, LE.le.trans, Finset.le_sup
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (g E).natDegree ≤ (Φ E).support.sup fun (i : ℕ) ↦ ((Φ E).coeff i).natDegree

Tactic:
(le_Φ_coeff_natDegree_natDegree h).trans <|
      Finset.le_sup (f := fun i ↦ ((Φ E).coeff i).natDegree) <|
      mem_support_iff.mpr (Φ_coeff_φ_natDegree_ne_zero h)

Premises used: Iff.mpr, Polynomial.mem_support_iff, _private.0.RatFunc.Luroth.le_Φ_coeff_natDegree_natDegree, LE.le.trans, _private.0.RatFunc.Luroth.Φ_coeff_φ_natDegree_ne_zero, Finset.le_sup
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (g E).natDegree ≤ (Φ E).support.sup fun (i : ℕ) ↦ ((Φ E).coeff i).natDegree

Tactic:
exact (le_Φ_coeff_natDegree_natDegree h).trans <|
      Finset.le_sup (f := fun i ↦ ((Φ E).coeff i).natDegree) <|
      mem_support_iff.mpr (Φ_coeff_φ_natDegree_ne_zero h)

Premises used: Iff.mpr, Polynomial.mem_support_iff, _private.0.RatFunc.Luroth.le_Φ_coeff_natDegree_natDegree, LE.le.trans, _private.0.RatFunc.Luroth.Φ_coeff_φ_natDegree_ne_zero, Finset.le_sup
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
hp :
  Eq (α := K⟮X⟯)
    ((aeval X : (a : (↥E)[X]) → K⟮X⟯)
        (Polynomial.map (R := ↥K⟮generator E⟯) (algebraMap ↥K⟮generator E⟯ ↥E)
          ((generator E).minpolyX ↥K⟮generator E⟯)) :
      K⟮X⟯)
    (0 : K⟮X⟯)
⊢ φ E ∣ Polynomial.map (R := ↥K⟮generator E⟯) (algebraMap ↥K⟮generator E⟯ ↥E) ((generator E).minpolyX ↥K⟮generator E⟯)

Tactic:
apply minpoly.dvd

Premises used: minpoly.dvd
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
hp :
  Eq (α := K⟮X⟯) ((aeval X : (a : (↥K⟮generator E⟯)[X]) → K⟮X⟯) ((generator E).minpolyX ↥K⟮generator E⟯) : K⟮X⟯)
    (0 : K⟮X⟯)
⊢ Eq (α := K⟮X⟯)
    ((aeval X : (a : (↥E)[X]) → K⟮X⟯)
        (Polynomial.map (R := ↥K⟮generator E⟯) (algebraMap ↥K⟮generator E⟯ ↥E)
          ((generator E).minpolyX ↥K⟮generator E⟯)) :
      K⟮X⟯)
    (0 : K⟮X⟯)

Tactic:
rw [← aeval_eq_aeval_map rfl]

Premises used: Polynomial.aeval_eq_aeval_map
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
⊢ Eq (α := K⟮X⟯) ((aeval X : (a : (↥K⟮generator E⟯)[X]) → K⟮X⟯) ((generator E).minpolyX ↥K⟮generator E⟯) : K⟮X⟯)
    (0 : K⟮X⟯)

Tactic:
(generator E).minpolyX_aeval_X

Premises used: RatFunc.minpolyX_aeval_X, RatFunc.Luroth.generator
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
⊢ Eq (α := K⟮X⟯) ((aeval X : (a : (↥K⟮generator E⟯)[X]) → K⟮X⟯) ((generator E).minpolyX ↥K⟮generator E⟯) : K⟮X⟯)
    (0 : K⟮X⟯)

Tactic:
exact (generator E).minpolyX_aeval_X

Premises used: RatFunc.minpolyX_aeval_X, RatFunc.Luroth.generator
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
⊢ φ E * q E =
    Polynomial.map (R := ↥K⟮generator E⟯) (algebraMap ↥K⟮generator E⟯ ↥E) ((generator E).minpolyX ↥K⟮generator E⟯)

Tactic:
φ_dvd_generator_minpolyX.choose_spec.symm

Premises used: Exists.choose_spec, Set.Mem, setOf, Eq.symm, _private.0.RatFunc.Luroth.φ_dvd_generator_minpolyX
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ q E ≠ 0

Tactic:
right_ne_zero_of_mul <|
  φ_mul_q (E := E) ▸ Polynomial.map_ne_zero <|
    (generator E).minpolyX_eq_zero_iff.not.mpr (generator_ne_C h)

Premises used: right_ne_zero_of_mul
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
ha :
  Ne (α := K⟮X⟯[X])
    ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X])
        (HDiv.hDiv (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯) (c E)) :
      K⟮X⟯[X])
    (0 : K⟮X⟯[X])
hb : Ne (α := K⟮X⟯[X]) (Polynomial.map (algebraMap (↥E) K⟮X⟯) (q E)) 0
⊢ Q₀ E ≠ 0

Tactic:
apply mul_ne_zero

Premises used: mul_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Ne (α := K⟮X⟯[X])
    ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X])
        (HDiv.hDiv (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯) (c E)) :
      K⟮X⟯[X])
    (0 : K⟮X⟯[X])

Tactic:
C_ne_zero.mpr (div_ne_zero (algebraMap_ne_zero (generator E).denom_ne_zero) (c_ne_zero h))

Premises used: Iff.mpr, _private.0.RatFunc.Luroth.c_ne_zero, RatFunc.algebraMap_ne_zero, div_ne_zero, RatFunc.Luroth.generator, RatFunc.denom_ne_zero, Polynomial.C_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Ne (α := K⟮X⟯[X])
    ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X])
        (HDiv.hDiv (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯) (c E)) :
      K⟮X⟯[X])
    (0 : K⟮X⟯[X])

Tactic:
exact C_ne_zero.mpr (div_ne_zero (algebraMap_ne_zero (generator E).denom_ne_zero) (c_ne_zero h))

Premises used: Iff.mpr, _private.0.RatFunc.Luroth.c_ne_zero, RatFunc.algebraMap_ne_zero, div_ne_zero, RatFunc.Luroth.generator, RatFunc.denom_ne_zero, Polynomial.C_ne_zero