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 ≠ ⊥
⊢ (g E).natDegree ≤ ((Φ E).coeff (φ E).natDegree).natDegree
have rw : (g E).natDegree ≤ (c E).num.natDegree
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 ≠ ⊥
⊢ m E ≤ natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Φ E))
have 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)))
Tactic: rw [← sum_monomial_eq (Φ E), sum_def, map_sum]
-- 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 ≠ ⊥
| fun (x : ℕ) ↦ (Bivariate.swap : (a : K[X][Y]) → K[X][Y]) ((monomial x : (a : K[X]) → K[X][Y]) ((Φ E).coeff x))
have h₁ : ∀ (x : ℕ), (Bivariate.swap : (a : K[X][Y]) → K[X][Y]) ((monomial x : (a : K[X]) → K[X][Y]) ((Φ E).coeff x))
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
x : ℕ
| (Bivariate.swap : (a : K[X][Y]) → K[X][Y]) ((monomial x : (a : K[X]) → K[X][Y]) ((Φ E).coeff x))
have h₁ : 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 [Bivariate.swap_monomial, mul_comm, ← Polynomial.smul_eq_C_mul,
      ← monomial_one_right_eq_X_pow, ← Polynomial.algebraMap_eq]
-- 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 ≠ ⊥
| fun (x : ℕ) ↦ (Bivariate.swap : (a : K[X][Y]) → K[X][Y]) ((monomial x : (a : K[X]) → K[X][Y]) ((Φ E).coeff x))
have 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))
Tactic: ext
    rw [Bivariate.swap_monomial, mul_comm, ← Polynomial.smul_eq_C_mul,
      ← monomial_one_right_eq_X_pow, ← Polynomial.algebraMap_eq]
-- 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 ≠ ⊥
⊢ 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)))
have 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)))
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]
-- 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 ≠ ⊥
⊢ 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)))
have rw : m E ≤ (Φ E).support.sup fun (i : ℕ) ↦ ((Φ E).coeff i).natDegree
Tactic: rw [natDegree_sum_eq_of_linearIndepOn _
    (coe_basisMonomials K ▸ (basisMonomials K).linearIndepOn (Φ E).support)]
-- 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 ≠ ⊥
⊢ m E ≤ (Φ E).support.sup fun (i : ℕ) ↦ ((Φ E).coeff i).natDegree
have h₁ : (f E).natDegree ≤ (Φ E).support.sup fun (i : ℕ) ↦ ((Φ E).coeff i).natDegree
Tactic: apply max_le
-- 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₁ : (f E).natDegree ≤ (Φ E).support.sup fun (i : ℕ) ↦ ((Φ E).coeff i).natDegree
⊢ m E ≤ (Φ E).support.sup fun (i : ℕ) ↦ ((Φ E).coeff i).natDegree
have h₂ : (g E).natDegree ≤ (Φ E).support.sup fun (i : ℕ) ↦ ((Φ E).coeff i).natDegree
Tactic: apply max_le
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
⊢ φ E ∣ Polynomial.map (R := ↥K⟮generator E⟯) (algebraMap ↥K⟮generator E⟯ ↥E) ((generator E).minpolyX ↥K⟮generator E⟯)
have 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⟯)
Tactic: apply minpoly.dvd
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K 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⟯)
have hp : Eq (α := K⟮X⟯) ((aeval X : (a : (↥K⟮generator E⟯)[X]) → K⟮X⟯) ((generator E).minpolyX ↥K⟮generator E⟯) : K⟮X⟯)
  (0 : K⟮X⟯)
Tactic: rw [← aeval_eq_aeval_map rfl]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Q₀ E ≠ 0
have 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])
Tactic: apply mul_ne_zero
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
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])
⊢ Q₀ E ≠ 0
have hb : Ne (α := K⟮X⟯[X]) (Polynomial.map (algebraMap (↥E) K⟮X⟯) (q E)) 0
Tactic: apply mul_ne_zero
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
⊢ (Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (θ E) = -θ E
have rw : HMul.hMul (β := K[X][Y]) (Polynomial.map Polynomial.C (g E)) ((Polynomial.C : (a : K[X]) → K[X][Y]) (f E) : K[X][Y]) -
    HMul.hMul (β := K[X][Y]) (Polynomial.map Polynomial.C (f E))
      ((Polynomial.C : (a : K[X]) → K[X][Y]) (g E) : K[X][Y]) =
  -θ E
Tactic: rw [map_sub, map_mul, map_mul, Bivariate.swap_C, Bivariate.swap_map_C, Bivariate.swap_C,
    Bivariate.swap_map_C]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (θ E).natDegree ≤ m E
have h₁ : (f E).natDegree =
  (HMul.hMul (α := K[X][Y]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (g E) : K[X][Y])
      (Polynomial.map Polynomial.C (f E))).natDegree
Tactic: convert! natDegree_sub_le _ _ using 3
-- 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₁ :
  (f E).natDegree =
    (HMul.hMul (α := K[X][Y]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (g E) : K[X][Y])
        (Polynomial.map Polynomial.C (f E))).natDegree
⊢ (θ E).natDegree ≤ m E
have h₂ : (g E).natDegree =
  (HMul.hMul (α := K[X][Y]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (f E) : K[X][Y])
      (Polynomial.map Polynomial.C (g E))).natDegree
Tactic: convert! natDegree_sub_le _ _ using 3
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (f E).natDegree =
    (HMul.hMul (α := K[X][Y]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (g E) : K[X][Y])
        (Polynomial.map Polynomial.C (f E))).natDegree
have h₁ : (f E).natDegree =
  natDegree.{u_1} (R := K[X]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (generator E).denom) +
    (Polynomial.map Polynomial.C (generator E).num).natDegree
Tactic: rw [natDegree_mul (C_ne_zero.mpr (generator E).denom_ne_zero)
      (Polynomial.map_ne_zero (num_ne_zero (generator_ne_zero h))), natDegree_C, zero_add,
      natDegree_map]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
h₁ :
  (f E).natDegree =
    natDegree.{u_1} (R := K[X]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (generator E).denom) +
      (Polynomial.map Polynomial.C (generator E).num).natDegree
⊢ (f E).natDegree =
    (HMul.hMul (α := K[X][Y]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (g E) : K[X][Y])
        (Polynomial.map Polynomial.C (f E))).natDegree
have h₂ : (f E).natDegree = 0 + (Polynomial.map Polynomial.C (generator E).num).natDegree
Tactic: rw [natDegree_mul (C_ne_zero.mpr (generator E).denom_ne_zero)
      (Polynomial.map_ne_zero (num_ne_zero (generator_ne_zero h))), natDegree_C, zero_add,
      natDegree_map]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
h₁ :
  (f E).natDegree =
    natDegree.{u_1} (R := K[X]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (generator E).denom) +
      (Polynomial.map Polynomial.C (generator E).num).natDegree
h₂ : (f E).natDegree = 0 + (Polynomial.map Polynomial.C (generator E).num).natDegree
⊢ (f E).natDegree =
    (HMul.hMul (α := K[X][Y]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (g E) : K[X][Y])
        (Polynomial.map Polynomial.C (f E))).natDegree
have h₃ : (f E).natDegree = (Polynomial.map Polynomial.C (generator E).num).natDegree
Tactic: rw [natDegree_mul (C_ne_zero.mpr (generator E).denom_ne_zero)
      (Polynomial.map_ne_zero (num_ne_zero (generator_ne_zero h))), natDegree_C, zero_add,
      natDegree_map]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
h₁ :
  (f E).natDegree =
    natDegree.{u_1} (R := K[X]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (generator E).denom) +
      (Polynomial.map Polynomial.C (generator E).num).natDegree
h₂ : (f E).natDegree = 0 + (Polynomial.map Polynomial.C (generator E).num).natDegree
h₃ : (f E).natDegree = (Polynomial.map Polynomial.C (generator E).num).natDegree
⊢ (f E).natDegree =
    (HMul.hMul (α := K[X][Y]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (g E) : K[X][Y])
        (Polynomial.map Polynomial.C (f E))).natDegree
have h₄ : (f E).natDegree = (generator E).num.natDegree
Tactic: rw [natDegree_mul (C_ne_zero.mpr (generator E).denom_ne_zero)
      (Polynomial.map_ne_zero (num_ne_zero (generator_ne_zero h))), natDegree_C, zero_add,
      natDegree_map]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (g E).natDegree =
    (HMul.hMul (α := K[X][Y]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (f E) : K[X][Y])
        (Polynomial.map Polynomial.C (g E))).natDegree
have h₁ : (g E).natDegree =
  natDegree.{u_1} (R := K[X]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (generator E).num) +
    (Polynomial.map Polynomial.C (generator E).denom).natDegree
Tactic: rw [natDegree_mul (C_ne_zero.mpr (num_ne_zero (generator_ne_zero h)))
      (Polynomial.map_ne_zero (generator E).denom_ne_zero), natDegree_C, zero_add, natDegree_map]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
h₁ :
  (g E).natDegree =
    natDegree.{u_1} (R := K[X]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (generator E).num) +
      (Polynomial.map Polynomial.C (generator E).denom).natDegree
⊢ (g E).natDegree =
    (HMul.hMul (α := K[X][Y]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (f E) : K[X][Y])
        (Polynomial.map Polynomial.C (g E))).natDegree
have h₂ : (g E).natDegree = 0 + (Polynomial.map Polynomial.C (generator E).denom).natDegree
Tactic: rw [natDegree_mul (C_ne_zero.mpr (num_ne_zero (generator_ne_zero h)))
      (Polynomial.map_ne_zero (generator E).denom_ne_zero), natDegree_C, zero_add, natDegree_map]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
h₁ :
  (g E).natDegree =
    natDegree.{u_1} (R := K[X]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (generator E).num) +
      (Polynomial.map Polynomial.C (generator E).denom).natDegree
h₂ : (g E).natDegree = 0 + (Polynomial.map Polynomial.C (generator E).denom).natDegree
⊢ (g E).natDegree =
    (HMul.hMul (α := K[X][Y]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (f E) : K[X][Y])
        (Polynomial.map Polynomial.C (g E))).natDegree
have h₃ : (g E).natDegree = (Polynomial.map Polynomial.C (generator E).denom).natDegree
Tactic: rw [natDegree_mul (C_ne_zero.mpr (num_ne_zero (generator_ne_zero h)))
      (Polynomial.map_ne_zero (generator E).denom_ne_zero), natDegree_C, zero_add, natDegree_map]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
h₁ :
  (g E).natDegree =
    natDegree.{u_1} (R := K[X]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (generator E).num) +
      (Polynomial.map Polynomial.C (generator E).denom).natDegree
h₂ : (g E).natDegree = 0 + (Polynomial.map Polynomial.C (generator E).denom).natDegree
h₃ : (g E).natDegree = (Polynomial.map Polynomial.C (generator E).denom).natDegree
⊢ (g E).natDegree =
    (HMul.hMul (α := K[X][Y]) ((Polynomial.C : (a : K[X]) → K[X][Y]) (f E) : K[X][Y])
        (Polynomial.map Polynomial.C (g E))).natDegree
have h₄ : (g E).natDegree = (generator E).denom.natDegree
Tactic: rw [natDegree_mul (C_ne_zero.mpr (num_ne_zero (generator_ne_zero h)))
      (Polynomial.map_ne_zero (generator E).denom_ne_zero), natDegree_C, zero_add, natDegree_map]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X])
        ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E)) : K⟮X⟯[X])
        (Polynomial.map (algebraMap (↥E) K⟮X⟯) (q E)) *
      Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
⊢ Q₀ E * Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E) = Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
have rw : HMul.hMul (α := 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])
    (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⟯) (q E)) *
      Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E)) =
  Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
Tactic: rw [← C_c_mul_φ h, mul_assoc, ← mul_assoc _ (Polynomial.C (c E)) _,
      mul_comm _ (Polynomial.C (c 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 ≠ ⊥
⊢ Q₀ E * Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E) = Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
have 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⟯) (g E)) : K⟮X⟯[X])
      (Polynomial.map (algebraMap (↥E) K⟮X⟯) (q E)) *
    Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E) =
  Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
Tactic: suffices
    Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E)) * (q E).map (algebraMap (↥E) K⟮X⟯) *
       (φ E).map (algebraMap (↥E) K⟮X⟯) = (θ E).map (algebraMap K[X] K⟮X⟯) by
    rw [← C_c_mul_φ h, mul_assoc, ← mul_assoc _ (Polynomial.C (c E)) _,
      mul_comm _ (Polynomial.C (c E))]
    simpa only [← mul_assoc, ← C_mul, div_mul_cancel₀ _ (c_ne_zero h)] using 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 ≠ ⊥
⊢ HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X])
        ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E)) : K⟮X⟯[X])
        (Polynomial.map (algebraMap (↥E) K⟮X⟯) (q E)) *
      Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
have 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⟯) (g E)) : K⟮X⟯[X])
      (Polynomial.map
        (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥E) K⟮X⟯)
            (↑(inclusion sorry) : ↥K⟮generator E⟯ →+* ↥E))
          (algebraMap K ↥K⟮generator E⟯))
        (generator E).num) -
    HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X])
      ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X])
          (HMul.hMul (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯)
            (↑(Subtype.mk (p := fun (x : K⟮X⟯) ↦ Membership.mem (γ := Subalgebra K K⟮X⟯) K[generator E] x) (generator E)
                  sorry) :
              K⟮X⟯)) :
        K⟮X⟯[X])
      (Polynomial.map
        (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥E) K⟮X⟯)
            (↑(inclusion sorry) : ↥K⟮generator E⟯ →+* ↥E))
          (algebraMap K ↥K⟮generator E⟯))
        (generator E).denom) =
  Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
Tactic: rw [mul_assoc, ← Polynomial.map_mul, mul_comm (q E) (φ E), φ_mul_q, Polynomial.map_map,
    Polynomial.map_sub, Polynomial.map_mul, map_C, RingHom.coe_comp, Function.comp_apply,
    IntermediateField.algebraMap_apply, Polynomial.map_map, Polynomial.map_map, mul_sub,
    ← mul_assoc, ← map_mul, (inclusion adjoin_generator_le).algebraMap_toAlgebra,
    AlgHom.toRingHom_eq_coe, RingHom.coe_coe, coe_inclusion, coe_algebraMap]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
| HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X])
        ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E)) : K⟮X⟯[X])
        (Polynomial.map
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥E) K⟮X⟯)
              (↑(inclusion ⋯) : ↥K⟮generator E⟯ →+* ↥E))
            (algebraMap K ↥K⟮generator E⟯))
          (generator E).num) -
      HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X])
        ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X])
            (HMul.hMul (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯)
              (↑(Subtype.mk (p := fun (x : K⟮X⟯) ↦ Membership.mem (γ := Subalgebra K K⟮X⟯) K[generator E] x)
                    (generator E) ⋯) :
                K⟮X⟯)) :
          K⟮X⟯[X])
        (Polynomial.map
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥E) K⟮X⟯)
              (↑(inclusion ⋯) : ↥K⟮generator E⟯ →+* ↥E))
            (algebraMap K ↥K⟮generator E⟯))
          (generator E).denom) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
have enter : (↑(Subtype.mk (p := fun (x : K⟮X⟯) ↦ Membership.mem (γ := Subalgebra K K⟮X⟯) K[generator E] x) (generator E) sorry) : K⟮X⟯)
Tactic: enter [1, 2, 1, 2, 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 ≠ ⊥
| (↑(Subtype.mk (p := fun (x : K⟮X⟯) ↦ Membership.mem (γ := Subalgebra K K⟮X⟯) K[generator E] x) (generator E) ⋯) :
    K⟮X⟯)
have rw : (↑(Subtype.mk (p := fun (x : K⟮X⟯) ↦
      Membership.mem (γ := Subalgebra K K⟮X⟯)
        K[HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (generator E).num : K⟮X⟯)
            ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (generator E).denom : K⟮X⟯)]
        x)
      (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (generator E).num : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (generator E).denom : K⟮X⟯))
      sorry) :
  K⟮X⟯)
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 ≠ ⊥
| HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X])
        ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E)) : K⟮X⟯[X])
        (Polynomial.map
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥E) K⟮X⟯)
              (↑(inclusion ⋯) : ↥K⟮generator E⟯ →+* ↥E))
            (algebraMap K ↥K⟮generator E⟯))
          (generator E).num) -
      HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X])
        ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X])
            (HMul.hMul (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯)
              (↑(Subtype.mk (p := fun (x : K⟮X⟯) ↦ Membership.mem (γ := Subalgebra K K⟮X⟯) K[generator E] x)
                    (generator E) ⋯) :
                K⟮X⟯)) :
          K⟮X⟯[X])
        (Polynomial.map
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥E) K⟮X⟯)
              (↑(inclusion ⋯) : ↥K⟮generator E⟯ →+* ↥E))
            (algebraMap K ↥K⟮generator E⟯))
          (generator E).denom) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
have enter : (↑(Subtype.mk (p := fun (x : K⟮X⟯) ↦
      Membership.mem (γ := Subalgebra K K⟮X⟯)
        K[HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (generator E).num : K⟮X⟯)
            ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (generator E).denom : K⟮X⟯)]
        x)
      (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (generator E).num : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (generator E).denom : K⟮X⟯))
      sorry) :
  K⟮X⟯)
Tactic: enter [1, 2, 1, 2, 2]; rw [← num_div_denom (generator E)]