intro ⟨y, ⟨x, hx, hxy⟩, hyz⟩
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
case a.mpr
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
z : γ
y : β
x : α
hx : x ∈ s
hxy : f x = y
hyz : g y = z
⊢ z ∈ Set.map (g ∘ f) s