∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeInf α] {s : Finset β} {t : Finset γ}
  (h : (s ×ˢ t).Nonempty) (f : β × γ → α), (s ×ˢ t).inf' h f = s.inf' ⋯ fun i => t.inf' ⋯ fun i' => f (i, i')