no goals
α : Type u_1
a : α
inst✝ : SizeOf α
as : List α
h : a ∈ as
⊢ sizeOf a < sizeOf as
induction h with
| head => simp_arith
| tail _ _ ih => exact Nat.lt_trans ih (by simp_arith)
no goals
case head
α : Type u_1
a : α
inst✝ : SizeOf α
as as✝ : List α
⊢ sizeOf a < sizeOf (a :: as✝)
simp_arith
no goals
case tail
α : Type u_1
a : α
inst✝ : SizeOf α
as : List α
b✝ : α
as✝ : List α
a✝ : Mem a as✝
ih : sizeOf a < sizeOf as✝
⊢ sizeOf a < sizeOf (b✝ :: as✝)
exact Nat.lt_trans ih (by simp_arith)
no goals
α : Type u_1
a : α
inst✝ : SizeOf α
as : List α
b✝ : α
as✝ : List α
a✝ : Mem a as✝
ih : sizeOf a < sizeOf as✝
⊢ sizeOf as✝ < sizeOf (b✝ :: as✝)
simp_arith