-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.NaturalTransformation (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
E' : Type u₄
inst_6 : Category.{v₄, u₄} E'
inst_7 : MonoidalCategory.{v₄, u₄} E'
F₁ F₂ F₃ : Functor.{v₁, v₂, u₁, u₂} C D
τ : F₁ ⟶ F₂
inst_8 : F₁.LaxMonoidal
inst_9 : F₂.LaxMonoidal
inst_10 : F₃.LaxMonoidal
e : F₁ ≅ F₂
inst_11 : NatTrans.IsMonoidal e.hom
X Y : C
rw :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₂.obj X) (F₂.obj Y) ⟶ F₂.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    ((LaxMonoidal.μ F₂ X Y ≫ e.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ≫
      e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (((e.inv.app X ⊗ₘ e.inv.app Y) ≫ LaxMonoidal.μ F₁ X Y) ≫ e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
rw₁ :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₂.obj X) (F₂.obj Y) ⟶ F₂.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (LaxMonoidal.μ F₂ X Y ≫
      e.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫ e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (((e.inv.app X ⊗ₘ e.inv.app Y) ≫ LaxMonoidal.μ F₁ X Y) ≫ e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
rw₂ :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₂.obj X) (F₂.obj Y) ⟶ F₂.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (LaxMonoidal.μ F₂ X Y ≫
      e.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫ e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    ((e.inv.app X ⊗ₘ e.inv.app Y) ≫ LaxMonoidal.μ F₁ X Y ≫ e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
rw₃ :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₂.obj X) (F₂.obj Y) ⟶ F₂.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (LaxMonoidal.μ F₂ X Y ≫ 𝟙 (F₂.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
    ((e.inv.app X ⊗ₘ e.inv.app Y) ≫ LaxMonoidal.μ F₁ X Y ≫ e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
rw₄ :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₂.obj X) (F₂.obj Y) ⟶ F₂.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (LaxMonoidal.μ F₂ X Y)
    ((e.inv.app X ⊗ₘ e.inv.app Y) ≫ LaxMonoidal.μ F₁ X Y ≫ e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
rw₅ :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₂.obj X) (F₂.obj Y) ⟶ F₂.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (LaxMonoidal.μ F₂ X Y) ((e.inv.app X ⊗ₘ e.inv.app Y) ≫ (e.hom.app X ⊗ₘ e.hom.app Y) ≫ LaxMonoidal.μ F₂ X Y)
rw₆ :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₂.obj X) (F₂.obj Y) ⟶ F₂.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (LaxMonoidal.μ F₂ X Y) ((e.inv.app X ≫ e.hom.app X ⊗ₘ e.inv.app Y ≫ e.hom.app Y) ≫ LaxMonoidal.μ F₂ X Y)
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₂.obj X) (F₂.obj Y) ⟶ F₁.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (LaxMonoidal.μ F₂ X Y ≫ e.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    ((e.inv.app X ⊗ₘ e.inv.app Y) ≫ LaxMonoidal.μ F₁ X Y)
have rw₇ : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₂.obj X) (F₂.obj Y) ⟶ F₂.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
  (LaxMonoidal.μ F₂ X Y) ((𝟙 (F₂.obj X) ⊗ₘ e.inv.app Y ≫ e.hom.app Y) ≫ LaxMonoidal.μ F₂ X Y)
Tactic: rw [← cancel_mono (e.hom.app (X ⊗ Y)), assoc, assoc, inv_hom_id_app, comp_id,
      NatTrans.IsMonoidal.tensor, MonoidalCategory.tensorHom_comp_tensorHom_assoc,
      inv_hom_id_app, inv_hom_id_app, tensorHom_id, id_whiskerRight, id_comp]