Theorem: T3 (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
⊢ a = e
Tactic:
simp [h1, h2, h3, h4, Nat.add_comm]
State after:
no goals