-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
lawful : LawfulMvFunctor F
α : TypeVec.{u} n
ι ι' : Type u
R : ι' → ι' → Prop
x : F (α ::: ι)
f g : ι → ι'
hh : ∀ (x : ι), R (f x) (g x)
h : ι → { x : ι' × ι' // uncurry R x } := fun (x : ι) ↦ Subtype.mk (p := fun (x : ι' × ι') ↦ uncurry R x) (f x, g x) ⋯
b : α ::: ι ⟹ Subtype_ (α := α ⊗ α) α.repeatEq ::: { x : ι' × ι' // uncurry R x } :=
  appendFun (α := α) (α' := Subtype_ (α := α ⊗ α) α.repeatEq) (diagSub (α := α)) h
c : Subtype_ (α := α ⊗ α) α.repeatEq ::: { x : ι' × ι' // uncurry R x } ⟹
  (fun (i : Fin2 n) ↦ { x : (α ::: ι' ⊗ α ::: ι') i.fs // ofRepeat (α.RelLast' R i.fs x) }) ::: Subtype (uncurry R) :=
  appendFun (α := Subtype_ (α := α ⊗ α) α.repeatEq) (α' := fun (i : Fin2 n) ↦
    { x : (α ::: ι' ⊗ α ::: ι') i.fs // ofRepeat (α.RelLast' R i.fs x) }) (ofSubtype (α := α ⊗ α) α.repeatEq) _root_.id
⊢ lastFun (α := α ::: ι) (β := α ::: ι' ⊗ α ::: ι')
      (TypeVec.comp (α := α ::: ι) (β := Subtype_ (α := α ::: ι' ⊗ α ::: ι') (α.RelLast' R)) (γ := α ::: ι' ⊗ α ::: ι')
        (subtypeVal (α := α ::: ι' ⊗ α ::: ι') (α.RelLast' R))
        (TypeVec.comp (α := α ::: ι) (β := fun (i : Fin2 (n + 1)) ↦
          { x : (α ::: ι' ⊗ α ::: ι') i // ofRepeat (α.RelLast' R i x) }) (γ :=
          Subtype_ (α := α ::: ι' ⊗ α ::: ι') (α.RelLast' R)) (toSubtype (α := α ::: ι' ⊗ α ::: ι') (α.RelLast' R))
          (TypeVec.comp (α := α ::: ι) (β :=
            (TypeVec.drop fun (i : Fin2 (n + 1)) ↦ { x : (α ::: ι' ⊗ α ::: ι') i // ofRepeat (α.RelLast' R i x) }) :::
              TypeVec.last (n := n) fun (i : Fin2 (n + 1)) ↦
                { x : (α ::: ι' ⊗ α ::: ι') i // ofRepeat (α.RelLast' R i x) })
            (γ := fun (i : Fin2 (n + 1)) ↦ { x : (α ::: ι' ⊗ α ::: ι') i // ofRepeat (α.RelLast' R i x) })
            (fromAppend1DropLast (α := fun (i : Fin2 (n + 1)) ↦
              { x : (α ::: ι' ⊗ α ::: ι') i // ofRepeat (α.RelLast' R i x) }))
            (TypeVec.comp (α := α ::: ι) (β := Subtype_ (α := α ⊗ α) α.repeatEq ::: { x : ι' × ι' // uncurry R x })
              (γ :=
              (TypeVec.drop fun (i : Fin2 (n + 1)) ↦ { x : (α ::: ι' ⊗ α ::: ι') i // ofRepeat (α.RelLast' R i x) }) :::
                TypeVec.last (n := n) fun (i : Fin2 (n + 1)) ↦
                  { x : (α ::: ι' ⊗ α ::: ι') i // ofRepeat (α.RelLast' R i x) })
              c (appendFun (α := α) (α' := Subtype_ (α := α ⊗ α) α.repeatEq) (diagSub (α := α)) h))))) =
    lastFun (α := α ::: ι) (β := α ::: ι' ⊗ α ::: ι')
      (TypeVec.comp (α := α ::: ι) (β := α ::: ι ⊗ α ::: ι) (γ := α ::: ι' ⊗ α ::: ι')
        (prod.map (α := α ::: ι) (α' := α ::: ι) (β := α ::: ι') (β' := α ::: ι')
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g))
        (prod.diag (α := α ::: ι)))
have h₁ : Subtype.val ∘
    lastFun (α := Subtype_ (α := α ⊗ α) α.repeatEq ::: { x : ι' × ι' // uncurry R x }) (β :=
        (TypeVec.drop fun (i : Fin2 (n + 1)) ↦ { x : (α ::: ι' ⊗ α ::: ι') i // ofRepeat (α.RelLast' R i x) }) :::
          TypeVec.last (n := n) fun (i : Fin2 (n + 1)) ↦ { x : (α ::: ι' ⊗ α ::: ι') i // ofRepeat (α.RelLast' R i x) })
        c ∘
      h =
  Prod.map f g ∘ lastFun (α := α ::: ι) (β := α ::: ι ⊗ α ::: ι) (prod.diag (α := α ::: ι))
Tactic: simp only [lastFun_from_append1_drop_last, lastFun_toSubtype, lastFun_appendFun,
      lastFun_subtypeVal, Function.id_comp, lastFun_comp, lastFun_prod]