∀ {α : 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₂ f (Finset.image g s) t = Finset.image₂ (fun a b => f (g a) b) s t