-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
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 ⋯)
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 ⋯))
    (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 ⋯)
mk₃ :
  ∀ {a_1 b c : FreeBicategory B} {f g : a_1 ⟶ b} (h : b ⟶ c) (η' : Hom₂ f g)
    (ih :
      ∀ (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 ⋯))
    (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 h)).hom =
      (normalizeIso p (Hom.comp f h)).hom ≫
        PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)
mk₄ :
  ∀ {a_1 b c d : FreeBicategory B} (f : a_1 ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (p : Path.{v, u} a a_1),
    Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
            { as := p } ◁
          Quot.mk Rel (Hom₂.associator f g h) ≫
        (normalizeIso p (f ≫ g ≫ h)).hom =
      (normalizeIso p ((f ≫ g) ≫ h)).hom ≫
        PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)
mk₅ :
  ∀ {a_1 b c d : FreeBicategory B} (f : a_1 ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (p : Path.{v, u} a a_1),
    Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
            { as := p } ◁
          Quot.mk Rel (Hom₂.associator_inv f g h) ≫
        (normalizeIso p ((f ≫ g) ≫ h)).hom =
      (normalizeIso p (f ≫ g ≫ h)).hom ≫
        PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)
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₂.right_unitor f) ≫
        (normalizeIso p f).hom =
      (normalizeIso p (f ≫ 𝟙 b)).hom ≫
        PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)
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₂.right_unitor_inv f) ≫
        Iso.hom (normalizeIso p (f ≫ 𝟙 b)) =
      (normalizeIso p f).hom ≫
        PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)
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₂.left_unitor f) ≫
        (normalizeIso p f).hom =
      (normalizeIso p (𝟙 a_1 ≫ f)).hom ≫
        PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)
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₂.left_unitor_inv f) ≫
        Iso.hom (normalizeIso p (𝟙 a_1 ≫ f)) =
      (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 ⋯)

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

Premises used: CategoryTheory.Bicategory.whiskerLeft_comp, CategoryTheory.FreeBicategory.mk_vcomp, CategoryTheory.Bicategory.comp_whiskerRight, id, CategoryTheory.Bicategory.comp_whiskerRight_assoc, CategoryTheory.Bicategory.whisker_exchange_assoc, CategoryTheory.Bicategory.associator_inv_naturality_right_assoc, CategoryTheory.Bicategory.associator_inv_naturality_middle_assoc