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 = ⊥
⊢ (↑((φ E).coeff (generatorIndex h)) : K⟮X⟯) ∈ E

Tactic:
SetLike.coe_mem _

Premises used: SetLike.coe_mem
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : ¬E = ⊥
⊢ (↑((φ E).coeff (generatorIndex h)) : K⟮X⟯) ∈ E

Tactic:
exact SetLike.coe_mem _

Premises used: SetLike.coe_mem
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
rw : (↑((φ E).coeff (generatorIndex h)) : K⟮X⟯) ∉ RingHom.range (R := K) (algebraMap K K⟮X⟯)
⊢ generator E ∉ RingHom.range (R := K) (algebraMap K K⟮X⟯)

Tactic:
rw [generator_eq_coeff h]

Premises used: _private.0.RatFunc.Luroth.generator_eq_coeff
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
f : K
hf : ((algebraMap K K⟮X⟯ : K →+* K⟮X⟯) : (a : K) → K⟮X⟯) f = (↑((φ E).coeff (generatorIndex h)) : K⟮X⟯)
a :
  (↑(((algebraMap K ↥E : K →+* ↥E) : (a : K) → ↥E) f) : K⟮X⟯) =
    (↑((φ E).coeff (⋯.choose (p := fun (i : ℕ) ↦ (φ E).coeff i ∉ RingHom.range (R := K) (algebraMap K ↥E)))) : K⟮X⟯)
⊢ ((algebraMap K ↥E : K →+* ↥E) : (a : K) → ↥E) f =
    (φ E).coeff (⋯.choose (p := fun (i : ℕ) ↦ (φ E).coeff i ∉ RingHom.range (R := K) (algebraMap K ↥E)))

Tactic:
ext
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
f : K
hf : ((algebraMap K K⟮X⟯ : K →+* K⟮X⟯) : (a : K) → K⟮X⟯) f = (↑((φ E).coeff (generatorIndex h)) : K⟮X⟯)
⊢ (↑(((algebraMap K ↥E : K →+* ↥E) : (a : K) → ↥E) f) : K⟮X⟯) =
    (↑((φ E).coeff (⋯.choose (p := fun (i : ℕ) ↦ (φ E).coeff i ∉ RingHom.range (R := K) (algebraMap K ↥E)))) : K⟮X⟯)

Tactic:
hf

Premises used: Set.Mem, _private.0.RatFunc.Luroth.generatorIndex
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
f : K
hf : ((algebraMap K K⟮X⟯ : K →+* K⟮X⟯) : (a : K) → K⟮X⟯) f = (↑((φ E).coeff (generatorIndex h)) : K⟮X⟯)
⊢ (↑(((algebraMap K ↥E : K →+* ↥E) : (a : K) → ↥E) f) : K⟮X⟯) =
    (↑((φ E).coeff (⋯.choose (p := fun (i : ℕ) ↦ (φ E).coeff i ∉ RingHom.range (R := K) (algebraMap K ↥E)))) : K⟮X⟯)

Tactic:
exact hf
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
f : K
hf : ((algebraMap K K⟮X⟯ : K →+* K⟮X⟯) : (a : K) → K⟮X⟯) f = (↑((φ E).coeff (generatorIndex h)) : K⟮X⟯)
⊢ False

Tactic:
exact (exists_φ_coeff_not_mem h).choose_spec ⟨f, by ext; exact hf⟩

Premises used: Exists.choose_spec, _private.0.RatFunc.Luroth.exists_φ_coeff_not_mem, Exists.intro
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
h_1 : ∃ (c : K), generator E = (C : (a : K) → K⟮X⟯) c
c : K
hc : generator E = (C : (a : K) → K⟮X⟯) c
⊢ ((algebraMap K K⟮X⟯ : K →+* K⟮X⟯) : (a : K) → K⟮X⟯) c = generator E

Tactic:
simpa using hc.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 ≠ ⊥
⊢ Transcendental K (generator E)

Tactic:
(generator E).transcendental_of_ne_C (generator_ne_C h)

Premises used: RatFunc.Luroth.generator_ne_C, RatFunc.transcendental_of_ne_C, RatFunc.Luroth.generator
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
H : generator E = 0
⊢ generator E = (C : (a : K) → K⟮X⟯) 0

Tactic:
simp [H]
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
⊢ K⟮generator E⟯ ≤ E

Tactic:
adjoin_simple_le_iff.mpr generator_mem

Premises used: Iff.mpr, RatFunc.Luroth.generator_mem, IntermediateField.adjoin_simple_le_iff
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Φ' E ≠ 0

Tactic:
IsFractionRing.integerNormalization_eq_zero_iff.not.mpr (map_ne_zero (φ_ne_zero h))

Premises used: Iff.mpr, IsFractionRing.integerNormalization_eq_zero_iff, Iff.not, Polynomial.map_ne_zero, _private.0.RatFunc.Luroth.φ_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
⊢ b E ≠ 0

Tactic:
nonZeroDivisors.ne_zero <| (IsLocalization.integerNormalization_spec _
    ((φ E).map (algebraMap ..))).choose_spec.1

Premises used: Exists.choose_spec, Algebra.algebraMap, _private.0.RatFunc.Luroth.φ, nonZeroDivisors.ne_zero, And.left, Polynomial.map, IsLocalization.integerNormalization_spec
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
⊢ Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ' E) =
    HSMul.hSMul (β := K⟮X⟯[X]) (b E) (Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E))

Tactic:
(IsLocalization.integerNormalization_spec _ ((φ E).map (algebraMap ..))).choose_spec.2

Premises used: _private.0.RatFunc.Luroth.b, Exists.choose_spec, Algebra.algebraMap, Set.Mem, _private.0.RatFunc.Luroth.φ, And.right, Polynomial.map, IsLocalization.integerNormalization_spec
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ c E ≠ 0

Tactic:
mul_ne_zero_iff.mpr ⟨inv_ne_zero <| (FaithfulSMul.algebraMap_eq_zero_iff _ _).not.mpr <|
    content_eq_zero_iff.not.mpr (Φ'_ne_zero h),
  (FaithfulSMul.algebraMap_eq_zero_iff _ _).not.mpr b_ne_zero⟩

Premises used: Iff.mpr, _private.0.RatFunc.Luroth.b_ne_zero, _private.0.RatFunc.Luroth.Φ'_ne_zero, Polynomial.content_eq_zero_iff, Iff.not, And.intro, inv_ne_zero, mul_ne_zero_iff, FaithfulSMul.algebraMap_eq_zero_iff
-- 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.C : (a : K⟮X⟯) → K⟮X⟯[X]) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (Φ' E).content)⁻¹ : K⟮X⟯[X])
      (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⟯) (b E)) : K⟮X⟯[X])
        (Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E))) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)
⊢ HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X]) ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) (c E) : K⟮X⟯[X])
      (Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E)) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)

Tactic:
rw [map_mul, mul_assoc]

Premises used: mul_assoc, map_mul
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
enter :
  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⟯) (b E)) : K⟮X⟯[X])
    (Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E))
| HMul.hMul (α := K⟮X⟯[X])
      ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (Φ' E).content)⁻¹ : K⟮X⟯[X])
      (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⟯) (b E)) : K⟮X⟯[X])
        (Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E))) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)

Tactic:
enter [1, 2]
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
rw :
  Polynomial.map (algebraMap K[X] K⟮X⟯)
    (HMul.hMul (α := K[X][Y]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (Φ' E).content : K[X][Y]) (Φ' E).primPart)
| 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⟯) (b E)) : K⟮X⟯[X])
    (Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E))

Tactic:
rw [← Polynomial.smul_eq_C_mul, algebraMap_smul, ← Φ'_map, eq_C_content_mul_primPart (Φ' E)]

Premises used: Polynomial.smul_eq_C_mul, _private.0.RatFunc.Luroth.Φ', _private.0.RatFunc.Luroth.Φ'_map, algebraMap_smul, Polynomial.eq_C_content_mul_primPart
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
enter :
  Polynomial.map (algebraMap K[X] K⟮X⟯)
    (HMul.hMul (α := K[X][Y]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (Φ' E).content : K[X][Y]) (Φ' E).primPart)
| HMul.hMul (α := K⟮X⟯[X])
      ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (Φ' E).content)⁻¹ : K⟮X⟯[X])
      (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⟯) (b E)) : K⟮X⟯[X])
        (Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E))) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)

Tactic:
enter [1, 2]
    rw [← Polynomial.smul_eq_C_mul, algebraMap_smul, ← Φ'_map, eq_C_content_mul_primPart (Φ' E)]

Premises used: Polynomial.smul_eq_C_mul, _private.0.RatFunc.Luroth.Φ', _private.0.RatFunc.Luroth.Φ'_map, algebraMap_smul, Polynomial.eq_C_content_mul_primPart
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
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⟯) (Φ' E).content)⁻¹ : K⟮X⟯[X])
      (Polynomial.map (algebraMap K[X] K⟮X⟯)
        (HMul.hMul (α := K[X][Y]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (Φ' E).content : K[X][Y]) (Φ' E).primPart)) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)
⊢ HMul.hMul (α := K⟮X⟯[X])
      ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (Φ' E).content)⁻¹ : K⟮X⟯[X])
      (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⟯) (b E)) : K⟮X⟯[X])
        (Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E))) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)

Tactic:
conv =>
    enter [1, 2]
    rw [← Polynomial.smul_eq_C_mul, algebraMap_smul, ← Φ'_map, eq_C_content_mul_primPart (Φ' E)]

Premises used: Polynomial.smul_eq_C_mul, _private.0.RatFunc.Luroth.Φ', _private.0.RatFunc.Luroth.Φ'_map, algebraMap_smul, Polynomial.eq_C_content_mul_primPart
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
rw : Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (Φ' E).content : K⟮X⟯) (0 : K⟮X⟯)
⊢ 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⟯) (Φ' E).content)⁻¹ : K⟮X⟯[X])
      (Polynomial.map (algebraMap K[X] K⟮X⟯)
        (HMul.hMul (α := K[X][Y]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (Φ' E).content : K[X][Y]) (Φ' E).primPart)) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)

Tactic:
rw [Polynomial.map_mul, map_C, ← mul_assoc, ← C_mul, inv_mul_cancel₀, map_one, one_mul]

Premises used: Polynomial.map_mul, mul_assoc, map_one, Polynomial.C_mul, Polynomial.map_C, inv_mul_cancel₀, one_mul
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
rw : ¬Φ' E = 0
⊢ Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (Φ' E).content : K⟮X⟯) (0 : K⟮X⟯)

Tactic:
rw [ne_eq, FaithfulSMul.algebraMap_eq_zero_iff, content_eq_zero_iff]

Premises used: Polynomial.content_eq_zero_iff, ne_eq, FaithfulSMul.algebraMap_eq_zero_iff
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ ¬Φ' E = 0

Tactic:
Φ'_ne_zero h

Premises used: _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 ≠ ⊥
⊢ ¬Φ' E = 0

Tactic:
exact Φ'_ne_zero h

Premises used: _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 ≠ ⊥
rw :
  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⟯) (Φ' E).content)⁻¹ : K⟮X⟯[X])
        ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (b E)) : K⟮X⟯[X]) *
      Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)
rw₁ rw₂ rw₃ :
  HMul.hMul (α := K⟮X⟯[X])
      ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (Φ' E).content)⁻¹ : K⟮X⟯[X])
      (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⟯) (b E)) : K⟮X⟯[X])
        (Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E))) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)
rw₄ :
  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⟯) (Φ' E).content)⁻¹ : K⟮X⟯[X])
      (Polynomial.map (algebraMap K[X] K⟮X⟯)
        (HMul.hMul (α := K[X][Y]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (Φ' E).content : K[X][Y]) (Φ' E).primPart)) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)
rw₅ : Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (Φ' E).content : K⟮X⟯) (0 : K⟮X⟯)
⊢ HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X]) ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) (c E) : K⟮X⟯[X])
      (Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E)) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)

Tactic:
classical
  rw [map_mul, mul_assoc]
  conv =>
    enter [1, 2]
    rw [← Polynomial.smul_eq_C_mul, algebraMap_smul, ← Φ'_map, eq_C_content_mul_primPart (Φ' E)]
  rw [Polynomial.map_mul, map_C, ← mul_assoc, ← C_mul, inv_mul_cancel₀, map_one, one_mul]
  · rw [ne_eq, FaithfulSMul.algebraMap_eq_zero_iff, content_eq_zero_iff]
    exact Φ'_ne_zero h

Premises used: Polynomial.map_mul, _private.0.RatFunc.Luroth.Φ'_ne_zero, Polynomial.content_eq_zero_iff, Polynomial.smul_eq_C_mul, mul_assoc, _private.0.RatFunc.Luroth.Φ'_map, algebraMap_smul, ne_eq, map_mul, map_one, Polynomial.C_mul, Polynomial.map_C, inv_mul_cancel₀, one_mul, FaithfulSMul.algebraMap_eq_zero_iff
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
rw : natDegree (R := K⟮X⟯) (Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)) = (φ E).natDegree
rw₁ :
  (HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X]) ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) (c E) : K⟮X⟯[X])
        (Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E))).natDegree =
    (φ E).natDegree
rw₂ :
  natDegree.{u_1} (R := K⟮X⟯) ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) (c E)) +
      natDegree (R := K⟮X⟯) (Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E)) =
    (φ E).natDegree
rw₃ : 0 + natDegree (R := K⟮X⟯) (Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E)) = (φ E).natDegree
rw₄ : 0 + (φ E).natDegree = (φ E).natDegree
rw₅ rw₆ : (φ E).natDegree = (φ E).natDegree
⊢ (Φ E).natDegree = (φ E).natDegree

Tactic:
rw [← natDegree_map_eq_of_injective (algebraMap_injective K), ← C_c_mul_φ h,
    natDegree_mul (C_ne_zero.mpr (c_ne_zero h)) (map_ne_zero (φ_ne_zero h)), natDegree_C,
    natDegree_map, zero_add]

Premises used: Iff.mpr, _private.0.RatFunc.Luroth.c_ne_zero, Polynomial.natDegree_mul, Polynomial.natDegree_map, Polynomial.natDegree_C, _private.0.RatFunc.Luroth.C_c_mul_φ, zero_add, RatFunc.algebraMap_injective, Polynomial.natDegree_map_eq_of_injective, Polynomial.map_ne_zero, _private.0.RatFunc.Luroth.φ_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 ≠ ⊥
⊢ (HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X]) ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) (c E) : K⟮X⟯[X])
          (Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E))).coeff
      (φ E).natDegree =
    coeff (Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)) (φ E).natDegree

Tactic:
have := congr($(C_c_mul_φ h).coeff (φ E).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⟯[X]) (β := K⟮X⟯[X]) ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) (c E) : K⟮X⟯[X])
          (Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E))).coeff
      (φ E).natDegree =
    coeff (Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)) (φ E).natDegree
⊢ c E = (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (φ E).natDegree)

Tactic:
rw [coeff_C_mul, coeff_map, coeff_map, coeff_natDegree, IntermediateField.algebraMap_apply,
    φ_monic h, OneMemClass.coe_one, mul_one] at this

Premises used: Polynomial.coeff_map, Polynomial.coeff_natDegree, OneMemClass.coe_one, Polynomial.coeff_C_mul, _private.0.RatFunc.Luroth.φ_monic, IntermediateField.algebraMap_apply, mul_one
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this : c E = (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (φ E).natDegree)
⊢ (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (φ E).natDegree) = c E

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 : c E = (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (φ E).natDegree)
⊢ (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (φ E).natDegree) = c E

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 ≠ ⊥
rw : Eq.{u_1 + 1} (α := K[X]) (denom ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (φ E).natDegree))) 1
⊢ (c E).denom = 1

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 ≠ ⊥
⊢ Eq.{u_1 + 1} (α := K[X]) (denom ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (φ E).natDegree))) 1

Tactic:
denom_algebraMap _

Premises used: RatFunc.denom_algebraMap
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Eq.{u_1 + 1} (α := K[X]) (denom ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (φ E).natDegree))) 1

Tactic:
exact denom_algebraMap _

Premises used: RatFunc.denom_algebraMap
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
a :
  Eq (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (φ E).natDegree) : K⟮X⟯)
    ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮X⟯)
⊢ (Φ E).coeff (φ E).natDegree = (c E).num

Tactic:
apply algebraMap_injective

Premises used: RatFunc.algebraMap_injective
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
a : c E = (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num
⊢ Eq (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (φ E).natDegree) : K⟮X⟯)
    ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮X⟯)

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 ≠ ⊥
rw : ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮X⟯)
| c E

Tactic:
rw [← num_div_denom (c E), c_denom h, map_one, div_one]

Premises used: _private.0.RatFunc.Luroth.c, map_one, RatFunc.num_div_denom, div_one, _private.0.RatFunc.Luroth.c_denom
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
conv_lhs : c E = (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num
a :
  Eq (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮X⟯)
    ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮X⟯)
⊢ c E = (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num

Tactic:
conv_lhs => rw [← num_div_denom (c E), c_denom h, map_one, div_one]

Premises used: _private.0.RatFunc.Luroth.c, map_one, RatFunc.num_div_denom, div_one, _private.0.RatFunc.Luroth.c_denom
-- Module: Mathlib.FieldTheory.RatFunc.Luroth
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
rw : (c E).num ≠ 0
⊢ (Φ E).coeff (φ E).natDegree ≠ 0

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 ≠ ⊥
⊢ (c E).num ≠ 0

Tactic:
num_ne_zero (c_ne_zero h)

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 ≠ ⊥
⊢ (c E).num ≠ 0

Tactic:
exact num_ne_zero (c_ne_zero h)

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⟯[X]) (β := K⟮X⟯[X]) ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) (c E) : K⟮X⟯[X])
          (Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E))).coeff
      (generatorIndex h) =
    coeff (Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)) (generatorIndex h)

Tactic:
have := congr($(C_c_mul_φ h).coeff (generatorIndex h))
-- 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⟯[X]) (β := K⟮X⟯[X]) ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) (c E) : K⟮X⟯[X])
          (Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E))).coeff
      (generatorIndex h) =
    coeff (Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)) (generatorIndex h)
⊢ HMul.hMul (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮X⟯)
      (↑((φ E).coeff (generatorIndex h)) : K⟮X⟯) =
    (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (generatorIndex h))

Tactic:
rw [coeff_map, coeff_C_mul, coeff_map, IntermediateField.algebraMap_apply,
    ← num_div_denom (c E), c_denom h, map_one, div_one] at this

Premises used: Polynomial.coeff_map, Polynomial.coeff_C_mul, _private.0.RatFunc.Luroth.c, IntermediateField.algebraMap_apply, map_one, RatFunc.num_div_denom, div_one, _private.0.RatFunc.Luroth.c_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⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮X⟯)
      (↑((φ E).coeff (generatorIndex h)) : K⟮X⟯) =
    (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (generatorIndex h))
rw :
  (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (generatorIndex h)) =
    HMul.hMul (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮X⟯)
      (↑((φ E).coeff (generatorIndex h)) : K⟮X⟯)
⊢ (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (generatorIndex h)) =
    HMul.hMul (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮X⟯) (generator E)

Tactic:
rw [generator_eq_coeff h]

Premises used: _private.0.RatFunc.Luroth.generator_eq_coeff
-- 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⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮X⟯)
      (↑((φ E).coeff (generatorIndex h)) : K⟮X⟯) =
    (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (generatorIndex h))
⊢ (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (generatorIndex h)) =
    HMul.hMul (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮X⟯)
      (↑((φ E).coeff (generatorIndex h)) : K⟮X⟯)

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 :
  HMul.hMul (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮X⟯)
      (↑((φ E).coeff (generatorIndex h)) : K⟮X⟯) =
    (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (generatorIndex h))
⊢ (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (generatorIndex h)) =
    HMul.hMul (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮X⟯)
      (↑((φ E).coeff (generatorIndex h)) : K⟮X⟯)

Tactic:
exact this.symm

Premises used: Eq.symm