awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : FreeBicategory B
f_1 g_1 h : a_1 ⟶ b_1
η : Hom₂ f_1 g_1
θ : Hom₂ g_1 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_1).hom =
      (normalizeIso p f_1).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_1).hom ≫
        PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)
p : Path.{v, u} a a_1
mk :
  Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B))) { as := p } ◁
        η.mk ≫
      (normalizeIso p g_1).hom ≫
        PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯) =
    (normalizeIso p f_1).hom ≫
      PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)
⊢ CategoryStruct.comp (Y :=
        Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
            { as := p } ≫
          g_1)
        (Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
            { as := p } ◁
          η.mk)
        (Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)))
            { as := p } ◁
          θ.mk) ≫
      (normalizeIso p h).hom =
    (normalizeIso p f_1).hom ≫
      PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)

Tactic:
slice_lhs 2 3 => rw [ihg]
-- 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 : FreeBicategory B
f_1 g_1 h : a_1 ⟶ b_1
η : Hom₂ f_1 g_1
θ : Hom₂ g_1 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_1).hom =
      (normalizeIso p f_1).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_1).hom ≫
        PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)
p : Path.{v, u} a a_1
a₁ :
  (normalizeIso p f_1).hom ≫ PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)
| Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B))) { as := p } ◁
      η.mk ≫
    (normalizeIso p g_1).hom

Tactic:
rw [ihf]
-- 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 : FreeBicategory B
f_1 g_1 h : a_1 ⟶ b_1
η : Hom₂ f_1 g_1
θ : Hom₂ g_1 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_1).hom =
      (normalizeIso p f_1).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_1).hom ≫
        PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)
p : Path.{v, u} a a_1
mk :
  ((normalizeIso p f_1).hom ≫
        PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)) ≫
      PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯) =
    (normalizeIso p f_1).hom ≫
      PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)
⊢ Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B))) { as := p } ◁
        η.mk ≫
      (normalizeIso p g_1).hom ≫
        PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯) =
    (normalizeIso p f_1).hom ≫
      PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)

Tactic:
slice_lhs 1 2 => rw [ihf]
-- 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 : FreeBicategory B
f_1 g_1 h : a_1 ⟶ b_1
η : Hom₂ f_1 g_1
θ : Hom₂ g_1 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_1).hom =
      (normalizeIso p f_1).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_1).hom ≫
        PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)
p : Path.{v, u} a a_1
⊢ ((normalizeIso p f_1).hom ≫
        PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)) ≫
      PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯) =
    (normalizeIso p f_1).hom ≫
      PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)

Tactic:
simp
-- 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 }))
    (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 ⋯)
⊢ Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B))) { as := p } ◁
        Quot.mk Rel (Hom₂.whisker_left f_1 η) ≫
      (normalizeIso p (f_1 ≫ h)).hom =
    (normalizeIso p (f_1 ≫ g_1)).hom ≫
      PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)

Tactic:
dsimp
-- 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
⊢ 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 ⋯)

Tactic:
simp
-- 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
⊢ (normalizeIso (normalizeAux p f_1) h).hom = eqToHom ⋯ ≫ (normalizeIso (normalizeAux p g_1) h).hom ≫ eqToHom ⋯

Tactic:
have := dcongr_arg (fun x => (normalizeIso x h).hom) (normalizeAux_congr p (Quot.mk _ η'))
-- 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
this : (normalizeIso (normalizeAux p f_1) h).hom = eqToHom ⋯ ≫ (normalizeIso (normalizeAux p g_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 }))
    (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 ⋯)

Tactic:
simp [this]
-- 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 d : FreeBicategory B
f_1 : a_1 ⟶ b_1
g_1 : b_1 ⟶ c_1
h : c_1 ⟶ d
p : Path.{v, u} a a_1
⊢ Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B))) { as := p } ◁
        Quot.mk Rel (Hom₂.associator f_1 g_1 h) ≫
      (normalizeIso p (f_1 ≫ g_1 ≫ h)).hom =
    (normalizeIso p ((f_1 ≫ g_1) ≫ h)).hom ≫
      PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)

Tactic:
simp
-- 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 d : FreeBicategory B
f_1 : a_1 ⟶ b_1
g_1 : b_1 ⟶ c_1
h : c_1 ⟶ 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_1 g_1 h) ≫
      (normalizeIso p ((f_1 ≫ g_1) ≫ h)).hom =
    (normalizeIso p (f_1 ≫ g_1 ≫ h)).hom ≫
      PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)

Tactic:
simp
-- 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 : FreeBicategory B
f_1 : a_1 ⟶ b_1
p : Path.{v, u} a a_1
⊢ Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B))) { as := p } ◁
        Quot.mk Rel (Hom₂.right_unitor f_1) ≫
      (normalizeIso p f_1).hom =
    (normalizeIso p (f_1 ≫ 𝟙 b_1)).hom ≫
      PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)

Tactic:
simp
-- 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 : FreeBicategory B
f_1 : a_1 ⟶ b_1
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_1) ≫
      Iso.hom (normalizeIso p (f_1 ≫ 𝟙 b_1)) =
    (normalizeIso p f_1).hom ≫
      PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)

Tactic:
simp
-- 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 : FreeBicategory B
f_1 : a_1 ⟶ b_1
p : Path.{v, u} a a_1
⊢ Prefunctor.map (PrelaxFunctorStruct.toPrefunctor (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B))) { as := p } ◁
        Quot.mk Rel (Hom₂.left_unitor f_1) ≫
      (normalizeIso p f_1).hom =
    (normalizeIso p (𝟙 a_1 ≫ f_1)).hom ≫
      PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)

Tactic:
simp
-- 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 : FreeBicategory B
f_1 : a_1 ⟶ b_1
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_1) ≫
      Iso.hom (normalizeIso p (𝟙 a_1 ≫ f_1)) =
    (normalizeIso p f_1).hom ≫
      PrelaxFunctorStruct.map₂ (PrelaxFunctor.toPrelaxFunctorStruct (preinclusion B)) (eqToHom ⋯)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
b c a_1 a : B
f : Hom.{v, u} a a_1
⊢ normalizeAux nil (f.comp (Hom.id a_1)) = (normalizeAux nil f).comp (normalizeAux nil (Hom.id a_1))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
b c a_1 b_1 : B
f_1 : a_1 ⟶ b_1
a : B
f : Hom.{v, u} a a_1
⊢ normalizeAux nil (f.comp (Hom.of f_1)) = (normalizeAux nil f).comp (normalizeAux nil (Hom.of f_1))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
b c a_1 b_1 c_1 : B
g : Hom.{v, u} a_1 b_1
g_1 : Hom.{v, u} b_1 c_1
ihf : ∀ {a : B} (f : Hom.{v, u} a a_1), normalizeAux nil (f.comp g) = (normalizeAux nil f).comp (normalizeAux nil g)
ihg : ∀ {a : B} (f : Hom.{v, u} a b_1), normalizeAux nil (f.comp g_1) = (normalizeAux nil f).comp (normalizeAux nil g_1)
a : B
f : Hom.{v, u} a a_1
comp :
  (normalizeAux nil (f.comp g)).comp (normalizeAux nil g_1) = (normalizeAux nil f).comp (normalizeAux nil (g.comp g_1))
comp₁ :
  ((normalizeAux nil f).comp (normalizeAux nil g)).comp (normalizeAux nil g_1) =
    (normalizeAux nil f).comp (normalizeAux nil (g.comp g_1))
comp₂ :
  ((normalizeAux nil f).comp (normalizeAux nil g)).comp (normalizeAux nil g_1) =
    (normalizeAux nil f).comp ((normalizeAux nil g).comp (normalizeAux nil g_1))
comp₃ comp₄ :
  (normalizeAux nil f).comp ((normalizeAux nil g).comp (normalizeAux nil g_1)) =
    (normalizeAux nil f).comp ((normalizeAux nil g).comp (normalizeAux nil g_1))
⊢ normalizeAux nil (f.comp (g.comp g_1)) = (normalizeAux nil f).comp (normalizeAux nil (g.comp g_1))

Tactic:
erw [ihg (f.comp g), ihf f, ihg g, comp_assoc]

Premises used: CategoryTheory.FreeBicategory.Hom.comp, Quiver.Path.comp_assoc
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b c : B
f : Hom.{v, u} a b
g : Hom.{v, u} b c
id :
  ∀ (a : B) {a_1 : B} (f : Hom.{v, u} a_1 a),
    normalizeAux nil (f.comp (Hom.id a)) = (normalizeAux nil f).comp (normalizeAux nil (Hom.id a))
of :
  ∀ {a b : B} (f : a ⟶ b) {a_1 : B} (f_1 : Hom.{v, u} a_1 a),
    normalizeAux nil (f_1.comp (Hom.of f)) = (normalizeAux nil f_1).comp (normalizeAux nil (Hom.of f))
comp :
  ∀ {a b c : B} (g : Hom.{v, u} a b) (g_1 : Hom.{v, u} b c)
    (ihf :
      ∀ {a_1 : B} (f : Hom.{v, u} a_1 a), normalizeAux nil (f.comp g) = (normalizeAux nil f).comp (normalizeAux nil g))
    (ihg :
      ∀ {a : B} (f : Hom.{v, u} a b), normalizeAux nil (f.comp g_1) = (normalizeAux nil f).comp (normalizeAux nil g_1))
    {a_1 : B} (f : Hom.{v, u} a_1 a),
    normalizeAux nil (f.comp (g.comp g_1)) = (normalizeAux nil f).comp (normalizeAux nil (g.comp g_1))
⊢ normalizeAux nil (f.comp g) = (normalizeAux nil f).comp (normalizeAux nil g)

Tactic:
induction g generalizing a with
  | id => rfl
  | of => rfl
  | comp g _ ihf ihg => erw [ihg (f.comp g), ihf f, ihg g, comp_assoc]

Premises used: CategoryTheory.FreeBicategory.of, id, Quiver.Path.comp_assoc, Quiver.Path.comp
-- Module: Mathlib.CategoryTheory.Bicategory.Coherence
Goal:
B : Type u
inst : Quiver.{v, u} B
a b : FreeBicategory B
f g : a ⟶ b
η : f ⟶ g
⊢ Eq (α :=
    Quiver.Hom (V := a ⟶ b) (𝟙 a ≫ Functor.obj (𝟭 (a ⟶ b)) f)
      (Functor.obj
        (Functor.comp (D :=
          Prefunctor.obj
              (PrelaxFunctorStruct.toPrefunctor
                (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
              a ⟶
            Prefunctor.obj
              (PrelaxFunctorStruct.toPrefunctor
                (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
              b)
          (PrelaxFunctor.mapFunctor (Pseudofunctor.toPrelaxFunctor (normalize B)) a b) (inclusionPath a b))
        g))
    (CategoryStruct.comp (Y := 𝟙 a ≫ Functor.obj (𝟭 (a ⟶ b)) g) (𝟙 a ◁ Functor.map (𝟭 (a ⟶ b)) η)
        (Iso.hom (normalizeIso nil g)) :
      Quiver.Hom (V := a ⟶ b) (𝟙 a ≫ Functor.obj (𝟭 (a ⟶ b)) f)
        (Functor.obj
          (Functor.comp (D :=
            Prefunctor.obj
                (PrelaxFunctorStruct.toPrefunctor
                  (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
                a ⟶
              Prefunctor.obj
                (PrelaxFunctorStruct.toPrefunctor
                  (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
                b)
            (PrelaxFunctor.mapFunctor (Pseudofunctor.toPrelaxFunctor (normalize B)) a b) (inclusionPath a b))
          g))
    (Iso.hom (normalizeIso nil f) ≫
        Functor.map
          (Functor.comp (D :=
            Prefunctor.obj
                (PrelaxFunctorStruct.toPrefunctor
                  (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
                a ⟶
              Prefunctor.obj
                (PrelaxFunctorStruct.toPrefunctor
                  (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
                b)
            (PrelaxFunctor.mapFunctor (Pseudofunctor.toPrelaxFunctor (normalize B)) a b) (inclusionPath a b))
          η :
      Quiver.Hom (V := a ⟶ b) (𝟙 a ≫ f : a ⟶ b)
        (Functor.obj
          (Functor.comp (D :=
            Prefunctor.obj
                (PrelaxFunctorStruct.toPrefunctor
                  (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
                a ⟶
              Prefunctor.obj
                (PrelaxFunctorStruct.toPrefunctor
                  (PrelaxFunctor.toPrelaxFunctorStruct (Pseudofunctor.toPrelaxFunctor (normalize B))))
                b)
            (PrelaxFunctor.mapFunctor (Pseudofunctor.toPrelaxFunctor (normalize B)) a b) (inclusionPath a b))
          g))

Tactic:
normalize_naturality nil η

Premises used: Quiver.Path.nil, CategoryTheory.FreeBicategory.normalize_naturality, CategoryTheory.FreeBicategory.inclusionPathAux