n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
⊢ u ∈ {y | ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i y} ↔
    ∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i '' univ
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
⊢ u ∈ supp x i ↔ ∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i '' univ
rw [supp]
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
⊢ (∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u) ↔
    ∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i '' univ
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
⊢ u ∈ {y | ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i y} ↔
    ∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i '' univ
dsimp
case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
⊢ (∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u) →
    ∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i '' univ

case mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
⊢ (∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i '' univ) →
    ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
⊢ (∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u) ↔
    ∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i '' univ
constructor
case mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
h : ∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i '' univ
p : (i : Fin2 n) → α i → Prop
⊢ LiftP p x → p i u
case mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
⊢ (∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i '' univ) →
    ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u
intro h p
case mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
h : ∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i '' univ
p : (i : Fin2 n) → α i → Prop
⊢ (∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p i (f i j)) → p i u
case mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
h : ∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i '' univ
p : (i : Fin2 n) → α i → Prop
⊢ LiftP p x → p i u
rw [liftP_iff]
case mpr.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
h : ∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i '' univ
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => α i
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p i (f i j)
⊢ p i u
case mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
h : ∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i '' univ
p : (i : Fin2 n) → α i → Prop
⊢ (∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p i (f i j)) → p i u
rintro ⟨a, f, xeq, h'⟩
case mpr.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i✝ : Fin2 n
u : α i✝
h : ∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i✝ '' univ
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => α i
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p i (f i j)
i : MvPFunctor.B (P F) a i✝
left✝ : i ∈ univ
hi : f i✝ i = u
⊢ p i✝ u
case mpr.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
h : ∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i '' univ
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => α i
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p i (f i j)
⊢ p i u
rcases h a f xeq.symm with ⟨i, _, hi⟩
case mpr.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i✝ : Fin2 n
u : α i✝
h : ∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i✝ '' univ
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => α i
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p i (f i j)
i : MvPFunctor.B (P F) a i✝
left✝ : i ∈ univ
hi : f i✝ i = u
⊢ p i✝ (f i✝ i)
case mpr.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i✝ : Fin2 n
u : α i✝
h : ∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i✝ '' univ
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => α i
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p i (f i j)
i : MvPFunctor.B (P F) a i✝
left✝ : i ∈ univ
hi : f i✝ i = u
⊢ p i✝ u
rw [← hi]
no goals
case mpr.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i✝ : Fin2 n
u : α i✝
h : ∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i✝ '' univ
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => α i
xeq : x = abs { fst := a, snd := f }
h' : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p i (f i j)
i : MvPFunctor.B (P F) a i✝
left✝ : i ∈ univ
hi : f i✝ i = u
⊢ p i✝ (f i✝ i)
apply h'
case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
haf : abs { fst := a, snd := f } = x
⊢ u ∈ f i '' univ
case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
⊢ (∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u) →
    ∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i '' univ
intro h a f haf
case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
haf : abs { fst := a, snd := f } = x
this : LiftP (fun i u => u ∈ f i '' univ) x
⊢ u ∈ f i '' univ
case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
haf : abs { fst := a, snd := f } = x
⊢ u ∈ f i '' univ
have : LiftP (fun i u => u ∈ f i '' univ) x := by
  rw [liftP_iff]
  refine' ⟨a, f, haf.symm, _⟩
  intro i u
  exact mem_image_of_mem _ (mem_univ _)
no goals
case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
haf : abs { fst := a, snd := f } = x
this : LiftP (fun i u => u ∈ f i '' univ) x
⊢ u ∈ f i '' univ
exact h this
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
haf : abs { fst := a, snd := f } = x
⊢ ∃ a_1 f_1, x = abs { fst := a_1, snd := f_1 } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a_1 i), f_1 i j ∈ f i '' univ
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
haf : abs { fst := a, snd := f } = x
⊢ LiftP (fun i u => u ∈ f i '' univ) x
rw [liftP_iff]
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
haf : abs { fst := a, snd := f } = x
⊢ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), f i j ∈ f i '' univ
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
haf : abs { fst := a, snd := f } = x
⊢ ∃ a_1 f_1, x = abs { fst := a_1, snd := f_1 } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a_1 i), f_1 i j ∈ f i '' univ
refine' ⟨a, f, haf.symm, _⟩
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i✝ : Fin2 n
u✝ : α i✝
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i✝ u✝
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
haf : abs { fst := a, snd := f } = x
i : Fin2 n
u : MvPFunctor.B (P F) a i
⊢ f i u ∈ f i '' univ
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i : Fin2 n
u : α i
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
haf : abs { fst := a, snd := f } = x
⊢ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), f i j ∈ f i '' univ
intro i u
no goals
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
i✝ : Fin2 n
u✝ : α i✝
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i✝ u✝
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
haf : abs { fst := a, snd := f } = x
i : Fin2 n
u : MvPFunctor.B (P F) a i
⊢ f i u ∈ f i '' univ
exact mem_image_of_mem _ (mem_univ _)