-- 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.LaxMonoidal
inst_8 : G.LaxMonoidal
x x_1 x_2 : C
simp_rw :
  Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj x_1)))
        (G.obj (F.obj x_2)) ⟶
      G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
    (CategoryStruct.comp (Y :=
        tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1)))
          (G.obj (F.obj x_2)))
        (μ G (F.obj x) (F.obj x_1) ▷ G.obj (F.obj x_2)) (G.map (μ F x x_1) ▷ G.obj (F.obj x_2)) ≫
      CategoryStruct.comp (Y :=
          G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (F.obj x_2)))
          (μ G (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (F.obj x_2))
          (G.map (μ F (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) x_2)) ≫
        G.map (F.map (Iso.hom (α_ x x_1 x_2))))
    (Iso.hom (α_ (G.obj (F.obj x)) (G.obj (F.obj x_1)) (G.obj (F.obj x_2))) ≫
      G.obj (F.obj x) ◁
          CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2)))
            (μ G (F.obj x_1) (F.obj x_2)) (G.map (μ F x_1 x_2)) ≫
        CategoryStruct.comp (Y :=
          G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
          (μ G (F.obj x) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2)))
          (G.map (μ F x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
⊢ Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj x_1)))
        (G.obj (F.obj x_2)) ⟶
      G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1)))
          (μ G (F.obj x) (F.obj x_1)) (G.map (μ F x x_1)) ▷
        G.obj (F.obj x_2) ≫
      CategoryStruct.comp (Y :=
          G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (F.obj x_2)))
          (μ G (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (F.obj x_2))
          (G.map (μ F (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) x_2)) ≫
        G.map (F.map (Iso.hom (α_ x x_1 x_2))))
    (Iso.hom (α_ (G.obj (F.obj x)) (G.obj (F.obj x_1)) (G.obj (F.obj x_2))) ≫
      G.obj (F.obj x) ◁
          CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2)))
            (μ G (F.obj x_1) (F.obj x_2)) (G.map (μ F x_1 x_2)) ≫
        CategoryStruct.comp (Y :=
          G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
          (μ G (F.obj x) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2)))
          (G.map (μ F x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
have simp_rw₁ : Eq (α :=
  tensorObj.{v₃, u₃} (𝒞 := inst_4) (tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj x_1)))
      (G.obj (F.obj x_2)) ⟶
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
  (CategoryStruct.comp (Y :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1)))
      (G.obj (F.obj x_2)))
    (μ G (F.obj x) (F.obj x_1) ▷ G.obj (F.obj x_2))
    (G.map (μ F x x_1) ▷ G.obj (F.obj x_2) ≫
      CategoryStruct.comp (Y :=
        G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (F.obj x_2)))
        (μ G (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (F.obj x_2))
        (G.map (μ F (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) x_2) ≫ G.map (F.map (Iso.hom (α_ x x_1 x_2))))))
  (Iso.hom (α_ (G.obj (F.obj x)) (G.obj (F.obj x_1)) (G.obj (F.obj x_2))) ≫
    G.obj (F.obj x) ◁
        CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2)))
          (μ G (F.obj x_1) (F.obj x_2)) (G.map (μ F x_1 x_2)) ≫
      CategoryStruct.comp (Y :=
        G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
        (μ G (F.obj x) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2)))
        (G.map (μ F x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
Tactic: simp_rw [comp_whiskerRight, assoc, μ_natural_left_assoc, MonoidalCategory.whiskerLeft_comp,
      assoc, μ_natural_right_assoc, ← associativity_assoc, ← G.map_comp, associativity]