cases hgof'
case a.mpr
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
z : γ
gof : α → γ
go : (α → β) → α → γ
g' : β → γ
hg' : g' ∈ g
hgo : (fun x x_1 => x ∘ x_1) g' = go
f' : α → β
hf' : f' ∈ f
hgof' : go f' = gof
x : α
hx : x ∈ s
hz : gof x = z
⊢ z ∈ g.seq (f.seq s)
case a.mpr.refl
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
z : γ
go : (α → β) → α → γ
g' : β → γ
hg' : g' ∈ g
hgo : (fun x x_1 => x ∘ x_1) g' = go
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hz : go f' x = z
⊢ z ∈ g.seq (f.seq s)