-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
α : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst : MvFunctor F
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst_1 : LawfulMvFunctor F
x y : F α
simp :
  ∀ (u : F fun (i : Fin2 n) ↦ { p : α i × α i // ofRepeat (R i (prod.mk (α := α) (β := α) i p.1 p.2)) }),
    map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // ofRepeat (R i (prod.mk (α := α) (β := α) i p.1 p.2)) })
            (β := α)
            (fun (i : Fin2 n) (t : { p : α i × α i // ofRepeat (R i (prod.mk (α := α) (β := α) i p.1 p.2)) }) ↦
              (↑t : α i × α i).1)
            u =
          x ∧
        map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // ofRepeat (R i (prod.mk (α := α) (β := α) i p.1 p.2)) })
            (β := α)
            (fun (i : Fin2 n) (t : { p : α i × α i // ofRepeat (R i (prod.mk (α := α) (β := α) i p.1 p.2)) }) ↦
              (↑t : α i × α i).2)
            u =
          y ↔
      map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // ofRepeat (R i (prod.mk (α := α) (β := α) i p.1 p.2)) })
            (β := α)
            (comp (α := fun (i : Fin2 n) ↦ { p : α i × α i // ofRepeat (R i (prod.mk (α := α) (β := α) i p.1 p.2)) })
              (β := α ⊗ α) (γ := α) (prod.fst (α := α) (β := α))
              fun (i : Fin2 n) (x : { x : α i × α i // ofRepeat (R i (prod.mk (α := α) (β := α) i x.1 x.2)) }) ↦
              prod.mk (α := α) (β := α) i (↑x : α i × α i).1 (↑x : α i × α i).2)
            u =
          x ∧
        map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // ofRepeat (R i (prod.mk (α := α) (β := α) i p.1 p.2)) })
            (β := α)
            (comp (α := fun (i : Fin2 n) ↦ { p : α i × α i // ofRepeat (R i (prod.mk (α := α) (β := α) i p.1 p.2)) })
              (β := α ⊗ α) (γ := α) (prod.snd (α := α) (β := α))
              fun (i : Fin2 n) (x : { x : α i × α i // ofRepeat (R i (prod.mk (α := α) (β := α) i x.1 x.2)) }) ↦
              prod.mk (α := α) (β := α) i (↑x : α i × α i).1 (↑x : α i × α i).2)
            u =
          y
⊢ ∀
    (u :
      F fun (i : Fin2 n) ↦
        { p : α i × α i //
          (fun (i : Fin2 n) (x y : α i) ↦ ofRepeat (R i (prod.mk (α := α) (β := α) i x y))) i p.1 p.2 }),
    map (F := F) (α := fun (i : Fin2 n) ↦
            { p : α i × α i //
              (fun (i : Fin2 n) (x y : α i) ↦ ofRepeat (R i (prod.mk (α := α) (β := α) i x y))) i p.1 p.2 })
            (β := α)
            (fun (i : Fin2 n)
                (t :
                  { p : α i × α i //
                    (fun (i : Fin2 n) (x y : α i) ↦ ofRepeat (R i (prod.mk (α := α) (β := α) i x y))) i p.1 p.2 }) ↦
              (↑t : α i × α i).1)
            u =
          x ∧
        map (F := F) (α := fun (i : Fin2 n) ↦
            { p : α i × α i //
              (fun (i : Fin2 n) (x y : α i) ↦ ofRepeat (R i (prod.mk (α := α) (β := α) i x y))) i p.1 p.2 })
            (β := α)
            (fun (i : Fin2 n)
                (t :
                  { p : α i × α i //
                    (fun (i : Fin2 n) (x y : α i) ↦ ofRepeat (R i (prod.mk (α := α) (β := α) i x y))) i p.1 p.2 }) ↦
              (↑t : α i × α i).2)
            u =
          y ↔
      map (F := F) (α := Subtype_ (α := α ⊗ α) R) (β := α)
            (comp (α := Subtype_ (α := α ⊗ α) R) (β := α ⊗ α) (γ := α) (prod.fst (α := α) (β := α))
              (subtypeVal (α := α ⊗ α) R))
            (map (F := F) (α := fun (i : Fin2 n) ↦
              { p : α i × α i //
                (fun (i : Fin2 n) (x y : α i) ↦ ofRepeat (R i (prod.mk (α := α) (β := α) i x y))) i p.1 p.2 })
              (β := Subtype_ (α := α ⊗ α) R) (toSubtype' (α := α) R) u) =
          x ∧
        map (F := F) (α := Subtype_ (α := α ⊗ α) R) (β := α)
            (comp (α := Subtype_ (α := α ⊗ α) R) (β := α ⊗ α) (γ := α) (prod.snd (α := α) (β := α))
              (subtypeVal (α := α ⊗ α) R))
            (map (F := F) (α := fun (i : Fin2 n) ↦
              { p : α i × α i //
                (fun (i : Fin2 n) (x y : α i) ↦ ofRepeat (R i (prod.mk (α := α) (β := α) i x y))) i p.1 p.2 })
              (β := Subtype_ (α := α ⊗ α) R) (toSubtype' (α := α) R) u) =
          y

Tactic:
simp only [map_map, comp_assoc, subtypeVal_toSubtype']

Premises used: TypeVec.comp_assoc, MvFunctor.map_map, TypeVec.subtypeVal_toSubtype'