Theorem: LoVe.BackwardProofs.Eq_trans_symm_rw (LoVe/Lectures/LoVe03_BackwardProofs_Demo.lean)

State before:
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ a = c
Tactic:
rw [hab]
State after:
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ b = c

State before:
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ b = c
Tactic:
rw [hcb]
State after:
no goals