-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f g : Hom.{v, u} b c
a_1 b_1 c_1 : FreeBicategory B
f_1 g_1 : a_1 ⟶ b_1
h : b_1 ⟶ c_1
η' : Hom₂ f_1 g_1
ih :
  ∀ (p : Path.{v, u} a a_1),
    Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
            { as := p } ◁
          Quot.mk Rel η' ≫
        (normalizeIso p g_1).hom =
      (normalizeIso p f_1).hom ≫
        PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)
p : Path.{v, u} a a_1
mk :
  Eq (α :=
    Quiver.Hom (V := a ⟶ c_1)
      (Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
          { as := p } ≫
        Hom.comp f_1 h)
      (Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
        { as := normalizeAux (normalizeAux p g_1) h }))
    (Iso.inv
        (α_
          (Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
            { as := p : Discrete (a ⟶ a_1) })
          f_1 h) ≫
      ((normalizeIso p f_1).hom ▷ h ≫
          PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯) ▷ h) ≫
        (normalizeIso (normalizeAux p g_1) h).hom)
    ((Iso.inv
          (α_
            (Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
              { as := p : Discrete (a ⟶ a_1) })
            f_1 h) ≫
        whiskerRight (B := FreeBicategory B) (a := a) (b := b_1) (c := c_1) (f :=
            Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
                { as := p : Discrete (a ⟶ a_1) } ≫
              f_1)
            (g :=
            Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
              { as := normalizeAux p f_1 : Discrete (a ⟶ b_1) })
            (normalizeIso p f_1).hom h ≫
          (normalizeIso (normalizeAux p f_1) h).hom) ≫
      eqToHom ⋯)
⊢ Eq (α :=
    Quiver.Hom (V := a ⟶ c_1)
      (Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
          { as := p } ≫
        Hom.comp f_1 h)
      (Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
        { as := normalizeAux (normalizeAux p g_1) h }))
    (CategoryStruct.comp (Y :=
      Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
          { as := p } ≫
        Hom.comp g_1 h)
      (Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
          { as := p } ◁
        whiskerRight (B := FreeBicategory B) (a := a_1) (b := b_1) (c := c_1) (f := f_1) (g := g_1) η'.mk h)
      (Iso.inv
          (α_
            (Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
              { as := p : Discrete (a ⟶ a_1) })
            g_1 h) ≫
        whiskerRight (B := FreeBicategory B) (a := a) (b := b_1) (c := c_1) (f :=
            Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
                { as := p } ≫
              g_1)
            (g :=
            Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
              { as := normalizeAux p g_1 })
            (normalizeIso p g_1).hom h ≫
          (normalizeIso (normalizeAux p g_1) h).hom))
    ((Iso.inv
          (α_
            (Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
              { as := p : Discrete (a ⟶ a_1) })
            f_1 h) ≫
        whiskerRight (B := FreeBicategory B) (a := a) (b := b_1) (c := c_1) (f :=
            Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
                { as := p : Discrete (a ⟶ a_1) } ≫
              f_1)
            (g :=
            Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
              { as := normalizeAux p f_1 : Discrete (a ⟶ b_1) })
            (normalizeIso p f_1).hom h ≫
          (normalizeIso (normalizeAux p f_1) h).hom) ≫
      eqToHom ⋯)

Tactic:
rw [associator_inv_naturality_middle_assoc, ← comp_whiskerRight_assoc, ih, comp_whiskerRight]

Premises used: CategoryTheory.Bicategory.comp_whiskerRight, CategoryTheory.Bicategory.comp_whiskerRight_assoc, CategoryTheory.Bicategory.associator_inv_naturality_middle_assoc