case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : 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) →
    ∃ a f,
      abs { fst := a, snd := f } = x ∧
        ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
          abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ

case mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
⊢ (∃ a f,
      abs { fst := a, snd := f } = x ∧
        ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
          abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ) →
    ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : 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) ↔
    ∃ a f,
      abs { fst := a, snd := f } = x ∧
        ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
          abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
constructor
case mpr.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
⊢ LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
case mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
⊢ (∃ a f,
      abs { fst := a, snd := f } = x ∧
        ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
          abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ) →
    ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
rintro ⟨a, f, xeq, h⟩ p
case mpr.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ 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)) ↔
    ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → 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 α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
⊢ LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
rw [liftP_iff]
case mpr.intro.intro.intro.mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ 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)) →
    ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u

case mpr.intro.intro.intro.mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
⊢ (∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u) →
    ∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p i (f i j)
case mpr.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ 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)) ↔
    ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
constructor
case mpr.intro.intro.intro.mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
h' : ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
⊢ ∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p i (f i j)
case mpr.intro.intro.intro.mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
⊢ (∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u) →
    ∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p i (f i j)
intro h'
case mpr.intro.intro.intro.mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
h' : ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
⊢ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p i (f i j)
case mpr.intro.intro.intro.mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
h' : ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
⊢ ∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p i (f i j)
refine' ⟨a, f, xeq.symm, _⟩
case mpr.intro.intro.intro.mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
h' : ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
j : Fin2 n
y : MvPFunctor.B (P F) a j
⊢ p j (f j y)
case mpr.intro.intro.intro.mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
h' : ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
⊢ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p i (f i j)
intro j y
case mpr.intro.intro.intro.mpr.a
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
h' : ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
j : Fin2 n
y : MvPFunctor.B (P F) a j
⊢ f j y ∈ supp x j
case mpr.intro.intro.intro.mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
h' : ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
j : Fin2 n
y : MvPFunctor.B (P F) a j
⊢ p j (f j y)
apply h'
case mpr.intro.intro.intro.mpr.a
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
h' : ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
j : Fin2 n
y : MvPFunctor.B (P F) a j
⊢ ∀ (a : (P F).A) (f_1 : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f_1 } = x → f j y ∈ f_1 j '' univ
case mpr.intro.intro.intro.mpr.a
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
h' : ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
j : Fin2 n
y : MvPFunctor.B (P F) a j
⊢ f j y ∈ supp x j
rw [mem_supp]
case mpr.intro.intro.intro.mpr.a
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
h' : ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
j : Fin2 n
y : MvPFunctor.B (P F) a j
a' : (P F).A
f' : MvPFunctor.B (P F) a' ⟹ α
xeq' : abs { fst := a', snd := f' } = x
⊢ f j y ∈ f' j '' univ
case mpr.intro.intro.intro.mpr.a
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
h' : ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
j : Fin2 n
y : MvPFunctor.B (P F) a j
⊢ ∀ (a : (P F).A) (f_1 : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f_1 } = x → f j y ∈ f_1 j '' univ
intro a' f' xeq'
case mpr.intro.intro.intro.mpr.a.a
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
h' : ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
j : Fin2 n
y : MvPFunctor.B (P F) a j
a' : (P F).A
f' : MvPFunctor.B (P F) a' ⟹ α
xeq' : abs { fst := a', snd := f' } = x
⊢ f j y ∈ f j '' univ
case mpr.intro.intro.intro.mpr.a
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
h' : ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
j : Fin2 n
y : MvPFunctor.B (P F) a j
a' : (P F).A
f' : MvPFunctor.B (P F) a' ⟹ α
xeq' : abs { fst := a', snd := f' } = x
⊢ f j y ∈ f' j '' univ
apply h _ a' f' xeq'
no goals
case mpr.intro.intro.intro.mpr.a.a
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
h' : ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
j : Fin2 n
y : MvPFunctor.B (P F) a j
a' : (P F).A
f' : MvPFunctor.B (P F) a' ⟹ α
xeq' : abs { fst := a', snd := f' } = x
⊢ f j y ∈ f j '' univ
apply mem_image_of_mem _ (mem_univ _)
case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
⊢ ∃ a f,
    abs { fst := a, snd := f } = x ∧
      ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
        abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : 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) →
    ∃ a f,
      abs { fst := a, snd := f } = x ∧
        ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
          abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
intro h
case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
this : LiftP (supp x) x
⊢ ∃ a f,
    abs { fst := a, snd := f } = x ∧
      ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
        abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
⊢ ∃ a f,
    abs { fst := a, snd := f } = x ∧
      ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
        abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
have : LiftP (supp x) x := by rw [h]; introv; exact id
case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
this✝ : LiftP (supp x) x
this : ∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), supp x i (f i j)
⊢ ∃ a f,
    abs { fst := a, snd := f } = x ∧
      ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
        abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
this : LiftP (supp x) x
⊢ ∃ a f,
    abs { fst := a, snd := f } = x ∧
      ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
        abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
rw [liftP_iff] at this
case mp.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
this : LiftP (supp x) x
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), supp x i (f i j)
⊢ ∃ a f,
    abs { fst := a, snd := f } = x ∧
      ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
        abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
this✝ : LiftP (supp x) x
this : ∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), supp x i (f i j)
⊢ ∃ a f,
    abs { fst := a, snd := f } = x ∧
      ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
        abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
rcases this with ⟨a, f, xeq, h'⟩
case mp.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
this : LiftP (supp x) x
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), supp x i (f i j)
⊢ ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
case mp.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
this : LiftP (supp x) x
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), supp x i (f i j)
⊢ ∃ a f,
    abs { fst := a, snd := f } = x ∧
      ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
        abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
refine' ⟨a, f, xeq.symm, _⟩
case mp.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
this : LiftP (supp x) x
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), supp x i (f i j)
a' : Fin2 n
f' : (P F).A
h'' : MvPFunctor.B (P F) f' ⟹ α
⊢ abs { fst := f', snd := h'' } = x → f a' '' univ ⊆ h'' a' '' univ
case mp.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
this : LiftP (supp x) x
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), supp x i (f i j)
⊢ ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ f' i '' univ
intro a' f' h''
case mp.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
this : LiftP (supp x) x
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), supp x i (f i j)
a' : Fin2 n
f' : (P F).A
h'' : MvPFunctor.B (P F) f' ⟹ α
hu : abs { fst := f', snd := h'' } = x
u : α a'
j : MvPFunctor.B (P F) a a'
_h₂ : j ∈ univ
hfi : f a' j = u
⊢ u ∈ h'' a' '' univ
case mp.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
this : LiftP (supp x) x
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), supp x i (f i j)
a' : Fin2 n
f' : (P F).A
h'' : MvPFunctor.B (P F) f' ⟹ α
⊢ abs { fst := f', snd := h'' } = x → f a' '' univ ⊆ h'' a' '' univ
rintro hu u ⟨j, _h₂, hfi⟩
case mp.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
this : LiftP (supp x) x
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), supp x i (f i j)
a' : Fin2 n
f' : (P F).A
h'' : MvPFunctor.B (P F) f' ⟹ α
hu : abs { fst := f', snd := h'' } = x
u : α a'
j : MvPFunctor.B (P F) a a'
_h₂ : j ∈ univ
hfi : f a' j = u
hh : u ∈ supp x a'
⊢ u ∈ h'' a' '' univ
case mp.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
this : LiftP (supp x) x
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), supp x i (f i j)
a' : Fin2 n
f' : (P F).A
h'' : MvPFunctor.B (P F) f' ⟹ α
hu : abs { fst := f', snd := h'' } = x
u : α a'
j : MvPFunctor.B (P F) a a'
_h₂ : j ∈ univ
hfi : f a' j = u
⊢ u ∈ h'' a' '' univ
have hh : u ∈ supp x a' := by rw [← hfi] ; apply h'
no goals
case mp.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
this : LiftP (supp x) x
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), supp x i (f i j)
a' : Fin2 n
f' : (P F).A
h'' : MvPFunctor.B (P F) f' ⟹ α
hu : abs { fst := f', snd := h'' } = x
u : α a'
j : MvPFunctor.B (P F) a a'
_h₂ : j ∈ univ
hfi : f a' j = u
hh : u ∈ supp x a'
⊢ u ∈ h'' a' '' univ
refine' (mem_supp x _ u).mp hh _ _ hu
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
⊢ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → supp x i u
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
⊢ LiftP (supp x) x
rw [h]
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
i : Fin2 n
u : α i
⊢ u ∈ supp x i → supp x i u
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
⊢ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → supp x i u
introv
no goals
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
i : Fin2 n
u : α i
⊢ u ∈ supp x i → supp x i u
exact id
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
this : LiftP (supp x) x
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), supp x i (f i j)
a' : Fin2 n
f' : (P F).A
h'' : MvPFunctor.B (P F) f' ⟹ α
hu : abs { fst := f', snd := h'' } = x
u : α a'
j : MvPFunctor.B (P F) a a'
_h₂ : j ∈ univ
hfi : f a' j = u
⊢ f a' j ∈ supp x a'
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
this : LiftP (supp x) x
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), supp x i (f i j)
a' : Fin2 n
f' : (P F).A
h'' : MvPFunctor.B (P F) f' ⟹ α
hu : abs { fst := f', snd := h'' } = x
u : α a'
j : MvPFunctor.B (P F) a a'
_h₂ : j ∈ univ
hfi : f a' j = u
⊢ u ∈ supp x a'
rw [← hfi]
no goals
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
this : LiftP (supp x) x
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), supp x i (f i j)
a' : Fin2 n
f' : (P F).A
h'' : MvPFunctor.B (P F) f' ⟹ α
hu : abs { fst := f', snd := h'' } = x
u : α a'
j : MvPFunctor.B (P F) a a'
_h₂ : j ∈ univ
hfi : f a' j = u
⊢ f a' j ∈ supp x a'
apply h'
case mpr.intro.intro.intro.mp.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ 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 : Fin2 n
u : α i
usuppx : u ∈ supp x i
⊢ p i u
case mpr.intro.intro.intro.mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ 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)) →
    ∀ (i : Fin2 n) (u : α i), u ∈ supp x i → p i u
rintro ⟨a', f', xeq', h'⟩ i u usuppx
case mpr.intro.intro.intro.mp.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ 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✝ : Fin2 n
u : α i✝
usuppx : u ∈ supp x i✝
i : MvPFunctor.B (P F) a' i✝
left✝ : i ∈ univ
f'ieq : f' i✝ i = u
⊢ p i✝ u
case mpr.intro.intro.intro.mp.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ 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 : Fin2 n
u : α i
usuppx : u ∈ supp x i
⊢ p i u
rcases(mem_supp x _ u).mp (@usuppx) a' f' xeq'.symm with ⟨i, _, f'ieq⟩
case mpr.intro.intro.intro.mp.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ 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✝ : Fin2 n
u : α i✝
usuppx : u ∈ supp x i✝
i : MvPFunctor.B (P F) a' i✝
left✝ : i ∈ univ
f'ieq : f' i✝ i = u
⊢ p i✝ (f' i✝ i)
case mpr.intro.intro.intro.mp.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ 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✝ : Fin2 n
u : α i✝
usuppx : u ∈ supp x i✝
i : MvPFunctor.B (P F) a' i✝
left✝ : i ∈ univ
f'ieq : f' i✝ i = u
⊢ p i✝ u
rw [← f'ieq]
no goals
case mpr.intro.intro.intro.mp.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
xeq : abs { fst := a, snd := f } = x
h :
  ∀ (i : Fin2 n) (a' : (P F).A) (f' : MvPFunctor.B (P F) a' ⟹ α),
    abs { fst := a', snd := f' } = x → f i '' univ ⊆ 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✝ : Fin2 n
u : α i✝
usuppx : u ∈ supp x i✝
i : MvPFunctor.B (P F) a' i✝
left✝ : i ∈ univ
f'ieq : f' i✝ i = u
⊢ p i✝ (f' i✝ i)
apply h'