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 : 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 ≫ l₂ ≫ 𝟙 d ⟶ l₁ ≫ g
⊢ Eq (α := r₁ ≫ f ⟶ g ≫ 𝟙 d ≫ r₂)
    ((mateEquiv adj₁ (adj₂.comp (Adjunction.id d)) : (a_1 : f ≫ l₂ ≫ 𝟙 d ⟶ l₁ ≫ g) → r₁ ≫ f ⟶ g ≫ 𝟙 d ≫ r₂) φ :
      r₁ ≫ f ⟶ g ≫ 𝟙 d ≫ r₂)
    ((mateEquiv adj₁ adj₂ : (a_1 : f ≫ l₂ ⟶ l₁ ≫ g) → r₁ ≫ f ⟶ g ≫ r₂) ((ρ_ (f ≫ l₂)).inv ≫ (α_ f l₂ (𝟙 d)).hom ≫ φ) ≫
        g ◁ (λ_ r₂).inv :
      r₁ ≫ f ⟶ g ≫ 𝟙 d ≫ r₂)
have simp : r₁ ◁
      (((ρ_ f).inv ≫
          f ◁
              (adj₂.comp
                  { unit := Iso.inv (ρ_ (𝟙 d)), counit := Iso.hom (ρ_ (𝟙 d)), left_triangle := sorry, right_triangle := sorry :
                    Adjunction.{w, v, u} (𝟙 d) (𝟙 d) }).unit ≫
            (α_ f (l₂ ≫ 𝟙 d) (𝟙 d ≫ r₂)).inv ≫ φ ▷ (𝟙 d ≫ r₂)) ≫
        (α_ l₁ g (𝟙 d ≫ r₂)).hom) ≫
    (α_ r₁ l₁ (g ≫ 𝟙 d ≫ r₂)).inv ≫ adj₁.counit ▷ (g ≫ 𝟙 d ≫ r₂) ≫ (λ_ (g ≫ 𝟙 d ≫ r₂)).hom =
  (r₁ ◁
        (((ρ_ f).inv ≫ f ◁ adj₂.unit ≫ (α_ f l₂ r₂).inv ≫ ((ρ_ (f ≫ l₂)).inv ≫ (α_ f l₂ (𝟙 d)).hom ≫ φ) ▷ r₂) ≫
          (α_ l₁ g r₂).hom) ≫
      (α_ r₁ l₁ (g ≫ r₂)).inv ≫ adj₁.counit ▷ (g ≫ r₂) ≫ (λ_ (g ≫ r₂)).hom) ≫
    g ◁ (λ_ r₂).inv
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 ≫ l₂ ≫ 𝟙 d ⟶ l₁ ≫ g
⊢ r₁ ◁
        (((ρ_ f).inv ≫
            f ◁
                (adj₂.comp
                    { unit := Iso.inv (ρ_ (𝟙 d)), counit := Iso.hom (ρ_ (𝟙 d)), left_triangle := ⋯,
                      right_triangle := ⋯ : Adjunction.{w, v, u} (𝟙 d) (𝟙 d) }).unit ≫
              (α_ f (l₂ ≫ 𝟙 d) (𝟙 d ≫ r₂)).inv ≫ φ ▷ (𝟙 d ≫ r₂)) ≫
          (α_ l₁ g (𝟙 d ≫ r₂)).hom) ≫
      (α_ r₁ l₁ (g ≫ 𝟙 d ≫ r₂)).inv ≫ adj₁.counit ▷ (g ≫ 𝟙 d ≫ r₂) ≫ (λ_ (g ≫ 𝟙 d ≫ r₂)).hom =
    (r₁ ◁
          (((ρ_ f).inv ≫ f ◁ adj₂.unit ≫ (α_ f l₂ r₂).inv ≫ ((ρ_ (f ≫ l₂)).inv ≫ (α_ f l₂ (𝟙 d)).hom ≫ φ) ▷ r₂) ≫
            (α_ l₁ g r₂).hom) ≫
        (α_ r₁ l₁ (g ≫ r₂)).inv ≫ adj₁.counit ▷ (g ≫ r₂) ≫ (λ_ (g ≫ r₂)).hom) ≫
      g ◁ (λ_ r₂).inv
have dsimp : r₁ ◁
      (((ρ_ f).inv ≫
          f ◁
              bicategoricalComp (h := l₂ ≫ 𝟙 d ≫ r₂) adj₂.unit
                (l₂ ◁ Iso.inv (ρ_ (𝟙 d)) ▷ r₂ ⊗≫ 𝟙 ((l₂ ≫ 𝟙 d) ≫ 𝟙 d ≫ r₂)) ≫
            (α_ f (l₂ ≫ 𝟙 d) (𝟙 d ≫ r₂)).inv ≫ φ ▷ (𝟙 d ≫ r₂)) ≫
        (α_ l₁ g (𝟙 d ≫ r₂)).hom) ≫
    (α_ r₁ l₁ (g ≫ 𝟙 d ≫ r₂)).inv ≫ adj₁.counit ▷ (g ≫ 𝟙 d ≫ r₂) ≫ (λ_ (g ≫ 𝟙 d ≫ r₂)).hom =
  (r₁ ◁
        (((ρ_ f).inv ≫ f ◁ adj₂.unit ≫ (α_ f l₂ r₂).inv ≫ ((ρ_ (f ≫ l₂)).inv ≫ (α_ f l₂ (𝟙 d)).hom ≫ φ) ▷ r₂) ≫
          (α_ l₁ g r₂).hom) ≫
      (α_ r₁ l₁ (g ≫ r₂)).inv ≫ adj₁.counit ▷ (g ≫ r₂) ≫ (λ_ (g ≫ r₂)).hom) ≫
    g ◁ (λ_ r₂).inv
Tactic: dsimp
-- 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 ⟶ c
g₂ : c ⟶ e
h₁ : b ⟶ d
h₂ : d ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : e ⟶ f
r₃ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g₁ ≫ l₂ ⟶ l₁ ≫ h₁
β : g₂ ≫ l₃ ⟶ l₂ ≫ h₂
⊢ Eq (α := r₁ ≫ g₁ ≫ g₂ ⟶ (h₁ ≫ h₂) ≫ r₃)
    ((mateEquiv adj₁ adj₃ : (a_1 : (g₁ ≫ g₂) ≫ l₃ ⟶ l₁ ≫ h₁ ≫ h₂) → r₁ ≫ g₁ ≫ g₂ ⟶ (h₁ ≫ h₂) ≫ r₃)
        (leftAdjointSquare.vcomp α β) :
      r₁ ≫ g₁ ≫ g₂ ⟶ (h₁ ≫ h₂) ≫ r₃)
    (rightAdjointSquare.vcomp (r₂ := r₂) ((mateEquiv adj₁ adj₂ : (a_1 : g₁ ≫ l₂ ⟶ l₁ ≫ h₁) → r₁ ≫ g₁ ⟶ h₁ ≫ r₂) α)
        ((mateEquiv adj₂ adj₃ : (a : g₂ ≫ l₃ ⟶ l₂ ≫ h₂) → r₂ ≫ g₂ ⟶ h₂ ≫ r₃) β) :
      r₁ ≫ g₁ ≫ g₂ ⟶ (h₁ ≫ h₂) ≫ r₃)
have simp : 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
    r₁ ◁ (g₁ ≫ g₂) ◁ adj₃.unit ⊗≫
      r₁ ◁ ((α_ g₁ g₂ l₃).hom ≫ g₁ ◁ β ≫ (α_ g₁ l₂ h₂).inv ≫ α ▷ h₂ ≫ (α_ l₁ h₁ h₂).hom) ▷ r₃ ⊗≫
        adj₁.counit ▷ (h₁ ≫ h₂) ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
  (α_ r₁ g₁ g₂).inv ≫
    (𝟙 (r₁ ≫ g₁) ⊗≫ r₁ ◁ g₁ ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h₁ ▷ r₂ ⊗≫ 𝟙 (h₁ ≫ r₂)) ▷ g₂ ≫
      (α_ h₁ r₂ g₂).hom ≫
        h₁ ◁ (𝟙 (r₂ ≫ g₂) ⊗≫ r₂ ◁ g₂ ◁ adj₃.unit ⊗≫ r₂ ◁ β ▷ r₃ ⊗≫ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 (h₂ ≫ r₃)) ≫
          (α_ h₁ h₂ r₃).inv
Tactic: simp only [leftAdjointSquare.vcomp, mateEquiv_apply', rightAdjointSquare.vcomp]
-- 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 ⟶ c
g₂ : c ⟶ e
h₁ : b ⟶ d
h₂ : d ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : e ⟶ f
r₃ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g₁ ≫ l₂ ⟶ l₁ ≫ h₁
β : g₂ ≫ l₃ ⟶ l₂ ≫ h₂
⊢ 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ (g₁ ≫ g₂) ◁ adj₃.unit ⊗≫
        r₁ ◁ ((α_ g₁ g₂ l₃).hom ≫ g₁ ◁ β ≫ (α_ g₁ l₂ h₂).inv ≫ α ▷ h₂ ≫ (α_ l₁ h₁ h₂).hom) ▷ r₃ ⊗≫
          adj₁.counit ▷ (h₁ ≫ h₂) ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    (α_ r₁ g₁ g₂).inv ≫
      (𝟙 (r₁ ≫ g₁) ⊗≫ r₁ ◁ g₁ ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h₁ ▷ r₂ ⊗≫ 𝟙 (h₁ ≫ r₂)) ▷ g₂ ≫
        (α_ h₁ r₂ g₂).hom ≫
          h₁ ◁ (𝟙 (r₂ ≫ g₂) ⊗≫ r₂ ◁ g₂ ◁ adj₃.unit ⊗≫ r₂ ◁ β ▷ r₃ ⊗≫ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 (h₂ ≫ r₃)) ≫
            (α_ h₁ h₂ r₃).inv
have symm : (α_ r₁ g₁ g₂).inv ≫
    (𝟙 (r₁ ≫ g₁) ⊗≫ r₁ ◁ g₁ ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h₁ ▷ r₂ ⊗≫ 𝟙 (h₁ ≫ r₂)) ▷ g₂ ≫
      (α_ h₁ r₂ g₂).hom ≫
        h₁ ◁ (𝟙 (r₂ ≫ g₂) ⊗≫ r₂ ◁ g₂ ◁ adj₃.unit ⊗≫ r₂ ◁ β ▷ r₃ ⊗≫ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 (h₂ ≫ r₃)) ≫
          (α_ h₁ h₂ r₃).inv =
  𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
    r₁ ◁ (g₁ ≫ g₂) ◁ adj₃.unit ⊗≫
      r₁ ◁ ((α_ g₁ g₂ l₃).hom ≫ g₁ ◁ β ≫ (α_ g₁ l₂ h₂).inv ≫ α ▷ h₂ ≫ (α_ l₁ h₁ h₂).hom) ▷ r₃ ⊗≫
        adj₁.counit ▷ (h₁ ≫ h₂) ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)
Tactic: symm
-- 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 ⟶ c
g₂ : c ⟶ e
h₁ : b ⟶ d
h₂ : d ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : e ⟶ f
r₃ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g₁ ≫ l₂ ⟶ l₁ ≫ h₁
β : g₂ ≫ l₃ ⟶ l₂ ≫ h₂
⊢ 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ adj₂.unit ▷ g₂ ⊗≫
        r₁ ◁ α ▷ r₂ ▷ g₂ ⊗≫
          (adj₁.counit ▷ (h₁ ≫ r₂ ≫ g₂ ≫ 𝟙 e) ≫ 𝟙 b ◁ h₁ ◁ r₂ ◁ g₂ ◁ adj₃.unit) ⊗≫
            h₁ ◁ r₂ ◁ β ▷ r₃ ⊗≫ h₁ ◁ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ adj₂.unit ▷ g₂ ⊗≫
        r₁ ◁ (α ▷ (r₂ ≫ g₂ ≫ 𝟙 e) ≫ (l₁ ≫ h₁) ◁ r₂ ◁ g₂ ◁ adj₃.unit) ⊗≫
          (adj₁.counit ▷ (h₁ ≫ r₂) ▷ (g₂ ≫ l₃) ≫ (𝟙 b ≫ h₁ ≫ r₂) ◁ β) ▷ r₃ ⊗≫
            h₁ ◁ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)
have rw : 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
    r₁ ◁ g₁ ◁ adj₂.unit ▷ g₂ ⊗≫
      r₁ ◁ α ▷ r₂ ▷ g₂ ⊗≫
        ((r₁ ≫ l₁) ◁ h₁ ◁ r₂ ◁ g₂ ◁ adj₃.unit ≫ adj₁.counit ▷ (h₁ ≫ r₂ ≫ g₂ ≫ l₃ ≫ r₃)) ⊗≫
          h₁ ◁ r₂ ◁ β ▷ r₃ ⊗≫ h₁ ◁ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
  𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
    r₁ ◁ g₁ ◁ adj₂.unit ▷ g₂ ⊗≫
      r₁ ◁ (α ▷ (r₂ ≫ g₂ ≫ 𝟙 e) ≫ (l₁ ≫ h₁) ◁ r₂ ◁ g₂ ◁ adj₃.unit) ⊗≫
        (adj₁.counit ▷ (h₁ ≫ r₂) ▷ (g₂ ≫ l₃) ≫ (𝟙 b ≫ h₁ ≫ r₂) ◁ β) ▷ r₃ ⊗≫
          h₁ ◁ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ 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 e f : B
g₁ : a ⟶ c
g₂ : c ⟶ e
h₁ : b ⟶ d
h₂ : d ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : e ⟶ f
r₃ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g₁ ≫ l₂ ⟶ l₁ ≫ h₁
β : g₂ ≫ l₃ ⟶ l₂ ≫ h₂
⊢ 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ adj₂.unit ▷ g₂ ⊗≫
        r₁ ◁ (α ▷ (r₂ ≫ g₂ ≫ 𝟙 e) ≫ (l₁ ≫ h₁) ◁ r₂ ◁ g₂ ◁ adj₃.unit) ⊗≫
          (adj₁.counit ▷ (h₁ ≫ r₂) ▷ (g₂ ≫ l₃) ≫ (𝟙 b ≫ h₁ ≫ r₂) ◁ β) ▷ r₃ ⊗≫
            h₁ ◁ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ (adj₂.unit ▷ (g₂ ≫ 𝟙 e) ≫ (l₂ ≫ r₂) ◁ g₂ ◁ adj₃.unit) ⊗≫
        r₁ ◁ (α ▷ (r₂ ≫ g₂ ≫ l₃) ≫ (l₁ ≫ h₁) ◁ r₂ ◁ β) ▷ r₃ ⊗≫
          (adj₁.counit ▷ h₁ ▷ (r₂ ≫ l₂) ≫ (𝟙 b ≫ h₁) ◁ adj₂.counit) ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)
have rw : 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
    r₁ ◁ g₁ ◁ adj₂.unit ▷ g₂ ⊗≫
      r₁ ◁ ((g₁ ≫ l₂) ◁ r₂ ◁ g₂ ◁ adj₃.unit ≫ α ▷ (r₂ ≫ g₂ ≫ l₃ ≫ r₃)) ⊗≫
        (((r₁ ≫ l₁) ≫ h₁ ≫ r₂) ◁ β ≫ adj₁.counit ▷ (h₁ ≫ r₂) ▷ (l₂ ≫ h₂)) ▷ r₃ ⊗≫
          h₁ ◁ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
  𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
    r₁ ◁ g₁ ◁ (adj₂.unit ▷ (g₂ ≫ 𝟙 e) ≫ (l₂ ≫ r₂) ◁ g₂ ◁ adj₃.unit) ⊗≫
      r₁ ◁ (α ▷ (r₂ ≫ g₂ ≫ l₃) ≫ (l₁ ≫ h₁) ◁ r₂ ◁ β) ▷ r₃ ⊗≫
        (adj₁.counit ▷ h₁ ▷ (r₂ ≫ l₂) ≫ (𝟙 b ≫ h₁) ◁ adj₂.counit) ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)
Tactic: rw [← whisker_exchange, ← 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 : B
g₁ : a ⟶ c
g₂ : c ⟶ e
h₁ : b ⟶ d
h₂ : d ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : e ⟶ f
r₃ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g₁ ≫ l₂ ⟶ l₁ ≫ h₁
β : g₂ ≫ l₃ ⟶ l₂ ≫ h₂
⊢ 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ (adj₂.unit ▷ (g₂ ≫ 𝟙 e) ≫ (l₂ ≫ r₂) ◁ g₂ ◁ adj₃.unit) ⊗≫
        r₁ ◁ (α ▷ (r₂ ≫ g₂ ≫ l₃) ≫ (l₁ ≫ h₁) ◁ r₂ ◁ β) ▷ r₃ ⊗≫
          (adj₁.counit ▷ h₁ ▷ (r₂ ≫ l₂) ≫ (𝟙 b ≫ h₁) ◁ adj₂.counit) ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ g₂ ◁ adj₃.unit ⊗≫
        r₁ ◁ g₁ ◁ (adj₂.unit ▷ (g₂ ≫ l₃) ≫ (l₂ ≫ r₂) ◁ β) ▷ r₃ ⊗≫
          r₁ ◁ (α ▷ (r₂ ≫ l₂) ≫ (l₁ ≫ h₁) ◁ adj₂.counit) ▷ h₂ ▷ r₃ ⊗≫ adj₁.counit ▷ h₁ ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)
have rw : 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
    r₁ ◁ g₁ ◁ (𝟙 c ◁ g₂ ◁ adj₃.unit ≫ adj₂.unit ▷ (g₂ ≫ l₃ ≫ r₃)) ⊗≫
      r₁ ◁ ((g₁ ≫ l₂) ◁ r₂ ◁ β ≫ α ▷ (r₂ ≫ l₂ ≫ h₂)) ▷ r₃ ⊗≫
        (((r₁ ≫ l₁) ≫ h₁) ◁ adj₂.counit ≫ adj₁.counit ▷ h₁ ▷ 𝟙 d) ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
  𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
    r₁ ◁ g₁ ◁ g₂ ◁ adj₃.unit ⊗≫
      r₁ ◁ g₁ ◁ (adj₂.unit ▷ (g₂ ≫ l₃) ≫ (l₂ ≫ r₂) ◁ β) ▷ r₃ ⊗≫
        r₁ ◁ (α ▷ (r₂ ≫ l₂) ≫ (l₁ ≫ h₁) ◁ adj₂.counit) ▷ h₂ ▷ r₃ ⊗≫ adj₁.counit ▷ h₁ ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)
Tactic: rw [← whisker_exchange, ← whisker_exchange, ← 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 : B
g₁ : a ⟶ c
g₂ : c ⟶ e
h₁ : b ⟶ d
h₂ : d ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : e ⟶ f
r₃ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g₁ ≫ l₂ ⟶ l₁ ≫ h₁
β : g₂ ≫ l₃ ⟶ l₂ ≫ h₂
⊢ 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ g₂ ◁ adj₃.unit ⊗≫
        r₁ ◁ g₁ ◁ (adj₂.unit ▷ (g₂ ≫ l₃) ≫ (l₂ ≫ r₂) ◁ β) ▷ r₃ ⊗≫
          r₁ ◁ (α ▷ (r₂ ≫ l₂) ≫ (l₁ ≫ h₁) ◁ adj₂.counit) ▷ h₂ ▷ r₃ ⊗≫ adj₁.counit ▷ h₁ ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ g₂ ◁ adj₃.unit ⊗≫
        r₁ ◁ g₁ ◁ β ▷ r₃ ⊗≫
          (r₁ ≫ g₁) ◁ leftZigzag adj₂.unit adj₂.counit ▷ (h₂ ≫ r₃) ⊗≫
            r₁ ◁ α ▷ h₂ ▷ r₃ ⊗≫ adj₁.counit ▷ h₁ ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)
have rw : 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
    r₁ ◁ g₁ ◁ g₂ ◁ adj₃.unit ⊗≫
      r₁ ◁ g₁ ◁ (𝟙 c ◁ β ≫ adj₂.unit ▷ (l₂ ≫ h₂)) ▷ r₃ ⊗≫
        r₁ ◁ ((g₁ ≫ l₂) ◁ adj₂.counit ≫ α ▷ 𝟙 d) ▷ h₂ ▷ r₃ ⊗≫ adj₁.counit ▷ h₁ ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
  𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
    r₁ ◁ g₁ ◁ g₂ ◁ adj₃.unit ⊗≫
      r₁ ◁ g₁ ◁ β ▷ r₃ ⊗≫
        (r₁ ≫ g₁) ◁ leftZigzag adj₂.unit adj₂.counit ▷ (h₂ ≫ r₃) ⊗≫
          r₁ ◁ α ▷ h₂ ▷ r₃ ⊗≫ adj₁.counit ▷ h₁ ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)
Tactic: rw [← whisker_exchange, ← 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 : B
g₁ : a ⟶ c
g₂ : c ⟶ e
h₁ : b ⟶ d
h₂ : d ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : e ⟶ f
r₃ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g₁ ≫ l₂ ⟶ l₁ ≫ h₁
β : g₂ ≫ l₃ ⟶ l₂ ≫ h₂
⊢ 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ g₂ ◁ adj₃.unit ⊗≫
        r₁ ◁ g₁ ◁ β ▷ r₃ ⊗≫
          (r₁ ≫ g₁) ◁ leftZigzag adj₂.unit adj₂.counit ▷ (h₂ ≫ r₃) ⊗≫
            r₁ ◁ α ▷ h₂ ▷ r₃ ⊗≫ adj₁.counit ▷ h₁ ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ (g₁ ≫ g₂) ◁ adj₃.unit ⊗≫
        r₁ ◁ ((α_ g₁ g₂ l₃).hom ≫ g₁ ◁ β ≫ (α_ g₁ l₂ h₂).inv ≫ α ▷ h₂ ≫ (α_ l₁ h₁ h₂).hom) ▷ r₃ ⊗≫
          adj₁.counit ▷ (h₁ ≫ h₂) ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)
have rw : 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
    r₁ ◁ g₁ ◁ g₂ ◁ adj₃.unit ⊗≫
      r₁ ◁ g₁ ◁ β ▷ r₃ ⊗≫
        (r₁ ≫ g₁) ◁ ((λ_ l₂).hom ≫ (ρ_ l₂).inv) ▷ (h₂ ≫ r₃) ⊗≫
          r₁ ◁ α ▷ h₂ ▷ r₃ ⊗≫ adj₁.counit ▷ h₁ ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
  𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
    r₁ ◁ (g₁ ≫ g₂) ◁ adj₃.unit ⊗≫
      r₁ ◁ ((α_ g₁ g₂ l₃).hom ≫ g₁ ◁ β ≫ (α_ g₁ l₂ h₂).inv ≫ α ▷ h₂ ≫ (α_ l₁ h₁ h₂).hom) ▷ r₃ ⊗≫
        adj₁.counit ▷ (h₁ ≫ h₂) ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)
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 e f : B
g₁ : a ⟶ c
g₂ : c ⟶ e
h₁ : b ⟶ d
h₂ : d ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : e ⟶ f
r₃ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g₁ ≫ l₂ ⟶ l₁ ≫ h₁
β : g₂ ≫ l₃ ⟶ l₂ ≫ h₂
⊢ (α_ r₁ g₁ g₂).inv ≫
      (𝟙 (r₁ ≫ g₁) ⊗≫ r₁ ◁ g₁ ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h₁ ▷ r₂ ⊗≫ 𝟙 (h₁ ≫ r₂)) ▷ g₂ ≫
        (α_ h₁ r₂ g₂).hom ≫
          h₁ ◁ (𝟙 (r₂ ≫ g₂) ⊗≫ r₂ ◁ g₂ ◁ adj₃.unit ⊗≫ r₂ ◁ β ▷ r₃ ⊗≫ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 (h₂ ≫ r₃)) ≫
            (α_ h₁ h₂ r₃).inv =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ (g₁ ≫ g₂) ◁ adj₃.unit ⊗≫
        r₁ ◁ ((α_ g₁ g₂ l₃).hom ≫ g₁ ◁ β ≫ (α_ g₁ l₂ h₂).inv ≫ α ▷ h₂ ≫ (α_ l₁ h₁ h₂).hom) ▷ r₃ ⊗≫
          adj₁.counit ▷ (h₁ ≫ h₂) ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)
have _ : (α_ r₁ g₁ g₂).inv ≫
    (𝟙 (r₁ ≫ g₁) ⊗≫ r₁ ◁ g₁ ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h₁ ▷ r₂ ⊗≫ 𝟙 (h₁ ≫ r₂)) ▷ g₂ ≫
      (α_ h₁ r₂ g₂).hom ≫
        h₁ ◁ (𝟙 (r₂ ≫ g₂) ⊗≫ r₂ ◁ g₂ ◁ adj₃.unit ⊗≫ r₂ ◁ β ▷ r₃ ⊗≫ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 (h₂ ≫ r₃)) ≫
          (α_ h₁ h₂ r₃).inv =
  𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
    r₁ ◁ g₁ ◁ adj₂.unit ▷ g₂ ⊗≫
      r₁ ◁ α ▷ r₂ ▷ g₂ ⊗≫
        (adj₁.counit ▷ (h₁ ≫ r₂ ≫ g₂ ≫ 𝟙 e) ≫ 𝟙 b ◁ h₁ ◁ r₂ ◁ g₂ ◁ adj₃.unit) ⊗≫
          h₁ ◁ r₂ ◁ β ▷ r₃ ⊗≫ h₁ ◁ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)
Tactic: calc
    _ = 𝟙 _ ⊗≫ r₁ ◁ g₁ ◁ adj₂.unit ▷ g₂ ⊗≫ r₁ ◁ α ▷ r₂ ▷ g₂ ⊗≫
          ((adj₁.counit ▷ (h₁ ≫ r₂ ≫ g₂ ≫ 𝟙 e)) ≫ 𝟙 b ◁ (h₁ ◁ r₂ ◁ g₂ ◁ adj₃.unit)) ⊗≫
            h₁ ◁ r₂ ◁ β ▷ r₃ ⊗≫ h₁ ◁ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 _ ⊗≫ r₁ ◁ g₁ ◁ adj₂.unit ▷ g₂ ⊗≫
          (r₁ ◁ (α ▷ (r₂ ≫ g₂ ≫ 𝟙 e) ≫ (l₁ ≫ h₁) ◁ r₂ ◁ g₂ ◁ adj₃.unit)) ⊗≫
            ((adj₁.counit ▷ (h₁ ≫ r₂) ▷ (g₂ ≫ l₃) ≫ (𝟙 b ≫ h₁ ≫ r₂) ◁ β) ▷ r₃) ⊗≫
              h₁ ◁ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 _ := by
      rw [← whisker_exchange]
      bicategory
    _ = 𝟙 _ ⊗≫ r₁ ◁ g₁ ◁ (adj₂.unit ▷ (g₂ ≫ 𝟙 e) ≫ (l₂ ≫ r₂) ◁ g₂ ◁ adj₃.unit) ⊗≫
          (r₁ ◁ (α ▷ (r₂ ≫ g₂ ≫ l₃) ≫ (l₁ ≫ h₁) ◁ r₂ ◁ β) ▷ r₃) ⊗≫
            (adj₁.counit ▷ h₁ ▷ (r₂ ≫ l₂) ≫ (𝟙 b ≫ h₁) ◁ adj₂.counit) ▷ h₂ ▷ r₃ ⊗≫ 𝟙 _ := by
      rw [← whisker_exchange, ← whisker_exchange]
      bicategory
    _ = 𝟙 _ ⊗≫ r₁ ◁ g₁ ◁ g₂ ◁ adj₃.unit ⊗≫
          r₁ ◁ g₁ ◁ (adj₂.unit ▷ (g₂ ≫ l₃) ≫ (l₂ ≫ r₂) ◁ β) ▷ r₃ ⊗≫
            r₁ ◁ (α ▷ (r₂ ≫ l₂) ≫ (l₁ ≫ h₁) ◁ adj₂.counit) ▷ h₂ ▷ r₃ ⊗≫
              adj₁.counit ▷ h₁ ▷ h₂ ▷ r₃ ⊗≫ 𝟙 _ := by
      rw [← whisker_exchange, ← whisker_exchange, ← whisker_exchange]
      bicategory
    _ = 𝟙 _ ⊗≫ r₁ ◁ g₁ ◁ g₂ ◁ adj₃.unit ⊗≫ r₁ ◁ g₁ ◁ β ▷ r₃ ⊗≫
          ((r₁ ≫ g₁) ◁ leftZigzag adj₂.unit adj₂.counit ▷ (h₂ ≫ r₃)) ⊗≫
            r₁ ◁ α ▷ h₂ ▷ r₃ ⊗≫ adj₁.counit ▷ h₁ ▷ h₂ ▷ r₃ ⊗≫ 𝟙 _ := by
      rw [← whisker_exchange, ← whisker_exchange]
      bicategory
    _ = _ := by
      rw [adj₂.left_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 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
⊢ 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₂)
have simp : 𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
    (r₃ ≫ r₁) ◁ g ◁ (adj₂.comp adj₄).unit ⊗≫
      (r₃ ≫ r₁) ◁ leftAdjointSquare.hcomp α β ▷ (r₄ ≫ r₂) ⊗≫
        (adj₁.comp adj₃).counit ▷ k ▷ (r₄ ≫ r₂) ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂) =
  rightAdjointSquare.hcomp (𝟙 (r₁ ≫ g) ⊗≫ r₁ ◁ g ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h ▷ r₂ ⊗≫ 𝟙 (h ≫ r₂))
    (𝟙 (r₃ ≫ h) ⊗≫ r₃ ◁ h ◁ adj₄.unit ⊗≫ r₃ ◁ β ▷ r₄ ⊗≫ adj₃.counit ▷ k ▷ r₄ ⊗≫ 𝟙 (k ≫ r₄))
Tactic: simp only [mateEquiv_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 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₂.comp adj₄).unit ⊗≫
        (r₃ ≫ r₁) ◁ leftAdjointSquare.hcomp α β ▷ (r₄ ≫ r₂) ⊗≫
          (adj₁.comp adj₃).counit ▷ k ▷ (r₄ ≫ r₂) ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂) =
    rightAdjointSquare.hcomp (𝟙 (r₁ ≫ g) ⊗≫ r₁ ◁ g ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h ▷ r₂ ⊗≫ 𝟙 (h ≫ r₂))
      (𝟙 (r₃ ≫ h) ⊗≫ r₃ ◁ h ◁ adj₄.unit ⊗≫ r₃ ◁ β ▷ r₄ ⊗≫ adj₃.counit ▷ k ▷ r₄ ⊗≫ 𝟙 (k ≫ r₄))
have dsimp : 𝟙 ((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
Tactic: dsimp [leftAdjointSquare.hcomp, rightAdjointSquare.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 : 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 ⊗≫
        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₂)
have rw : 𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
    r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
      r₃ ◁ r₁ ◁ (α ▷ 𝟙 e ≫ (l₁ ≫ h) ◁ adj₄.unit) ▷ r₂ ⊗≫
        r₃ ◁ (adj₁.counit ▷ (h ≫ l₄) ≫ 𝟙 b ◁ β) ▷ 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: rw [whisker_exchange, 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 : 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 ⊗≫
        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
have rw : 𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
    r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
      r₃ ◁ r₁ ◁ α ▷ r₂ ⊗≫
        r₃ ◁ (adj₁.counit ▷ (h ≫ 𝟙 e) ≫ 𝟙 b ◁ h ◁ adj₄.unit) ▷ 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: 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 : 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).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 ⊗≫ 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₂)
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