-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x y : F (α ::: β)
u :
  F fun (i : Fin2 (n + 1)) ↦
    { p_1 : (α ::: β) i × (α ::: β) i //
      ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p_1.1 p_1.2)) }
h₁ :
  map (F := F) (α := fun (i : Fin2 (n + 1)) ↦
          { p : (α ::: β) i × (α ::: β) i //
            ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p.1 p.2)) })
          (β := α ::: β)
          (fun (i : Fin2 (n + 1))
              (t :
                { p : (α ::: β) i × (α ::: β) i //
                  ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p.1 p.2)) }) ↦
            (↑t : (α ::: β) i × (α ::: β) i).1)
          u =
        x ∧
      map (F := F) (α := fun (i : Fin2 (n + 1)) ↦
          { p : (α ::: β) i × (α ::: β) i //
            ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p.1 p.2)) })
          (β := α ::: β)
          (fun (i : Fin2 (n + 1))
              (t :
                { p : (α ::: β) i × (α ::: β) i //
                  ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p.1 p.2)) }) ↦
            (↑t : (α ::: β) i × (α ::: β) i).2)
          u =
        y ↔
    map (F := F) (α := fun (i : Fin2 (n + 1)) ↦
          { p_1 : (α ::: β) i × (α ::: β) i //
            ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p_1.1 p_1.2)) })
          (β := α ::: β)
          (fun (i : Fin2 (n + 1))
              (x :
                { p_1 : (α ::: β) i × (α ::: β) i //
                  ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p_1.1 p_1.2)) }) ↦
            (↑(f' rr n α i x) : (α ::: β) i × (α ::: β) i).1)
          u =
        x ∧
      map (F := F) (α := fun (i : Fin2 (n + 1)) ↦
          { p_1 : (α ::: β) i × (α ::: β) i //
            ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p_1.1 p_1.2)) })
          (β := α ::: β)
          (fun (i : Fin2 (n + 1))
              (x :
                { p_1 : (α ::: β) i × (α ::: β) i //
                  ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p_1.1 p_1.2)) }) ↦
            (↑(f' rr n α i x) : (α ::: β) i × (α ::: β) i).2)
          u =
        y
⊢ map (F := F) (α := fun (i : Fin2 (n + 1)) ↦
          { p : (α ::: β) i × (α ::: β) i //
            ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p.1 p.2)) })
          (β := α ::: β)
          (fun (i : Fin2 (n + 1))
              (t :
                { p : (α ::: β) i × (α ::: β) i //
                  ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p.1 p.2)) }) ↦
            (↑t : (α ::: β) i × (α ::: β) i).1)
          u =
        x ∧
      map (F := F) (α := fun (i : Fin2 (n + 1)) ↦
          { p : (α ::: β) i × (α ::: β) i //
            ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p.1 p.2)) })
          (β := α ::: β)
          (fun (i : Fin2 (n + 1))
              (t :
                { p : (α ::: β) i × (α ::: β) i //
                  ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p.1 p.2)) }) ↦
            (↑t : (α ::: β) i × (α ::: β) i).2)
          u =
        y ↔
    map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { p : (α ::: β) i × (α ::: β) i // α.RelLast rr p.1 p.2 }) (β :=
          α ::: β)
          (fun (i : Fin2 (n + 1)) (t : { p : (α ::: β) i × (α ::: β) i // α.RelLast rr p.1 p.2 }) ↦
            (↑t : (α ::: β) i × (α ::: β) i).1)
          (map (F := F) (α := fun (i : Fin2 (n + 1)) ↦
            { p_1 : (α ::: β) i × (α ::: β) i //
              ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p_1.1 p_1.2)) })
            (β := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i × (α ::: β) i // α.RelLast rr p_1.1 p_1.2 }) (f' rr n α)
            u) =
        x ∧
      map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { p : (α ::: β) i × (α ::: β) i // α.RelLast rr p.1 p.2 }) (β :=
          α ::: β)
          (fun (i : Fin2 (n + 1)) (t : { p : (α ::: β) i × (α ::: β) i // α.RelLast rr p.1 p.2 }) ↦
            (↑t : (α ::: β) i × (α ::: β) i).2)
          (map (F := F) (α := fun (i : Fin2 (n + 1)) ↦
            { p_1 : (α ::: β) i × (α ::: β) i //
              ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p_1.1 p_1.2)) })
            (β := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i × (α ::: β) i // α.RelLast rr p_1.1 p_1.2 }) (f' rr n α)
            u) =
        y

Tactic:
simp +unfoldPartialApp only [map_map, TypeVec.comp]

Premises used: TypeVec.comp, MvFunctor.map_map