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