no goals
α : Type u_4
β : Type u_2
γ : Type u_3
f✝ : α ↪ β
s : Finset α
β' : Type u_1
f : β ↪ γ
g : α ↪ β
f' : α ↪ β'
g' : β' ↪ γ
h_comm : ∀ (a : α), ↑f (↑g a) = ↑g' (↑f' a)
⊢ map f (map g s) = map g' (map f' s)
simp_rw [map_map, Embedding.trans, Function.comp, h_comm]