-- 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 : β
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))
have dsimp : Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
  (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a
    (splitFun (α := P.B a) (α' := α ::: P.M α) (dropFun (α := P.B a) (β := α ::: β) f)
      ((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 a) (β := α ::: β) f)))
  (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: dsimp