no goals
α : Type u_1
β : Type ?u.95849
γ : Type ?u.95852
ι : Sort ?u.95855
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : Set.Nonempty s
⊢ ↑(sInf s) = ⨅ (a : α) (_ : a ∈ s), ↑a
rw [coe_sInf' hs, sInf_image]