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
Proof Assistants Stack Exchange is a question and answer site for mathematicians and computer scientists who develop and use proof assistants. It only takes a minute to sign up.Sign up to join this community
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.