case mp
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : SuppPreservation
⊢ LiftpPreservation

case mpr
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : LiftpPreservation
⊢ SuppPreservation
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
⊢ SuppPreservation ↔ LiftpPreservation
constructor <;> intro h
case mp.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : SuppPreservation
α : Type u
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
⊢ Liftp p (abs { fst := a, snd := f }) ↔ Liftp p { fst := a, snd := f }
case mp
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : SuppPreservation
⊢ LiftpPreservation
rintro α p ⟨a, f⟩
case mp.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : SuppPreservation
α : Type u
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
h' : SuppPreservation
⊢ Liftp p (abs { fst := a, snd := f }) ↔ Liftp p { fst := a, snd := f }
case mp.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : SuppPreservation
α : Type u
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
⊢ Liftp p (abs { fst := a, snd := f }) ↔ Liftp p { fst := a, snd := f }
have h' := h
case mp.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : SuppPreservation
α : Type u
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
h' : IsUniform
⊢ Liftp p (abs { fst := a, snd := f }) ↔ Liftp p { fst := a, snd := f }
case mp.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : SuppPreservation
α : Type u
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
h' : SuppPreservation
⊢ Liftp p (abs { fst := a, snd := f }) ↔ Liftp p { fst := a, snd := f }
rw [suppPreservation_iff_uniform] at h'
case mp.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h :
  ∀ ⦃α : Type u⦄ (x : PFunctor.Obj (P F) α),
    {y | ∀ ⦃p : α → Prop⦄, Liftp p (abs x) → p y} = {y | ∀ ⦃p : α → Prop⦄, Liftp p x → p y}
α : Type u
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
h' : IsUniform
⊢ Liftp p (abs { fst := a, snd := f }) ↔ Liftp p { fst := a, snd := f }
case mp.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : SuppPreservation
α : Type u
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
h' : IsUniform
⊢ Liftp p (abs { fst := a, snd := f }) ↔ Liftp p { fst := a, snd := f }
dsimp only [SuppPreservation, supp] at h
case mp.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h :
  ∀ ⦃α : Type u⦄ (x : PFunctor.Obj (P F) α),
    {y | ∀ ⦃p : α → Prop⦄, Liftp p (abs x) → p y} = {y | ∀ ⦃p : α → Prop⦄, Liftp p x → p y}
α : Type u
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
h' : IsUniform
⊢ (∀ (u : α), u ∈ f '' univ → p u) ↔ ∀ (i : PFunctor.B (P F) a), p (f i)
case mp.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h :
  ∀ ⦃α : Type u⦄ (x : PFunctor.Obj (P F) α),
    {y | ∀ ⦃p : α → Prop⦄, Liftp p (abs x) → p y} = {y | ∀ ⦃p : α → Prop⦄, Liftp p x → p y}
α : Type u
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
h' : IsUniform
⊢ Liftp p (abs { fst := a, snd := f }) ↔ Liftp p { fst := a, snd := f }
rw [liftp_iff_of_isUniform h', supp_eq_of_isUniform h', PFunctor.liftp_iff']
case mp.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h :
  ∀ ⦃α : Type u⦄ (x : PFunctor.Obj (P F) α),
    {y | ∀ ⦃p : α → Prop⦄, Liftp p (abs x) → p y} = {y | ∀ ⦃p : α → Prop⦄, Liftp p x → p y}
α : Type u
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
h' : IsUniform
⊢ (∀ (u : α) (x : PFunctor.B (P F) a), f x = u → p u) ↔ ∀ (i : PFunctor.B (P F) a), p (f i)
case mp.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h :
  ∀ ⦃α : Type u⦄ (x : PFunctor.Obj (P F) α),
    {y | ∀ ⦃p : α → Prop⦄, Liftp p (abs x) → p y} = {y | ∀ ⦃p : α → Prop⦄, Liftp p x → p y}
α : Type u
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
h' : IsUniform
⊢ (∀ (u : α), u ∈ f '' univ → p u) ↔ ∀ (i : PFunctor.B (P F) a), p (f i)
simp only [image_univ, mem_range, exists_imp]
no goals
case mp.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h :
  ∀ ⦃α : Type u⦄ (x : PFunctor.Obj (P F) α),
    {y | ∀ ⦃p : α → Prop⦄, Liftp p (abs x) → p y} = {y | ∀ ⦃p : α → Prop⦄, Liftp p x → p y}
α : Type u
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
h' : IsUniform
⊢ (∀ (u : α) (x : PFunctor.B (P F) a), f x = u → p u) ↔ ∀ (i : PFunctor.B (P F) a), p (f i)
constructor <;> intros <;> subst_vars <;> solve_by_elim
case mpr.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : LiftpPreservation
α : Type u
a : (P F).A
f : PFunctor.B (P F) a → α
⊢ supp (abs { fst := a, snd := f }) = supp { fst := a, snd := f }
case mpr
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : LiftpPreservation
⊢ SuppPreservation
rintro α ⟨a, f⟩
case mpr.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : ∀ ⦃α : Type u⦄ (p : α → Prop) (x : PFunctor.Obj (P F) α), Liftp p (abs x) ↔ Liftp p x
α : Type u
a : (P F).A
f : PFunctor.B (P F) a → α
⊢ supp (abs { fst := a, snd := f }) = supp { fst := a, snd := f }
case mpr.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : LiftpPreservation
α : Type u
a : (P F).A
f : PFunctor.B (P F) a → α
⊢ supp (abs { fst := a, snd := f }) = supp { fst := a, snd := f }
simp only [LiftpPreservation] at h
no goals
case mpr.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : ∀ ⦃α : Type u⦄ (p : α → Prop) (x : PFunctor.Obj (P F) α), Liftp p (abs x) ↔ Liftp p x
α : Type u
a : (P F).A
f : PFunctor.B (P F) a → α
⊢ supp (abs { fst := a, snd := f }) = supp { fst := a, snd := f }
simp only [supp, h]