-- Mathlib/Data/PFunctor/Multivariate/Basic.lean
theorem liftP_iff' {α : TypeVec n} (p : ∀ ⦃i⦄, α i → Prop) (a : P.A) (f : P.B a ⟹ α) :
    @LiftP.{u} _ P.Obj _ α p ⟨a, f⟩ ↔ ∀ i x, p (f i x)

Proof state:
case mp
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
⊢ (∃ a_1 f_1, ⟨a, f⟩ = ⟨a_1, f_1⟩ ∧ ∀ (i : Fin2 n) (j : P.B a_1 i), p (f_1 i j)) →
    ∀ (i : Fin2 n) (x : P.B a i), p (f i x)

Tactic:
rintro ⟨_, _, ⟨⟩, _⟩

Result:
case mp.intro.intro.intro.refl
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
right✝ : ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
⊢ ∀ (i : Fin2 n) (x : P.B a i), p (f i x)

Proof state:
case mpr
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ ∃ a_1 f_1, ⟨a, f⟩ = ⟨a_1, f_1⟩ ∧ ∀ (i : Fin2 n) (j : P.B a_1 i), p (f_1 i j)

Tactic:
repeat' first |constructor|assumption

Result:
no goals

Proof state:
case mpr.h.h.right
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)

Tactic:
assumption

Result:
no goals

Proof state:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
⊢ LiftP p ⟨a, f⟩ ↔ ∀ (i : Fin2 n) (x : P.B a i), p (f i x)

Tactic:
simp only [liftP_iff, Sigma.mk.inj_iff]

Result:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
⊢ (∃ a_1 f_1, ⟨a, f⟩ = ⟨a_1, f_1⟩ ∧ ∀ (i : Fin2 n) (j : P.B a_1 i), p (f_1 i j)) ↔
    ∀ (i : Fin2 n) (x : P.B a i), p (f i x)

Proof state:
case mpr.h.h.left
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ ⟨a, f⟩ = ⟨?mpr.w, ?mpr.h.w⟩

Tactic:
constructor

Result:
no goals

Proof state:
case mpr.h.h.right
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)

Tactic:
first |constructor|assumption

Result:
no goals

Proof state:
case mpr
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
⊢ (∀ (i : Fin2 n) (x : P.B a i), p (f i x)) →
    ∃ a_2 f_1, ⟨a, f⟩ = ⟨a_2, f_1⟩ ∧ ∀ (i : Fin2 n) (j : P.B a_2 i), p (f_1 i j)

Tactic:
intro

Result:
case mpr
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ ∃ a_1 f_1, ⟨a, f⟩ = ⟨a_1, f_1⟩ ∧ ∀ (i : Fin2 n) (j : P.B a_1 i), p (f_1 i j)

Proof state:
case mp.intro.intro.intro.refl
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
right✝ : ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
⊢ ∀ (i : Fin2 n) (x : P.B a i), p (f i x)

Tactic:
assumption

Result:
no goals

Proof state:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
⊢ (∃ a_1 f_1, ⟨a, f⟩ = ⟨a_1, f_1⟩ ∧ ∀ (i : Fin2 n) (j : P.B a_1 i), p (f_1 i j)) ↔
    ∀ (i : Fin2 n) (x : P.B a i), p (f i x)

Tactic:
constructor

Result:
case mp
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
⊢ (∃ a_1 f_1, ⟨a, f⟩ = ⟨a_1, f_1⟩ ∧ ∀ (i : Fin2 n) (j : P.B a_1 i), p (f_1 i j)) →
    ∀ (i : Fin2 n) (x : P.B a i), p (f i x)

case mpr
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
⊢ (∀ (i : Fin2 n) (x : P.B a i), p (f i x)) →
    ∃ a_2 f_1, ⟨a, f⟩ = ⟨a_2, f_1⟩ ∧ ∀ (i : Fin2 n) (j : P.B a_2 i), p (f_1 i j)