-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Center (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : Center.{v₁, u₁} C
U U' : C
⊢ (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
          (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) U U') ≪≫
        X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ᵢ
            Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β
              (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) U U') ≪≫
          Iso.symm
              (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) U U')
                (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≪≫
            X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β
                  (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) U U') ▷ᵢ
                Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≪≫
              α_ (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) U U')
                (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))).hom =
    Iso.inv
        (α_
          (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
            (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))
          U U') ≫
      (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U ≪≫
              X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ᵢ
                  Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U ≪≫
                Iso.symm
                    (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U
                      (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≪≫
                  X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U ▷ᵢ
                      Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≪≫
                    α_ U (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                      (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))).hom ▷
          U' ≫
        Iso.hom
            (α_ U
              (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst)
                (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))
              U') ≫
          U ◁
              (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                    (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U' ≪≫
                  X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ᵢ
                      Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U' ≪≫
                    Iso.symm
                        (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U'
                          (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≪≫
                      X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U' ▷ᵢ
                          Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≪≫
                        α_ U' (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                          (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))).hom ≫
            Iso.inv
              (α_ U U'
                (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst)
                  (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                  (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))))
have dsimp : Iso.hom
      (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
        (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) U U')) ≫
    X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁
        Iso.hom
          (Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β
            (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) U U')) ≫
      Iso.inv
          (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
            (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) U U')
            (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≫
        Iso.hom
              (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β
                (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) U U')) ▷
            Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
          Iso.hom
            (α_ (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) U U')
              (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
              (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) =
  Iso.inv
      (α_
        (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
          (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))
        U U') ≫
    (Iso.hom
            (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
              (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U) ≫
          X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁
              (Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
            Iso.inv
                (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U
                  (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≫
              (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ▷
                  Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
                Iso.hom
                  (α_ U (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                    (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))) ▷
        U' ≫
      Iso.hom
          (α_ U
            (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
              (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))
            U') ≫
        U ◁
            (Iso.hom
                (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                  (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U') ≫
              X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁
                  (Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U').hom ≫
                Iso.inv
                    (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U'
                      (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≫
                  (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U').hom ▷
                      Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
                    Iso.hom
                      (α_ U' (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                        (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))) ≫
          Iso.inv
            (α_ U U'
              (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst)
                (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))))
Tactic: dsimp only [Iso.trans_hom, whiskerLeftIso_hom, Iso.symm_hom, whiskerRightIso_hom]