a b c q r : ℚ
hq' : ↑q.den ≠ 0
⊢ q * r = q.num * r.num /. ↑(q.den * r.den)
a b c q r : ℚ
⊢ q * r = q.num * r.num /. ↑(q.den * r.den)
have hq' : (↑q.den : ℤ) ≠ 0 := by have := den_nz q; simpa
a b c q r : ℚ
hq' : ↑q.den ≠ 0
hr' : ↑r.den ≠ 0
⊢ q * r = q.num * r.num /. ↑(q.den * r.den)
a b c q r : ℚ
hq' : ↑q.den ≠ 0
⊢ q * r = q.num * r.num /. ↑(q.den * r.den)
have hr' : (↑r.den : ℤ) ≠ 0 := by have := den_nz r; simpa
a b c q r : ℚ
hq' : ↑q.den ≠ 0
hr' : ↑r.den ≠ 0
⊢ q.num /. ↑q.den * (r.num /. ↑r.den) = q.num * r.num /. ↑(q.den * r.den)
a b c q r : ℚ
hq' : ↑q.den ≠ 0
hr' : ↑r.den ≠ 0
⊢ q * r = q.num * r.num /. ↑(q.den * r.den)
suffices q.num /. ↑q.den * (r.num /. ↑r.den) = q.num * r.num /. ↑(q.den * r.den) by
  simpa [num_den] using this
no goals
a b c q r : ℚ
hq' : ↑q.den ≠ 0
hr' : ↑r.den ≠ 0
⊢ q.num /. ↑q.den * (r.num /. ↑r.den) = q.num * r.num /. ↑(q.den * r.den)
simp [mul_def' hq' hr']
a b c q r : ℚ
this : q.den ≠ 0
⊢ ↑q.den ≠ 0
a b c q r : ℚ
⊢ ↑q.den ≠ 0
have := den_nz q
no goals
a b c q r : ℚ
this : q.den ≠ 0
⊢ ↑q.den ≠ 0
simpa
a b c q r : ℚ
hq' : ↑q.den ≠ 0
this : r.den ≠ 0
⊢ ↑r.den ≠ 0
a b c q r : ℚ
hq' : ↑q.den ≠ 0
⊢ ↑r.den ≠ 0
have := den_nz r
no goals
a b c q r : ℚ
hq' : ↑q.den ≠ 0
this : r.den ≠ 0
⊢ ↑r.den ≠ 0
simpa
no goals
a b c q r : ℚ
hq' : ↑q.den ≠ 0
hr' : ↑r.den ≠ 0
this : q.num /. ↑q.den * (r.num /. ↑r.den) = q.num * r.num /. ↑(q.den * r.den)
⊢ q * r = q.num * r.num /. ↑(q.den * r.den)
simpa [num_den] using this