∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  (gi : GaloisInsertion l u) {ι : Sort x} {p : ι → Prop} (f : (i : ι) → p i → β),
  l (⨅ i, ⨅ (hi : p i), u (f i hi)) = ⨅ i, ⨅ (hi : p i), f i hi