-- Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean
theorem normalize_naturality (n : NormalMonoidalObject C) {X Y : F C} (f : X ⟶ Y) :
    inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom =
      (normalizeIsoApp' C X n).hom ≫
        inclusion.map (eqToHom (Discrete.ext (normalizeObj_congr n f)))

Proof state:
case id
C : Type u
X Y X✝ : F C
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ 𝟙 X✝ ≫ (normalizeIsoApp' C X✝ n).hom = (normalizeIsoApp' C X✝ n).hom ≫ inclusion.map (eqToHom ⋯)

case α_hom
C : Type u
X Y X✝ Y✝ Z✝ : F C
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ (α_ X✝ Y✝ Z✝).hom ≫ (normalizeIsoApp' C (X✝ ⊗ Y✝ ⊗ Z✝) n).hom =
      (normalizeIsoApp' C ((X✝ ⊗ Y✝) ⊗ Z✝) n).hom ≫ inclusion.map (eqToHom ⋯)

case α_inv
C : Type u
X Y X✝ Y✝ Z✝ : F C
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ (α_ X✝ Y✝ Z✝).inv ≫ (normalizeIsoApp' C ((X✝ ⊗ Y✝) ⊗ Z✝) n).hom =
      (normalizeIsoApp' C (X✝ ⊗ Y✝ ⊗ Z✝) n).hom ≫ inclusion.map (eqToHom ⋯)

case l_hom
C : Type u
X Y X✝ : F C
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ (λ_ X✝).hom ≫ (normalizeIsoApp' C X✝ n).hom =
      (normalizeIsoApp' C (𝟙_ (F C) ⊗ X✝) n).hom ≫ inclusion.map (eqToHom ⋯)

case l_inv
C : Type u
X Y X✝ : F C
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ (λ_ X✝).inv ≫ (normalizeIsoApp' C (𝟙_ (F C) ⊗ X✝) n).hom =
      (normalizeIsoApp' C X✝ n).hom ≫ inclusion.map (eqToHom ⋯)

case ρ_hom
C : Type u
X Y X✝ : F C
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ (ρ_ X✝).hom ≫ (normalizeIsoApp' C X✝ n).hom =
      (normalizeIsoApp' C (X✝ ⊗ 𝟙_ (F C)) n).hom ≫ inclusion.map (eqToHom ⋯)

case ρ_inv
C : Type u
X Y X✝ : F C
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ (ρ_ X✝).inv ≫ (normalizeIsoApp' C (X✝ ⊗ 𝟙_ (F C)) n).hom =
      (normalizeIsoApp' C X✝ n).hom ≫ inclusion.map (eqToHom ⋯)

case comp
C : Type u
X Y X✝ Y✝ Z✝ : F C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
a✝¹ :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ f✝ ≫ (normalizeIsoApp' C Y✝ n).hom = (normalizeIsoApp' C X✝ n).hom ≫ inclusion.map (eqToHom ⋯)
a✝ :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ g✝ ≫ (normalizeIsoApp' C Z✝ n).hom = (normalizeIsoApp' C Y✝ n).hom ≫ inclusion.map (eqToHom ⋯)
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ (f✝ ≫ g✝) ≫ (normalizeIsoApp' C Z✝ n).hom =
      (normalizeIsoApp' C X✝ n).hom ≫ inclusion.map (eqToHom ⋯)

case whiskerLeft
C : Type u
X Y X✝ Y✝ Z✝ : F C
f✝ : Y✝ ⟶ Z✝
a✝ :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ f✝ ≫ (normalizeIsoApp' C Z✝ n).hom = (normalizeIsoApp' C Y✝ n).hom ≫ inclusion.map (eqToHom ⋯)
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ X✝ ◁ f✝ ≫ (normalizeIsoApp' C (X✝ ⊗ Z✝) n).hom =
      (normalizeIsoApp' C (X✝ ⊗ Y✝) n).hom ≫ inclusion.map (eqToHom ⋯)

case whiskerRight
C : Type u
X Y X✝ Y✝ : F C
f✝ : X✝ ⟶ Y✝
Z✝ : F C
a✝ :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ f✝ ≫ (normalizeIsoApp' C Y✝ n).hom = (normalizeIsoApp' C X✝ n).hom ≫ inclusion.map (eqToHom ⋯)
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ f✝ ▷ Z✝ ≫ (normalizeIsoApp' C (Y✝ ⊗ Z✝) n).hom =
      (normalizeIsoApp' C (X✝ ⊗ Z✝) n).hom ≫ inclusion.map (eqToHom ⋯)

Tactic:
case comp f g ihf ihg => simp [ihg, reassoc_of% (ihf _)]

Result:
case id
C : Type u
X Y X✝ : F C
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ 𝟙 X✝ ≫ (normalizeIsoApp' C X✝ n).hom = (normalizeIsoApp' C X✝ n).hom ≫ inclusion.map (eqToHom ⋯)

case α_hom
C : Type u
X Y X✝ Y✝ Z✝ : F C
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ (α_ X✝ Y✝ Z✝).hom ≫ (normalizeIsoApp' C (X✝ ⊗ Y✝ ⊗ Z✝) n).hom =
      (normalizeIsoApp' C ((X✝ ⊗ Y✝) ⊗ Z✝) n).hom ≫ inclusion.map (eqToHom ⋯)

case α_inv
C : Type u
X Y X✝ Y✝ Z✝ : F C
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ (α_ X✝ Y✝ Z✝).inv ≫ (normalizeIsoApp' C ((X✝ ⊗ Y✝) ⊗ Z✝) n).hom =
      (normalizeIsoApp' C (X✝ ⊗ Y✝ ⊗ Z✝) n).hom ≫ inclusion.map (eqToHom ⋯)

case l_hom
C : Type u
X Y X✝ : F C
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ (λ_ X✝).hom ≫ (normalizeIsoApp' C X✝ n).hom =
      (normalizeIsoApp' C (𝟙_ (F C) ⊗ X✝) n).hom ≫ inclusion.map (eqToHom ⋯)

case l_inv
C : Type u
X Y X✝ : F C
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ (λ_ X✝).inv ≫ (normalizeIsoApp' C (𝟙_ (F C) ⊗ X✝) n).hom =
      (normalizeIsoApp' C X✝ n).hom ≫ inclusion.map (eqToHom ⋯)

case ρ_hom
C : Type u
X Y X✝ : F C
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ (ρ_ X✝).hom ≫ (normalizeIsoApp' C X✝ n).hom =
      (normalizeIsoApp' C (X✝ ⊗ 𝟙_ (F C)) n).hom ≫ inclusion.map (eqToHom ⋯)

case ρ_inv
C : Type u
X Y X✝ : F C
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ (ρ_ X✝).inv ≫ (normalizeIsoApp' C (X✝ ⊗ 𝟙_ (F C)) n).hom =
      (normalizeIsoApp' C X✝ n).hom ≫ inclusion.map (eqToHom ⋯)

case whiskerLeft
C : Type u
X Y X✝ Y✝ Z✝ : F C
f✝ : Y✝ ⟶ Z✝
a✝ :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ f✝ ≫ (normalizeIsoApp' C Z✝ n).hom = (normalizeIsoApp' C Y✝ n).hom ≫ inclusion.map (eqToHom ⋯)
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ X✝ ◁ f✝ ≫ (normalizeIsoApp' C (X✝ ⊗ Z✝) n).hom =
      (normalizeIsoApp' C (X✝ ⊗ Y✝) n).hom ≫ inclusion.map (eqToHom ⋯)

case whiskerRight
C : Type u
X Y X✝ Y✝ : F C
f✝ : X✝ ⟶ Y✝
Z✝ : F C
a✝ :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ f✝ ≫ (normalizeIsoApp' C Y✝ n).hom = (normalizeIsoApp' C X✝ n).hom ≫ inclusion.map (eqToHom ⋯)
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ f✝ ▷ Z✝ ≫ (normalizeIsoApp' C (Y✝ ⊗ Z✝) n).hom =
      (normalizeIsoApp' C (X✝ ⊗ Z✝) n).hom ≫ inclusion.map (eqToHom ⋯)

Proof state:
C : Type u
X✝ Y✝ X' X Y : F C
f : X ⟶ Y
ih :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ inclusion.map (eqToHom ⋯)
n : NormalMonoidalObject C
⊢ inclusionObj n ◁ X' ◁ f ≫
      (α_ (inclusionObj n) X' Y).inv ≫
        (normalizeIsoApp' C X' n).hom ▷ Y ≫ (normalizeIsoApp' C Y (X'.normalizeObj n)).hom =
    ((α_ (inclusionObj n) X' X).inv ≫
        (normalizeIsoApp' C X' n).hom ▷ X ≫ (normalizeIsoApp' C X (X'.normalizeObj n)).hom) ≫
      inclusion.map (eqToHom ⋯)

Tactic:
rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc, ih]

Result:
C : Type u
X✝ Y✝ X' X Y : F C
f : X ⟶ Y
ih :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ inclusion.map (eqToHom ⋯)
n : NormalMonoidalObject C
⊢ (α_ (inclusionObj n) X' X).inv ≫
      (normalizeIsoApp' C X' n).hom ▷ X ≫ (normalizeIsoApp' C X (X'.normalizeObj n)).hom ≫ inclusion.map (eqToHom ⋯) =
    ((α_ (inclusionObj n) X' X).inv ≫
        (normalizeIsoApp' C X' n).hom ▷ X ≫ (normalizeIsoApp' C X (X'.normalizeObj n)).hom) ≫
      inclusion.map (eqToHom ⋯)

Proof state:
case ρ_inv
C : Type u
X Y X✝ : F C
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ (ρ_ X✝).inv ≫ (normalizeIsoApp' C (X✝ ⊗ 𝟙_ (F C)) n).hom =
      (normalizeIsoApp' C X✝ n).hom ≫ inclusion.map (eqToHom ⋯)

Tactic:
simp

Result:
no goals