-- 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 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 whiskerRight X Y h η' ih =>
  intro n
  dsimp only [normalizeObj_tensor, normalizeIsoApp', tensor_eq_tensor, Iso.trans_hom,
    Iso.symm_hom, whiskerRightIso_hom, Function.comp_apply, inclusion_obj]
  rw [associator_inv_naturality_middle_assoc, ← comp_whiskerRight_assoc, ih]
  have := dcongr_arg (fun x => (normalizeIsoApp' C η' x).hom) (normalizeObj_congr n h)
  simp [this]

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 ⋯)

Proof state:
C : Type u
X Y X✝ Y✝ Z✝ : F C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
ihf :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y✝ n).hom = (normalizeIsoApp' C X✝ n).hom ≫ inclusion.map (eqToHom ⋯)
ihg :
  ∀ (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 ⋯)

Tactic:
simp [ihg, reassoc_of% (ihf _)]

Result:
no goals

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

Tactic:
simp [this]

Result:
no goals

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

Tactic:
rw [associator_inv_naturality_middle_assoc, ← comp_whiskerRight_assoc, ih]

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