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
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₂
⊢ ((ρ_ 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 =
    bicategoricalComp (h := r₁ ≫ 𝟙 c ≫ 𝟙 c) (𝟙 r₁)
      (bicategoricalComp (g := (𝟙 d ≫ 𝟙 d) ≫ r₃)
        (rightAdjointSquare.vcomp (r₂ := r₂)
          ((mateEquiv adj₁ adj₂ : (a : 𝟙 c ≫ l₂ ⟶ l₁ ≫ 𝟙 d) → r₁ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv))
          ((mateEquiv adj₂ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₂ ≫ 𝟙 d) → r₂ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)))
        (𝟙 r₃))
have dsimp : ((ρ_ 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₁ ⊗≫
    bicategoricalComp (g := (𝟙 d ≫ 𝟙 d) ≫ r₃)
      ((α_ r₁ (𝟙 c) (𝟙 c)).inv ≫
        (mateEquiv adj₁ adj₂ : (a : 𝟙 c ≫ l₂ ⟶ l₁ ≫ 𝟙 d) → r₁ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ▷ 𝟙 c ≫
          Iso.hom (α_ (𝟙 d) r₂ (𝟙 c)) ≫
            𝟙 d ◁
                (mateEquiv adj₂ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₂ ≫ 𝟙 d) → r₂ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃)
                  ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫
              Iso.inv (α_ (𝟙 d) (𝟙 d) r₃))
      (𝟙 r₃)
Tactic: dsimp only [rightAdjointSquare.vcomp]
-- 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₂
⊢ bicategoricalComp (h := r₁ ≫ 𝟙 c ≫ 𝟙 c) (𝟙 r₁)
      (bicategoricalComp (g := (𝟙 d ≫ 𝟙 d) ≫ r₃)
        (rightAdjointSquare.vcomp (r₂ := r₂)
          ((mateEquiv adj₁ adj₂ : (a : 𝟙 c ≫ l₂ ⟶ l₁ ≫ 𝟙 d) → r₁ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv))
          ((mateEquiv adj₂ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₂ ≫ 𝟙 d) → r₂ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)))
        (𝟙 r₃)) =
    (ρ_ r₁).inv ≫
      (mateEquiv adj₁ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₁ ≫ 𝟙 d) → r₁ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ (β ≫ α) ≫ (ρ_ l₁).inv) ≫
        (λ_ r₃).hom
have rw : bicategoricalComp (h := r₁ ≫ 𝟙 c ≫ 𝟙 c) (𝟙 r₁)
    (bicategoricalComp (g := (𝟙 d ≫ 𝟙 d) ≫ r₃)
      ((mateEquiv adj₁ adj₃ : (a : (𝟙 c ≫ 𝟙 c) ≫ l₃ ⟶ l₁ ≫ 𝟙 d ≫ 𝟙 d) → r₁ ≫ 𝟙 c ≫ 𝟙 c ⟶ (𝟙 d ≫ 𝟙 d) ≫ r₃)
        (leftAdjointSquare.vcomp ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)))
      (𝟙 r₃)) =
  (ρ_ r₁).inv ≫
    (mateEquiv adj₁ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₁ ≫ 𝟙 d) → r₁ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ (β ≫ α) ≫ (ρ_ l₁).inv) ≫
      (λ_ r₃).hom
Tactic: rw [← mateEquiv_vcomp]
-- 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₂
⊢ bicategoricalComp (h := r₁ ≫ 𝟙 c ≫ 𝟙 c) (𝟙 r₁)
      (bicategoricalComp (g := (𝟙 d ≫ 𝟙 d) ≫ r₃)
        ((mateEquiv adj₁ adj₃ : (a : (𝟙 c ≫ 𝟙 c) ≫ l₃ ⟶ l₁ ≫ 𝟙 d ≫ 𝟙 d) → r₁ ≫ 𝟙 c ≫ 𝟙 c ⟶ (𝟙 d ≫ 𝟙 d) ≫ r₃)
          (leftAdjointSquare.vcomp ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)))
        (𝟙 r₃)) =
    (ρ_ r₁).inv ≫
      (mateEquiv adj₁ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₁ ≫ 𝟙 d) → r₁ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ (β ≫ α) ≫ (ρ_ l₁).inv) ≫
        (λ_ r₃).hom
have simp : 𝟙 r₁ ⊗≫
    bicategoricalComp (h := r₁ ≫ (𝟙 c ≫ 𝟙 c) ≫ 𝟙 c) (𝟙 (r₁ ≫ 𝟙 c ≫ 𝟙 c))
        (bicategoricalComp (h := r₁ ≫ ((𝟙 c ≫ 𝟙 c) ≫ l₃) ≫ r₃) (r₁ ◁ (𝟙 c ≫ 𝟙 c) ◁ adj₃.unit)
          (r₁ ◁
              (Iso.hom (α_ (𝟙 c) (𝟙 c) l₃) ≫
                  𝟙 c ◁ ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫
                    Iso.inv (α_ (𝟙 c) l₂ (𝟙 d)) ≫ ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ▷ 𝟙 d ≫ (α_ l₁ (𝟙 d) (𝟙 d)).hom) ▷
                r₃ ⊗≫
            adj₁.counit ▷ (𝟙 d ≫ 𝟙 d) ▷ r₃ ⊗≫ 𝟙 ((𝟙 d ≫ 𝟙 d) ≫ r₃))) ⊗≫
      𝟙 r₃ =
  (ρ_ 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
Tactic: simp only [leftAdjointSquare.vcomp, 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₂ l₃ : c ⟶ d
r₁ r₂ r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : l₃ ⟶ l₂
⊢ 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)
have _ : ((ρ_ 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 =
  bicategoricalComp (h := r₁ ≫ 𝟙 c ≫ 𝟙 c) (𝟙 r₁)
    (bicategoricalComp (g := (𝟙 d ≫ 𝟙 d) ≫ r₃)
      (rightAdjointSquare.vcomp (r₂ := r₂)
        ((mateEquiv adj₁ adj₂ : (a : 𝟙 c ≫ l₂ ⟶ l₁ ≫ 𝟙 d) → r₁ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv))
        ((mateEquiv adj₂ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₂ ≫ 𝟙 d) → r₂ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)))
      (𝟙 r₃))
Tactic: calc
    _ = 𝟙 r₁ ⊗≫
          rightAdjointSquare.vcomp
            (mateEquiv adj₁ adj₂ ((λ_ _).hom ≫ α ≫ (ρ_ _).inv))
            (mateEquiv adj₂ adj₃ ((λ_ _).hom ≫ β ≫ (ρ_ _).inv)) ⊗≫ 𝟙 r₃ := by
      dsimp only [rightAdjointSquare.vcomp]
      bicategory
    _ = _ := by
      rw [← mateEquiv_vcomp]
      simp only [leftAdjointSquare.vcomp, mateEquiv_apply']
      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₁ l₂ l₃ : c ⟶ d
r₁ r₂ r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : l₃ ⟶ l₂
_ :
  ((ρ_ 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 =
    bicategoricalComp (h := r₁ ≫ 𝟙 c ≫ 𝟙 c) (𝟙 r₁)
      (bicategoricalComp (g := (𝟙 d ≫ 𝟙 d) ≫ r₃)
        (rightAdjointSquare.vcomp (r₂ := r₂)
          ((mateEquiv adj₁ adj₂ : (a : 𝟙 c ≫ l₂ ⟶ l₁ ≫ 𝟙 d) → r₁ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv))
          ((mateEquiv adj₂ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₂ ≫ 𝟙 d) → r₂ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)))
        (𝟙 r₃))
⊢ 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)
have _₁ : bicategoricalComp (h := r₁ ≫ 𝟙 c ≫ 𝟙 c) (𝟙 r₁)
    (bicategoricalComp (g := (𝟙 d ≫ 𝟙 d) ≫ r₃)
      (rightAdjointSquare.vcomp (r₂ := r₂)
        ((mateEquiv adj₁ adj₂ : (a : 𝟙 c ≫ l₂ ⟶ l₁ ≫ 𝟙 d) → r₁ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv))
        ((mateEquiv adj₂ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₂ ≫ 𝟙 d) → r₂ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)))
      (𝟙 r₃)) =
  (ρ_ r₁).inv ≫
    (mateEquiv adj₁ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₁ ≫ 𝟙 d) → r₁ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ (β ≫ α) ≫ (ρ_ l₁).inv) ≫
      (λ_ r₃).hom
Tactic: calc
    _ = 𝟙 r₁ ⊗≫
          rightAdjointSquare.vcomp
            (mateEquiv adj₁ adj₂ ((λ_ _).hom ≫ α ≫ (ρ_ _).inv))
            (mateEquiv adj₂ adj₃ ((λ_ _).hom ≫ β ≫ (ρ_ _).inv)) ⊗≫ 𝟙 r₃ := by
      dsimp only [rightAdjointSquare.vcomp]
      bicategory
    _ = _ := by
      rw [← mateEquiv_vcomp]
      simp only [leftAdjointSquare.vcomp, mateEquiv_apply']
      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₁ l₂ l₃ : c ⟶ d
r₁ r₂ r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : r₁ ⟶ r₂
β : r₂ ⟶ r₃
⊢ Eq (α := l₃ ⟶ l₁)
    (CategoryStruct.comp (Y := l₂) (((conjugateEquiv adj₂ adj₃).symm : (a : r₂ ⟶ r₃) → l₃ ⟶ l₂) β)
        (((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁) α) :
      l₃ ⟶ l₁)
    (((conjugateEquiv adj₁ adj₃).symm : (a : r₁ ⟶ r₃) → l₃ ⟶ l₁) (α ≫ β) : l₃ ⟶ l₁)
have rw : CategoryStruct.comp (Y := r₂)
    ((conjugateEquiv adj₁ adj₂ : (a : l₂ ⟶ l₁) → r₁ ⟶ r₂)
      (((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁) α : l₂ ⟶ l₁))
    ((conjugateEquiv adj₂ adj₃ : (a : l₃ ⟶ l₂) → r₂ ⟶ r₃)
      (((conjugateEquiv adj₂ adj₃).symm : (a : r₂ ⟶ r₃) → l₃ ⟶ l₂) β : l₃ ⟶ l₂)) =
  α ≫ β
Tactic: rw [Equiv.eq_symm_apply, ← conjugateEquiv_comp _ 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₁
β : 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₁)
    (𝟙 r₁ : r₁ ⟶ r₁)
have rw : Eq (α := r₁ ⟶ r₁) ((conjugateEquiv adj₁ adj₁ : (a : l₁ ⟶ l₁) → r₁ ⟶ r₁) (β ≫ α) : r₁ ⟶ r₁) (𝟙 r₁ : r₁ ⟶ r₁)
Tactic: rw [conjugateEquiv_comp, βα, 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₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : l₂ ⟶ l₁
β : l₁ ⟶ l₂
βα : β ≫ α = 𝟙 l₁
rw : Eq (α := r₁ ⟶ r₁) ((conjugateEquiv adj₁ adj₁ : (a : l₁ ⟶ l₁) → r₁ ⟶ r₁) (β ≫ α) : r₁ ⟶ r₁) (𝟙 r₁ : r₁ ⟶ r₁)
⊢ 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₁)
    (𝟙 r₁ : r₁ ⟶ r₁)
have rw₁ : Eq (α := r₁ ⟶ r₁) ((conjugateEquiv adj₁ adj₁ : (a : l₁ ⟶ l₁) → r₁ ⟶ r₁) (𝟙 l₁) : r₁ ⟶ r₁) (𝟙 r₁ : r₁ ⟶ r₁)
Tactic: rw [conjugateEquiv_comp, βα, 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₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : l₂ ⟶ l₁
β : l₁ ⟶ l₂
βα : β ≫ α = 𝟙 l₁
rw : Eq (α := r₁ ⟶ r₁) ((conjugateEquiv adj₁ adj₁ : (a : l₁ ⟶ l₁) → r₁ ⟶ r₁) (β ≫ α) : r₁ ⟶ r₁) (𝟙 r₁ : r₁ ⟶ r₁)
rw₁ : Eq (α := r₁ ⟶ r₁) ((conjugateEquiv adj₁ adj₁ : (a : l₁ ⟶ l₁) → r₁ ⟶ r₁) (𝟙 l₁) : r₁ ⟶ r₁) (𝟙 r₁ : r₁ ⟶ r₁)
⊢ 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₁)
    (𝟙 r₁ : r₁ ⟶ r₁)
have rw₂ : 𝟙 r₁ = 𝟙 r₁
Tactic: rw [conjugateEquiv_comp, βα, 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₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : r₁ ⟶ r₂
β : r₂ ⟶ r₁
αβ : α ≫ β = 𝟙 r₁
⊢ Eq (α := l₁ ⟶ l₁)
    (CategoryStruct.comp (Y := l₂) (((conjugateEquiv adj₂ adj₁).symm : (a : r₂ ⟶ r₁) → l₁ ⟶ l₂) β)
        (((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁) α) :
      l₁ ⟶ l₁)
    (𝟙 l₁ : l₁ ⟶ l₁)
have rw : Eq (α := l₁ ⟶ l₁) (((conjugateEquiv adj₁ adj₁).symm : (a : r₁ ⟶ r₁) → l₁ ⟶ l₁) (α ≫ β) : l₁ ⟶ l₁) (𝟙 l₁ : l₁ ⟶ l₁)
Tactic: rw [conjugateEquiv_symm_comp, αβ, conjugateEquiv_symm_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₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : r₁ ⟶ r₂
β : r₂ ⟶ r₁
αβ : α ≫ β = 𝟙 r₁
rw : Eq (α := l₁ ⟶ l₁) (((conjugateEquiv adj₁ adj₁).symm : (a : r₁ ⟶ r₁) → l₁ ⟶ l₁) (α ≫ β) : l₁ ⟶ l₁) (𝟙 l₁ : l₁ ⟶ l₁)
⊢ Eq (α := l₁ ⟶ l₁)
    (CategoryStruct.comp (Y := l₂) (((conjugateEquiv adj₂ adj₁).symm : (a : r₂ ⟶ r₁) → l₁ ⟶ l₂) β)
        (((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁) α) :
      l₁ ⟶ l₁)
    (𝟙 l₁ : l₁ ⟶ l₁)
have rw₁ : Eq (α := l₁ ⟶ l₁) (((conjugateEquiv adj₁ adj₁).symm : (a : r₁ ⟶ r₁) → l₁ ⟶ l₁) (𝟙 r₁) : l₁ ⟶ l₁) (𝟙 l₁ : l₁ ⟶ l₁)
Tactic: rw [conjugateEquiv_symm_comp, αβ, conjugateEquiv_symm_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₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : r₁ ⟶ r₂
β : r₂ ⟶ r₁
αβ : α ≫ β = 𝟙 r₁
rw : Eq (α := l₁ ⟶ l₁) (((conjugateEquiv adj₁ adj₁).symm : (a : r₁ ⟶ r₁) → l₁ ⟶ l₁) (α ≫ β) : l₁ ⟶ l₁) (𝟙 l₁ : l₁ ⟶ l₁)
rw₁ : Eq (α := l₁ ⟶ l₁) (((conjugateEquiv adj₁ adj₁).symm : (a : r₁ ⟶ r₁) → l₁ ⟶ l₁) (𝟙 r₁) : l₁ ⟶ l₁) (𝟙 l₁ : l₁ ⟶ l₁)
⊢ Eq (α := l₁ ⟶ l₁)
    (CategoryStruct.comp (Y := l₂) (((conjugateEquiv adj₂ adj₁).symm : (a : r₂ ⟶ r₁) → l₁ ⟶ l₂) β)
        (((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁) α) :
      l₁ ⟶ l₁)
    (𝟙 l₁ : l₁ ⟶ l₁)
have rw₂ : 𝟙 l₁ = 𝟙 l₁
Tactic: rw [conjugateEquiv_symm_comp, αβ, conjugateEquiv_symm_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₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : l₂ ⟶ l₁
inst_1 : IsIso (X := r₁) ((conjugateEquiv adj₁ adj₂ : (a : l₂ ⟶ l₁) → r₁ ⟶ r₂) α : r₁ ⟶ r₂)
⊢ IsIso α
have suffices : IsIso (C := c ⟶ d) (X := l₂) (Y := l₁)
  (((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁)
      ((conjugateEquiv adj₁ adj₂ : (a : l₂ ⟶ l₁) → r₁ ⟶ r₂) α : r₁ ⟶ r₂) :
    l₂ ⟶ l₁)
Tactic: suffices IsIso ((conjugateEquiv adj₁ adj₂).symm (conjugateEquiv adj₁ adj₂ α))
    by simpa only [Equiv.symm_apply_apply] using this
-- 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₂
inst_1 : IsIso (X := l₂) (((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁) α : l₂ ⟶ l₁)
⊢ IsIso α
have suffices : IsIso (C := d ⟶ c) (X := r₁) (Y := r₂)
  ((conjugateEquiv adj₁ adj₂ : (a : l₂ ⟶ l₁) → r₁ ⟶ r₂)
      (((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁) α : l₂ ⟶ l₁) :
    r₁ ⟶ r₂)
Tactic: suffices IsIso ((conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α))
    by simpa only [Equiv.apply_symm_apply] using this
-- 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₁
⊢ Eq (α := r₁ ⟶ r₁)
    (CategoryStruct.comp (Y := r₂) ((conjugateEquiv adj₁ adj₂ : (a : l₂ ⟶ l₁) → r₁ ⟶ r₂) α.hom)
        ((conjugateEquiv adj₂ adj₁ : (a : l₁ ⟶ l₂) → r₂ ⟶ r₁) α.inv) :
      r₁ ⟶ r₁)
    (𝟙 r₁ : r₁ ⟶ r₁)
have rw : Eq (α := r₁ ⟶ r₁) ((conjugateEquiv adj₁ adj₁ : (a : l₁ ⟶ l₁) → r₁ ⟶ r₁) (α.inv ≫ α.hom) : r₁ ⟶ r₁) (𝟙 r₁ : r₁ ⟶ r₁)
Tactic: rw [conjugateEquiv_comp, Iso.inv_hom_id, 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₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : l₂ ≅ l₁
rw : Eq (α := r₁ ⟶ r₁) ((conjugateEquiv adj₁ adj₁ : (a : l₁ ⟶ l₁) → r₁ ⟶ r₁) (α.inv ≫ α.hom) : r₁ ⟶ r₁) (𝟙 r₁ : r₁ ⟶ r₁)
⊢ Eq (α := r₁ ⟶ r₁)
    (CategoryStruct.comp (Y := r₂) ((conjugateEquiv adj₁ adj₂ : (a : l₂ ⟶ l₁) → r₁ ⟶ r₂) α.hom)
        ((conjugateEquiv adj₂ adj₁ : (a : l₁ ⟶ l₂) → r₂ ⟶ r₁) α.inv) :
      r₁ ⟶ r₁)
    (𝟙 r₁ : r₁ ⟶ r₁)
have rw₁ : Eq (α := r₁ ⟶ r₁) ((conjugateEquiv adj₁ adj₁ : (a : l₁ ⟶ l₁) → r₁ ⟶ r₁) (𝟙 l₁) : r₁ ⟶ r₁) (𝟙 r₁ : r₁ ⟶ r₁)
Tactic: rw [conjugateEquiv_comp, Iso.inv_hom_id, 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₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : l₂ ≅ l₁
rw : Eq (α := r₁ ⟶ r₁) ((conjugateEquiv adj₁ adj₁ : (a : l₁ ⟶ l₁) → r₁ ⟶ r₁) (α.inv ≫ α.hom) : r₁ ⟶ r₁) (𝟙 r₁ : r₁ ⟶ r₁)
rw₁ : Eq (α := r₁ ⟶ r₁) ((conjugateEquiv adj₁ adj₁ : (a : l₁ ⟶ l₁) → r₁ ⟶ r₁) (𝟙 l₁) : r₁ ⟶ r₁) (𝟙 r₁ : r₁ ⟶ r₁)
⊢ Eq (α := r₁ ⟶ r₁)
    (CategoryStruct.comp (Y := r₂) ((conjugateEquiv adj₁ adj₂ : (a : l₂ ⟶ l₁) → r₁ ⟶ r₂) α.hom)
        ((conjugateEquiv adj₂ adj₁ : (a : l₁ ⟶ l₂) → r₂ ⟶ r₁) α.inv) :
      r₁ ⟶ r₁)
    (𝟙 r₁ : r₁ ⟶ r₁)
have rw₂ : 𝟙 r₁ = 𝟙 r₁
Tactic: rw [conjugateEquiv_comp, Iso.inv_hom_id, 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₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : l₂ ≅ l₁
⊢ Eq (α := r₂ ⟶ r₂)
    (CategoryStruct.comp (Y := r₁) ((conjugateEquiv adj₂ adj₁ : (a : l₁ ⟶ l₂) → r₂ ⟶ r₁) α.inv)
        ((conjugateEquiv adj₁ adj₂ : (a : l₂ ⟶ l₁) → r₁ ⟶ r₂) α.hom) :
      r₂ ⟶ r₂)
    (𝟙 r₂ : r₂ ⟶ r₂)
have rw : Eq (α := r₂ ⟶ r₂) ((conjugateEquiv adj₂ adj₂ : (a : l₂ ⟶ l₂) → r₂ ⟶ r₂) (α.hom ≫ α.inv) : r₂ ⟶ r₂) (𝟙 r₂ : r₂ ⟶ r₂)
Tactic: rw [conjugateEquiv_comp, Iso.hom_inv_id, 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₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : l₂ ≅ l₁
rw : Eq (α := r₂ ⟶ r₂) ((conjugateEquiv adj₂ adj₂ : (a : l₂ ⟶ l₂) → r₂ ⟶ r₂) (α.hom ≫ α.inv) : r₂ ⟶ r₂) (𝟙 r₂ : r₂ ⟶ r₂)
⊢ Eq (α := r₂ ⟶ r₂)
    (CategoryStruct.comp (Y := r₁) ((conjugateEquiv adj₂ adj₁ : (a : l₁ ⟶ l₂) → r₂ ⟶ r₁) α.inv)
        ((conjugateEquiv adj₁ adj₂ : (a : l₂ ⟶ l₁) → r₁ ⟶ r₂) α.hom) :
      r₂ ⟶ r₂)
    (𝟙 r₂ : r₂ ⟶ r₂)
have rw₁ : Eq (α := r₂ ⟶ r₂) ((conjugateEquiv adj₂ adj₂ : (a : l₂ ⟶ l₂) → r₂ ⟶ r₂) (𝟙 l₂) : r₂ ⟶ r₂) (𝟙 r₂ : r₂ ⟶ r₂)
Tactic: rw [conjugateEquiv_comp, Iso.hom_inv_id, 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₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : l₂ ≅ l₁
rw : Eq (α := r₂ ⟶ r₂) ((conjugateEquiv adj₂ adj₂ : (a : l₂ ⟶ l₂) → r₂ ⟶ r₂) (α.hom ≫ α.inv) : r₂ ⟶ r₂) (𝟙 r₂ : r₂ ⟶ r₂)
rw₁ : Eq (α := r₂ ⟶ r₂) ((conjugateEquiv adj₂ adj₂ : (a : l₂ ⟶ l₂) → r₂ ⟶ r₂) (𝟙 l₂) : r₂ ⟶ r₂) (𝟙 r₂ : r₂ ⟶ r₂)
⊢ Eq (α := r₂ ⟶ r₂)
    (CategoryStruct.comp (Y := r₁) ((conjugateEquiv adj₂ adj₁ : (a : l₁ ⟶ l₂) → r₂ ⟶ r₁) α.inv)
        ((conjugateEquiv adj₁ adj₂ : (a : l₂ ⟶ l₁) → r₁ ⟶ r₂) α.hom) :
      r₂ ⟶ r₂)
    (𝟙 r₂ : r₂ ⟶ r₂)
have rw₂ : 𝟙 r₂ = 𝟙 r₂
Tactic: rw [conjugateEquiv_comp, Iso.hom_inv_id, 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₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
β : r₁ ≅ r₂
⊢ Eq (α := l₂ ⟶ l₂)
    (CategoryStruct.comp (Y := l₁) (((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁) β.hom)
        (((conjugateEquiv adj₂ adj₁).symm : (a : r₂ ⟶ r₁) → l₁ ⟶ l₂) β.inv) :
      l₂ ⟶ l₂)
    (𝟙 l₂ : l₂ ⟶ l₂)
have rw : Eq (α := l₂ ⟶ l₂) (((conjugateEquiv adj₂ adj₂).symm : (a : r₂ ⟶ r₂) → l₂ ⟶ l₂) (β.inv ≫ β.hom) : l₂ ⟶ l₂)
  (𝟙 l₂ : l₂ ⟶ l₂)
Tactic: rw [conjugateEquiv_symm_comp, Iso.inv_hom_id, conjugateEquiv_symm_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₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
β : r₁ ≅ r₂
rw :
  Eq (α := l₂ ⟶ l₂) (((conjugateEquiv adj₂ adj₂).symm : (a : r₂ ⟶ r₂) → l₂ ⟶ l₂) (β.inv ≫ β.hom) : l₂ ⟶ l₂)
    (𝟙 l₂ : l₂ ⟶ l₂)
⊢ Eq (α := l₂ ⟶ l₂)
    (CategoryStruct.comp (Y := l₁) (((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁) β.hom)
        (((conjugateEquiv adj₂ adj₁).symm : (a : r₂ ⟶ r₁) → l₁ ⟶ l₂) β.inv) :
      l₂ ⟶ l₂)
    (𝟙 l₂ : l₂ ⟶ l₂)
have rw₁ : Eq (α := l₂ ⟶ l₂) (((conjugateEquiv adj₂ adj₂).symm : (a : r₂ ⟶ r₂) → l₂ ⟶ l₂) (𝟙 r₂) : l₂ ⟶ l₂) (𝟙 l₂ : l₂ ⟶ l₂)
Tactic: rw [conjugateEquiv_symm_comp, Iso.inv_hom_id, conjugateEquiv_symm_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₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
β : r₁ ≅ r₂
rw :
  Eq (α := l₂ ⟶ l₂) (((conjugateEquiv adj₂ adj₂).symm : (a : r₂ ⟶ r₂) → l₂ ⟶ l₂) (β.inv ≫ β.hom) : l₂ ⟶ l₂)
    (𝟙 l₂ : l₂ ⟶ l₂)
rw₁ : Eq (α := l₂ ⟶ l₂) (((conjugateEquiv adj₂ adj₂).symm : (a : r₂ ⟶ r₂) → l₂ ⟶ l₂) (𝟙 r₂) : l₂ ⟶ l₂) (𝟙 l₂ : l₂ ⟶ l₂)
⊢ Eq (α := l₂ ⟶ l₂)
    (CategoryStruct.comp (Y := l₁) (((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁) β.hom)
        (((conjugateEquiv adj₂ adj₁).symm : (a : r₂ ⟶ r₁) → l₁ ⟶ l₂) β.inv) :
      l₂ ⟶ l₂)
    (𝟙 l₂ : l₂ ⟶ l₂)
have rw₂ : 𝟙 l₂ = 𝟙 l₂
Tactic: rw [conjugateEquiv_symm_comp, Iso.inv_hom_id, conjugateEquiv_symm_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₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
β : r₁ ≅ r₂
⊢ Eq (α := l₁ ⟶ l₁)
    (CategoryStruct.comp (Y := l₂) (((conjugateEquiv adj₂ adj₁).symm : (a : r₂ ⟶ r₁) → l₁ ⟶ l₂) β.inv)
        (((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁) β.hom) :
      l₁ ⟶ l₁)
    (𝟙 l₁ : l₁ ⟶ l₁)
have rw : Eq (α := l₁ ⟶ l₁) (((conjugateEquiv adj₁ adj₁).symm : (a : r₁ ⟶ r₁) → l₁ ⟶ l₁) (β.hom ≫ β.inv) : l₁ ⟶ l₁)
  (𝟙 l₁ : l₁ ⟶ l₁)
Tactic: rw [conjugateEquiv_symm_comp, Iso.hom_inv_id, conjugateEquiv_symm_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₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
β : r₁ ≅ r₂
rw :
  Eq (α := l₁ ⟶ l₁) (((conjugateEquiv adj₁ adj₁).symm : (a : r₁ ⟶ r₁) → l₁ ⟶ l₁) (β.hom ≫ β.inv) : l₁ ⟶ l₁)
    (𝟙 l₁ : l₁ ⟶ l₁)
⊢ Eq (α := l₁ ⟶ l₁)
    (CategoryStruct.comp (Y := l₂) (((conjugateEquiv adj₂ adj₁).symm : (a : r₂ ⟶ r₁) → l₁ ⟶ l₂) β.inv)
        (((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁) β.hom) :
      l₁ ⟶ l₁)
    (𝟙 l₁ : l₁ ⟶ l₁)
have rw₁ : Eq (α := l₁ ⟶ l₁) (((conjugateEquiv adj₁ adj₁).symm : (a : r₁ ⟶ r₁) → l₁ ⟶ l₁) (𝟙 r₁) : l₁ ⟶ l₁) (𝟙 l₁ : l₁ ⟶ l₁)
Tactic: rw [conjugateEquiv_symm_comp, Iso.hom_inv_id, conjugateEquiv_symm_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₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
β : r₁ ≅ r₂
rw :
  Eq (α := l₁ ⟶ l₁) (((conjugateEquiv adj₁ adj₁).symm : (a : r₁ ⟶ r₁) → l₁ ⟶ l₁) (β.hom ≫ β.inv) : l₁ ⟶ l₁)
    (𝟙 l₁ : l₁ ⟶ l₁)
rw₁ : Eq (α := l₁ ⟶ l₁) (((conjugateEquiv adj₁ adj₁).symm : (a : r₁ ⟶ r₁) → l₁ ⟶ l₁) (𝟙 r₁) : l₁ ⟶ l₁) (𝟙 l₁ : l₁ ⟶ l₁)
⊢ Eq (α := l₁ ⟶ l₁)
    (CategoryStruct.comp (Y := l₂) (((conjugateEquiv adj₂ adj₁).symm : (a : r₂ ⟶ r₁) → l₁ ⟶ l₂) β.inv)
        (((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁) β.hom) :
      l₁ ⟶ l₁)
    (𝟙 l₁ : l₁ ⟶ l₁)
have rw₂ : 𝟙 l₁ = 𝟙 l₁
Tactic: rw [conjugateEquiv_symm_comp, Iso.hom_inv_id, conjugateEquiv_symm_id]