-- 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 : C
f : X ⟶ Y
X' : C
rw :
  Eq (α :=
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X')) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj Y)) (G.obj (F.obj X')))
    (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.map (F.map f) ▷ G.obj (F.obj X')))
    (G.map (F.map (f ▷ X')) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X'))) (G.map (δ F Y X'))
        (δ G (F.obj Y) (F.obj X')))
rw₁ :
  Eq (α :=
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X')) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj Y)) (G.obj (F.obj X')))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj X'))) (G.map (δ F X X'))
      (G.map (F.map f ▷ F.obj X') ≫ δ G (F.obj Y) (F.obj X')))
    (G.map (F.map (f ▷ X')) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X'))) (G.map (δ F Y X'))
        (δ G (F.obj Y) (F.obj X')))
rw₂ :
  Eq (α :=
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X')) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj Y)) (G.obj (F.obj X')))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X')))
      (G.map (δ F X X' ≫ F.map f ▷ F.obj X')) (δ G (F.obj Y) (F.obj X')))
    (G.map (F.map (f ▷ X')) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X'))) (G.map (δ F Y X'))
        (δ G (F.obj Y) (F.obj X')))
rw₃ :
  Eq (α :=
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X')) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj Y)) (G.obj (F.obj X')))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X')))
      (G.map (F.map (f ▷ X') ≫ δ F Y X')) (δ G (F.obj Y) (F.obj X')))
    (G.map (F.map (f ▷ X')) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X'))) (G.map (δ F Y X'))
        (δ G (F.obj Y) (F.obj X')))
⊢ Eq (α :=
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X')) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj Y)) (G.obj (F.obj X')))
    (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.map (F.map f) ▷ G.obj (F.obj X'))
    (G.map (F.map (f ▷ X')) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X'))) (G.map (δ F Y X'))
        (δ G (F.obj Y) (F.obj X')))
have rw₄ : Eq (α :=
  G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X')) ⟶
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj Y)) (G.obj (F.obj X')))
  (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X')))
    (G.map (F.map (f ▷ X')) ≫ G.map (δ F Y X')) (δ G (F.obj Y) (F.obj X')))
  (G.map (F.map (f ▷ X')) ≫
    CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X'))) (G.map (δ F Y X'))
      (δ G (F.obj Y) (F.obj X')))
Tactic: rw [assoc, δ_natural_left, ← G.map_comp_assoc, δ_natural_left, map_comp, assoc]