n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
⊢ (∃ a_1 f_1, { fst := a, snd := f } = { fst := a_1, snd := f_1 } ∧ ∀ (i : Fin2 n) (j : B P a_1 i), p (f_1 i j)) ↔
    ∀ (i : Fin2 n) (x : B P a i), p (f i x)
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
⊢ LiftP p { fst := a, snd := f } ↔ ∀ (i : Fin2 n) (x : B P a i), p (f i x)
simp only [liftP_iff, Sigma.mk.inj_iff]
case mp
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
⊢ (∃ a_1 f_1, { fst := a, snd := f } = { fst := a_1, snd := f_1 } ∧ ∀ (i : Fin2 n) (j : B P a_1 i), p (f_1 i j)) →
    ∀ (i : Fin2 n) (x : B P a i), p (f i x)

case mpr
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
⊢ (∀ (i : Fin2 n) (x : B P a i), p (f i x)) →
    ∃ a_2 f_1, { fst := a, snd := f } = { fst := a_2, snd := f_1 } ∧ ∀ (i : Fin2 n) (j : B P a_2 i), p (f_1 i j)
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
⊢ (∃ a_1 f_1, { fst := a, snd := f } = { fst := a_1, snd := f_1 } ∧ ∀ (i : Fin2 n) (j : B P a_1 i), p (f_1 i j)) ↔
    ∀ (i : Fin2 n) (x : B P a i), p (f i x)
constructor
no goals
case mpr
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
⊢ (∀ (i : Fin2 n) (x : B P a i), p (f i x)) →
    ∃ a_2 f_1, { fst := a, snd := f } = { fst := a_2, snd := f_1 } ∧ ∀ (i : Fin2 n) (j : B P a_2 i), p (f_1 i j)
. intro
  repeat' first |constructor|assumption
case mp.intro.intro.intro.refl
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
right✝ : ∀ (i : Fin2 n) (j : B P a i), p (f i j)
⊢ ∀ (i : Fin2 n) (x : B P a i), p (f i x)
case mp
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
⊢ (∃ a_1 f_1, { fst := a, snd := f } = { fst := a_1, snd := f_1 } ∧ ∀ (i : Fin2 n) (j : B P a_1 i), p (f_1 i j)) →
    ∀ (i : Fin2 n) (x : B P a i), p (f i x)
rintro ⟨_, _, ⟨⟩, _⟩
no goals
case mp.intro.intro.intro.refl
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
right✝ : ∀ (i : Fin2 n) (j : B P a i), p (f i j)
⊢ ∀ (i : Fin2 n) (x : B P a i), p (f i x)
assumption
case mpr
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : B P a i), p (f i x)
⊢ ∃ a_1 f_1, { fst := a, snd := f } = { fst := a_1, snd := f_1 } ∧ ∀ (i : Fin2 n) (j : B P a_1 i), p (f_1 i j)
case mpr
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
⊢ (∀ (i : Fin2 n) (x : B P a i), p (f i x)) →
    ∃ a_2 f_1, { fst := a, snd := f } = { fst := a_2, snd := f_1 } ∧ ∀ (i : Fin2 n) (j : B P a_2 i), p (f_1 i j)
intro
no goals
case mpr
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : B P a i), p (f i x)
⊢ ∃ a_1 f_1, { fst := a, snd := f } = { fst := a_1, snd := f_1 } ∧ ∀ (i : Fin2 n) (j : B P a_1 i), p (f_1 i j)
repeat' first |constructor|assumption
no goals
case mpr.h.h.right
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : B P a i), p (f i x)
⊢ ∀ (i : Fin2 n) (j : B P a i), p (f i j)
first |constructor|assumption
case mpr.h.h.right
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : B P a i), p (f i x)
⊢ ∀ (i : Fin2 n) (j : B P a i), p (f i j)
case mpr.h.h.right
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : B P a i), p (f i x)
⊢ ∀ (i : Fin2 n) (j : B P a i), p (f i j)
constructor
no goals
case mpr.h.h.right
n m : ℕ
P : MvPFunctor n
Q : Fin2 n → MvPFunctor m
α✝ β : TypeVec m
α : TypeVec n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : B P a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : B P a i), p (f i x)
⊢ ∀ (i : Fin2 n) (j : B P a i), p (f i j)
assumption