intro z
case a
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
⊢ ∀ (x : γ), x ∈ Set.map (g ∘ f) s ↔ x ∈ Set.map g (Set.map f s)
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)