-- 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
⊢ TypeVec.comp (α := (α ::: ι).drop) (β := (Subtype_ (α := α ::: ι' ⊗ α ::: ι') (α.RelLast' R)).drop) (γ :=
      (α ::: ι' ⊗ α ::: ι').drop) (subtypeVal (α := (α ::: ι' ⊗ α ::: ι').drop) α.repeatEq)
      (TypeVec.comp (α := (α ::: ι).drop) (β :=
        TypeVec.drop fun (i : Fin2 (n + 1)) ↦ { x : (α ::: ι' ⊗ α ::: ι') i // ofRepeat (α.RelLast' R i x) }) (γ :=
        (Subtype_ (α := α ::: ι' ⊗ α ::: ι') (α.RelLast' R)).drop)
        (toSubtype (α := fun (i : Fin2 n) ↦ (α ::: ι' ⊗ α ::: ι') i.fs) fun (i : Fin2 n) ↦ α.RelLast' R i.fs)
        (TypeVec.comp (α := (α ::: ι).drop) (β :=
          (Subtype_ (α := α ⊗ α) α.repeatEq ::: { x : ι' × ι' // uncurry R x }).drop) (γ :=
          TypeVec.drop
            ((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) }))
          (dropFun (α := 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)
          (diagSub (α := α)))) =
    TypeVec.comp (α := (α ::: ι).drop) (β := (α ::: ι ⊗ α ::: ι).drop) (γ := (α ::: ι' ⊗ α ::: ι').drop)
      (prod.map (α := (α ::: ι).drop) (α' := (α ::: ι).drop) (β := (α ::: ι').drop) (β' := (α ::: ι').drop)
        (TypeVec.id (α := α)) (TypeVec.id (α := α)))
      (prod.diag (α := (α ::: ι).drop))
have h₀ : TypeVec.comp (α := (α ::: ι).drop) (β := (Subtype_ (α := α ::: ι' ⊗ α ::: ι') (α.RelLast' R)).drop) (γ :=
    (α ::: ι' ⊗ α ::: ι').drop) (subtypeVal (α := (α ::: ι' ⊗ α ::: ι').drop) α.repeatEq)
    (TypeVec.comp (α := (α ::: ι).drop) (β :=
      TypeVec.drop fun (i : Fin2 (n + 1)) ↦ { x : (α ::: ι' ⊗ α ::: ι') i // ofRepeat (α.RelLast' R i x) }) (γ :=
      (Subtype_ (α := α ::: ι' ⊗ α ::: ι') (α.RelLast' R)).drop)
      (toSubtype (α := fun (i : Fin2 n) ↦ (α ::: ι' ⊗ α ::: ι') i.fs) fun (i : Fin2 n) ↦ α.RelLast' R i.fs)
      (TypeVec.comp (α := (α ::: ι).drop) (β :=
        (Subtype_ (α := α ⊗ α) α.repeatEq ::: { x : ι' × ι' // uncurry R x }).drop) (γ :=
        TypeVec.drop
          ((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) }))
        (dropFun (α := 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)
        (diagSub (α := α)))) =
  prod.diag (α := (α ::: ι).drop)
Tactic: simp only [prod_map_id, TypeVec.id_comp]