α : Type u_1
inst✝ : AddMonoidWithOne α
⊢ ↑(1 + 1) = 2
α : Type u_1
inst✝ : AddMonoidWithOne α
⊢ 1 + 1 = 2
rw [←Nat.cast_one, ←Nat.cast_add]
case h
α : Type u_1
inst✝ : AddMonoidWithOne α
⊢ 1 + 1 = 2
α : Type u_1
inst✝ : AddMonoidWithOne α
⊢ ↑(1 + 1) = 2
apply congrArg
no goals
case h
α : Type u_1
inst✝ : AddMonoidWithOne α
⊢ 1 + 1 = 2
decide