case mp
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : Obj P α
⊢ LiftP p x → ∃ a f, x = { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : B P a i), p (f i j)

case mpr
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : Obj P α
⊢ (∃ a f, x = { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : B P a i), p (f i j)) → LiftP p x
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : Obj P α
⊢ LiftP p x ↔ ∃ a f, x = { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : B P a i), p (f i j)
constructor
case mpr.intro.intro.intro
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : Obj P α
a : P.A
f : B P a ⟹ α
xeq : x = { fst := a, snd := f }
pf : ∀ (i : Fin2 n) (j : B P a i), p (f i j)
⊢ LiftP p x
case mpr
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : Obj P α
⊢ (∃ a f, x = { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : B P a i), p (f i j)) → LiftP p x
rintro ⟨a, f, xeq, pf⟩
case mpr.intro.intro.intro
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : Obj P α
a : P.A
f : B P a ⟹ α
xeq : x = { fst := a, snd := f }
pf : ∀ (i : Fin2 n) (j : B P a i), p (f i j)
⊢ (fun i => Subtype.val) <$$> { fst := a, snd := fun i j => { val := f i j, property := (_ : p (f i j)) } } = x
case mpr.intro.intro.intro
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : Obj P α
a : P.A
f : B P a ⟹ α
xeq : x = { fst := a, snd := f }
pf : ∀ (i : Fin2 n) (j : B P a i), p (f i j)
⊢ LiftP p x
use ⟨a, fun i j => ⟨f i j, pf i j⟩⟩
case mpr.intro.intro.intro
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : Obj P α
a : P.A
f : B P a ⟹ α
xeq : x = { fst := a, snd := f }
pf : ∀ (i : Fin2 n) (j : B P a i), p (f i j)
⊢ (fun i => Subtype.val) <$$> { fst := a, snd := fun i j => { val := f i j, property := (_ : p (f i j)) } } =
    { fst := a, snd := f }
case mpr.intro.intro.intro
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : Obj P α
a : P.A
f : B P a ⟹ α
xeq : x = { fst := a, snd := f }
pf : ∀ (i : Fin2 n) (j : B P a i), p (f i j)
⊢ (fun i => Subtype.val) <$$> { fst := a, snd := fun i j => { val := f i j, property := (_ : p (f i j)) } } = x
rw [xeq]
no goals
case mpr.intro.intro.intro
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : Obj P α
a : P.A
f : B P a ⟹ α
xeq : x = { fst := a, snd := f }
pf : ∀ (i : Fin2 n) (j : B P a i), p (f i j)
⊢ (fun i => Subtype.val) <$$> { fst := a, snd := fun i j => { val := f i j, property := (_ : p (f i j)) } } =
    { fst := a, snd := f }
rfl
case mp.intro
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : Obj P α
y : Obj P fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
⊢ ∃ a f, x = { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : B P a i), p (f i j)
case mp
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : Obj P α
⊢ LiftP p x → ∃ a f, x = { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : B P a i), p (f i j)
rintro ⟨y, hy⟩
case mp.intro.mk
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : Obj P α
y : Obj P fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : P.A
f : B P a ⟹ fun i => Subtype p
h : y = { fst := a, snd := f }
⊢ ∃ a f, x = { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : B P a i), p (f i j)
case mp.intro
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : Obj P α
y : Obj P fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
⊢ ∃ a f, x = { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : B P a i), p (f i j)
cases' h : y with a f
case mp.intro.mk
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : Obj P α
y : Obj P fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : P.A
f : B P a ⟹ fun i => Subtype p
h : y = { fst := a, snd := f }
⊢ x = { fst := a, snd := fun i j => ↑(f i j) }
case mp.intro.mk
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : Obj P α
y : Obj P fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : P.A
f : B P a ⟹ fun i => Subtype p
h : y = { fst := a, snd := f }
⊢ ∃ a f, x = { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : B P a i), p (f i j)
refine' ⟨a, fun i j => (f i j).val, _, fun i j => (f i j).property⟩
case mp.intro.mk
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : Obj P α
y : Obj P fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : P.A
f : B P a ⟹ fun i => Subtype p
h : y = { fst := a, snd := f }
⊢ { fst := a, snd := (fun i => Subtype.val) ⊚ f } = { fst := a, snd := fun i j => ↑(f i j) }
case mp.intro.mk
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : Obj P α
y : Obj P fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : P.A
f : B P a ⟹ fun i => Subtype p
h : y = { fst := a, snd := f }
⊢ x = { fst := a, snd := fun i j => ↑(f i j) }
rw [← hy, h, map_eq]
no goals
case mp.intro.mk
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : Obj P α
y : Obj P fun i => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : P.A
f : B P a ⟹ fun i => Subtype p
h : y = { fst := a, snd := f }
⊢ { fst := a, snd := (fun i => Subtype.val) ⊚ f } = { fst := a, snd := fun i j => ↑(f i j) }
rfl