-- 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_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:
apply iff_of_eq

Premises used: iff_of_eq