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

State before:
xs : List Packet
⊢ ¬IsSingle (Multiple xs)
Tactic:
intros ex
State after:
xs : List Packet
ex : IsSingle (Multiple xs)
⊢ False

State before:
xs : List Packet
ex : IsSingle (Multiple xs)
⊢ False
Tactic:
cases ex
State after:
case intro
xs : List Packet
w✝ : Nat
h✝ : Multiple xs = Single w✝
⊢ False

State before:
case intro
xs : List Packet
w✝ : Nat
h✝ : Multiple xs = Single w✝
⊢ False
Tactic:
contradiction
State after:
no goals