-- Mathlib/CategoryTheory/Bicategory/Coherence.lean
theorem normalize_naturality {a b c : B} (p : Path a b) {f g : Hom b c} (η : f ⟶ g) :
    (preinclusion B).map ⟨p⟩ ◁ η ≫ (normalizeIso p g).hom =
      (normalizeIso p f).hom ≫
        (preinclusion B).map₂ (eqToHom (Discrete.ext (normalizeAux_congr p η)))

Proof state:
B : Type u
inst✝ : Quiver B
a b c : B
p : Path a b
f g : Hom b c
η : f ⟶ g
⊢ (preinclusion B).map { as := p } ◁ η ≫ (normalizeIso p g).hom =
    (normalizeIso p f).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)

Tactic:
rcases η with ⟨η'⟩

Result:
case mk
B : Type u
inst✝ : Quiver B
a b c : B
p : Path a b
f g : Hom b c
η : f ⟶ g
η' : Hom₂ f g
⊢ (preinclusion B).map { as := p } ◁ Quot.mk Rel η' ≫ (normalizeIso p g).hom =
    (normalizeIso p f).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)

Proof state:
case mk.vcomp
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η : Hom₂ f✝ g✝
θ : Hom₂ g✝ h✝
ihf :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel η ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
ihg :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel θ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
⊢ ((normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)) ≫ (preinclusion B).map₂ (eqToHom ⋯) =
    (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)

Tactic:
simp

Result:
no goals

Proof state:
case mk.whisker_left
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
g✝ h✝ : b✝ ⟶ c✝
η✝ : Hom₂ g✝ h✝
ih :
  ∀ (p : Path a b✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel η✝ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
⊢ (preinclusion B).map { as := p } ◁ f✝ ◁ η✝.mk ≫
      (α_ ((preinclusion B).map { as := p }) f✝ h✝).inv ≫
        (normalizeIso p f✝).hom ▷ h✝ ≫ (normalizeIso (normalizeAux p f✝) h✝).hom =
    ((α_ ((preinclusion B).map { as := p }) f✝ g✝).inv ≫
        (normalizeIso p f✝).hom ▷ g✝ ≫ (normalizeIso (normalizeAux p f✝) g✝).hom) ≫
      (preinclusion B).map₂ (eqToHom ⋯)

Tactic:
rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc, ih]

Result:
case mk.whisker_left
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
g✝ h✝ : b✝ ⟶ c✝
η✝ : Hom₂ g✝ h✝
ih :
  ∀ (p : Path a b✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel η✝ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
⊢ (α_ ((preinclusion B).map { as := p }) f✝ g✝).inv ≫
      (normalizeIso p f✝).hom ▷ g✝ ≫ (normalizeIso (normalizeAux p f✝) g✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯) =
    ((α_ ((preinclusion B).map { as := p }) f✝ g✝).inv ≫
        (normalizeIso p f✝).hom ▷ g✝ ≫ (normalizeIso (normalizeAux p f✝) g✝).hom) ≫
      (preinclusion B).map₂ (eqToHom ⋯)

Proof state:
case mk.vcomp
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η : Hom₂ f✝ g✝
θ : Hom₂ g✝ h✝
ihf :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel η ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
ihg :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel θ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
⊢ (preinclusion B).map { as := p } ◁ Quot.mk Rel (η.vcomp θ) ≫ (normalizeIso p h✝).hom =
    (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)

Tactic:
simp only [mk_vcomp, Bicategory.whiskerLeft_comp]

Result:
case mk.vcomp
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η : Hom₂ f✝ g✝
θ : Hom₂ g✝ h✝
ihf :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel η ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
ihg :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel θ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
⊢ ((preinclusion B).map { as := p } ◁ η.mk ≫ (preinclusion B).map { as := p } ◁ θ.mk) ≫ (normalizeIso p h✝).hom =
    (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)

Proof state:
case mk.whisker_right
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
h : b✝ ⟶ c✝
η' : Hom₂ f✝ g✝
ih :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel η' ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
this : (normalizeIso (normalizeAux p f✝) h).hom = eqToHom ⋯ ≫ (normalizeIso (normalizeAux p g✝) h).hom ≫ eqToHom ⋯
⊢ (α_ ((preinclusion B).map { as := p }) f✝ h).inv ≫
      ((normalizeIso p f✝).hom ▷ h ≫ (preinclusion B).map₂ (eqToHom ⋯) ▷ h) ≫ (normalizeIso (normalizeAux p g✝) h).hom =
    ((α_ ((preinclusion B).map { as := p }) f✝ h).inv ≫
        (normalizeIso p f✝).hom ▷ h ≫ (normalizeIso (normalizeAux p f✝) h).hom) ≫
      (preinclusion B).map₂ (eqToHom ⋯)

Tactic:
simp [this]

Result:
no goals

Proof state:
case mk
B : Type u
inst✝ : Quiver B
a b c : B
p : Path a b
f g : Hom b c
η : f ⟶ g
η' : Hom₂ f g
⊢ (preinclusion B).map { as := p } ◁ Quot.mk Rel η' ≫ (normalizeIso p g).hom =
    (normalizeIso p f).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)

Tactic:
clear η

Result:
case mk
B : Type u
inst✝ : Quiver B
a b c : B
p : Path a b
f g : Hom b c
η' : Hom₂ f g
⊢ (preinclusion B).map { as := p } ◁ Quot.mk Rel η' ≫ (normalizeIso p g).hom =
    (normalizeIso p f).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)

Proof state:
case mk.vcomp
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η : Hom₂ f✝ g✝
θ : Hom₂ g✝ h✝
ihf :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel η ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
ihg :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel θ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
⊢ (preinclusion B).map { as := p } ◁ η.mk ≫ (normalizeIso p g✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯) =
    (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)

Tactic:
slice_lhs 1 2 => rw [ihf]

Result:
case mk.vcomp
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η : Hom₂ f✝ g✝
θ : Hom₂ g✝ h✝
ihf :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel η ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
ihg :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel θ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
⊢ ((normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)) ≫ (preinclusion B).map₂ (eqToHom ⋯) =
    (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)