awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q r : ℚ
s : ℚ := (q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hs : HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) ≠ 0
c : ℤ
c_mul_num :
  q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ) =
    c *
      (HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
          (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num
c_mul_den :
  HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) =
    c *
      (↑(HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
              (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den :
        ℤ)
⊢ c *
        (↑(HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
                (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den :
          ℤ) *
      (q + r).num =
    c *
        (HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
            (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num *
      (↑(q + r).den : ℤ)
have rw : c *
    ((↑(HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
              (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den :
        ℤ) *
      (q + r).num) =
  c *
      (HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
          (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num *
    (↑(q + r).den : ℤ)
Tactic: rw [Int.mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q r : ℚ
s : ℚ := (q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hs : HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) ≠ 0
c : ℤ
c_mul_num :
  q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ) =
    c *
      (HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
          (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num
c_mul_den :
  HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) =
    c *
      (↑(HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
              (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den :
        ℤ)
⊢ c *
      ((↑(HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
                (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den :
          ℤ) *
        (q + r).num) =
    c *
        (HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
            (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num *
      (↑(q + r).den : ℤ)
have rw : c *
    ((↑(HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
              (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den :
        ℤ) *
      (q + r).num) =
  c *
    ((HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
          (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num *
      (↑(q + r).den : ℤ))
Tactic: rw [Int.mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q r : ℚ
s : ℚ := (q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hs : HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) ≠ 0
c : ℤ
c_mul_num :
  q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ) =
    c *
      (HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
          (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num
c_mul_den :
  HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) =
    c *
      (↑(HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
              (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den :
        ℤ)
⊢ c *
        (↑(HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
                (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den :
          ℤ) *
      (q + r).num =
    c *
        (HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
            (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num *
      (↑(q + r).den : ℤ)
have repeat : c *
    ((↑(HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
              (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den :
        ℤ) *
      (q + r).num) =
  c *
    ((HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
          (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num *
      (↑(q + r).den : ℤ))
Tactic: repeat rw [Int.mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q r : ℚ
s : ℚ := (q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hs : HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) ≠ 0
c : ℤ
c_mul_num :
  q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ) =
    c *
      (HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
          (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num
c_mul_den :
  HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) =
    c *
      (↑(HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
              (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den :
        ℤ)
⊢ c *
      ((↑(HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
                (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den :
          ℤ) *
        (q + r).num) =
    c *
      ((HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
            (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num *
        (↑(q + r).den : ℤ))
have apply : (↑(HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
              (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den :
        ℤ) *
      (q + r).num =
    (HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
          (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num *
      (↑(q + r).den : ℤ) ∨
  c = 0
Tactic: apply mul_eq_mul_left_iff.2
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q r : ℚ
s : ℚ := (q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hs : HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) ≠ 0
c : ℤ
c_mul_num :
  q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ) =
    c *
      (HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
          (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num
c_mul_den :
  HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) =
    c *
      (↑(HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
              (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den :
        ℤ)
⊢ (↑(HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
                (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den :
          ℤ) *
        (q + r).num =
      (HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
            (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num *
        (↑(q + r).den : ℤ) ∨
    c = 0
have rw : ¬c = 0 →
  (↑(HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
              (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den :
        ℤ) *
      (q + r).num =
    (HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
          (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num *
      (↑(q + r).den : ℤ)
Tactic: rw [or_iff_not_imp_right]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (hypothesis)
Goal:
q r : ℚ
s : ℚ := (q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hs : HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) ≠ 0
c : ℤ
c_mul_num :
  q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ) =
    c *
      (HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
          (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num
c_mul_den :
  HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) =
    c *
      (↑(HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
              (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den :
        ℤ)
h : ¬c = 0
⊢ (↑(HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
              (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den :
        ℤ) *
      (q + r).num =
    (HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
          (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num *
      (↑(q + r).den : ℤ)
have h : q.num /. (↑q.den : ℤ) + r.num /. (↑r.den : ℤ) = s
Tactic: have h : _ = s := divInt_add_divInt q.num r.num (mod_cast q.den_ne_zero) (mod_cast r.den_ne_zero)
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (hypothesis)
Goal:
q r : ℚ
s : ℚ := (q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hs : HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) ≠ 0
c : ℤ
c_mul_num :
  q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ) =
    c *
      (HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
          (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num
c_mul_den :
  HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) =
    c *
      (↑(HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
              (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den :
        ℤ)
h_1 : ¬c = 0
h : q.num /. (↑q.den : ℤ) + r.num /. (↑r.den : ℤ) = s
⊢ (↑(HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
              (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den :
        ℤ) *
      (q + r).num =
    (HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
          (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num *
      (↑(q + r).den : ℤ)
have h₁ : q + r = s
Tactic: rw [num_divInt_den, num_divInt_den] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q r : ℚ
s : ℚ := (q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hs : HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) ≠ 0
c : ℤ
c_mul_num :
  q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ) =
    c *
      (HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
          (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num
c_mul_den :
  HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) =
    c *
      (↑(HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
              (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den :
        ℤ)
h_1 : ¬c = 0
h : q + r = s
⊢ (↑(HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
              (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den :
        ℤ) *
      (q + r).num =
    (HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
          (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num *
      (↑(q + r).den : ℤ)
have rw : (↑(HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
            (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den :
      ℤ) *
    s.num =
  (HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
        (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num *
    (↑s.den : ℤ)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q r : ℚ
s : ℚ := (q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hs : HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) ≠ 0
c : ℤ
c_mul_num :
  q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ) =
    c *
      (HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
          (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num
c_mul_den :
  HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) =
    c *
      (↑(HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
              (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den :
        ℤ)
h_1 : ¬c = 0
h : q + r = s
⊢ (↑(HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
              (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den :
        ℤ) *
      s.num =
    (HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
          (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num *
      (↑s.den : ℤ)
have rw : s.num *
    (↑(HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
            (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den :
      ℤ) =
  (HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
        (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num *
    (↑s.den : ℤ)
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q r : ℚ
s : ℚ := (q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hs : HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) ≠ 0
c : ℤ
c_mul_num :
  q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ) =
    c *
      (HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
          (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num
c_mul_den :
  HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) =
    c *
      (↑(HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
              (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den :
        ℤ)
h_1 : ¬c = 0
h : q + r = s
⊢ s.num *
      (↑(HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
              (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den :
        ℤ) =
    (HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
          (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num *
      (↑s.den : ℤ)
have apply : s =
  HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
    (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)
Tactic: apply Rat.eq_iff_mul_eq_mul.mp
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q r : ℚ
s : ℚ := (q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hs : HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) ≠ 0
c : ℤ
c_mul_num :
  q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ) =
    c *
      (HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
          (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num
c_mul_den :
  HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) =
    c *
      (↑(HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
              (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den :
        ℤ)
h_1 : ¬c = 0
h : q + r = s
⊢ s =
    HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
      (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)
have rw : s = (q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
Tactic: rw [← divInt_eq_div]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q r : ℚ
⊢ (q - r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = (q.num * (↑r.den : ℤ) - r.num * (↑q.den : ℤ)) * (↑(q - r).den : ℤ)
have rw : (q + -r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = (q.num * (↑r.den : ℤ) - r.num * (↑q.den : ℤ)) * (↑(q + -r).den : ℤ)
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, ← neg_mul, ← num_neg_eq_neg_num, ← den_neg_eq_den r,
    add_num_den' q (-r)]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q r : ℚ
rw : (q + -r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = (q.num * (↑r.den : ℤ) - r.num * (↑q.den : ℤ)) * (↑(q + -r).den : ℤ)
⊢ (q - r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = (q.num * (↑r.den : ℤ) - r.num * (↑q.den : ℤ)) * (↑(q - r).den : ℤ)
have rw₁ : (q + -r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = (q.num * (↑r.den : ℤ) + -(r.num * (↑q.den : ℤ))) * (↑(q + -r).den : ℤ)
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, ← neg_mul, ← num_neg_eq_neg_num, ← den_neg_eq_den r,
    add_num_den' q (-r)]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q r : ℚ
rw : (q + -r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = (q.num * (↑r.den : ℤ) - r.num * (↑q.den : ℤ)) * (↑(q + -r).den : ℤ)
rw₁ :
  (q + -r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = (q.num * (↑r.den : ℤ) + -(r.num * (↑q.den : ℤ))) * (↑(q + -r).den : ℤ)
⊢ (q - r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = (q.num * (↑r.den : ℤ) - r.num * (↑q.den : ℤ)) * (↑(q - r).den : ℤ)
have rw₂ : (q + -r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = (q.num * (↑r.den : ℤ) + -r.num * (↑q.den : ℤ)) * (↑(q + -r).den : ℤ)
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, ← neg_mul, ← num_neg_eq_neg_num, ← den_neg_eq_den r,
    add_num_den' q (-r)]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q r : ℚ
rw : (q + -r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = (q.num * (↑r.den : ℤ) - r.num * (↑q.den : ℤ)) * (↑(q + -r).den : ℤ)
rw₁ :
  (q + -r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = (q.num * (↑r.den : ℤ) + -(r.num * (↑q.den : ℤ))) * (↑(q + -r).den : ℤ)
rw₂ : (q + -r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = (q.num * (↑r.den : ℤ) + -r.num * (↑q.den : ℤ)) * (↑(q + -r).den : ℤ)
⊢ (q - r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = (q.num * (↑r.den : ℤ) - r.num * (↑q.den : ℤ)) * (↑(q - r).den : ℤ)
have rw₃ : (q + -r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = (q.num * (↑r.den : ℤ) + (-r).num * (↑q.den : ℤ)) * (↑(q + -r).den : ℤ)
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, ← neg_mul, ← num_neg_eq_neg_num, ← den_neg_eq_den r,
    add_num_den' q (-r)]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q r : ℚ
rw : (q + -r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = (q.num * (↑r.den : ℤ) - r.num * (↑q.den : ℤ)) * (↑(q + -r).den : ℤ)
rw₁ :
  (q + -r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = (q.num * (↑r.den : ℤ) + -(r.num * (↑q.den : ℤ))) * (↑(q + -r).den : ℤ)
rw₂ : (q + -r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = (q.num * (↑r.den : ℤ) + -r.num * (↑q.den : ℤ)) * (↑(q + -r).den : ℤ)
rw₃ :
  (q + -r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = (q.num * (↑r.den : ℤ) + (-r).num * (↑q.den : ℤ)) * (↑(q + -r).den : ℤ)
⊢ (q - r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = (q.num * (↑r.den : ℤ) - r.num * (↑q.den : ℤ)) * (↑(q - r).den : ℤ)
have rw₄ : (q + -r).num * (↑q.den : ℤ) * (↑(-r).den : ℤ) =
  (q.num * (↑(-r).den : ℤ) + (-r).num * (↑q.den : ℤ)) * (↑(q + -r).den : ℤ)
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, ← neg_mul, ← num_neg_eq_neg_num, ← den_neg_eq_den r,
    add_num_den' q (-r)]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q r : ℚ
rw : (q + -r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = (q.num * (↑r.den : ℤ) - r.num * (↑q.den : ℤ)) * (↑(q + -r).den : ℤ)
rw₁ :
  (q + -r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = (q.num * (↑r.den : ℤ) + -(r.num * (↑q.den : ℤ))) * (↑(q + -r).den : ℤ)
rw₂ : (q + -r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = (q.num * (↑r.den : ℤ) + -r.num * (↑q.den : ℤ)) * (↑(q + -r).den : ℤ)
rw₃ :
  (q + -r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = (q.num * (↑r.den : ℤ) + (-r).num * (↑q.den : ℤ)) * (↑(q + -r).den : ℤ)
rw₄ :
  (q + -r).num * (↑q.den : ℤ) * (↑(-r).den : ℤ) =
    (q.num * (↑(-r).den : ℤ) + (-r).num * (↑q.den : ℤ)) * (↑(q + -r).den : ℤ)
⊢ (q - r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = (q.num * (↑r.den : ℤ) - r.num * (↑q.den : ℤ)) * (↑(q - r).den : ℤ)
have rw₅ : (q.num * (↑(-r).den : ℤ) + (-r).num * (↑q.den : ℤ)) * (↑(q + -r).den : ℤ) =
  (q.num * (↑(-r).den : ℤ) + (-r).num * (↑q.den : ℤ)) * (↑(q + -r).den : ℤ)
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, ← neg_mul, ← num_neg_eq_neg_num, ← den_neg_eq_den r,
    add_num_den' q (-r)]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
q : ℚ
⊢ (-q)⁻¹ = -q⁻¹
have rw : (-(q.num /. (↑q.den : ℤ)))⁻¹ = -(q.num /. (↑q.den : ℤ))⁻¹
Tactic: rw [← num_divInt_den q]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
a b : ℤ
hb0 : 0 < b
h : a.natAbs.Coprime b.natAbs
⊢ (HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ)).num = a
have lift : ∀ (b : ℕ) (hb0 : LT.lt (α := ℤ) 0 (↑b : ℤ)) (h : a.natAbs.Coprime (Int.natAbs (↑b : ℤ))),
  (HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑(↑b : ℤ) : ℚ)).num = a
Tactic: lift b to ℕ using hb0.le
Cleared hypotheses: b, hb0, h
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (hypothesis)
Goal:
a : ℤ
b : ℕ
hb0 : LT.lt (α := ℤ) 0 (↑b : ℤ)
h : a.natAbs.Coprime (Int.natAbs (↑b : ℤ))
⊢ (HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑(↑b : ℤ) : ℚ)).num = a
have hb0₁ : 0 < b
Tactic: simp only [Int.natAbs_natCast, Int.natCast_pos] at h hb0
Cleared hypotheses: hb0
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
a : ℤ
b : ℕ
h : a.natAbs.Coprime b
hb0 : 0 < b
⊢ (HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑(↑b : ℤ) : ℚ)).num = a
have rw : (a /. (↑b : ℤ)).num = a
Tactic: rw [← Rat.divInt_eq_div, ← mk_eq_divInt (nz := hb0.ne') (c := h)]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
a : ℤ
b : ℕ
h : a.natAbs.Coprime b
hb0 : 0 < b
rw : (a /. (↑b : ℤ)).num = a
⊢ (HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑(↑b : ℤ) : ℚ)).num = a
have rw₁ : { num := a, den := b, den_nz := sorry, reduced := h : ℚ }.num = a
Tactic: rw [← Rat.divInt_eq_div, ← mk_eq_divInt (nz := hb0.ne') (c := h)]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
a b : ℤ
hb0 : 0 < b
h : a.natAbs.Coprime b.natAbs
⊢ (↑(HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ)).den : ℤ) = b
have lift : ∀ (b : ℕ) (hb0 : LT.lt (α := ℤ) 0 (↑b : ℤ)) (h : a.natAbs.Coprime (Int.natAbs (↑b : ℤ))),
  Eq (α := ℤ) (↑(HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑(↑b : ℤ) : ℚ)).den : ℤ) (↑b : ℤ)
Tactic: lift b to ℕ using hb0.le
Cleared hypotheses: b, hb0, h
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (hypothesis)
Goal:
a : ℤ
b : ℕ
hb0 : LT.lt (α := ℤ) 0 (↑b : ℤ)
h : a.natAbs.Coprime (Int.natAbs (↑b : ℤ))
⊢ Eq (α := ℤ) (↑(HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑(↑b : ℤ) : ℚ)).den : ℤ) (↑b : ℤ)
have hb0₁ : 0 < b
Tactic: simp only [Int.natAbs_natCast, Int.natCast_pos] at h hb0
Cleared hypotheses: hb0
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
a : ℤ
b : ℕ
h : a.natAbs.Coprime b
hb0 : 0 < b
⊢ Eq (α := ℤ) (↑(HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑(↑b : ℤ) : ℚ)).den : ℤ) (↑b : ℤ)
have rw : Eq (α := ℤ) (↑(a /. (↑b : ℤ)).den : ℤ) (↑b : ℤ)
Tactic: rw [← Rat.divInt_eq_div, ← mk_eq_divInt (nz := hb0.ne') (c := h)]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
a : ℤ
b : ℕ
h : a.natAbs.Coprime b
hb0 : 0 < b
rw : Eq (α := ℤ) (↑(a /. (↑b : ℤ)).den : ℤ) (↑b : ℤ)
⊢ Eq (α := ℤ) (↑(HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑(↑b : ℤ) : ℚ)).den : ℤ) (↑b : ℤ)
have rw₁ : Eq (α := ℤ) (↑{ num := a, den := b, den_nz := sorry, reduced := h }.den : ℤ) (↑b : ℤ)
Tactic: rw [← Rat.divInt_eq_div, ← mk_eq_divInt (nz := hb0.ne') (c := h)]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : a.natAbs.Coprime b.natAbs
h2 : c.natAbs.Coprime d.natAbs
h : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = HDiv.hDiv (α := ℚ) (↑c : ℚ) (↑d : ℚ)
⊢ a = c ∧ b = d
have left : a = c
Tactic: apply And.intro
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : a.natAbs.Coprime b.natAbs
h2 : c.natAbs.Coprime d.natAbs
h : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = HDiv.hDiv (α := ℚ) (↑c : ℚ) (↑d : ℚ)
left : a = c
⊢ a = c ∧ b = d
have right : b = d
Tactic: apply And.intro
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : a.natAbs.Coprime b.natAbs
h2 : c.natAbs.Coprime d.natAbs
h : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = HDiv.hDiv (α := ℚ) (↑c : ℚ) (↑d : ℚ)
⊢ a = c
have left : (HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ)).num = c
Tactic: rw [← num_div_eq_of_coprime hb0 h1, h, num_div_eq_of_coprime hd0 h2]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : a.natAbs.Coprime b.natAbs
h2 : c.natAbs.Coprime d.natAbs
h : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = HDiv.hDiv (α := ℚ) (↑c : ℚ) (↑d : ℚ)
left : (HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ)).num = c
⊢ a = c
have left₁ : (HDiv.hDiv (α := ℚ) (↑c : ℚ) (↑d : ℚ)).num = c
Tactic: rw [← num_div_eq_of_coprime hb0 h1, h, num_div_eq_of_coprime hd0 h2]
-- Lean 4 proof step from Mathlib.Data.Rat.Lemmas (goal)
Goal:
a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : a.natAbs.Coprime b.natAbs
h2 : c.natAbs.Coprime d.natAbs
h : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = HDiv.hDiv (α := ℚ) (↑c : ℚ) (↑d : ℚ)
left : (HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ)).num = c
left₁ : (HDiv.hDiv (α := ℚ) (↑c : ℚ) (↑d : ℚ)).num = c
⊢ a = c
have left₂ : c = c
Tactic: rw [← num_div_eq_of_coprime hb0 h1, h, num_div_eq_of_coprime hd0 h2]