-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Coherence (goal)
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
p : Path.{v, u} a b
f g : Hom.{v, u} b c
η' : Hom₂ f g
mk :
  ∀ {a_1 b : FreeBicategory B} (f : a_1 ⟶ b) (p : Path.{v, u} a a_1),
    Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
            { as := p } ◁
          Quot.mk Rel (Hom₂.id f) ≫
        (normalizeIso p f).hom =
      (normalizeIso p f).hom ≫
        PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)
mk₁ :
  ∀ {a_1 b : FreeBicategory B} {f g h : a_1 ⟶ b} (η : Hom₂ f g) (θ : Hom₂ g h)
    (ihf :
      ∀ (p : Path.{v, u} a a_1),
        Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
                { as := p } ◁
              Quot.mk Rel η ≫
            (normalizeIso p g).hom =
          (normalizeIso p f).hom ≫
            PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯))
    (ihg :
      ∀ (p : Path.{v, u} a a_1),
        Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
                { as := p } ◁
              Quot.mk Rel θ ≫
            (normalizeIso p h).hom =
          (normalizeIso p g).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 (η.vcomp θ) ≫
        (normalizeIso p h).hom =
      (normalizeIso p f).hom ≫
        PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)
⊢ Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B))) { as := p } ◁
        Quot.mk Rel η' ≫
      (normalizeIso p g).hom =
    (normalizeIso p f).hom ≫ PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)
have mk₂ : ∀ {a_1 b c : FreeBicategory B} (f : a_1 ⟶ b) {g h : b ⟶ c} (η : Hom₂ g h)
  (ih :
    ∀ (p : Path.{v, u} a b),
      Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
              { as := p } ◁
            Quot.mk Rel η ≫
          (normalizeIso p h).hom =
        (normalizeIso p g).hom ≫
          PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom sorry))
  (p : Path.{v, u} a a_1),
  Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B))) { as := p } ◁
        Quot.mk Rel (Hom₂.whisker_left f η) ≫
      (normalizeIso p (f ≫ h)).hom =
    (normalizeIso p (f ≫ g)).hom ≫
      PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom sorry)
Tactic: induction η' with
  | id => simp
  | vcomp η θ ihf ihg =>
    simp only [mk_vcomp, whiskerLeft_comp]
    slice_lhs 2 3 => rw [ihg]
    slice_lhs 1 2 => rw [ihf]
    simp
  -- p ≠ nil required! See the docstring of `normalizeAux`.
  | whisker_left _ _ ih =>
    dsimp
    rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc, ih]
    simp
  | whisker_right h η' ih =>
    dsimp
    rw [associator_inv_naturality_middle_assoc, ← comp_whiskerRight_assoc, ih, comp_whiskerRight]
    have := dcongr_arg (fun x => (normalizeIso x h).hom) (normalizeAux_congr p (Quot.mk _ η'))
    dsimp at this; simp [this]
  | _ => simp
Cleared hypotheses: p, η'