-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Basic (goal)
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C
D : Type u₂
inst_3 : EnrichedCategory.{w, v, u₂} V D
inst_4 : BraidedCategory.{w, v} V
F G : EnrichedFunctor.{w, v, u₁, u₂} V C D
X_1 Y_1 : Vᵒᵖ
f : X_1 ⟶ Y_1
σ : GradedNatTrans (Functor.obj (Center.ofBraided V) (unop X_1)) F G
X Y : C
p :
  Iso.hom (β_ (unop X_1) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      (F.map X Y ⊗ₘ σ.app Y) ≫ eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
rw :
  Iso.hom (β_ (unop Y_1) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      ((𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ⊗ₘ f.unop ≫ σ.app Y) ≫
          (F.map X Y ⊗ₘ 𝟙 (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (F.obj Y) (G.obj Y)))) ≫
        eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (f.unop ≫ σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
rw₁ :
  Iso.hom (β_ (unop Y_1) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      (((𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ⊗ₘ f.unop) ≫
            (𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ⊗ₘ σ.app Y)) ≫
          (F.map X Y ⊗ₘ 𝟙 (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (F.obj Y) (G.obj Y)))) ≫
        eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (f.unop ≫ σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
rw₂ :
  Iso.hom (β_ (unop Y_1) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      ((𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ⊗ₘ f.unop) ≫
          (𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ⊗ₘ σ.app Y)) ≫
        (F.map X Y ⊗ₘ 𝟙 (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (F.obj Y) (G.obj Y))) ≫
          eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (f.unop ≫ σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
rw₃ :
  Iso.hom (β_ (unop Y_1) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      (𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ⊗ₘ f.unop) ≫
        (𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ⊗ₘ σ.app Y) ≫
          (F.map X Y ⊗ₘ 𝟙 (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (F.obj Y) (G.obj Y))) ≫
            eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (f.unop ≫ σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
rw₄ :
  (f.unop ⊗ₘ 𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      Iso.hom (β_ (unop X_1) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
        (𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ⊗ₘ σ.app Y) ≫
          (F.map X Y ⊗ₘ 𝟙 (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (F.obj Y) (G.obj Y))) ≫
            eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (f.unop ≫ σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
⊢ Iso.hom (β_ (unop Y_1) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      (F.map X Y ⊗ₘ f.unop ≫ σ.app Y) ≫ eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (f.unop ≫ σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
have rw₅ : (f.unop ⊗ₘ 𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
    Iso.hom (β_ (unop X_1) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      (F.map X Y ⊗ₘ σ.app Y) ≫ eComp V (F.obj X) (F.obj Y) (G.obj Y) =
  (f.unop ≫ σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
Tactic: rw [← id_tensor_comp_tensor_id (f.unop ≫ σ.app Y) _, id_tensor_comp, Category.assoc,
          Category.assoc, ← braiding_naturality_assoc, id_tensor_comp_tensor_id_assoc, p,
          tensorHom_comp_tensorHom_assoc, Category.id_comp]