-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b : FreeBicategory B
f g : a ⟶ b
η : f ⟶ g
erw :
  Eq (α :=
    Functor.obj (𝟭 (a ⟶ b)) f ⟶
      Functor.obj
        (Functor.comp (D :=
          Prefunctor.obj
              (PrelaxFunctorStruct.toPrefunctor
                (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
              a ⟶
            Prefunctor.obj
              (PrelaxFunctorStruct.toPrefunctor
                (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
              b)
          (PrelaxFunctor.mapFunctor (Pseudofunctor.toPrelaxFunctor (normalize B)) a b) (inclusionPath a b))
        g)
    (CategoryStruct.comp (Y := 𝟙 a ≫ Functor.obj (𝟭 (a ⟶ b)) f) (Iso.inv (λ_ (Functor.obj (𝟭 (a ⟶ b)) f)))
        (CategoryStruct.comp (Y := 𝟙 a ≫ Functor.obj (𝟭 (a ⟶ b)) g) (𝟙 a ◁ Functor.map (𝟭 (a ⟶ b)) η)
          (Iso.hom (normalizeIso nil g))) :
      Functor.obj (𝟭 (a ⟶ b)) f ⟶
        Functor.obj
          (Functor.comp (D :=
            Prefunctor.obj
                (PrelaxFunctorStruct.toPrefunctor
                  (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
                a ⟶
              Prefunctor.obj
                (PrelaxFunctorStruct.toPrefunctor
                  (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
                b)
            (PrelaxFunctor.mapFunctor (Pseudofunctor.toPrelaxFunctor (normalize B)) a b) (inclusionPath a b))
          g)
    (CategoryStruct.comp (Y := 𝟙 a ≫ f) (Iso.hom (Iso.symm (λ_ f)) : Functor.obj (𝟭 (a ⟶ b)) f ⟶ 𝟙 a ≫ f)
        (Iso.hom (normalizeIso nil f) ≫
            Functor.map
              (Functor.comp (D :=
                Prefunctor.obj
                    (PrelaxFunctorStruct.toPrefunctor
                      (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
                    a ⟶
                  Prefunctor.obj
                    (PrelaxFunctorStruct.toPrefunctor
                      (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
                    b)
                (PrelaxFunctor.mapFunctor (Pseudofunctor.toPrelaxFunctor (normalize B)) a b) (inclusionPath a b))
              η :
          Quiver.Hom (V := a ⟶ b) (𝟙 a ≫ f : a ⟶ b)
            (Functor.obj
              (Functor.comp (D :=
                Prefunctor.obj
                    (PrelaxFunctorStruct.toPrefunctor
                      (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
                    a ⟶
                  Prefunctor.obj
                    (PrelaxFunctorStruct.toPrefunctor
                      (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
                    b)
                (PrelaxFunctor.mapFunctor (Pseudofunctor.toPrelaxFunctor (normalize B)) a b) (inclusionPath a b))
              g)) :
      Functor.obj (𝟭 (a ⟶ b)) f ⟶
        Functor.obj
          (Functor.comp (D :=
            Prefunctor.obj
                (PrelaxFunctorStruct.toPrefunctor
                  (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
                a ⟶
              Prefunctor.obj
                (PrelaxFunctorStruct.toPrefunctor
                  (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
                b)
            (PrelaxFunctor.mapFunctor (Pseudofunctor.toPrelaxFunctor (normalize B)) a b) (inclusionPath a b))
          g)
⊢ Eq (α :=
    Functor.obj (𝟭 (a ⟶ b)) f ⟶
      Functor.obj
        (Functor.comp (D :=
          Prefunctor.obj
              (PrelaxFunctorStruct.toPrefunctor
                (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
              a ⟶
            Prefunctor.obj
              (PrelaxFunctorStruct.toPrefunctor
                (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
              b)
          (PrelaxFunctor.mapFunctor (Pseudofunctor.toPrelaxFunctor (normalize B)) a b) (inclusionPath a b))
        g)
    (Functor.map (𝟭 (a ⟶ b)) η ≫
      Iso.hom
        ((fun (f : a ⟶ b) ↦
            (Iso.symm (λ_ f) ≪≫ normalizeIso nil f :
              Functor.obj (𝟭 (a ⟶ b)) f ≅
                Functor.obj
                  (Functor.comp (D :=
                    Prefunctor.obj
                        (PrelaxFunctorStruct.toPrefunctor
                          (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
                        a ⟶
                      Prefunctor.obj
                        (PrelaxFunctorStruct.toPrefunctor
                          (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
                        b)
                    (PrelaxFunctor.mapFunctor (Pseudofunctor.toPrelaxFunctor (normalize B)) a b) (inclusionPath a b))
                  f))
          g))
    (Iso.hom
        ((fun (f : a ⟶ b) ↦
            (Iso.symm (λ_ f) ≪≫ normalizeIso nil f :
              Functor.obj (𝟭 (a ⟶ b)) f ≅
                Functor.obj
                  (Functor.comp (D :=
                    Prefunctor.obj
                        (PrelaxFunctorStruct.toPrefunctor
                          (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
                        a ⟶
                      Prefunctor.obj
                        (PrelaxFunctorStruct.toPrefunctor
                          (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
                        b)
                    (PrelaxFunctor.mapFunctor (Pseudofunctor.toPrelaxFunctor (normalize B)) a b) (inclusionPath a b))
                  f))
          f) ≫
      Functor.map
        (Functor.comp (D :=
          Prefunctor.obj
              (PrelaxFunctorStruct.toPrefunctor
                (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
              a ⟶
            Prefunctor.obj
              (PrelaxFunctorStruct.toPrefunctor
                (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
              b)
          (PrelaxFunctor.mapFunctor (Pseudofunctor.toPrelaxFunctor (normalize B)) a b) (inclusionPath a b))
        η)

Tactic:
erw [leftUnitor_inv_naturality_assoc, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Bicategory.leftUnitor_inv_naturality_assoc