English
norm_cast: the nat-cast of the sum of two PosNum equals the sum of their nat-casts: ((m+n : PosNum) : ℕ) = m + n.
Русский
norm_cast: натурализованный сумм PosNum даёт то же, что и сумма их нормированных значений: ((m+n : PosNum) : ℕ) = m+n.
LaTeX
$$$((m + n : \\mathrm{PosNum}) : \\mathbb{N}) = m + n$$$
Lean4
@[norm_cast]
theorem add_to_nat : ∀ m n, ((m + n : PosNum) : ℕ) = m + n
| 1, b => by rw [one_add b, succ_to_nat, add_comm, cast_one]
| a, 1 => by rw [add_one a, succ_to_nat, cast_one]
| bit0 a, bit0 b => (congr_arg (fun n ↦ n + n) (add_to_nat a b)).trans <| add_add_add_comm _ _ _ _
| bit0 a, bit1 b =>
(congr_arg (fun n ↦ (n + n) + 1) (add_to_nat a b)).trans <|
show (a + b + (a + b) + 1 : ℕ) = a + a + (b + b + 1) by simp [add_left_comm]
| bit1 a, bit0 b =>
(congr_arg (fun n ↦ (n + n) + 1) (add_to_nat a b)).trans <|
show (a + b + (a + b) + 1 : ℕ) = a + a + 1 + (b + b) by simp [add_comm, add_left_comm]
| bit1 a, bit1 b =>
show (succ (a + b) + succ (a + b) : ℕ) = a + a + 1 + (b + b + 1) by rw [succ_to_nat, add_to_nat a b];
simp [add_left_comm]
