-- 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
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_7 : F.OplaxMonoidal
inst_8 : G.OplaxMonoidal
X Y x : C
x_1 : X ⟶ Y
rw :
  Eq (α :=
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x X)) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj Y)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (G.map (δ F x X))
      (δ G (F.obj x) (F.obj X) ≫ G.obj (F.obj x) ◁ G.map (F.map x_1)))
    (G.map (F.map (x ◁ x_1)) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (G.map (δ F x Y))
        (δ G (F.obj x) (F.obj Y)))
rw₁ :
  Eq (α :=
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x X)) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj Y)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (G.map (δ F x X))
      (G.map (F.obj x ◁ F.map x_1) ≫ δ G (F.obj x) (F.obj Y)))
    (G.map (F.map (x ◁ x_1)) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (G.map (δ F x Y))
        (δ G (F.obj x) (F.obj Y)))
rw₂ :
  Eq (α :=
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x X)) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj Y)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y)))
      (G.map (δ F x X ≫ F.obj x ◁ F.map x_1)) (δ G (F.obj x) (F.obj Y)))
    (G.map (F.map (x ◁ x_1)) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (G.map (δ F x Y))
        (δ G (F.obj x) (F.obj Y)))
rw₃ :
  Eq (α :=
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x X)) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj Y)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y)))
      (G.map (F.map (x ◁ x_1) ≫ δ F x Y)) (δ G (F.obj x) (F.obj Y)))
    (G.map (F.map (x ◁ x_1)) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (G.map (δ F x Y))
        (δ G (F.obj x) (F.obj Y)))
⊢ Eq (α :=
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x X)) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj Y)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (G.map (δ F x X))
        (δ G (F.obj x) (F.obj X)) ≫
      G.obj (F.obj x) ◁ G.map (F.map x_1))
    (G.map (F.map (x ◁ x_1)) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (G.map (δ F x Y))
        (δ G (F.obj x) (F.obj Y)))
have rw₄ : Eq (α :=
  G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x X)) ⟶
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj Y)))
  (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y)))
    (G.map (F.map (x ◁ x_1)) ≫ G.map (δ F x Y)) (δ G (F.obj x) (F.obj Y)))
  (G.map (F.map (x ◁ x_1)) ≫
    CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (G.map (δ F x Y))
      (δ G (F.obj x) (F.obj Y)))
Tactic: rw [assoc, δ_natural_right, ← G.map_comp_assoc, δ_natural_right, map_comp, assoc]