-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: β)
x : β
⊢ 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)
have 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))
Tactic: obtain ⟨a, f⟩ := g x