-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
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
⊢ Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B))) { as := p } ◁
        Quot.mk Rel (Hom₂.whisker_right h η') ≫
      (normalizeIso p (Hom.comp g_1 h)).hom =
    (normalizeIso p (Hom.comp f_1 h)).hom ≫
      PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)
have 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 }))
  (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 sorry)
Tactic: dsimp