case cons.head
ι : Type ?u.320638
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x : α
l : List α
hx : x ∈ l
t : List α
ih : x ∈ t → sizeOf x < sizeOf t
⊢ sizeOf x < 1 + sizeOf x + sizeOf t

case cons.tail
ι : Type ?u.320638
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x : α
l : List α
hx : x ∈ l
h : α
t : List α
ih : x ∈ t → sizeOf x < sizeOf t
a✝ : Mem x t
⊢ sizeOf x < 1 + sizeOf h + sizeOf t
ι : Type ?u.320638
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x : α
l : List α
hx : x ∈ l
⊢ sizeOf x < sizeOf l
induction' l with h t ih <;> cases hx <;> rw [cons.sizeOf_spec]
no goals
case cons.head
ι : Type ?u.320638
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x : α
l : List α
hx : x ∈ l
t : List α
ih : x ∈ t → sizeOf x < sizeOf t
⊢ sizeOf x < 1 + sizeOf x + sizeOf t
exact lt_add_of_lt_of_nonneg (lt_one_add _) (Nat.zero_le _)
case cons.tail
ι : Type ?u.320638
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x : α
l : List α
hx : x ∈ l
h : α
t : List α
ih : x ∈ t → sizeOf x < sizeOf t
a✝ : Mem x t
⊢ 0 < 1 + sizeOf h
case cons.tail
ι : Type ?u.320638
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x : α
l : List α
hx : x ∈ l
h : α
t : List α
ih : x ∈ t → sizeOf x < sizeOf t
a✝ : Mem x t
⊢ sizeOf x < 1 + sizeOf h + sizeOf t
refine lt_add_of_pos_of_le ?_ (le_of_lt (ih ‹_›))
case cons.tail
ι : Type ?u.320638
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x : α
l : List α
hx : x ∈ l
h : α
t : List α
ih : x ∈ t → sizeOf x < sizeOf t
a✝ : Mem x t
⊢ 0 < sizeOf h + 1
case cons.tail
ι : Type ?u.320638
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x : α
l : List α
hx : x ∈ l
h : α
t : List α
ih : x ∈ t → sizeOf x < sizeOf t
a✝ : Mem x t
⊢ 0 < 1 + sizeOf h
rw [add_comm]
no goals
case cons.tail
ι : Type ?u.320638
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : SizeOf α
x : α
l : List α
hx : x ∈ l
h : α
t : List α
ih : x ∈ t → sizeOf x < sizeOf t
a✝ : Mem x t
⊢ 0 < sizeOf h + 1
exact succ_pos _