constructor
case a
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
z : γ
⊢ z ∈ Set.map (g ∘ f) s ↔ z ∈ Set.map g (Set.map f s)
case a.mp
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
z : γ
⊢ z ∈ Set.map (g ∘ f) s → z ∈ Set.map g (Set.map f s)

case a.mpr
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
z : γ
⊢ z ∈ Set.map g (Set.map f s) → z ∈ Set.map (g ∘ f) s