Theorem: Cpdt.Chapter3.NatTree.splice_size (Cpdt/Chapter3/Nested.lean)

State before:
⊢ ∀ (t1 t2 : NatTree), size (splice t1 t2) = size t1 + size t2
Tactic:
intro t1
State after:
t1 : NatTree
⊢ ∀ (t2 : NatTree), size (splice t1 t2) = size t1 + size t2

State before:
t1 : NatTree
⊢ ∀ (t2 : NatTree), size (splice t1 t2) = size t1 + size t2
Tactic:
induction t1 using nat_tree_ind with
| node_case x ts ih =>
  cases ts <;> simp_all
  simp_arith
State after:
no goals

State before:
case node_case
x : Nat
ts : List NatTree
ih : all (fun t1 => ∀ (t2 : NatTree), size (splice t1 t2) = size t1 + size t2) ts
⊢ ∀ (t2 : NatTree), size (splice (node x ts) t2) = size (node x ts) + size t2
Tactic:
cases ts <;> simp_all
State after:
case node_case.cons
x : Nat
head✝ : NatTree
tail✝ : List NatTree
ih :
  (∀ (t2 : NatTree), size (splice head✝ t2) = size head✝ + size t2) ∧
    all (fun t1 => ∀ (t2 : NatTree), size (splice t1 t2) = size t1 + size t2) tail✝
⊢ ∀ (t2 : NatTree), 1 + (size head✝ + size t2 + nodeListSize tail✝) = 1 + (size head✝ + nodeListSize tail✝) + size t2

State before:
case node_case.cons
x : Nat
head✝ : NatTree
tail✝ : List NatTree
ih :
  (∀ (t2 : NatTree), size (splice head✝ t2) = size head✝ + size t2) ∧
    all (fun t1 => ∀ (t2 : NatTree), size (splice t1 t2) = size t1 + size t2) tail✝
⊢ ∀ (t2 : NatTree), 1 + (size head✝ + size t2 + nodeListSize tail✝) = 1 + (size head✝ + nodeListSize tail✝) + size t2
Tactic:
simp_arith
State after:
no goals