awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ 𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      adj₁.unit ▷ (f₁ ≫ f₂) ⊗≫
        f₁ ◁ (adj₂.unit ▷ (g₁ ≫ f₁) ≫ (f₂ ≫ g₂) ◁ adj₁.counit) ▷ f₂ ⊗≫ (f₁ ≫ f₂) ◁ adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c) =
    𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      leftZigzag adj₁.unit adj₁.counit ▷ f₂ ⊗≫ f₁ ◁ leftZigzag adj₂.unit adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c)
have rw : 𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
    adj₁.unit ▷ (f₁ ≫ f₂) ⊗≫
      f₁ ◁ (𝟙 b ◁ adj₁.counit ≫ adj₂.unit ▷ 𝟙 b) ▷ f₂ ⊗≫ (f₁ ≫ f₂) ◁ adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c) =
  𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
    leftZigzag adj₁.unit adj₁.counit ▷ f₂ ⊗≫ f₁ ◁ leftZigzag adj₂.unit adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c)
Tactic: rw [← whisker_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ 𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      leftZigzag adj₁.unit adj₁.counit ▷ f₂ ⊗≫ f₁ ◁ leftZigzag adj₂.unit adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c) =
    (λ_ (f₁ ≫ f₂)).hom ≫ (ρ_ (f₁ ≫ f₂)).inv
have simp_rw : 𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫ ((λ_ f₁).hom ≫ (ρ_ f₁).inv) ▷ f₂ ⊗≫ f₁ ◁ ((λ_ f₂).hom ≫ (ρ_ f₂).inv) ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c) =
  (λ_ (f₁ ≫ f₂)).hom ≫ (ρ_ (f₁ ≫ f₂)).inv
Tactic: simp_rw [left_triangle]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ leftZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) = (λ_ (f₁ ≫ f₂)).hom ≫ (ρ_ (f₁ ≫ f₂)).inv
have _ : leftZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) =
  𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
    adj₁.unit ▷ (f₁ ≫ f₂) ⊗≫
      f₁ ◁ (adj₂.unit ▷ (g₁ ≫ f₁) ≫ (f₂ ≫ g₂) ◁ adj₁.counit) ▷ f₂ ⊗≫ (f₁ ≫ f₂) ◁ adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c)
Tactic: calc
    _ = 𝟙 _ ⊗≫
          adj₁.unit ▷ (f₁ ≫ f₂) ⊗≫
            f₁ ◁ (adj₂.unit ▷ (g₁ ≫ f₁) ≫ (f₂ ≫ g₂) ◁ adj₁.counit) ▷ f₂ ⊗≫
              (f₁ ≫ f₂) ◁ adj₂.counit ⊗≫ 𝟙 _ := by
      dsimp only [compUnit, compCounit]; bicategory
    _ = 𝟙 _ ⊗≫
          (leftZigzag adj₁.unit adj₁.counit) ▷ f₂ ⊗≫
            f₁ ◁ (leftZigzag adj₂.unit adj₂.counit) ⊗≫ 𝟙 _ := by
      rw [← whisker_exchange]; bicategory
    _ = _ := by
      simp_rw [left_triangle]; bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
_ :
  leftZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) =
    𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      adj₁.unit ▷ (f₁ ≫ f₂) ⊗≫
        f₁ ◁ (adj₂.unit ▷ (g₁ ≫ f₁) ≫ (f₂ ≫ g₂) ◁ adj₁.counit) ▷ f₂ ⊗≫ (f₁ ≫ f₂) ◁ adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c)
⊢ leftZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) = (λ_ (f₁ ≫ f₂)).hom ≫ (ρ_ (f₁ ≫ f₂)).inv
have _₁ : 𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
    adj₁.unit ▷ (f₁ ≫ f₂) ⊗≫
      f₁ ◁ (adj₂.unit ▷ (g₁ ≫ f₁) ≫ (f₂ ≫ g₂) ◁ adj₁.counit) ▷ f₂ ⊗≫ (f₁ ≫ f₂) ◁ adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c) =
  𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
    leftZigzag adj₁.unit adj₁.counit ▷ f₂ ⊗≫ f₁ ◁ leftZigzag adj₂.unit adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c)
Tactic: calc
    _ = 𝟙 _ ⊗≫
          adj₁.unit ▷ (f₁ ≫ f₂) ⊗≫
            f₁ ◁ (adj₂.unit ▷ (g₁ ≫ f₁) ≫ (f₂ ≫ g₂) ◁ adj₁.counit) ▷ f₂ ⊗≫
              (f₁ ≫ f₂) ◁ adj₂.counit ⊗≫ 𝟙 _ := by
      dsimp only [compUnit, compCounit]; bicategory
    _ = 𝟙 _ ⊗≫
          (leftZigzag adj₁.unit adj₁.counit) ▷ f₂ ⊗≫
            f₁ ◁ (leftZigzag adj₂.unit adj₂.counit) ⊗≫ 𝟙 _ := by
      rw [← whisker_exchange]; bicategory
    _ = _ := by
      simp_rw [left_triangle]; bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
_ :
  leftZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) =
    𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      adj₁.unit ▷ (f₁ ≫ f₂) ⊗≫
        f₁ ◁ (adj₂.unit ▷ (g₁ ≫ f₁) ≫ (f₂ ≫ g₂) ◁ adj₁.counit) ▷ f₂ ⊗≫ (f₁ ≫ f₂) ◁ adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c)
_₁ :
  𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      adj₁.unit ▷ (f₁ ≫ f₂) ⊗≫
        f₁ ◁ (adj₂.unit ▷ (g₁ ≫ f₁) ≫ (f₂ ≫ g₂) ◁ adj₁.counit) ▷ f₂ ⊗≫ (f₁ ≫ f₂) ◁ adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c) =
    𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      leftZigzag adj₁.unit adj₁.counit ▷ f₂ ⊗≫ f₁ ◁ leftZigzag adj₂.unit adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c)
⊢ leftZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) = (λ_ (f₁ ≫ f₂)).hom ≫ (ρ_ (f₁ ≫ f₂)).inv
have _₂ : 𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
    leftZigzag adj₁.unit adj₁.counit ▷ f₂ ⊗≫ f₁ ◁ leftZigzag adj₂.unit adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c) =
  (λ_ (f₁ ≫ f₂)).hom ≫ (ρ_ (f₁ ≫ f₂)).inv
Tactic: calc
    _ = 𝟙 _ ⊗≫
          adj₁.unit ▷ (f₁ ≫ f₂) ⊗≫
            f₁ ◁ (adj₂.unit ▷ (g₁ ≫ f₁) ≫ (f₂ ≫ g₂) ◁ adj₁.counit) ▷ f₂ ⊗≫
              (f₁ ≫ f₂) ◁ adj₂.counit ⊗≫ 𝟙 _ := by
      dsimp only [compUnit, compCounit]; bicategory
    _ = 𝟙 _ ⊗≫
          (leftZigzag adj₁.unit adj₁.counit) ▷ f₂ ⊗≫
            f₁ ◁ (leftZigzag adj₂.unit adj₂.counit) ⊗≫ 𝟙 _ := by
      rw [← whisker_exchange]; bicategory
    _ = _ := by
      simp_rw [left_triangle]; bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ rightZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) =
    𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
        g₂ ◁ ((g₁ ≫ f₁) ◁ adj₂.unit ≫ adj₁.counit ▷ (f₂ ≫ g₂)) ▷ g₁ ⊗≫ adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁)
have dsimp : rightZigzag (adj₁.unit ⊗≫ f₁ ◁ adj₂.unit ▷ g₁ ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ g₂ ≫ g₁))
    (𝟙 ((g₂ ≫ g₁) ≫ f₁ ≫ f₂) ⊗≫ g₂ ◁ adj₁.counit ▷ f₂ ⊗≫ adj₂.counit) =
  𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
    (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
      g₂ ◁ ((g₁ ≫ f₁) ◁ adj₂.unit ≫ adj₁.counit ▷ (f₂ ≫ g₂)) ▷ g₁ ⊗≫ adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁)
Tactic: dsimp only [compUnit, compCounit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ 𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
        g₂ ◁ ((g₁ ≫ f₁) ◁ adj₂.unit ≫ adj₁.counit ▷ (f₂ ≫ g₂)) ▷ g₁ ⊗≫ adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁) =
    𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      g₂ ◁ rightZigzag adj₁.unit adj₁.counit ⊗≫ rightZigzag adj₂.unit adj₂.counit ▷ g₁ ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁)
have rw : 𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
    (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
      g₂ ◁ (adj₁.counit ▷ 𝟙 b ≫ 𝟙 b ◁ adj₂.unit) ▷ g₁ ⊗≫ adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁) =
  𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
    g₂ ◁ rightZigzag adj₁.unit adj₁.counit ⊗≫ rightZigzag adj₂.unit adj₂.counit ▷ g₁ ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁)
Tactic: rw [whisker_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ 𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      g₂ ◁ rightZigzag adj₁.unit adj₁.counit ⊗≫ rightZigzag adj₂.unit adj₂.counit ▷ g₁ ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁) =
    (ρ_ (g₂ ≫ g₁)).hom ≫ (λ_ (g₂ ≫ g₁)).inv
have simp_rw : 𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫ g₂ ◁ ((ρ_ g₁).hom ≫ (λ_ g₁).inv) ⊗≫ ((ρ_ g₂).hom ≫ (λ_ g₂).inv) ▷ g₁ ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁) =
  (ρ_ (g₂ ≫ g₁)).hom ≫ (λ_ (g₂ ≫ g₁)).inv
Tactic: simp_rw [right_triangle]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ rightZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) = (ρ_ (g₂ ≫ g₁)).hom ≫ (λ_ (g₂ ≫ g₁)).inv
have _ : rightZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) =
  𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
    (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
      g₂ ◁ ((g₁ ≫ f₁) ◁ adj₂.unit ≫ adj₁.counit ▷ (f₂ ≫ g₂)) ▷ g₁ ⊗≫ adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁)
Tactic: calc
    _ = 𝟙 _ ⊗≫
          (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
            g₂ ◁ ((g₁ ≫ f₁) ◁ adj₂.unit ≫ adj₁.counit ▷ (f₂ ≫ g₂)) ▷ g₁ ⊗≫
              adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 _ := by
      dsimp only [compUnit, compCounit]; bicategory
    _ = 𝟙 _ ⊗≫
          g₂ ◁ (rightZigzag adj₁.unit adj₁.counit) ⊗≫
            (rightZigzag adj₂.unit adj₂.counit) ▷ g₁ ⊗≫ 𝟙 _ := by
      rw [whisker_exchange]; bicategory
    _ = _ := by
      simp_rw [right_triangle]; bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
_ :
  rightZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) =
    𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
        g₂ ◁ ((g₁ ≫ f₁) ◁ adj₂.unit ≫ adj₁.counit ▷ (f₂ ≫ g₂)) ▷ g₁ ⊗≫ adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁)
⊢ rightZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) = (ρ_ (g₂ ≫ g₁)).hom ≫ (λ_ (g₂ ≫ g₁)).inv
have _₁ : 𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
    (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
      g₂ ◁ ((g₁ ≫ f₁) ◁ adj₂.unit ≫ adj₁.counit ▷ (f₂ ≫ g₂)) ▷ g₁ ⊗≫ adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁) =
  𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
    g₂ ◁ rightZigzag adj₁.unit adj₁.counit ⊗≫ rightZigzag adj₂.unit adj₂.counit ▷ g₁ ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁)
Tactic: calc
    _ = 𝟙 _ ⊗≫
          (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
            g₂ ◁ ((g₁ ≫ f₁) ◁ adj₂.unit ≫ adj₁.counit ▷ (f₂ ≫ g₂)) ▷ g₁ ⊗≫
              adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 _ := by
      dsimp only [compUnit, compCounit]; bicategory
    _ = 𝟙 _ ⊗≫
          g₂ ◁ (rightZigzag adj₁.unit adj₁.counit) ⊗≫
            (rightZigzag adj₂.unit adj₂.counit) ▷ g₁ ⊗≫ 𝟙 _ := by
      rw [whisker_exchange]; bicategory
    _ = _ := by
      simp_rw [right_triangle]; bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
_ :
  rightZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) =
    𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
        g₂ ◁ ((g₁ ≫ f₁) ◁ adj₂.unit ≫ adj₁.counit ▷ (f₂ ≫ g₂)) ▷ g₁ ⊗≫ adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁)
_₁ :
  𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
        g₂ ◁ ((g₁ ≫ f₁) ◁ adj₂.unit ≫ adj₁.counit ▷ (f₂ ≫ g₂)) ▷ g₁ ⊗≫ adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁) =
    𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      g₂ ◁ rightZigzag adj₁.unit adj₁.counit ⊗≫ rightZigzag adj₂.unit adj₂.counit ▷ g₁ ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁)
⊢ rightZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) = (ρ_ (g₂ ≫ g₁)).hom ≫ (λ_ (g₂ ≫ g₁)).inv
have _₂ : 𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
    g₂ ◁ rightZigzag adj₁.unit adj₁.counit ⊗≫ rightZigzag adj₂.unit adj₂.counit ▷ g₁ ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁) =
  (ρ_ (g₂ ≫ g₁)).hom ≫ (λ_ (g₂ ≫ g₁)).inv
Tactic: calc
    _ = 𝟙 _ ⊗≫
          (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
            g₂ ◁ ((g₁ ≫ f₁) ◁ adj₂.unit ≫ adj₁.counit ▷ (f₂ ≫ g₂)) ▷ g₁ ⊗≫
              adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 _ := by
      dsimp only [compUnit, compCounit]; bicategory
    _ = 𝟙 _ ⊗≫
          g₂ ◁ (rightZigzag adj₁.unit adj₁.counit) ⊗≫
            (rightZigzag adj₂.unit adj₂.counit) ▷ g₁ ⊗≫ 𝟙 _ := by
      rw [whisker_exchange]; bicategory
    _ = _ := by
      simp_rw [right_triangle]; bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
h : leftZigzag η.hom ε.hom = (λ_ f).hom ≫ (ρ_ f).inv
⊢ rightZigzag η.hom ε.hom = (ρ_ g).hom ≫ (λ_ g).inv
have rw : (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv) ≫ rightZigzag η.hom ε.hom =
  (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv) ≫ (ρ_ g).hom ≫ (λ_ g).inv
Tactic: rw [← cancel_epi (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
h : leftZigzag η.hom ε.hom = (λ_ f).hom ≫ (ρ_ f).inv
⊢ (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv) ≫ rightZigzag η.hom ε.hom =
    (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv) ≫ (ρ_ g).hom ≫ (λ_ g).inv
have _ : (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv) ≫ rightZigzag η.hom ε.hom =
  rightZigzag η.hom ε.hom ⊗≫ rightZigzag η.hom ε.hom
Tactic: calc
    _ = rightZigzag η.hom ε.hom ⊗≫ rightZigzag η.hom ε.hom := by bicategory
    _ = rightZigzag η.hom ε.hom := rightZigzag_idempotent_of_left_triangle _ _ h
    _ = _ := by simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
h : leftZigzag η.hom ε.hom = (λ_ f).hom ≫ (ρ_ f).inv
_ :
  (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv) ≫ rightZigzag η.hom ε.hom =
    rightZigzag η.hom ε.hom ⊗≫ rightZigzag η.hom ε.hom
⊢ (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv) ≫ rightZigzag η.hom ε.hom =
    (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv) ≫ (ρ_ g).hom ≫ (λ_ g).inv
have _₁ : rightZigzag η.hom ε.hom = (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv) ≫ (ρ_ g).hom ≫ (λ_ g).inv
Tactic: calc
    _ = rightZigzag η.hom ε.hom ⊗≫ rightZigzag η.hom ε.hom := by bicategory
    _ = rightZigzag η.hom ε.hom := rightZigzag_idempotent_of_left_triangle _ _ h
    _ = _ := by simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ leftZigzagIso η (adjointifyCounit η ε) = λ_ f ≪≫ (ρ_ f).symm
have w : (leftZigzagIso η (adjointifyCounit η ε)).hom = (λ_ f ≪≫ (ρ_ f).symm).hom
Tactic: apply Iso.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ (leftZigzagIso η (adjointifyCounit η ε)).hom = (λ_ f ≪≫ (ρ_ f).symm).hom
have w : leftZigzag η.hom (g ◁ ((ρ_ f).inv ≫ rightZigzag ε.inv η.inv ≫ (λ_ f).hom) ≫ ε.hom) = (λ_ f).hom ≫ (ρ_ f).inv
Tactic: dsimp [adjointifyCounit, bicategoricalIsoComp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom =
    𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom
have rw : 𝟙 (𝟙 a ≫ f) ⊗≫ (𝟙 a ◁ f ◁ ε.inv ≫ η.hom ▷ (f ≫ g ≫ f)) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom =
  𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom
Tactic: rw [← whisker_exchange η.hom (f ◁ ε.inv)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom =
    𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom
have rw : 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (𝟙 a ◁ η.inv ≫ η.hom ▷ 𝟙 a) ▷ f ⊗≫ f ◁ ε.hom =
  𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom
Tactic: rw [← whisker_exchange η.hom η.inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom = 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ (ε.inv ≫ ε.hom)
have rw : 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ 𝟙 (f ≫ g) ▷ f ⊗≫ f ◁ ε.hom = 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ (ε.inv ≫ ε.hom)
Tactic: rw [Iso.inv_hom_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ (ε.inv ≫ ε.hom) = (λ_ f).hom ≫ (ρ_ f).inv
have rw : 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ 𝟙 (𝟙 b) = (λ_ f).hom ≫ (ρ_ f).inv
Tactic: rw [Iso.inv_hom_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ leftZigzag η.hom (g ◁ ((ρ_ f).inv ≫ rightZigzag ε.inv η.inv ≫ (λ_ f).hom) ≫ ε.hom) = (λ_ f).hom ≫ (ρ_ f).inv
have _ : leftZigzag η.hom (g ◁ ((ρ_ f).inv ≫ rightZigzag ε.inv η.inv ≫ (λ_ f).hom) ≫ ε.hom) =
  𝟙 (𝟙 a ≫ f) ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom
Tactic: calc
    _ = 𝟙 _ ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫
          f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom := by
      bicategory
    _ = 𝟙 _ ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom := by
      rw [← whisker_exchange η.hom (f ◁ ε.inv)]; bicategory
    _ = 𝟙 _ ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom := by
      rw [← whisker_exchange η.hom η.inv]; bicategory
    _ = 𝟙 _ ⊗≫ f ◁ (ε.inv ≫ ε.hom) := by
      rw [Iso.inv_hom_id]; bicategory
    _ = _ := by
      rw [Iso.inv_hom_id]; bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
_ :
  leftZigzag η.hom (g ◁ ((ρ_ f).inv ≫ rightZigzag ε.inv η.inv ≫ (λ_ f).hom) ≫ ε.hom) =
    𝟙 (𝟙 a ≫ f) ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom
⊢ leftZigzag η.hom (g ◁ ((ρ_ f).inv ≫ rightZigzag ε.inv η.inv ≫ (λ_ f).hom) ≫ ε.hom) = (λ_ f).hom ≫ (ρ_ f).inv
have _₁ : 𝟙 (𝟙 a ≫ f) ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom =
  𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom
Tactic: calc
    _ = 𝟙 _ ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫
          f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom := by
      bicategory
    _ = 𝟙 _ ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom := by
      rw [← whisker_exchange η.hom (f ◁ ε.inv)]; bicategory
    _ = 𝟙 _ ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom := by
      rw [← whisker_exchange η.hom η.inv]; bicategory
    _ = 𝟙 _ ⊗≫ f ◁ (ε.inv ≫ ε.hom) := by
      rw [Iso.inv_hom_id]; bicategory
    _ = _ := by
      rw [Iso.inv_hom_id]; bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
_ :
  leftZigzag η.hom (g ◁ ((ρ_ f).inv ≫ rightZigzag ε.inv η.inv ≫ (λ_ f).hom) ≫ ε.hom) =
    𝟙 (𝟙 a ≫ f) ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom
_₁ :
  𝟙 (𝟙 a ≫ f) ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom =
    𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom
⊢ leftZigzag η.hom (g ◁ ((ρ_ f).inv ≫ rightZigzag ε.inv η.inv ≫ (λ_ f).hom) ≫ ε.hom) = (λ_ f).hom ≫ (ρ_ f).inv
have _₂ : 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom =
  𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom
Tactic: calc
    _ = 𝟙 _ ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫
          f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom := by
      bicategory
    _ = 𝟙 _ ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom := by
      rw [← whisker_exchange η.hom (f ◁ ε.inv)]; bicategory
    _ = 𝟙 _ ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom := by
      rw [← whisker_exchange η.hom η.inv]; bicategory
    _ = 𝟙 _ ⊗≫ f ◁ (ε.inv ≫ ε.hom) := by
      rw [Iso.inv_hom_id]; bicategory
    _ = _ := by
      rw [Iso.inv_hom_id]; bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
_ :
  leftZigzag η.hom (g ◁ ((ρ_ f).inv ≫ rightZigzag ε.inv η.inv ≫ (λ_ f).hom) ≫ ε.hom) =
    𝟙 (𝟙 a ≫ f) ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom
_₁ :
  𝟙 (𝟙 a ≫ f) ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom =
    𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom
_₂ :
  𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom =
    𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom
⊢ leftZigzag η.hom (g ◁ ((ρ_ f).inv ≫ rightZigzag ε.inv η.inv ≫ (λ_ f).hom) ≫ ε.hom) = (λ_ f).hom ≫ (ρ_ f).inv
have _₃ : 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom = 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ (ε.inv ≫ ε.hom)
Tactic: calc
    _ = 𝟙 _ ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫
          f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom := by
      bicategory
    _ = 𝟙 _ ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom := by
      rw [← whisker_exchange η.hom (f ◁ ε.inv)]; bicategory
    _ = 𝟙 _ ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom := by
      rw [← whisker_exchange η.hom η.inv]; bicategory
    _ = 𝟙 _ ⊗≫ f ◁ (ε.inv ≫ ε.hom) := by
      rw [Iso.inv_hom_id]; bicategory
    _ = _ := by
      rw [Iso.inv_hom_id]; bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
_ :
  leftZigzag η.hom (g ◁ ((ρ_ f).inv ≫ rightZigzag ε.inv η.inv ≫ (λ_ f).hom) ≫ ε.hom) =
    𝟙 (𝟙 a ≫ f) ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom
_₁ :
  𝟙 (𝟙 a ≫ f) ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom =
    𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom
_₂ :
  𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom =
    𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom
_₃ : 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom = 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ (ε.inv ≫ ε.hom)
⊢ leftZigzag η.hom (g ◁ ((ρ_ f).inv ≫ rightZigzag ε.inv η.inv ≫ (λ_ f).hom) ≫ ε.hom) = (λ_ f).hom ≫ (ρ_ f).inv
have _₄ : 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ (ε.inv ≫ ε.hom) = (λ_ f).hom ≫ (ρ_ f).inv
Tactic: calc
    _ = 𝟙 _ ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫
          f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom := by
      bicategory
    _ = 𝟙 _ ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom := by
      rw [← whisker_exchange η.hom (f ◁ ε.inv)]; bicategory
    _ = 𝟙 _ ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom := by
      rw [← whisker_exchange η.hom η.inv]; bicategory
    _ = 𝟙 _ ⊗≫ f ◁ (ε.inv ≫ ε.hom) := by
      rw [Iso.inv_hom_id]; bicategory
    _ = _ := by
      rw [Iso.inv_hom_id]; bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a_1 b c : B
f : a_1 ⟶ b
g : b ⟶ a_1
η : 𝟙 a_1 ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
a : B
⊢ Eq.{w + 1} (α := Iso.{w, v} (C := a ⟶ a) (𝟙 a ≫ 𝟙 a) (𝟙 a ≫ 𝟙 a)) (leftZigzagIso (Iso.symm (ρ_ (𝟙 a))) (ρ_ (𝟙 a)))
    (λ_ (𝟙 a) ≪≫ Iso.symm (ρ_ (𝟙 a)))
have w : Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := a ⟶ a) (𝟙 a ≫ 𝟙 a) (𝟙 a ≫ 𝟙 a))
  (Iso.hom (leftZigzagIso (Iso.symm (ρ_ (𝟙 a))) (ρ_ (𝟙 a)))) (Iso.hom (λ_ (𝟙 a) ≪≫ Iso.symm (ρ_ (𝟙 a))))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Cat (goal)
Goal:
C D E : Cat
F : C ⟶ D
G : D ⟶ C
adj : F ⊣ G
F' : D ⟶ E
G' : E ⟶ D
adj' : F' ⊣ G'
⊢ Adjunction.ofCat (adj.comp adj') = (Adjunction.ofCat adj).comp (Adjunction.ofCat adj')
have h : ∀ (x : (↑C : Type u)),
  (Adjunction.ofCat (adj.comp adj')).unit.app x = ((Adjunction.ofCat adj).comp (Adjunction.ofCat adj')).unit.app x
Tactic: ext