∀ {ι : Type u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] (f : ι → α) {s : Finset ι},
  (∃ x ∈ s, f x ≤ sInf ∅) →
    ∀ (h' : autoParam (Finset.image f s).Nonempty Finset.ciInf_eq_min'_image._auto_1),
      ⨅ i ∈ s, f i = (Finset.image f s).min' h'