-- 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 (α ::: β)
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 })
⊢ (∃ (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
have 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
Tactic: apply exists_iff_exists_of_mono F (f' rr _ _) (g' rr _ _)