awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₃)
⊢ 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 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₅)
Tactic: have hcomp2 := mateEquiv_hcomp adj₃ adj₅ adj₄ adj₆ γ δ
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : l₂ ⟶ l₁
⊢ (conjugateEquiv adj₁ adj₂ : (a : l₂ ⟶ l₁) → r₁ ⟶ r₂) α =
    (ρ_ r₁).inv ≫ r₁ ◁ adj₂.unit ≫ r₁ ◁ α ▷ r₂ ≫ (α_ r₁ l₁ r₂).inv ≫ adj₁.counit ▷ r₂ ≫ (λ_ r₂).hom
have rw : (ρ_ r₁).inv ≫
    bicategoricalComp (h := r₁ ≫ 𝟙 c ≫ 𝟙 c) (𝟙 (r₁ ≫ 𝟙 c))
        (r₁ ◁ 𝟙 c ◁ adj₂.unit ⊗≫ r₁ ◁ ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ▷ r₂ ⊗≫ adj₁.counit ▷ 𝟙 d ▷ r₂ ⊗≫ 𝟙 (𝟙 d ≫ r₂)) ≫
      (λ_ r₂).hom =
  (ρ_ r₁).inv ≫ r₁ ◁ adj₂.unit ≫ r₁ ◁ α ▷ r₂ ≫ (α_ r₁ l₁ r₂).inv ≫ adj₁.counit ▷ r₂ ≫ (λ_ r₂).hom
Tactic: rw [conjugateEquiv_apply, mateEquiv_apply']
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : r₁ ⟶ r₂
⊢ ((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁) α =
    (λ_ l₂).inv ≫ adj₁.unit ▷ l₂ ≫ (α_ l₁ r₁ l₂).hom ≫ l₁ ◁ α ▷ l₂ ≫ l₁ ◁ adj₂.counit ≫ (ρ_ l₁).hom
have rw : (λ_ l₂).inv ≫
    (𝟙 (𝟙 c ≫ l₂) ⊗≫
        adj₁.unit ▷ 𝟙 c ▷ l₂ ⊗≫
          bicategoricalComp (h := l₁ ≫ 𝟙 d ≫ r₂ ≫ l₂) (l₁ ◁ ((ρ_ r₁).hom ≫ α ≫ (λ_ r₂).inv) ▷ l₂)
            (l₁ ◁ 𝟙 d ◁ adj₂.counit ⊗≫ 𝟙 (l₁ ≫ 𝟙 d))) ≫
      (ρ_ l₁).hom =
  (λ_ l₂).inv ≫ adj₁.unit ▷ l₂ ≫ (α_ l₁ r₁ l₂).hom ≫ l₁ ◁ α ▷ l₂ ≫ l₁ ◁ adj₂.counit ≫ (ρ_ l₁).hom
Tactic: rw [conjugateEquiv_symm_apply, mateEquiv_symm_apply']
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c d : B
l₁ : c ⟶ d
r₁ : d ⟶ c
adj₁ : l₁ ⊣ r₁
⊢ Eq (α := r₁ ⟶ r₁) ((conjugateEquiv adj₁ adj₁ : (a : l₁ ⟶ l₁) → r₁ ⟶ r₁) (𝟙 l₁) : r₁ ⟶ r₁) (𝟙 r₁ : r₁ ⟶ r₁)
have rw : (ρ_ r₁).inv ≫
    bicategoricalComp (h := r₁ ≫ 𝟙 c ≫ 𝟙 c) (𝟙 (r₁ ≫ 𝟙 c))
        (r₁ ◁ 𝟙 c ◁ adj₁.unit ⊗≫
          r₁ ◁ ((λ_ l₁).hom ≫ 𝟙 l₁ ≫ (ρ_ l₁).inv) ▷ r₁ ⊗≫ adj₁.counit ▷ 𝟙 d ▷ r₁ ⊗≫ 𝟙 (𝟙 d ≫ r₁)) ≫
      (λ_ r₁).hom =
  𝟙 r₁
Tactic: rw [conjugateEquiv_apply, mateEquiv_apply']
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c d : B
l₁ : c ⟶ d
r₁ : d ⟶ c
adj₁ : l₁ ⊣ r₁
⊢ 𝟙 r₁ ⊗≫ rightZigzag adj₁.unit adj₁.counit ⊗≫ 𝟙 r₁ = 𝟙 r₁
have rw : 𝟙 r₁ ⊗≫ ((ρ_ r₁).hom ≫ (λ_ r₁).inv) ⊗≫ 𝟙 r₁ = 𝟙 r₁
Tactic: rw [adj₁.right_triangle]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c d : B
l₁ : c ⟶ d
r₁ : d ⟶ c
adj₁ : l₁ ⊣ r₁
⊢ (ρ_ r₁).inv ≫
      bicategoricalComp (h := r₁ ≫ 𝟙 c ≫ 𝟙 c) (𝟙 (r₁ ≫ 𝟙 c))
          (r₁ ◁ 𝟙 c ◁ adj₁.unit ⊗≫
            r₁ ◁ ((λ_ l₁).hom ≫ 𝟙 l₁ ≫ (ρ_ l₁).inv) ▷ r₁ ⊗≫ adj₁.counit ▷ 𝟙 d ▷ r₁ ⊗≫ 𝟙 (𝟙 d ≫ r₁)) ≫
        (λ_ r₁).hom =
    𝟙 r₁
have _ : (ρ_ r₁).inv ≫
    bicategoricalComp (h := r₁ ≫ 𝟙 c ≫ 𝟙 c) (𝟙 (r₁ ≫ 𝟙 c))
        (r₁ ◁ 𝟙 c ◁ adj₁.unit ⊗≫
          r₁ ◁ ((λ_ l₁).hom ≫ 𝟙 l₁ ≫ (ρ_ l₁).inv) ▷ r₁ ⊗≫ adj₁.counit ▷ 𝟙 d ▷ r₁ ⊗≫ 𝟙 (𝟙 d ≫ r₁)) ≫
      (λ_ r₁).hom =
  𝟙 r₁ ⊗≫ rightZigzag adj₁.unit adj₁.counit ⊗≫ 𝟙 r₁
Tactic: calc
    _ = 𝟙 _ ⊗≫ rightZigzag adj₁.unit adj₁.counit ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 r₁ := by
      rw [adj₁.right_triangle]
      bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c d : B
l₁ : c ⟶ d
r₁ : d ⟶ c
adj₁ : l₁ ⊣ r₁
_ :
  (ρ_ r₁).inv ≫
      bicategoricalComp (h := r₁ ≫ 𝟙 c ≫ 𝟙 c) (𝟙 (r₁ ≫ 𝟙 c))
          (r₁ ◁ 𝟙 c ◁ adj₁.unit ⊗≫
            r₁ ◁ ((λ_ l₁).hom ≫ 𝟙 l₁ ≫ (ρ_ l₁).inv) ▷ r₁ ⊗≫ adj₁.counit ▷ 𝟙 d ▷ r₁ ⊗≫ 𝟙 (𝟙 d ≫ r₁)) ≫
        (λ_ r₁).hom =
    𝟙 r₁ ⊗≫ rightZigzag adj₁.unit adj₁.counit ⊗≫ 𝟙 r₁
⊢ (ρ_ r₁).inv ≫
      bicategoricalComp (h := r₁ ≫ 𝟙 c ≫ 𝟙 c) (𝟙 (r₁ ≫ 𝟙 c))
          (r₁ ◁ 𝟙 c ◁ adj₁.unit ⊗≫
            r₁ ◁ ((λ_ l₁).hom ≫ 𝟙 l₁ ≫ (ρ_ l₁).inv) ▷ r₁ ⊗≫ adj₁.counit ▷ 𝟙 d ▷ r₁ ⊗≫ 𝟙 (𝟙 d ≫ r₁)) ≫
        (λ_ r₁).hom =
    𝟙 r₁
have _₁ : 𝟙 r₁ ⊗≫ rightZigzag adj₁.unit adj₁.counit ⊗≫ 𝟙 r₁ = 𝟙 r₁
Tactic: calc
    _ = 𝟙 _ ⊗≫ rightZigzag adj₁.unit adj₁.counit ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 r₁ := by
      rw [adj₁.right_triangle]
      bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c d : B
l₁ : c ⟶ d
r₁ : d ⟶ c
adj₁ : l₁ ⊣ r₁
⊢ Eq (α := l₁ ⟶ l₁) (((conjugateEquiv adj₁ adj₁).symm : (a : r₁ ⟶ r₁) → l₁ ⟶ l₁) (𝟙 r₁) : l₁ ⟶ l₁) (𝟙 l₁ : l₁ ⟶ l₁)
have rw : Eq.{w + 1} (α := r₁ ⟶ r₁) (𝟙 r₁) ((conjugateEquiv adj₁ adj₁ : (a : l₁ ⟶ l₁) → r₁ ⟶ r₁) (𝟙 l₁))
Tactic: rw [Equiv.symm_apply_eq, conjugateEquiv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c d : B
l₁ : c ⟶ d
r₁ : d ⟶ c
adj₁ : l₁ ⊣ r₁
rw : Eq.{w + 1} (α := r₁ ⟶ r₁) (𝟙 r₁) ((conjugateEquiv adj₁ adj₁ : (a : l₁ ⟶ l₁) → r₁ ⟶ r₁) (𝟙 l₁))
⊢ Eq (α := l₁ ⟶ l₁) (((conjugateEquiv adj₁ adj₁).symm : (a : r₁ ⟶ r₁) → l₁ ⟶ l₁) (𝟙 r₁) : l₁ ⟶ l₁) (𝟙 l₁ : l₁ ⟶ l₁)
have rw₁ : 𝟙 r₁ = 𝟙 r₁
Tactic: rw [Equiv.symm_apply_eq, conjugateEquiv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c : B
l r : c ⟶ c
adj : l ⊣ r
α : 𝟙 c ⟶ l
⊢ (conjugateEquiv adj (Adjunction.id c) : (a : 𝟙 c ⟶ l) → r ⟶ 𝟙 c) α = (ρ_ r).inv ≫ r ◁ α ≫ adj.counit
have rw : (ρ_ r).inv ≫
    bicategoricalComp (h := r ≫ 𝟙 c ≫ 𝟙 c) (𝟙 (r ≫ 𝟙 c))
        (r ◁ 𝟙 c ◁ Adjunction.unit (Adjunction.id c) ⊗≫
          r ◁ (Iso.hom (λ_ (𝟙 c)) ≫ α ≫ (ρ_ l).inv) ▷ 𝟙 c ⊗≫ adj.counit ▷ 𝟙 c ▷ 𝟙 c ⊗≫ 𝟙 (𝟙 c ≫ 𝟙 c)) ≫
      Iso.hom (λ_ (𝟙 c)) =
  (ρ_ r).inv ≫ r ◁ α ≫ adj.counit
Tactic: rw [conjugateEquiv_apply, mateEquiv_apply']
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c : B
l r : c ⟶ c
adj : l ⊣ r
α : 𝟙 c ⟶ l
⊢ (ρ_ r).inv ≫
      bicategoricalComp (h := r ≫ 𝟙 c ≫ 𝟙 c) (𝟙 (r ≫ 𝟙 c))
          (r ◁ 𝟙 c ◁ Adjunction.unit (Adjunction.id c) ⊗≫
            r ◁ (Iso.hom (λ_ (𝟙 c)) ≫ α ≫ (ρ_ l).inv) ▷ 𝟙 c ⊗≫ adj.counit ▷ 𝟙 c ▷ 𝟙 c ⊗≫ 𝟙 (𝟙 c ≫ 𝟙 c)) ≫
        Iso.hom (λ_ (𝟙 c)) =
    (ρ_ r).inv ≫ r ◁ α ≫ adj.counit
have dsimp : (ρ_ r).inv ≫
    bicategoricalComp (h := r ≫ 𝟙 c ≫ 𝟙 c) (𝟙 (r ≫ 𝟙 c))
        (r ◁ 𝟙 c ◁ Iso.inv (ρ_ (𝟙 c)) ⊗≫
          r ◁ (Iso.hom (λ_ (𝟙 c)) ≫ α ≫ (ρ_ l).inv) ▷ 𝟙 c ⊗≫ adj.counit ▷ 𝟙 c ▷ 𝟙 c ⊗≫ 𝟙 (𝟙 c ≫ 𝟙 c)) ≫
      Iso.hom (λ_ (𝟙 c)) =
  (ρ_ r).inv ≫ r ◁ α ≫ adj.counit
Tactic: dsimp [Adjunction.id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c : B
l r : c ⟶ c
adj : l ⊣ r
α : r ⟶ 𝟙 c
⊢ ((conjugateEquiv adj (Adjunction.id c)).symm : (a : r ⟶ 𝟙 c) → 𝟙 c ⟶ l) α = adj.unit ≫ l ◁ α ≫ (ρ_ l).hom
have rw : Iso.inv (λ_ (𝟙 c)) ≫
    (𝟙 (𝟙 c ≫ 𝟙 c) ⊗≫
        adj.unit ▷ 𝟙 c ▷ 𝟙 c ⊗≫
          bicategoricalComp (h := l ≫ 𝟙 c ≫ 𝟙 c ≫ 𝟙 c) (l ◁ ((ρ_ r).hom ≫ α ≫ Iso.inv (λ_ (𝟙 c))) ▷ 𝟙 c)
            (l ◁ 𝟙 c ◁ Adjunction.counit (Adjunction.id c) ⊗≫ 𝟙 (l ≫ 𝟙 c))) ≫
      (ρ_ l).hom =
  adj.unit ≫ l ◁ α ≫ (ρ_ l).hom
Tactic: rw [conjugateEquiv_symm_apply, mateEquiv_symm_apply']
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c : B
l r : c ⟶ c
adj : l ⊣ r
α : r ⟶ 𝟙 c
⊢ Iso.inv (λ_ (𝟙 c)) ≫
      (𝟙 (𝟙 c ≫ 𝟙 c) ⊗≫
          adj.unit ▷ 𝟙 c ▷ 𝟙 c ⊗≫
            bicategoricalComp (h := l ≫ 𝟙 c ≫ 𝟙 c ≫ 𝟙 c) (l ◁ ((ρ_ r).hom ≫ α ≫ Iso.inv (λ_ (𝟙 c))) ▷ 𝟙 c)
              (l ◁ 𝟙 c ◁ Adjunction.counit (Adjunction.id c) ⊗≫ 𝟙 (l ≫ 𝟙 c))) ≫
        (ρ_ l).hom =
    adj.unit ≫ l ◁ α ≫ (ρ_ l).hom
have dsimp : Iso.inv (λ_ (𝟙 c)) ≫
    (𝟙 (𝟙 c ≫ 𝟙 c) ⊗≫
        adj.unit ▷ 𝟙 c ▷ 𝟙 c ⊗≫
          bicategoricalComp (h := l ≫ 𝟙 c ≫ 𝟙 c ≫ 𝟙 c) (l ◁ ((ρ_ r).hom ≫ α ≫ Iso.inv (λ_ (𝟙 c))) ▷ 𝟙 c)
            (l ◁ 𝟙 c ◁ Iso.hom (ρ_ (𝟙 c)) ⊗≫ 𝟙 (l ≫ 𝟙 c))) ≫
      (ρ_ l).hom =
  adj.unit ≫ l ◁ α ≫ (ρ_ l).hom
Tactic: dsimp [Adjunction.id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
l : a ⟶ b
r : b ⟶ a
adj : l ⊣ r
l' : a ⟶ b
r' : b ⟶ a
adj' : l' ⊣ r'
φ : l' ⟶ l
⊢ Eq (α := r ⟶ r' ≫ 𝟙 a)
    ((conjugateEquiv adj (Adjunction.comp (Adjunction.id a) adj') : (a_1 : 𝟙 a ≫ l' ⟶ l) → r ⟶ r' ≫ 𝟙 a)
        ((λ_ l').hom ≫ φ) :
      r ⟶ r' ≫ 𝟙 a)
    ((conjugateEquiv adj adj' : (a_1 : l' ⟶ l) → r ⟶ r') φ ≫ (ρ_ r').inv : r ⟶ r' ≫ 𝟙 a)
have simp : Eq (α := r ⟶ r' ≫ 𝟙 a)
  ((ρ_ r).inv ≫
    (mateEquiv adj adj' : (a_1 : 𝟙 a ≫ l' ⟶ l ≫ 𝟙 b) → r ≫ 𝟙 a ⟶ 𝟙 b ≫ r') ((λ_ l').hom ≫ φ ≫ (ρ_ l).inv) ≫
      (ρ_ (𝟙 b ≫ r')).inv ≫ Iso.hom (α_ (𝟙 b) r' (𝟙 a)) ≫ (λ_ (r' ≫ 𝟙 a)).hom)
  ((ρ_ r).inv ≫
    (mateEquiv adj adj' : (a_1 : 𝟙 a ≫ l' ⟶ l ≫ 𝟙 b) → r ≫ 𝟙 a ⟶ 𝟙 b ≫ r') ((λ_ l').hom ≫ φ ≫ (ρ_ l).inv) ≫
      (λ_ r').hom ≫ (ρ_ r').inv)
Tactic: simp only [conjugateEquiv_apply, mateEquiv_id_comp_right,
    id_whiskerLeft, Category.assoc, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
l : a ⟶ b
r : b ⟶ a
adj : l ⊣ r
l' : a ⟶ b
r' : b ⟶ a
adj' : l' ⊣ r'
φ : l' ⟶ l
⊢ Eq (α := r ⟶ 𝟙 b ≫ r')
    ((conjugateEquiv adj (adj'.comp (Adjunction.id b)) : (a_1 : l' ≫ 𝟙 b ⟶ l) → r ⟶ 𝟙 b ≫ r') ((ρ_ l').hom ≫ φ) :
      r ⟶ 𝟙 b ≫ r')
    ((conjugateEquiv adj adj' : (a_1 : l' ⟶ l) → r ⟶ r') φ ≫ (λ_ r').inv : r ⟶ 𝟙 b ≫ r')
have simp : (ρ_ (𝟙 a ≫ l')).inv ≫ Iso.hom (α_ (𝟙 a) l' (𝟙 b)) ≫ (λ_ (l' ≫ 𝟙 b)).hom ≫ (ρ_ l').hom ≫ φ ≫ (ρ_ l).inv =
  (λ_ l').hom ≫ φ ≫ (ρ_ l).inv
Tactic: simp only [conjugateEquiv_apply, Category.assoc, mateEquiv_comp_id_right, id_whiskerLeft,
    Iso.inv_hom_id, Category.comp_id, Iso.hom_inv_id, Iso.cancel_iso_inv_left,
    EmbeddingLike.apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (hypothesis)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
l₁ : a ⟶ b
r₁ : b ⟶ a
adj₁ : l₁ ⊣ r₁
l₂ : b ⟶ c
r₂ : c ⟶ b
adj₂ : l₂ ⊣ r₂
l₂' : b ⟶ c
r₂' : c ⟶ b
adj₂' : l₂' ⊣ r₂'
φ : l₂' ⟶ l₂
⊢ Eq (α := r₂ ≫ r₁ ⟶ r₂' ≫ r₁)
    ((conjugateEquiv (adj₁.comp adj₂) (adj₁.comp adj₂') : (a_1 : l₁ ≫ l₂' ⟶ l₁ ≫ l₂) → r₂ ≫ r₁ ⟶ r₂' ≫ r₁) (l₁ ◁ φ) :
      r₂ ≫ r₁ ⟶ r₂' ≫ r₁)
    ((conjugateEquiv adj₂ adj₂' : (a : l₂' ⟶ l₂) → r₂ ⟶ r₂') φ ▷ r₁ : r₂ ≫ r₁ ⟶ r₂' ≫ r₁)
have this : Eq (α := (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂' ≫ r₁)
  ((mateEquiv (adj₁.comp adj₂) (adj₁.comp adj₂') :
        (a_1 : 𝟙 a ≫ l₁ ≫ l₂' ⟶ (l₁ ≫ l₂) ≫ 𝟙 c) → (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂' ≫ r₁)
      (leftAdjointSquare.hcomp ((λ_ l₁).hom ≫ (ρ_ l₁).inv) ((λ_ l₂').hom ≫ φ ≫ (ρ_ l₂).inv)) :
    (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂' ≫ r₁)
  (rightAdjointSquare.hcomp (h := 𝟙 b)
      ((mateEquiv adj₁ adj₁ : (a_1 : 𝟙 a ≫ l₁ ⟶ l₁ ≫ 𝟙 b) → r₁ ≫ 𝟙 a ⟶ 𝟙 b ≫ r₁) ((λ_ l₁).hom ≫ (ρ_ l₁).inv))
      ((mateEquiv adj₂ adj₂' : (a : 𝟙 b ≫ l₂' ⟶ l₂ ≫ 𝟙 c) → r₂ ≫ 𝟙 b ⟶ 𝟙 c ≫ r₂') ((λ_ l₂').hom ≫ φ ≫ (ρ_ l₂).inv)) :
    (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂' ≫ r₁)
Tactic: have := mateEquiv_hcomp adj₁ adj₁ adj₂ adj₂' ((λ_ _).hom ≫ (ρ_ _).inv)
    ((λ_ _).hom ≫ φ ≫ (ρ_ _).inv)
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (hypothesis)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
l₁ : a ⟶ b
r₁ : b ⟶ a
adj₁ : l₁ ⊣ r₁
l₂ : b ⟶ c
r₂ : c ⟶ b
adj₂ : l₂ ⊣ r₂
l₂' : b ⟶ c
r₂' : c ⟶ b
adj₂' : l₂' ⊣ r₂'
φ : l₂' ⟶ l₂
this :
  Eq (α := (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂' ≫ r₁)
    ((mateEquiv (adj₁.comp adj₂) (adj₁.comp adj₂') :
          (a_1 : 𝟙 a ≫ l₁ ≫ l₂' ⟶ (l₁ ≫ l₂) ≫ 𝟙 c) → (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂' ≫ r₁)
        (Iso.inv (α_ (𝟙 a) l₁ l₂') ≫
          ((λ_ l₁).hom ≫ (ρ_ l₁).inv) ▷ l₂' ≫
            (α_ l₁ (𝟙 b) l₂').hom ≫ l₁ ◁ ((λ_ l₂').hom ≫ φ ≫ (ρ_ l₂).inv) ≫ (α_ l₁ l₂ (𝟙 c)).inv) :
      (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂' ≫ r₁)
    ((α_ r₂ r₁ (𝟙 a)).hom ≫
        r₂ ◁ (mateEquiv adj₁ adj₁ : (a_1 : 𝟙 a ≫ l₁ ⟶ l₁ ≫ 𝟙 b) → r₁ ≫ 𝟙 a ⟶ 𝟙 b ≫ r₁) ((λ_ l₁).hom ≫ (ρ_ l₁).inv) ≫
          (α_ r₂ (𝟙 b) r₁).inv ≫
            (mateEquiv adj₂ adj₂' : (a : 𝟙 b ≫ l₂' ⟶ l₂ ≫ 𝟙 c) → r₂ ≫ 𝟙 b ⟶ 𝟙 c ≫ r₂')
                  ((λ_ l₂').hom ≫ φ ≫ (ρ_ l₂).inv) ▷
                r₁ ≫
              Iso.hom (α_ (𝟙 c) r₂' r₁) :
      (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂' ≫ r₁)
⊢ Eq (α := r₂ ≫ r₁ ⟶ r₂' ≫ r₁)
    ((conjugateEquiv (adj₁.comp adj₂) (adj₁.comp adj₂') : (a_1 : l₁ ≫ l₂' ⟶ l₁ ≫ l₂) → r₂ ≫ r₁ ⟶ r₂' ≫ r₁) (l₁ ◁ φ) :
      r₂ ≫ r₁ ⟶ r₂' ≫ r₁)
    ((conjugateEquiv adj₂ adj₂' : (a : l₂' ⟶ l₂) → r₂ ⟶ r₂') φ ▷ r₁ : r₂ ≫ r₁ ⟶ r₂' ≫ r₁)
have this₁ : Eq (α := (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂' ≫ r₁)
  ((mateEquiv (adj₁.comp adj₂) (adj₁.comp adj₂') :
        (a_1 : 𝟙 a ≫ l₁ ≫ l₂' ⟶ (l₁ ≫ l₂) ≫ 𝟙 c) → (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂' ≫ r₁)
      ((λ_ (l₁ ≫ l₂')).hom ≫ l₁ ◁ φ ≫ (ρ_ (l₁ ≫ l₂)).inv) :
    (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂' ≫ r₁)
  ((ρ_ (r₂ ≫ r₁)).hom ≫
      (ρ_ r₂).inv ▷ r₁ ≫
        (mateEquiv adj₂ adj₂' : (a : 𝟙 b ≫ l₂' ⟶ l₂ ≫ 𝟙 c) → r₂ ≫ 𝟙 b ⟶ 𝟙 c ≫ r₂') ((λ_ l₂').hom ≫ φ ≫ (ρ_ l₂).inv) ▷
            r₁ ≫
          Iso.hom (α_ (𝟙 c) r₂' r₁) :
    (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂' ≫ r₁)
Tactic: simp only [comp_whiskerRight, leftUnitor_whiskerRight, Category.assoc, whiskerLeft_comp,
    whiskerLeft_rightUnitor_inv, Iso.hom_inv_id, Category.comp_id, triangle_assoc,
    inv_hom_whiskerRight_assoc, Iso.inv_hom_id_assoc, mateEquiv_leftUnitor_hom_rightUnitor_inv,
    whiskerLeft_rightUnitor, triangle_assoc_comp_left_inv_assoc, Iso.hom_inv_id_assoc] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (hypothesis)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
l₁ : a ⟶ b
r₁ : b ⟶ a
adj₁ : l₁ ⊣ r₁
l₁' : a ⟶ b
r₁' : b ⟶ a
adj₁' : l₁' ⊣ r₁'
l₂ : b ⟶ c
r₂ : c ⟶ b
adj₂ : l₂ ⊣ r₂
φ : l₁' ⟶ l₁
⊢ Eq (α := r₂ ≫ r₁ ⟶ r₂ ≫ r₁')
    ((conjugateEquiv (adj₁.comp adj₂) (adj₁'.comp adj₂) : (a_1 : l₁' ≫ l₂ ⟶ l₁ ≫ l₂) → r₂ ≫ r₁ ⟶ r₂ ≫ r₁') (φ ▷ l₂) :
      r₂ ≫ r₁ ⟶ r₂ ≫ r₁')
    (r₂ ◁ (conjugateEquiv adj₁ adj₁' : (a_1 : l₁' ⟶ l₁) → r₁ ⟶ r₁') φ : r₂ ≫ r₁ ⟶ r₂ ≫ r₁')
have this : Eq (α := (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂ ≫ r₁')
  ((mateEquiv (adj₁.comp adj₂) (adj₁'.comp adj₂) :
        (a_1 : 𝟙 a ≫ l₁' ≫ l₂ ⟶ (l₁ ≫ l₂) ≫ 𝟙 c) → (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂ ≫ r₁')
      (leftAdjointSquare.hcomp ((λ_ l₁').hom ≫ φ ≫ (ρ_ l₁).inv) ((λ_ l₂).hom ≫ (ρ_ l₂).inv)) :
    (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂ ≫ r₁')
  (rightAdjointSquare.hcomp (h := 𝟙 b)
      ((mateEquiv adj₁ adj₁' : (a_1 : 𝟙 a ≫ l₁' ⟶ l₁ ≫ 𝟙 b) → r₁ ≫ 𝟙 a ⟶ 𝟙 b ≫ r₁') ((λ_ l₁').hom ≫ φ ≫ (ρ_ l₁).inv))
      ((mateEquiv adj₂ adj₂ : (a : 𝟙 b ≫ l₂ ⟶ l₂ ≫ 𝟙 c) → r₂ ≫ 𝟙 b ⟶ 𝟙 c ≫ r₂) ((λ_ l₂).hom ≫ (ρ_ l₂).inv)) :
    (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂ ≫ r₁')
Tactic: have := mateEquiv_hcomp adj₁ adj₁' adj₂ adj₂
    ((λ_ _).hom ≫ φ ≫ (ρ_ _).inv) ((λ_ _).hom ≫ (ρ_ _).inv)
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (hypothesis)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
l₁ : a ⟶ b
r₁ : b ⟶ a
adj₁ : l₁ ⊣ r₁
l₁' : a ⟶ b
r₁' : b ⟶ a
adj₁' : l₁' ⊣ r₁'
l₂ : b ⟶ c
r₂ : c ⟶ b
adj₂ : l₂ ⊣ r₂
φ : l₁' ⟶ l₁
this :
  Eq (α := (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂ ≫ r₁')
    ((mateEquiv (adj₁.comp adj₂) (adj₁'.comp adj₂) :
          (a_1 : 𝟙 a ≫ l₁' ≫ l₂ ⟶ (l₁ ≫ l₂) ≫ 𝟙 c) → (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂ ≫ r₁')
        (Iso.inv (α_ (𝟙 a) l₁' l₂) ≫
          ((λ_ l₁').hom ≫ φ ≫ (ρ_ l₁).inv) ▷ l₂ ≫
            (α_ l₁ (𝟙 b) l₂).hom ≫ l₁ ◁ ((λ_ l₂).hom ≫ (ρ_ l₂).inv) ≫ (α_ l₁ l₂ (𝟙 c)).inv) :
      (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂ ≫ r₁')
    ((α_ r₂ r₁ (𝟙 a)).hom ≫
        r₂ ◁
            (mateEquiv adj₁ adj₁' : (a_1 : 𝟙 a ≫ l₁' ⟶ l₁ ≫ 𝟙 b) → r₁ ≫ 𝟙 a ⟶ 𝟙 b ≫ r₁')
              ((λ_ l₁').hom ≫ φ ≫ (ρ_ l₁).inv) ≫
          (α_ r₂ (𝟙 b) r₁').inv ≫
            (mateEquiv adj₂ adj₂ : (a : 𝟙 b ≫ l₂ ⟶ l₂ ≫ 𝟙 c) → r₂ ≫ 𝟙 b ⟶ 𝟙 c ≫ r₂) ((λ_ l₂).hom ≫ (ρ_ l₂).inv) ▷ r₁' ≫
              Iso.hom (α_ (𝟙 c) r₂ r₁') :
      (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂ ≫ r₁')
⊢ Eq (α := r₂ ≫ r₁ ⟶ r₂ ≫ r₁')
    ((conjugateEquiv (adj₁.comp adj₂) (adj₁'.comp adj₂) : (a_1 : l₁' ≫ l₂ ⟶ l₁ ≫ l₂) → r₂ ≫ r₁ ⟶ r₂ ≫ r₁') (φ ▷ l₂) :
      r₂ ≫ r₁ ⟶ r₂ ≫ r₁')
    (r₂ ◁ (conjugateEquiv adj₁ adj₁' : (a_1 : l₁' ⟶ l₁) → r₁ ⟶ r₁') φ : r₂ ≫ r₁ ⟶ r₂ ≫ r₁')
have this₁ : (mateEquiv (adj₁.comp adj₂) (adj₁'.comp adj₂) :
      (a_1 : 𝟙 a ≫ l₁' ≫ l₂ ⟶ (l₁ ≫ l₂) ≫ 𝟙 c) → (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂ ≫ r₁')
    ((λ_ (l₁' ≫ l₂)).hom ≫ φ ▷ l₂ ≫ (ρ_ (l₁ ≫ l₂)).inv) =
  (α_ r₂ r₁ (𝟙 a)).hom ≫
    r₂ ◁ (mateEquiv adj₁ adj₁' : (a_1 : 𝟙 a ≫ l₁' ⟶ l₁ ≫ 𝟙 b) → r₁ ≫ 𝟙 a ⟶ 𝟙 b ≫ r₁') ((λ_ l₁').hom ≫ φ ≫ (ρ_ l₁).inv) ≫
      r₂ ◁ (λ_ r₁').hom ≫ (λ_ (r₂ ≫ r₁')).inv
Tactic: simp only [comp_whiskerRight, leftUnitor_whiskerRight, Category.assoc, whiskerLeft_comp,
    whiskerLeft_rightUnitor_inv, Iso.hom_inv_id, Category.comp_id, triangle_assoc,
    inv_hom_whiskerRight_assoc, Iso.inv_hom_id_assoc, mateEquiv_leftUnitor_hom_rightUnitor_inv,
    leftUnitor_inv_whiskerRight, Iso.inv_hom_id, triangle_assoc_comp_right_assoc] at this
Cleared hypotheses: this
-- 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 : B
l₁ : a ⟶ b
r₁ : b ⟶ a
adj₁ : l₁ ⊣ r₁
l₂ : b ⟶ c
r₂ : c ⟶ b
adj₂ : l₂ ⊣ r₂
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₃ : l₃ ⊣ r₃
⊢ (conjugateEquiv (adj₁.comp (adj₂.comp adj₃)) ((adj₁.comp adj₂).comp adj₃) :
        (a_1 : (l₁ ≫ l₂) ≫ l₃ ⟶ l₁ ≫ l₂ ≫ l₃) → (r₃ ≫ r₂) ≫ r₁ ⟶ r₃ ≫ r₂ ≫ r₁)
      (α_ l₁ l₂ l₃).hom =
    (α_ r₃ r₂ r₁).hom
have simp : (adj₁.unit ⊗≫
      l₁ ◁ (adj₂.unit ⊗≫ l₂ ◁ adj₃.unit ▷ r₂ ⊗≫ 𝟙 ((l₂ ≫ l₃) ≫ r₃ ≫ r₂)) ▷ r₁ ⊗≫ 𝟙 ((l₁ ≫ l₂ ≫ l₃) ≫ (r₃ ≫ r₂) ≫ r₁)) ≫
    (α_ l₁ (l₂ ≫ l₃) ((r₃ ≫ r₂) ≫ r₁)).hom ≫
      l₁ ◁ (α_ l₂ l₃ ((r₃ ≫ r₂) ≫ r₁)).hom ≫
        l₁ ◁ l₂ ◁ l₃ ◁ (α_ r₃ r₂ r₁).hom ≫
          l₁ ◁ l₂ ◁ l₃ ◁ (λ_ (r₃ ≫ r₂ ≫ r₁)).inv ≫
            l₁ ◁ (α_ l₂ l₃ (𝟙 d ≫ r₃ ≫ r₂ ≫ r₁)).inv ≫ (α_ l₁ (l₂ ≫ l₃) (𝟙 d ≫ r₃ ≫ r₂ ≫ r₁)).inv =
  ((adj₁.unit ⊗≫ l₁ ◁ adj₂.unit ▷ r₁ ⊗≫ 𝟙 ((l₁ ≫ l₂) ≫ r₂ ≫ r₁)) ⊗≫
      ((α_ l₁ l₂ (𝟙 c ≫ r₂ ≫ r₁)).hom ≫
          l₁ ◁ l₂ ◁ Iso.inv (α_ (𝟙 c) r₂ r₁) ≫
            l₁ ◁ l₂ ◁ adj₃.unit ▷ r₂ ▷ r₁ ≫
              l₁ ◁ l₂ ◁ (α_ (l₃ ≫ r₃) r₂ r₁).hom ≫ (α_ l₁ l₂ ((l₃ ≫ r₃) ≫ r₂ ≫ r₁)).inv) ⊗≫
        𝟙 (((l₁ ≫ l₂) ≫ l₃) ≫ r₃ ≫ r₂ ≫ r₁)) ≫
    (λ_ (((l₁ ≫ l₂) ≫ l₃) ≫ r₃ ≫ r₂ ≫ r₁)).inv ≫
      Iso.inv (α_ (𝟙 a) ((l₁ ≫ l₂) ≫ l₃) (r₃ ≫ r₂ ≫ r₁)) ≫
        (α_ (𝟙 a ≫ (l₁ ≫ l₂) ≫ l₃) r₃ (r₂ ≫ r₁)).inv ≫
          (α_ ((𝟙 a ≫ (l₁ ≫ l₂) ≫ l₃) ≫ r₃) r₂ r₁).inv ≫
            Iso.hom (α_ (𝟙 a) ((l₁ ≫ l₂) ≫ l₃) r₃) ▷ r₂ ▷ r₁ ≫
              Iso.hom (α_ (𝟙 a) (((l₁ ≫ l₂) ≫ l₃) ≫ r₃) r₂) ▷ r₁ ≫
                Iso.hom (α_ (𝟙 a) ((((l₁ ≫ l₂) ≫ l₃) ≫ r₃) ≫ r₂) r₁) ≫
                  (λ_ (((((l₁ ≫ l₂) ≫ l₃) ≫ r₃) ≫ r₂) ≫ r₁)).hom ≫
                    (α_ l₁ l₂ l₃).hom ▷ r₃ ▷ r₂ ▷ r₁ ≫
                      (ρ_ (l₁ ≫ l₂ ≫ l₃)).inv ▷ r₃ ▷ r₂ ▷ r₁ ≫
                        (α_ (((l₁ ≫ l₂ ≫ l₃) ≫ 𝟙 d) ≫ r₃) r₂ r₁).hom ≫
                          (α_ ((l₁ ≫ l₂ ≫ l₃) ≫ 𝟙 d) r₃ (r₂ ≫ r₁)).hom ≫ (α_ (l₁ ≫ l₂ ≫ l₃) (𝟙 d) (r₃ ≫ r₂ ≫ r₁)).hom
Tactic: simp [← cancel_epi (ρ_ ((r₃ ≫ r₂) ≫ r₁)).hom, ← cancel_mono (λ_ (r₃ ≫ r₂ ≫ r₁)).inv,
    conjugateEquiv_apply, mateEquiv_eq_iff, Adjunction.homEquiv₁_symm_apply,
    Adjunction.homEquiv₂_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c d : B
l₁ l₂ l₃ : c ⟶ d
r₁ r₂ r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : l₃ ⟶ l₂
⊢ Eq (α := r₁ ⟶ r₃)
    (CategoryStruct.comp (Y := r₂) ((conjugateEquiv adj₁ adj₂ : (a : l₂ ⟶ l₁) → r₁ ⟶ r₂) α)
        ((conjugateEquiv adj₂ adj₃ : (a : l₃ ⟶ l₂) → r₂ ⟶ r₃) β) :
      r₁ ⟶ r₃)
    ((conjugateEquiv adj₁ adj₃ : (a : l₃ ⟶ l₁) → r₁ ⟶ r₃) (β ≫ α) : r₁ ⟶ r₃)
have simp : Eq (α := r₁ ⟶ r₃)
  (((ρ_ r₁).inv ≫
      (mateEquiv adj₁ adj₂ : (a : 𝟙 c ≫ l₂ ⟶ l₁ ≫ 𝟙 d) → r₁ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ≫
        (λ_ r₂).hom) ≫
    (ρ_ r₂).inv ≫
      (mateEquiv adj₂ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₂ ≫ 𝟙 d) → r₂ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫
        (λ_ r₃).hom)
  ((ρ_ r₁).inv ≫
    (mateEquiv adj₁ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₁ ≫ 𝟙 d) → r₁ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ (β ≫ α) ≫ (ρ_ l₁).inv) ≫
      (λ_ r₃).hom)
Tactic: simp only [conjugateEquiv_apply]