case h
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 → α
u : α
⊢ u ∈ supp (abs { fst := a, snd := f }) ↔ u ∈ f '' univ
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 }) = f '' univ
ext u
case h
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 → α
u : α
⊢ (∀ (a_1 : (P F).A) (f_1 : PFunctor.B (P F) a_1 → α),
      abs { fst := a_1, snd := f_1 } = abs { fst := a, snd := f } → u ∈ f_1 '' univ) ↔
    u ∈ f '' univ
case h
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 → α
u : α
⊢ u ∈ supp (abs { fst := a, snd := f }) ↔ u ∈ f '' univ
rw [mem_supp]
case h.mp
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 → α
u : α
⊢ (∀ (a_1 : (P F).A) (f_1 : PFunctor.B (P F) a_1 → α),
      abs { fst := a_1, snd := f_1 } = abs { fst := a, snd := f } → u ∈ f_1 '' univ) →
    u ∈ f '' univ

case h.mpr
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 → α
u : α
⊢ u ∈ f '' univ →
    ∀ (a_2 : (P F).A) (f_1 : PFunctor.B (P F) a_2 → α),
      abs { fst := a_2, snd := f_1 } = abs { fst := a, snd := f } → u ∈ f_1 '' univ
case h
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 → α
u : α
⊢ (∀ (a_1 : (P F).A) (f_1 : PFunctor.B (P F) a_1 → α),
      abs { fst := a_1, snd := f_1 } = abs { fst := a, snd := f } → u ∈ f_1 '' univ) ↔
    u ∈ f '' univ
constructor
case h.mpr
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 → α
u : α
h' : u ∈ f '' univ
a' : (P F).A
f' : PFunctor.B (P F) a' → α
e : abs { fst := a', snd := f' } = abs { fst := a, snd := f }
⊢ u ∈ f' '' univ
case h.mpr
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 → α
u : α
⊢ u ∈ f '' univ →
    ∀ (a_2 : (P F).A) (f_1 : PFunctor.B (P F) a_2 → α),
      abs { fst := a_2, snd := f_1 } = abs { fst := a, snd := f } → u ∈ f_1 '' univ
intro h' a' f' e
case h.mpr
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 → α
u : α
h' : u ∈ f '' univ
a' : (P F).A
f' : PFunctor.B (P F) a' → α
e : abs { fst := a', snd := f' } = abs { fst := a, snd := f }
⊢ u ∈ f '' univ
case h.mpr
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 → α
u : α
h' : u ∈ f '' univ
a' : (P F).A
f' : PFunctor.B (P F) a' → α
e : abs { fst := a', snd := f' } = abs { fst := a, snd := f }
⊢ u ∈ f' '' univ
rw [← h _ _ _ _ e.symm]
no goals
case h.mpr
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 → α
u : α
h' : u ∈ f '' univ
a' : (P F).A
f' : PFunctor.B (P F) a' → α
e : abs { fst := a', snd := f' } = abs { fst := a, snd := f }
⊢ u ∈ f '' univ
apply h'
case h.mp
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 → α
u : α
h' :
  ∀ (a_1 : (P F).A) (f_1 : PFunctor.B (P F) a_1 → α),
    abs { fst := a_1, snd := f_1 } = abs { fst := a, snd := f } → u ∈ f_1 '' univ
⊢ u ∈ f '' univ
case h.mp
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 → α
u : α
⊢ (∀ (a_1 : (P F).A) (f_1 : PFunctor.B (P F) a_1 → α),
      abs { fst := a_1, snd := f_1 } = abs { fst := a, snd := f } → u ∈ f_1 '' univ) →
    u ∈ f '' univ
intro h'
no goals
case h.mp
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 → α
u : α
h' :
  ∀ (a_1 : (P F).A) (f_1 : PFunctor.B (P F) a_1 → α),
    abs { fst := a_1, snd := f_1 } = abs { fst := a, snd := f } → u ∈ f_1 '' univ
⊢ u ∈ f '' univ
apply h' _ _ rfl