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

State before:
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ a = c
Tactic:
apply Eq.trans
State after:
case h₁
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ a = ?b

case h₂
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ ?b = c

case b
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ α

State before:
case h₁
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ a = ?b

case h₂
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ ?b = c

case b
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ α
Tactic:
{ exact hab }
State after:
case h₂
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ b = c

State before:
case h₂
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ b = c
Tactic:
{ apply Eq.symm
  exact hcb }
State after:
no goals

State before:
case h₁
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ a = ?b
Tactic:
exact hab
State after:
no goals

State before:
case h₂
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ b = c
Tactic:
apply Eq.symm
State after:
case h₂.h
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ c = b

State before:
case h₂.h
α : Type
a b c : α
hab : a = b
hcb : c = b
⊢ c = b
Tactic:
exact hcb
State after:
no goals