awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
⊢ Module.finrank.{u_1, u_1} (↥K⟮f⟯) K⟮X⟯ = max f.num.natDegree f.denom.natDegree
have pos : ∀ (hf : ∃ (c : K), f = (C : (a : K) → K⟮X⟯) c),
  Module.finrank.{u_1, u_1} (↥K⟮f⟯) K⟮X⟯ = max f.num.natDegree f.denom.natDegree
Tactic: by_cases hf : ∃ c, f = C c
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
pos :
  ∀ (hf : ∃ (c : K), f = (C : (a : K) → K⟮X⟯) c),
    Module.finrank.{u_1, u_1} (↥K⟮f⟯) K⟮X⟯ = max f.num.natDegree f.denom.natDegree
⊢ Module.finrank.{u_1, u_1} (↥K⟮f⟯) K⟮X⟯ = max f.num.natDegree f.denom.natDegree
have neg : ∀ (hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c),
  Module.finrank.{u_1, u_1} (↥K⟮f⟯) K⟮X⟯ = max f.num.natDegree f.denom.natDegree
Tactic: by_cases hf : ∃ c, f = C c
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
⊢ Module.finrank.{u_1, u_1} (↥K⟮f⟯) K⟮X⟯ = max f.num.natDegree f.denom.natDegree
have pos : ∀ (c : K),
  Module.finrank.{u_1, u_1} (↥K⟮((C : (a : K) → K⟮X⟯) c : K⟮X⟯)⟯) K⟮X⟯ =
    max (natDegree.{u_1} (R := K) (num ((C : (a : K) → K⟮X⟯) c)))
      (natDegree.{u_1} (R := K) (denom ((C : (a : K) → K⟮X⟯) c)))
Tactic: obtain ⟨c, rfl⟩ := hf
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
Goal:
K : Type u_1
inst : Field K
c : K
⊢ Module.finrank.{u_1, u_1} (↥K⟮((C : (a : K) → K⟮X⟯) c : K⟮X⟯)⟯) K⟮X⟯ =
    max (natDegree.{u_1} (R := K) (num ((C : (a : K) → K⟮X⟯) c)))
      (natDegree.{u_1} (R := K) (denom ((C : (a : K) → K⟮X⟯) c)))
have pos : 0 =
  max (natDegree.{u_1} (R := K) (num ((C : (a : K) → K⟮X⟯) c)))
    (natDegree.{u_1} (R := K) (denom ((C : (a : K) → K⟮X⟯) c)))
Tactic: rw [adjoin_simple_eq_bot_iff.mpr (show C c ∈ ⊥ from ⟨c, rfl⟩), finrank_bot',
      Module.finrank_of_not_finite fun H ↦ Algebra.transcendental_iff_not_isAlgebraic.mp
      transcendental <| Algebra.IsAlgebraic.of_finite K K⟮X⟯]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
⊢ Module.finrank.{u_1, u_1} (↥K⟮f⟯) K⟮X⟯ = max f.num.natDegree f.denom.natDegree
have neg : Module.finrank.{u_1, u_1} ↥K⟮f⟯ ↥(↥K⟮f⟯)⟮ X⟯ = max f.num.natDegree f.denom.natDegree
Tactic: rw [← (IntermediateField.adjoinXEquiv K⟮f⟯).toLinearEquiv.finrank_eq,
    adjoin.finrank (f.isAlgebraic_adjoin_simple_X hf).isIntegral,
    ← minpoly.eq_of_irreducible (f.irreducible_minpolyX hf) f.minpolyX_aeval_X, mul_comm,
    natDegree_C_mul <| inv_ne_zero <| leadingCoeff_ne_zero.mpr fun H ↦
    hf ((minpolyX_eq_zero_iff f).mp H), natDegree_minpolyX]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
neg : Module.finrank.{u_1, u_1} ↥K⟮f⟯ ↥(↥K⟮f⟯)⟮ X⟯ = max f.num.natDegree f.denom.natDegree
⊢ Module.finrank.{u_1, u_1} (↥K⟮f⟯) K⟮X⟯ = max f.num.natDegree f.denom.natDegree
have neg₁ : natDegree.{u_1} (R := ↥K⟮f⟯) (minpoly ↥K⟮f⟯ (B := K⟮X⟯) X) = max f.num.natDegree f.denom.natDegree
Tactic: rw [← (IntermediateField.adjoinXEquiv K⟮f⟯).toLinearEquiv.finrank_eq,
    adjoin.finrank (f.isAlgebraic_adjoin_simple_X hf).isIntegral,
    ← minpoly.eq_of_irreducible (f.irreducible_minpolyX hf) f.minpolyX_aeval_X, mul_comm,
    natDegree_C_mul <| inv_ne_zero <| leadingCoeff_ne_zero.mpr fun H ↦
    hf ((minpolyX_eq_zero_iff f).mp H), natDegree_minpolyX]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
neg : Module.finrank.{u_1, u_1} ↥K⟮f⟯ ↥(↥K⟮f⟯)⟮ X⟯ = max f.num.natDegree f.denom.natDegree
neg₁ : natDegree.{u_1} (R := ↥K⟮f⟯) (minpoly ↥K⟮f⟯ (B := K⟮X⟯) X) = max f.num.natDegree f.denom.natDegree
⊢ Module.finrank.{u_1, u_1} (↥K⟮f⟯) K⟮X⟯ = max f.num.natDegree f.denom.natDegree
have neg₂ : (HMul.hMul (α := (↥K⟮f⟯)[X]) (f.minpolyX ↥K⟮f⟯)
      ((Polynomial.C : (a : ↥K⟮f⟯) → (↥K⟮f⟯)[X]) (leadingCoeff (f.minpolyX ↥K⟮f⟯))⁻¹)).natDegree =
  max f.num.natDegree f.denom.natDegree
Tactic: rw [← (IntermediateField.adjoinXEquiv K⟮f⟯).toLinearEquiv.finrank_eq,
    adjoin.finrank (f.isAlgebraic_adjoin_simple_X hf).isIntegral,
    ← minpoly.eq_of_irreducible (f.irreducible_minpolyX hf) f.minpolyX_aeval_X, mul_comm,
    natDegree_C_mul <| inv_ne_zero <| leadingCoeff_ne_zero.mpr fun H ↦
    hf ((minpolyX_eq_zero_iff f).mp H), natDegree_minpolyX]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
neg : Module.finrank.{u_1, u_1} ↥K⟮f⟯ ↥(↥K⟮f⟯)⟮ X⟯ = max f.num.natDegree f.denom.natDegree
neg₁ : natDegree.{u_1} (R := ↥K⟮f⟯) (minpoly ↥K⟮f⟯ (B := K⟮X⟯) X) = max f.num.natDegree f.denom.natDegree
neg₂ :
  (HMul.hMul (α := (↥K⟮f⟯)[X]) (f.minpolyX ↥K⟮f⟯)
        ((Polynomial.C : (a : ↥K⟮f⟯) → (↥K⟮f⟯)[X]) (leadingCoeff (f.minpolyX ↥K⟮f⟯))⁻¹)).natDegree =
    max f.num.natDegree f.denom.natDegree
⊢ Module.finrank.{u_1, u_1} (↥K⟮f⟯) K⟮X⟯ = max f.num.natDegree f.denom.natDegree
have neg₃ : (HMul.hMul (α := (↥K⟮f⟯)[X]) ((Polynomial.C : (a : ↥K⟮f⟯) → (↥K⟮f⟯)[X]) (leadingCoeff (f.minpolyX ↥K⟮f⟯))⁻¹)
      (f.minpolyX ↥K⟮f⟯)).natDegree =
  max f.num.natDegree f.denom.natDegree
Tactic: rw [← (IntermediateField.adjoinXEquiv K⟮f⟯).toLinearEquiv.finrank_eq,
    adjoin.finrank (f.isAlgebraic_adjoin_simple_X hf).isIntegral,
    ← minpoly.eq_of_irreducible (f.irreducible_minpolyX hf) f.minpolyX_aeval_X, mul_comm,
    natDegree_C_mul <| inv_ne_zero <| leadingCoeff_ne_zero.mpr fun H ↦
    hf ((minpolyX_eq_zero_iff f).mp H), natDegree_minpolyX]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
neg : Module.finrank.{u_1, u_1} ↥K⟮f⟯ ↥(↥K⟮f⟯)⟮ X⟯ = max f.num.natDegree f.denom.natDegree
neg₁ : natDegree.{u_1} (R := ↥K⟮f⟯) (minpoly ↥K⟮f⟯ (B := K⟮X⟯) X) = max f.num.natDegree f.denom.natDegree
neg₂ :
  (HMul.hMul (α := (↥K⟮f⟯)[X]) (f.minpolyX ↥K⟮f⟯)
        ((Polynomial.C : (a : ↥K⟮f⟯) → (↥K⟮f⟯)[X]) (leadingCoeff (f.minpolyX ↥K⟮f⟯))⁻¹)).natDegree =
    max f.num.natDegree f.denom.natDegree
neg₃ :
  (HMul.hMul (α := (↥K⟮f⟯)[X]) ((Polynomial.C : (a : ↥K⟮f⟯) → (↥K⟮f⟯)[X]) (leadingCoeff (f.minpolyX ↥K⟮f⟯))⁻¹)
        (f.minpolyX ↥K⟮f⟯)).natDegree =
    max f.num.natDegree f.denom.natDegree
⊢ Module.finrank.{u_1, u_1} (↥K⟮f⟯) K⟮X⟯ = max f.num.natDegree f.denom.natDegree
have neg₄ : natDegree (R := ↥K⟮f⟯) (f.minpolyX ↥K⟮f⟯) = max f.num.natDegree f.denom.natDegree
Tactic: rw [← (IntermediateField.adjoinXEquiv K⟮f⟯).toLinearEquiv.finrank_eq,
    adjoin.finrank (f.isAlgebraic_adjoin_simple_X hf).isIntegral,
    ← minpoly.eq_of_irreducible (f.irreducible_minpolyX hf) f.minpolyX_aeval_X, mul_comm,
    natDegree_C_mul <| inv_ne_zero <| leadingCoeff_ne_zero.mpr fun H ↦
    hf ((minpolyX_eq_zero_iff f).mp H), natDegree_minpolyX]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
neg : Module.finrank.{u_1, u_1} ↥K⟮f⟯ ↥(↥K⟮f⟯)⟮ X⟯ = max f.num.natDegree f.denom.natDegree
neg₁ : natDegree.{u_1} (R := ↥K⟮f⟯) (minpoly ↥K⟮f⟯ (B := K⟮X⟯) X) = max f.num.natDegree f.denom.natDegree
neg₂ :
  (HMul.hMul (α := (↥K⟮f⟯)[X]) (f.minpolyX ↥K⟮f⟯)
        ((Polynomial.C : (a : ↥K⟮f⟯) → (↥K⟮f⟯)[X]) (leadingCoeff (f.minpolyX ↥K⟮f⟯))⁻¹)).natDegree =
    max f.num.natDegree f.denom.natDegree
neg₃ :
  (HMul.hMul (α := (↥K⟮f⟯)[X]) ((Polynomial.C : (a : ↥K⟮f⟯) → (↥K⟮f⟯)[X]) (leadingCoeff (f.minpolyX ↥K⟮f⟯))⁻¹)
        (f.minpolyX ↥K⟮f⟯)).natDegree =
    max f.num.natDegree f.denom.natDegree
neg₄ : natDegree (R := ↥K⟮f⟯) (f.minpolyX ↥K⟮f⟯) = max f.num.natDegree f.denom.natDegree
⊢ Module.finrank.{u_1, u_1} (↥K⟮f⟯) K⟮X⟯ = max f.num.natDegree f.denom.natDegree
have neg₅ : max f.num.natDegree f.denom.natDegree = max f.num.natDegree f.denom.natDegree
Tactic: rw [← (IntermediateField.adjoinXEquiv K⟮f⟯).toLinearEquiv.finrank_eq,
    adjoin.finrank (f.isAlgebraic_adjoin_simple_X hf).isIntegral,
    ← minpoly.eq_of_irreducible (f.irreducible_minpolyX hf) f.minpolyX_aeval_X, mul_comm,
    natDegree_C_mul <| inv_ne_zero <| leadingCoeff_ne_zero.mpr fun H ↦
    hf ((minpolyX_eq_zero_iff f).mp H), natDegree_minpolyX]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (hypothesis)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
hE : E ≠ ⊥
⊢ IsAlgebraic.{u_1, u_1} ↥E (A := K⟮X⟯) X
have hE₁ : ∃ x ∈ E, x ∉ ⊥
Tactic: rw [ne_eq, ← le_bot_iff, SetLike.not_le_iff_exists] at hE
Cleared hypotheses: hE
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
hE : ∃ x ∈ E, x ∉ ⊥
⊢ IsAlgebraic.{u_1, u_1} ↥E (A := K⟮X⟯) X
have obtain : ∀ (f : K⟮X⟯) (hf₁ : f ∈ E) (hf₂ : f ∉ ⊥), IsAlgebraic.{u_1, u_1} ↥E (A := K⟮X⟯) X
Tactic: obtain ⟨f, hf₁, hf₂⟩ := hE
Cleared hypotheses: hE
-- 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 = Module.finrank.{u_1, u_1} (↥E) K⟮X⟯
have rw : (φ E).natDegree = Module.finrank.{u_1, u_1} ↥E ↥(↥E)⟮ X⟯
Tactic: rw [← (IntermediateField.adjoinXEquiv E).toLinearEquiv.finrank_eq,
    adjoin.finrank (IntermediateField.isAlgebraic_X h).isIntegral]
-- 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 : (φ E).natDegree = Module.finrank.{u_1, u_1} ↥E ↥(↥E)⟮ X⟯
⊢ (φ E).natDegree = Module.finrank.{u_1, u_1} (↥E) K⟮X⟯
have rw₁ : (φ E).natDegree = natDegree.{u_1} (R := ↥E) (minpoly ↥E (B := K⟮X⟯) X)
Tactic: rw [← (IntermediateField.adjoinXEquiv E).toLinearEquiv.finrank_eq,
    adjoin.finrank (IntermediateField.isAlgebraic_X h).isIntegral]
-- 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 ≠ ⊥
⊢ ∃ (i : ℕ), (φ E).coeff i ∉ RingHom.range (R := K) (algebraMap K ↥E)
have rw : φ E ∉ RingHom.range (R := K[X]) (Polynomial.mapRingHom (algebraMap K ↥E))
Tactic: rw [← notMem_map_range]
-- 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 : K[X]
hf : ((Polynomial.mapRingHom (algebraMap K ↥E) : K[X] →+* (↥E)[X]) : (a : K[X]) → (↥E)[X]) f = φ E
⊢ False
have hf₁ : Polynomial.map (algebraMap K ↥E) f = φ E
Tactic: rw [coe_mapRingHom] at hf
Cleared hypotheses: hf
-- 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 : K[X]
hf : Polynomial.map (algebraMap K ↥E) f = φ E
⊢ False
have refine_1 : f ≠ 0
Tactic: refine transcendental_X ⟨f, ?_, ?_⟩
-- 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 : K[X]
hf : Polynomial.map (algebraMap K ↥E) f = φ E
refine_1 : f ≠ 0
⊢ False
have refine_2 : Eq (α := K⟮X⟯) ((aeval X : (a : K[X]) → K⟮X⟯) f : K⟮X⟯) (0 : K⟮X⟯)
Tactic: refine transcendental_X ⟨f, ?_, ?_⟩
-- 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 : K[X]
hf : Polynomial.map (algebraMap K ↥E) f = φ E
⊢ f ≠ 0
have refine_1 : Ne (α := (↥E)[X]) (Polynomial.map (algebraMap K ↥E) f) 0
Tactic: apply (Polynomial.map_ne_zero_iff (FaithfulSMul.algebraMap_injective K E)).mp
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
⊢ generator E ∈ E
have pos : ∀ (h : E = ⊥), generator E ∈ E
Tactic: by_cases h : E = ⊥
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
pos : ∀ (h : E = ⊥), generator E ∈ E
⊢ generator E ∈ E
have neg : ∀ (h : ¬E = ⊥), generator E ∈ E
Tactic: by_cases h : 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 = ⊥
⊢ generator E ∈ E
have pos : 0 ∈ E
Tactic: rw [generator_eq_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 = ⊥
⊢ generator E ∈ E
have neg : (↑((φ E).coeff (generatorIndex h)) : K⟮X⟯) ∈ E
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 ≠ ⊥
⊢ generator E ∉ RingHom.range (R := K) (algebraMap K K⟮X⟯)
have rw : (↑((φ E).coeff (generatorIndex h)) : K⟮X⟯) ∉ RingHom.range (R := K) (algebraMap K 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 ≠ ⊥
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 =
    (φ E).coeff (⋯.choose (p := fun (i : ℕ) ↦ (φ E).coeff i ∉ RingHom.range (R := K) (algebraMap K ↥E)))
have a : (↑(((algebraMap K ↥E : K →+* ↥E) : (a : K) → ↥E) f) : K⟮X⟯) =
  (↑((φ E).coeff (sorry.choose (p := fun (i : ℕ) ↦ (φ E).coeff i ∉ RingHom.range (R := K) (algebraMap K ↥E)))) : K⟮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 ≠ ⊥
⊢ 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 : 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: rw [map_mul, mul_assoc]
-- 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])
      ((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)
have 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))
Tactic: enter [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 ≠ ⊥
| 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))
have 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)
Tactic: rw [← Polynomial.smul_eq_C_mul, algebraMap_smul, ← Φ'_map, eq_C_content_mul_primPart (Φ' 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])
      ((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)
have 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)
Tactic: enter [1, 2]
    rw [← Polynomial.smul_eq_C_mul, algebraMap_smul, ← Φ'_map, eq_C_content_mul_primPart (Φ' 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])
      ((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)
have 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)
Tactic: conv =>
    enter [1, 2]
    rw [← Polynomial.smul_eq_C_mul, algebraMap_smul, ← Φ'_map, eq_C_content_mul_primPart (Φ' 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⟯) (Φ' 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)
have rw : Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (Φ' E).content : K⟮X⟯) (0 : K⟮X⟯)
Tactic: rw [Polynomial.map_mul, map_C, ← mul_assoc, ← C_mul, inv_mul_cancel₀, map_one, one_mul]
-- 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).content : K⟮X⟯) (0 : K⟮X⟯)
have rw : ¬Φ' E = 0
Tactic: rw [ne_eq, FaithfulSMul.algebraMap_eq_zero_iff, content_eq_zero_iff]
-- 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]) (c E) : K⟮X⟯[X])
      (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⟯) (Φ' 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)
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 ≠ ⊥
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)
⊢ 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₁ : 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: 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 ≠ ⊥
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)
⊢ 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₄ : 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: 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