-- 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
⊢ dropFun (α := α ::: ι) (β := α ::: ι' ⊗ α ::: ι')
      (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))))) =
    dropFun (α := α ::: ι) (β := α ::: ι' ⊗ α ::: ι')
      (TypeVec.comp (α := α ::: ι) (β := α ::: ι ⊗ α ::: ι) (γ := α ::: ι' ⊗ α ::: ι')
        (prod.map (α := α ::: ι) (α' := α ::: ι) (β := α ::: ι') (β' := α ::: ι')
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g))
        (prod.diag (α := α ::: ι)))
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 (α := α)))) =
  TypeVec.comp (α := (α ::: ι).drop) (β := (α ::: ι ⊗ α ::: ι).drop) (γ := (α ::: ι' ⊗ α ::: ι').drop)
    (prod.map (α := (α ::: ι).drop) (α' := (α ::: ι).drop) (β := (α ::: ι').drop) (β' := (α ::: ι').drop)
      (TypeVec.id (α := α)) (TypeVec.id (α := α)))
    (prod.diag (α := (α ::: ι).drop))
Tactic: dsimp