F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
u : α
⊢ u ∈ {y | ∀ ⦃p : α → Prop⦄, Liftp p x → p y} ↔
    ∀ (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 α
u : α
⊢ u ∈ supp x ↔ ∀ (a : (P F).A) (f : PFunctor.B (P F) a → α), abs { fst := a, snd := f } = x → u ∈ f '' univ
rw [supp]
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
u : α
⊢ (∀ ⦃p : α → Prop⦄, Liftp p x → p 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 α
u : α
⊢ u ∈ {y | ∀ ⦃p : α → Prop⦄, Liftp p x → p y} ↔
    ∀ (a : (P F).A) (f : PFunctor.B (P F) a → α), abs { fst := a, snd := f } = x → u ∈ f '' univ
dsimp
case mp
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
u : α
⊢ (∀ ⦃p : α → Prop⦄, Liftp p x → p u) →
    ∀ (a : (P F).A) (f : PFunctor.B (P F) a → α), abs { fst := a, snd := f } = x → u ∈ f '' univ

case mpr
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
u : α
⊢ (∀ (a : (P F).A) (f : PFunctor.B (P F) a → α), abs { fst := a, snd := f } = x → u ∈ f '' univ) →
    ∀ ⦃p : α → Prop⦄, Liftp p x → p u
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
u : α
⊢ (∀ ⦃p : α → Prop⦄, Liftp p x → p u) ↔
    ∀ (a : (P F).A) (f : PFunctor.B (P F) a → α), abs { fst := a, snd := f } = x → u ∈ f '' univ
constructor
case mpr
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
u : α
h : ∀ (a : (P F).A) (f : PFunctor.B (P F) a → α), abs { fst := a, snd := f } = x → u ∈ f '' univ
p : α → Prop
⊢ Liftp p x → p u
case mpr
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
u : α
⊢ (∀ (a : (P F).A) (f : PFunctor.B (P F) a → α), abs { fst := a, snd := f } = x → u ∈ f '' univ) →
    ∀ ⦃p : α → Prop⦄, Liftp p x → p u
intro h p
case mpr
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
u : α
h : ∀ (a : (P F).A) (f : PFunctor.B (P F) a → α), abs { fst := a, snd := f } = x → u ∈ f '' univ
p : α → Prop
⊢ (∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : PFunctor.B (P F) a), p (f i)) → p u
case mpr
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
u : α
h : ∀ (a : (P F).A) (f : PFunctor.B (P F) a → α), abs { fst := a, snd := f } = x → u ∈ f '' univ
p : α → Prop
⊢ Liftp p x → p u
rw [liftp_iff]
case mpr.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
u : α
h : ∀ (a : (P F).A) (f : PFunctor.B (P F) a → α), abs { fst := a, snd := f } = x → u ∈ f '' univ
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : PFunctor.B (P F) a), p (f i)
⊢ p u
case mpr
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
u : α
h : ∀ (a : (P F).A) (f : PFunctor.B (P F) a → α), abs { fst := a, snd := f } = x → u ∈ f '' univ
p : α → Prop
⊢ (∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : PFunctor.B (P F) a), p (f i)) → p u
rintro ⟨a, f, xeq, h'⟩
case mpr.intro.intro.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
u : α
h : ∀ (a : (P F).A) (f : PFunctor.B (P F) a → α), abs { fst := a, snd := f } = x → u ∈ f '' univ
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : PFunctor.B (P F) a), p (f i)
i : PFunctor.B (P F) a
left✝ : i ∈ univ
hi : f i = u
⊢ p u
case mpr.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
u : α
h : ∀ (a : (P F).A) (f : PFunctor.B (P F) a → α), abs { fst := a, snd := f } = x → u ∈ f '' univ
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : PFunctor.B (P F) a), p (f i)
⊢ p u
rcases h a f xeq.symm with ⟨i, _, hi⟩
case mpr.intro.intro.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
u : α
h : ∀ (a : (P F).A) (f : PFunctor.B (P F) a → α), abs { fst := a, snd := f } = x → u ∈ f '' univ
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : PFunctor.B (P F) a), p (f i)
i : PFunctor.B (P F) a
left✝ : i ∈ univ
hi : f i = u
⊢ p (f i)
case mpr.intro.intro.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
u : α
h : ∀ (a : (P F).A) (f : PFunctor.B (P F) a → α), abs { fst := a, snd := f } = x → u ∈ f '' univ
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : PFunctor.B (P F) a), p (f i)
i : PFunctor.B (P F) a
left✝ : i ∈ univ
hi : f i = u
⊢ p u
rw [← hi]
no goals
case mpr.intro.intro.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
u : α
h : ∀ (a : (P F).A) (f : PFunctor.B (P F) a → α), abs { fst := a, snd := f } = x → u ∈ f '' univ
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : PFunctor.B (P F) a), p (f i)
i : PFunctor.B (P F) a
left✝ : i ∈ univ
hi : f i = u
⊢ p (f i)
apply h'
case mp
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
u : α
h : ∀ ⦃p : α → Prop⦄, Liftp p x → p u
a : (P F).A
f : PFunctor.B (P F) a → α
haf : abs { fst := a, snd := f } = x
⊢ u ∈ f '' univ
case mp
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
u : α
⊢ (∀ ⦃p : α → Prop⦄, Liftp p x → p u) →
    ∀ (a : (P F).A) (f : PFunctor.B (P F) a → α), abs { fst := a, snd := f } = x → u ∈ f '' univ
intro h a f haf
case mp
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
u : α
h : ∀ ⦃p : α → Prop⦄, Liftp p x → p u
a : (P F).A
f : PFunctor.B (P F) a → α
haf : abs { fst := a, snd := f } = x
this : Liftp (fun u => u ∈ f '' univ) x
⊢ u ∈ f '' univ
case mp
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
u : α
h : ∀ ⦃p : α → Prop⦄, Liftp p x → p u
a : (P F).A
f : PFunctor.B (P F) a → α
haf : abs { fst := a, snd := f } = x
⊢ u ∈ f '' univ
have : Liftp (fun u => u ∈ f '' univ) x := by
  rw [liftp_iff]
  refine' ⟨a, f, haf.symm, fun i => mem_image_of_mem _ (mem_univ _)⟩
no goals
case mp
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
u : α
h : ∀ ⦃p : α → Prop⦄, Liftp p x → p u
a : (P F).A
f : PFunctor.B (P F) a → α
haf : abs { fst := a, snd := f } = x
this : Liftp (fun u => u ∈ f '' univ) x
⊢ u ∈ f '' univ
exact h this
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
u : α
h : ∀ ⦃p : α → Prop⦄, Liftp p x → p u
a : (P F).A
f : PFunctor.B (P F) a → α
haf : abs { fst := a, snd := f } = x
⊢ ∃ a_1 f_1, x = abs { fst := a_1, snd := f_1 } ∧ ∀ (i : PFunctor.B (P F) a_1), f_1 i ∈ f '' univ
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
u : α
h : ∀ ⦃p : α → Prop⦄, Liftp p x → p u
a : (P F).A
f : PFunctor.B (P F) a → α
haf : abs { fst := a, snd := f } = x
⊢ Liftp (fun u => u ∈ f '' univ) x
rw [liftp_iff]
no goals
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
u : α
h : ∀ ⦃p : α → Prop⦄, Liftp p x → p u
a : (P F).A
f : PFunctor.B (P F) a → α
haf : abs { fst := a, snd := f } = x
⊢ ∃ a_1 f_1, x = abs { fst := a_1, snd := f_1 } ∧ ∀ (i : PFunctor.B (P F) a_1), f_1 i ∈ f '' univ
refine' ⟨a, f, haf.symm, fun i => mem_image_of_mem _ (mem_univ _)⟩