F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : IsUniform
α : Type u
x : F α
p : α → Prop
⊢ (∃ a f, abs (repr x) = abs { fst := a, snd := f } ∧ ∀ (i : PFunctor.B (P F) a), p (f i)) ↔
    ∀ (u : α), u ∈ supp (abs (repr x)) → p u
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : IsUniform
α : Type u
x : F α
p : α → Prop
⊢ Liftp p x ↔ ∀ (u : α), u ∈ supp x → p u
rw [liftp_iff, ← abs_repr x]
case mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
⊢ (∃ a_1 f_1, abs { fst := a, snd := f } = abs { fst := a_1, snd := f_1 } ∧ ∀ (i : PFunctor.B (P F) a_1), p (f_1 i)) ↔
    ∀ (u : α), u ∈ supp (abs { fst := a, snd := f }) → p u
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : IsUniform
α : Type u
x : F α
p : α → Prop
⊢ (∃ a f, abs (repr x) = abs { fst := a, snd := f } ∧ ∀ (i : PFunctor.B (P F) a), p (f i)) ↔
    ∀ (u : α), u ∈ supp (abs (repr x)) → p u
cases' repr x with a f
case mk.mp
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
⊢ (∃ a_1 f_1, abs { fst := a, snd := f } = abs { fst := a_1, snd := f_1 } ∧ ∀ (i : PFunctor.B (P F) a_1), p (f_1 i)) →
    ∀ (u : α), u ∈ supp (abs { fst := a, snd := f }) → p u

case mk.mpr
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
⊢ (∀ (u : α), u ∈ supp (abs { fst := a, snd := f }) → p u) →
    ∃ a_2 f_1, abs { fst := a, snd := f } = abs { fst := a_2, snd := f_1 } ∧ ∀ (i : PFunctor.B (P F) a_2), p (f_1 i)
case mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
⊢ (∃ a_1 f_1, abs { fst := a, snd := f } = abs { fst := a_1, snd := f_1 } ∧ ∀ (i : PFunctor.B (P F) a_1), p (f_1 i)) ↔
    ∀ (u : α), u ∈ supp (abs { fst := a, snd := f }) → p u
constructor
case mk.mpr
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
h' : ∀ (u : α), u ∈ supp (abs { fst := a, snd := f }) → p u
⊢ ∃ a_1 f_1, abs { fst := a, snd := f } = abs { fst := a_1, snd := f_1 } ∧ ∀ (i : PFunctor.B (P F) a_1), p (f_1 i)
case mk.mpr
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
⊢ (∀ (u : α), u ∈ supp (abs { fst := a, snd := f }) → p u) →
    ∃ a_2 f_1, abs { fst := a, snd := f } = abs { fst := a_2, snd := f_1 } ∧ ∀ (i : PFunctor.B (P F) a_2), p (f_1 i)
intro h'
case mk.mpr
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
h' : ∀ (u : α), u ∈ supp (abs { fst := a, snd := f }) → p u
i : PFunctor.B (P F) a
⊢ f i ∈ supp (abs { fst := a, snd := f })
case mk.mpr
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
h' : ∀ (u : α), u ∈ supp (abs { fst := a, snd := f }) → p u
⊢ ∃ a_1 f_1, abs { fst := a, snd := f } = abs { fst := a_1, snd := f_1 } ∧ ∀ (i : PFunctor.B (P F) a_1), p (f_1 i)
refine' ⟨a, f, rfl, fun i => h' _ _⟩
case mk.mpr
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
h' : ∀ (u : α), u ∈ supp (abs { fst := a, snd := f }) → p u
i : PFunctor.B (P F) a
⊢ f i ∈ f '' univ
case mk.mpr
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
h' : ∀ (u : α), u ∈ supp (abs { fst := a, snd := f }) → p u
i : PFunctor.B (P F) a
⊢ f i ∈ supp (abs { fst := a, snd := f })
rw [supp_eq_of_isUniform h]
no goals
case mk.mpr
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
h' : ∀ (u : α), u ∈ supp (abs { fst := a, snd := f }) → p u
i : PFunctor.B (P F) a
⊢ f i ∈ f '' univ
exact ⟨i, mem_univ i, rfl⟩
case mk.mp.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
a' : (P F).A
f' : PFunctor.B (P F) a' → α
abseq : abs { fst := a, snd := f } = abs { fst := a', snd := f' }
hf : ∀ (i : PFunctor.B (P F) a'), p (f' i)
u : α
⊢ u ∈ supp (abs { fst := a, snd := f }) → p u
case mk.mp
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
⊢ (∃ a_1 f_1, abs { fst := a, snd := f } = abs { fst := a_1, snd := f_1 } ∧ ∀ (i : PFunctor.B (P F) a_1), p (f_1 i)) →
    ∀ (u : α), u ∈ supp (abs { fst := a, snd := f }) → p u
rintro ⟨a', f', abseq, hf⟩ u
case mk.mp.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
a' : (P F).A
f' : PFunctor.B (P F) a' → α
abseq : abs { fst := a, snd := f } = abs { fst := a', snd := f' }
hf : ∀ (i : PFunctor.B (P F) a'), p (f' i)
u : α
⊢ u ∈ f' '' univ → p u
case mk.mp.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
a' : (P F).A
f' : PFunctor.B (P F) a' → α
abseq : abs { fst := a, snd := f } = abs { fst := a', snd := f' }
hf : ∀ (i : PFunctor.B (P F) a'), p (f' i)
u : α
⊢ u ∈ supp (abs { fst := a, snd := f }) → p u
rw [supp_eq_of_isUniform h, h _ _ _ _ abseq]
case mk.mp.intro.intro.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
a' : (P F).A
f' : PFunctor.B (P F) a' → α
abseq : abs { fst := a, snd := f } = abs { fst := a', snd := f' }
hf : ∀ (i : PFunctor.B (P F) a'), p (f' i)
u : α
i : PFunctor.B (P F) a'
left✝ : i ∈ univ
hi : f' i = u
⊢ p u
case mk.mp.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
a' : (P F).A
f' : PFunctor.B (P F) a' → α
abseq : abs { fst := a, snd := f } = abs { fst := a', snd := f' }
hf : ∀ (i : PFunctor.B (P F) a'), p (f' i)
u : α
⊢ u ∈ f' '' univ → p u
rintro ⟨i, _, hi⟩
case mk.mp.intro.intro.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
a' : (P F).A
f' : PFunctor.B (P F) a' → α
abseq : abs { fst := a, snd := f } = abs { fst := a', snd := f' }
hf : ∀ (i : PFunctor.B (P F) a'), p (f' i)
u : α
i : PFunctor.B (P F) a'
left✝ : i ∈ univ
hi : f' i = u
⊢ p (f' i)
case mk.mp.intro.intro.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
a' : (P F).A
f' : PFunctor.B (P F) a' → α
abseq : abs { fst := a, snd := f } = abs { fst := a', snd := f' }
hf : ∀ (i : PFunctor.B (P F) a'), p (f' i)
u : α
i : PFunctor.B (P F) a'
left✝ : i ∈ univ
hi : f' i = u
⊢ p u
rw [← hi]
no goals
case mk.mp.intro.intro.intro.intro.intro
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : PFunctor.B (P F) a → α
a' : (P F).A
f' : PFunctor.B (P F) a' → α
abseq : abs { fst := a, snd := f } = abs { fst := a', snd := f' }
hf : ∀ (i : PFunctor.B (P F) a'), p (f' i)
u : α
i : PFunctor.B (P F) a'
left✝ : i ∈ univ
hi : f' i = u
⊢ p (f' i)
apply hf