Theorem: List.sizeOf_pos (One.lean)

State before:
α : Type u_1
l : List α
⊢ sizeOf l > 0
Tactic:
cases l <;> simp only [cons.sizeOf_spec, nil.sizeOf_spec, sizeOf_default, add_zero, zero_le, ge_iff_le, nonpos_iff_eq_zero, gt_iff_lt,
  add_pos_iff, true_or]
State after:
no goals