-- 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 ⋯))
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ map inclusion (eqToHom ⋯)
have 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 sorry))
Tactic: induction f using Hom.inductionOn
Cleared hypotheses: f