awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d e f : B
g : a ⟶ d
h : b ⟶ e
k : c ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : d ⟶ e
r₂ : e ⟶ d
l₃ : b ⟶ c
r₃ : c ⟶ b
l₄ : e ⟶ f
r₄ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
adj₄ : l₄ ⊣ r₄
α : g ≫ l₂ ⟶ l₁ ≫ h
β : h ≫ l₄ ⟶ l₃ ≫ k
_ :
  𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      (r₃ ≫ r₁) ◁ g ◁ (adj₂.unit ⊗≫ l₂ ◁ adj₄.unit ▷ r₂ ⊗≫ 𝟙 ((l₂ ≫ l₄) ≫ r₄ ≫ r₂)) ⊗≫
        (r₃ ≫ r₁) ◁ ((α_ g l₂ l₄).inv ≫ α ▷ l₄ ≫ (α_ l₁ h l₄).hom ≫ l₁ ◁ β ≫ (α_ l₁ l₃ k).inv) ▷ (r₄ ≫ r₂) ⊗≫
          (𝟙 ((r₃ ≫ r₁) ≫ l₁ ≫ l₃) ⊗≫ r₃ ◁ adj₁.counit ▷ l₃ ⊗≫ adj₃.counit) ▷ k ▷ (r₄ ≫ r₂) ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂) =
    𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
        r₃ ◁ r₁ ◁ ((g ≫ l₂) ◁ adj₄.unit ≫ α ▷ (l₄ ≫ r₄)) ▷ r₂ ⊗≫
          r₃ ◁ ((r₁ ≫ l₁) ◁ β ≫ adj₁.counit ▷ (l₃ ≫ k)) ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂)
⊢ 𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      (r₃ ≫ r₁) ◁ g ◁ (adj₂.unit ⊗≫ l₂ ◁ adj₄.unit ▷ r₂ ⊗≫ 𝟙 ((l₂ ≫ l₄) ≫ r₄ ≫ r₂)) ⊗≫
        (r₃ ≫ r₁) ◁ ((α_ g l₂ l₄).inv ≫ α ▷ l₄ ≫ (α_ l₁ h l₄).hom ≫ l₁ ◁ β ≫ (α_ l₁ l₃ k).inv) ▷ (r₄ ≫ r₂) ⊗≫
          (𝟙 ((r₃ ≫ r₁) ≫ l₁ ≫ l₃) ⊗≫ r₃ ◁ adj₁.counit ▷ l₃ ⊗≫ adj₃.counit) ▷ k ▷ (r₄ ≫ r₂) ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂) =
    (α_ r₃ r₁ g).hom ≫
      r₃ ◁ (𝟙 (r₁ ≫ g) ⊗≫ r₁ ◁ g ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h ▷ r₂ ⊗≫ 𝟙 (h ≫ r₂)) ≫
        (α_ r₃ h r₂).inv ≫
          (𝟙 (r₃ ≫ h) ⊗≫ r₃ ◁ h ◁ adj₄.unit ⊗≫ r₃ ◁ β ▷ r₄ ⊗≫ adj₃.counit ▷ k ▷ r₄ ⊗≫ 𝟙 (k ≫ r₄)) ▷ r₂ ≫
            (α_ k r₄ r₂).hom
have _₁ : 𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
    r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
      r₃ ◁ r₁ ◁ ((g ≫ l₂) ◁ adj₄.unit ≫ α ▷ (l₄ ≫ r₄)) ▷ r₂ ⊗≫
        r₃ ◁ ((r₁ ≫ l₁) ◁ β ≫ adj₁.counit ▷ (l₃ ≫ k)) ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂) =
  𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
    r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
      r₃ ◁ r₁ ◁ α ▷ r₂ ⊗≫
        r₃ ◁ ((r₁ ≫ l₁) ◁ h ◁ adj₄.unit ≫ adj₁.counit ▷ (h ≫ l₄ ≫ r₄)) ▷ r₂ ⊗≫
          r₃ ◁ β ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂)
Tactic: calc
    _ = 𝟙 _ ⊗≫ r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
          r₃ ◁ r₁ ◁ ((g ≫ l₂) ◁ adj₄.unit ≫ α ▷ (l₄ ≫ r₄)) ▷ r₂ ⊗≫
            r₃ ◁ ((r₁ ≫ l₁) ◁ β ≫ adj₁.counit ▷ (l₃ ≫ k)) ▷ r₄ ▷ r₂ ⊗≫
              adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 _ ⊗≫ r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫ r₃ ◁ r₁ ◁ α ▷ r₂ ⊗≫
          r₃ ◁ ((r₁ ≫ l₁) ◁ h ◁ adj₄.unit ≫ adj₁.counit ▷ (h ≫ l₄ ≫ r₄)) ▷ r₂ ⊗≫
            r₃ ◁ β ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 _ := by
      rw [whisker_exchange, whisker_exchange]
      bicategory
    _ = _ := by
      rw [whisker_exchange]
      bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d e f : B
g : a ⟶ d
h : b ⟶ e
k : c ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : d ⟶ e
r₂ : e ⟶ d
l₃ : b ⟶ c
r₃ : c ⟶ b
l₄ : e ⟶ f
r₄ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
adj₄ : l₄ ⊣ r₄
α : g ≫ l₂ ⟶ l₁ ≫ h
β : h ≫ l₄ ⟶ l₃ ≫ k
_ :
  𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      (r₃ ≫ r₁) ◁ g ◁ (adj₂.unit ⊗≫ l₂ ◁ adj₄.unit ▷ r₂ ⊗≫ 𝟙 ((l₂ ≫ l₄) ≫ r₄ ≫ r₂)) ⊗≫
        (r₃ ≫ r₁) ◁ ((α_ g l₂ l₄).inv ≫ α ▷ l₄ ≫ (α_ l₁ h l₄).hom ≫ l₁ ◁ β ≫ (α_ l₁ l₃ k).inv) ▷ (r₄ ≫ r₂) ⊗≫
          (𝟙 ((r₃ ≫ r₁) ≫ l₁ ≫ l₃) ⊗≫ r₃ ◁ adj₁.counit ▷ l₃ ⊗≫ adj₃.counit) ▷ k ▷ (r₄ ≫ r₂) ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂) =
    𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
        r₃ ◁ r₁ ◁ ((g ≫ l₂) ◁ adj₄.unit ≫ α ▷ (l₄ ≫ r₄)) ▷ r₂ ⊗≫
          r₃ ◁ ((r₁ ≫ l₁) ◁ β ≫ adj₁.counit ▷ (l₃ ≫ k)) ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂)
_₁ :
  𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
        r₃ ◁ r₁ ◁ ((g ≫ l₂) ◁ adj₄.unit ≫ α ▷ (l₄ ≫ r₄)) ▷ r₂ ⊗≫
          r₃ ◁ ((r₁ ≫ l₁) ◁ β ≫ adj₁.counit ▷ (l₃ ≫ k)) ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂) =
    𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
        r₃ ◁ r₁ ◁ α ▷ r₂ ⊗≫
          r₃ ◁ ((r₁ ≫ l₁) ◁ h ◁ adj₄.unit ≫ adj₁.counit ▷ (h ≫ l₄ ≫ r₄)) ▷ r₂ ⊗≫
            r₃ ◁ β ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂)
⊢ 𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      (r₃ ≫ r₁) ◁ g ◁ (adj₂.unit ⊗≫ l₂ ◁ adj₄.unit ▷ r₂ ⊗≫ 𝟙 ((l₂ ≫ l₄) ≫ r₄ ≫ r₂)) ⊗≫
        (r₃ ≫ r₁) ◁ ((α_ g l₂ l₄).inv ≫ α ▷ l₄ ≫ (α_ l₁ h l₄).hom ≫ l₁ ◁ β ≫ (α_ l₁ l₃ k).inv) ▷ (r₄ ≫ r₂) ⊗≫
          (𝟙 ((r₃ ≫ r₁) ≫ l₁ ≫ l₃) ⊗≫ r₃ ◁ adj₁.counit ▷ l₃ ⊗≫ adj₃.counit) ▷ k ▷ (r₄ ≫ r₂) ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂) =
    (α_ r₃ r₁ g).hom ≫
      r₃ ◁ (𝟙 (r₁ ≫ g) ⊗≫ r₁ ◁ g ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h ▷ r₂ ⊗≫ 𝟙 (h ≫ r₂)) ≫
        (α_ r₃ h r₂).inv ≫
          (𝟙 (r₃ ≫ h) ⊗≫ r₃ ◁ h ◁ adj₄.unit ⊗≫ r₃ ◁ β ▷ r₄ ⊗≫ adj₃.counit ▷ k ▷ r₄ ⊗≫ 𝟙 (k ≫ r₄)) ▷ r₂ ≫
            (α_ k r₄ r₂).hom
have _₂ : 𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
    r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
      r₃ ◁ r₁ ◁ α ▷ r₂ ⊗≫
        r₃ ◁ ((r₁ ≫ l₁) ◁ h ◁ adj₄.unit ≫ adj₁.counit ▷ (h ≫ l₄ ≫ r₄)) ▷ r₂ ⊗≫
          r₃ ◁ β ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂) =
  (α_ r₃ r₁ g).hom ≫
    r₃ ◁ (𝟙 (r₁ ≫ g) ⊗≫ r₁ ◁ g ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h ▷ r₂ ⊗≫ 𝟙 (h ≫ r₂)) ≫
      (α_ r₃ h r₂).inv ≫
        (𝟙 (r₃ ≫ h) ⊗≫ r₃ ◁ h ◁ adj₄.unit ⊗≫ r₃ ◁ β ▷ r₄ ⊗≫ adj₃.counit ▷ k ▷ r₄ ⊗≫ 𝟙 (k ≫ r₄)) ▷ r₂ ≫ (α_ k r₄ r₂).hom
Tactic: calc
    _ = 𝟙 _ ⊗≫ r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
          r₃ ◁ r₁ ◁ ((g ≫ l₂) ◁ adj₄.unit ≫ α ▷ (l₄ ≫ r₄)) ▷ r₂ ⊗≫
            r₃ ◁ ((r₁ ≫ l₁) ◁ β ≫ adj₁.counit ▷ (l₃ ≫ k)) ▷ r₄ ▷ r₂ ⊗≫
              adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 _ ⊗≫ r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫ r₃ ◁ r₁ ◁ α ▷ r₂ ⊗≫
          r₃ ◁ ((r₁ ≫ l₁) ◁ h ◁ adj₄.unit ≫ adj₁.counit ▷ (h ≫ l₄ ≫ r₄)) ▷ r₂ ⊗≫
            r₃ ◁ β ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 _ := by
      rw [whisker_exchange, whisker_exchange]
      bicategory
    _ = _ := by
      rw [whisker_exchange]
      bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (goal)
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
l₂ : b ⟶ c
l₃ : d ⟶ e
l₄ : e ⟶ f
l₅ : x ⟶ y
l₆ : y ⟶ z
α : g₁ ≫ l₃ ⟶ l₁ ≫ h₁
β : h₁ ≫ l₄ ⟶ l₂ ≫ k₁
γ : g₂ ≫ l₅ ⟶ l₃ ≫ h₂
δ : h₂ ≫ l₆ ⟶ l₄ ≫ k₂
⊢ comp α β γ δ = hcomp (vcomp α γ) (vcomp β δ)
have dsimp : (α_ g₁ g₂ (l₅ ≫ l₆)).hom ≫
    g₁ ◁ ((α_ g₂ l₅ l₆).inv ≫ γ ▷ l₆ ≫ (α_ l₃ h₂ l₆).hom ≫ l₃ ◁ δ ≫ (α_ l₃ l₄ k₂).inv) ≫
      (α_ g₁ (l₃ ≫ l₄) k₂).inv ≫
        ((α_ g₁ l₃ l₄).inv ≫ α ▷ l₄ ≫ (α_ l₁ h₁ l₄).hom ≫ l₁ ◁ β ≫ (α_ l₁ l₂ k₁).inv) ▷ k₂ ≫ (α_ (l₁ ≫ l₂) k₁ k₂).hom =
  (α_ (g₁ ≫ g₂) l₅ l₆).inv ≫
    ((α_ g₁ g₂ l₅).hom ≫ g₁ ◁ γ ≫ (α_ g₁ l₃ h₂).inv ≫ α ▷ h₂ ≫ (α_ l₁ h₁ h₂).hom) ▷ l₆ ≫
      (α_ l₁ (h₁ ≫ h₂) l₆).hom ≫
        l₁ ◁ ((α_ h₁ h₂ l₆).hom ≫ h₁ ◁ δ ≫ (α_ h₁ l₄ k₂).inv ≫ β ▷ k₂ ≫ (α_ l₂ k₁ k₂).hom) ≫ (α_ l₁ l₂ (k₁ ≫ k₂)).inv
Tactic: dsimp only [comp, vcomp, hcomp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (goal)
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
l₂ : b ⟶ c
l₃ : d ⟶ e
l₄ : e ⟶ f
l₅ : x ⟶ y
l₆ : y ⟶ z
α : g₁ ≫ l₃ ⟶ l₁ ≫ h₁
β : h₁ ≫ l₄ ⟶ l₂ ≫ k₁
γ : g₂ ≫ l₅ ⟶ l₃ ≫ h₂
δ : h₂ ≫ l₆ ⟶ l₄ ≫ k₂
⊢ 𝟙 ((g₁ ≫ g₂) ≫ l₅ ≫ l₆) ⊗≫ g₁ ◁ γ ▷ l₆ ⊗≫ ((g₁ ≫ l₃) ◁ δ ≫ α ▷ (l₄ ≫ k₂)) ⊗≫ l₁ ◁ β ▷ k₂ ⊗≫ 𝟙 ((l₁ ≫ l₂) ≫ k₁ ≫ k₂) =
    (α_ (g₁ ≫ g₂) l₅ l₆).inv ≫
      ((α_ g₁ g₂ l₅).hom ≫ g₁ ◁ γ ≫ (α_ g₁ l₃ h₂).inv ≫ α ▷ h₂ ≫ (α_ l₁ h₁ h₂).hom) ▷ l₆ ≫
        (α_ l₁ (h₁ ≫ h₂) l₆).hom ≫
          l₁ ◁ ((α_ h₁ h₂ l₆).hom ≫ h₁ ◁ δ ≫ (α_ h₁ l₄ k₂).inv ≫ β ▷ k₂ ≫ (α_ l₂ k₁ k₂).hom) ≫ (α_ l₁ l₂ (k₁ ≫ k₂)).inv
have rw : 𝟙 ((g₁ ≫ g₂) ≫ l₅ ≫ l₆) ⊗≫ g₁ ◁ γ ▷ l₆ ⊗≫ (α ▷ (h₂ ≫ l₆) ≫ (l₁ ≫ h₁) ◁ δ) ⊗≫ l₁ ◁ β ▷ k₂ ⊗≫ 𝟙 ((l₁ ≫ l₂) ≫ k₁ ≫ k₂) =
  (α_ (g₁ ≫ g₂) l₅ l₆).inv ≫
    ((α_ g₁ g₂ l₅).hom ≫ g₁ ◁ γ ≫ (α_ g₁ l₃ h₂).inv ≫ α ▷ h₂ ≫ (α_ l₁ h₁ h₂).hom) ▷ l₆ ≫
      (α_ l₁ (h₁ ≫ h₂) l₆).hom ≫
        l₁ ◁ ((α_ h₁ h₂ l₆).hom ≫ h₁ ◁ δ ≫ (α_ h₁ l₄ k₂).inv ≫ β ▷ k₂ ≫ (α_ l₂ k₁ k₂).hom) ≫ (α_ l₁ l₂ (k₁ ≫ k₂)).inv
Tactic: rw [whisker_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (goal)
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
l₂ : b ⟶ c
l₃ : d ⟶ e
l₄ : e ⟶ f
l₅ : x ⟶ y
l₆ : y ⟶ z
α : g₁ ≫ l₃ ⟶ l₁ ≫ h₁
β : h₁ ≫ l₄ ⟶ l₂ ≫ k₁
γ : g₂ ≫ l₅ ⟶ l₃ ≫ h₂
δ : h₂ ≫ l₆ ⟶ l₄ ≫ k₂
⊢ (α_ g₁ g₂ (l₅ ≫ l₆)).hom ≫
      g₁ ◁ ((α_ g₂ l₅ l₆).inv ≫ γ ▷ l₆ ≫ (α_ l₃ h₂ l₆).hom ≫ l₃ ◁ δ ≫ (α_ l₃ l₄ k₂).inv) ≫
        (α_ g₁ (l₃ ≫ l₄) k₂).inv ≫
          ((α_ g₁ l₃ l₄).inv ≫ α ▷ l₄ ≫ (α_ l₁ h₁ l₄).hom ≫ l₁ ◁ β ≫ (α_ l₁ l₂ k₁).inv) ▷ k₂ ≫
            (α_ (l₁ ≫ l₂) k₁ k₂).hom =
    (α_ (g₁ ≫ g₂) l₅ l₆).inv ≫
      ((α_ g₁ g₂ l₅).hom ≫ g₁ ◁ γ ≫ (α_ g₁ l₃ h₂).inv ≫ α ▷ h₂ ≫ (α_ l₁ h₁ h₂).hom) ▷ l₆ ≫
        (α_ l₁ (h₁ ≫ h₂) l₆).hom ≫
          l₁ ◁ ((α_ h₁ h₂ l₆).hom ≫ h₁ ◁ δ ≫ (α_ h₁ l₄ k₂).inv ≫ β ▷ k₂ ≫ (α_ l₂ k₁ k₂).hom) ≫ (α_ l₁ l₂ (k₁ ≫ k₂)).inv
have _ : (α_ g₁ g₂ (l₅ ≫ l₆)).hom ≫
    g₁ ◁ ((α_ g₂ l₅ l₆).inv ≫ γ ▷ l₆ ≫ (α_ l₃ h₂ l₆).hom ≫ l₃ ◁ δ ≫ (α_ l₃ l₄ k₂).inv) ≫
      (α_ g₁ (l₃ ≫ l₄) k₂).inv ≫
        ((α_ g₁ l₃ l₄).inv ≫ α ▷ l₄ ≫ (α_ l₁ h₁ l₄).hom ≫ l₁ ◁ β ≫ (α_ l₁ l₂ k₁).inv) ▷ k₂ ≫ (α_ (l₁ ≫ l₂) k₁ k₂).hom =
  𝟙 ((g₁ ≫ g₂) ≫ l₅ ≫ l₆) ⊗≫ g₁ ◁ γ ▷ l₆ ⊗≫ ((g₁ ≫ l₃) ◁ δ ≫ α ▷ (l₄ ≫ k₂)) ⊗≫ l₁ ◁ β ▷ k₂ ⊗≫ 𝟙 ((l₁ ≫ l₂) ≫ k₁ ≫ k₂)
Tactic: calc
    _ = 𝟙 _ ⊗≫ g₁ ◁ γ ▷ l₆ ⊗≫ ((g₁ ≫ l₃) ◁ δ ≫ α ▷ (l₄ ≫ k₂)) ⊗≫ l₁ ◁ β ▷ k₂ ⊗≫ 𝟙 _ := by
      bicategory
    _ = _ := by
      rw [whisker_exchange]
      bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (goal)
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
l₂ : b ⟶ c
l₃ : d ⟶ e
l₄ : e ⟶ f
l₅ : x ⟶ y
l₆ : y ⟶ z
α : g₁ ≫ l₃ ⟶ l₁ ≫ h₁
β : h₁ ≫ l₄ ⟶ l₂ ≫ k₁
γ : g₂ ≫ l₅ ⟶ l₃ ≫ h₂
δ : h₂ ≫ l₆ ⟶ l₄ ≫ k₂
_ :
  (α_ g₁ g₂ (l₅ ≫ l₆)).hom ≫
      g₁ ◁ ((α_ g₂ l₅ l₆).inv ≫ γ ▷ l₆ ≫ (α_ l₃ h₂ l₆).hom ≫ l₃ ◁ δ ≫ (α_ l₃ l₄ k₂).inv) ≫
        (α_ g₁ (l₃ ≫ l₄) k₂).inv ≫
          ((α_ g₁ l₃ l₄).inv ≫ α ▷ l₄ ≫ (α_ l₁ h₁ l₄).hom ≫ l₁ ◁ β ≫ (α_ l₁ l₂ k₁).inv) ▷ k₂ ≫
            (α_ (l₁ ≫ l₂) k₁ k₂).hom =
    𝟙 ((g₁ ≫ g₂) ≫ l₅ ≫ l₆) ⊗≫ g₁ ◁ γ ▷ l₆ ⊗≫ ((g₁ ≫ l₃) ◁ δ ≫ α ▷ (l₄ ≫ k₂)) ⊗≫ l₁ ◁ β ▷ k₂ ⊗≫ 𝟙 ((l₁ ≫ l₂) ≫ k₁ ≫ k₂)
⊢ (α_ g₁ g₂ (l₅ ≫ l₆)).hom ≫
      g₁ ◁ ((α_ g₂ l₅ l₆).inv ≫ γ ▷ l₆ ≫ (α_ l₃ h₂ l₆).hom ≫ l₃ ◁ δ ≫ (α_ l₃ l₄ k₂).inv) ≫
        (α_ g₁ (l₃ ≫ l₄) k₂).inv ≫
          ((α_ g₁ l₃ l₄).inv ≫ α ▷ l₄ ≫ (α_ l₁ h₁ l₄).hom ≫ l₁ ◁ β ≫ (α_ l₁ l₂ k₁).inv) ▷ k₂ ≫
            (α_ (l₁ ≫ l₂) k₁ k₂).hom =
    (α_ (g₁ ≫ g₂) l₅ l₆).inv ≫
      ((α_ g₁ g₂ l₅).hom ≫ g₁ ◁ γ ≫ (α_ g₁ l₃ h₂).inv ≫ α ▷ h₂ ≫ (α_ l₁ h₁ h₂).hom) ▷ l₆ ≫
        (α_ l₁ (h₁ ≫ h₂) l₆).hom ≫
          l₁ ◁ ((α_ h₁ h₂ l₆).hom ≫ h₁ ◁ δ ≫ (α_ h₁ l₄ k₂).inv ≫ β ▷ k₂ ≫ (α_ l₂ k₁ k₂).hom) ≫ (α_ l₁ l₂ (k₁ ≫ k₂)).inv
have _₁ : 𝟙 ((g₁ ≫ g₂) ≫ l₅ ≫ l₆) ⊗≫ g₁ ◁ γ ▷ l₆ ⊗≫ ((g₁ ≫ l₃) ◁ δ ≫ α ▷ (l₄ ≫ k₂)) ⊗≫ l₁ ◁ β ▷ k₂ ⊗≫ 𝟙 ((l₁ ≫ l₂) ≫ k₁ ≫ k₂) =
  (α_ (g₁ ≫ g₂) l₅ l₆).inv ≫
    ((α_ g₁ g₂ l₅).hom ≫ g₁ ◁ γ ≫ (α_ g₁ l₃ h₂).inv ≫ α ▷ h₂ ≫ (α_ l₁ h₁ h₂).hom) ▷ l₆ ≫
      (α_ l₁ (h₁ ≫ h₂) l₆).hom ≫
        l₁ ◁ ((α_ h₁ h₂ l₆).hom ≫ h₁ ◁ δ ≫ (α_ h₁ l₄ k₂).inv ≫ β ▷ k₂ ≫ (α_ l₂ k₁ k₂).hom) ≫ (α_ l₁ l₂ (k₁ ≫ k₂)).inv
Tactic: calc
    _ = 𝟙 _ ⊗≫ g₁ ◁ γ ▷ l₆ ⊗≫ ((g₁ ≫ l₃) ◁ δ ≫ α ▷ (l₄ ≫ k₂)) ⊗≫ l₁ ◁ β ▷ k₂ ⊗≫ 𝟙 _ := by
      bicategory
    _ = _ := by
      rw [whisker_exchange]
      bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (goal)
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
r₁ : b ⟶ a
r₂ : c ⟶ b
r₃ : e ⟶ d
r₄ : f ⟶ e
r₅ : y ⟶ x
r₆ : z ⟶ y
α : r₁ ≫ g₁ ⟶ h₁ ≫ r₃
β : r₂ ≫ h₁ ⟶ k₁ ≫ r₄
γ : r₃ ≫ g₂ ⟶ h₂ ≫ r₅
δ : r₄ ≫ h₂ ⟶ k₂ ≫ r₆
⊢ comp α β γ δ = hcomp (vcomp α γ) (vcomp β δ)
have dsimp : (α_ (r₂ ≫ r₁) g₁ g₂).inv ≫
    ((α_ r₂ r₁ g₁).hom ≫ r₂ ◁ α ≫ (α_ r₂ h₁ r₃).inv ≫ β ▷ r₃ ≫ (α_ k₁ r₄ r₃).hom) ▷ g₂ ≫
      (α_ k₁ (r₄ ≫ r₃) g₂).hom ≫
        k₁ ◁ ((α_ r₄ r₃ g₂).hom ≫ r₄ ◁ γ ≫ (α_ r₄ h₂ r₅).inv ≫ δ ▷ r₅ ≫ (α_ k₂ r₆ r₅).hom) ≫ (α_ k₁ k₂ (r₆ ≫ r₅)).inv =
  (α_ r₂ r₁ (g₁ ≫ g₂)).hom ≫
    r₂ ◁ ((α_ r₁ g₁ g₂).inv ≫ α ▷ g₂ ≫ (α_ h₁ r₃ g₂).hom ≫ h₁ ◁ γ ≫ (α_ h₁ h₂ r₅).inv) ≫
      (α_ r₂ (h₁ ≫ h₂) r₅).inv ≫
        ((α_ r₂ h₁ h₂).inv ≫ β ▷ h₂ ≫ (α_ k₁ r₄ h₂).hom ≫ k₁ ◁ δ ≫ (α_ k₁ k₂ r₆).inv) ▷ r₅ ≫ (α_ (k₁ ≫ k₂) r₆ r₅).hom
Tactic: dsimp only [comp, vcomp, hcomp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (goal)
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
r₁ : b ⟶ a
r₂ : c ⟶ b
r₃ : e ⟶ d
r₄ : f ⟶ e
r₅ : y ⟶ x
r₆ : z ⟶ y
α : r₁ ≫ g₁ ⟶ h₁ ≫ r₃
β : r₂ ≫ h₁ ⟶ k₁ ≫ r₄
γ : r₃ ≫ g₂ ⟶ h₂ ≫ r₅
δ : r₄ ≫ h₂ ⟶ k₂ ≫ r₆
⊢ 𝟙 ((r₂ ≫ r₁) ≫ g₁ ≫ g₂) ⊗≫ r₂ ◁ α ▷ g₂ ⊗≫ (β ▷ (r₃ ≫ g₂) ≫ (k₁ ≫ r₄) ◁ γ) ⊗≫ k₁ ◁ δ ▷ r₅ ⊗≫ 𝟙 ((k₁ ≫ k₂) ≫ r₆ ≫ r₅) =
    (α_ r₂ r₁ (g₁ ≫ g₂)).hom ≫
      r₂ ◁ ((α_ r₁ g₁ g₂).inv ≫ α ▷ g₂ ≫ (α_ h₁ r₃ g₂).hom ≫ h₁ ◁ γ ≫ (α_ h₁ h₂ r₅).inv) ≫
        (α_ r₂ (h₁ ≫ h₂) r₅).inv ≫
          ((α_ r₂ h₁ h₂).inv ≫ β ▷ h₂ ≫ (α_ k₁ r₄ h₂).hom ≫ k₁ ◁ δ ≫ (α_ k₁ k₂ r₆).inv) ▷ r₅ ≫ (α_ (k₁ ≫ k₂) r₆ r₅).hom
have rw : 𝟙 ((r₂ ≫ r₁) ≫ g₁ ≫ g₂) ⊗≫ r₂ ◁ α ▷ g₂ ⊗≫ ((r₂ ≫ h₁) ◁ γ ≫ β ▷ (h₂ ≫ r₅)) ⊗≫ k₁ ◁ δ ▷ r₅ ⊗≫ 𝟙 ((k₁ ≫ k₂) ≫ r₆ ≫ r₅) =
  (α_ r₂ r₁ (g₁ ≫ g₂)).hom ≫
    r₂ ◁ ((α_ r₁ g₁ g₂).inv ≫ α ▷ g₂ ≫ (α_ h₁ r₃ g₂).hom ≫ h₁ ◁ γ ≫ (α_ h₁ h₂ r₅).inv) ≫
      (α_ r₂ (h₁ ≫ h₂) r₅).inv ≫
        ((α_ r₂ h₁ h₂).inv ≫ β ▷ h₂ ≫ (α_ k₁ r₄ h₂).hom ≫ k₁ ◁ δ ≫ (α_ k₁ k₂ r₆).inv) ▷ r₅ ≫ (α_ (k₁ ≫ k₂) r₆ r₅).hom
Tactic: rw [← whisker_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (goal)
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
r₁ : b ⟶ a
r₂ : c ⟶ b
r₃ : e ⟶ d
r₄ : f ⟶ e
r₅ : y ⟶ x
r₆ : z ⟶ y
α : r₁ ≫ g₁ ⟶ h₁ ≫ r₃
β : r₂ ≫ h₁ ⟶ k₁ ≫ r₄
γ : r₃ ≫ g₂ ⟶ h₂ ≫ r₅
δ : r₄ ≫ h₂ ⟶ k₂ ≫ r₆
⊢ (α_ (r₂ ≫ r₁) g₁ g₂).inv ≫
      ((α_ r₂ r₁ g₁).hom ≫ r₂ ◁ α ≫ (α_ r₂ h₁ r₃).inv ≫ β ▷ r₃ ≫ (α_ k₁ r₄ r₃).hom) ▷ g₂ ≫
        (α_ k₁ (r₄ ≫ r₃) g₂).hom ≫
          k₁ ◁ ((α_ r₄ r₃ g₂).hom ≫ r₄ ◁ γ ≫ (α_ r₄ h₂ r₅).inv ≫ δ ▷ r₅ ≫ (α_ k₂ r₆ r₅).hom) ≫
            (α_ k₁ k₂ (r₆ ≫ r₅)).inv =
    (α_ r₂ r₁ (g₁ ≫ g₂)).hom ≫
      r₂ ◁ ((α_ r₁ g₁ g₂).inv ≫ α ▷ g₂ ≫ (α_ h₁ r₃ g₂).hom ≫ h₁ ◁ γ ≫ (α_ h₁ h₂ r₅).inv) ≫
        (α_ r₂ (h₁ ≫ h₂) r₅).inv ≫
          ((α_ r₂ h₁ h₂).inv ≫ β ▷ h₂ ≫ (α_ k₁ r₄ h₂).hom ≫ k₁ ◁ δ ≫ (α_ k₁ k₂ r₆).inv) ▷ r₅ ≫ (α_ (k₁ ≫ k₂) r₆ r₅).hom
have _ : (α_ (r₂ ≫ r₁) g₁ g₂).inv ≫
    ((α_ r₂ r₁ g₁).hom ≫ r₂ ◁ α ≫ (α_ r₂ h₁ r₃).inv ≫ β ▷ r₃ ≫ (α_ k₁ r₄ r₃).hom) ▷ g₂ ≫
      (α_ k₁ (r₄ ≫ r₃) g₂).hom ≫
        k₁ ◁ ((α_ r₄ r₃ g₂).hom ≫ r₄ ◁ γ ≫ (α_ r₄ h₂ r₅).inv ≫ δ ▷ r₅ ≫ (α_ k₂ r₆ r₅).hom) ≫ (α_ k₁ k₂ (r₆ ≫ r₅)).inv =
  𝟙 ((r₂ ≫ r₁) ≫ g₁ ≫ g₂) ⊗≫ r₂ ◁ α ▷ g₂ ⊗≫ (β ▷ (r₃ ≫ g₂) ≫ (k₁ ≫ r₄) ◁ γ) ⊗≫ k₁ ◁ δ ▷ r₅ ⊗≫ 𝟙 ((k₁ ≫ k₂) ≫ r₆ ≫ r₅)
Tactic: calc
    _ = 𝟙 _ ⊗≫ r₂ ◁ α ▷ g₂ ⊗≫ (β ▷ (r₃ ≫ g₂) ≫ (k₁ ≫ r₄) ◁ γ) ⊗≫ k₁ ◁ δ ▷ r₅ ⊗≫ 𝟙 _ := by
      bicategory
    _ = _ := by
      rw [← whisker_exchange]
      bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (goal)
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
r₁ : b ⟶ a
r₂ : c ⟶ b
r₃ : e ⟶ d
r₄ : f ⟶ e
r₅ : y ⟶ x
r₆ : z ⟶ y
α : r₁ ≫ g₁ ⟶ h₁ ≫ r₃
β : r₂ ≫ h₁ ⟶ k₁ ≫ r₄
γ : r₃ ≫ g₂ ⟶ h₂ ≫ r₅
δ : r₄ ≫ h₂ ⟶ k₂ ≫ r₆
_ :
  (α_ (r₂ ≫ r₁) g₁ g₂).inv ≫
      ((α_ r₂ r₁ g₁).hom ≫ r₂ ◁ α ≫ (α_ r₂ h₁ r₃).inv ≫ β ▷ r₃ ≫ (α_ k₁ r₄ r₃).hom) ▷ g₂ ≫
        (α_ k₁ (r₄ ≫ r₃) g₂).hom ≫
          k₁ ◁ ((α_ r₄ r₃ g₂).hom ≫ r₄ ◁ γ ≫ (α_ r₄ h₂ r₅).inv ≫ δ ▷ r₅ ≫ (α_ k₂ r₆ r₅).hom) ≫
            (α_ k₁ k₂ (r₆ ≫ r₅)).inv =
    𝟙 ((r₂ ≫ r₁) ≫ g₁ ≫ g₂) ⊗≫ r₂ ◁ α ▷ g₂ ⊗≫ (β ▷ (r₃ ≫ g₂) ≫ (k₁ ≫ r₄) ◁ γ) ⊗≫ k₁ ◁ δ ▷ r₅ ⊗≫ 𝟙 ((k₁ ≫ k₂) ≫ r₆ ≫ r₅)
⊢ (α_ (r₂ ≫ r₁) g₁ g₂).inv ≫
      ((α_ r₂ r₁ g₁).hom ≫ r₂ ◁ α ≫ (α_ r₂ h₁ r₃).inv ≫ β ▷ r₃ ≫ (α_ k₁ r₄ r₃).hom) ▷ g₂ ≫
        (α_ k₁ (r₄ ≫ r₃) g₂).hom ≫
          k₁ ◁ ((α_ r₄ r₃ g₂).hom ≫ r₄ ◁ γ ≫ (α_ r₄ h₂ r₅).inv ≫ δ ▷ r₅ ≫ (α_ k₂ r₆ r₅).hom) ≫
            (α_ k₁ k₂ (r₆ ≫ r₅)).inv =
    (α_ r₂ r₁ (g₁ ≫ g₂)).hom ≫
      r₂ ◁ ((α_ r₁ g₁ g₂).inv ≫ α ▷ g₂ ≫ (α_ h₁ r₃ g₂).hom ≫ h₁ ◁ γ ≫ (α_ h₁ h₂ r₅).inv) ≫
        (α_ r₂ (h₁ ≫ h₂) r₅).inv ≫
          ((α_ r₂ h₁ h₂).inv ≫ β ▷ h₂ ≫ (α_ k₁ r₄ h₂).hom ≫ k₁ ◁ δ ≫ (α_ k₁ k₂ r₆).inv) ▷ r₅ ≫ (α_ (k₁ ≫ k₂) r₆ r₅).hom
have _₁ : 𝟙 ((r₂ ≫ r₁) ≫ g₁ ≫ g₂) ⊗≫ r₂ ◁ α ▷ g₂ ⊗≫ (β ▷ (r₃ ≫ g₂) ≫ (k₁ ≫ r₄) ◁ γ) ⊗≫ k₁ ◁ δ ▷ r₅ ⊗≫ 𝟙 ((k₁ ≫ k₂) ≫ r₆ ≫ r₅) =
  (α_ r₂ r₁ (g₁ ≫ g₂)).hom ≫
    r₂ ◁ ((α_ r₁ g₁ g₂).inv ≫ α ▷ g₂ ≫ (α_ h₁ r₃ g₂).hom ≫ h₁ ◁ γ ≫ (α_ h₁ h₂ r₅).inv) ≫
      (α_ r₂ (h₁ ≫ h₂) r₅).inv ≫
        ((α_ r₂ h₁ h₂).inv ≫ β ▷ h₂ ≫ (α_ k₁ r₄ h₂).hom ≫ k₁ ◁ δ ≫ (α_ k₁ k₂ r₆).inv) ▷ r₅ ≫ (α_ (k₁ ≫ k₂) r₆ r₅).hom
Tactic: calc
    _ = 𝟙 _ ⊗≫ r₂ ◁ α ▷ g₂ ⊗≫ (β ▷ (r₃ ≫ g₂) ≫ (k₁ ≫ r₄) ◁ γ) ⊗≫ k₁ ◁ δ ▷ r₅ ⊗≫ 𝟙 _ := by
      bicategory
    _ = _ := by
      rw [← whisker_exchange]
      bicategory
-- 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₂
⊢ 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₃)
      ((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₅)
Tactic: have vcomp :=
    mateEquiv_vcomp (adj₁.comp adj₂) (adj₃.comp adj₄) (adj₅.comp adj₆)
      (leftAdjointSquare.hcomp α β) (leftAdjointSquare.hcomp γ δ)
-- 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₅)
⊢ 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 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₃)
Tactic: have hcomp1 := mateEquiv_hcomp adj₁ adj₃ adj₂ adj₄ α β