no goals
α : Type u_4
β : Type u_3
γ : Type u_2
ι : Sort ?u.27932
ι' : Sort ?u.27935
f✝ : α → β
s t : Set α
β' : Type u_1
f : β → γ
g : α → β
f' : α → β'
g' : β' → γ
h_comm : ∀ (a : α), f (g a) = g' (f' a)
⊢ f '' (g '' s) = g' '' (f' '' s)
simp_rw [image_image, h_comm]