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

State before:
a b c : Prop
ha : a
hb : b
hab : a → b
hbc : b → c
⊢ c
Tactic:
clear ha hab a
State after:
b c : Prop
hb : b
hbc : b → c
⊢ c

State before:
b c : Prop
hb : b
hbc : b → c
⊢ c
Tactic:
apply hbc
State after:
b c : Prop
hb : b
hbc : b → c
⊢ b

State before:
b c : Prop
hb : b
hbc : b → c
⊢ b
Tactic:
clear hbc c
State after:
b : Prop
hb : b
⊢ b

State before:
b : Prop
hb : b
⊢ b
Tactic:
rename b => h
State after:
b : Prop
h : b
⊢ b

State before:
b : Prop
h : b
⊢ b
Tactic:
exact h
State after:
no goals