awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x y : 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⟯)
have conv_lhs : 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⟯) =
  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: conv_lhs => rw [← num_div_denom x, ← num_div_denom y]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x y : 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⟯) y.num : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.denom : K⟮X⟯) =
    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⟯)
have hb : Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯) (0 : K⟮X⟯)
Tactic: rw [div_add_div, map_mul, map_add, map_mul, map_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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⟯)
⊢ 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⟯) =
    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⟯)
have hd : Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.denom : K⟮X⟯) (0 : K⟮X⟯)
Tactic: rw [div_add_div, map_mul, map_add, map_mul, map_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
⊢ (-x).num * x.denom = -x.num * (-x).denom
have 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⟯)
Tactic: rw [num_mul_eq_mul_denom_iff (denom_ne_zero x), map_neg, neg_div, num_div_denom]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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⟯)
⊢ (-x).num * x.denom = -x.num * (-x).denom
have 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⟯)
Tactic: rw [num_mul_eq_mul_denom_iff (denom_ne_zero x), map_neg, neg_div, num_div_denom]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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⟯)
⊢ (-x).num * x.denom = -x.num * (-x).denom
have 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⟯)
Tactic: rw [num_mul_eq_mul_denom_iff (denom_ne_zero x), map_neg, neg_div, num_div_denom]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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⟯)
⊢ (-x).num * x.denom = -x.num * (-x).denom
have rw₃ : -x = -x
Tactic: rw [num_mul_eq_mul_denom_iff (denom_ne_zero x), map_neg, neg_div, num_div_denom]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
| x * y
have 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⟯)
Tactic: rw [← num_div_denom x, ← num_div_denom y, div_mul_div_comm, ← map_mul, ← map_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x y : 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⟯)
have 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⟯)
Tactic: conv_lhs =>
      rw [← num_div_denom x, ← num_div_denom y, div_mul_div_comm, ← map_mul, ← map_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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⟯)
⊢ 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⟯)
have 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⟯)
Tactic: conv_lhs =>
      rw [← num_div_denom x, ← num_div_denom y, div_mul_div_comm, ← map_mul, ← map_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
p : K[X]
hp : p ≠ 0
⊢ 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⟯)
have 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⟯)
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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⟯)
⊢ 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⟯)
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (hypothesis)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
q : K[X]
hp : x.num * q ≠ 0
⊢ ∃ (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⟯)
have _hx : x.num ≠ 0
Tactic: obtain ⟨_hx, hq⟩ := mul_ne_zero_iff.mp hp
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (hypothesis)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
q : K[X]
hp : x.num * q ≠ 0
_hx : x.num ≠ 0
⊢ ∃ (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⟯)
have hq : q ≠ 0
Tactic: obtain ⟨_hx, hq⟩ := mul_ne_zero_iff.mp hp
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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
⊢ ∃ (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⟯)
have 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⟯)
Tactic: use denom x * q
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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 =
      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⟯)
have h : x.denom * q ≠ 0 ∧ x = x
Tactic: rw [map_mul, map_mul, ← div_mul_div_comm, div_self, mul_one, num_div_denom]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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
⊢ 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⟯)
have h₁ : Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) (0 : K⟮X⟯)
Tactic: rw [map_mul, map_mul, ← div_mul_div_comm, div_self, mul_one, num_div_denom]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
q : K[X]
hq : q ≠ 0
⊢ 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⟯)
have 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⟯)
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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⟯)
⊢ 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⟯)
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (hypothesis)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
p : K[X]
hq : x.denom * p ≠ 0
⊢ ∃ (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⟯)
have _hx : x.denom ≠ 0
Tactic: obtain ⟨_hx, hp⟩ := mul_ne_zero_iff.mp hq
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (hypothesis)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
p : K[X]
hq : x.denom * p ≠ 0
_hx : x.denom ≠ 0
⊢ ∃ (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⟯)
have hp : p ≠ 0
Tactic: obtain ⟨_hx, hp⟩ := mul_ne_zero_iff.mp hq
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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
⊢ ∃ (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⟯)
have 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⟯)
Tactic: use num x * p
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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
⊢ 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⟯)
have h : Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯) (0 : K⟮X⟯)
Tactic: rw [map_mul, map_mul, ← div_mul_div_comm, div_self, mul_one, num_div_denom]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
⊢ (x * y).num ∣ x.num * y.num
have pos : ∀ (hx : x = 0), (x * y).num ∣ x.num * y.num
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
pos : ∀ (hx : x = 0), (x * y).num ∣ x.num * y.num
⊢ (x * y).num ∣ x.num * y.num
have neg : ∀ (hx : ¬x = 0), (x * y).num ∣ x.num * y.num
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hx : ¬x = 0
⊢ (x * y).num ∣ x.num * y.num
have pos : ∀ (hy : y = 0), (x * y).num ∣ x.num * y.num
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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
⊢ (x * y).num ∣ x.num * y.num
have neg : ∀ (hy : ¬y = 0), (x * y).num ∣ x.num * y.num
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hx : ¬x = 0
hy : ¬y = 0
⊢ (x * y).num ∣ x.num * y.num
have 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⟯)
Tactic: rw [num_dvd (mul_ne_zero (num_ne_zero hx) (num_ne_zero hy))]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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⟯)
have 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⟯)
Tactic: refine ⟨x.denom * y.denom, mul_ne_zero (denom_ne_zero x) (denom_ne_zero y), ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hx : ¬x = 0
hy : ¬y = 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⟯) (x.denom * y.denom) : K⟮X⟯)
have 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⟯)
Tactic: rw [map_mul, map_mul, ← div_mul_div_comm, num_div_denom, num_div_denom]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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⟯)
⊢ 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⟯)
have 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⟯)
Tactic: rw [map_mul, map_mul, ← div_mul_div_comm, num_div_denom, num_div_denom]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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⟯)
⊢ 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⟯)
have 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⟯)
Tactic: rw [map_mul, map_mul, ← div_mul_div_comm, num_div_denom, num_div_denom]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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⟯)
⊢ 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⟯)
have 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⟯)
Tactic: rw [map_mul, map_mul, ← div_mul_div_comm, num_div_denom, num_div_denom]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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⟯)
⊢ 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⟯)
have neg₄ : x * y = x * y
Tactic: rw [map_mul, map_mul, ← div_mul_div_comm, num_div_denom, num_div_denom]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
⊢ (x * y).denom ∣ x.denom * y.denom
have 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⟯)
Tactic: rw [denom_dvd (mul_ne_zero (denom_ne_zero x) (denom_ne_zero y))]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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⟯)
have 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⟯)
Tactic: refine ⟨x.num * y.num, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x y : 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⟯)
have 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⟯)
Tactic: rw [map_mul, map_mul, ← div_mul_div_comm, num_div_denom, num_div_denom]