awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Cat (goal)
Goal:
C D E F : Cat
G : C ⟶ E
H : D ⟶ F
L₁ : C ⟶ D
R₁ : D ⟶ C
L₂ : E ⟶ F
R₂ : F ⟶ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
f : G ≫ L₂ ⟶ L₁ ≫ H
⊢ Eq (α := (R₁ ≫ G).toFunctor ⟶ (H ≫ R₂).toFunctor)
    (Cat.Hom₂.toNatTrans ((mateEquiv adj₁ adj₂ : (a : G ≫ L₂ ⟶ L₁ ≫ H) → R₁ ≫ G ⟶ H ≫ R₂) f))
    ((CategoryTheory.mateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂) :
        (a : TwoSquare G.toFunctor L₁.toFunctor L₂.toFunctor H.toFunctor) →
          TwoSquare R₁.toFunctor H.toFunctor G.toFunctor R₂.toFunctor)
      f.toNatTrans)
have w : ∀ (X : (↑D : Type u_2)),
  Eq (α := (R₁ ≫ G).toFunctor.obj X ⟶ (H ≫ R₂).toFunctor.obj X)
    (NatTrans.app (Cat.Hom₂.toNatTrans ((mateEquiv adj₁ adj₂ : (a : G ≫ L₂ ⟶ L₁ ≫ H) → R₁ ≫ G ⟶ H ≫ R₂) f)) X)
    (NatTrans.app
      ((CategoryTheory.mateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂) :
          (a : TwoSquare G.toFunctor L₁.toFunctor L₂.toFunctor H.toFunctor) →
            TwoSquare R₁.toFunctor H.toFunctor G.toFunctor R₂.toFunctor)
        f.toNatTrans)
      X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Cat (goal)
Goal:
C D : Cat
L₁ L₂ : C ⟶ D
R₁ R₂ : D ⟶ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
f : L₂ ⟶ L₁
⊢ Eq (α := R₁.toFunctor ⟶ R₂.toFunctor) (Cat.Hom₂.toNatTrans ((conjugateEquiv adj₁ adj₂ : (a : L₂ ⟶ L₁) → R₁ ⟶ R₂) f))
    ((CategoryTheory.conjugateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂) :
        (a : L₂.toFunctor ⟶ L₁.toFunctor) → R₁.toFunctor ⟶ R₂.toFunctor)
      f.toNatTrans)
have dsimp : R₁.toFunctor.rightUnitor.inv ≫
    Cat.Hom₂.toNatTrans
        ((mateEquiv adj₁ adj₂ : (a : 𝟙 C ≫ L₂ ⟶ L₁ ≫ 𝟙 D) → R₁ ≫ 𝟙 C ⟶ 𝟙 D ≫ R₂) ((λ_ L₂).hom ≫ f ≫ (ρ_ L₁).inv)) ≫
      R₂.toFunctor.leftUnitor.hom =
  (CategoryTheory.conjugateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂) :
      (a : L₂.toFunctor ⟶ L₁.toFunctor) → R₁.toFunctor ⟶ R₂.toFunctor)
    f.toNatTrans
Tactic: dsimp [Bicategory.conjugateEquiv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Cat (goal)
Goal:
C D : Cat
L₁ L₂ : C ⟶ D
R₁ R₂ : D ⟶ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
f : L₂ ⟶ L₁
⊢ R₁.toFunctor.rightUnitor.inv ≫
      Cat.Hom₂.toNatTrans
          ((mateEquiv adj₁ adj₂ : (a : 𝟙 C ≫ L₂ ⟶ L₁ ≫ 𝟙 D) → R₁ ≫ 𝟙 C ⟶ 𝟙 D ≫ R₂) ((λ_ L₂).hom ≫ f ≫ (ρ_ L₁).inv)) ≫
        R₂.toFunctor.leftUnitor.hom =
    (CategoryTheory.conjugateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂) :
        (a : L₂.toFunctor ⟶ L₁.toFunctor) → R₁.toFunctor ⟶ R₂.toFunctor)
      f.toNatTrans
have rw : Eq (α := R₁.toFunctor ⟶ R₂.toFunctor)
  (R₁.toFunctor.rightUnitor.inv ≫
    (CategoryTheory.mateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂) :
          (a : TwoSquare (𝟙 C).toFunctor L₁.toFunctor L₂.toFunctor (𝟙 D).toFunctor) →
            TwoSquare R₁.toFunctor (𝟙 D).toFunctor (𝟙 C).toFunctor R₂.toFunctor)
        ((λ_ L₂).hom ≫ f ≫ (ρ_ L₁).inv).toNatTrans ≫
      R₂.toFunctor.leftUnitor.hom)
  ((CategoryTheory.conjugateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂) :
      (a : L₂.toFunctor ⟶ L₁.toFunctor) → R₁.toFunctor ⟶ R₂.toFunctor)
    f.toNatTrans)
Tactic: rw [toNatTrans_mateEquiv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Cat (goal)
Goal:
C D : Cat
L₁ L₂ : C ⟶ D
R₁ R₂ : D ⟶ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
f : L₂ ⟶ L₁
⊢ Eq (α := R₁.toFunctor ⟶ R₂.toFunctor)
    (R₁.toFunctor.rightUnitor.inv ≫
      (CategoryTheory.mateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂) :
            (a : TwoSquare (𝟙 C).toFunctor L₁.toFunctor L₂.toFunctor (𝟙 D).toFunctor) →
              TwoSquare R₁.toFunctor (𝟙 D).toFunctor (𝟙 C).toFunctor R₂.toFunctor)
          ((λ_ L₂).hom ≫ f ≫ (ρ_ L₁).inv).toNatTrans ≫
        R₂.toFunctor.leftUnitor.hom)
    ((CategoryTheory.conjugateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂) :
        (a : L₂.toFunctor ⟶ L₁.toFunctor) → R₁.toFunctor ⟶ R₂.toFunctor)
      f.toNatTrans)
have w : ∀ (X : (↑D : Type u_2)),
  Eq (α := R₁.toFunctor.obj X ⟶ R₂.toFunctor.obj X)
    (NatTrans.app
      (R₁.toFunctor.rightUnitor.inv ≫
        (CategoryTheory.mateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂) :
              (a : TwoSquare (𝟙 C).toFunctor L₁.toFunctor L₂.toFunctor (𝟙 D).toFunctor) →
                TwoSquare R₁.toFunctor (𝟙 D).toFunctor (𝟙 C).toFunctor R₂.toFunctor)
            ((λ_ L₂).hom ≫ f ≫ (ρ_ L₁).inv).toNatTrans ≫
          R₂.toFunctor.leftUnitor.hom)
      X)
    (NatTrans.app
      ((CategoryTheory.conjugateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂) :
          (a : L₂.toFunctor ⟶ L₁.toFunctor) → R₁.toFunctor ⟶ R₂.toFunctor)
        f.toNatTrans)
      X)
Tactic: ext X
-- 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 : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : b ⟶ d
h : c ⟶ d
γ : g ⟶ l ≫ h
⊢ 𝟙 g ⊗≫ (adj.unit ▷ g ≫ (l ≫ r) ◁ γ) ⊗≫ l ◁ adj.counit ▷ h ⊗≫ 𝟙 (l ≫ h) =
    γ ⊗≫ leftZigzag adj.unit adj.counit ▷ h ⊗≫ 𝟙 (l ≫ h)
have rw : 𝟙 g ⊗≫ (𝟙 b ◁ γ ≫ adj.unit ▷ (l ≫ h)) ⊗≫ l ◁ adj.counit ▷ h ⊗≫ 𝟙 (l ≫ h) =
  γ ⊗≫ leftZigzag adj.unit adj.counit ▷ h ⊗≫ 𝟙 (l ≫ h)
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 : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : b ⟶ d
h : c ⟶ d
γ : g ⟶ l ≫ h
⊢ γ ⊗≫ leftZigzag adj.unit adj.counit ▷ h ⊗≫ 𝟙 (l ≫ h) = γ
have rw : γ ⊗≫ ((λ_ l).hom ≫ (ρ_ l).inv) ▷ h ⊗≫ 𝟙 (l ≫ h) = γ
Tactic: rw [adj.left_triangle]
-- 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 : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : b ⟶ d
h : c ⟶ d
β : r ≫ g ⟶ h
⊢ 𝟙 (r ≫ g) ⊗≫ r ◁ adj.unit ▷ g ⊗≫ ((r ≫ l) ◁ β ≫ adj.counit ▷ h) ⊗≫ 𝟙 h =
    𝟙 (r ≫ g) ⊗≫ rightZigzag adj.unit adj.counit ▷ g ⊗≫ β
have rw : 𝟙 (r ≫ g) ⊗≫ r ◁ adj.unit ▷ g ⊗≫ (adj.counit ▷ (r ≫ g) ≫ 𝟙 c ◁ β) ⊗≫ 𝟙 h =
  𝟙 (r ≫ g) ⊗≫ rightZigzag adj.unit adj.counit ▷ g ⊗≫ β
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 : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : b ⟶ d
h : c ⟶ d
β : r ≫ g ⟶ h
⊢ 𝟙 (r ≫ g) ⊗≫ rightZigzag adj.unit adj.counit ▷ g ⊗≫ β = β
have rw : 𝟙 (r ≫ g) ⊗≫ ((ρ_ r).hom ≫ (λ_ r).inv) ▷ g ⊗≫ β = β
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
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : b ⟶ d
h : c ⟶ d
β : r ≫ g ⟶ h
⊢ (fun (γ : g ⟶ l ≫ h) ↦ r ◁ γ ≫ (α_ r l h).inv ≫ adj.counit ▷ h ≫ (λ_ h).hom)
      ((fun (β : r ≫ g ⟶ h) ↦ (λ_ g).inv ≫ adj.unit ▷ g ≫ (α_ l r g).hom ≫ l ◁ β) β) =
    β
have _ : (fun (γ : g ⟶ l ≫ h) ↦ r ◁ γ ≫ (α_ r l h).inv ≫ adj.counit ▷ h ≫ (λ_ h).hom)
    ((fun (β : r ≫ g ⟶ h) ↦ (λ_ g).inv ≫ adj.unit ▷ g ≫ (α_ l r g).hom ≫ l ◁ β) β) =
  𝟙 (r ≫ g) ⊗≫ r ◁ adj.unit ▷ g ⊗≫ ((r ≫ l) ◁ β ≫ adj.counit ▷ h) ⊗≫ 𝟙 h
Tactic: calc
      _ = 𝟙 _ ⊗≫ r ◁ adj.unit ▷ g ⊗≫ ((r ≫ l) ◁ β ≫ adj.counit ▷ h) ⊗≫ 𝟙 _ := by
        bicategory
      _ = 𝟙 _ ⊗≫ rightZigzag adj.unit adj.counit ▷ g ⊗≫ β := by
        rw [whisker_exchange]
        bicategory
      _ = β := 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
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : b ⟶ d
h : c ⟶ d
β : r ≫ g ⟶ h
_ :
  (fun (γ : g ⟶ l ≫ h) ↦ r ◁ γ ≫ (α_ r l h).inv ≫ adj.counit ▷ h ≫ (λ_ h).hom)
      ((fun (β : r ≫ g ⟶ h) ↦ (λ_ g).inv ≫ adj.unit ▷ g ≫ (α_ l r g).hom ≫ l ◁ β) β) =
    𝟙 (r ≫ g) ⊗≫ r ◁ adj.unit ▷ g ⊗≫ ((r ≫ l) ◁ β ≫ adj.counit ▷ h) ⊗≫ 𝟙 h
⊢ (fun (γ : g ⟶ l ≫ h) ↦ r ◁ γ ≫ (α_ r l h).inv ≫ adj.counit ▷ h ≫ (λ_ h).hom)
      ((fun (β : r ≫ g ⟶ h) ↦ (λ_ g).inv ≫ adj.unit ▷ g ≫ (α_ l r g).hom ≫ l ◁ β) β) =
    β
have _₁ : 𝟙 (r ≫ g) ⊗≫ r ◁ adj.unit ▷ g ⊗≫ ((r ≫ l) ◁ β ≫ adj.counit ▷ h) ⊗≫ 𝟙 h =
  𝟙 (r ≫ g) ⊗≫ rightZigzag adj.unit adj.counit ▷ g ⊗≫ β
Tactic: calc
      _ = 𝟙 _ ⊗≫ r ◁ adj.unit ▷ g ⊗≫ ((r ≫ l) ◁ β ≫ adj.counit ▷ h) ⊗≫ 𝟙 _ := by
        bicategory
      _ = 𝟙 _ ⊗≫ rightZigzag adj.unit adj.counit ▷ g ⊗≫ β := by
        rw [whisker_exchange]
        bicategory
      _ = β := 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
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : b ⟶ d
h : c ⟶ d
β : r ≫ g ⟶ h
_ :
  (fun (γ : g ⟶ l ≫ h) ↦ r ◁ γ ≫ (α_ r l h).inv ≫ adj.counit ▷ h ≫ (λ_ h).hom)
      ((fun (β : r ≫ g ⟶ h) ↦ (λ_ g).inv ≫ adj.unit ▷ g ≫ (α_ l r g).hom ≫ l ◁ β) β) =
    𝟙 (r ≫ g) ⊗≫ r ◁ adj.unit ▷ g ⊗≫ ((r ≫ l) ◁ β ≫ adj.counit ▷ h) ⊗≫ 𝟙 h
_₁ :
  𝟙 (r ≫ g) ⊗≫ r ◁ adj.unit ▷ g ⊗≫ ((r ≫ l) ◁ β ≫ adj.counit ▷ h) ⊗≫ 𝟙 h =
    𝟙 (r ≫ g) ⊗≫ rightZigzag adj.unit adj.counit ▷ g ⊗≫ β
⊢ (fun (γ : g ⟶ l ≫ h) ↦ r ◁ γ ≫ (α_ r l h).inv ≫ adj.counit ▷ h ≫ (λ_ h).hom)
      ((fun (β : r ≫ g ⟶ h) ↦ (λ_ g).inv ≫ adj.unit ▷ g ≫ (α_ l r g).hom ≫ l ◁ β) β) =
    β
have _₂ : 𝟙 (r ≫ g) ⊗≫ rightZigzag adj.unit adj.counit ▷ g ⊗≫ β = β
Tactic: calc
      _ = 𝟙 _ ⊗≫ r ◁ adj.unit ▷ g ⊗≫ ((r ≫ l) ◁ β ≫ adj.counit ▷ h) ⊗≫ 𝟙 _ := by
        bicategory
      _ = 𝟙 _ ⊗≫ rightZigzag adj.unit adj.counit ▷ g ⊗≫ β := by
        rw [whisker_exchange]
        bicategory
      _ = β := 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
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : a ⟶ b
h : a ⟶ c
α : g ≫ l ⟶ h
⊢ 𝟙 (g ≫ l) ⊗≫ g ◁ adj.unit ▷ l ⊗≫ (α ▷ (r ≫ l) ≫ h ◁ adj.counit) ⊗≫ 𝟙 h =
    𝟙 (g ≫ l) ⊗≫ g ◁ leftZigzag adj.unit adj.counit ⊗≫ α
have rw : 𝟙 (g ≫ l) ⊗≫ g ◁ adj.unit ▷ l ⊗≫ ((g ≫ l) ◁ adj.counit ≫ α ▷ 𝟙 c) ⊗≫ 𝟙 h =
  𝟙 (g ≫ l) ⊗≫ g ◁ leftZigzag adj.unit adj.counit ⊗≫ α
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 : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : a ⟶ b
h : a ⟶ c
α : g ≫ l ⟶ h
⊢ 𝟙 (g ≫ l) ⊗≫ g ◁ leftZigzag adj.unit adj.counit ⊗≫ α = α
have rw : 𝟙 (g ≫ l) ⊗≫ g ◁ ((λ_ l).hom ≫ (ρ_ l).inv) ⊗≫ α = α
Tactic: rw [adj.left_triangle]
-- 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 : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : a ⟶ b
h : a ⟶ c
γ : g ⟶ h ≫ r
⊢ 𝟙 g ⊗≫ (g ◁ adj.unit ≫ γ ▷ (l ≫ r)) ⊗≫ h ◁ adj.counit ▷ r ⊗≫ 𝟙 (h ≫ r) =
    𝟙 g ⊗≫ γ ⊗≫ h ◁ rightZigzag adj.unit adj.counit ⊗≫ 𝟙 (h ≫ r)
have rw : 𝟙 g ⊗≫ (γ ▷ 𝟙 b ≫ (h ≫ r) ◁ adj.unit) ⊗≫ h ◁ adj.counit ▷ r ⊗≫ 𝟙 (h ≫ r) =
  𝟙 g ⊗≫ γ ⊗≫ h ◁ rightZigzag adj.unit adj.counit ⊗≫ 𝟙 (h ≫ r)
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 : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : a ⟶ b
h : a ⟶ c
γ : g ⟶ h ≫ r
⊢ 𝟙 g ⊗≫ γ ⊗≫ h ◁ rightZigzag adj.unit adj.counit ⊗≫ 𝟙 (h ≫ r) = γ
have rw : 𝟙 g ⊗≫ γ ⊗≫ h ◁ ((ρ_ r).hom ≫ (λ_ r).inv) ⊗≫ 𝟙 (h ≫ 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 e f : B
g : c ⟶ e
h : d ⟶ f
l₁ : c ⟶ d
r₁ : d ⟶ c
l₂ : e ⟶ f
r₂ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : g ≫ l₂ ⟶ l₁ ≫ h
β : r₁ ≫ g ⟶ h ≫ r₂
| (mateEquiv adj₁ adj₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α = β
have rw : Eq (α := g ⟶ l₁ ≫ h ≫ r₂) ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂) β : g ⟶ l₁ ≫ h ≫ r₂)
  ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂)
      ((mateEquiv adj₁ adj₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α : r₁ ≫ g ⟶ h ≫ r₂) :
    g ⟶ l₁ ≫ h ≫ r₂)
Tactic: rw [eq_comm, ← adj₁.homEquiv₁.symm.injective.eq_iff']
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c d e f : B
g : c ⟶ e
h : d ⟶ f
l₁ : c ⟶ d
r₁ : d ⟶ c
l₂ : e ⟶ f
r₂ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : g ≫ l₂ ⟶ l₁ ≫ h
β : r₁ ≫ g ⟶ h ≫ r₂
rw :
  Eq (α := g ⟶ l₁ ≫ h ≫ r₂) ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂) β : g ⟶ l₁ ≫ h ≫ r₂)
    ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂)
        ((mateEquiv adj₁ adj₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α : r₁ ≫ g ⟶ h ≫ r₂) :
      g ⟶ l₁ ≫ h ≫ r₂)
| (mateEquiv adj₁ adj₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α = β
have rw₁ : Eq (α := g ⟶ l₁ ≫ h ≫ r₂)
  ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂)
      ((mateEquiv adj₁ adj₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α : r₁ ≫ g ⟶ h ≫ r₂) :
    g ⟶ l₁ ≫ h ≫ r₂)
  ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂)
      ((mateEquiv adj₁ adj₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α : r₁ ≫ g ⟶ h ≫ r₂) :
    g ⟶ l₁ ≫ h ≫ r₂)
Tactic: rw [eq_comm, ← adj₁.homEquiv₁.symm.injective.eq_iff']
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c d e f : B
g : c ⟶ e
h : d ⟶ f
l₁ : c ⟶ d
r₁ : d ⟶ c
l₂ : e ⟶ f
r₂ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : g ≫ l₂ ⟶ l₁ ≫ h
β : r₁ ≫ g ⟶ h ≫ r₂
rw :
  Eq (α := g ⟶ l₁ ≫ h ≫ r₂) ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂) β : g ⟶ l₁ ≫ h ≫ r₂)
    ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂)
        ((mateEquiv adj₁ adj₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α : r₁ ≫ g ⟶ h ≫ r₂) :
      g ⟶ l₁ ≫ h ≫ r₂)
rw₁ :
  Eq (α := g ⟶ l₁ ≫ h ≫ r₂)
    ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂)
        ((mateEquiv adj₁ adj₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α : r₁ ≫ g ⟶ h ≫ r₂) :
      g ⟶ l₁ ≫ h ≫ r₂)
    ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂)
        ((mateEquiv adj₁ adj₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α : r₁ ≫ g ⟶ h ≫ r₂) :
      g ⟶ l₁ ≫ h ≫ r₂)
| (mateEquiv adj₁ adj₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α = β
have rw₂ : g ⟶ l₁ ≫ h ≫ r₂
Tactic: rw [eq_comm, ← adj₁.homEquiv₁.symm.injective.eq_iff']
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c d e f : B
g : c ⟶ e
h : d ⟶ f
l₁ : c ⟶ d
r₁ : d ⟶ c
l₂ : e ⟶ f
r₂ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : g ≫ l₂ ⟶ l₁ ≫ h
β : r₁ ≫ g ⟶ h ≫ r₂
⊢ (mateEquiv adj₁ adj₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α = β ↔
    Eq (α := g ⟶ l₁ ≫ h ≫ r₂)
      ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂) β : g ⟶ l₁ ≫ h ≫ r₂)
      ((adj₂.homEquiv₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → g ⟶ (l₁ ≫ h) ≫ r₂) α ≫ (α_ l₁ h r₂).hom : g ⟶ l₁ ≫ h ≫ r₂)
have conv_lhs : Eq (α := g ⟶ l₁ ≫ h ≫ r₂) ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂) β : g ⟶ l₁ ≫ h ≫ r₂)
    ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂)
        ((mateEquiv adj₁ adj₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α : r₁ ≫ g ⟶ h ≫ r₂) :
      g ⟶ l₁ ≫ h ≫ r₂) ↔
  Eq (α := g ⟶ l₁ ≫ h ≫ r₂) ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂) β : g ⟶ l₁ ≫ h ≫ r₂)
    ((adj₂.homEquiv₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → g ⟶ (l₁ ≫ h) ≫ r₂) α ≫ (α_ l₁ h r₂).hom : g ⟶ l₁ ≫ h ≫ r₂)
Tactic: conv_lhs => rw [eq_comm, ← adj₁.homEquiv₁.symm.injective.eq_iff']
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c d e f : B
g : c ⟶ e
h : d ⟶ f
l₁ : c ⟶ d
r₁ : d ⟶ c
l₂ : e ⟶ f
r₂ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : g ≫ l₂ ⟶ l₁ ≫ h
β : r₁ ≫ g ⟶ h ≫ r₂
⊢ Eq (α := g ⟶ l₁ ≫ h ≫ r₂) ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂) β : g ⟶ l₁ ≫ h ≫ r₂)
      ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂)
          ((mateEquiv adj₁ adj₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α : r₁ ≫ g ⟶ h ≫ r₂) :
        g ⟶ l₁ ≫ h ≫ r₂) ↔
    Eq (α := g ⟶ l₁ ≫ h ≫ r₂)
      ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂) β : g ⟶ l₁ ≫ h ≫ r₂)
      ((adj₂.homEquiv₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → g ⟶ (l₁ ≫ h) ≫ r₂) α ≫ (α_ l₁ h r₂).hom : g ⟶ l₁ ≫ h ≫ r₂)
have rw : Eq (α := g ⟶ l₁ ≫ h ≫ r₂) ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂) β : g ⟶ l₁ ≫ h ≫ r₂)
    ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂)
        ((adj₁.homEquiv₁ : (a : g ⟶ l₁ ≫ h ≫ r₂) → r₁ ≫ g ⟶ h ≫ r₂)
            ((adj₂.homEquiv₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → g ⟶ (l₁ ≫ h) ≫ r₂) α ≫ (α_ l₁ h r₂).hom : g ⟶ l₁ ≫ h ≫ r₂) :
          r₁ ≫ g ⟶ h ≫ r₂) :
      g ⟶ l₁ ≫ h ≫ r₂) ↔
  Eq (α := g ⟶ l₁ ≫ h ≫ r₂) ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂) β : g ⟶ l₁ ≫ h ≫ r₂)
    ((adj₂.homEquiv₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → g ⟶ (l₁ ≫ h) ≫ r₂) α ≫ (α_ l₁ h r₂).hom : g ⟶ l₁ ≫ h ≫ r₂)
Tactic: rw [mateEquiv_apply, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c d e f : B
g : c ⟶ e
h : d ⟶ f
l₁ : c ⟶ d
r₁ : d ⟶ c
l₂ : e ⟶ f
r₂ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : g ≫ l₂ ⟶ l₁ ≫ h
β : r₁ ≫ g ⟶ h ≫ r₂
rw :
  Eq (α := g ⟶ l₁ ≫ h ≫ r₂) ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂) β : g ⟶ l₁ ≫ h ≫ r₂)
      ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂)
          ((adj₁.homEquiv₁ : (a : g ⟶ l₁ ≫ h ≫ r₂) → r₁ ≫ g ⟶ h ≫ r₂)
              ((adj₂.homEquiv₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → g ⟶ (l₁ ≫ h) ≫ r₂) α ≫ (α_ l₁ h r₂).hom : g ⟶ l₁ ≫ h ≫ r₂) :
            r₁ ≫ g ⟶ h ≫ r₂) :
        g ⟶ l₁ ≫ h ≫ r₂) ↔
    Eq (α := g ⟶ l₁ ≫ h ≫ r₂)
      ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂) β : g ⟶ l₁ ≫ h ≫ r₂)
      ((adj₂.homEquiv₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → g ⟶ (l₁ ≫ h) ≫ r₂) α ≫ (α_ l₁ h r₂).hom : g ⟶ l₁ ≫ h ≫ r₂)
⊢ Eq (α := g ⟶ l₁ ≫ h ≫ r₂) ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂) β : g ⟶ l₁ ≫ h ≫ r₂)
      ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂)
          ((mateEquiv adj₁ adj₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α : r₁ ≫ g ⟶ h ≫ r₂) :
        g ⟶ l₁ ≫ h ≫ r₂) ↔
    Eq (α := g ⟶ l₁ ≫ h ≫ r₂)
      ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂) β : g ⟶ l₁ ≫ h ≫ r₂)
      ((adj₂.homEquiv₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → g ⟶ (l₁ ≫ h) ≫ r₂) α ≫ (α_ l₁ h r₂).hom : g ⟶ l₁ ≫ h ≫ r₂)
have rw₁ : Eq (α := g ⟶ l₁ ≫ h ≫ r₂) ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂) β : g ⟶ l₁ ≫ h ≫ r₂)
    ((adj₂.homEquiv₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → g ⟶ (l₁ ≫ h) ≫ r₂) α ≫ (α_ l₁ h r₂).hom : g ⟶ l₁ ≫ h ≫ r₂) ↔
  Eq (α := g ⟶ l₁ ≫ h ≫ r₂) ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂) β : g ⟶ l₁ ≫ h ≫ r₂)
    ((adj₂.homEquiv₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → g ⟶ (l₁ ≫ h) ≫ r₂) α ≫ (α_ l₁ h r₂).hom : g ⟶ l₁ ≫ h ≫ r₂)
Tactic: rw [mateEquiv_apply, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c d e f : B
g : c ⟶ e
h : d ⟶ f
l₁ : c ⟶ d
r₁ : d ⟶ c
l₂ : e ⟶ f
r₂ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : g ≫ l₂ ⟶ l₁ ≫ h
⊢ (mateEquiv adj₁ adj₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α =
    𝟙 (r₁ ≫ g) ⊗≫ r₁ ◁ g ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h ▷ r₂ ⊗≫ 𝟙 (h ≫ r₂)
have rw : r₁ ◁ (((ρ_ g).inv ≫ g ◁ adj₂.unit ≫ (α_ g l₂ r₂).inv ≫ α ▷ r₂) ≫ (α_ l₁ h r₂).hom) ≫
    (α_ r₁ l₁ (h ≫ r₂)).inv ≫ adj₁.counit ▷ (h ≫ r₂) ≫ (λ_ (h ≫ r₂)).hom =
  𝟙 (r₁ ≫ g) ⊗≫ r₁ ◁ g ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h ▷ r₂ ⊗≫ 𝟙 (h ≫ r₂)
Tactic: rw [mateEquiv_apply, Adjunction.homEquiv₂_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 e f : B
g : c ⟶ e
h : d ⟶ f
l₁ : c ⟶ d
r₁ : d ⟶ c
l₂ : e ⟶ f
r₂ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
β : r₁ ≫ g ⟶ h ≫ r₂
⊢ (Equiv.symm (mateEquiv adj₁ adj₂) : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ≫ l₂ ⟶ l₁ ≫ h) β =
    𝟙 (g ≫ l₂) ⊗≫ adj₁.unit ▷ g ▷ l₂ ⊗≫ l₁ ◁ β ▷ l₂ ⊗≫ l₁ ◁ h ◁ adj₂.counit ⊗≫ 𝟙 (l₁ ≫ h)
have rw : (((λ_ g).inv ≫ adj₁.unit ▷ g ≫ (α_ l₁ r₁ g).hom ≫ l₁ ◁ β) ≫ (α_ l₁ h r₂).inv) ▷ l₂ ≫
    (α_ (l₁ ≫ h) r₂ l₂).hom ≫ (l₁ ≫ h) ◁ adj₂.counit ≫ (ρ_ (l₁ ≫ h)).hom =
  𝟙 (g ≫ l₂) ⊗≫ adj₁.unit ▷ g ▷ l₂ ⊗≫ l₁ ◁ β ▷ l₂ ⊗≫ l₁ ◁ h ◁ adj₂.counit ⊗≫ 𝟙 (l₁ ≫ h)
Tactic: rw [mateEquiv_symm_apply, Adjunction.homEquiv₂_symm_apply, Adjunction.homEquiv₁_symm_apply]
-- 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₂ : c ⟶ d
r₂ : d ⟶ c
adj₂ : l₂ ⊣ r₂
f : a ⟶ c
g : b ⟶ d
φ : f ≫ 𝟙 c ≫ l₂ ⟶ l₁ ≫ g
⊢ Eq (α := r₁ ≫ f ⟶ g ≫ r₂ ≫ 𝟙 c)
    ((mateEquiv adj₁ (Adjunction.comp (Adjunction.id c) adj₂) : (a_1 : f ≫ 𝟙 c ≫ l₂ ⟶ l₁ ≫ g) → r₁ ≫ f ⟶ g ≫ r₂ ≫ 𝟙 c)
        φ :
      r₁ ≫ f ⟶ g ≫ r₂ ≫ 𝟙 c)
    ((mateEquiv adj₁ adj₂ : (a_1 : f ≫ l₂ ⟶ l₁ ≫ g) → r₁ ≫ f ⟶ g ≫ r₂) (f ◁ (λ_ l₂).inv ≫ φ) ≫
        (ρ_ (g ≫ r₂)).inv ≫ (α_ g r₂ (𝟙 c)).hom :
      r₁ ≫ f ⟶ g ≫ r₂ ≫ 𝟙 c)
have simp : r₁ ◁
      (((ρ_ f).inv ≫
          f ◁
              (Adjunction.comp
                  { unit := Iso.inv (ρ_ (𝟙 c)), counit := Iso.hom (ρ_ (𝟙 c)), left_triangle := sorry, right_triangle := sorry :
                    Adjunction.{w, v, u} (𝟙 c) (𝟙 c) }
                  adj₂).unit ≫
            (α_ f (𝟙 c ≫ l₂) (r₂ ≫ 𝟙 c)).inv ≫ φ ▷ (r₂ ≫ 𝟙 c)) ≫
        (α_ l₁ g (r₂ ≫ 𝟙 c)).hom) ≫
    (α_ r₁ l₁ (g ≫ r₂ ≫ 𝟙 c)).inv ≫ adj₁.counit ▷ (g ≫ r₂ ≫ 𝟙 c) ≫ (λ_ (g ≫ r₂ ≫ 𝟙 c)).hom =
  (r₁ ◁ (((ρ_ f).inv ≫ f ◁ adj₂.unit ≫ (α_ f l₂ r₂).inv ≫ (f ◁ (λ_ l₂).inv ≫ φ) ▷ r₂) ≫ (α_ l₁ g r₂).hom) ≫
      (α_ r₁ l₁ (g ≫ r₂)).inv ≫ adj₁.counit ▷ (g ≫ r₂) ≫ (λ_ (g ≫ r₂)).hom) ≫
    (ρ_ (g ≫ r₂)).inv ≫ (α_ g r₂ (𝟙 c)).hom
Tactic: simp only [mateEquiv_apply, Adjunction.homEquiv₁_apply, Adjunction.homEquiv₂_apply,
    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 c d : B
l₁ : a ⟶ b
r₁ : b ⟶ a
adj₁ : l₁ ⊣ r₁
l₂ : c ⟶ d
r₂ : d ⟶ c
adj₂ : l₂ ⊣ r₂
f : a ⟶ c
g : b ⟶ d
φ : f ≫ 𝟙 c ≫ l₂ ⟶ l₁ ≫ g
⊢ r₁ ◁
        (((ρ_ f).inv ≫
            f ◁
                (Adjunction.comp
                    { unit := Iso.inv (ρ_ (𝟙 c)), counit := Iso.hom (ρ_ (𝟙 c)), left_triangle := ⋯,
                      right_triangle := ⋯ : Adjunction.{w, v, u} (𝟙 c) (𝟙 c) }
                    adj₂).unit ≫
              (α_ f (𝟙 c ≫ l₂) (r₂ ≫ 𝟙 c)).inv ≫ φ ▷ (r₂ ≫ 𝟙 c)) ≫
          (α_ l₁ g (r₂ ≫ 𝟙 c)).hom) ≫
      (α_ r₁ l₁ (g ≫ r₂ ≫ 𝟙 c)).inv ≫ adj₁.counit ▷ (g ≫ r₂ ≫ 𝟙 c) ≫ (λ_ (g ≫ r₂ ≫ 𝟙 c)).hom =
    (r₁ ◁ (((ρ_ f).inv ≫ f ◁ adj₂.unit ≫ (α_ f l₂ r₂).inv ≫ (f ◁ (λ_ l₂).inv ≫ φ) ▷ r₂) ≫ (α_ l₁ g r₂).hom) ≫
        (α_ r₁ l₁ (g ≫ r₂)).inv ≫ adj₁.counit ▷ (g ≫ r₂) ≫ (λ_ (g ≫ r₂)).hom) ≫
      (ρ_ (g ≫ r₂)).inv ≫ (α_ g r₂ (𝟙 c)).hom
have dsimp : r₁ ◁
      (((ρ_ f).inv ≫
          f ◁
              bicategoricalComp (h := 𝟙 c ≫ 𝟙 c ≫ 𝟙 c) (Iso.inv (ρ_ (𝟙 c)))
                (𝟙 c ◁ adj₂.unit ▷ 𝟙 c ⊗≫ 𝟙 ((𝟙 c ≫ l₂) ≫ r₂ ≫ 𝟙 c)) ≫
            (α_ f (𝟙 c ≫ l₂) (r₂ ≫ 𝟙 c)).inv ≫ φ ▷ (r₂ ≫ 𝟙 c)) ≫
        (α_ l₁ g (r₂ ≫ 𝟙 c)).hom) ≫
    (α_ r₁ l₁ (g ≫ r₂ ≫ 𝟙 c)).inv ≫ adj₁.counit ▷ (g ≫ r₂ ≫ 𝟙 c) ≫ (λ_ (g ≫ r₂ ≫ 𝟙 c)).hom =
  (r₁ ◁ (((ρ_ f).inv ≫ f ◁ adj₂.unit ≫ (α_ f l₂ r₂).inv ≫ (f ◁ (λ_ l₂).inv ≫ φ) ▷ r₂) ≫ (α_ l₁ g r₂).hom) ≫
      (α_ r₁ l₁ (g ≫ r₂)).inv ≫ adj₁.counit ▷ (g ≫ r₂) ≫ (λ_ (g ≫ r₂)).hom) ≫
    (ρ_ (g ≫ r₂)).inv ≫ (α_ g r₂ (𝟙 c)).hom
Tactic: dsimp