-- 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.LaxMonoidal
X : C
rw :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (ε F ▷ F.obj X ≫ μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) (Iso.hom (λ_ (F.obj X)) ≫ F.map (Iso.inv (λ_ X)))
rw₁ :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (ε F ▷ F.obj X ≫ μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X))
        (ε F ▷ F.obj X) (μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X))) ≫
      F.map (Iso.inv (λ_ X)))
rw₂ :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (ε F ▷ F.obj X ≫ μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X))
      (ε F ▷ F.obj X) ((μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X))) ≫ F.map (Iso.inv (λ_ X))))
rw₃ :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (ε F ▷ F.obj X ≫ μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X))
      (ε F ▷ F.obj X) (μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X)) ≫ F.map (Iso.inv (λ_ X))))
rw₄ :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (ε F ▷ F.obj X ≫ μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X))
      (ε F ▷ F.obj X) (μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X) ≫ Iso.inv (λ_ X))))
⊢ Eq (α := F.obj X ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X))
      (Iso.inv (λ_ (F.obj X))) (ε F ▷ F.obj X ≫ μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (F.map (Iso.inv (λ_ X)))
have rw₅ : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X) ⟶
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
  (ε F ▷ F.obj X ≫ μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
  (ε F ▷ F.obj X ≫
    μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫
      F.map (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)))
Tactic: rw [Iso.inv_comp_eq, left_unitality, Category.assoc, Category.assoc, ← F.map_comp,
    Iso.hom_inv_id, F.map_id, comp_id]