awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q r : ℚ
s : ℚ := q.num * r.num /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hs : HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) ≠ 0
c : ℤ
c_mul_num :
  q.num * r.num =
    c * (HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num
c_mul_den :
  HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) =
    c * (↑(HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den : ℤ)
h_1 : ¬c = 0
h : q.num /. (↑q.den : ℤ) * (r.num /. (↑r.den : ℤ)) = s
⊢ q * r = s

Tactic:
rw [num_divInt_den, num_divInt_den] at h

Premises used: Rat.num_divInt_den
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q r : ℚ
s : ℚ := q.num * r.num /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hs : HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) ≠ 0
c : ℤ
c_mul_num :
  q.num * r.num =
    c * (HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num
c_mul_den :
  HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) =
    c * (↑(HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den : ℤ)
h_1 : ¬c = 0
h : q * r = s
rw :
  (↑(HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den : ℤ) * s.num =
    (HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num * (↑s.den : ℤ)
rw₁ :
  s.num * (↑(HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den : ℤ) =
    (HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num * (↑s.den : ℤ)
rw₂ : s = HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)
rw₃ rw₄ : s = q.num * r.num /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
⊢ (↑(HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).den : ℤ) *
      (q * r).num =
    (HDiv.hDiv (α := ℚ) (↑(q.num * r.num) : ℚ) (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)).num *
      (↑(q * r).den : ℤ)

Tactic:
rw [h, mul_comm, ← Rat.eq_iff_mul_eq_mul, ← divInt_eq_div]

Premises used: Rat.divInt_eq_div, mul_comm, Rat.eq_iff_mul_eq_mul
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q r : ℚ
s : ℚ := (q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
⊢ HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ) ≠ 0

Tactic:
have hs : (q.den * r.den : ℤ) ≠ 0 := Int.natCast_ne_zero_iff_pos.mpr (Nat.mul_pos q.pos r.pos)
-- Module: Mathlib.Data.Rat.Lemmas
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
obtain :
  ∀ (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 :
            ℤ)),
    (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 : ℤ)

Tactic:
obtain ⟨c, ⟨c_mul_num, c_mul_den⟩⟩ :=
    exists_eq_mul_div_num_and_eq_mul_div_den (q.num * r.den + r.num * q.den) hs

Premises used: Rat.num, HMul.hMul, Rat.exists_eq_mul_div_num_and_eq_mul_div_den, Rat.den, Nat.cast, HAdd.hAdd
-- Module: Mathlib.Data.Rat.Lemmas
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 :
        ℤ)
rw :
  HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.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 : ℤ)
⊢ (q + r).num * (↑q.den : ℤ) * (↑r.den : ℤ) = (q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) * (↑(q + r).den : ℤ)

Tactic:
rw [c_mul_num, mul_assoc, mul_comm]

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.Data.Rat.Lemmas
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 :
        ℤ)
nth_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 : ℤ)
⊢ HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.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:
nth_rw 1 [c_mul_den]
-- Module: Mathlib.Data.Rat.Lemmas
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 :
        ℤ)
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 : ℤ)
⊢ 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]

Premises used: Int.mul_assoc
-- Module: Mathlib.Data.Rat.Lemmas
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 :
        ℤ)
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 : ℤ))
⊢ 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]

Premises used: Int.mul_assoc
-- Module: Mathlib.Data.Rat.Lemmas
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 :
        ℤ)
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 : ℤ))
⊢ 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]

Premises used: Int.mul_assoc
-- Module: Mathlib.Data.Rat.Lemmas
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 :
        ℤ)
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
⊢ 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:
apply mul_eq_mul_left_iff.2

Premises used: Iff.mpr, mul_eq_mul_left_iff
-- Module: Mathlib.Data.Rat.Lemmas
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 :
        ℤ)
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 : ℤ)
⊢ (↑(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:
rw [or_iff_not_imp_right]

Premises used: Classical.or_iff_not_imp_right
-- Module: Mathlib.Data.Rat.Lemmas
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
⊢ 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)
-- Module: Mathlib.Data.Rat.Lemmas
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
⊢ q + r = s

Tactic:
rw [num_divInt_den, num_divInt_den] at h

Premises used: Rat.num_divInt_den
-- Module: Mathlib.Data.Rat.Lemmas
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
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 : ℤ)
⊢ (↑(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 [h]
-- Module: Mathlib.Data.Rat.Lemmas
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
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 : ℤ)
⊢ (↑(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 [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Data.Rat.Lemmas
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
apply :
  s =
    HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
      (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)
⊢ 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:
apply Rat.eq_iff_mul_eq_mul.mp

Premises used: Iff.mp, Rat.eq_iff_mul_eq_mul
-- Module: Mathlib.Data.Rat.Lemmas
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
rw rw₁ : s = (q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
⊢ s =
    HDiv.hDiv (α := ℚ) (↑(q.num * (↑r.den : ℤ) + r.num * (↑q.den : ℤ)) : ℚ)
      (↑(HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)) : ℚ)

Tactic:
rw [← divInt_eq_div]

Premises used: Rat.divInt_eq_div
-- Module: Mathlib.Data.Rat.Lemmas
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 : ℤ)
rw₅ rw₆ :
  (q.num * (↑(-r).den : ℤ) + (-r).num * (↑q.den : ℤ)) * (↑(q + -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 : ℤ)

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)]

Premises used: Rat.den_neg_eq_den, sub_eq_add_neg, Rat.num_neg_eq_neg_num, neg_mul, Rat.add_num_den', Neg.neg
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
rw : (-(q.num /. (↑q.den : ℤ)))⁻¹ = -(q.num /. (↑q.den : ℤ))⁻¹
⊢ (-q)⁻¹ = -q⁻¹

Tactic:
rw [← num_divInt_den q]

Premises used: Rat.num_divInt_den
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
⊢ (-(q.num /. (↑q.den : ℤ)))⁻¹ = -(q.num /. (↑q.den : ℤ))⁻¹

Tactic:
simp only [Rat.neg_divInt, Rat.inv_divInt, Rat.divInt_neg]

Premises used: Rat.inv_divInt, Rat.neg_divInt, Rat.divInt_neg
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a b : ℤ
hb0 : 0 < b
h : a.natAbs.Coprime b.natAbs
⊢ 0 ≤ b

Tactic:
hb0.le

Premises used: LT.lt.le
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a b : ℤ
hb0 : 0 < b
h : a.natAbs.Coprime b.natAbs
lift :
  ∀ (b : ℕ) (hb0 : LT.lt (α := ℤ) 0 (↑b : ℤ)) (h : a.natAbs.Coprime (Int.natAbs (↑b : ℤ))),
    (HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑(↑b : ℤ) : ℚ)).num = a
⊢ (HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ)).num = a

Tactic:
lift b to ℕ using hb0.le

Premises used: LT.lt.le
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a : ℤ
b : ℕ
hb0 : LT.lt (α := ℤ) 0 (↑b : ℤ)
h : a.natAbs.Coprime (Int.natAbs (↑b : ℤ))
⊢ 0 < b

Tactic:
simp only [Int.natAbs_natCast, Int.natCast_pos] at h hb0

Premises used: Int.natAbs_natCast, Int.natCast_pos
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a : ℤ
b : ℕ
h : a.natAbs.Coprime b
hb0 : 0 < b
rw : (a /. (↑b : ℤ)).num = a
rw₁ rw₂ : { num := a, den := b, den_nz := ⋯, reduced := h : ℚ }.num = a
⊢ (HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑(↑b : ℤ) : ℚ)).num = a

Tactic:
rw [← Rat.divInt_eq_div, ← mk_eq_divInt (nz := hb0.ne') (c := h)]

Premises used: Rat.mk_eq_divInt, Rat.divInt_eq_div
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a b : ℤ
hb0 : 0 < b
h : a.natAbs.Coprime b.natAbs
lift :
  ∀ (b : ℕ) (hb0 : LT.lt (α := ℤ) 0 (↑b : ℤ)) (h : a.natAbs.Coprime (Int.natAbs (↑b : ℤ))),
    Eq (α := ℤ) (↑(HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑(↑b : ℤ) : ℚ)).den : ℤ) (↑b : ℤ)
⊢ (↑(HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ)).den : ℤ) = b

Tactic:
lift b to ℕ using hb0.le

Premises used: LT.lt.le
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a : ℤ
b : ℕ
h : a.natAbs.Coprime b
hb0 : 0 < b
rw : Eq (α := ℤ) (↑(a /. (↑b : ℤ)).den : ℤ) (↑b : ℤ)
rw₁ rw₂ : Eq (α := ℤ) (↑{ num := a, den := b, den_nz := ⋯, reduced := h }.den : ℤ) (↑b : ℤ)
⊢ Eq (α := ℤ) (↑(HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑(↑b : ℤ) : ℚ)).den : ℤ) (↑b : ℤ)

Tactic:
rw [← Rat.divInt_eq_div, ← mk_eq_divInt (nz := hb0.ne') (c := h)]

Premises used: Rat.mk_eq_divInt, Rat.divInt_eq_div
-- Module: Mathlib.Data.Rat.Lemmas
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
right : b = d
⊢ a = c ∧ b = d

Tactic:
apply And.intro

Premises used: And.intro