case mk
α : Type u_1
β : Type ?u.287378
γ : Type ?u.287381
inst✝ : SizeOf α
x : α
val✝ : Multiset α
nodup✝ : Nodup val✝
hx : x ∈ { val := val✝, nodup := nodup✝ }
⊢ SizeOf.sizeOf x < SizeOf.sizeOf { val := val✝, nodup := nodup✝ }
α : Type u_1
β : Type ?u.287378
γ : Type ?u.287381
inst✝ : SizeOf α
x : α
s : Finset α
hx : x ∈ s
⊢ SizeOf.sizeOf x < SizeOf.sizeOf s
cases s
case mk
α : Type u_1
β : Type ?u.287378
γ : Type ?u.287381
inst✝ : SizeOf α
x : α
val✝ : Multiset α
nodup✝ : Nodup val✝
hx : x ∈ { val := val✝, nodup := nodup✝ }
⊢ SizeOf.sizeOf x <
    1 +
      Quot.liftOn val✝ (fun m => List._sizeOf_1 m)
        (_ : ∀ (x x_1 : List α), x ~ x_1 → SizeOf.sizeOf x = SizeOf.sizeOf x_1)
case mk
α : Type u_1
β : Type ?u.287378
γ : Type ?u.287381
inst✝ : SizeOf α
x : α
val✝ : Multiset α
nodup✝ : Nodup val✝
hx : x ∈ { val := val✝, nodup := nodup✝ }
⊢ SizeOf.sizeOf x < SizeOf.sizeOf { val := val✝, nodup := nodup✝ }
dsimp [SizeOf.sizeOf, SizeOf.sizeOf, Multiset.sizeOf]
case mk
α : Type u_1
β : Type ?u.287378
γ : Type ?u.287381
inst✝ : SizeOf α
x : α
val✝ : Multiset α
nodup✝ : Nodup val✝
hx : x ∈ { val := val✝, nodup := nodup✝ }
⊢ SizeOf.sizeOf x <
    Quot.liftOn val✝ (fun m => List._sizeOf_1 m)
        (_ : ∀ (x x_1 : List α), x ~ x_1 → SizeOf.sizeOf x = SizeOf.sizeOf x_1) +
      1
case mk
α : Type u_1
β : Type ?u.287378
γ : Type ?u.287381
inst✝ : SizeOf α
x : α
val✝ : Multiset α
nodup✝ : Nodup val✝
hx : x ∈ { val := val✝, nodup := nodup✝ }
⊢ SizeOf.sizeOf x <
    1 +
      Quot.liftOn val✝ (fun m => List._sizeOf_1 m)
        (_ : ∀ (x x_1 : List α), x ~ x_1 → SizeOf.sizeOf x = SizeOf.sizeOf x_1)
rw [add_comm]
case mk
α : Type u_1
β : Type ?u.287378
γ : Type ?u.287381
inst✝ : SizeOf α
x : α
val✝ : Multiset α
nodup✝ : Nodup val✝
hx : x ∈ { val := val✝, nodup := nodup✝ }
⊢ SizeOf.sizeOf x <
    Quot.liftOn val✝ (fun m => List._sizeOf_1 m) (_ : ∀ (x x_1 : List α), x ~ x_1 → SizeOf.sizeOf x = SizeOf.sizeOf x_1)
case mk
α : Type u_1
β : Type ?u.287378
γ : Type ?u.287381
inst✝ : SizeOf α
x : α
val✝ : Multiset α
nodup✝ : Nodup val✝
hx : x ∈ { val := val✝, nodup := nodup✝ }
⊢ SizeOf.sizeOf x <
    Quot.liftOn val✝ (fun m => List._sizeOf_1 m)
        (_ : ∀ (x x_1 : List α), x ~ x_1 → SizeOf.sizeOf x = SizeOf.sizeOf x_1) +
      1
refine' lt_trans _ (Nat.lt_succ_self _)
no goals
case mk
α : Type u_1
β : Type ?u.287378
γ : Type ?u.287381
inst✝ : SizeOf α
x : α
val✝ : Multiset α
nodup✝ : Nodup val✝
hx : x ∈ { val := val✝, nodup := nodup✝ }
⊢ SizeOf.sizeOf x <
    Quot.liftOn val✝ (fun m => List._sizeOf_1 m) (_ : ∀ (x x_1 : List α), x ~ x_1 → SizeOf.sizeOf x = SizeOf.sizeOf x_1)
exact Multiset.sizeOf_lt_sizeOf_of_mem hx