Theorem: eq_rel_trans (Instructor/Exams/Final/final_part1_key.lean)

State before:
α : Type
a b c : α
ab : a = b
bc : b = c
⊢ a = c
Tactic:
rw [ab]
State after:
α : Type
a b c : α
ab : a = b
bc : b = c
⊢ b = c

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