awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
⊢ Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯) (0 : K⟮X⟯)

Tactic:
algebraMap_ne_zero (denom_ne_zero x)

Premises used: RatFunc.algebraMap_ne_zero, RatFunc.denom_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
⊢ Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯) (0 : K⟮X⟯)

Tactic:
exact algebraMap_ne_zero (denom_ne_zero x)

Premises used: RatFunc.algebraMap_ne_zero, RatFunc.denom_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
⊢ Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.denom : K⟮X⟯) (0 : K⟮X⟯)

Tactic:
algebraMap_ne_zero (denom_ne_zero y)

Premises used: RatFunc.algebraMap_ne_zero, RatFunc.denom_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
⊢ Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.denom : K⟮X⟯) (0 : K⟮X⟯)

Tactic:
exact algebraMap_ne_zero (denom_ne_zero y)

Premises used: RatFunc.algebraMap_ne_zero, RatFunc.denom_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
rw :
  -x =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (-x.num) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯)
rw₁ :
  -x =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) (-(algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯)
rw₂ :
  -x =
    -HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯)
rw₃ rw₄ : -x = -x
⊢ (-x).num * x.denom = -x.num * (-x).denom

Tactic:
rw [num_mul_eq_mul_denom_iff (denom_ne_zero x), map_neg, neg_div, num_div_denom]

Premises used: neg_div, map_neg, RatFunc.num_mul_eq_mul_denom_iff, RatFunc.num_div_denom, RatFunc.denom_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
rw :
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * y.num) : K⟮X⟯)
    ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)
| x * y

Tactic:
rw [← num_div_denom x, ← num_div_denom y, div_mul_div_comm, ← map_mul, ← map_mul]

Premises used: div_mul_div_comm, map_mul, RatFunc.num_div_denom
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
conv_lhs :
  x * y =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * y.num) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)
conv_lhs₁ :
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * y.num) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯) =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * y.num) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)
⊢ x * y =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * y.num) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)

Tactic:
conv_lhs =>
      rw [← num_div_denom x, ← num_div_denom y, div_mul_div_comm, ← map_mul, ← map_mul]

Premises used: div_mul_div_comm, map_mul, RatFunc.num_div_denom
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
p : K[X]
hp : p ≠ 0
mp :
  x.num ∣ p →
    ∃ (q : K[X]),
      q ≠ 0 ∧
        x =
          HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
            ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)
mpr :
  (∃ (q : K[X]),
      q ≠ 0 ∧
        x =
          HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
            ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)) →
    x.num ∣ p
⊢ x.num ∣ p ↔
    ∃ (q : K[X]),
      q ≠ 0 ∧
        x =
          HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
            ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)

Tactic:
constructor
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
q : K[X]
hp : x.num * q ≠ 0
⊢ x.num ≠ 0

Tactic:
obtain ⟨_hx, hq⟩ := mul_ne_zero_iff.mp hp

Premises used: Iff.mp, mul_ne_zero_iff
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
q : K[X]
hp : x.num * q ≠ 0
_hx : x.num ≠ 0
⊢ q ≠ 0

Tactic:
obtain ⟨_hx, hq⟩ := mul_ne_zero_iff.mp hp

Premises used: Iff.mp, mul_ne_zero_iff
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
q : K[X]
hp : x.num * q ≠ 0
_hx : x.num ≠ 0
hq : q ≠ 0
h :
  x.denom * q ≠ 0 ∧
    x =
      HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * q) : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * q) : K⟮X⟯)
⊢ ∃ (q_1 : K[X]),
    q_1 ≠ 0 ∧
      x =
        HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * q) : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q_1 : K⟮X⟯)

Tactic:
use denom x * q

Premises used: RatFunc.denom
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
q : K[X]
hp : x.num * q ≠ 0
_hx : x.num ≠ 0
hq : q ≠ 0
h : x.denom * q ≠ 0 ∧ x = x
h₁ : Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) (0 : K⟮X⟯)
⊢ x.denom * q ≠ 0 ∧
    x =
      HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * q) : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * q) : K⟮X⟯)

Tactic:
rw [map_mul, map_mul, ← div_mul_div_comm, div_self, mul_one, num_div_denom]

Premises used: div_mul_div_comm, map_mul, mul_one, RatFunc.num_div_denom, div_self
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
q : K[X]
hp : x.num * q ≠ 0
_hx : x.num ≠ 0
hq : q ≠ 0
⊢ x.denom * q ≠ 0 ∧ x = x

Tactic:
⟨mul_ne_zero (denom_ne_zero x) hq, rfl⟩

Premises used: And.intro, mul_ne_zero, rfl, RatFunc.denom_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
q : K[X]
hp : x.num * q ≠ 0
_hx : x.num ≠ 0
hq : q ≠ 0
⊢ x.denom * q ≠ 0 ∧ x = x

Tactic:
exact ⟨mul_ne_zero (denom_ne_zero x) hq, rfl⟩
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
q : K[X]
hp : x.num * q ≠ 0
_hx : x.num ≠ 0
hq : q ≠ 0
⊢ Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) (0 : K⟮X⟯)

Tactic:
algebraMap_ne_zero hq

Premises used: RatFunc.algebraMap_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
q : K[X]
hp : x.num * q ≠ 0
_hx : x.num ≠ 0
hq : q ≠ 0
⊢ Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) (0 : K⟮X⟯)

Tactic:
exact algebraMap_ne_zero hq

Premises used: RatFunc.algebraMap_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
p : K[X]
hp : p ≠ 0
q : K[X]
hq : q ≠ 0
⊢ (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)).num ∣
    p

Tactic:
num_div_dvd p hq

Premises used: RatFunc.num_div_dvd
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
p : K[X]
hp : p ≠ 0
q : K[X]
hq : q ≠ 0
⊢ (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)).num ∣
    p

Tactic:
exact num_div_dvd p hq

Premises used: RatFunc.num_div_dvd
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
q : K[X]
hq : q ≠ 0
mp :
  x.denom ∣ q →
    ∃ (p : K[X]),
      x =
        HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)
mpr :
  (∃ (p : K[X]),
      x =
        HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)) →
    x.denom ∣ q
⊢ x.denom ∣ q ↔
    ∃ (p : K[X]),
      x =
        HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)

Tactic:
constructor
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
p : K[X]
hq : x.denom * p ≠ 0
⊢ x.denom ≠ 0

Tactic:
obtain ⟨_hx, hp⟩ := mul_ne_zero_iff.mp hq

Premises used: Iff.mp, mul_ne_zero_iff
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
p : K[X]
hq : x.denom * p ≠ 0
_hx : x.denom ≠ 0
⊢ p ≠ 0

Tactic:
obtain ⟨_hx, hp⟩ := mul_ne_zero_iff.mp hq

Premises used: Iff.mp, mul_ne_zero_iff
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
p : K[X]
hq : x.denom * p ≠ 0
_hx : x.denom ≠ 0
hp : p ≠ 0
h :
  x =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * p) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * p) : K⟮X⟯)
⊢ ∃ (p_1 : K[X]),
    x =
      HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p_1 : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * p) : K⟮X⟯)

Tactic:
use num x * p

Premises used: RatFunc.num
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
p : K[X]
hq : x.denom * p ≠ 0
_hx : x.denom ≠ 0
hp : p ≠ 0
h : Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯) (0 : K⟮X⟯)
⊢ x =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * p) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * p) : K⟮X⟯)

Tactic:
rw [map_mul, map_mul, ← div_mul_div_comm, div_self, mul_one, num_div_denom]

Premises used: div_mul_div_comm, map_mul, mul_one, RatFunc.num_div_denom, div_self
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
p : K[X]
hq : x.denom * p ≠ 0
_hx : x.denom ≠ 0
hp : p ≠ 0
⊢ Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯) (0 : K⟮X⟯)

Tactic:
algebraMap_ne_zero hp

Premises used: RatFunc.algebraMap_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
p : K[X]
hq : x.denom * p ≠ 0
_hx : x.denom ≠ 0
hp : p ≠ 0
⊢ Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯) (0 : K⟮X⟯)

Tactic:
exact algebraMap_ne_zero hp

Premises used: RatFunc.algebraMap_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
q : K[X]
hq : q ≠ 0
p : K[X]
⊢ (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)).denom ∣
    q

Tactic:
denom_div_dvd p q

Premises used: RatFunc.denom_div_dvd
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
q : K[X]
hq : q ≠ 0
p : K[X]
⊢ (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)).denom ∣
    q

Tactic:
exact denom_div_dvd p q

Premises used: RatFunc.denom_div_dvd
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
pos : ∀ (hx : x = 0), (x * y).num ∣ x.num * y.num
neg : ∀ (hx : ¬x = 0), (x * y).num ∣ x.num * y.num
⊢ (x * y).num ∣ x.num * y.num

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hx : x = 0
⊢ (x * y).num ∣ x.num * y.num

Tactic:
simp [hx]
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hx : ¬x = 0
pos : ∀ (hy : y = 0), (x * y).num ∣ x.num * y.num
neg : ∀ (hy : ¬y = 0), (x * y).num ∣ x.num * y.num
⊢ (x * y).num ∣ x.num * y.num

Tactic:
by_cases hy : y = 0
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hx : ¬x = 0
hy : y = 0
⊢ (x * y).num ∣ x.num * y.num

Tactic:
simp [hy]
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hx : ¬x = 0
hy : ¬y = 0
neg :
  ∃ (q : K[X]),
    q ≠ 0 ∧
      x * y =
        HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * y.num) : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)
⊢ (x * y).num ∣ x.num * y.num

Tactic:
rw [num_dvd (mul_ne_zero (num_ne_zero hx) (num_ne_zero hy))]

Premises used: RatFunc.num_ne_zero, RatFunc.num_dvd, mul_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hx : ¬x = 0
hy : ¬y = 0
⊢ ∃ (q : K[X]),
    q ≠ 0 ∧
      x * y =
        HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * y.num) : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)

Tactic:
⟨x.denom * y.denom, mul_ne_zero (denom_ne_zero x) (denom_ne_zero y), ?_⟩

Premises used: RatFunc.denom, HMul.hMul, And.intro, Exists.intro, mul_ne_zero, RatFunc.denom_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hx : ¬x = 0
hy : ¬y = 0
neg :
  x * y =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * y.num) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)
⊢ ∃ (q : K[X]),
    q ≠ 0 ∧
      x * y =
        HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * y.num) : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)

Tactic:
refine ⟨x.denom * y.denom, mul_ne_zero (denom_ne_zero x) (denom_ne_zero y), ?_⟩
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hx : ¬x = 0
hy : ¬y = 0
neg :
  x * y =
    HDiv.hDiv (β := K⟮X⟯)
      (HMul.hMul (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.num : K⟮X⟯))
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)
neg₁ :
  x * y =
    HMul.hMul (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.num : K⟮X⟯) /
      HMul.hMul (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.denom : K⟮X⟯)
neg₂ :
  x * y =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯) *
      HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.num : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.denom : K⟮X⟯)
neg₃ :
  x * y =
    x *
      HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.num : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.denom : K⟮X⟯)
neg₄ neg₅ : x * y = x * y
⊢ x * y =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * y.num) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)

Tactic:
rw [map_mul, map_mul, ← div_mul_div_comm, num_div_denom, num_div_denom]

Premises used: div_mul_div_comm, map_mul, RatFunc.num_div_denom
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
rw :
  ∃ (p : K[X]),
    x * y =
      HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)
⊢ (x * y).denom ∣ x.denom * y.denom

Tactic:
rw [denom_dvd (mul_ne_zero (denom_ne_zero x) (denom_ne_zero y))]

Premises used: mul_ne_zero, RatFunc.denom_dvd, RatFunc.denom_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
⊢ ∃ (p : K[X]),
    x * y =
      HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)

Tactic:
⟨x.num * y.num, ?_⟩

Premises used: HMul.hMul, RatFunc.num, Exists.intro
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
refine :
  x * y =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * y.num) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)
⊢ ∃ (p : K[X]),
    x * y =
      HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)

Tactic:
refine ⟨x.num * y.num, ?_⟩
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
rw :
  x * y =
    HDiv.hDiv (β := K⟮X⟯)
      (HMul.hMul (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.num : K⟮X⟯))
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)
rw₁ :
  x * y =
    HMul.hMul (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.num : K⟮X⟯) /
      HMul.hMul (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.denom : K⟮X⟯)
rw₂ :
  x * y =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯) *
      HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.num : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.denom : K⟮X⟯)
rw₃ :
  x * y =
    x *
      HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.num : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.denom : K⟮X⟯)
rw₄ rw₅ : x * y = x * y
⊢ x * y =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * y.num) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)

Tactic:
rw [map_mul, map_mul, ← div_mul_div_comm, num_div_denom, num_div_denom]

Premises used: div_mul_div_comm, map_mul, RatFunc.num_div_denom
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
rw :
  ∃ (p : K[X]),
    x + y =
      HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)
⊢ (x + y).denom ∣ x.denom * y.denom

Tactic:
rw [denom_dvd (mul_ne_zero (denom_ne_zero x) (denom_ne_zero y))]

Premises used: mul_ne_zero, RatFunc.denom_dvd, RatFunc.denom_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
⊢ ∃ (p : K[X]),
    x + y =
      HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)

Tactic:
⟨x.num * y.denom + x.denom * y.num, ?_⟩

Premises used: RatFunc.denom, HMul.hMul, HAdd.hAdd, RatFunc.num, Exists.intro
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
refine :
  x + y =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * y.denom + x.denom * y.num) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)
⊢ ∃ (p : K[X]),
    x + y =
      HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)

Tactic:
refine ⟨x.num * y.denom + x.denom * y.num, ?_⟩
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hb : Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯) (0 : K⟮X⟯)
hd : Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.denom : K⟮X⟯) (0 : K⟮X⟯)
⊢ x + y =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * y.denom + x.denom * y.num) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)

Tactic:
rw [map_mul, map_add, map_mul, map_mul, ← div_add_div, num_div_denom, num_div_denom]

Premises used: map_add, map_mul, div_add_div, RatFunc.num_div_denom
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x ≠ 0
rw :
  ∃ (q : K[X]),
    q ≠ 0 ∧
      x⁻¹ =
        HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)
⊢ x⁻¹.num ∣ x.denom

Tactic:
rw [num_dvd x.denom_ne_zero]

Premises used: RatFunc.num_dvd, RatFunc.denom_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x ≠ 0
⊢ ∃ (q : K[X]),
    q ≠ 0 ∧
      x⁻¹ =
        HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)

Tactic:
⟨x.num, num_ne_zero hx, ?_⟩

Premises used: RatFunc.num_ne_zero, RatFunc.num, And.intro, Exists.intro
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x ≠ 0
refine :
  x⁻¹ =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
⊢ ∃ (q : K[X]),
    q ≠ 0 ∧
      x⁻¹ =
        HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)

Tactic:
refine ⟨x.num, num_ne_zero hx, ?_⟩
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x ≠ 0
nth_rw :
  (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯))⁻¹ =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
⊢ x⁻¹ =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)

Tactic:
nth_rw 1 [← x.num_div_denom]

Premises used: RatFunc.num_div_denom
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x ≠ 0
rw rw₁ :
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯) =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
⊢ (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯))⁻¹ =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)

Tactic:
rw [inv_div]

Premises used: inv_div
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x ≠ 0
rw :
  ∃ (p : K[X]),
    x⁻¹ =
      HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
⊢ x⁻¹.denom ∣ x.num

Tactic:
rw [denom_dvd (num_ne_zero hx)]

Premises used: RatFunc.num_ne_zero, RatFunc.denom_dvd
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x ≠ 0
⊢ ∃ (p : K[X]),
    x⁻¹ =
      HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)

Tactic:
⟨x.denom, ?_⟩

Premises used: RatFunc.denom, Exists.intro