case inl
α β : Type u
⊢ lift (sInf ∅) = sInf (lift '' ∅)

case inr
α β : Type u
s : Set Cardinal
hs : Set.Nonempty s
⊢ lift (sInf s) = sInf (lift '' s)
α β : Type u
s : Set Cardinal
⊢ lift (sInf s) = sInf (lift '' s)
rcases eq_empty_or_nonempty s with (rfl | hs)
no goals
case inl
α β : Type u
⊢ lift (sInf ∅) = sInf (lift '' ∅)
simp
no goals
case inr
α β : Type u
s : Set Cardinal
hs : Set.Nonempty s
⊢ lift (sInf s) = sInf (lift '' s)
exact  lift_monotone.map_csInf hs