-- 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 : a_1 ⟶ b_1
g_1 h : b_1 ⟶ c_1
η : Hom₂ g_1 h
ih :
  ∀ (p : Path.{v, u} a b_1),
    Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
            { as := p } ◁
          Quot.mk Rel η ≫
        (normalizeIso p h).hom =
      (normalizeIso p g_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 } ≫
        f_1 ≫ g_1)
      (Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
        { as := normalizeAux (normalizeAux p f_1) h }))
    (Iso.inv
        (α_
          (Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
            { as := p : Discrete (a ⟶ a_1) })
          f_1 g_1) ≫
      (normalizeIso p f_1).hom ▷ g_1 ≫
        (normalizeIso (normalizeAux p f_1) g_1).hom ≫
          PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯))
    ((Iso.inv
          (α_
            (Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
              { as := p : Discrete (a ⟶ a_1) })
            f_1 g_1) ≫
        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 g_1 ≫
          (normalizeIso (normalizeAux p f_1) g_1).hom) ≫
      eqToHom ⋯)
⊢ Eq (α :=
    Quiver.Hom (V := a ⟶ c_1)
      (Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
          { as := p } ≫
        f_1 ≫ g_1)
      (Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
        { as := normalizeAux (normalizeAux p f_1) h }))
    (Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
          { as := p } ◁
        whiskerLeft (B := FreeBicategory B) (a := a_1) (b := b_1) (c := c_1) f_1 (g := g_1) (h := h) η.mk ≫
      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)
    ((Iso.inv
          (α_
            (Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
              { as := p : Discrete (a ⟶ a_1) })
            f_1 g_1) ≫
        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 g_1 ≫
          (normalizeIso (normalizeAux p f_1) g_1).hom) ≫
      eqToHom ⋯)

Tactic:
rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc, ih]

Premises used: CategoryTheory.Bicategory.whisker_exchange_assoc, CategoryTheory.Bicategory.associator_inv_naturality_right_assoc