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

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

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

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

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

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

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