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

State before:
α : Type
t u v : BTree α
⊢ graft (graft t u) v = graft t (graft u v)
Tactic:
induction t with
| empty                => rfl
| node a l r ih_l ih_r => simp [BTree.graft, ih_l, ih_r]
State after:
no goals

State before:
case empty
α : Type
u v : BTree α
⊢ graft (graft empty u) v = graft empty (graft u v)
Tactic:
rfl
State after:
no goals

State before:
case node
α : Type
u v : BTree α
a : α
l r : BTree α
ih_l : graft (graft l u) v = graft l (graft u v)
ih_r : graft (graft r u) v = graft r (graft u v)
⊢ graft (graft (node a l r) u) v = graft (node a l r) (graft u v)
Tactic:
simp [BTree.graft, ih_l, ih_r]
State after:
no goals