awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : Field K
f : K⟮X⟯
a : K
ha : (Polynomial.C : (a : K) → K[X]) a = f.num
b : K
hb : (Polynomial.C : (a : K) → K[X]) b = f.denom
h :
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.num : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.denom : K⟮X⟯) =
    (C : (a : K) → K⟮X⟯) (a / b)
h₁ :
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Polynomial.C : (a : K) → K[X]) a) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.denom : K⟮X⟯) =
    (C : (a : K) → K⟮X⟯) (a / b)
h₂ :
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Polynomial.C : (a : K) → K[X]) a) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Polynomial.C : (a : K) → K[X]) b) : K⟮X⟯) =
    (C : (a : K) → K⟮X⟯) (a / b)
h₃ :
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((C : (a : K) → K⟮X⟯) a : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((Polynomial.C : (a : K) → K[X]) b) : K⟮X⟯) =
    (C : (a : K) → K⟮X⟯) (a / b)
h₄ :
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((C : (a : K) → K⟮X⟯) a : K⟮X⟯) ((C : (a : K) → K⟮X⟯) b : K⟮X⟯) =
    (C : (a : K) → K⟮X⟯) (a / b)
⊢ f = (C : (a : K) → K⟮X⟯) (a / b)
have h₅ : HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((C : (a : K) → K⟮X⟯) a : K⟮X⟯) ((C : (a : K) → K⟮X⟯) b : K⟮X⟯) =
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((C : (a : K) → K⟮X⟯) a : K⟮X⟯) ((C : (a : K) → K⟮X⟯) b : K⟮X⟯)
Tactic: rw [← num_div_denom f, ← ha, ← hb, algebraMap_C, algebraMap_C, map_div₀]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
x : K⟮X⟯
h : Polynomial.eval₂ f a x.denom = 0
⊢ eval f a x = 0
have rw : Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom = 0
Tactic: rw [eval, h, div_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
x : K⟮X⟯
h : Polynomial.eval₂ f a x.denom = 0
rw : Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom = 0
⊢ eval f a x = 0
have rw₁ : Polynomial.eval₂ f a x.num / 0 = 0
Tactic: rw [eval, h, div_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
x : K⟮X⟯
h : Polynomial.eval₂ f a x.denom = 0
rw : Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom = 0
rw₁ : Polynomial.eval₂ f a x.num / 0 = 0
⊢ eval f a x = 0
have rw₂ : Eq.{u + 1} (α := L) 0 0
Tactic: rw [eval, h, div_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
⊢ eval f a (x + y) = eval f a x + eval f a y
have unfold : Polynomial.eval₂ f a (x + y).num / Polynomial.eval₂ f a (x + y).denom =
  Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom + Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom
Tactic: unfold eval
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
⊢ Polynomial.eval₂ f a (x + y).num / Polynomial.eval₂ f a (x + y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom +
      Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom
have pos : ∀ (hxy : Polynomial.eval₂ f a (x + y).denom = 0),
  Polynomial.eval₂ f a (x + y).num / Polynomial.eval₂ f a (x + y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom +
      Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom
Tactic: by_cases hxy : Polynomial.eval₂ f a (denom (x + y)) = 0
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
pos :
  ∀ (hxy : Polynomial.eval₂ f a (x + y).denom = 0),
    Polynomial.eval₂ f a (x + y).num / Polynomial.eval₂ f a (x + y).denom =
      Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom +
        Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom
⊢ Polynomial.eval₂ f a (x + y).num / Polynomial.eval₂ f a (x + y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom +
      Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom
have neg : ∀ (hxy : ¬Polynomial.eval₂ f a (x + y).denom = 0),
  Polynomial.eval₂ f a (x + y).num / Polynomial.eval₂ f a (x + y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom +
      Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom
Tactic: by_cases hxy : Polynomial.eval₂ f a (denom (x + y)) = 0
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (hypothesis)
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : Polynomial.eval₂ f a (x + y).denom = 0
⊢ Polynomial.eval₂ f a (x + y).num / Polynomial.eval₂ f a (x + y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom +
      Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom
have this : Polynomial.eval₂ f a (x.denom * y.denom) = 0
Tactic: have := Polynomial.eval₂_eq_zero_of_dvd_of_eval₂_eq_zero f a (denom_add_dvd x y) hxy
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (hypothesis)
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : Polynomial.eval₂ f a (x + y).denom = 0
this : Polynomial.eval₂ f a (x.denom * y.denom) = 0
⊢ Polynomial.eval₂ f a (x + y).num / Polynomial.eval₂ f a (x + y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom +
      Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom
have this₁ : Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom = 0
Tactic: rw [Polynomial.eval₂_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : Polynomial.eval₂ f a (x + y).denom = 0
this : Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom = 0
⊢ Polynomial.eval₂ f a (x + y).num / Polynomial.eval₂ f a (x + y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom +
      Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom
have pos : Polynomial.eval₂ f a x.denom = 0 →
  Polynomial.eval₂ f a (x + y).num / Polynomial.eval₂ f a (x + y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom +
      Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom
Tactic: cases mul_eq_zero.mp this
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : Polynomial.eval₂ f a (x + y).denom = 0
this : Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom = 0
pos :
  Polynomial.eval₂ f a x.denom = 0 →
    Polynomial.eval₂ f a (x + y).num / Polynomial.eval₂ f a (x + y).denom =
      Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom +
        Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom
⊢ Polynomial.eval₂ f a (x + y).num / Polynomial.eval₂ f a (x + y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom +
      Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom
have pos₁ : Polynomial.eval₂ f a y.denom = 0 →
  Polynomial.eval₂ f a (x + y).num / Polynomial.eval₂ f a (x + y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom +
      Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom
Tactic: cases mul_eq_zero.mp this
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : ¬Polynomial.eval₂ f a (x + y).denom = 0
⊢ Polynomial.eval₂ f a (x + y).num / Polynomial.eval₂ f a (x + y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom +
      Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom
have neg : Polynomial.eval₂ f a (x + y).num * (Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom) =
  (Polynomial.eval₂ f a x.num * Polynomial.eval₂ f a y.denom +
      Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.num) *
    Polynomial.eval₂ f a (x + y).denom
Tactic: rw [div_add_div _ _ hx hy, eq_div_iff (mul_ne_zero hx hy), div_eq_mul_inv, mul_right_comm, ←
    div_eq_mul_inv, div_eq_iff hxy]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : ¬Polynomial.eval₂ f a (x + y).denom = 0
⊢ Polynomial.eval₂ f a (x + y).num * (Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom) =
    (Polynomial.eval₂ f a x.num * Polynomial.eval₂ f a y.denom +
        Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.num) *
      Polynomial.eval₂ f a (x + y).denom
have neg : Polynomial.eval₂ f a ((x + y).num * (x.denom * y.denom)) =
  Polynomial.eval₂ f a ((x.num * y.denom + x.denom * y.num) * (x + y).denom)
Tactic: simp only [← Polynomial.eval₂_mul, ← Polynomial.eval₂_add]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : ¬Polynomial.eval₂ f a (x + y).denom = 0
⊢ Polynomial.eval₂ f a ((x + y).num * (x.denom * y.denom)) =
    Polynomial.eval₂ f a ((x.num * y.denom + x.denom * y.num) * (x + y).denom)
have neg : (x + y).num * (x.denom * y.denom) = (x.num * y.denom + x.denom * y.num) * (x + y).denom
Tactic: congr 1
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
⊢ eval f a (x * y) = eval f a x * eval f a y
have unfold : Polynomial.eval₂ f a (x * y).num / Polynomial.eval₂ f a (x * y).denom =
  Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom *
    (Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom)
Tactic: unfold eval
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
⊢ Polynomial.eval₂ f a (x * y).num / Polynomial.eval₂ f a (x * y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom *
      (Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom)
have pos : ∀ (hxy : Polynomial.eval₂ f a (x * y).denom = 0),
  Polynomial.eval₂ f a (x * y).num / Polynomial.eval₂ f a (x * y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom *
      (Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom)
Tactic: by_cases hxy : Polynomial.eval₂ f a (denom (x * y)) = 0
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
pos :
  ∀ (hxy : Polynomial.eval₂ f a (x * y).denom = 0),
    Polynomial.eval₂ f a (x * y).num / Polynomial.eval₂ f a (x * y).denom =
      Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom *
        (Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom)
⊢ Polynomial.eval₂ f a (x * y).num / Polynomial.eval₂ f a (x * y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom *
      (Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom)
have neg : ∀ (hxy : ¬Polynomial.eval₂ f a (x * y).denom = 0),
  Polynomial.eval₂ f a (x * y).num / Polynomial.eval₂ f a (x * y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom *
      (Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom)
Tactic: by_cases hxy : Polynomial.eval₂ f a (denom (x * y)) = 0
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (hypothesis)
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : Polynomial.eval₂ f a (x * y).denom = 0
⊢ Polynomial.eval₂ f a (x * y).num / Polynomial.eval₂ f a (x * y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom *
      (Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom)
have this : Polynomial.eval₂ f a (x.denom * y.denom) = 0
Tactic: have := Polynomial.eval₂_eq_zero_of_dvd_of_eval₂_eq_zero f a (denom_mul_dvd x y) hxy
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (hypothesis)
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : Polynomial.eval₂ f a (x * y).denom = 0
this : Polynomial.eval₂ f a (x.denom * y.denom) = 0
⊢ Polynomial.eval₂ f a (x * y).num / Polynomial.eval₂ f a (x * y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom *
      (Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom)
have this₁ : Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom = 0
Tactic: rw [Polynomial.eval₂_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : Polynomial.eval₂ f a (x * y).denom = 0
this : Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom = 0
⊢ Polynomial.eval₂ f a (x * y).num / Polynomial.eval₂ f a (x * y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom *
      (Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom)
have pos : Polynomial.eval₂ f a x.denom = 0 →
  Polynomial.eval₂ f a (x * y).num / Polynomial.eval₂ f a (x * y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom *
      (Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom)
Tactic: cases mul_eq_zero.mp this
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : Polynomial.eval₂ f a (x * y).denom = 0
this : Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom = 0
pos :
  Polynomial.eval₂ f a x.denom = 0 →
    Polynomial.eval₂ f a (x * y).num / Polynomial.eval₂ f a (x * y).denom =
      Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom *
        (Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom)
⊢ Polynomial.eval₂ f a (x * y).num / Polynomial.eval₂ f a (x * y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom *
      (Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom)
have pos₁ : Polynomial.eval₂ f a y.denom = 0 →
  Polynomial.eval₂ f a (x * y).num / Polynomial.eval₂ f a (x * y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom *
      (Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom)
Tactic: cases mul_eq_zero.mp this
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : ¬Polynomial.eval₂ f a (x * y).denom = 0
⊢ Polynomial.eval₂ f a (x * y).num / Polynomial.eval₂ f a (x * y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom *
      (Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom)
have neg : Polynomial.eval₂ f a (x * y).num * (Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom) =
  Polynomial.eval₂ f a x.num * Polynomial.eval₂ f a y.num * Polynomial.eval₂ f a (x * y).denom
Tactic: rw [div_mul_div_comm, eq_div_iff (mul_ne_zero hx hy), div_eq_mul_inv, mul_right_comm, ←
    div_eq_mul_inv, div_eq_iff hxy]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : ¬Polynomial.eval₂ f a (x * y).denom = 0
⊢ Polynomial.eval₂ f a (x * y).num * (Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom) =
    Polynomial.eval₂ f a x.num * Polynomial.eval₂ f a y.num * Polynomial.eval₂ f a (x * y).denom
have neg : Polynomial.eval₂ f a (x * y).num * Polynomial.eval₂ f a (x.denom * y.denom) =
  Polynomial.eval₂ f a x.num * Polynomial.eval₂ f a y.num * Polynomial.eval₂ f a (x * y).denom
Tactic: rw [← Polynomial.eval₂_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : ¬Polynomial.eval₂ f a (x * y).denom = 0
⊢ Polynomial.eval₂ f a (x * y).num * Polynomial.eval₂ f a (x.denom * y.denom) =
    Polynomial.eval₂ f a x.num * Polynomial.eval₂ f a y.num * Polynomial.eval₂ f a (x * y).denom
have neg : Polynomial.eval₂ f a ((x * y).num * (x.denom * y.denom)) =
  Polynomial.eval₂ f a x.num * Polynomial.eval₂ f a y.num * Polynomial.eval₂ f a (x * y).denom
Tactic: rw [← Polynomial.eval₂_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : ¬Polynomial.eval₂ f a (x * y).denom = 0
⊢ Polynomial.eval₂ f a ((x * y).num * (x.denom * y.denom)) =
    Polynomial.eval₂ f a x.num * Polynomial.eval₂ f a y.num * Polynomial.eval₂ f a (x * y).denom
have neg : Polynomial.eval₂ f a ((x * y).num * (x.denom * y.denom)) =
  Polynomial.eval₂ f a (x.num * y.num) * Polynomial.eval₂ f a (x * y).denom
Tactic: rw [← Polynomial.eval₂_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : ¬Polynomial.eval₂ f a (x * y).denom = 0
⊢ Polynomial.eval₂ f a ((x * y).num * (x.denom * y.denom)) =
    Polynomial.eval₂ f a (x.num * y.num) * Polynomial.eval₂ f a (x * y).denom
have neg : Polynomial.eval₂ f a ((x * y).num * (x.denom * y.denom)) = Polynomial.eval₂ f a (x.num * y.num * (x * y).denom)
Tactic: rw [← Polynomial.eval₂_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : ¬Polynomial.eval₂ f a (x * y).denom = 0
⊢ Polynomial.eval₂ f a (x * y).num * (Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom) =
    Polynomial.eval₂ f a x.num * Polynomial.eval₂ f a y.num * Polynomial.eval₂ f a (x * y).denom
have neg : Polynomial.eval₂ f a ((x * y).num * (x.denom * y.denom)) = Polynomial.eval₂ f a (x.num * y.num * (x * y).denom)
Tactic: repeat' rw [← Polynomial.eval₂_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : ¬Polynomial.eval₂ f a (x * y).denom = 0
⊢ Polynomial.eval₂ f a ((x * y).num * (x.denom * y.denom)) = Polynomial.eval₂ f a (x.num * y.num * (x * y).denom)
have neg : (x * y).num * (x.denom * y.denom) = x.num * y.num * (x * y).denom
Tactic: congr 1
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
f : L
h : Transcendental K f
g : K[X]
⊢ Eq.{u_2 + 1} (α := ↥K⟮f⟯)
    ((algEquivOfTranscendental f h : (a : K⟮X⟯) → ↥K⟮f⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) g) : ↥K⟮f⟯)
    ((aeval (AdjoinSimple.gen K f) : (a : K[X]) → ↥K⟮f⟯) g : ↥K⟮f⟯)
have a : Eq.{u_2 + 1} (α := L)
  (↑((algEquivOfTranscendental f h : (a : K⟮X⟯) → ↥K⟮f⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) g)) : L)
  (↑((aeval (AdjoinSimple.gen K f) : (a : K[X]) → ↥K⟮f⟯) g) : L)
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
f : L
h : Transcendental K f
u : K⟮X⟯
| (↑((algEquivOfTranscendental f h : (a : K⟮X⟯) → ↥K⟮f⟯) u) : L)
have rw : (↑((algEquivOfTranscendental f h : (a : K⟮X⟯) → ↥K⟮f⟯)
      (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) u.num : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) u.denom : K⟮X⟯))) :
  L)
Tactic: rw [← num_div_denom u]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
f : L
h : Transcendental K f
u : K⟮X⟯
⊢ (↑((algEquivOfTranscendental f h : (a : K⟮X⟯) → ↥K⟮f⟯) u) : L) =
    HDiv.hDiv (α := L) (β := L) ((aeval f : (a : K[X]) → L) u.num : L) ((aeval f : (a : K[X]) → L) u.denom : L)
have conv_lhs : (↑((algEquivOfTranscendental f h : (a : K⟮X⟯) → ↥K⟮f⟯)
        (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) u.num : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) u.denom : K⟮X⟯))) :
    L) =
  HDiv.hDiv (α := L) (β := L) ((aeval f : (a : K[X]) → L) u.num : L) ((aeval f : (a : K[X]) → L) u.denom : L)
Tactic: conv_lhs => rw [← num_div_denom u]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
⊢ Transcendental K (A := K⟮X⟯) X
have rw : Transcendental K (A := Polynomial K) Polynomial.X
Tactic: rw [← RatFunc.algebraMap_X, transcendental_algebraMap_iff (algebraMap_injective K)]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K_1 : Type u
K : Type u_1
inst : Field K
⊢ Ideal.IsPrime (α := K[X]) (Ideal.span {X})
have rw : Prime.{u_1} (M := K[X]) X
Tactic: rw [Ideal.span_singleton_prime]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K_1 : Type u
K : Type u_1
inst : Field K
rw : Prime.{u_1} (M := K[X]) X
⊢ Ideal.IsPrime (α := K[X]) (Ideal.span {X})
have rw₁ : Ne.{u_1 + 1} (α := K[X]) X 0
Tactic: rw [Ideal.span_singleton_prime]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K_1 : Type u
K : Type u_1
inst : Field K
⊢ Ne (α := Ideal K[X]) (Ideal.span {X}) ⊥
have rw : ¬Eq.{u_1 + 1} (α := K[X]) X 0
Tactic: rw [ne_eq, Ideal.span_singleton_eq_bot]