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 ≠ ⊥
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)
⊢ 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)
have rw₅ : Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (Φ' E).content : K⟮X⟯) (0 : K⟮X⟯)
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
-- 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 ≠ ⊥
⊢ (Φ E).natDegree = (φ E).natDegree
have rw : natDegree (R := K⟮X⟯) (Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)) = (φ 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]
-- 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 : natDegree (R := K⟮X⟯) (Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)) = (φ E).natDegree
⊢ (Φ E).natDegree = (φ E).natDegree
have 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
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]
-- 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 : 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
⊢ (Φ E).natDegree = (φ E).natDegree
have 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
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]
-- 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 : 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
⊢ (Φ E).natDegree = (φ E).natDegree
have rw₃ : 0 + natDegree (R := K⟮X⟯) (Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E)) = (φ 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]
-- 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 : 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
⊢ (Φ E).natDegree = (φ E).natDegree
have rw₄ : 0 + (φ 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]
-- 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 : 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
⊢ (Φ E).natDegree = (φ E).natDegree
have rw₅ : (φ 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]
-- 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 ≠ ⊥
⊢ (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (φ E).natDegree) = c E
have 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
Tactic: have := congr($(C_c_mul_φ h).coeff (φ E).natDegree)
-- 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⟯[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
⊢ (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (φ E).natDegree) = c E
have this₁ : 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
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 ≠ ⊥
⊢ (c E).denom = 1
have rw : Eq.{u_1 + 1} (α := K[X]) (denom ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Φ E).coeff (φ E).natDegree))) 1
Tactic: rw [← Φ_coeff_φ_natDegree 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 ≠ ⊥
⊢ (Φ E).coeff (φ E).natDegree = (c E).num
have 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⟯)
Tactic: apply algebraMap_injective
-- 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⟯) ((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⟯)
have a : c E = (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num
Tactic: rw [Φ_coeff_φ_natDegree 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 ≠ ⊥
| c E
have rw : ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮X⟯)
Tactic: rw [← num_div_denom (c E), c_denom h, map_one, div_one]
-- 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 ≠ ⊥
⊢ c E = (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num
have conv_lhs : 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]
-- 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 ≠ ⊥
conv_lhs : c E = (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num
⊢ c E = (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num
have 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⟯)
Tactic: conv_lhs => rw [← num_div_denom (c E), c_denom h, map_one, div_one]
-- 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 ≠ ⊥
⊢ (Φ E).coeff (φ E).natDegree ≠ 0
have rw : (c E).num ≠ 0
Tactic: rw [Φ_coeff_φ_natDegree' 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 ≠ ⊥
⊢ (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)
have 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)
Tactic: have := congr($(C_c_mul_φ h).coeff (generatorIndex 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 :
  (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)
⊢ (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)
have 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))
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
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 :
  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⟯) (generator E)
have 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⟯)
Tactic: rw [generator_eq_coeff 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 ≠ ⊥
⊢ (Φ E).coeff (generatorIndex h) ≠ 0
have 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⟯)
Tactic: apply_fun 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⟯) ((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⟯)
have rw : HMul.hMul (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c E).num : K⟮X⟯) (generator E) ≠ 0
Tactic: rw [map_zero, Φ_coeff_generatorIndex 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 ≠ ⊥
⊢ g E ∣ (c E).num
have 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⟯)
Tactic: rw [denom_dvd (num_ne_zero (c_ne_zero h))]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ ∃ (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⟯)
have 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⟯)
Tactic: use (Φ E).coeff (generatorIndex 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 ≠ ⊥
⊢ 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⟯)
have 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⟯)
Tactic: rw [Φ_coeff_generatorIndex h,
    mul_div_cancel_left₀ _ (algebraMap_ne_zero (num_ne_zero (c_ne_zero h)))]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
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⟯)
⊢ 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⟯)
have h₂ : generator E = generator E
Tactic: rw [Φ_coeff_generatorIndex h,
    mul_div_cancel_left₀ _ (algebraMap_ne_zero (num_ne_zero (c_ne_zero 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 : Φ E = 0
⊢ False
have this : (c E).num = coeff 0 (φ E).natDegree
Tactic: have := Φ_coeff_φ_natDegree' h ▸ congr($(H).coeff (φ E).natDegree)
-- 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 : Φ E = 0
this : (c E).num = coeff 0 (φ E).natDegree
⊢ False
have this₁ : (c E).num = 0
Tactic: rw [coeff_zero] 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 ≠ ⊥
⊢ (f E).natDegree ≤ ((Φ E).coeff (generatorIndex h)).natDegree
have 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⟯)
Tactic: have := congr($(Φ_coeff_generatorIndex h) * algebraMap K[X] K⟮X⟯ (g 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 ≠ ⊥
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⟯) (generator E))
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯)
have enter : generator E
Tactic: enter [2, 1, 2]
-- 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 :
  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⟯)
| generator E
have 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⟯)
Tactic: 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 ≠ ⊥
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⟯) (generator E))
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯)
have 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⟯)
Tactic: enter [2, 1, 2]; rw [← num_div_denom (generator E)]
-- 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⟯) (β := 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⟯)
⊢ (f E).natDegree ≤ ((Φ E).coeff (generatorIndex h)).natDegree
have 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⟯)
Tactic: conv at this => enter [2, 1, 2]; rw [← num_div_denom (generator E)]
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⟯) (β := 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⟯)
⊢ (f E).natDegree ≤ ((Φ E).coeff (generatorIndex h)).natDegree
have 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⟯)
Tactic: rw [mul_assoc, div_mul_cancel₀ _ (algebraMap_ne_zero (generator E).denom_ne_zero),
    ← map_mul, ← 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 :
  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⟯)
⊢ (f E).natDegree ≤ ((Φ E).coeff (generatorIndex h)).natDegree
have this₁ : ((Φ E).coeff (generatorIndex h) * g E).natDegree = ((c E).num * (generator E).num).natDegree
Tactic: replace this := congr($(algebraMap_injective K this).natDegree)
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 : ((Φ E).coeff (generatorIndex h) * g E).natDegree = ((c E).num * (generator E).num).natDegree
⊢ (f E).natDegree ≤ ((Φ E).coeff (generatorIndex h)).natDegree
have this₁ : ((Φ 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
Cleared hypotheses: this