Theorem: LoVe.Nat_coe_Int_add_eq_add_Nat_coe_Int (LoVe/Lectures/LoVe13_BasicMathematicalStructures_Demo.lean)

State before:
m n : ℕ
⊢ ↑m + ↑n = ↑(m + n)
Tactic:
norm_cast
State after:
no goals