English
Let q and r be rationals. Then (q + r).num * q.den * r.den = (q.num * r.den + r.num * q.den) * (q + r).den.
Русский
Пусть q и r — рациональные числа. Тогда (q + r).num · q.den · r.den = (q.num · r.den + r.num · q.den) · (q + r).den.
LaTeX
$$(q + r).num * q.den * r.den = (q.num * r.den + r.num * q.den) * (q + r).den$$
Lean4
theorem add_num_den' (q r : ℚ) : (q + r).num * q.den * r.den = (q.num * r.den + r.num * q.den) * (q + r).den :=
by
let s := divInt (q.num * r.den + r.num * q.den) (q.den * r.den : ℤ)
have hs : (q.den * r.den : ℤ) ≠ 0 := Int.natCast_ne_zero_iff_pos.mpr (Nat.mul_pos q.pos r.pos)
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
rw [c_mul_num, mul_assoc, mul_comm]
nth_rw 1 [c_mul_den]
repeat rw [Int.mul_assoc]
apply mul_eq_mul_left_iff.2
rw [or_iff_not_imp_right]
intro
have h : _ = s := divInt_add_divInt q.num r.num (mod_cast q.den_ne_zero) (mod_cast r.den_ne_zero)
rw [num_divInt_den, num_divInt_den] at h
rw [h]
rw [mul_comm]
apply Rat.eq_iff_mul_eq_mul.mp
rw [← divInt_eq_div]
