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