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

case mpr
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
⊢ IsUniform → SuppPreservation
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
⊢ SuppPreservation ↔ IsUniform
constructor
case mp
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : SuppPreservation
α : Type u
a a' : (P F).A
f : PFunctor.B (P F) a → α
f' : PFunctor.B (P F) a' → α
h' : abs { fst := a, snd := f } = abs { fst := a', snd := f' }
⊢ f '' univ = f' '' univ
case mp
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
⊢ SuppPreservation → IsUniform
intro h α a a' f f' h'
no goals
case mp
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : SuppPreservation
α : Type u
a a' : (P F).A
f : PFunctor.B (P F) a → α
f' : PFunctor.B (P F) a' → α
h' : abs { fst := a, snd := f } = abs { fst := a', snd := f' }
⊢ f '' univ = f' '' univ
rw [← PFunctor.supp_eq, ← PFunctor.supp_eq, ← h, h', h]
case mpr.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : IsUniform
α : 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
⊢ IsUniform → SuppPreservation
rintro h α ⟨a, f⟩
no goals
case mpr.mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : IsUniform
α : Type u
a : (P F).A
f : PFunctor.B (P F) a → α
⊢ supp (abs { fst := a, snd := f }) = supp { fst := a, snd := f }
rwa [supp_eq_of_isUniform, PFunctor.supp_eq]