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

State before:
m n : ℕ
h : ↑m = ↑n
⊢ m = n
Tactic:
norm_cast at h
State after:
no goals