-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: β)
x : β
obtain :
  ∀ (a : P.A) (f : P.B a ⟹ α ::: β),
    Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α)
        (Sigma.fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β) a f))
        (splitFun (α :=
          P.B (Sigma.fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β) a f)))
          (α' := α ::: P.M α)
          (dropFun (α :=
            P.B
              (Sigma.fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β) a f)))
            (β := α ::: β)
            (Sigma.snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β) a f)))
          (Function.comp (β := β)
            (corec' P (α := α) (fun (b : β) ↦ (g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))
                (fun (b : β) ↦
                  dropFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
                    ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))
                fun (b : β) ↦
                lastFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
                  ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)) :
              β → P.M α)
            (lastFun (α :=
                P.B
                  (Sigma.fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)
                    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β) a f)))
                (β := α ::: β)
                (Sigma.snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)
                  (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β) a f)) :
              (P.B
                    (Sigma.fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)
                      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β) a f))).last →
                (α ::: β).last))))
      (MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: β) (β := α ::: P.M α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec P (α := α) g))
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β) a f))
⊢ Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))
      (splitFun (α := P.B ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (α' := α ::: P.M α)
        (dropFun (α := P.B ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
          ((g x).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))
        ((corec' P (α := α) (fun (b : β) ↦ (g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))
            (fun (b : β) ↦
              dropFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
                ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))
            fun (b : β) ↦
            lastFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
              ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) ∘
          lastFun (α := P.B ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
            ((g x).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: β) (β := α ::: P.M α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec P (α := α) g)) (g x)

Tactic:
obtain ⟨a, f⟩ := g x