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

State before:
a b c : Prop
⊢ (a → b → c) → b → a → c
Tactic:
intro hg hb ha
State after:
a b c : Prop
hg : a → b → c
hb : b
ha : a
⊢ c

State before:
a b c : Prop
hg : a → b → c
hb : b
ha : a
⊢ c
Tactic:
apply hg
State after:
case a
a b c : Prop
hg : a → b → c
hb : b
ha : a
⊢ a

case a
a b c : Prop
hg : a → b → c
hb : b
ha : a
⊢ b

State before:
case a
a b c : Prop
hg : a → b → c
hb : b
ha : a
⊢ a

case a
a b c : Prop
hg : a → b → c
hb : b
ha : a
⊢ b
Tactic:
exact ha
State after:
case a
a b c : Prop
hg : a → b → c
hb : b
ha : a
⊢ b

State before:
case a
a b c : Prop
hg : a → b → c
hb : b
ha : a
⊢ b
Tactic:
exact hb
State after:
no goals