-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (hypothesis)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₁, v₃, u₁, u₃} A C
H : Functor.{v₂, v₄, u₂, u₄} B D
L₁ : Functor.{v₁, v₂, u₁, u₂} A B
R₁ : Functor.{v₂, v₁, u₂, u₁} B A
L₂ : Functor.{v₁, v₂, u₁, u₂} A B
R₂ : Functor.{v₂, v₁, u₂, u₁} B A
L₃ : Functor.{v₃, v₄, u₃, u₄} C D
R₃ : Functor.{v₄, v₃, u₄, u₃} D C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : L₂ ⟶ L₁
β : TwoSquare G L₂ L₃ H
b : B
vcomp :
  (mateEquiv adj₁ adj₃ : (a : TwoSquare (𝟭 A ⋙ G) L₁ L₃ (𝟭 B ⋙ H)) → TwoSquare R₁ (𝟭 B ⋙ H) (𝟭 A ⋙ G) R₃)
      (TwoSquare.mk (𝟭 A ⋙ G) L₁ L₃ (𝟭 B ⋙ H)
        (Iso.hom (associator (𝟭 A) G L₃) ≫
          whiskerLeft (𝟭 A) β.natTrans ≫
            Iso.inv (associator (𝟭 A) L₂ H) ≫
              whiskerRight (natTrans (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)) H ≫ (L₁.associator (𝟭 B) H).hom)) =
    TwoSquare.mk R₁ (𝟭 B ⋙ H) (𝟭 A ⋙ G) R₃
      ((R₁.associator (𝟭 A) G).inv ≫
        whiskerRight
            (natTrans
              ((mateEquiv adj₁ adj₂ : (a : TwoSquare (𝟭 A) L₁ L₂ (𝟭 B)) → TwoSquare R₁ (𝟭 B) (𝟭 A) R₂)
                (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)))
            G ≫
          Iso.hom (associator (𝟭 B) R₂ G) ≫
            whiskerLeft (𝟭 B) (natTrans ((mateEquiv adj₂ adj₃ : (a : TwoSquare G L₂ L₃ H) → TwoSquare R₂ H G R₃) β)) ≫
              Iso.inv (associator (𝟭 B) H R₃))
vcompb :
  app
      ((mateEquiv adj₁ adj₃ : (a : TwoSquare (𝟭 A ⋙ G) L₁ L₃ (𝟭 B ⋙ H)) → TwoSquare R₁ (𝟭 B ⋙ H) (𝟭 A ⋙ G) R₃)
        (TwoSquare.mk (𝟭 A ⋙ G) L₁ L₃ (𝟭 B ⋙ H)
          (Iso.hom (associator (𝟭 A) G L₃) ≫
            whiskerLeft (𝟭 A) β.natTrans ≫
              Iso.inv (associator (𝟭 A) L₂ H) ≫
                whiskerRight (natTrans (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)) H ≫ (L₁.associator (𝟭 B) H).hom)))
      b =
    (TwoSquare.mk R₁ (𝟭 B ⋙ H) (𝟭 A ⋙ G) R₃
          ((R₁.associator (𝟭 A) G).inv ≫
            whiskerRight
                (natTrans
                  ((mateEquiv adj₁ adj₂ : (a : TwoSquare (𝟭 A) L₁ L₂ (𝟭 B)) → TwoSquare R₁ (𝟭 B) (𝟭 A) R₂)
                    (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)))
                G ≫
              Iso.hom (associator (𝟭 B) R₂ G) ≫
                whiskerLeft (𝟭 B)
                    (natTrans ((mateEquiv adj₂ adj₃ : (a : TwoSquare G L₂ L₃ H) → TwoSquare R₂ H G R₃) β)) ≫
                  Iso.inv (associator (𝟭 B) H R₃))).app
      b
⊢ Eq.{v₃ + 1} (α := (R₁ ⋙ G).obj b ⟶ (H ⋙ R₃).obj b)
    (app (natTrans ((mateEquiv adj₁ adj₃ : (a : TwoSquare G L₁ L₃ H) → TwoSquare R₁ H G R₃) (β.whiskerLeft α))) b)
    (app
      (natTrans
        (TwoSquare.whiskerTop (T' := R₂) ((mateEquiv adj₂ adj₃ : (a : TwoSquare G L₂ L₃ H) → TwoSquare R₂ H G R₃) β)
          ((conjugateEquiv adj₁ adj₂ : (a : L₂ ⟶ L₁) → R₁ ⟶ R₂) α)))
      b)
have vcompb₁ : adj₃.unit.app (G.obj (R₁.obj b)) ≫
    R₃.map (β.natTrans.app (R₁.obj b)) ≫ R₃.map (H.map (α.app (R₁.obj b))) ≫ R₃.map (H.map (adj₁.counit.app b)) =
  G.map (adj₂.unit.app (R₁.obj b)) ≫
    G.map (R₂.map (α.app (R₁.obj b))) ≫
      G.map (R₂.map (adj₁.counit.app b)) ≫
        adj₃.unit.app (G.obj (R₂.obj b)) ≫ R₃.map (β.natTrans.app (R₂.obj b)) ≫ R₃.map (H.map (adj₂.counit.app b))
Tactic: simp only [comp_obj, id_obj, whiskerRight_comp, assoc, mateEquiv_apply, whiskerLeft_comp,
    whiskerLeft_twice, comp_app, Functor.whiskerLeft_app, Functor.whiskerRight_app,
    associator_hom_app, map_id, associator_inv_app, leftUnitor_hom_app, rightUnitor_inv_app,
    Functor.comp_map, Functor.id_map, id_comp, whiskerRight_twice, Iso.inv_hom_id_assoc,
    comp_id] at vcompb
Cleared hypotheses: vcompb