∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq γ] {s : Finset α} {t : Finset β}
  [inst_1 : DecidableEq δ] (f : α → β → γ) (g : γ → δ),
  Finset.image g (Finset.image₂ f s t) = Finset.image₂ (fun a b => g (f a b)) s t