-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Coherence (goal)
Goal:
C : Type u
X Y : F C
f : X ⟶ Y
id :
  ∀ (X : F C) (n : NormalMonoidalObject C),
    inclusionObj n ◁ 𝟙 X ≫ (normalizeIsoApp' C X n).hom = (normalizeIsoApp' C X n).hom ≫ map inclusion (eqToHom ⋯)
α_hom :
  ∀ (X Y Z : F C) (n : NormalMonoidalObject C),
    Eq (α :=
      tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n)
          (tensorObj (𝒞 := categoryFreeMonoidalCategory) (tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) Z) ⟶
        inclusionObj
          ((tensorObj (𝒞 := categoryFreeMonoidalCategory) X
                (tensorObj (𝒞 := categoryFreeMonoidalCategory) Y Z)).normalizeObj
            n))
      (inclusionObj n ◁ Iso.hom (α_ X Y Z) ≫
        Iso.hom
          (normalizeIsoApp' C
            (tensorObj (𝒞 := categoryFreeMonoidalCategory) X (tensorObj (𝒞 := categoryFreeMonoidalCategory) Y Z)) n))
      (Iso.hom
          (normalizeIsoApp' C
            (tensorObj (𝒞 := categoryFreeMonoidalCategory) (tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) Z) n) ≫
        map inclusion (eqToHom ⋯))
α_inv :
  ∀ (X Y Z : F C) (n : NormalMonoidalObject C),
    Eq (α :=
      tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n)
          (tensorObj (𝒞 := categoryFreeMonoidalCategory) X (tensorObj (𝒞 := categoryFreeMonoidalCategory) Y Z)) ⟶
        inclusionObj
          ((tensorObj (𝒞 := categoryFreeMonoidalCategory) (tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y)
                Z).normalizeObj
            n))
      (inclusionObj n ◁ Iso.inv (α_ X Y Z) ≫
        Iso.hom
          (normalizeIsoApp' C
            (tensorObj (𝒞 := categoryFreeMonoidalCategory) (tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) Z) n))
      (Iso.hom
          (normalizeIsoApp' C
            (tensorObj (𝒞 := categoryFreeMonoidalCategory) X (tensorObj (𝒞 := categoryFreeMonoidalCategory) Y Z)) n) ≫
        map inclusion (eqToHom ⋯))
l_hom :
  ∀ (X : F C) (n : NormalMonoidalObject C),
    Eq (α :=
      tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n)
          (tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X) ⟶
        inclusionObj (X.normalizeObj n))
      (inclusionObj n ◁ Iso.hom (λ_ X) ≫ (normalizeIsoApp' C X n).hom)
      (Iso.hom
          (normalizeIsoApp' C
            (tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X) n) ≫
        map inclusion (eqToHom ⋯))
l_inv :
  ∀ (X : F C) (n : NormalMonoidalObject C),
    Eq (α :=
      tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n) X ⟶
        inclusionObj
          ((tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory))
                X).normalizeObj
            n))
      (inclusionObj n ◁ Iso.inv (λ_ X) ≫
        Iso.hom
          (normalizeIsoApp' C
            (tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X) n))
      ((normalizeIsoApp' C X n).hom ≫ map inclusion (eqToHom ⋯))
ρ_hom :
  ∀ (X : F C) (n : NormalMonoidalObject C),
    Eq (α :=
      tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n)
          (tensorObj (𝒞 := categoryFreeMonoidalCategory) X ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory))) ⟶
        inclusionObj (X.normalizeObj n))
      (inclusionObj n ◁ Iso.hom (ρ_ X) ≫ (normalizeIsoApp' C X n).hom)
      (Iso.hom
          (normalizeIsoApp' C
            (tensorObj (𝒞 := categoryFreeMonoidalCategory) X ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory))) n) ≫
        map inclusion (eqToHom ⋯))
ρ_inv :
  ∀ (X : F C) (n : NormalMonoidalObject C),
    Eq (α :=
      tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n) X ⟶
        inclusionObj
          ((tensorObj (𝒞 := categoryFreeMonoidalCategory) X
                ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory))).normalizeObj
            n))
      (inclusionObj n ◁ Iso.inv (ρ_ X) ≫
        Iso.hom
          (normalizeIsoApp' C
            (tensorObj (𝒞 := categoryFreeMonoidalCategory) X ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory))) n))
      ((normalizeIsoApp' C X n).hom ≫ map inclusion (eqToHom ⋯))
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ map inclusion (eqToHom ⋯)
have comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z),
  (∀ (n : NormalMonoidalObject C),
      inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ map inclusion (eqToHom sorry)) →
    (∀ (n : NormalMonoidalObject C),
        inclusionObj n ◁ g ≫ (normalizeIsoApp' C Z n).hom = (normalizeIsoApp' C Y n).hom ≫ map inclusion (eqToHom sorry)) →
      ∀ (n : NormalMonoidalObject C),
        inclusionObj n ◁ (f ≫ g) ≫ (normalizeIsoApp' C Z n).hom =
          (normalizeIsoApp' C X n).hom ≫ map inclusion (eqToHom sorry)
Tactic: induction f using Hom.inductionOn
Cleared hypotheses: f