-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
Goal:
B : Type u
inst : Quiver.{v, u} B
a b : FreeBicategory B
f g : a ⟶ b
η : f ⟶ 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))
        η)
have 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)
Tactic: erw [leftUnitor_inv_naturality_assoc, assoc]