case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
⊢ LiftP p x → ∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p (f i j)

case mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
⊢ (∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p (f i j)) → LiftP p x
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
⊢ LiftP p x ↔ ∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p (f i j)
constructor
case mpr.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
h₀ : x = abs { fst := a, snd := f }
h₁ : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p (f i j)
⊢ LiftP p x
case mpr
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
⊢ (∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p (f i j)) → LiftP p x
rintro ⟨a, f, h₀, h₁⟩
case mpr.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
h₀ : x = abs { fst := a, snd := f }
h₁ : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p (f i j)
⊢ LiftP p x
case mpr.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
h₀ : x = abs { fst := a, snd := f }
h₁ : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p (f i j)
⊢ LiftP p x
dsimp at *
case mpr.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
h₀ : x = abs { fst := a, snd := f }
h₁ : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p (f i j)
⊢ (fun i => Subtype.val) <$$> abs { fst := a, snd := fun i j => { val := f i j, property := (_ : p (f i j)) } } = x
case mpr.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
h₀ : x = abs { fst := a, snd := f }
h₁ : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p (f i j)
⊢ LiftP p x
use abs ⟨a, fun i j => ⟨f i j, h₁ i j⟩⟩
case mpr.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
h₀ : x = abs { fst := a, snd := f }
h₁ : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p (f i j)
⊢ abs ((fun i => Subtype.val) <$$> { fst := a, snd := fun i j => { val := f i j, property := (_ : p (f i j)) } }) =
    abs { fst := a, snd := f }
case mpr.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
h₀ : x = abs { fst := a, snd := f }
h₁ : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p (f i j)
⊢ (fun i => Subtype.val) <$$> abs { fst := a, snd := fun i j => { val := f i j, property := (_ : p (f i j)) } } = x
rw [← abs_map, h₀]
no goals
case mpr.intro.intro.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α
h₀ : x = abs { fst := a, snd := f }
h₁ : ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p (f i j)
⊢ abs ((fun i => Subtype.val) <$$> { fst := a, snd := fun i j => { val := f i j, property := (_ : p (f i j)) } }) =
    abs { fst := a, snd := f }
rfl
case mp.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
⊢ ∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p (f i j)
case mp
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
⊢ LiftP p x → ∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p (f i j)
rintro ⟨y, hy⟩
case mp.intro.mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => Subtype p
h : repr y = { fst := a, snd := f }
⊢ ∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p (f i j)
case mp.intro
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
⊢ ∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p (f i j)
cases' h : repr y with a f
case mp.intro.mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => Subtype p
h : repr y = { fst := a, snd := f }
⊢ x = abs { fst := a, snd := fun i j => ↑(f i j) } ∧
    ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p ((fun i j => ↑(f i j)) i j)
case mp.intro.mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => Subtype p
h : repr y = { fst := a, snd := f }
⊢ ∃ a f, x = abs { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p (f i j)
use a, fun i j => (f i j).val
case mp.intro.mk.left
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => Subtype p
h : repr y = { fst := a, snd := f }
⊢ x = abs { fst := a, snd := fun i j => ↑(f i j) }

case mp.intro.mk.right
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => Subtype p
h : repr y = { fst := a, snd := f }
⊢ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p ((fun i j => ↑(f i j)) i j)
case mp.intro.mk
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => Subtype p
h : repr y = { fst := a, snd := f }
⊢ x = abs { fst := a, snd := fun i j => ↑(f i j) } ∧
    ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p ((fun i j => ↑(f i j)) i j)
constructor
case mp.intro.mk.right
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => Subtype p
h : repr y = { fst := a, snd := f }
i : Fin2 n
j : MvPFunctor.B (P F) a i
⊢ p ((fun i j => ↑(f i j)) i j)
case mp.intro.mk.right
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => Subtype p
h : repr y = { fst := a, snd := f }
⊢ ∀ (i : Fin2 n) (j : MvPFunctor.B (P F) a i), p ((fun i j => ↑(f i j)) i j)
intro i j
no goals
case mp.intro.mk.right
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => Subtype p
h : repr y = { fst := a, snd := f }
i : Fin2 n
j : MvPFunctor.B (P F) a i
⊢ p ((fun i j => ↑(f i j)) i j)
apply (f i j).property
case mp.intro.mk.left
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => Subtype p
h : repr y = { fst := a, snd := f }
⊢ abs ((fun i => Subtype.val) <$$> { fst := a, snd := f }) = abs { fst := a, snd := fun i j => ↑(f i j) }
case mp.intro.mk.left
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => Subtype p
h : repr y = { fst := a, snd := f }
⊢ x = abs { fst := a, snd := fun i j => ↑(f i j) }
rw [← hy, ← abs_repr y, h, ← abs_map]
no goals
case mp.intro.mk.left
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ fun i => Subtype p
h : repr y = { fst := a, snd := f }
⊢ abs ((fun i => Subtype.val) <$$> { fst := a, snd := f }) = abs { fst := a, snd := fun i j => ↑(f i j) }
rfl