-- 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 (α ::: β)
h₀ :
  comp (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i × (α ::: β) i // α.RelLast rr p_1.1 p_1.2 }) (β :=
      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 α)
      (g' rr n α) =
    TypeVec.id (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i × (α ::: β) i // α.RelLast rr p_1.1 p_1.2 })
h₁ :
  ∀
    (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
⊢ (∃ (u :
      F fun (i : Fin2 (n + 1)) ↦
        { p : (α ::: β) i × (α ::: β) i //
          ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p.1 p.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) ↔
    ∃ (u : F fun (i : Fin2 (n + 1)) ↦ { p : (α ::: β) i × (α ::: β) i // α.RelLast rr p.1 p.2 }),
      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)
            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)
            u =
          y

Tactic:
apply exists_iff_exists_of_mono F (f' rr _ _) (g' rr _ _)

Premises used: _private.0.MvFunctor.f', _private.0.MvFunctor.g', MvFunctor.exists_iff_exists_of_mono