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

State before:
x y : Packet
p : ¬(IsSingle x ∧ IsSingle y)
⊢ levels (children x) + levels (children y) < level x + level y
Tactic:
cases x
State after:
case Single
y : Packet
a✝ : Nat
p : ¬(IsSingle (Single a✝) ∧ IsSingle y)
⊢ levels (children (Single a✝)) + levels (children y) < level (Single a✝) + level y

case Multiple
y : Packet
a✝ : List Packet
p : ¬(IsSingle (Multiple a✝) ∧ IsSingle y)
⊢ levels (children (Multiple a✝)) + levels (children y) < level (Multiple a✝) + level y

State before:
case Single
y : Packet
a✝ : Nat
p : ¬(IsSingle (Single a✝) ∧ IsSingle y)
⊢ levels (children (Single a✝)) + levels (children y) < level (Single a✝) + level y

case Multiple
y : Packet
a✝ : List Packet
p : ¬(IsSingle (Multiple a✝) ∧ IsSingle y)
⊢ levels (children (Multiple a✝)) + levels (children y) < level (Multiple a✝) + level y
Tactic:
. case Single x =>
  cases y
  . case Single y =>
    apply False.elim
    apply p
    constructor
    . exists x
    . exists y
  . case Multiple ys => 
    apply children_mult_levels
State after:
case Multiple
y : Packet
a✝ : List Packet
p : ¬(IsSingle (Multiple a✝) ∧ IsSingle y)
⊢ levels (children (Multiple a✝)) + levels (children y) < level (Multiple a✝) + level y

State before:
case Multiple
y : Packet
a✝ : List Packet
p : ¬(IsSingle (Multiple a✝) ∧ IsSingle y)
⊢ levels (children (Multiple a✝)) + levels (children y) < level (Multiple a✝) + level y
Tactic:
. case Multiple xs =>
    conv => 
      lhs
      rw [Nat.add_comm] 
    conv => 
      rhs
      rw [Nat.add_comm] 
    apply children_mult_levels
State after:
no goals

State before:
y : Packet
x : Nat
p : ¬(IsSingle (Single x) ∧ IsSingle y)
⊢ levels (children (Single x)) + levels (children y) < level (Single x) + level y
Tactic:
cases y
State after:
case Single
x a✝ : Nat
p : ¬(IsSingle (Single x) ∧ IsSingle (Single a✝))
⊢ levels (children (Single x)) + levels (children (Single a✝)) < level (Single x) + level (Single a✝)

case Multiple
x : Nat
a✝ : List Packet
p : ¬(IsSingle (Single x) ∧ IsSingle (Multiple a✝))
⊢ levels (children (Single x)) + levels (children (Multiple a✝)) < level (Single x) + level (Multiple a✝)

State before:
case Single
x a✝ : Nat
p : ¬(IsSingle (Single x) ∧ IsSingle (Single a✝))
⊢ levels (children (Single x)) + levels (children (Single a✝)) < level (Single x) + level (Single a✝)

case Multiple
x : Nat
a✝ : List Packet
p : ¬(IsSingle (Single x) ∧ IsSingle (Multiple a✝))
⊢ levels (children (Single x)) + levels (children (Multiple a✝)) < level (Single x) + level (Multiple a✝)
Tactic:
. case Single y =>
  apply False.elim
  apply p
  constructor
  . exists x
  . exists y
State after:
case Multiple
x : Nat
a✝ : List Packet
p : ¬(IsSingle (Single x) ∧ IsSingle (Multiple a✝))
⊢ levels (children (Single x)) + levels (children (Multiple a✝)) < level (Single x) + level (Multiple a✝)

State before:
case Multiple
x : Nat
a✝ : List Packet
p : ¬(IsSingle (Single x) ∧ IsSingle (Multiple a✝))
⊢ levels (children (Single x)) + levels (children (Multiple a✝)) < level (Single x) + level (Multiple a✝)
Tactic:
. case Multiple ys => 
  apply children_mult_levels
State after:
no goals

State before:
x y : Nat
p : ¬(IsSingle (Single x) ∧ IsSingle (Single y))
⊢ levels (children (Single x)) + levels (children (Single y)) < level (Single x) + level (Single y)
Tactic:
apply False.elim
State after:
case h
x y : Nat
p : ¬(IsSingle (Single x) ∧ IsSingle (Single y))
⊢ False

State before:
case h
x y : Nat
p : ¬(IsSingle (Single x) ∧ IsSingle (Single y))
⊢ False
Tactic:
apply p
State after:
case h
x y : Nat
p : ¬(IsSingle (Single x) ∧ IsSingle (Single y))
⊢ IsSingle (Single x) ∧ IsSingle (Single y)

State before:
case h
x y : Nat
p : ¬(IsSingle (Single x) ∧ IsSingle (Single y))
⊢ IsSingle (Single x) ∧ IsSingle (Single y)
Tactic:
constructor
State after:
case h.left
x y : Nat
p : ¬(IsSingle (Single x) ∧ IsSingle (Single y))
⊢ IsSingle (Single x)

case h.right
x y : Nat
p : ¬(IsSingle (Single x) ∧ IsSingle (Single y))
⊢ IsSingle (Single y)

State before:
case h.left
x y : Nat
p : ¬(IsSingle (Single x) ∧ IsSingle (Single y))
⊢ IsSingle (Single x)

case h.right
x y : Nat
p : ¬(IsSingle (Single x) ∧ IsSingle (Single y))
⊢ IsSingle (Single y)
Tactic:
. exists x
State after:
case h.right
x y : Nat
p : ¬(IsSingle (Single x) ∧ IsSingle (Single y))
⊢ IsSingle (Single y)

State before:
case h.right
x y : Nat
p : ¬(IsSingle (Single x) ∧ IsSingle (Single y))
⊢ IsSingle (Single y)
Tactic:
. exists y
State after:
no goals

State before:
x : Nat
ys : List Packet
p : ¬(IsSingle (Single x) ∧ IsSingle (Multiple ys))
⊢ levels (children (Single x)) + levels (children (Multiple ys)) < level (Single x) + level (Multiple ys)
Tactic:
apply children_mult_levels
State after:
no goals

State before:
y : Packet
xs : List Packet
p : ¬(IsSingle (Multiple xs) ∧ IsSingle y)
⊢ levels (children (Multiple xs)) + levels (children y) < level (Multiple xs) + level y
Tactic:
conv => 
  lhs
  rw [Nat.add_comm]
State after:
y : Packet
xs : List Packet
p : ¬(IsSingle (Multiple xs) ∧ IsSingle y)
⊢ levels (children y) + levels (children (Multiple xs)) < level (Multiple xs) + level y

State before:
y : Packet
xs : List Packet
p : ¬(IsSingle (Multiple xs) ∧ IsSingle y)
⊢ levels (children y) + levels (children (Multiple xs)) < level (Multiple xs) + level y
Tactic:
conv => 
  rhs
  rw [Nat.add_comm]
State after:
y : Packet
xs : List Packet
p : ¬(IsSingle (Multiple xs) ∧ IsSingle y)
⊢ levels (children y) + levels (children (Multiple xs)) < level y + level (Multiple xs)

State before:
y : Packet
xs : List Packet
p : ¬(IsSingle (Multiple xs) ∧ IsSingle y)
⊢ levels (children y) + levels (children (Multiple xs)) < level y + level (Multiple xs)
Tactic:
apply children_mult_levels
State after:
no goals