-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.FunctorCategory (goal)
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
K : Type u₄
inst_4 : Category.{v₄, u₄} K
inst_5 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ F₃ F₄ : Functor.{v₃, v₂, u₃, u₂} J C
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_7 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_8 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
i j : J
f : i ⟶ j
this :
  Eq.{v₁ + 1} (α :=
    end_.{v₃, v₁, u₃, u₁} (diagram V F₂ F₃) ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₂.obj i) (F₃.obj j))
    (end_.π (diagram V F₂ F₃) i ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₂.obj i) (F₃.obj i))
          (tensorUnit.{v₁, u₁} V (𝒞 := inst)))
        (Iso.inv (ρ_ (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₂.obj i) (F₃.obj i))))
        (CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₂.obj i) (F₃.obj i))
            (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₃.obj i) (F₃.obj j)))
          (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₂.obj i) (F₃.obj i) ◁
            (eHomEquiv V : (a : F₃.obj i ⟶ F₃.obj j) → 𝟙_ V ⟶ F₃.obj i ⟶[V] F₃.obj j) (F₃.map f))
          (eComp V (F₂.obj i) (F₃.obj i) (F₃.obj j))))
    (end_.π (diagram V F₂ F₃) j ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} V (𝒞 := inst))
          (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₂.obj j) (F₃.obj j)))
        (Iso.inv (λ_ (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₂.obj j) (F₃.obj j))))
        (CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₂.obj i) (F₂.obj j))
            (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₂.obj j) (F₃.obj j)))
          ((eHomEquiv V : (a : F₂.obj i ⟶ F₂.obj j) → 𝟙_ V ⟶ F₂.obj i ⟶[V] F₂.obj j) (F₂.map f) ▷
            @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₂.obj j) (F₃.obj j))
          (eComp V (F₂.obj i) (F₂.obj j) (F₃.obj j))))
conv_rhs :
  Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
        (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃) ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₃.obj j))
    (end_.π (diagram V F₁ F₂) i ▷ enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃ ≫
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj i) ◁ end_.π (diagram V F₂ F₃) i ≫
        eComp V (F₁.obj i) (F₂.obj i) (F₃.obj i) ≫
          CategoryStruct.comp (Y :=
            tensorObj.{v₁, u₁} (𝒞 := inst) (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₃.obj i))
              (tensorUnit.{v₁, u₁} V (𝒞 := inst)))
            (Iso.inv (ρ_ (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₃.obj i))))
            (CategoryStruct.comp (Y :=
              tensorObj.{v₁, u₁} (𝒞 := inst)
                (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₃.obj i))
                (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₃.obj i) (F₃.obj j)))
              (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₃.obj i) ◁
                (eHomEquiv V : (a : F₃.obj i ⟶ F₃.obj j) → 𝟙_ V ⟶ F₃.obj i ⟶[V] F₃.obj j) (F₃.map f))
              (eComp V (F₁.obj i) (F₃.obj i) (F₃.obj j))))
    ((end_.π (diagram V F₁ F₂) i ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst)
          (tensorObj.{v₁, u₁} (𝒞 := inst) (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj i))
            (tensorUnit.{v₁, u₁} V (𝒞 := inst)))
          (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₂.obj j) (F₃.obj j)))
        (Iso.inv (ρ_ (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj i))) ▷
          @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₂.obj j) (F₃.obj j))
        (CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst)
            (tensorObj.{v₁, u₁} (𝒞 := inst) (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj i))
              (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₂.obj i) (F₂.obj j)))
            (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₂.obj j) (F₃.obj j)))
          ((@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj i) ◁
              (eHomEquiv V : (a : F₂.obj i ⟶ F₂.obj j) → 𝟙_ V ⟶ F₂.obj i ⟶[V] F₂.obj j) (F₂.map f)) ▷
            @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₂.obj j) (F₃.obj j))
          (eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j) ▷
              @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₂.obj j) (F₃.obj j) ≫
            eComp V (F₁.obj i) (F₂.obj j) (F₃.obj j))))
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
        (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃) ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₃.obj j))
    (end_.π (diagram V F₁ F₂) i ▷ enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃ ≫
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj i) ◁ end_.π (diagram V F₂ F₃) i ≫
        eComp V (F₁.obj i) (F₂.obj i) (F₃.obj i) ≫
          CategoryStruct.comp (Y :=
            tensorObj.{v₁, u₁} (𝒞 := inst) (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₃.obj i))
              (tensorUnit.{v₁, u₁} V (𝒞 := inst)))
            (Iso.inv (ρ_ (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₃.obj i))))
            (CategoryStruct.comp (Y :=
              tensorObj.{v₁, u₁} (𝒞 := inst)
                (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₃.obj i))
                (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₃.obj i) (F₃.obj j)))
              (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₃.obj i) ◁
                (eHomEquiv V : (a : F₃.obj i ⟶ F₃.obj j) → 𝟙_ V ⟶ F₃.obj i ⟶[V] F₃.obj j) (F₃.map f))
              (eComp V (F₁.obj i) (F₃.obj i) (F₃.obj j))))
    ((end_.π (diagram V F₁ F₂) i ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst)
          (tensorObj.{v₁, u₁} (𝒞 := inst) (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj i))
            (tensorUnit.{v₁, u₁} V (𝒞 := inst)))
          (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₂.obj j) (F₃.obj j)))
        (Iso.inv (ρ_ (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj i))) ▷
          @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₂.obj j) (F₃.obj j))
        (CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst)
            (tensorObj.{v₁, u₁} (𝒞 := inst) (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj i))
              (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₂.obj i) (F₂.obj j)))
            (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₂.obj j) (F₃.obj j)))
          ((@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj i) ◁
              (eHomEquiv V : (a : F₂.obj i ⟶ F₂.obj j) → 𝟙_ V ⟶ F₂.obj i ⟶[V] F₂.obj j) (F₂.map f)) ▷
            @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₂.obj j) (F₃.obj j))
          (eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j) ▷
              @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₂.obj j) (F₃.obj j) ≫
            eComp V (F₁.obj i) (F₂.obj j) (F₃.obj j))))
have conv_rhs₁ : Eq.{v₁ + 1} (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
      (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃) ⟶
    @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₃.obj j))
  (end_.π (diagram V F₁ F₂) i ▷ enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃ ≫
    @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj i) ◁ end_.π (diagram V F₂ F₃) i ≫
      eComp V (F₁.obj i) (F₂.obj i) (F₃.obj i) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₃.obj i))
            (tensorUnit.{v₁, u₁} V (𝒞 := inst)))
          (Iso.inv (ρ_ (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₃.obj i))))
          (CategoryStruct.comp (Y :=
            tensorObj.{v₁, u₁} (𝒞 := inst) (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₃.obj i))
              (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₃.obj i) (F₃.obj j)))
            (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₃.obj i) ◁
              (eHomEquiv V : (a : F₃.obj i ⟶ F₃.obj j) → 𝟙_ V ⟶ F₃.obj i ⟶[V] F₃.obj j) (F₃.map f))
            (eComp V (F₁.obj i) (F₃.obj i) (F₃.obj j))))
  (end_.π (diagram V F₁ F₂) i ▷ enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃ ≫
    @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj i) ◁ end_.π (diagram V F₂ F₃) i ≫
      eComp V (F₁.obj i) (F₂.obj i) (F₃.obj i) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₃.obj i))
            (tensorUnit.{v₁, u₁} V (𝒞 := inst)))
          (Iso.inv (ρ_ (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₃.obj i))))
          (CategoryStruct.comp (Y :=
            tensorObj.{v₁, u₁} (𝒞 := inst) (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₃.obj i))
              (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₃.obj i) (F₃.obj j)))
            (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₃.obj i) ◁
              (eHomEquiv V : (a : F₃.obj i ⟶ F₃.obj j) → 𝟙_ V ⟶ F₃.obj i ⟶[V] F₃.obj j) (F₃.map f))
            (eComp V (F₁.obj i) (F₃.obj i) (F₃.obj j))))
Tactic: conv_rhs =>
        rw [tensorHom_def_assoc, whisker_assoc_assoc, e_assoc,
          triangle_assoc_comp_right_inv_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc,
          ← MonoidalCategory.whiskerLeft_comp_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc,
          assoc, assoc, ← this, MonoidalCategory.whiskerLeft_comp_assoc,
          MonoidalCategory.whiskerLeft_comp_assoc, MonoidalCategory.whiskerLeft_comp_assoc,
          ← e_assoc, whiskerLeft_rightUnitor_inv_assoc, associator_inv_naturality_right_assoc,
          Iso.hom_inv_id_assoc, whisker_exchange_assoc, MonoidalCategory.whiskerRight_id_assoc,
          Iso.inv_hom_id_assoc]