-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (hypothesis)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d e f x y z : B
g₁ : a ⟶ d
h₁ : b ⟶ e
k₁ : c ⟶ f
g₂ : d ⟶ x
h₂ : e ⟶ y
k₂ : f ⟶ z
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : b ⟶ c
r₂ : c ⟶ b
l₃ : d ⟶ e
r₃ : e ⟶ d
l₄ : e ⟶ f
r₄ : f ⟶ e
l₅ : x ⟶ y
r₅ : y ⟶ x
l₆ : y ⟶ z
r₆ : z ⟶ y
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
adj₄ : l₄ ⊣ r₄
adj₅ : l₅ ⊣ r₅
adj₆ : l₆ ⊣ r₆
α : g₁ ≫ l₃ ⟶ l₁ ≫ h₁
β : h₁ ≫ l₄ ⟶ l₂ ≫ k₁
γ : g₂ ≫ l₅ ⟶ l₃ ≫ h₂
δ : h₂ ≫ l₆ ⟶ l₄ ≫ k₂
vcomp :
  Eq (α := (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
    ((mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆) :
          (a_1 : (g₁ ≫ g₂) ≫ l₅ ≫ l₆ ⟶ (l₁ ≫ l₂) ≫ k₁ ≫ k₂) → (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
        (leftAdjointSquare.vcomp (leftAdjointSquare.hcomp α β) (leftAdjointSquare.hcomp γ δ)) :
      (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
    (rightAdjointSquare.vcomp (r₂ := r₄ ≫ r₃)
        ((mateEquiv (adj₁.comp adj₂) (adj₃.comp adj₄) :
            (a_1 : g₁ ≫ l₃ ≫ l₄ ⟶ (l₁ ≫ l₂) ≫ k₁) → (r₂ ≫ r₁) ≫ g₁ ⟶ k₁ ≫ r₄ ≫ r₃)
          (leftAdjointSquare.hcomp α β))
        ((mateEquiv (adj₃.comp adj₄) (adj₅.comp adj₆) :
            (a : g₂ ≫ l₅ ≫ l₆ ⟶ (l₃ ≫ l₄) ≫ k₂) → (r₄ ≫ r₃) ≫ g₂ ⟶ k₂ ≫ r₆ ≫ r₅)
          (leftAdjointSquare.hcomp γ δ)) :
      (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
hcomp1 :
  Eq (α := (r₂ ≫ r₁) ≫ g₁ ⟶ k₁ ≫ r₄ ≫ r₃)
    ((mateEquiv (adj₁.comp adj₂) (adj₃.comp adj₄) :
          (a_1 : g₁ ≫ l₃ ≫ l₄ ⟶ (l₁ ≫ l₂) ≫ k₁) → (r₂ ≫ r₁) ≫ g₁ ⟶ k₁ ≫ r₄ ≫ r₃)
        (leftAdjointSquare.hcomp α β) :
      (r₂ ≫ r₁) ≫ g₁ ⟶ k₁ ≫ r₄ ≫ r₃)
    (rightAdjointSquare.hcomp (h := h₁) ((mateEquiv adj₁ adj₃ : (a_1 : g₁ ≫ l₃ ⟶ l₁ ≫ h₁) → r₁ ≫ g₁ ⟶ h₁ ≫ r₃) α)
        ((mateEquiv adj₂ adj₄ : (a : h₁ ≫ l₄ ⟶ l₂ ≫ k₁) → r₂ ≫ h₁ ⟶ k₁ ≫ r₄) β) :
      (r₂ ≫ r₁) ≫ g₁ ⟶ k₁ ≫ r₄ ≫ r₃)
hcomp2 :
  Eq (α := (r₄ ≫ r₃) ≫ g₂ ⟶ k₂ ≫ r₆ ≫ r₅)
    ((mateEquiv (adj₃.comp adj₄) (adj₅.comp adj₆) : (a : g₂ ≫ l₅ ≫ l₆ ⟶ (l₃ ≫ l₄) ≫ k₂) → (r₄ ≫ r₃) ≫ g₂ ⟶ k₂ ≫ r₆ ≫ r₅)
        (leftAdjointSquare.hcomp γ δ) :
      (r₄ ≫ r₃) ≫ g₂ ⟶ k₂ ≫ r₆ ≫ r₅)
    (rightAdjointSquare.hcomp (h := h₂) ((mateEquiv adj₃ adj₅ : (a : g₂ ≫ l₅ ⟶ l₃ ≫ h₂) → r₃ ≫ g₂ ⟶ h₂ ≫ r₅) γ)
        ((mateEquiv adj₄ adj₆ : (a : h₂ ≫ l₆ ⟶ l₄ ≫ k₂) → r₄ ≫ h₂ ⟶ k₂ ≫ r₆) δ) :
      (r₄ ≫ r₃) ≫ g₂ ⟶ k₂ ≫ r₆ ≫ r₅)
⊢ Eq (α := (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
    ((mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆) :
          (a_1 : (g₁ ≫ g₂) ≫ l₅ ≫ l₆ ⟶ (l₁ ≫ l₂) ≫ k₁ ≫ k₂) → (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
        (leftAdjointSquare.comp α β γ δ) :
      (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
    (rightAdjointSquare.comp (e := e) (h₁ := h₁) (h₂ := h₂) (r₃ := r₃) (r₄ := r₄)
        ((mateEquiv adj₁ adj₃ : (a_1 : g₁ ≫ l₃ ⟶ l₁ ≫ h₁) → r₁ ≫ g₁ ⟶ h₁ ≫ r₃) α)
        ((mateEquiv adj₂ adj₄ : (a : h₁ ≫ l₄ ⟶ l₂ ≫ k₁) → r₂ ≫ h₁ ⟶ k₁ ≫ r₄) β)
        ((mateEquiv adj₃ adj₅ : (a : g₂ ≫ l₅ ⟶ l₃ ≫ h₂) → r₃ ≫ g₂ ⟶ h₂ ≫ r₅) γ)
        ((mateEquiv adj₄ adj₆ : (a : h₂ ≫ l₆ ⟶ l₄ ≫ k₂) → r₄ ≫ h₂ ⟶ k₂ ≫ r₆) δ) :
      (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
have vcomp₁ : Eq (α := (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
  ((mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆) :
        (a_1 : (g₁ ≫ g₂) ≫ l₅ ≫ l₆ ⟶ (l₁ ≫ l₂) ≫ k₁ ≫ k₂) → (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
      (leftAdjointSquare.vcomp (leftAdjointSquare.hcomp α β) (leftAdjointSquare.hcomp γ δ)) :
    (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
  (rightAdjointSquare.vcomp (r₂ := r₄ ≫ r₃)
      (rightAdjointSquare.hcomp (h := h₁) ((mateEquiv adj₁ adj₃ : (a_1 : g₁ ≫ l₃ ⟶ l₁ ≫ h₁) → r₁ ≫ g₁ ⟶ h₁ ≫ r₃) α)
        ((mateEquiv adj₂ adj₄ : (a : h₁ ≫ l₄ ⟶ l₂ ≫ k₁) → r₂ ≫ h₁ ⟶ k₁ ≫ r₄) β))
      (rightAdjointSquare.hcomp (h := h₂) ((mateEquiv adj₃ adj₅ : (a : g₂ ≫ l₅ ⟶ l₃ ≫ h₂) → r₃ ≫ g₂ ⟶ h₂ ≫ r₅) γ)
        ((mateEquiv adj₄ adj₆ : (a : h₂ ≫ l₆ ⟶ l₄ ≫ k₂) → r₄ ≫ h₂ ⟶ k₂ ≫ r₆) δ)) :
    (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
Tactic: rw [hcomp1, hcomp2] at vcomp
Cleared hypotheses: vcomp, hcomp1, hcomp2