∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op]
  {f : α → β} {b : β} [inst : DecidableEq α] {g : γ → α} {s : Finset γ} [hi : Std.IdempotentOp op],
  Finset.fold op b f (Finset.image g s) = Finset.fold op b (f ∘ g) s