awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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)
h₅ 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⟯)
⊢ f = (C : (a : K) → K⟮X⟯) (a / b)

Tactic:
rw [← num_div_denom f, ← ha, ← hb, algebraMap_C, algebraMap_C, map_div₀]

Premises used: RatFunc.algebraMap_C, map_div₀, RatFunc.num_div_denom
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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
rw₂ rw₃ : Eq.{u + 1} (α := L) 0 0
⊢ eval f a x = 0

Tactic:
rw [eval, h, div_zero]

Premises used: RatFunc.eval, div_zero
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
x : K⟮X⟯
h : eval f a x ≠ 0
⊢ Polynomial.eval₂ f a x.denom ≠ 0

Tactic:
mt eval_eq_zero_of_eval₂_denom_eq_zero h

Premises used: mt, RatFunc.eval_eq_zero_of_eval₂_denom_eq_zero
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
c : K
⊢ eval f a ((C : (a : K) → K⟮X⟯) c) = (f : (a : K) → L) c

Tactic:
simp [eval]

Premises used: RatFunc.eval
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
⊢ eval f a X = a

Tactic:
simp [eval]

Premises used: RatFunc.eval
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
⊢ eval f a 0 = 0

Tactic:
simp [eval]

Premises used: RatFunc.eval
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
⊢ eval f a 1 = 1

Tactic:
simp [eval]

Premises used: RatFunc.eval
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u
inst : Field K
L : Type u
inst_1 : Field L
f : K →+* L
a : L
S : Type u_1
inst_2 : CommSemiring S
inst_3 : Algebra.{u_1, u} S K[X]
p : S
⊢ eval f a ((algebraMap S K⟮X⟯ : (a : S) → K⟮X⟯) p) = Polynomial.eval₂ f a ((algebraMap S K[X] : (a : S) → K[X]) p)

Tactic:
simp [eval, IsScalarTower.algebraMap_apply S K[X] K⟮X⟯]

Premises used: RatFunc.eval, Polynomial, RatFunc, IsScalarTower.algebraMap_apply
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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
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
⊢ eval f a (x + y) = eval f a x + eval f a y

Tactic:
unfold eval

Premises used: RatFunc.eval
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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
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
⊢ 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

Premises used: RatFunc.denom, Polynomial.eval₂, HAdd.hAdd
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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.denom * y.denom) = 0

Tactic:
have := Polynomial.eval₂_eq_zero_of_dvd_of_eval₂_eq_zero f a (denom_add_dvd x y) hxy
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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.denom * Polynomial.eval₂ f a y.denom = 0

Tactic:
rw [Polynomial.eval₂_mul] at this

Premises used: Polynomial.eval₂_mul
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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
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
⊢ 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

Premises used: mul_eq_zero, Iff.mp
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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
h : 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:
contradiction
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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
h : 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:
contradiction
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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
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
⊢ 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:
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]

Premises used: div_eq_mul_inv, div_eq_iff, div_add_div, mul_right_comm, mul_ne_zero, eq_div_iff
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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
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)
⊢ 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:
simp only [← Polynomial.eval₂_mul, ← Polynomial.eval₂_add]

Premises used: Polynomial.eval₂_mul, Polynomial.eval₂_add
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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
neg : (x + y).num * (x.denom * y.denom) = (x.num * y.denom + x.denom * y.num) * (x + y).denom
⊢ 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:
congr 1
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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
⊢ (x + y).num * (x.denom * y.denom) = (x.num * y.denom + x.denom * y.num) * (x + y).denom

Tactic:
apply num_denom_add

Premises used: RatFunc.num_denom_add
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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
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)
⊢ eval f a (x * y) = eval f a x * eval f a y

Tactic:
unfold eval

Premises used: RatFunc.eval
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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)
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)
⊢ 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

Premises used: RatFunc.denom, HMul.hMul, Polynomial.eval₂
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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.denom * y.denom) = 0

Tactic:
have := Polynomial.eval₂_eq_zero_of_dvd_of_eval₂_eq_zero f a (denom_mul_dvd x y) hxy
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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.denom * Polynomial.eval₂ f a y.denom = 0

Tactic:
rw [Polynomial.eval₂_mul] at this

Premises used: Polynomial.eval₂_mul
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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)
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)
⊢ 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

Premises used: mul_eq_zero, Iff.mp
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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
h : 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:
contradiction
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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
h : 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:
contradiction
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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
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
⊢ 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:
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]

Premises used: div_mul_div_comm, div_eq_mul_inv, div_eq_iff, mul_right_comm, mul_ne_zero, eq_div_iff
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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
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
⊢ 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 [← Polynomial.eval₂_mul]

Premises used: Polynomial.eval₂_mul
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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
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
⊢ 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]

Premises used: Polynomial.eval₂_mul
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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
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
⊢ 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]

Premises used: Polynomial.eval₂_mul
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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
neg : Polynomial.eval₂ f a ((x * y).num * (x.denom * y.denom)) = Polynomial.eval₂ f a (x.num * y.num * (x * y).denom)
⊢ 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]

Premises used: Polynomial.eval₂_mul
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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
neg : Polynomial.eval₂ f a ((x * y).num * (x.denom * y.denom)) = Polynomial.eval₂ f a (x.num * y.num * (x * y).denom)
⊢ 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:
repeat' rw [← Polynomial.eval₂_mul]

Premises used: Polynomial.eval₂_mul
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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
neg : (x * y).num * (x.denom * y.denom) = x.num * y.num * (x * y).denom
⊢ Polynomial.eval₂ f a ((x * y).num * (x.denom * y.denom)) = Polynomial.eval₂ f a (x.num * y.num * (x * y).denom)

Tactic:
congr 1
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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
⊢ (x * y).num * (x.denom * y.denom) = x.num * y.num * (x * y).denom

Tactic:
apply num_denom_mul

Premises used: RatFunc.num_denom_mul
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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]
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)
⊢ 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⟯)

Tactic:
ext
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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} (α := 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:
simp [algEquivOfTranscendental]

Premises used: RatFunc.algEquivOfTranscendental
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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
⊢ (↑((algEquivOfTranscendental f h : (a : K⟮X⟯) → ↥K⟮f⟯) X) : L) = f

Tactic:
simp [← algebraMap_X]

Premises used: RatFunc.algebraMap_X
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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⟯
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)
| (↑((algEquivOfTranscendental f h : (a : K⟮X⟯) → ↥K⟮f⟯) u) : L)

Tactic:
rw [← num_div_denom u]

Premises used: RatFunc.num_div_denom
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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⟯
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)
⊢ (↑((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)

Tactic:
conv_lhs => rw [← num_div_denom u]

Premises used: RatFunc.num_div_denom
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
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⟯)
          (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:
simp [-num_div_denom]

Premises used: RatFunc.num_div_denom