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
f₁ : a ⟶ c
u₁ : c ⟶ a
f₂ : b ⟶ d
u₂ : d ⟶ b
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : f₁ ⊣ u₁
adj₄ : f₂ ⊣ u₂
α : f₁ ≫ l₂ ⟶ l₁ ≫ f₂
⊢ Eq (α := u₂ ≫ r₁ ⟶ r₂ ≫ u₁)
    ((mateEquiv adj₄ adj₃ : (a_1 : r₁ ≫ f₁ ⟶ f₂ ≫ r₂) → u₂ ≫ r₁ ⟶ r₂ ≫ u₁)
        ((mateEquiv adj₁ adj₂ : (a_1 : f₁ ≫ l₂ ⟶ l₁ ≫ f₂) → r₁ ≫ f₁ ⟶ f₂ ≫ r₂) α : r₁ ≫ f₁ ⟶ f₂ ≫ r₂) :
      u₂ ≫ r₁ ⟶ r₂ ≫ u₁)
    ((conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂) : (a_1 : f₁ ≫ l₂ ⟶ l₁ ≫ f₂) → u₂ ≫ r₁ ⟶ r₂ ≫ u₁) α :
      u₂ ≫ r₁ ⟶ r₂ ≫ u₁)
have simp : 𝟙 (u₂ ≫ r₁) ⊗≫
    u₂ ◁ r₁ ◁ adj₃.unit ⊗≫
      u₂ ◁ (𝟙 (r₁ ≫ f₁) ⊗≫ r₁ ◁ f₁ ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ f₂ ▷ r₂ ⊗≫ 𝟙 (f₂ ≫ r₂)) ▷ u₁ ⊗≫
        adj₄.counit ▷ r₂ ▷ u₁ ⊗≫ 𝟙 (r₂ ≫ u₁) =
  (ρ_ (u₂ ≫ r₁)).inv ≫
    bicategoricalComp (h := (u₂ ≫ r₁) ≫ 𝟙 a ≫ 𝟙 a) (𝟙 ((u₂ ≫ r₁) ≫ 𝟙 a))
        ((u₂ ≫ r₁) ◁ 𝟙 a ◁ (adj₃.comp adj₂).unit ⊗≫
          (u₂ ≫ r₁) ◁ ((λ_ (f₁ ≫ l₂)).hom ≫ α ≫ (ρ_ (l₁ ≫ f₂)).inv) ▷ (r₂ ≫ u₁) ⊗≫
            (adj₁.comp adj₄).counit ▷ 𝟙 d ▷ (r₂ ≫ u₁) ⊗≫ 𝟙 (𝟙 d ≫ r₂ ≫ u₁)) ≫
      (λ_ (r₂ ≫ u₁)).hom
Tactic: simp only [conjugateEquiv_apply, mateEquiv_apply']
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Adjunction.Mate (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
f₁ : a ⟶ c
u₁ : c ⟶ a
f₂ : b ⟶ d
u₂ : d ⟶ b
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : f₁ ⊣ u₁
adj₄ : f₂ ⊣ u₂
α : f₁ ≫ l₂ ⟶ l₁ ≫ f₂
⊢ 𝟙 (u₂ ≫ r₁) ⊗≫
      u₂ ◁ r₁ ◁ adj₃.unit ⊗≫
        u₂ ◁ (𝟙 (r₁ ≫ f₁) ⊗≫ r₁ ◁ f₁ ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ f₂ ▷ r₂ ⊗≫ 𝟙 (f₂ ≫ r₂)) ▷ u₁ ⊗≫
          adj₄.counit ▷ r₂ ▷ u₁ ⊗≫ 𝟙 (r₂ ≫ u₁) =
    (ρ_ (u₂ ≫ r₁)).inv ≫
      bicategoricalComp (h := (u₂ ≫ r₁) ≫ 𝟙 a ≫ 𝟙 a) (𝟙 ((u₂ ≫ r₁) ≫ 𝟙 a))
          ((u₂ ≫ r₁) ◁ 𝟙 a ◁ (adj₃.comp adj₂).unit ⊗≫
            (u₂ ≫ r₁) ◁ ((λ_ (f₁ ≫ l₂)).hom ≫ α ≫ (ρ_ (l₁ ≫ f₂)).inv) ▷ (r₂ ≫ u₁) ⊗≫
              (adj₁.comp adj₄).counit ▷ 𝟙 d ▷ (r₂ ≫ u₁) ⊗≫ 𝟙 (𝟙 d ≫ r₂ ≫ u₁)) ≫
        (λ_ (r₂ ≫ u₁)).hom
have dsimp : 𝟙 (u₂ ≫ r₁) ⊗≫
    u₂ ◁ r₁ ◁ adj₃.unit ⊗≫
      u₂ ◁ (𝟙 (r₁ ≫ f₁) ⊗≫ r₁ ◁ f₁ ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ f₂ ▷ r₂ ⊗≫ 𝟙 (f₂ ≫ r₂)) ▷ u₁ ⊗≫
        adj₄.counit ▷ r₂ ▷ u₁ ⊗≫ 𝟙 (r₂ ≫ u₁) =
  (ρ_ (u₂ ≫ r₁)).inv ≫
    bicategoricalComp (h := (u₂ ≫ r₁) ≫ 𝟙 a ≫ 𝟙 a) (𝟙 ((u₂ ≫ r₁) ≫ 𝟙 a))
        ((u₂ ≫ r₁) ◁ 𝟙 a ◁ (adj₃.unit ⊗≫ f₁ ◁ adj₂.unit ▷ u₁ ⊗≫ 𝟙 ((f₁ ≫ l₂) ≫ r₂ ≫ u₁)) ⊗≫
          (u₂ ≫ r₁) ◁ ((λ_ (f₁ ≫ l₂)).hom ≫ α ≫ (ρ_ (l₁ ≫ f₂)).inv) ▷ (r₂ ≫ u₁) ⊗≫
            (𝟙 ((u₂ ≫ r₁) ≫ l₁ ≫ f₂) ⊗≫ u₂ ◁ adj₁.counit ▷ f₂ ⊗≫ adj₄.counit) ▷ 𝟙 d ▷ (r₂ ≫ u₁) ⊗≫ 𝟙 (𝟙 d ≫ r₂ ≫ u₁)) ≫
      (λ_ (r₂ ≫ u₁)).hom
Tactic: dsimp [Adjunction.comp]
-- 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
f₁ : a ⟶ c
u₁ : c ⟶ a
f₂ : b ⟶ d
u₂ : d ⟶ b
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : f₁ ⊣ u₁
adj₄ : f₂ ⊣ u₂
α : u₂ ≫ r₁ ⟶ r₂ ≫ u₁
⊢ Eq (α := f₁ ≫ l₂ ⟶ l₁ ≫ f₂)
    ((Equiv.symm (mateEquiv adj₁ adj₂) : (a_1 : r₁ ≫ f₁ ⟶ f₂ ≫ r₂) → f₁ ≫ l₂ ⟶ l₁ ≫ f₂)
        ((Equiv.symm (mateEquiv adj₄ adj₃) : (a_1 : u₂ ≫ r₁ ⟶ r₂ ≫ u₁) → r₁ ≫ f₁ ⟶ f₂ ≫ r₂) α : r₁ ≫ f₁ ⟶ f₂ ≫ r₂) :
      f₁ ≫ l₂ ⟶ l₁ ≫ f₂)
    (((conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)).symm : (a_1 : u₂ ≫ r₁ ⟶ r₂ ≫ u₁) → f₁ ≫ l₂ ⟶ l₁ ≫ f₂) α :
      f₁ ≫ l₂ ⟶ l₁ ≫ f₂)
have rw : (mateEquiv adj₄ adj₃ : (a_1 : r₁ ≫ f₁ ⟶ f₂ ≫ r₂) → u₂ ≫ r₁ ⟶ r₂ ≫ u₁)
    ((mateEquiv adj₁ adj₂ : (a_1 : f₁ ≫ l₂ ⟶ l₁ ≫ f₂) → r₁ ≫ f₁ ⟶ f₂ ≫ r₂)
        ((Equiv.symm (mateEquiv adj₁ adj₂) : (a_1 : r₁ ≫ f₁ ⟶ f₂ ≫ r₂) → f₁ ≫ l₂ ⟶ l₁ ≫ f₂)
            ((Equiv.symm (mateEquiv adj₄ adj₃) : (a_1 : u₂ ≫ r₁ ⟶ r₂ ≫ u₁) → r₁ ≫ f₁ ⟶ f₂ ≫ r₂) α : r₁ ≫ f₁ ⟶ f₂ ≫ r₂) :
          f₁ ≫ l₂ ⟶ l₁ ≫ f₂) :
      r₁ ≫ f₁ ⟶ f₂ ≫ r₂) =
  α
Tactic: rw [Equiv.eq_symm_apply, ← iterated_mateEquiv_conjugateEquiv]
-- 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
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g ≫ l₂ ⟶ l₁ ≫ h
β : l₃ ⟶ l₂
⊢ Eq (α := r₁ ≫ g ⟶ h ≫ r₃)
    ((mateEquiv adj₁ adj₃ : (a_1 : g ≫ l₃ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₃) (leftAdjointSquareConjugate.vcomp α β) :
      r₁ ≫ g ⟶ h ≫ r₃)
    (rightAdjointSquareConjugate.vcomp (r₂ := r₂) ((mateEquiv adj₁ adj₂ : (a_1 : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α)
        ((conjugateEquiv adj₂ adj₃ : (a : l₃ ⟶ l₂) → r₂ ⟶ r₃) β) :
      r₁ ≫ g ⟶ h ≫ r₃)
have symm : Eq.{w + 1} (α := r₁ ≫ g ⟶ h ≫ r₃)
  (rightAdjointSquareConjugate.vcomp (r₂ := r₂) ((mateEquiv adj₁ adj₂ : (a_1 : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α)
    ((conjugateEquiv adj₂ adj₃ : (a : l₃ ⟶ l₂) → r₂ ⟶ r₃) β))
  ((mateEquiv adj₁ adj₃ : (a_1 : g ≫ l₃ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₃) (leftAdjointSquareConjugate.vcomp α β))
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 : B
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g ≫ l₂ ⟶ l₁ ≫ h
β : l₃ ⟶ l₂
⊢ rightAdjointSquareConjugate.vcomp (r₂ := r₂) ((mateEquiv adj₁ adj₂ : (a_1 : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α)
      ((conjugateEquiv adj₂ adj₃ : (a : l₃ ⟶ l₂) → r₂ ⟶ r₃) β) =
    bicategoricalComp (h := r₁ ≫ g ≫ 𝟙 c) (𝟙 (r₁ ≫ g))
      (bicategoricalComp (g := (h ≫ 𝟙 d) ≫ r₃)
        (rightAdjointSquare.vcomp (r₂ := r₂) ((mateEquiv adj₁ adj₂ : (a_1 : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α)
          ((mateEquiv adj₂ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₂ ≫ 𝟙 d) → r₂ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)))
        (𝟙 (h ≫ r₃)))
have dsimp : (mateEquiv adj₁ adj₂ : (a_1 : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α ≫
    h ◁
      ((ρ_ r₂).inv ≫
        (mateEquiv adj₂ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₂ ≫ 𝟙 d) → r₂ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫
          (λ_ r₃).hom) =
  𝟙 (r₁ ≫ g) ⊗≫
    ((α_ r₁ g (𝟙 c)).inv ≫
        (mateEquiv adj₁ adj₂ : (a_1 : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α ▷ 𝟙 c ≫
          (α_ h r₂ (𝟙 c)).hom ≫
            h ◁
                (mateEquiv adj₂ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₂ ≫ 𝟙 d) → r₂ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃)
                  ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫
              (α_ h (𝟙 d) r₃).inv) ⊗≫
      𝟙 (h ≫ r₃)
Tactic: dsimp only [conjugateEquiv_apply, rightAdjointSquareConjugate.vcomp,
        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 : B
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g ≫ l₂ ⟶ l₁ ≫ h
β : l₃ ⟶ l₂
⊢ bicategoricalComp (h := r₁ ≫ g ≫ 𝟙 c) (𝟙 (r₁ ≫ g))
      (bicategoricalComp (g := (h ≫ 𝟙 d) ≫ r₃)
        (rightAdjointSquare.vcomp (r₂ := r₂) ((mateEquiv adj₁ adj₂ : (a_1 : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α)
          ((mateEquiv adj₂ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₂ ≫ 𝟙 d) → r₂ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)))
        (𝟙 (h ≫ r₃))) =
    (mateEquiv adj₁ adj₃ : (a_1 : g ≫ l₃ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₃) (leftAdjointSquareConjugate.vcomp α β)
have rw : bicategoricalComp (h := r₁ ≫ g ≫ 𝟙 c) (𝟙 (r₁ ≫ g))
    (bicategoricalComp (g := (h ≫ 𝟙 d) ≫ r₃)
      ((mateEquiv adj₁ adj₃ : (a_1 : (g ≫ 𝟙 c) ≫ l₃ ⟶ l₁ ≫ h ≫ 𝟙 d) → r₁ ≫ g ≫ 𝟙 c ⟶ (h ≫ 𝟙 d) ≫ r₃)
        (leftAdjointSquare.vcomp α ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)))
      (𝟙 (h ≫ r₃))) =
  (mateEquiv adj₁ adj₃ : (a_1 : g ≫ l₃ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₃) (leftAdjointSquareConjugate.vcomp α β)
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
a b c d : B
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g ≫ l₂ ⟶ l₁ ≫ h
β : l₃ ⟶ l₂
⊢ bicategoricalComp (h := r₁ ≫ g ≫ 𝟙 c) (𝟙 (r₁ ≫ g))
      (bicategoricalComp (g := (h ≫ 𝟙 d) ≫ r₃)
        ((mateEquiv adj₁ adj₃ : (a_1 : (g ≫ 𝟙 c) ≫ l₃ ⟶ l₁ ≫ h ≫ 𝟙 d) → r₁ ≫ g ≫ 𝟙 c ⟶ (h ≫ 𝟙 d) ≫ r₃)
          (leftAdjointSquare.vcomp α ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)))
        (𝟙 (h ≫ r₃))) =
    (mateEquiv adj₁ adj₃ : (a_1 : g ≫ l₃ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₃) (leftAdjointSquareConjugate.vcomp α β)
have simp : 𝟙 (r₁ ≫ g) ⊗≫
    (𝟙 (r₁ ≫ g ≫ 𝟙 c) ⊗≫
        r₁ ◁ (g ≫ 𝟙 c) ◁ adj₃.unit ⊗≫
          r₁ ◁
              ((α_ g (𝟙 c) l₃).hom ≫
                  g ◁ ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫ (α_ g l₂ (𝟙 d)).inv ≫ α ▷ 𝟙 d ≫ (α_ l₁ h (𝟙 d)).hom) ▷
                r₃ ⊗≫
            adj₁.counit ▷ (h ≫ 𝟙 d) ▷ r₃ ⊗≫ 𝟙 ((h ≫ 𝟙 d) ≫ r₃)) ⊗≫
      𝟙 (h ≫ r₃) =
  𝟙 (r₁ ≫ g) ⊗≫ r₁ ◁ g ◁ adj₃.unit ⊗≫ r₁ ◁ (g ◁ β ≫ α) ▷ r₃ ⊗≫ adj₁.counit ▷ h ▷ r₃ ⊗≫ 𝟙 (h ≫ r₃)
Tactic: simp only [leftAdjointSquare.vcomp, mateEquiv_apply', leftAdjointSquareConjugate.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 : B
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g ≫ l₂ ⟶ l₁ ≫ h
β : l₃ ⟶ l₂
⊢ Eq.{w + 1} (α := r₁ ≫ g ⟶ h ≫ r₃)
    (rightAdjointSquareConjugate.vcomp (r₂ := r₂) ((mateEquiv adj₁ adj₂ : (a_1 : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α)
      ((conjugateEquiv adj₂ adj₃ : (a : l₃ ⟶ l₂) → r₂ ⟶ r₃) β))
    ((mateEquiv adj₁ adj₃ : (a_1 : g ≫ l₃ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₃) (leftAdjointSquareConjugate.vcomp α β))
have _ : rightAdjointSquareConjugate.vcomp (r₂ := r₂) ((mateEquiv adj₁ adj₂ : (a_1 : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α)
    ((conjugateEquiv adj₂ adj₃ : (a : l₃ ⟶ l₂) → r₂ ⟶ r₃) β) =
  bicategoricalComp (h := r₁ ≫ g ≫ 𝟙 c) (𝟙 (r₁ ≫ g))
    (bicategoricalComp (g := (h ≫ 𝟙 d) ≫ r₃)
      (rightAdjointSquare.vcomp (r₂ := r₂) ((mateEquiv adj₁ adj₂ : (a_1 : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α)
        ((mateEquiv adj₂ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₂ ≫ 𝟙 d) → r₂ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)))
      (𝟙 (h ≫ r₃)))
Tactic: calc
    _ = 𝟙 _ ⊗≫
          rightAdjointSquare.vcomp
            (mateEquiv adj₁ adj₂ α)
            (mateEquiv adj₂ adj₃ ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)) ⊗≫ 𝟙 _ := by
      dsimp only [conjugateEquiv_apply, rightAdjointSquareConjugate.vcomp,
        rightAdjointSquare.vcomp]
      bicategory
    _ = _ := by
      rw [← mateEquiv_vcomp]
      simp only [leftAdjointSquare.vcomp, mateEquiv_apply', leftAdjointSquareConjugate.vcomp]
      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
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g ≫ l₂ ⟶ l₁ ≫ h
β : l₃ ⟶ l₂
_ :
  rightAdjointSquareConjugate.vcomp (r₂ := r₂) ((mateEquiv adj₁ adj₂ : (a_1 : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α)
      ((conjugateEquiv adj₂ adj₃ : (a : l₃ ⟶ l₂) → r₂ ⟶ r₃) β) =
    bicategoricalComp (h := r₁ ≫ g ≫ 𝟙 c) (𝟙 (r₁ ≫ g))
      (bicategoricalComp (g := (h ≫ 𝟙 d) ≫ r₃)
        (rightAdjointSquare.vcomp (r₂ := r₂) ((mateEquiv adj₁ adj₂ : (a_1 : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α)
          ((mateEquiv adj₂ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₂ ≫ 𝟙 d) → r₂ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)))
        (𝟙 (h ≫ r₃)))
⊢ Eq.{w + 1} (α := r₁ ≫ g ⟶ h ≫ r₃)
    (rightAdjointSquareConjugate.vcomp (r₂ := r₂) ((mateEquiv adj₁ adj₂ : (a_1 : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α)
      ((conjugateEquiv adj₂ adj₃ : (a : l₃ ⟶ l₂) → r₂ ⟶ r₃) β))
    ((mateEquiv adj₁ adj₃ : (a_1 : g ≫ l₃ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₃) (leftAdjointSquareConjugate.vcomp α β))
have _₁ : bicategoricalComp (h := r₁ ≫ g ≫ 𝟙 c) (𝟙 (r₁ ≫ g))
    (bicategoricalComp (g := (h ≫ 𝟙 d) ≫ r₃)
      (rightAdjointSquare.vcomp (r₂ := r₂) ((mateEquiv adj₁ adj₂ : (a_1 : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α)
        ((mateEquiv adj₂ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₂ ≫ 𝟙 d) → r₂ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)))
      (𝟙 (h ≫ r₃))) =
  (mateEquiv adj₁ adj₃ : (a_1 : g ≫ l₃ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₃) (leftAdjointSquareConjugate.vcomp α β)
Tactic: calc
    _ = 𝟙 _ ⊗≫
          rightAdjointSquare.vcomp
            (mateEquiv adj₁ adj₂ α)
            (mateEquiv adj₂ adj₃ ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)) ⊗≫ 𝟙 _ := by
      dsimp only [conjugateEquiv_apply, rightAdjointSquareConjugate.vcomp,
        rightAdjointSquare.vcomp]
      bicategory
    _ = _ := by
      rw [← mateEquiv_vcomp]
      simp only [leftAdjointSquare.vcomp, mateEquiv_apply', leftAdjointSquareConjugate.vcomp]
      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
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : a ⟶ b
r₂ : b ⟶ a
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : g ≫ l₃ ⟶ l₂ ≫ h
⊢ Eq (α := r₁ ≫ g ⟶ h ≫ r₃)
    ((mateEquiv adj₁ adj₃ : (a_1 : g ≫ l₃ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₃) (leftAdjointConjugateSquare.vcomp α β) :
      r₁ ≫ g ⟶ h ≫ r₃)
    (rightAdjointConjugateSquare.vcomp (r₂ := r₂) ((conjugateEquiv adj₁ adj₂ : (a_1 : l₂ ⟶ l₁) → r₁ ⟶ r₂) α)
        ((mateEquiv adj₂ adj₃ : (a_1 : g ≫ l₃ ⟶ l₂ ≫ h) → r₂ ≫ g ⟶ h ≫ r₃) β) :
      r₁ ≫ g ⟶ h ≫ r₃)
have symm : Eq.{w + 1} (α := r₁ ≫ g ⟶ h ≫ r₃)
  (rightAdjointConjugateSquare.vcomp (r₂ := r₂) ((conjugateEquiv adj₁ adj₂ : (a_1 : l₂ ⟶ l₁) → r₁ ⟶ r₂) α)
    ((mateEquiv adj₂ adj₃ : (a_1 : g ≫ l₃ ⟶ l₂ ≫ h) → r₂ ≫ g ⟶ h ≫ r₃) β))
  ((mateEquiv adj₁ adj₃ : (a_1 : g ≫ l₃ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₃) (leftAdjointConjugateSquare.vcomp α β))
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 : B
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : a ⟶ b
r₂ : b ⟶ a
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : g ≫ l₃ ⟶ l₂ ≫ h
⊢ rightAdjointConjugateSquare.vcomp (r₂ := r₂) ((conjugateEquiv adj₁ adj₂ : (a_1 : l₂ ⟶ l₁) → r₁ ⟶ r₂) α)
      ((mateEquiv adj₂ adj₃ : (a_1 : g ≫ l₃ ⟶ l₂ ≫ h) → r₂ ≫ g ⟶ h ≫ r₃) β) =
    bicategoricalComp (h := r₁ ≫ 𝟙 a ≫ g) (𝟙 (r₁ ≫ g))
      (bicategoricalComp (g := (𝟙 b ≫ h) ≫ r₃)
        (rightAdjointSquare.vcomp (r₂ := r₂)
          ((mateEquiv adj₁ adj₂ : (a_1 : 𝟙 a ≫ l₂ ⟶ l₁ ≫ 𝟙 b) → r₁ ≫ 𝟙 a ⟶ 𝟙 b ≫ r₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv))
          ((mateEquiv adj₂ adj₃ : (a_1 : g ≫ l₃ ⟶ l₂ ≫ h) → r₂ ≫ g ⟶ h ≫ r₃) β))
        (𝟙 (h ≫ r₃)))
have dsimp : CategoryStruct.comp (Y := r₂ ≫ g)
    (((ρ_ r₁).inv ≫
        (mateEquiv adj₁ adj₂ : (a_1 : 𝟙 a ≫ l₂ ⟶ l₁ ≫ 𝟙 b) → r₁ ≫ 𝟙 a ⟶ 𝟙 b ≫ r₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ≫
          (λ_ r₂).hom) ▷
      g)
    ((mateEquiv adj₂ adj₃ : (a_1 : g ≫ l₃ ⟶ l₂ ≫ h) → r₂ ≫ g ⟶ h ≫ r₃) β) =
  𝟙 (r₁ ≫ g) ⊗≫
    bicategoricalComp (g := (𝟙 b ≫ h) ≫ r₃)
      ((α_ r₁ (𝟙 a) g).inv ≫
        (mateEquiv adj₁ adj₂ : (a_1 : 𝟙 a ≫ l₂ ⟶ l₁ ≫ 𝟙 b) → r₁ ≫ 𝟙 a ⟶ 𝟙 b ≫ r₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ▷ g ≫
          Iso.hom (α_ (𝟙 b) r₂ g) ≫
            𝟙 b ◁ (mateEquiv adj₂ adj₃ : (a_1 : g ≫ l₃ ⟶ l₂ ≫ h) → r₂ ≫ g ⟶ h ≫ r₃) β ≫ Iso.inv (α_ (𝟙 b) h r₃))
      (𝟙 (h ≫ r₃))
Tactic: dsimp only [conjugateEquiv_apply, rightAdjointConjugateSquare.vcomp, 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 : B
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : a ⟶ b
r₂ : b ⟶ a
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : g ≫ l₃ ⟶ l₂ ≫ h
⊢ bicategoricalComp (h := r₁ ≫ 𝟙 a ≫ g) (𝟙 (r₁ ≫ g))
      (bicategoricalComp (g := (𝟙 b ≫ h) ≫ r₃)
        (rightAdjointSquare.vcomp (r₂ := r₂)
          ((mateEquiv adj₁ adj₂ : (a_1 : 𝟙 a ≫ l₂ ⟶ l₁ ≫ 𝟙 b) → r₁ ≫ 𝟙 a ⟶ 𝟙 b ≫ r₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv))
          ((mateEquiv adj₂ adj₃ : (a_1 : g ≫ l₃ ⟶ l₂ ≫ h) → r₂ ≫ g ⟶ h ≫ r₃) β))
        (𝟙 (h ≫ r₃))) =
    (mateEquiv adj₁ adj₃ : (a_1 : g ≫ l₃ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₃) (leftAdjointConjugateSquare.vcomp α β)
have rw : bicategoricalComp (h := r₁ ≫ 𝟙 a ≫ g) (𝟙 (r₁ ≫ g))
    (bicategoricalComp (g := (𝟙 b ≫ h) ≫ r₃)
      ((mateEquiv adj₁ adj₃ : (a_1 : (𝟙 a ≫ g) ≫ l₃ ⟶ l₁ ≫ 𝟙 b ≫ h) → r₁ ≫ 𝟙 a ≫ g ⟶ (𝟙 b ≫ h) ≫ r₃)
        (leftAdjointSquare.vcomp ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) β))
      (𝟙 (h ≫ r₃))) =
  (mateEquiv adj₁ adj₃ : (a_1 : g ≫ l₃ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₃) (leftAdjointConjugateSquare.vcomp α β)
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
a b c d : B
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : a ⟶ b
r₂ : b ⟶ a
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : g ≫ l₃ ⟶ l₂ ≫ h
⊢ bicategoricalComp (h := r₁ ≫ 𝟙 a ≫ g) (𝟙 (r₁ ≫ g))
      (bicategoricalComp (g := (𝟙 b ≫ h) ≫ r₃)
        ((mateEquiv adj₁ adj₃ : (a_1 : (𝟙 a ≫ g) ≫ l₃ ⟶ l₁ ≫ 𝟙 b ≫ h) → r₁ ≫ 𝟙 a ≫ g ⟶ (𝟙 b ≫ h) ≫ r₃)
          (leftAdjointSquare.vcomp ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) β))
        (𝟙 (h ≫ r₃))) =
    (mateEquiv adj₁ adj₃ : (a_1 : g ≫ l₃ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₃) (leftAdjointConjugateSquare.vcomp α β)
have simp : 𝟙 (r₁ ≫ g) ⊗≫
    (𝟙 (r₁ ≫ 𝟙 a ≫ g) ⊗≫
        bicategoricalComp (h := r₁ ≫ ((𝟙 a ≫ g) ≫ l₃) ≫ r₃) (r₁ ◁ (𝟙 a ≫ g) ◁ adj₃.unit)
          (r₁ ◁
              (Iso.hom (α_ (𝟙 a) g l₃) ≫
                  𝟙 a ◁ β ≫ Iso.inv (α_ (𝟙 a) l₂ h) ≫ ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ▷ h ≫ (α_ l₁ (𝟙 b) h).hom) ▷
                r₃ ⊗≫
            adj₁.counit ▷ (𝟙 b ≫ h) ▷ r₃ ⊗≫ 𝟙 ((𝟙 b ≫ h) ≫ r₃))) ⊗≫
      𝟙 (h ≫ r₃) =
  𝟙 (r₁ ≫ g) ⊗≫ r₁ ◁ g ◁ adj₃.unit ⊗≫ r₁ ◁ (β ≫ α ▷ h) ▷ r₃ ⊗≫ adj₁.counit ▷ h ▷ r₃ ⊗≫ 𝟙 (h ≫ r₃)
Tactic: simp only [leftAdjointSquare.vcomp, mateEquiv_apply', leftAdjointConjugateSquare.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 : B
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : a ⟶ b
r₂ : b ⟶ a
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : g ≫ l₃ ⟶ l₂ ≫ h
⊢ Eq.{w + 1} (α := r₁ ≫ g ⟶ h ≫ r₃)
    (rightAdjointConjugateSquare.vcomp (r₂ := r₂) ((conjugateEquiv adj₁ adj₂ : (a_1 : l₂ ⟶ l₁) → r₁ ⟶ r₂) α)
      ((mateEquiv adj₂ adj₃ : (a_1 : g ≫ l₃ ⟶ l₂ ≫ h) → r₂ ≫ g ⟶ h ≫ r₃) β))
    ((mateEquiv adj₁ adj₃ : (a_1 : g ≫ l₃ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₃) (leftAdjointConjugateSquare.vcomp α β))
have _ : rightAdjointConjugateSquare.vcomp (r₂ := r₂) ((conjugateEquiv adj₁ adj₂ : (a_1 : l₂ ⟶ l₁) → r₁ ⟶ r₂) α)
    ((mateEquiv adj₂ adj₃ : (a_1 : g ≫ l₃ ⟶ l₂ ≫ h) → r₂ ≫ g ⟶ h ≫ r₃) β) =
  bicategoricalComp (h := r₁ ≫ 𝟙 a ≫ g) (𝟙 (r₁ ≫ g))
    (bicategoricalComp (g := (𝟙 b ≫ h) ≫ r₃)
      (rightAdjointSquare.vcomp (r₂ := r₂)
        ((mateEquiv adj₁ adj₂ : (a_1 : 𝟙 a ≫ l₂ ⟶ l₁ ≫ 𝟙 b) → r₁ ≫ 𝟙 a ⟶ 𝟙 b ≫ r₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv))
        ((mateEquiv adj₂ adj₃ : (a_1 : g ≫ l₃ ⟶ l₂ ≫ h) → r₂ ≫ g ⟶ h ≫ r₃) β))
      (𝟙 (h ≫ r₃)))
Tactic: calc
    _ = 𝟙 _ ⊗≫
          rightAdjointSquare.vcomp
            (mateEquiv adj₁ adj₂ ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv))
            (mateEquiv adj₂ adj₃ β) ⊗≫ 𝟙 _ := by
      dsimp only [conjugateEquiv_apply, rightAdjointConjugateSquare.vcomp, rightAdjointSquare.vcomp]
      bicategory
    _ = _ := by
      rw [← mateEquiv_vcomp]
      simp only [leftAdjointSquare.vcomp, mateEquiv_apply', leftAdjointConjugateSquare.vcomp]
      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
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : a ⟶ b
r₂ : b ⟶ a
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : g ≫ l₃ ⟶ l₂ ≫ h
_ :
  rightAdjointConjugateSquare.vcomp (r₂ := r₂) ((conjugateEquiv adj₁ adj₂ : (a_1 : l₂ ⟶ l₁) → r₁ ⟶ r₂) α)
      ((mateEquiv adj₂ adj₃ : (a_1 : g ≫ l₃ ⟶ l₂ ≫ h) → r₂ ≫ g ⟶ h ≫ r₃) β) =
    bicategoricalComp (h := r₁ ≫ 𝟙 a ≫ g) (𝟙 (r₁ ≫ g))
      (bicategoricalComp (g := (𝟙 b ≫ h) ≫ r₃)
        (rightAdjointSquare.vcomp (r₂ := r₂)
          ((mateEquiv adj₁ adj₂ : (a_1 : 𝟙 a ≫ l₂ ⟶ l₁ ≫ 𝟙 b) → r₁ ≫ 𝟙 a ⟶ 𝟙 b ≫ r₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv))
          ((mateEquiv adj₂ adj₃ : (a_1 : g ≫ l₃ ⟶ l₂ ≫ h) → r₂ ≫ g ⟶ h ≫ r₃) β))
        (𝟙 (h ≫ r₃)))
⊢ Eq.{w + 1} (α := r₁ ≫ g ⟶ h ≫ r₃)
    (rightAdjointConjugateSquare.vcomp (r₂ := r₂) ((conjugateEquiv adj₁ adj₂ : (a_1 : l₂ ⟶ l₁) → r₁ ⟶ r₂) α)
      ((mateEquiv adj₂ adj₃ : (a_1 : g ≫ l₃ ⟶ l₂ ≫ h) → r₂ ≫ g ⟶ h ≫ r₃) β))
    ((mateEquiv adj₁ adj₃ : (a_1 : g ≫ l₃ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₃) (leftAdjointConjugateSquare.vcomp α β))
have _₁ : bicategoricalComp (h := r₁ ≫ 𝟙 a ≫ g) (𝟙 (r₁ ≫ g))
    (bicategoricalComp (g := (𝟙 b ≫ h) ≫ r₃)
      (rightAdjointSquare.vcomp (r₂ := r₂)
        ((mateEquiv adj₁ adj₂ : (a_1 : 𝟙 a ≫ l₂ ⟶ l₁ ≫ 𝟙 b) → r₁ ≫ 𝟙 a ⟶ 𝟙 b ≫ r₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv))
        ((mateEquiv adj₂ adj₃ : (a_1 : g ≫ l₃ ⟶ l₂ ≫ h) → r₂ ≫ g ⟶ h ≫ r₃) β))
      (𝟙 (h ≫ r₃))) =
  (mateEquiv adj₁ adj₃ : (a_1 : g ≫ l₃ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₃) (leftAdjointConjugateSquare.vcomp α β)
Tactic: calc
    _ = 𝟙 _ ⊗≫
          rightAdjointSquare.vcomp
            (mateEquiv adj₁ adj₂ ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv))
            (mateEquiv adj₂ adj₃ β) ⊗≫ 𝟙 _ := by
      dsimp only [conjugateEquiv_apply, rightAdjointConjugateSquare.vcomp, rightAdjointSquare.vcomp]
      bicategory
    _ = _ := by
      rw [← mateEquiv_vcomp]
      simp only [leftAdjointSquare.vcomp, mateEquiv_apply', leftAdjointConjugateSquare.vcomp]
      bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ≅ h
⊢ f ◁ η.hom ≫ f ◁ η.inv = 𝟙 (f ≫ g)
have rw : f ◁ (η.hom ≫ η.inv) = 𝟙 (f ≫ g)
Tactic: rw [← whiskerLeft_comp, hom_inv_id, whiskerLeft_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ≅ h
rw : f ◁ (η.hom ≫ η.inv) = 𝟙 (f ≫ g)
⊢ f ◁ η.hom ≫ f ◁ η.inv = 𝟙 (f ≫ g)
have rw₁ : f ◁ 𝟙 g = 𝟙 (f ≫ g)
Tactic: rw [← whiskerLeft_comp, hom_inv_id, whiskerLeft_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ≅ h
rw : f ◁ (η.hom ≫ η.inv) = 𝟙 (f ≫ g)
rw₁ : f ◁ 𝟙 g = 𝟙 (f ≫ g)
⊢ f ◁ η.hom ≫ f ◁ η.inv = 𝟙 (f ≫ g)
have rw₂ : 𝟙 (f ≫ g) = 𝟙 (f ≫ g)
Tactic: rw [← whiskerLeft_comp, hom_inv_id, whiskerLeft_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f g : a ⟶ b
η : f ≅ g
h : b ⟶ c
⊢ η.hom ▷ h ≫ η.inv ▷ h = 𝟙 (f ≫ h)
have rw : (η.hom ≫ η.inv) ▷ h = 𝟙 (f ≫ h)
Tactic: rw [← comp_whiskerRight, hom_inv_id, id_whiskerRight]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f g : a ⟶ b
η : f ≅ g
h : b ⟶ c
rw : (η.hom ≫ η.inv) ▷ h = 𝟙 (f ≫ h)
⊢ η.hom ▷ h ≫ η.inv ▷ h = 𝟙 (f ≫ h)
have rw₁ : 𝟙 f ▷ h = 𝟙 (f ≫ h)
Tactic: rw [← comp_whiskerRight, hom_inv_id, id_whiskerRight]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f g : a ⟶ b
η : f ≅ g
h : b ⟶ c
rw : (η.hom ≫ η.inv) ▷ h = 𝟙 (f ≫ h)
rw₁ : 𝟙 f ▷ h = 𝟙 (f ≫ h)
⊢ η.hom ▷ h ≫ η.inv ▷ h = 𝟙 (f ≫ h)
have rw₂ : 𝟙 (f ≫ h) = 𝟙 (f ≫ h)
Tactic: rw [← comp_whiskerRight, hom_inv_id, id_whiskerRight]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ≅ h
⊢ f ◁ η.inv ≫ f ◁ η.hom = 𝟙 (f ≫ h)
have rw : f ◁ (η.inv ≫ η.hom) = 𝟙 (f ≫ h)
Tactic: rw [← whiskerLeft_comp, inv_hom_id, whiskerLeft_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ≅ h
rw : f ◁ (η.inv ≫ η.hom) = 𝟙 (f ≫ h)
⊢ f ◁ η.inv ≫ f ◁ η.hom = 𝟙 (f ≫ h)
have rw₁ : f ◁ 𝟙 h = 𝟙 (f ≫ h)
Tactic: rw [← whiskerLeft_comp, inv_hom_id, whiskerLeft_id]