-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
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
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 (α := α ::: ι))
⊢ 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 (α := α ::: ι)))

Tactic:
simp only [lastFun_from_append1_drop_last, lastFun_toSubtype, lastFun_appendFun,
      lastFun_subtypeVal, Function.id_comp, lastFun_comp, lastFun_prod]

Premises used: TypeVec.lastFun_toSubtype, TypeVec.lastFun_comp, TypeVec.lastFun_subtypeVal, TypeVec.lastFun_from_append1_drop_last, TypeVec.lastFun_prod, TypeVec.lastFun_appendFun, Function.id_comp