-- Mathlib/CategoryTheory/Monoidal/Center.lean
theorem whiskerLeft_comm (X : Center C) {Y₁ Y₂ : Center C} (f : Y₁ ⟶ Y₂) (U : C) :
    (X.1 ◁ f.f) ▷ U ≫ ((tensorObj X Y₂).2.β U).hom =
      ((tensorObj X Y₁).2.β U).hom ≫ U ◁ X.1 ◁ f.f

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y₁ Y₂ : Center C
f : Y₁ ⟶ Y₂
U : C
⊢ 𝟙 ((X.fst ⊗ Y₁.fst) ⊗ U) ⊗≫
      X.fst ◁ (Y₁.snd.β U).hom ⊗≫ ((X.snd.β U).hom ▷ Y₁.fst ≫ (U ⊗ X.fst) ◁ f.f) ⊗≫ 𝟙 (U ⊗ X.fst ⊗ Y₂.fst) =
    ((α_ X.fst Y₁.fst U).hom ≫
        X.fst ◁ (Y₁.snd.β U).hom ≫ (α_ X.fst U Y₁.fst).inv ≫ (X.snd.β U).hom ▷ Y₁.fst ≫ (α_ U X.fst Y₁.fst).hom) ≫
      U ◁ X.fst ◁ f.f

Tactic:
monoidal

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y₁ Y₂ : Center C
f : Y₁ ⟶ Y₂
U : C
⊢ (X.fst ◁ f.f) ▷ U ≫
      (α_ X.fst Y₂.fst U).hom ≫
        X.fst ◁ (Y₂.snd.β U).hom ≫ (α_ X.fst U Y₂.fst).inv ≫ (X.snd.β U).hom ▷ Y₂.fst ≫ (α_ U X.fst Y₂.fst).hom =
    𝟙 ((X.fst ⊗ Y₁.fst) ⊗ U) ⊗≫
      X.fst ◁ (f.f ▷ U ≫ (Y₂.snd.β U).hom) ⊗≫ (X.snd.β U).hom ▷ Y₂.fst ⊗≫ 𝟙 (U ⊗ X.fst ⊗ Y₂.fst)

Tactic:
monoidal

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y₁ Y₂ : Center C
f : Y₁ ⟶ Y₂
U : C
⊢ 𝟙 ((X.fst ⊗ Y₁.fst) ⊗ U) ⊗≫
      X.fst ◁ (f.f ▷ U ≫ (Y₂.snd.β U).hom) ⊗≫ (X.snd.β U).hom ▷ Y₂.fst ⊗≫ 𝟙 (U ⊗ X.fst ⊗ Y₂.fst) =
    𝟙 ((X.fst ⊗ Y₁.fst) ⊗ U) ⊗≫
      X.fst ◁ (Y₁.snd.β U).hom ⊗≫ ((X.fst ⊗ U) ◁ f.f ≫ (X.snd.β U).hom ▷ Y₂.fst) ⊗≫ 𝟙 (U ⊗ X.fst ⊗ Y₂.fst)

Tactic:
rw [f.comm]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y₁ Y₂ : Center C
f : Y₁ ⟶ Y₂
U : C
⊢ 𝟙 ((X.fst ⊗ Y₁.fst) ⊗ U) ⊗≫
      X.fst ◁ ((Y₁.snd.β U).hom ≫ U ◁ f.f) ⊗≫ (X.snd.β U).hom ▷ Y₂.fst ⊗≫ 𝟙 (U ⊗ X.fst ⊗ Y₂.fst) =
    𝟙 ((X.fst ⊗ Y₁.fst) ⊗ U) ⊗≫
      X.fst ◁ (Y₁.snd.β U).hom ⊗≫ ((X.fst ⊗ U) ◁ f.f ≫ (X.snd.β U).hom ▷ Y₂.fst) ⊗≫ 𝟙 (U ⊗ X.fst ⊗ Y₂.fst)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y₁ Y₂ : Center C
f : Y₁ ⟶ Y₂
U : C
⊢ 𝟙 ((X.fst ⊗ Y₁.fst) ⊗ U) ⊗≫
      X.fst ◁ (Y₁.snd.β U).hom ⊗≫ ((X.fst ⊗ U) ◁ f.f ≫ (X.snd.β U).hom ▷ Y₂.fst) ⊗≫ 𝟙 (U ⊗ X.fst ⊗ Y₂.fst) =
    ((α_ X.fst Y₁.fst U).hom ≫
        X.fst ◁ (Y₁.snd.β U).hom ≫ (α_ X.fst U Y₁.fst).inv ≫ (X.snd.β U).hom ▷ Y₁.fst ≫ (α_ U X.fst Y₁.fst).hom) ≫
      U ◁ X.fst ◁ f.f

Tactic:
rw [whisker_exchange]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y₁ Y₂ : Center C
f : Y₁ ⟶ Y₂
U : C
⊢ 𝟙 ((X.fst ⊗ Y₁.fst) ⊗ U) ⊗≫
      X.fst ◁ (Y₁.snd.β U).hom ⊗≫ ((X.snd.β U).hom ▷ Y₁.fst ≫ (U ⊗ X.fst) ◁ f.f) ⊗≫ 𝟙 (U ⊗ X.fst ⊗ Y₂.fst) =
    ((α_ X.fst Y₁.fst U).hom ≫
        X.fst ◁ (Y₁.snd.β U).hom ≫ (α_ X.fst U Y₁.fst).inv ≫ (X.snd.β U).hom ▷ Y₁.fst ≫ (α_ U X.fst Y₁.fst).hom) ≫
      U ◁ X.fst ◁ f.f

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y₁ Y₂ : Center C
f : Y₁ ⟶ Y₂
U : C
⊢ (X.fst ◁ f.f) ▷ U ≫ ((X.tensorObj Y₂).snd.β U).hom = ((X.tensorObj Y₁).snd.β U).hom ≫ U ◁ X.fst ◁ f.f

Tactic:
dsimp only [tensorObj_fst, tensorObj_snd_β, Iso.trans_hom, whiskerLeftIso_hom,
  Iso.symm_hom, whiskerRightIso_hom]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y₁ Y₂ : Center C
f : Y₁ ⟶ Y₂
U : C
⊢ (X.fst ◁ f.f) ▷ U ≫
      (α_ X.fst Y₂.fst U).hom ≫
        X.fst ◁ (Y₂.snd.β U).hom ≫ (α_ X.fst U Y₂.fst).inv ≫ (X.snd.β U).hom ▷ Y₂.fst ≫ (α_ U X.fst Y₂.fst).hom =
    ((α_ X.fst Y₁.fst U).hom ≫
        X.fst ◁ (Y₁.snd.β U).hom ≫ (α_ X.fst U Y₁.fst).inv ≫ (X.snd.β U).hom ▷ Y₁.fst ≫ (α_ U X.fst Y₁.fst).hom) ≫
      U ◁ X.fst ◁ f.f

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y₁ Y₂ : Center C
f : Y₁ ⟶ Y₂
U : C
⊢ (X.fst ◁ f.f) ▷ U ≫
      (α_ X.fst Y₂.fst U).hom ≫
        X.fst ◁ (Y₂.snd.β U).hom ≫ (α_ X.fst U Y₂.fst).inv ≫ (X.snd.β U).hom ▷ Y₂.fst ≫ (α_ U X.fst Y₂.fst).hom =
    ((α_ X.fst Y₁.fst U).hom ≫
        X.fst ◁ (Y₁.snd.β U).hom ≫ (α_ X.fst U Y₁.fst).inv ≫ (X.snd.β U).hom ▷ Y₁.fst ≫ (α_ U X.fst Y₁.fst).hom) ≫
      U ◁ X.fst ◁ f.f

Tactic:
calc
  _ = 𝟙 _ ⊗≫
    X.fst ◁ (f.f ▷ U ≫ (HalfBraiding.β Y₂.snd U).hom) ⊗≫
      (HalfBraiding.β X.snd U).hom ▷ Y₂.fst ⊗≫ 𝟙 _ := by monoidal
  _ = 𝟙 _ ⊗≫
    X.fst ◁ (HalfBraiding.β Y₁.snd U).hom ⊗≫
      ((X.fst ⊗ U) ◁ f.f ≫ (HalfBraiding.β X.snd U).hom ▷ Y₂.fst) ⊗≫ 𝟙 _ := by
    rw [f.comm]; monoidal
  _ = _ := by rw [whisker_exchange]; monoidal

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y₁ Y₂ : Center C
f : Y₁ ⟶ Y₂
U : C
⊢ 𝟙 ((X.fst ⊗ Y₁.fst) ⊗ U) ⊗≫
      X.fst ◁ ((Y₁.snd.β U).hom ≫ U ◁ f.f) ⊗≫ (X.snd.β U).hom ▷ Y₂.fst ⊗≫ 𝟙 (U ⊗ X.fst ⊗ Y₂.fst) =
    𝟙 ((X.fst ⊗ Y₁.fst) ⊗ U) ⊗≫
      X.fst ◁ (Y₁.snd.β U).hom ⊗≫ ((X.fst ⊗ U) ◁ f.f ≫ (X.snd.β U).hom ▷ Y₂.fst) ⊗≫ 𝟙 (U ⊗ X.fst ⊗ Y₂.fst)

Tactic:
monoidal

Result:
no goals