-- Mathlib/Data/Rat/Lemmas.lean
theorem add_num_den' (q r : ℚ) :
    (q + r).num * q.den * r.den = (q.num * r.den + r.num * q.den) * (q + r).den

Proof state:
case intro.intro
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
h : q.num /. ↑q.den + r.num /. ↑r.den = s
⊢ ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num =
    (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den

Tactic:
rw [num_divInt_den, num_divInt_den] at h

Result:
case intro.intro
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
h : q + r = s
⊢ ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num =
    (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den

Proof state:
case intro.intro
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
h : q + r = s
⊢ s = ↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)

Tactic:
rw [← divInt_eq_div]

Result:
no goals

Proof state:
case intro.intro
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num =
      (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den ∨
    c = 0

Tactic:
rw [or_iff_not_imp_right]

Result:
case intro.intro
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ ¬c = 0 →
    ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num =
      (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den

Proof state:
case intro.intro
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
h : q + r = s
⊢ ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num =
    (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den

Tactic:
rw [h]

Result:
case intro.intro
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
h : q + r = s
⊢ ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * s.num =
    (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑s.den

Proof state:
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
⊢ (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

Result:
case intro.intro
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ (q + r).num * ↑q.den * ↑r.den = (q.num * ↑r.den + r.num * ↑q.den) * ↑(q + r).den

Proof state:
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
⊢ (q + r).num * ↑q.den * ↑r.den = (q.num * ↑r.den + r.num * ↑q.den) * ↑(q + r).den

Tactic:
have hs : (q.den * r.den : ℤ) ≠ 0 := Int.natCast_ne_zero_iff_pos.mpr (Nat.mul_pos q.pos r.pos)

Result:
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
⊢ (q + r).num * ↑q.den * ↑r.den = (q.num * ↑r.den + r.num * ↑q.den) * ↑(q + r).den

Proof state:
case intro.intro
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
h : q + r = s
⊢ ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * s.num =
    (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑s.den

Tactic:
rw [mul_comm]

Result:
case intro.intro
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
h : q + r = s
⊢ s.num * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den =
    (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑s.den

Proof state:
case intro.intro
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ c * (↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num) =
    c * ((↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den)

Tactic:
apply mul_eq_mul_left_iff.2

Result:
case intro.intro
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num =
      (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den ∨
    c = 0