∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] (p : ι → Prop) [inst_1 : DecidablePred p] (f g : ι → α),
  (⨅ i, if p i then f i else g i) = (⨅ i, ⨅ (_ : p i), f i) ⊓ ⨅ i, ⨅ (_ : ¬p i), g i