-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L₁ L₂ L₃ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ R₂ R₃ : Functor.{v₂, v₁, u₂, u₁} D C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : L₂ ⟶ L₁
β : L₃ ⟶ L₂
d : D
vcomp :
  Eq (α := TwoSquare R₁ (𝟭 D ⋙ 𝟭 D) (𝟭 C ⋙ 𝟭 C) R₃)
    ((mateEquiv adj₁ adj₃ : (a : TwoSquare (𝟭 C ⋙ 𝟭 C) L₁ L₃ (𝟭 D ⋙ 𝟭 D)) → TwoSquare R₁ (𝟭 D ⋙ 𝟭 D) (𝟭 C ⋙ 𝟭 C) R₃)
        ((L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) ≫ₕ L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv) :
      TwoSquare R₁ (𝟭 D ⋙ 𝟭 D) (𝟭 C ⋙ 𝟭 C) R₃)
    (vComp (B := R₂)
        ((mateEquiv adj₁ adj₂ : (a : TwoSquare (𝟭 C) L₁ L₂ (𝟭 D)) → TwoSquare R₁ (𝟭 D) (𝟭 C) R₂)
          (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv))
        ((mateEquiv adj₂ adj₃ : (a : TwoSquare (𝟭 C) L₂ L₃ (𝟭 D)) → TwoSquare R₂ (𝟭 D) (𝟭 C) R₃)
          (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)) :
      TwoSquare R₁ (𝟭 D ⋙ 𝟭 D) (𝟭 C ⋙ 𝟭 C) R₃)
vcompd :
  Eq.{v₁ + 1} (α := (R₁ ⋙ 𝟭 C ⋙ 𝟭 C).obj d ⟶ ((𝟭 D ⋙ 𝟭 D) ⋙ R₃).obj d)
    (app
      ((mateEquiv adj₁ adj₃ : (a : TwoSquare (𝟭 C ⋙ 𝟭 C) L₁ L₃ (𝟭 D ⋙ 𝟭 D)) → TwoSquare R₁ (𝟭 D ⋙ 𝟭 D) (𝟭 C ⋙ 𝟭 C) R₃)
        ((L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) ≫ₕ L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv))
      d)
    (app
      (vComp (B := R₂)
        ((mateEquiv adj₁ adj₂ : (a : TwoSquare (𝟭 C) L₁ L₂ (𝟭 D)) → TwoSquare R₁ (𝟭 D) (𝟭 C) R₂)
          (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv))
        ((mateEquiv adj₂ adj₃ : (a : TwoSquare (𝟭 C) L₂ L₃ (𝟭 D)) → TwoSquare R₂ (𝟭 D) (𝟭 C) R₃)
          (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)))
      d)
⊢ (𝟙 (R₁.obj d) ≫
        (𝟙 (R₁.obj d) ≫
            adj₂.unit.app (R₁.obj d) ≫
              𝟙 (R₂.obj (L₂.obj (R₁.obj d))) ≫
                𝟙 (R₂.obj (L₂.obj (R₁.obj d))) ≫
                  R₂.map (𝟙 (L₂.obj (R₁.obj d)) ≫ α.app (R₁.obj d) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫
                    𝟙 (R₂.obj (L₁.obj (R₁.obj d))) ≫
                      𝟙 (R₂.obj (L₁.obj (R₁.obj d))) ≫ R₂.map (adj₁.counit.app d) ≫ 𝟙 (R₂.obj d)) ≫
          𝟙 (R₂.obj d)) ≫
      𝟙 (R₂.obj d) ≫
        (𝟙 (R₂.obj d) ≫
            adj₃.unit.app (R₂.obj d) ≫
              𝟙 (R₃.obj (L₃.obj (R₂.obj d))) ≫
                𝟙 (R₃.obj (L₃.obj (R₂.obj d))) ≫
                  R₃.map (𝟙 (L₃.obj (R₂.obj d)) ≫ β.app (R₂.obj d) ≫ 𝟙 (L₂.obj (R₂.obj d))) ≫
                    𝟙 (R₃.obj (L₂.obj (R₂.obj d))) ≫
                      𝟙 (R₃.obj (L₂.obj (R₂.obj d))) ≫ R₃.map (adj₂.counit.app d) ≫ 𝟙 (R₃.obj d)) ≫
          𝟙 (R₃.obj d) =
    𝟙 (R₁.obj d) ≫
      (𝟙 (R₁.obj d) ≫
          adj₃.unit.app (R₁.obj d) ≫
            𝟙 (R₃.obj (L₃.obj (R₁.obj d))) ≫
              𝟙 (R₃.obj (L₃.obj (R₁.obj d))) ≫
                R₃.map (𝟙 (L₃.obj (R₁.obj d)) ≫ (β.app (R₁.obj d) ≫ α.app (R₁.obj d)) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫
                  𝟙 (R₃.obj (L₁.obj (R₁.obj d))) ≫
                    𝟙 (R₃.obj (L₁.obj (R₁.obj d))) ≫ R₃.map (adj₁.counit.app d) ≫ 𝟙 (R₃.obj d)) ≫
        𝟙 (R₃.obj d)
have w : ∀
  (vcompd :
    adj₃.unit.app (R₁.obj d) ≫ R₃.map (β.app (R₁.obj d)) ≫ R₃.map (α.app (R₁.obj d)) ≫ R₃.map (adj₁.counit.app d) =
      adj₂.unit.app (R₁.obj d) ≫
        R₂.map (α.app (R₁.obj d)) ≫
          R₂.map (adj₁.counit.app d) ≫
            adj₃.unit.app (R₂.obj d) ≫ R₃.map (β.app (R₂.obj d)) ≫ R₃.map (adj₂.counit.app d)),
  adj₂.unit.app (R₁.obj d) ≫
      R₂.map (α.app (R₁.obj d)) ≫
        R₂.map (adj₁.counit.app d) ≫ adj₃.unit.app (R₂.obj d) ≫ R₃.map (β.app (R₂.obj d)) ≫ R₃.map (adj₂.counit.app d) =
    adj₃.unit.app (R₁.obj d) ≫ R₃.map (β.app (R₁.obj d)) ≫ R₃.map (α.app (R₁.obj d)) ≫ R₃.map (adj₁.counit.app d)
Tactic: simp only [comp_obj, id_obj, mateEquiv_apply, comp_app, rightUnitor_inv_app,
    Functor.whiskerLeft_app, associator_hom_app, associator_inv_app, Functor.whiskerRight_app,
    hComp_app, leftUnitor_hom_app, comp_id, id_comp, Functor.id_map, map_comp, Functor.comp_map,
    assoc, whiskerRight_comp, whiskerLeft_comp, vComp_app, map_id] at vcompd ⊢
Cleared hypotheses: vcompd