Theorem: Packet.children_mult_levels (days/day13.lean)

State before:
x : Packet
ys : List Packet
⊢ levels (children x) + levels ys < level x + level (Multiple ys)
Tactic:
cases x <;> simp [children, levels, level]
State after:
case Single
ys : List Packet
a✝ : Nat
⊢ 1 + levels ys < levels ys + 2

case Multiple
ys a✝ : List Packet
⊢ levels a✝ + levels ys < levels a✝ + 2 + (levels ys + 2)

State before:
case Single
ys : List Packet
a✝ : Nat
⊢ 1 + levels ys < levels ys + 2

case Multiple
ys a✝ : List Packet
⊢ levels a✝ + levels ys < levels a✝ + 2 + (levels ys + 2)
Tactic:
. case Single x => 
  rw [Nat.add_comm]
  apply Nat.lt_succ_self
State after:
case Multiple
ys a✝ : List Packet
⊢ levels a✝ + levels ys < levels a✝ + 2 + (levels ys + 2)

State before:
case Multiple
ys a✝ : List Packet
⊢ levels a✝ + levels ys < levels a✝ + 2 + (levels ys + 2)
Tactic:
. case Multiple xs => 
  conv => 
    rhs
    rw [Nat.add_assoc]
    conv => 
      rhs
      rw [← Nat.add_assoc]
      conv => 
        lhs
        rw [Nat.add_comm]  
      rw [Nat.add_assoc]
      simp [Nat.add]
    rw [←Nat.add_assoc]
  apply @Nat.add_lt_add_left 0
  apply Nat.zero_lt_succ
State after:
no goals

State before:
ys : List Packet
x : Nat
⊢ 1 + levels ys < levels ys + 2
Tactic:
rw [Nat.add_comm]
State after:
ys : List Packet
x : Nat
⊢ levels ys + 1 < levels ys + 2

State before:
ys : List Packet
x : Nat
⊢ levels ys + 1 < levels ys + 2
Tactic:
apply Nat.lt_succ_self
State after:
no goals

State before:
ys xs : List Packet
⊢ levels xs + levels ys < levels xs + 2 + (levels ys + 2)
Tactic:
conv => 
  rhs
  rw [Nat.add_assoc]
  conv => 
    rhs
    rw [← Nat.add_assoc]
    conv => 
      lhs
      rw [Nat.add_comm]  
    rw [Nat.add_assoc]
    simp [Nat.add]
  rw [←Nat.add_assoc]
State after:
ys xs : List Packet
⊢ levels xs + levels ys < levels xs + levels ys + (2 + 2)

State before:
ys xs : List Packet
⊢ levels xs + levels ys < levels xs + levels ys + (2 + 2)
Tactic:
apply @Nat.add_lt_add_left 0
State after:
case h
ys xs : List Packet
⊢ 0 < 2 + 2

State before:
case h
ys xs : List Packet
⊢ 0 < 2 + 2
Tactic:
apply Nat.zero_lt_succ
State after:
no goals