case h
α : Type u_1
β : Type ?u.137282
γ : Type ?u.137285
inst✝ : SizeOf α
x : α
s : Multiset α
hx✝ : x ∈ s
l : List α
hx : x ∈ Quot.mk Setoid.r l
⊢ SizeOf.sizeOf x < SizeOf.sizeOf (Quot.mk Setoid.r l)
α : Type u_1
β : Type ?u.137282
γ : Type ?u.137285
inst✝ : SizeOf α
x : α
s : Multiset α
hx : x ∈ s
⊢ SizeOf.sizeOf x < SizeOf.sizeOf s
induction' s using Quot.inductionOn with l a b
no goals
case h
α : Type u_1
β : Type ?u.137282
γ : Type ?u.137285
inst✝ : SizeOf α
x : α
s : Multiset α
hx✝ : x ∈ s
l : List α
hx : x ∈ Quot.mk Setoid.r l
⊢ SizeOf.sizeOf x < SizeOf.sizeOf (Quot.mk Setoid.r l)
exact List.sizeOf_lt_sizeOf_of_mem hx