-- 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 ⋯))
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 ⋯)) →
      (∀ (n : NormalMonoidalObject C),
          inclusionObj n ◁ g ≫ (normalizeIsoApp' C Z n).hom =
            (normalizeIsoApp' C Y n).hom ≫ map inclusion (eqToHom ⋯)) →
        ∀ (n : NormalMonoidalObject C),
          inclusionObj n ◁ (f ≫ g) ≫ (normalizeIsoApp' C Z n).hom =
            (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 whiskerLeft : ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z),
  (∀ (n : NormalMonoidalObject C),
      inclusionObj n ◁ f ≫ (normalizeIsoApp' C Z n).hom = (normalizeIsoApp' C Y n).hom ≫ map inclusion (eqToHom sorry)) →
    ∀ (n : NormalMonoidalObject C),
      Eq (α :=
        tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n)
            (tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) ⟶
          inclusionObj ((tensorObj (𝒞 := categoryFreeMonoidalCategory) X Z).normalizeObj n))
        (inclusionObj n ◁ X ◁ f ≫ Iso.hom (normalizeIsoApp' C (tensorObj (𝒞 := categoryFreeMonoidalCategory) X Z) n))
        (Iso.hom (normalizeIsoApp' C (tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) n) ≫ map inclusion (eqToHom sorry))
Tactic: induction f using Hom.inductionOn
Cleared hypotheses: f