case h
P : PFunctor
α : Type u
a : P.A
f : B P a → α
x : α
⊢ x ∈ supp { fst := a, snd := f } ↔ x ∈ f '' univ
P : PFunctor
α : Type u
a : P.A
f : B P a → α
⊢ supp { fst := a, snd := f } = f '' univ
ext x
case h
P : PFunctor
α : Type u
a : P.A
f : B P a → α
x : α
⊢ (∀ ⦃p : α → Prop⦄, Liftp p { fst := a, snd := f } → p x) ↔ ∃ y, f y = x
case h
P : PFunctor
α : Type u
a : P.A
f : B P a → α
x : α
⊢ x ∈ supp { fst := a, snd := f } ↔ x ∈ f '' univ
simp only [supp, image_univ, mem_range, mem_setOf_eq]
case h.mp
P : PFunctor
α : Type u
a : P.A
f : B P a → α
x : α
h : ∀ ⦃p : α → Prop⦄, Liftp p { fst := a, snd := f } → p x
⊢ ∃ y, f y = x

case h.mpr
P : PFunctor
α : Type u
a : P.A
f : B P a → α
x : α
h : ∃ y, f y = x
⊢ ∀ ⦃p : α → Prop⦄, Liftp p { fst := a, snd := f } → p x
case h
P : PFunctor
α : Type u
a : P.A
f : B P a → α
x : α
⊢ (∀ ⦃p : α → Prop⦄, Liftp p { fst := a, snd := f } → p x) ↔ ∃ y, f y = x
constructor <;> intro h
case h.mp
P : PFunctor
α : Type u
a : P.A
f : B P a → α
x : α
h : ∀ ⦃p : α → Prop⦄, Liftp p { fst := a, snd := f } → p x
⊢ Liftp (fun x => ∃ y, f y = x) { fst := a, snd := f }
case h.mp
P : PFunctor
α : Type u
a : P.A
f : B P a → α
x : α
h : ∀ ⦃p : α → Prop⦄, Liftp p { fst := a, snd := f } → p x
⊢ ∃ y, f y = x
apply @h fun x => ∃ y : P.B a, f y = x
case h.mp
P : PFunctor
α : Type u
a : P.A
f : B P a → α
x : α
h : ∀ ⦃p : α → Prop⦄, Liftp p { fst := a, snd := f } → p x
⊢ ∀ (i : B P a), ∃ y, f y = f i
case h.mp
P : PFunctor
α : Type u
a : P.A
f : B P a → α
x : α
h : ∀ ⦃p : α → Prop⦄, Liftp p { fst := a, snd := f } → p x
⊢ Liftp (fun x => ∃ y, f y = x) { fst := a, snd := f }
rw [liftp_iff']
case h.mp
P : PFunctor
α : Type u
a : P.A
f : B P a → α
x : α
h : ∀ ⦃p : α → Prop⦄, Liftp p { fst := a, snd := f } → p x
i✝ : B P a
⊢ ∃ y, f y = f i✝
case h.mp
P : PFunctor
α : Type u
a : P.A
f : B P a → α
x : α
h : ∀ ⦃p : α → Prop⦄, Liftp p { fst := a, snd := f } → p x
⊢ ∀ (i : B P a), ∃ y, f y = f i
intro
no goals
case h.mp
P : PFunctor
α : Type u
a : P.A
f : B P a → α
x : α
h : ∀ ⦃p : α → Prop⦄, Liftp p { fst := a, snd := f } → p x
i✝ : B P a
⊢ ∃ y, f y = f i✝
refine' ⟨_, rfl⟩
case h.mpr
P : PFunctor
α : Type u
a : P.A
f : B P a → α
x : α
h : ∃ y, f y = x
⊢ ∀ ⦃p : α → Prop⦄, (∀ (i : B P a), p (f i)) → p x
case h.mpr
P : PFunctor
α : Type u
a : P.A
f : B P a → α
x : α
h : ∃ y, f y = x
⊢ ∀ ⦃p : α → Prop⦄, Liftp p { fst := a, snd := f } → p x
simp only [liftp_iff']
case h.mpr.intro
P : PFunctor
α : Type u
a : P.A
f : B P a → α
x : α
w✝ : B P a
h✝ : f w✝ = x
⊢ ∀ ⦃p : α → Prop⦄, (∀ (i : B P a), p (f i)) → p x
case h.mpr
P : PFunctor
α : Type u
a : P.A
f : B P a → α
x : α
h : ∃ y, f y = x
⊢ ∀ ⦃p : α → Prop⦄, (∀ (i : B P a), p (f i)) → p x
cases h
case h.mpr.intro
P : PFunctor
α : Type u
a : P.A
f : B P a → α
w✝ : B P a
⊢ ∀ ⦃p : α → Prop⦄, (∀ (i : B P a), p (f i)) → p (f w✝)
case h.mpr.intro
P : PFunctor
α : Type u
a : P.A
f : B P a → α
x : α
w✝ : B P a
h✝ : f w✝ = x
⊢ ∀ ⦃p : α → Prop⦄, (∀ (i : B P a), p (f i)) → p x
subst x
no goals
case h.mpr.intro
P : PFunctor
α : Type u
a : P.A
f : B P a → α
w✝ : B P a
⊢ ∀ ⦃p : α → Prop⦄, (∀ (i : B P a), p (f i)) → p (f w✝)
tauto