Theorem: LoVe.BTree.add_left_neg_counterexample (LoVe/Labs/Lab7Solution.lean)

State before:
⊢ ∃ x, ∀ (y : BTree ℕ), graft y x ≠ empty
Tactic:
apply Exists.intro (BTree.node 0 BTree.empty BTree.empty)
State after:
⊢ ∀ (y : BTree ℕ), graft y (node 0 empty empty) ≠ empty

State before:
⊢ ∀ (y : BTree ℕ), graft y (node 0 empty empty) ≠ empty
Tactic:
intro y hy
State after:
y : BTree ℕ
hy : graft y (node 0 empty empty) = empty
⊢ False

State before:
y : BTree ℕ
hy : graft y (node 0 empty empty) = empty
⊢ False
Tactic:
cases y with
| empty      => cases hy
| node a l r => cases' hy
State after:
no goals

State before:
case empty
hy : graft empty (node 0 empty empty) = empty
⊢ False
Tactic:
cases hy
State after:
no goals

State before:
case node
a : ℕ
l r : BTree ℕ
hy : graft (node a l r) (node 0 empty empty) = empty
⊢ False
Tactic:
cases' hy
State after:
no goals