n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
x : F α
p : (i : Fin2 n) → α i → Prop
⊢ (∃ a f, abs (repr x) = abs { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p i (f i j)) ↔
    ∀ (i : Fin2 n) (u : α i), u ∈ supp (abs (repr x)) i → p i u
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
x : F α
p : (i : Fin2 n) → α i → Prop
⊢ LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
rw [liftP_iff, ← abs_repr x]
case mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
⊢ (∃ a_1 f_1,
      abs { fst := a, snd := f } = abs { fst := a_1, snd := f_1 } ∧
        ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a_1 i), p i (f_1 i j)) ↔
    ∀ (i : Fin2 n) (u : α i), u ∈ supp (abs { fst := a, snd := f }) i → p i u
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
x : F α
p : (i : Fin2 n) → α i → Prop
⊢ (∃ a f, abs (repr x) = abs { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p i (f i j)) ↔
    ∀ (i : Fin2 n) (u : α i), u ∈ supp (abs (repr x)) i → p i u
cases' repr x with a f
case mk.mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
h : IsUniform
α : TypeVec n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
⊢ (∃ a_1 f_1,
      abs { fst := a, snd := f } = abs { fst := a_1, snd := f_1 } ∧
        ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a_1 i), p i (f_1 i j)) →
    ∀ (i : Fin2 n) (u : α i), u ∈ supp (abs { fst := a, snd := f }) i → p i u

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