Theorem: T2 (TheoremProvingLean/quantifiers_and_equality.lean)

State before:
a b c d e : Nat
h1 : a = b
h2 : b = c + 1
h3 : c = d
h4 : e = 1 + d
⊢ c + 1 = d + 1
Tactic:
rw [h3]
State after:
no goals

State before:
a b c d e : Nat
h1 : a = b
h2 : b = c + 1
h3 : c = d
h4 : e = 1 + d
⊢ d + 1 = e
Tactic:
rw [Nat.add_comm, h4]
State after:
no goals