-- Module: Mathlib.CategoryTheory.Bicategory.Monad.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a : B
F : OplaxFunctor.{0, w, 0, v, 0, u} (LocallyDiscrete (Discrete Unit)) B
simp :
  F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
      F.mapComp (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
          (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ≫
        F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ◁
            F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
          F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ◁
            F.mapComp (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
              (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) =
    F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
      F.mapComp (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
          (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ≫
        F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ▷
            F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ≫
          F.mapComp (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
                (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ▷
              F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ≫
            (α_ (F.map (𝟙 { as := { as := () } })) (F.map (𝟙 { as := { as := () } }))
                (F.map (𝟙 { as := { as := () } }))).hom
⊢ (F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
        F.mapComp (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
          (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })) ≫
      MonoidalCategoryStruct.whiskerLeft
        (F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }))
        (F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
          F.mapComp (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
            (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })) =
    (F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
        F.mapComp (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
          (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })) ≫
      MonoidalCategoryStruct.whiskerRight
          (F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
            F.mapComp (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
              (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }))
          (F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })) ≫
        Iso.hom
          (MonoidalCategoryStruct.associator (F.map (𝟙 { as := { as := () } })) (F.map (𝟙 { as := { as := () } }))
            (F.map (𝟙 { as := { as := () } })))

Tactic:
simp only [tensorObj_def, MonoidalCategory.whiskerLeft_comp, whiskerLeft_def, Category.assoc,
      MonoidalCategory.comp_whiskerRight, whiskerRight_def, associator_def]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.whiskerLeft_def, CategoryTheory.whiskerRight_def, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.associator_def, CategoryTheory.tensorObj_def