Lean4
/-- Auxiliary definition for `normalize`. Here we prove that objects that are related by
associators and unitors map to the same normal form. -/
@[simp]
def normalizeMapAux : ∀ {X Y : F C}, (X ⟶ᵐ Y) → (normalizeObj' X ⟶ normalizeObj' Y)
| _, _, Hom.id _ => 𝟙 _
| _, _, α_hom X Y Z => by dsimp; exact Discrete.natTrans (fun _ => 𝟙 _)
| _, _, α_inv _ _ _ => by dsimp; exact Discrete.natTrans (fun _ => 𝟙 _)
| _, _, l_hom _ => by dsimp; exact Discrete.natTrans (fun _ => 𝟙 _)
| _, _, l_inv _ => by dsimp; exact Discrete.natTrans (fun _ => 𝟙 _)
| _, _, ρ_hom _ => by dsimp; exact Discrete.natTrans (fun _ => 𝟙 _)
| _, _, ρ_inv _ => by dsimp; exact Discrete.natTrans (fun _ => 𝟙 _)
| _, _, (@Hom.comp _ _ _ _ f g) => normalizeMapAux f ≫ normalizeMapAux g
| _, _, (@Hom.tensor _ T _ _ W f g) =>
Discrete.natTrans <| fun ⟨X⟩ =>
(normalizeMapAux g).app ⟨normalizeObj T X⟩ ≫ (normalizeObj' W).map ((normalizeMapAux f).app ⟨X⟩)
| _, _, (@Hom.whiskerLeft _ T _ W f) => Discrete.natTrans <| fun ⟨X⟩ => (normalizeMapAux f).app ⟨normalizeObj T X⟩
| _, _, (@Hom.whiskerRight _ T _ f W) =>
Discrete.natTrans <| fun X => (normalizeObj' W).map <| (normalizeMapAux f).app X
