∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s : Finset β} (p : β → Prop)
  [inst_2 : DecidablePred p] {f : (b : β) → p b → α} {g : (b : β) → ¬p b → α} {b : β},
  b ∈ s → ∀ (h₁ : ¬p b), (s.inf fun i => if h : p i then f i h else g i h) ≤ g b h₁