Theorem: LoVe.BackwardProofs.contrapositive (LoVe/Labs/Lab2Solution.lean)

State before:
a b : Prop
⊢ (a → b) → ¬b → ¬a
Tactic:
intro hab hnb ha
State after:
a b : Prop
hab : a → b
hnb : ¬b
ha : a
⊢ False

State before:
a b : Prop
hab : a → b
hnb : ¬b
ha : a
⊢ False
Tactic:
apply hnb
State after:
a b : Prop
hab : a → b
hnb : ¬b
ha : a
⊢ b

State before:
a b : Prop
hab : a → b
hnb : ¬b
ha : a
⊢ b
Tactic:
apply hab
State after:
a b : Prop
hab : a → b
hnb : ¬b
ha : a
⊢ a

State before:
a b : Prop
hab : a → b
hnb : ¬b
ha : a
⊢ a
Tactic:
apply ha
State after:
no goals