-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X Y Z : C
rw :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
    (F.map (Iso.hom (α_ X Y Z)) ≫ F.map (Iso.inv (α_ X Y Z)))
    (F.map (Iso.hom (α_ X Y Z)) ≫
      CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
        (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
        (F.obj X ◁ δ F Y Z ≫
          Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
rw₁ :
  𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)) =
    F.map (Iso.hom (α_ X Y Z)) ≫
      CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
        (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
        (F.obj X ◁ δ F Y Z ≫
          Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
rw₂ :
  𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)) =
    CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
      (CategoryStruct.comp (Y :=
        tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
        (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
        (δ F X Y ▷ F.obj Z ≫
          Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ F.obj X ◁ μ F Y Z ≫ μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
      (CategoryStruct.comp (Y :=
        tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
        (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
        (F.obj X ◁ δ F Y Z ≫
          Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
rw₃ :
  𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)) =
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
      (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
      (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
        (δ F X Y ▷ F.obj Z ≫
          Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ F.obj X ◁ μ F Y Z ≫ μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
        (CategoryStruct.comp (Y :=
          tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
          (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
          (F.obj X ◁ δ F Y Z ≫
            Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫
              μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)))
rw₄ :
  𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)) =
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
      (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
      (δ F X Y ▷ F.obj Z ≫
        CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
          (Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ F.obj X ◁ μ F Y Z ≫ μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
          (CategoryStruct.comp (Y :=
            tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
            (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
            (F.obj X ◁ δ F Y Z ≫
              Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫
                μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)))
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
    (F.map (Iso.inv (α_ X Y Z)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
      (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
      (F.obj X ◁ δ F Y Z ≫
        Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
have rw₅ : 𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)) =
  CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
    (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
    (δ F X Y ▷ F.obj Z ≫
      Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫
        CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
          (F.obj X ◁ μ F Y Z ≫ μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
          (CategoryStruct.comp (Y :=
            tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
            (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
            (F.obj X ◁ δ F Y Z ≫
              Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫
                μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)))
Tactic: rw [← cancel_epi (F.map (α_ X Y Z).hom), Iso.map_hom_inv_id, map_associator,
    assoc, assoc, assoc, assoc, OplaxMonoidal.associativity_inv_assoc,
    whiskerRight_δ_μ_assoc, δ_μ, comp_id, LaxMonoidal.associativity_inv,
    Iso.hom_inv_id_assoc, whiskerRight_δ_μ_assoc, δ_μ]