∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α}
  {t : Finset β} [inst_1 : SemilatticeSup δ] {g : γ → δ} {a : δ} (h : (Finset.image₂ f s t).Nonempty),
  ((Finset.image₂ f s t).sup' h g ≤ a) = ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a