no goals
α : Type u_2
β : Type u_1
γ : Type u_3
ι : Sort ?u.23873
π : α → Type ?u.23878
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f✝ f₁ f₂ f₃ : α → β
g✝ g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
f : α → β
g : γ → α
s : Set β
⊢ MapsTo f (range g) s ↔ MapsTo (f ∘ g) univ s
rw [← image_univ, maps_image_to]