-- 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₀ :
  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))
⊢ 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 (α := α ::: ι)))

Tactic:
dsimp