I'm working my way through the chapter 4 of the lean tutorial.
I'd like to be able to prove simple equalities, such as a = b → a + 1 = b + 1 without having to use the calc environment. In other words I'd like to explicitly construct the proof term of:
example (a b : nat) (H1 : a = b) : a + 1 = b + 1 := sorry
My best guess is that I need to use eq.subst and some relevant lemma about equality on natural numbers from the standard library, but I'm at loss. The closest lean example I can find is this:
example (A : Type) (a b : A) (P : A → Prop) (H1 : a = b) (H2 : P a) : P b :=
eq.subst H1 H2
While congr_arg is a good solution in general, this specific example can indeed be solved with eq.subst + higher-order unification (which congr_arg uses internally).
example (a b : nat) (H1 : a = b) : a + 1 = b + 1 :=
eq.subst H1 rfl