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