# how to prove 2+2+a=4+a in lean4?

It should be simple but dig it for a while and still not successful. theorem example (a : R) : 2 + 2 + a = 4 + a := ...

can someone help to figure out how to do next? many thanks

• I recommend learning a bit about MWEs. There is a good website on MWEs in Lean. In particular, use triple backquotes for code and provide all imports (say for the real numbers in your example). Oct 27, 2023 at 1:12
• thanks. that is fine Oct 27, 2023 at 1:19

norm_num is a good tactic for this sort of stuff:

import Mathlib.Tactic.NormNum
import Mathlib.Data.Real.Basic

example (a : ℝ) : 2 + 2 + a = 4 + a := by norm_num


(I couldn't find the tactic documentation for Lean 4, so I gave you the documentation for norm_num in Lean 3.). But in short, norm_num normalizes both sides of this equation. It works in many places that rfl can't work.

• thanks. it works. Oct 27, 2023 at 1:18
• What does norm_num do? Oct 29, 2023 at 3:49
• @AgnishomChattopadhyay I believe it uses various rewrite rules to simplify the expression efficiently. In particular, I think it uses binary to represent integers (even integer real numbers like in this example). I know it’s also extensible and you can mark lemmas to be used in norm_num. This allows you to use norm_num on custom functions or even custom types. I think for more details it’s best to ask a question here or on the lean Zulip, since I don’t know. Oct 29, 2023 at 4:35