-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b : FreeBicategory B
f g : a ⟶ b
η : f ⟶ g
e_a :
  Eq (α :=
    Quiver.Hom (V := a ⟶ b) (𝟙 a ≫ 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)) g) (𝟙 a ◁ Functor.map (𝟭 (a ⟶ b)) η)
        (Iso.hom (normalizeIso nil g)) :
      Quiver.Hom (V := a ⟶ b) (𝟙 a ≫ 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))
    (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))
⊢ 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)

Tactic:
congr 1