-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Monad.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a : B
F : OplaxFunctor.{0, w, 0, v, 0, u} (LocallyDiscrete (Discrete Unit)) B
⊢ (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 := () } })))
have 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
Tactic: simp only [tensorObj_def, MonoidalCategory.whiskerLeft_comp, whiskerLeft_def, Category.assoc,
      MonoidalCategory.comp_whiskerRight, whiskerRight_def, associator_def]