-- Lean 4 proof step from Mathlib.Control.Functor.Multivariate (goal)
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)) }
⊢ 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
have 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
Tactic: simp +unfoldPartialApp only [map_map, TypeVec.comp]