case h
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
x✝ : α
⊢ x✝ ∈ supp x ↔ x✝ ∈ {u | ∀ (a : (P F).A) (f : PFunctor.B (P F) a → α), abs { fst := a, snd := f } = x → u ∈ f '' univ}
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
⊢ supp x = {u | ∀ (a : (P F).A) (f : PFunctor.B (P F) a → α), abs { fst := a, snd := f } = x → u ∈ f '' univ}
ext
no goals
case h
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
x✝ : α
⊢ x✝ ∈ supp x ↔ x✝ ∈ {u | ∀ (a : (P F).A) (f : PFunctor.B (P F) a → α), abs { fst := a, snd := f } = x → u ∈ f '' univ}
apply mem_supp