-- 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)
    (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)
have 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))
Tactic: congr 1