awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
A : Type u
α : TypeVec.{u} n
x : (↑(const n A) : (α : TypeVec.{u} n) → Type u) α
mk :
  ∀ (fst : (const n A).A) (snd : (const n A).B fst ⟹ α),
    Eq (α := (↑(const n A) : (α : TypeVec.{u} n) → Type u) α)
      (const.mk n (get (α := α) (Sigma.mk (β := fun (a : (const n A).A) ↦ (const n A).B a ⟹ α) fst snd)) (α := α))
      (Sigma.mk (β := fun (a : (const n A).A) ↦ (const n A).B a ⟹ α) fst snd)
⊢ const.mk n (get (α := α) x) (α := α) = x

Tactic:
cases x
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
A : Type u
α : TypeVec.{u} n
fst : (const n A).A
snd : (const n A).B fst ⟹ α
mk :
  Eq (α := (↑(const n A) : (α : TypeVec.{u} n) → Type u) α)
    (Sigma.mk (β := fun (a : (const n A).A) ↦ (const n A).B a ⟹ α) fst fun (x : Fin2 n) (a : (const n A).B fst x) ↦
      PEmpty.elim a)
    (Sigma.mk (β := fun (a : (const n A).A) ↦ (const n A).B a ⟹ α) fst snd)
⊢ Eq (α := (↑(const n A) : (α : TypeVec.{u} n) → Type u) α)
    (const.mk n (get (α := α) (Sigma.mk (β := fun (a : (const n A).A) ↦ (const n A).B a ⟹ α) fst snd)) (α := α))
    (Sigma.mk (β := fun (a : (const n A).A) ↦ (const n A).B a ⟹ α) fst snd)

Tactic:
dsimp [const.get, const.mk]

Premises used: MvPFunctor.const.get, MvPFunctor.const.mk
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
A : Type u
α : TypeVec.{u} n
fst : (const n A).A
snd : (const n A).B fst ⟹ α
mk mk₁ mk₂ mk₃ : (fun (x : Fin2 n) (a : (const n A).B fst x) ↦ PEmpty.elim a) = snd
⊢ Eq (α := (↑(const n A) : (α : TypeVec.{u} n) → Type u) α)
    (Sigma.mk (β := fun (a : (const n A).A) ↦ (const n A).B a ⟹ α) fst fun (x : Fin2 n) (a : (const n A).B fst x) ↦
      PEmpty.elim a)
    (Sigma.mk (β := fun (a : (const n A).A) ↦ (const n A).B a ⟹ α) fst snd)

Tactic:
congr with (_⟨⟩)
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n m : ℕ
P : MvPFunctor.{u} n
Q : Fin2 n → MvPFunctor.{u} m
α β : TypeVec.{u} m
f : α ⟹ β
x : (↑(P.comp Q) : (α : TypeVec.{u} m) → Type u) α
⊢ get (α := β) (MvFunctor.map (F := (↑(P.comp Q) : (α : TypeVec.{u} m) → Type u)) (α := α) (β := β) f x) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦
      (↑(Q i) : (α : TypeVec.{u} m) → Type u) α) (β := fun (i : Fin2 n) ↦ (↑(Q i) : (α : TypeVec.{u} m) → Type u) β)
      (fun (i : Fin2 n) (x : (↑(Q i) : (α : TypeVec.{u} m) → Type u) α) ↦
        MvFunctor.map (F := (↑(Q i) : (α : TypeVec.{u} m) → Type u)) (α := α) (β := β) f x)
      (get (α := α) x)

Tactic:
rfl
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n m : ℕ
P : MvPFunctor.{u} n
Q : Fin2 n → MvPFunctor.{u} m
α : TypeVec.{u} m
x : (↑P : (α : TypeVec.{u} n) → Type u) fun (i : Fin2 n) ↦ (↑(Q i) : (α : TypeVec.{u} m) → Type u) α
⊢ get (α := α) (mk (α := α) x) = x

Tactic:
rfl
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n m : ℕ
P : MvPFunctor.{u} n
Q : Fin2 n → MvPFunctor.{u} m
α : TypeVec.{u} m
x : (↑(P.comp Q) : (α : TypeVec.{u} m) → Type u) α
⊢ mk (α := α) (get (α := α) x) = x

Tactic:
rfl
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : (↑P : (α : TypeVec.{u} n) → Type u) α
mp :
  LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) p x →
    ∃ (a : P.A) (f : P.B a ⟹ α),
      x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f ∧ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
mpr :
  (∃ (a : P.A) (f : P.B a ⟹ α),
      x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f ∧ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)) →
    LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) p x
⊢ LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) p x ↔
    ∃ (a : P.A) (f : P.B a ⟹ α),
      x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f ∧ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)

Tactic:
constructor
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : (↑P : (α : TypeVec.{u} n) → Type u) α
y : (↑P : (α : TypeVec.{u} n) → Type u) fun (i : Fin2 n) ↦ Subtype (α := α i) p
hy :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) p) (β := α)
      (fun (i : Fin2 n) ↦ Subtype.val (p := p)) y =
    x
mp :
  ∀ (a : P.A) (f : P.B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p)
    (h : y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p) a f),
    ∃ (a : P.A) (f : P.B a ⟹ α),
      x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f ∧ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
⊢ ∃ (a : P.A) (f : P.B a ⟹ α),
    x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f ∧ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)

Tactic:
rcases h : y with ⟨a, f⟩
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : (↑P : (α : TypeVec.{u} n) → Type u) α
y : (↑P : (α : TypeVec.{u} n) → Type u) fun (i : Fin2 n) ↦ Subtype (α := α i) p
hy :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) p) (β := α)
      (fun (i : Fin2 n) ↦ Subtype.val (p := p)) y =
    x
a : P.A
f : P.B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p
h : y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p) a f
⊢ ∃ (a : P.A) (f : P.B a ⟹ α),
    x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f ∧ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)

Tactic:
⟨a, fun i j => (f i j).val, ?_, fun i j => (f i j).property⟩

Premises used: And.intro, Exists.intro, Subtype.val, Subtype.property
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : (↑P : (α : TypeVec.{u} n) → Type u) α
y : (↑P : (α : TypeVec.{u} n) → Type u) fun (i : Fin2 n) ↦ Subtype (α := α i) p
hy :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) p) (β := α)
      (fun (i : Fin2 n) ↦ Subtype.val (p := p)) y =
    x
a : P.A
f : P.B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p
h : y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p) a f
mp : x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i)
⊢ ∃ (a : P.A) (f : P.B a ⟹ α),
    x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f ∧ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)

Tactic:
refine ⟨a, fun i j => (f i j).val, ?_, fun i j => (f i j).property⟩
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : (↑P : (α : TypeVec.{u} n) → Type u) α
y : (↑P : (α : TypeVec.{u} n) → Type u) fun (i : Fin2 n) ↦ Subtype (α := α i) p
hy :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) p) (β := α)
      (fun (i : Fin2 n) ↦ Subtype.val (p := p)) y =
    x
a : P.A
f : P.B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p
h : y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p) a f
mp :
  Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α)
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a
      (TypeVec.comp (α := P.B a) (β := fun (i : Fin2 n) ↦ Subtype (α := α i) p) (γ := α)
        (fun (i : Fin2 n) ↦ Subtype.val (p := p)) f))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i))
⊢ x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i)

Tactic:
rw [← hy, h, map_eq]

Premises used: MvPFunctor.map_eq
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : (↑P : (α : TypeVec.{u} n) → Type u) α
y : (↑P : (α : TypeVec.{u} n) → Type u) fun (i : Fin2 n) ↦ Subtype (α := α i) p
hy :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) p) (β := α)
      (fun (i : Fin2 n) ↦ Subtype.val (p := p)) y =
    x
a : P.A
f : P.B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p
h : y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p) a f
⊢ Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α)
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a
      (TypeVec.comp (α := P.B a) (β := fun (i : Fin2 n) ↦ Subtype (α := α i) p) (γ := α)
        (fun (i : Fin2 n) ↦ Subtype.val (p := p)) f))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i))

Tactic:
rfl
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : (↑P : (α : TypeVec.{u} n) → Type u) α
a : P.A
f : P.B a ⟹ α
xeq : x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f
pf : ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
h :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) p) (β := α)
      (fun (i : Fin2 n) ↦ Subtype.val (p := p))
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p) a
        fun (i : Fin2 n) (j : P.B a i) ↦ Subtype.mk (p := p) (f i j) ⋯) =
    x
⊢ LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) p x

Tactic:
use ⟨a, fun i j => ⟨f i j, pf i j⟩⟩
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : (↑P : (α : TypeVec.{u} n) → Type u) α
a : P.A
f : P.B a ⟹ α
xeq : x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f
pf : ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
h :
  Eq.{u + 1} (α := (↑P : (α : TypeVec.{u} n) → Type u) α)
    (MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) p) (β := α)
      (fun (i : Fin2 n) ↦ Subtype.val (p := p))
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p) a
        fun (i : Fin2 n) (j : P.B a i) ↦ Subtype.mk (p := p) (f i j) ⋯))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
⊢ MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) p) (β := α)
      (fun (i : Fin2 n) ↦ Subtype.val (p := p))
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p) a
        fun (i : Fin2 n) (j : P.B a i) ↦ Subtype.mk (p := p) (f i j) ⋯) =
    x

Tactic:
rw [xeq]
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : (↑P : (α : TypeVec.{u} n) → Type u) α
a : P.A
f : P.B a ⟹ α
xeq : x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f
pf : ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
⊢ Eq.{u + 1} (α := (↑P : (α : TypeVec.{u} n) → Type u) α)
    (MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) p) (β := α)
      (fun (i : Fin2 n) ↦ Subtype.val (p := p))
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p) a
        fun (i : Fin2 n) (j : P.B a i) ↦ Subtype.mk (p := p) (f i j) ⋯))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)

Tactic:
rfl
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
simp :
  (∃ (a_1 : P.A) (f_1 : P.B a_1 ⟹ α),
      Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
          (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) 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)
⊢ LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) p (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) ↔
    ∀ (i : Fin2 n) (x : P.B a i), p (f i x)

Tactic:
simp only [liftP_iff]

Premises used: MvPFunctor.liftP_iff
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
mp :
  (∃ (a_1 : P.A) (f_1 : P.B a_1 ⟹ α),
      Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
          (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) 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)
mpr :
  (∀ (i : Fin2 n) (x : P.B a i), p (f i x)) →
    ∃ (a_2 : P.A) (f_1 : P.B a_2 ⟹ α),
      Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
          (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a_2 f_1) ∧
        ∀ (i : Fin2 n) (j : P.B a_2 i), p (f_1 i j)
⊢ (∃ (a_1 : P.A) (f_1 : P.B a_1 ⟹ α),
      Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
          (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) 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
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
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
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
h : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
mpr :
  ∃ (f_1 : P.B a ⟹ α),
    Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f_1) ∧
      ∀ (i : Fin2 n) (j : P.B a i), p (f_1 i j)
mpr₁ : P.A
⊢ ∃ (a_1 : P.A) (f_1 : P.B a_1 ⟹ α),
    Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a_1 f_1) ∧
      ∀ (i : Fin2 n) (j : P.B a_1 i), p (f_1 i j)

Tactic:
constructor
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
h : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
mpr :
  ∃ (f_1 : P.B a ⟹ α),
    Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f_1) ∧
      ∀ (i : Fin2 n) (j : P.B a i), p (f_1 i j)
mpr₁ : P.A
⊢ ∃ (a_1 : P.A) (f_1 : P.B a_1 ⟹ α),
    Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a_1 f_1) ∧
      ∀ (i : Fin2 n) (j : P.B a_1 i), p (f_1 i j)

Tactic:
first | constructor | assumption
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
h : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
mpr :
  Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) ∧
    ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
mpr₁ : P.B a ⟹ α
⊢ ∃ (f_1 : P.B a ⟹ α),
    Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f_1) ∧
      ∀ (i : Fin2 n) (j : P.B a i), p (f_1 i j)

Tactic:
constructor
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
h : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
mpr :
  Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) ∧
    ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
mpr₁ : P.B a ⟹ α
⊢ ∃ (f_1 : P.B a ⟹ α),
    Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f_1) ∧
      ∀ (i : Fin2 n) (j : P.B a i), p (f_1 i j)

Tactic:
first | constructor | assumption
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
h : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
mpr :
  Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
mpr₁ : ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
⊢ Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) ∧
    ∀ (i : Fin2 n) (j : P.B a i), p (f i j)

Tactic:
constructor
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
h : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
mpr :
  Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
mpr₁ : ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
⊢ Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) ∧
    ∀ (i : Fin2 n) (j : P.B a i), p (f i j)

Tactic:
first | constructor | assumption
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
h : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)

Tactic:
constructor
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
h : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)

Tactic:
first | constructor | assumption
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
h : ∀ (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
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
h : ∀ (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
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
h : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
mpr :
  ∃ (f_1 : P.B a ⟹ α),
    Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f_1) ∧
      ∀ (i : Fin2 n) (j : P.B a i), p (f_1 i j)
mpr₁ :
  Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) ∧
    ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
mpr₂ :
  Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
mpr₃ : ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
⊢ ∃ (a_1 : P.A) (f_1 : P.B a_1 ⟹ α),
    Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a_1 f_1) ∧
      ∀ (i : Fin2 n) (j : P.B a_1 i), p (f_1 i j)

Tactic:
repeat' first | constructor | assumption
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : (↑P : (α : TypeVec.{u} n) → Type u) α
mp :
  LiftR (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) r x y →
    ∃ (a : P.A) (f₀ : P.B a ⟹ α) (f₁ : P.B a ⟹ α),
      x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f₀ ∧
        y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f₁ ∧ ∀ (i : Fin2 n) (j : P.B a i), r (f₀ i j) (f₁ i j)
mpr :
  (∃ (a : P.A) (f₀ : P.B a ⟹ α) (f₁ : P.B a ⟹ α),
      x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f₀ ∧
        y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f₁ ∧ ∀ (i : Fin2 n) (j : P.B a i), r (f₀ i j) (f₁ i j)) →
    LiftR (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) r x y
⊢ LiftR (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) r x y ↔
    ∃ (a : P.A) (f₀ : P.B a ⟹ α) (f₁ : P.B a ⟹ α),
      x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f₀ ∧
        y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f₁ ∧ ∀ (i : Fin2 n) (j : P.B a i), r (f₀ i j) (f₁ i j)

Tactic:
constructor
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : (↑P : (α : TypeVec.{u} n) → Type u) α
u : (↑P : (α : TypeVec.{u} n) → Type u) fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
xeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1) u =
    x
yeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2) u =
    y
mp :
  ∀ (a : P.A) (f : P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
    (h : u = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f),
    ∃ (a : P.A) (f₀ : P.B a ⟹ α) (f₁ : P.B a ⟹ α),
      x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f₀ ∧
        y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f₁ ∧ ∀ (i : Fin2 n) (j : P.B a i), r (f₀ i j) (f₁ i j)
⊢ ∃ (a : P.A) (f₀ : P.B a ⟹ α) (f₁ : P.B a ⟹ α),
    x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f₀ ∧
      y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f₁ ∧ ∀ (i : Fin2 n) (j : P.B a i), r (f₀ i j) (f₁ i j)

Tactic:
rcases h : u with ⟨a, f⟩
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : (↑P : (α : TypeVec.{u} n) → Type u) α
u : (↑P : (α : TypeVec.{u} n) → Type u) fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
xeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1) u =
    x
yeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2) u =
    y
a : P.A
f : P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
h : u = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f
h₁ :
  (x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).1) ∧
    (y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).2) ∧
      ∀ (i : Fin2 n) (j : P.B a i),
        r (↑(f i j) : α i × α i).1 ((fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).2) i j)
⊢ ∃ (a : P.A) (f₀ : P.B a ⟹ α) (f₁ : P.B a ⟹ α),
    x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f₀ ∧
      y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f₁ ∧ ∀ (i : Fin2 n) (j : P.B a i), r (f₀ i j) (f₁ i j)

Tactic:
use a, fun i j => (f i j).val.fst, fun i j => (f i j).val.snd

Premises used: Prod.fst, Subtype.val, Prod.snd