awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) x) =
        MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) y)
x y : P.M α
r : R x y
refine_3 : ∀ (this : ∀ (x y : P.M α) (r : Relation.EqvGen R x y), x = y), x = y
refine_1 : Equivalence (Relation.EqvGen R)
refine_2 :
  ∀ (x y : P.M α),
    Relation.EqvGen R x y →
      MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
          α ::: Quot (Relation.EqvGen R))
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R))) (dest P (α := α) x) =
        MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
          α ::: Quot (Relation.EqvGen R))
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R))) (dest P (α := α) y)
⊢ x = y

Tactic:
have := M.bisim₀ P (Relation.EqvGen R) ?_ ?_
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) x) =
        MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) y)
x y : P.M α
r : R x y
this : ∀ (x y : P.M α) (r : Relation.EqvGen R x y), x = y
⊢ x = y

Tactic:
solve_by_elim [Relation.EqvGen.rel]

Premises used: Relation.EqvGen.rel
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) x) =
        MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) y)
x y : P.M α
r : R x y
⊢ Equivalence (Relation.EqvGen R)

Tactic:
apply Relation.EqvGen.is_equivalence

Premises used: Relation.EqvGen.is_equivalence
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) x) =
        MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) y)
x y : P.M α
Hr : Relation.EqvGen R x y
⊢ ∀ (x y : P.M α), R x y → Relation.EqvGen R x y

Tactic:
have : ∀ x y, R x y → Relation.EqvGen R x y := @Relation.EqvGen.rel _ R
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) x) =
        MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) y)
x y : P.M α
this : ∀ (x y : P.M α), R x y → Relation.EqvGen R x y
x_1 : P.M α
⊢ MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R)) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R)))
      (dest P (α := α) x_1) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R)) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R)))
      (dest P (α := α) x_1)

Tactic:
simp_all
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) x) =
        MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) y)
x y : P.M α
this : ∀ (x y : P.M α), R x y → Relation.EqvGen R x y
x_1 y_1 : P.M α
h_1 : Relation.EqvGen R x_1 y_1
a_ih :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R)) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R)))
      (dest P (α := α) x_1) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R)) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R)))
      (dest P (α := α) y_1)
⊢ MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R)) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R)))
      (dest P (α := α) y_1) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R)) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R)))
      (dest P (α := α) x_1)

Tactic:
simp_all
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) x) =
        MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) y)
x y : P.M α
this : ∀ (x y : P.M α), R x y → Relation.EqvGen R x y
x_1 y_1 z : P.M α
h_1 : Relation.EqvGen R x_1 y_1
h_2 : Relation.EqvGen R y_1 z
a_ih :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R)) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R)))
      (dest P (α := α) x_1) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R)) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R)))
      (dest P (α := α) y_1)
a_ih_1 :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R)) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R)))
      (dest P (α := α) y_1) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R)) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R)))
      (dest P (α := α) z)
⊢ MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R)) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R)))
      (dest P (α := α) x_1) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R)) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R)))
      (dest P (α := α) z)

Tactic:
simp_all
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
x : P.M α
obtain :
  ∀ (a : P.mp.A) (f : P.mp.B a ⟹ α),
    dest P (α := β)
        (MvFunctor.map (F := P.M) (α := α) (β := β) g (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f)) =
      MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := β ::: P.M β)
        (appendFun (α := α) (α' := β) g fun (x : P.M α) ↦ MvFunctor.map (F := P.M) (α := α) (β := β) g x)
        (dest P (α := α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))
⊢ dest P (α := β) (MvFunctor.map (F := P.M) (α := α) (β := β) g x) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := β ::: P.M β)
      (appendFun (α := α) (α' := β) g fun (x : P.M α) ↦ MvFunctor.map (F := P.M) (α := α) (β := β) g x)
      (dest P (α := α) x)

Tactic:
obtain ⟨a, f⟩ := x
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.mp.A
f : P.mp.B a ⟹ α
rhs :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := β ::: P.M β)
    (appendFun (α := α) (α' := β) g fun (x : P.M α) ↦ MvFunctor.map (F := P.M) (α := α) (β := β) g x)
    (dest P (α := α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))
| dest P (α := β)
      (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ β) a (TypeVec.comp (α := P.mp.B a) (β := α) (γ := β) g f)) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := β ::: P.M β)
      (appendFun (α := α) (α' := β) g fun (x : P.M α) ↦ MvFunctor.map (F := P.M) (α := α) (β := β) g x)
      (dest P (α := α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))

Tactic:
rhs
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.mp.A
f : P.mp.B a ⟹ α
rw :
  Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ β ::: P.M β)
    ((PFunctor.M.dest
          (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).fst
      (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M))
    (splitFun (α :=
      P.B
        ((PFunctor.M.dest
              (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
                (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).fst
          (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M)))
      (α' := β ::: P.M β)
      (TypeVec.comp (α :=
        (P.B
            ((PFunctor.M.dest
                  (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
                    (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).fst
              (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M))).drop)
        (β := α) (γ := (β ::: P.M β).drop) g
        (pathDestLeft P (α := (α ::: P.M α).drop) ⋯
          (Sigma.snd (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))))
      ((fun (x : P.M α) ↦ MvFunctor.map (F := P.M) (α := α) (β := β) g x) ∘
        fun
          (x :
            (P.B
                ((PFunctor.M.dest
                      (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
                        (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).fst
                  (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M))).last) ↦
        Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
          ((PFunctor.M.dest
                (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
                  (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).snd
            (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M) x)
          (pathDestRight P (α := α) ⋯
            (Sigma.snd (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))
            x)))
| MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := β ::: P.M β)
    (appendFun (α := α) (α' := β) g fun (x : P.M α) ↦ MvFunctor.map (F := P.M) (α := α) (β := β) g x)
    (dest P (α := α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))

Tactic:
rw [M.dest, M.dest', map_eq, appendFun_comp_splitFun]

Premises used: MvPFunctor.map_eq, MvPFunctor.M.dest, MvPFunctor.M.dest', TypeVec.appendFun_comp_splitFun
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.mp.A
f : P.mp.B a ⟹ α
rw :
  Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ β ::: P.M β)
    ((PFunctor.M.dest
          (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).fst
      (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M))
    (splitFun (α :=
      P.B
        ((PFunctor.M.dest
              (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
                (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).fst
          (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M)))
      (α' := β ::: P.M β)
      (TypeVec.comp (α :=
        (P.B
            ((PFunctor.M.dest
                  (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
                    (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).fst
              (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M))).drop)
        (β := α) (γ := (β ::: P.M β).drop) g
        (pathDestLeft P (α := (α ::: P.M α).drop) ⋯
          (Sigma.snd (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))))
      ((fun (x : P.M α) ↦ MvFunctor.map (F := P.M) (α := α) (β := β) g x) ∘
        fun
          (x :
            (P.B
                ((PFunctor.M.dest
                      (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
                        (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).fst
                  (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M))).last) ↦
        Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
          ((PFunctor.M.dest
                (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
                  (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).snd
            (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M) x)
          (pathDestRight P (α := α) ⋯
            (Sigma.snd (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))
            x)))
| dest P (α := β)
      (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ β) a (TypeVec.comp (α := P.mp.B a) (β := α) (γ := β) g f)) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := β ::: P.M β)
      (appendFun (α := α) (α' := β) g fun (x : P.M α) ↦ MvFunctor.map (F := P.M) (α := α) (β := β) g x)
      (dest P (α := α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))

Tactic:
rhs
    rw [M.dest, M.dest', map_eq, appendFun_comp_splitFun]

Premises used: MvPFunctor.map_eq, MvPFunctor.M.dest, MvPFunctor.M.dest', TypeVec.appendFun_comp_splitFun
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.mp.A
f : P.mp.B a ⟹ α
conv :
  Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (β ::: P.M β))
    (dest P (α := β)
      (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ β) a (TypeVec.comp (α := P.mp.B a) (β := α) (γ := β) g f)))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ β ::: P.M β)
      ((PFunctor.M.dest
            (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
              (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).fst
        (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M))
      (splitFun (α :=
        P.B
          ((PFunctor.M.dest
                (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
                  (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).fst
            (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M)))
        (α' := β ::: P.M β)
        (TypeVec.comp (α :=
          (P.B
              ((PFunctor.M.dest
                    (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
                      (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).fst
                (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M))).drop)
          (β := α) (γ := (β ::: P.M β).drop) g
          (pathDestLeft P (α := (α ::: P.M α).drop) ⋯
            (Sigma.snd (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))))
        ((fun (x : P.M α) ↦ MvFunctor.map (F := P.M) (α := α) (β := β) g x) ∘
          fun
            (x :
              (P.B
                  ((PFunctor.M.dest
                        (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
                          (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).fst
                    (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M))).last) ↦
          Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
            ((PFunctor.M.dest
                  (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
                    (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).snd
              (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M) x)
            (pathDestRight P (α := α) ⋯
              (Sigma.snd (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))
              x))))
⊢ dest P (α := β)
      (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ β) a (TypeVec.comp (α := P.mp.B a) (β := α) (γ := β) g f)) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := β ::: P.M β)
      (appendFun (α := α) (α' := β) g fun (x : P.M α) ↦ MvFunctor.map (F := P.M) (α := α) (β := β) g x)
      (dest P (α := α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))

Tactic:
conv =>
    rhs
    rw [M.dest, M.dest', map_eq, appendFun_comp_splitFun]

Premises used: MvPFunctor.map_eq, MvPFunctor.M.dest, MvPFunctor.M.dest', TypeVec.appendFun_comp_splitFun
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.mp.A
f : P.mp.B a ⟹ α
⊢ Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (β ::: P.M β))
    (dest P (α := β)
      (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ β) a (TypeVec.comp (α := P.mp.B a) (β := α) (γ := β) g f)))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ β ::: P.M β)
      ((PFunctor.M.dest
            (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
              (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).fst
        (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M))
      (splitFun (α :=
        P.B
          ((PFunctor.M.dest
                (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
                  (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).fst
            (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M)))
        (α' := β ::: P.M β)
        (TypeVec.comp (α :=
          (P.B
              ((PFunctor.M.dest
                    (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
                      (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).fst
                (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M))).drop)
          (β := α) (γ := (β ::: P.M β).drop) g
          (pathDestLeft P (α := (α ::: P.M α).drop) ⋯
            (Sigma.snd (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))))
        ((fun (x : P.M α) ↦ MvFunctor.map (F := P.M) (α := α) (β := β) g x) ∘
          fun
            (x :
              (P.B
                  ((PFunctor.M.dest
                        (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
                          (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).fst
                    (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M))).last) ↦
          Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
            ((PFunctor.M.dest
                  (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
                    (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).snd
              (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M) x)
            (pathDestRight P (α := α) ⋯
              (Sigma.snd (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))
              x))))

Tactic:
rfl
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ::: P.M α ⟹ β ::: P.M β
x : P.M α
h :
  ∀ (x : P.M α),
    lastFun (α := α ::: P.M α) (β := β ::: P.M β) g x =
      MvFunctor.map (F := P.M) (α := (α ::: P.M α).drop) (β := β) (dropFun (α := α ::: P.M α) (β := β ::: P.M β) g) x
rw :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := β ::: P.M β) g
      (dest P (α := α) x) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := (α ::: P.M α).drop ::: P.M (α ::: P.M α).drop)
      (β := (β ::: P.M β).drop ::: P.M (β ::: P.M β).drop)
      (appendFun (α := (α ::: P.M α).drop) (α' := (β ::: P.M β).drop) (dropFun (α := α ::: P.M α) (β := β ::: P.M β) g)
        fun (x : P.M (α ::: P.M α).drop) ↦
        MvFunctor.map (F := P.M) (α := (α ::: P.M α).drop) (β := (β ::: P.M β).drop)
          (dropFun (α := α ::: P.M α) (β := β ::: P.M β) g) x)
      (dest P (α := (α ::: P.M α).drop) x)
⊢ MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := β ::: P.M β) g
      (dest P (α := α) x) =
    dest P (α := (β ::: P.M β).drop)
      (MvFunctor.map (F := P.M) (α := (α ::: P.M α).drop) (β := (β ::: P.M β).drop)
        (dropFun (α := α ::: P.M α) (β := β ::: P.M β) g) x)

Tactic:
rw [M.dest_map]

Premises used: MvPFunctor.M.dest_map
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ::: P.M α ⟹ β ::: P.M β
x : P.M α
h :
  ∀ (x : P.M α),
    lastFun (α := α ::: P.M α) (β := β ::: P.M β) g x =
      MvFunctor.map (F := P.M) (α := (α ::: P.M α).drop) (β := β) (dropFun (α := α ::: P.M α) (β := β ::: P.M β) g) x
e_a :
  g =
    appendFun (α := (α ::: P.M α).drop) (α' := (β ::: P.M β).drop) (dropFun (α := α ::: P.M α) (β := β ::: P.M β) g)
      fun (x : P.M (α ::: P.M α).drop) ↦
      MvFunctor.map (F := P.M) (α := (α ::: P.M α).drop) (β := (β ::: P.M β).drop)
        (dropFun (α := α ::: P.M α) (β := β ::: P.M β) g) x
⊢ MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := β ::: P.M β) g
      (dest P (α := α) x) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := (α ::: P.M α).drop ::: P.M (α ::: P.M α).drop)
      (β := (β ::: P.M β).drop ::: P.M (β ::: P.M β).drop)
      (appendFun (α := (α ::: P.M α).drop) (α' := (β ::: P.M β).drop) (dropFun (α := α ::: P.M α) (β := β ::: P.M β) g)
        fun (x : P.M (α ::: P.M α).drop) ↦
        MvFunctor.map (F := P.M) (α := (α ::: P.M α).drop) (β := (β ::: P.M β).drop)
          (dropFun (α := α ::: P.M α) (β := β ::: P.M β) g) x)
      (dest P (α := (α ::: P.M α).drop) x)

Tactic:
congr
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ::: P.M α ⟹ β ::: P.M β
x : P.M α
h :
  ∀ (x : P.M α),
    lastFun (α := α ::: P.M α) (β := β ::: P.M β) g x =
      MvFunctor.map (F := P.M) (α := (α ::: P.M α).drop) (β := β) (dropFun (α := α ::: P.M α) (β := β ::: P.M β) g) x
⊢ dropFun (α := α ::: P.M α) (β := β ::: P.M β) g =
    dropFun (α := α ::: P.M α) (β := β ::: P.M β)
      (appendFun (α := (α ::: P.M α).drop) (α' := (β ::: P.M β).drop) (dropFun (α := α ::: P.M α) (β := β ::: P.M β) g)
        fun (x : P.M (α ::: P.M α).drop) ↦
        MvFunctor.map (F := P.M) (α := (α ::: P.M α).drop) (β := (β ::: P.M β).drop)
          (dropFun (α := α ::: P.M α) (β := β ::: P.M β) g) x)

Tactic:
simp