English
If the denominators of q and r, viewed in α, are nonzero, then the sum q + r cast to α equals the sum q + r cast to α.
Русский
Если знаменатели q и r, рассмотренные в α, не равны нулю, то (q + r) в α равно сумме q и r в α.
LaTeX
$$$\forall q,r \in \mathbb{Q},\ (q.den : \alpha) \neq 0 \land (r.den : \alpha) \neq 0 \Rightarrow (q + r : \mathbb{Q}) = (q + r : \alpha).$$$
Lean4
@[norm_cast]
theorem cast_add_of_ne_zero {q r : ℚ} (hq : (q.den : α) ≠ 0) (hr : (r.den : α) ≠ 0) : (q + r : ℚ) = (q + r : α) :=
by
rw [add_def', cast_mkRat_of_ne_zero, cast_def, cast_def, mul_comm r.num,
(Nat.cast_commute _ _).div_add_div (Nat.commute_cast _ _) hq hr]
· push_cast
rfl
· push_cast
exact mul_ne_zero hq hr
