English
Let q1 and q2 be rationals. Then (q1 * q2).num * q1.den * q2.den = q1.num * q2.num * (q1 * q2).den.
Русский
Пусть q1 и q2 — рациональные числа. Тогда (q1 q2).num · q1.den · q2.den = q1.num · q2.num · (q1 q2).den.
LaTeX
$$$(q_1 * q_2).num * q_1.den * q_2.den = q_1.num * q_2.num * (q_1 * q_2).den$$
Lean4
theorem mul_num_den' (q r : ℚ) : (q * r).num * q.den * r.den = q.num * r.num * (q * r).den :=
by
let s := q.num * r.num /. (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.num) hs
rw [c_mul_num, mul_assoc, mul_comm]
nth_rw 1 [c_mul_den]
rw [Int.mul_assoc, Int.mul_assoc, mul_eq_mul_left_iff, or_iff_not_imp_right]
intro
have h : _ = s := divInt_mul_divInt q.num r.num
rw [num_divInt_den, num_divInt_den] at h
rw [h, mul_comm, ← Rat.eq_iff_mul_eq_mul, ← divInt_eq_div]
