case mp
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
⊢ (∀ (p : α → Prop), Liftp p x ↔ ∀ (u : α), u ∈ supp x → p u) →
    ∃ a f,
      abs { fst := a, snd := f } = x ∧
        ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ

case mpr
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
⊢ (∃ a f,
      abs { fst := a, snd := f } = x ∧
        ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ) →
    ∀ (p : α → Prop), Liftp p x ↔ ∀ (u : α), u ∈ supp x → p u
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
⊢ (∀ (p : α → Prop), Liftp p x ↔ ∀ (u : α), u ∈ supp x → p u) ↔
    ∃ a f,
      abs { fst := a, snd := f } = x ∧
        ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
constructor
case mpr.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : abs { fst := a, snd := f } = x
h : ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
p : α → Prop
⊢ Liftp p x ↔ ∀ (u : α), u ∈ supp x → p u
case mpr
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
⊢ (∃ a f,
      abs { fst := a, snd := f } = x ∧
        ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ) →
    ∀ (p : α → Prop), Liftp p x ↔ ∀ (u : α), u ∈ supp x → p u
rintro ⟨a, f, xeq, h⟩ p
case mpr.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : abs { fst := a, snd := f } = x
h : ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
p : α → Prop
⊢ (∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : PFunctor.B (P F) a), p (f i)) ↔ ∀ (u : α), u ∈ supp x → p u
case mpr.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : abs { fst := a, snd := f } = x
h : ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
p : α → Prop
⊢ Liftp p x ↔ ∀ (u : α), u ∈ supp x → p u
rw [liftp_iff]
case mpr.intro.intro.intro.mp
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : abs { fst := a, snd := f } = x
h : ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
p : α → Prop
⊢ (∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : PFunctor.B (P F) a), p (f i)) → ∀ (u : α), u ∈ supp x → p u

case mpr.intro.intro.intro.mpr
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : abs { fst := a, snd := f } = x
h : ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
p : α → Prop
⊢ (∀ (u : α), u ∈ supp x → p u) → ∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : PFunctor.B (P F) a), p (f i)
case mpr.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : abs { fst := a, snd := f } = x
h : ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
p : α → Prop
⊢ (∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : PFunctor.B (P F) a), p (f i)) ↔ ∀ (u : α), u ∈ supp x → p u
constructor
case mpr.intro.intro.intro.mpr
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : abs { fst := a, snd := f } = x
h : ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
p : α → Prop
h' : ∀ (u : α), u ∈ supp x → p u
⊢ ∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : PFunctor.B (P F) a), p (f i)
case mpr.intro.intro.intro.mpr
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : abs { fst := a, snd := f } = x
h : ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
p : α → Prop
⊢ (∀ (u : α), u ∈ supp x → p u) → ∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : PFunctor.B (P F) a), p (f i)
intro h'
case mpr.intro.intro.intro.mpr
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : abs { fst := a, snd := f } = x
h : ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
p : α → Prop
h' : ∀ (u : α), u ∈ supp x → p u
⊢ ∀ (i : PFunctor.B (P F) a), p (f i)
case mpr.intro.intro.intro.mpr
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : abs { fst := a, snd := f } = x
h : ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
p : α → Prop
h' : ∀ (u : α), u ∈ supp x → p u
⊢ ∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : PFunctor.B (P F) a), p (f i)
refine' ⟨a, f, xeq.symm, _⟩
case mpr.intro.intro.intro.mpr
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : abs { fst := a, snd := f } = x
h : ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
p : α → Prop
h' : ∀ (u : α), u ∈ supp x → p u
i : PFunctor.B (P F) a
⊢ p (f i)
case mpr.intro.intro.intro.mpr
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : abs { fst := a, snd := f } = x
h : ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
p : α → Prop
h' : ∀ (u : α), u ∈ supp x → p u
⊢ ∀ (i : PFunctor.B (P F) a), p (f i)
intro i
case mpr.intro.intro.intro.mpr.a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : abs { fst := a, snd := f } = x
h : ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
p : α → Prop
h' : ∀ (u : α), u ∈ supp x → p u
i : PFunctor.B (P F) a
⊢ f i ∈ supp x
case mpr.intro.intro.intro.mpr
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : abs { fst := a, snd := f } = x
h : ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
p : α → Prop
h' : ∀ (u : α), u ∈ supp x → p u
i : PFunctor.B (P F) a
⊢ p (f i)
apply h'
case mpr.intro.intro.intro.mpr.a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : abs { fst := a, snd := f } = x
h : ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
p : α → Prop
h' : ∀ (u : α), u ∈ supp x → p u
i : PFunctor.B (P F) a
⊢ ∀ (a : (P F).A) (f_1 : PFunctor.B (P F) a → α), abs { fst := a, snd := f_1 } = x → f i ∈ f_1 '' univ
case mpr.intro.intro.intro.mpr.a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : abs { fst := a, snd := f } = x
h : ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
p : α → Prop
h' : ∀ (u : α), u ∈ supp x → p u
i : PFunctor.B (P F) a
⊢ f i ∈ supp x
rw [mem_supp]
case mpr.intro.intro.intro.mpr.a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : abs { fst := a, snd := f } = x
h : ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
p : α → Prop
h' : ∀ (u : α), u ∈ supp x → p u
i : PFunctor.B (P F) a
a' : (P F).A
f' : PFunctor.B (P F) a' → α
xeq' : abs { fst := a', snd := f' } = x
⊢ f i ∈ f' '' univ
case mpr.intro.intro.intro.mpr.a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : abs { fst := a, snd := f } = x
h : ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
p : α → Prop
h' : ∀ (u : α), u ∈ supp x → p u
i : PFunctor.B (P F) a
⊢ ∀ (a : (P F).A) (f_1 : PFunctor.B (P F) a → α), abs { fst := a, snd := f_1 } = x → f i ∈ f_1 '' univ
intro a' f' xeq'
case mpr.intro.intro.intro.mpr.a.a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : abs { fst := a, snd := f } = x
h : ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
p : α → Prop
h' : ∀ (u : α), u ∈ supp x → p u
i : PFunctor.B (P F) a
a' : (P F).A
f' : PFunctor.B (P F) a' → α
xeq' : abs { fst := a', snd := f' } = x
⊢ f i ∈ f '' univ
case mpr.intro.intro.intro.mpr.a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : abs { fst := a, snd := f } = x
h : ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
p : α → Prop
h' : ∀ (u : α), u ∈ supp x → p u
i : PFunctor.B (P F) a
a' : (P F).A
f' : PFunctor.B (P F) a' → α
xeq' : abs { fst := a', snd := f' } = x
⊢ f i ∈ f' '' univ
apply h a' f' xeq'
no goals
case mpr.intro.intro.intro.mpr.a.a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : abs { fst := a, snd := f } = x
h : ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
p : α → Prop
h' : ∀ (u : α), u ∈ supp x → p u
i : PFunctor.B (P F) a
a' : (P F).A
f' : PFunctor.B (P F) a' → α
xeq' : abs { fst := a', snd := f' } = x
⊢ f i ∈ f '' univ
apply mem_image_of_mem _ (mem_univ _)
case mp
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ (u : α), u ∈ supp x → p u
⊢ ∃ a f,
    abs { fst := a, snd := f } = x ∧
      ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
case mp
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
⊢ (∀ (p : α → Prop), Liftp p x ↔ ∀ (u : α), u ∈ supp x → p u) →
    ∃ a f,
      abs { fst := a, snd := f } = x ∧
        ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
intro h
case mp
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ (u : α), u ∈ supp x → p u
this : Liftp (supp x) x
⊢ ∃ a f,
    abs { fst := a, snd := f } = x ∧
      ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
case mp
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ (u : α), u ∈ supp x → p u
⊢ ∃ a f,
    abs { fst := a, snd := f } = x ∧
      ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
have : Liftp (supp x) x := by rw [h]; intro u; exact id
case mp
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ (u : α), u ∈ supp x → p u
this✝ : Liftp (supp x) x
this : ∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : PFunctor.B (P F) a), supp x (f i)
⊢ ∃ a f,
    abs { fst := a, snd := f } = x ∧
      ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
case mp
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ (u : α), u ∈ supp x → p u
this : Liftp (supp x) x
⊢ ∃ a f,
    abs { fst := a, snd := f } = x ∧
      ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
rw [liftp_iff] at this
case mp.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ (u : α), u ∈ supp x → p u
this : Liftp (supp x) x
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : PFunctor.B (P F) a), supp x (f i)
⊢ ∃ a f,
    abs { fst := a, snd := f } = x ∧
      ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
case mp
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ (u : α), u ∈ supp x → p u
this✝ : Liftp (supp x) x
this : ∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : PFunctor.B (P F) a), supp x (f i)
⊢ ∃ a f,
    abs { fst := a, snd := f } = x ∧
      ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
rcases this with ⟨a, f, xeq, h'⟩
case mp.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ (u : α), u ∈ supp x → p u
this : Liftp (supp x) x
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : PFunctor.B (P F) a), supp x (f i)
⊢ ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
case mp.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ (u : α), u ∈ supp x → p u
this : Liftp (supp x) x
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : PFunctor.B (P F) a), supp x (f i)
⊢ ∃ a f,
    abs { fst := a, snd := f } = x ∧
      ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
refine' ⟨a, f, xeq.symm, _⟩
case mp.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ (u : α), u ∈ supp x → p u
this : Liftp (supp x) x
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : PFunctor.B (P F) a), supp x (f i)
a' : (P F).A
f' : PFunctor.B (P F) a' → α
h'' : abs { fst := a', snd := f' } = x
⊢ f '' univ ⊆ f' '' univ
case mp.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ (u : α), u ∈ supp x → p u
this : Liftp (supp x) x
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : PFunctor.B (P F) a), supp x (f i)
⊢ ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
intro a' f' h''
case mp.intro.intro.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ (u : α), u ∈ supp x → p u
this : Liftp (supp x) x
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : PFunctor.B (P F) a), supp x (f i)
a' : (P F).A
f' : PFunctor.B (P F) a' → α
h'' : abs { fst := a', snd := f' } = x
u : α
i : PFunctor.B (P F) a
left✝ : i ∈ univ
hfi : f i = u
⊢ u ∈ f' '' univ
case mp.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ (u : α), u ∈ supp x → p u
this : Liftp (supp x) x
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : PFunctor.B (P F) a), supp x (f i)
a' : (P F).A
f' : PFunctor.B (P F) a' → α
h'' : abs { fst := a', snd := f' } = x
⊢ f '' univ ⊆ f' '' univ
rintro u ⟨i, _, hfi⟩
case mp.intro.intro.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ (u : α), u ∈ supp x → p u
this✝ : Liftp (supp x) x
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : PFunctor.B (P F) a), supp x (f i)
a' : (P F).A
f' : PFunctor.B (P F) a' → α
h'' : abs { fst := a', snd := f' } = x
u : α
i : PFunctor.B (P F) a
left✝ : i ∈ univ
hfi : f i = u
this : u ∈ supp x
⊢ u ∈ f' '' univ
case mp.intro.intro.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ (u : α), u ∈ supp x → p u
this : Liftp (supp x) x
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : PFunctor.B (P F) a), supp x (f i)
a' : (P F).A
f' : PFunctor.B (P F) a' → α
h'' : abs { fst := a', snd := f' } = x
u : α
i : PFunctor.B (P F) a
left✝ : i ∈ univ
hfi : f i = u
⊢ u ∈ f' '' univ
have : u ∈ supp x := by rw [← hfi]; apply h'
no goals
case mp.intro.intro.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ (u : α), u ∈ supp x → p u
this✝ : Liftp (supp x) x
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : PFunctor.B (P F) a), supp x (f i)
a' : (P F).A
f' : PFunctor.B (P F) a' → α
h'' : abs { fst := a', snd := f' } = x
u : α
i : PFunctor.B (P F) a
left✝ : i ∈ univ
hfi : f i = u
this : u ∈ supp x
⊢ u ∈ f' '' univ
exact (mem_supp x u).mp this _ _ h''
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ (u : α), u ∈ supp x → p u
⊢ ∀ (u : α), u ∈ supp x → supp x u
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ (u : α), u ∈ supp x → p u
⊢ Liftp (supp x) x
rw [h]
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ (u : α), u ∈ supp x → p u
u : α
⊢ u ∈ supp x → supp x u
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ (u : α), u ∈ supp x → p u
⊢ ∀ (u : α), u ∈ supp x → supp x u
intro u
no goals
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ (u : α), u ∈ supp x → p u
u : α
⊢ u ∈ supp x → supp x u
exact id
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ (u : α), u ∈ supp x → p u
this : Liftp (supp x) x
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : PFunctor.B (P F) a), supp x (f i)
a' : (P F).A
f' : PFunctor.B (P F) a' → α
h'' : abs { fst := a', snd := f' } = x
u : α
i : PFunctor.B (P F) a
left✝ : i ∈ univ
hfi : f i = u
⊢ f i ∈ supp x
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ (u : α), u ∈ supp x → p u
this : Liftp (supp x) x
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : PFunctor.B (P F) a), supp x (f i)
a' : (P F).A
f' : PFunctor.B (P F) a' → α
h'' : abs { fst := a', snd := f' } = x
u : α
i : PFunctor.B (P F) a
left✝ : i ∈ univ
hfi : f i = u
⊢ u ∈ supp x
rw [← hfi]
no goals
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ (u : α), u ∈ supp x → p u
this : Liftp (supp x) x
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : PFunctor.B (P F) a), supp x (f i)
a' : (P F).A
f' : PFunctor.B (P F) a' → α
h'' : abs { fst := a', snd := f' } = x
u : α
i : PFunctor.B (P F) a
left✝ : i ∈ univ
hfi : f i = u
⊢ f i ∈ supp x
apply h'
case mpr.intro.intro.intro.mp.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : abs { fst := a, snd := f } = x
h : ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ 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)
u : α
usuppx : u ∈ supp x
⊢ p u
case mpr.intro.intro.intro.mp
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : abs { fst := a, snd := f } = x
h : ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ f' '' univ
p : α → Prop
⊢ (∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : PFunctor.B (P F) a), p (f i)) → ∀ (u : α), u ∈ supp x → p u
rintro ⟨a', f', xeq', h'⟩ u usuppx
case mpr.intro.intro.intro.mp.intro.intro.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : abs { fst := a, snd := f } = x
h : ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ 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)
u : α
usuppx : u ∈ supp x
i : PFunctor.B (P F) a'
left✝ : i ∈ univ
f'ieq : f' i = u
⊢ p u
case mpr.intro.intro.intro.mp.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : abs { fst := a, snd := f } = x
h : ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ 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)
u : α
usuppx : u ∈ supp x
⊢ p u
rcases (mem_supp x u).mp usuppx a' f' xeq'.symm with ⟨i, _, f'ieq⟩
case mpr.intro.intro.intro.mp.intro.intro.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : abs { fst := a, snd := f } = x
h : ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ 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)
u : α
usuppx : u ∈ supp x
i : PFunctor.B (P F) a'
left✝ : i ∈ univ
f'ieq : f' i = u
⊢ p (f' i)
case mpr.intro.intro.intro.mp.intro.intro.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : abs { fst := a, snd := f } = x
h : ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ 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)
u : α
usuppx : u ∈ supp x
i : PFunctor.B (P F) a'
left✝ : i ∈ univ
f'ieq : f' i = u
⊢ p u
rw [← f'ieq]
no goals
case mpr.intro.intro.intro.mp.intro.intro.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
xeq : abs { fst := a, snd := f } = x
h : ∀ (a' : (P F).A) (f' : PFunctor.B (P F) a' → α), abs { fst := a', snd := f' } = x → f '' univ ⊆ 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)
u : α
usuppx : u ∈ supp x
i : PFunctor.B (P F) a'
left✝ : i ∈ univ
f'ieq : f' i = u
⊢ p (f' i)
apply h'