awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v', u'} D
inst_1 : MonoidalCategory.{v', u'} D
f_1 : C → D
X Y : F C
f : X ⟶ Y
x : F C
f₁ :
  ∀ (a : X ⟶ᵐ Y),
    Functor.map (project f_1) ⟦a⟧ ▷ Functor.obj.{u, v', u, u'} (project f_1) x ≫
        Iso.hom
          (Iso.refl
            (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) Y)
              (Functor.obj.{u, v', u, u'} (project f_1) x))) =
      Iso.hom
          (Iso.refl
            (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) X)
              (Functor.obj.{u, v', u, u'} (project f_1) x))) ≫
        Functor.map (project f_1) (⟦a⟧ ▷ x)
h :
  ∀ (a b : X ⟶ᵐ Y) (p : a ≈ b),
    Eq (α :=
      Functor.map (project f_1) ⟦b⟧ ▷ Functor.obj.{u, v', u, u'} (project f_1) x ≫
          Iso.hom
            (Iso.refl
              (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) Y)
                (Functor.obj.{u, v', u, u'} (project f_1) x))) =
        Iso.hom
            (Iso.refl
              (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) X)
                (Functor.obj.{u, v', u, u'} (project f_1) x))) ≫
          Functor.map (project f_1) (⟦b⟧ ▷ x))
      ⋯ ⋯
⊢ Functor.map (project f_1) f ▷ Functor.obj.{u, v', u, u'} (project f_1) x ≫
      Iso.hom
        (Iso.refl
          (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) Y)
            (Functor.obj.{u, v', u, u'} (project f_1) x))) =
    Iso.hom
        (Iso.refl
          (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) X)
            (Functor.obj.{u, v', u, u'} (project f_1) x))) ≫
      Functor.map (project f_1) (f ▷ x)

Tactic:
induction f using Quotient.recOn
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v', u'} D
inst_1 : MonoidalCategory.{v', u'} D
f : C → D
X Y x : F C
a : X ⟶ᵐ Y
⊢ Functor.map (project f) ⟦a⟧ ▷ Functor.obj.{u, v', u, u'} (project f) x ≫
      Iso.hom
        (Iso.refl
          (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f) Y)
            (Functor.obj.{u, v', u, u'} (project f) x))) =
    Iso.hom
        (Iso.refl
          (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f) X)
            (Functor.obj.{u, v', u, u'} (project f) x))) ≫
      Functor.map (project f) (⟦a⟧ ▷ x)

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v', u'} D
inst_1 : MonoidalCategory.{v', u'} D
f_1 : C → D
X Y : F C
f : X ⟶ Y
x : F C
a b : X ⟶ᵐ Y
p : a ≈ b
⊢ Eq (α :=
    Functor.map (project f_1) ⟦b⟧ ▷ Functor.obj.{u, v', u, u'} (project f_1) x ≫
        Iso.hom
          (Iso.refl
            (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) Y)
              (Functor.obj.{u, v', u, u'} (project f_1) x))) =
      Iso.hom
          (Iso.refl
            (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) X)
              (Functor.obj.{u, v', u, u'} (project f_1) x))) ≫
        Functor.map (project f_1) (⟦b⟧ ▷ x))
    ⋯ ⋯

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v', u'} D
inst_1 : MonoidalCategory.{v', u'} D
f_1 : C → D
X Y x : F C
f : X ⟶ Y
f₁ :
  ∀ (a : X ⟶ᵐ Y),
    Functor.obj.{u, v', u, u'} (project f_1) x ◁ Functor.map (project f_1) ⟦a⟧ ≫
        Iso.hom
          (Iso.refl
            (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) x)
              (Functor.obj.{u, v', u, u'} (project f_1) Y))) =
      Iso.hom
          (Iso.refl
            (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) x)
              (Functor.obj.{u, v', u, u'} (project f_1) X))) ≫
        Functor.map (project f_1) (x ◁ ⟦a⟧)
h :
  ∀ (a b : X ⟶ᵐ Y) (p : a ≈ b),
    Eq (α :=
      Functor.obj.{u, v', u, u'} (project f_1) x ◁ Functor.map (project f_1) ⟦b⟧ ≫
          Iso.hom
            (Iso.refl
              (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) x)
                (Functor.obj.{u, v', u, u'} (project f_1) Y))) =
        Iso.hom
            (Iso.refl
              (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) x)
                (Functor.obj.{u, v', u, u'} (project f_1) X))) ≫
          Functor.map (project f_1) (x ◁ ⟦b⟧))
      ⋯ ⋯
⊢ Functor.obj.{u, v', u, u'} (project f_1) x ◁ Functor.map (project f_1) f ≫
      Iso.hom
        (Iso.refl
          (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) x)
            (Functor.obj.{u, v', u, u'} (project f_1) Y))) =
    Iso.hom
        (Iso.refl
          (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) x)
            (Functor.obj.{u, v', u, u'} (project f_1) X))) ≫
      Functor.map (project f_1) (x ◁ f)

Tactic:
induction f using Quotient.recOn
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v', u'} D
inst_1 : MonoidalCategory.{v', u'} D
f : C → D
X Y x : F C
a : X ⟶ᵐ Y
⊢ Functor.obj.{u, v', u, u'} (project f) x ◁ Functor.map (project f) ⟦a⟧ ≫
      Iso.hom
        (Iso.refl
          (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f) x)
            (Functor.obj.{u, v', u, u'} (project f) Y))) =
    Iso.hom
        (Iso.refl
          (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f) x)
            (Functor.obj.{u, v', u, u'} (project f) X))) ≫
      Functor.map (project f) (x ◁ ⟦a⟧)

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v', u'} D
inst_1 : MonoidalCategory.{v', u'} D
f_1 : C → D
X Y x : F C
f : X ⟶ Y
a b : X ⟶ᵐ Y
p : a ≈ b
⊢ Eq (α :=
    Functor.obj.{u, v', u, u'} (project f_1) x ◁ Functor.map (project f_1) ⟦b⟧ ≫
        Iso.hom
          (Iso.refl
            (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) x)
              (Functor.obj.{u, v', u, u'} (project f_1) Y))) =
      Iso.hom
          (Iso.refl
            (tensorObj.{v', u'} (𝒞 := inst) (Functor.obj.{u, v', u, u'} (project f_1) x)
              (Functor.obj.{u, v', u, u'} (project f_1) X))) ≫
        Functor.map (project f_1) (x ◁ ⟦b⟧))
    ⋯ ⋯

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
x y : (Discrete ∘ NormalMonoidalObject) C
⊢ Subsingleton.{u + 1} (x ⟶ y)

Tactic:
Discrete.instSubsingletonDiscreteHom _ _

Premises used: CategoryTheory.Discrete.instSubsingletonDiscreteHom
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X : (Discrete ∘ NormalMonoidalObject) C
⊢ obj inclusion X = inclusionObj X.as

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y : (Discrete ∘ NormalMonoidalObject) C
f : X ⟶ Y
⊢ Eq (α := obj inclusion X ⟶ obj inclusion Y) (map inclusion f) (eqToHom ⋯)

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, Quotient, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
n : NormalMonoidalObject C
⊢ normalizeObj ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) n = n

Tactic:
rfl

Premises used: CategoryTheory.FreeMonoidalCategory.normalizeObj, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y : F C
n : NormalMonoidalObject C
⊢ (tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y).normalizeObj n = Y.normalizeObj (X.normalizeObj n)

Tactic:
rfl

Premises used: CategoryTheory.FreeMonoidalCategory.normalizeObj, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y Z : F C
⊢ (tensorObj (𝒞 := categoryFreeMonoidalCategory) (tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) Z).normalizeObj' ⟶
    (tensorObj (𝒞 := categoryFreeMonoidalCategory) X (tensorObj (𝒞 := categoryFreeMonoidalCategory) Y Z)).normalizeObj'

Tactic:
exact Discrete.natTrans (fun _ => 𝟙 _)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Discrete.natTrans, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y Z : F C
⊢ (tensorObj (𝒞 := categoryFreeMonoidalCategory) X (tensorObj (𝒞 := categoryFreeMonoidalCategory) Y Z)).normalizeObj' ⟶
    (tensorObj (𝒞 := categoryFreeMonoidalCategory) (tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) Z).normalizeObj'

Tactic:
exact Discrete.natTrans (fun _ => 𝟙 _)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Discrete.natTrans, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
a : F C
⊢ (tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) a).normalizeObj' ⟶
    a.normalizeObj'

Tactic:
exact Discrete.natTrans (fun _ => 𝟙 _)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Discrete.natTrans, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
a : F C
⊢ a.normalizeObj' ⟶
    (tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) a).normalizeObj'

Tactic:
exact Discrete.natTrans (fun _ => 𝟙 _)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Discrete.natTrans, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
a : F C
⊢ (tensorObj (𝒞 := categoryFreeMonoidalCategory) a ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory))).normalizeObj' ⟶
    a.normalizeObj'

Tactic:
exact Discrete.natTrans (fun _ => 𝟙 _)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Discrete.natTrans, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
a : F C
⊢ a.normalizeObj' ⟶
    (tensorObj (𝒞 := categoryFreeMonoidalCategory) a ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory))).normalizeObj'

Tactic:
exact Discrete.natTrans (fun _ => 𝟙 _)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Discrete.natTrans, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y : F C
f : X ⟶ Y
n : (Discrete ∘ NormalMonoidalObject) C
⊢ ((tensorFunc C).map f).app n = obj inclusion { as := n.as : Discrete (NormalMonoidalObject C) } ◁ f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
Z : F C
n n' : (Discrete ∘ NormalMonoidalObject) C
f : n ⟶ n'
mk :
  ∀ (as : NormalMonoidalObject C) (f : { as := as : Discrete (NormalMonoidalObject C) } ⟶ n'),
    ((tensorFunc C).obj Z).map f = map inclusion f ▷ Z
⊢ ((tensorFunc C).obj Z).map f = map inclusion f ▷ Z

Tactic:
cases n
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
Z : F C
n' : (Discrete ∘ NormalMonoidalObject) C
as : NormalMonoidalObject C
f : { as := as : Discrete (NormalMonoidalObject C) } ⟶ n'
mk :
  ∀ (as_1 : NormalMonoidalObject C) (f : { as := as : Discrete (NormalMonoidalObject C) } ⟶ { as := as_1 }),
    ((tensorFunc C).obj Z).map f = map inclusion f ▷ Z
⊢ ((tensorFunc C).obj Z).map f = map inclusion f ▷ Z

Tactic:
cases n'
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
Z : F C
as as_1 : NormalMonoidalObject C
f : { as := as : Discrete (NormalMonoidalObject C) } ⟶ { as := as_1 }
mk :
  ∀ (h : { as := as : Discrete (NormalMonoidalObject C) }.as = { as := as_1 }.as),
    ((tensorFunc C).obj Z).map
        {
          down :=
            { down := h :
              PLift
                ({ as := as : Discrete (NormalMonoidalObject C) }.as =
                  { as := as_1 : Discrete (NormalMonoidalObject C) }.as) } :
          ULift.{u, 0}
            (PLift
              ({ as := as : Discrete (NormalMonoidalObject C) }.as =
                { as := as_1 : Discrete (NormalMonoidalObject C) }.as)) } =
      map inclusion { down := { down := h } } ▷ Z
⊢ ((tensorFunc C).obj Z).map f = map inclusion f ▷ Z

Tactic:
rcases f with ⟨⟨h⟩⟩
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
Z : F C
as as_1 : NormalMonoidalObject C
h : as = as_1
mk :
  ((tensorFunc C).obj Z).map
      {
        down :=
          { down := ⋯ :
            PLift
              ({ as := as : Discrete (NormalMonoidalObject C) }.as =
                { as := as : Discrete (NormalMonoidalObject C) }.as) } :
        ULift.{u, 0}
          (PLift
            ({ as := as : Discrete (NormalMonoidalObject C) }.as =
              { as := as : Discrete (NormalMonoidalObject C) }.as)) } =
    map inclusion { down := { down := ⋯ } } ▷ Z
⊢ ((tensorFunc C).obj Z).map
      {
        down :=
          { down := h :
            PLift
              ({ as := as : Discrete (NormalMonoidalObject C) }.as =
                { as := as_1 : Discrete (NormalMonoidalObject C) }.as) } :
        ULift.{u, 0}
          (PLift
            ({ as := as : Discrete (NormalMonoidalObject C) }.as =
              { as := as_1 : Discrete (NormalMonoidalObject C) }.as)) } =
    map inclusion { down := { down := h } } ▷ Z

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
Z : F C
as : NormalMonoidalObject C
⊢ ((tensorFunc C).obj Z).map
      {
        down :=
          { down := ⋯ :
            PLift
              ({ as := as : Discrete (NormalMonoidalObject C) }.as =
                { as := as : Discrete (NormalMonoidalObject C) }.as) } :
        ULift.{u, 0}
          (PLift
            ({ as := as : Discrete (NormalMonoidalObject C) }.as =
              { as := as : Discrete (NormalMonoidalObject C) }.as)) } =
    map inclusion { down := { down := ⋯ } } ▷ Z

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y : F C
n : (Discrete ∘ NormalMonoidalObject) C
rw :
  Iso.symm (α_ (obj inclusion { as := n.as : Discrete (NormalMonoidalObject C) }) X Y) ≪≫
      normalizeIsoApp' C X n.as ▷ᵢ Y ≪≫
        normalizeIsoApp C Y { as := X.normalizeObj n.as : Discrete (NormalMonoidalObject C) } =
    Iso.symm (α_ (inclusionObj n.as) X Y) ≪≫
      normalizeIsoApp' C X n.as ▷ᵢ Y ≪≫ normalizeIsoApp' C Y (X.normalizeObj n.as)
⊢ Iso.symm (α_ (obj inclusion { as := n.as : Discrete (NormalMonoidalObject C) }) X Y) ≪≫
      normalizeIsoApp C X n ▷ᵢ Y ≪≫
        normalizeIsoApp C Y { as := X.normalizeObj n.as : Discrete (NormalMonoidalObject C) } =
    Iso.symm (α_ (inclusionObj n.as) X Y) ≪≫
      normalizeIsoApp' C X n.as ▷ᵢ Y ≪≫ normalizeIsoApp' C Y (X.normalizeObj n.as)

Tactic:
rw [normalizeIsoApp_eq X n]
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y : F C
n : (Discrete ∘ NormalMonoidalObject) C
rw :
  Iso.symm (α_ (obj inclusion { as := n.as : Discrete (NormalMonoidalObject C) }) X Y) ≪≫
      normalizeIsoApp' C X n.as ▷ᵢ Y ≪≫
        normalizeIsoApp' C Y { as := X.normalizeObj n.as : Discrete (NormalMonoidalObject C) }.as =
    Iso.symm (α_ (inclusionObj n.as) X Y) ≪≫
      normalizeIsoApp' C X n.as ▷ᵢ Y ≪≫ normalizeIsoApp' C Y (X.normalizeObj n.as)
⊢ Iso.symm (α_ (obj inclusion { as := n.as : Discrete (NormalMonoidalObject C) }) X Y) ≪≫
      normalizeIsoApp' C X n.as ▷ᵢ Y ≪≫
        normalizeIsoApp C Y { as := X.normalizeObj n.as : Discrete (NormalMonoidalObject C) } =
    Iso.symm (α_ (inclusionObj n.as) X Y) ≪≫
      normalizeIsoApp' C X n.as ▷ᵢ Y ≪≫ normalizeIsoApp' C Y (X.normalizeObj n.as)

Tactic:
rw [normalizeIsoApp_eq Y ⟨normalizeObj X n.as⟩]

Premises used: CategoryTheory.Discrete.mk, CategoryTheory.FreeMonoidalCategory.normalizeObj, CategoryTheory.Discrete.as
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ Iso.symm (α_ (obj inclusion { as := n.as : Discrete (NormalMonoidalObject C) }) X Y) ≪≫
      normalizeIsoApp' C X n.as ▷ᵢ Y ≪≫
        normalizeIsoApp' C Y { as := X.normalizeObj n.as : Discrete (NormalMonoidalObject C) }.as =
    Iso.symm (α_ (inclusionObj n.as) X Y) ≪≫
      normalizeIsoApp' C X n.as ▷ᵢ Y ≪≫ normalizeIsoApp' C Y (X.normalizeObj n.as)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ normalizeIsoApp C (tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) n =
    Iso.symm (α_ (obj inclusion { as := n.as : Discrete (NormalMonoidalObject C) }) X Y) ≪≫
      normalizeIsoApp C X n ▷ᵢ Y ≪≫
        normalizeIsoApp C Y { as := X.normalizeObj n.as : Discrete (NormalMonoidalObject C) }

Tactic:
rfl

Premises used: CategoryTheory.FreeMonoidalCategory.normalizeObj, CategoryTheory.FreeMonoidalCategory.normalizeIsoApp, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
n : (Discrete ∘ NormalMonoidalObject) C
⊢ normalizeIsoApp C ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) n =
    ρ_ (obj inclusion { as := n.as : Discrete (NormalMonoidalObject C) })

Tactic:
rfl

Premises used: CategoryTheory.FreeMonoidalCategory.normalizeIsoApp, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X_1 : F C
X Y : NormalMonoidalObject C
f : X = Y
subst :
  ((tensorFunc C).obj X_1).map
        {
          down :=
            { down := ⋯ :
              PLift
                ({ as := X : Discrete (NormalMonoidalObject C) }.as =
                  { as := X : Discrete (NormalMonoidalObject C) }.as) } :
          ULift.{u, 0}
            (PLift
              ({ as := X : Discrete (NormalMonoidalObject C) }.as =
                { as := X : Discrete (NormalMonoidalObject C) }.as)) } ≫
      Iso.hom (normalizeIsoApp C X_1 { as := X : Discrete (NormalMonoidalObject C) }) =
    Iso.hom (normalizeIsoApp C X_1 { as := X }) ≫
      ((normalize' C).obj X_1).map
        {
          down :=
            { down := ⋯ :
              PLift
                ({ as := X : Discrete (NormalMonoidalObject C) }.as =
                  { as := X : Discrete (NormalMonoidalObject C) }.as) } :
          ULift.{u, 0}
            (PLift
              ({ as := X : Discrete (NormalMonoidalObject C) }.as =
                { as := X : Discrete (NormalMonoidalObject C) }.as)) }
⊢ ((tensorFunc C).obj X_1).map
        {
          down :=
            { down := f :
              PLift
                ({ as := X : Discrete (NormalMonoidalObject C) }.as =
                  { as := Y : Discrete (NormalMonoidalObject C) }.as) } :
          ULift.{u, 0}
            (PLift
              ({ as := X : Discrete (NormalMonoidalObject C) }.as =
                { as := Y : Discrete (NormalMonoidalObject C) }.as)) } ≫
      Iso.hom (normalizeIsoApp C X_1 { as := Y : Discrete (NormalMonoidalObject C) }) =
    Iso.hom (normalizeIsoApp C X_1 { as := X }) ≫
      ((normalize' C).obj X_1).map
        {
          down :=
            { down := f :
              PLift
                ({ as := X : Discrete (NormalMonoidalObject C) }.as =
                  { as := Y : Discrete (NormalMonoidalObject C) }.as) } :
          ULift.{u, 0}
            (PLift
              ({ as := X : Discrete (NormalMonoidalObject C) }.as =
                { as := Y : Discrete (NormalMonoidalObject C) }.as)) }

Tactic:
subst f
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X_1 : F C
X : NormalMonoidalObject C
dsimp :
  map
        (Discrete.functor fun (n : NormalMonoidalObject C) ↦
          tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n) X_1)
        (𝟙 { as := X : Discrete (NormalMonoidalObject C) }) ≫
      Iso.hom (normalizeIsoApp C X_1 { as := X : Discrete (NormalMonoidalObject C) }) =
    Iso.hom (normalizeIsoApp C X_1 { as := X : Discrete (NormalMonoidalObject C) }) ≫
      𝟙 (inclusionObj (X_1.normalizeObj'.obj { as := X }).as)
⊢ ((tensorFunc C).obj X_1).map
        {
          down :=
            { down := ⋯ :
              PLift
                ({ as := X : Discrete (NormalMonoidalObject C) }.as =
                  { as := X : Discrete (NormalMonoidalObject C) }.as) } :
          ULift.{u, 0}
            (PLift
              ({ as := X : Discrete (NormalMonoidalObject C) }.as =
                { as := X : Discrete (NormalMonoidalObject C) }.as)) } ≫
      Iso.hom (normalizeIsoApp C X_1 { as := X : Discrete (NormalMonoidalObject C) }) =
    Iso.hom (normalizeIsoApp C X_1 { as := X }) ≫
      ((normalize' C).obj X_1).map
        {
          down :=
            { down := ⋯ :
              PLift
                ({ as := X : Discrete (NormalMonoidalObject C) }.as =
                  { as := X : Discrete (NormalMonoidalObject C) }.as) } :
          ULift.{u, 0}
            (PLift
              ({ as := X : Discrete (NormalMonoidalObject C) }.as =
                { as := X : Discrete (NormalMonoidalObject C) }.as)) }

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X_1 : F C
X : NormalMonoidalObject C
⊢ map
        (Discrete.functor fun (n : NormalMonoidalObject C) ↦
          tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n) X_1)
        (𝟙 { as := X : Discrete (NormalMonoidalObject C) }) ≫
      Iso.hom (normalizeIsoApp C X_1 { as := X : Discrete (NormalMonoidalObject C) }) =
    Iso.hom (normalizeIsoApp C X_1 { as := X : Discrete (NormalMonoidalObject C) }) ≫
      𝟙 (inclusionObj (X_1.normalizeObj'.obj { as := X }).as)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
n : NormalMonoidalObject C
X Y : F C
f : X ⟶ Y
mk : ∀ (f' : X ⟶ᵐ Y), X.normalizeObj n = Y.normalizeObj n
⊢ X.normalizeObj n = Y.normalizeObj n

Tactic:
rcases f with ⟨f'⟩
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
n : NormalMonoidalObject C
X Y : F C
f : X ⟶ Y
f' : X ⟶ᵐ Y
mk : (fun (n : NormalMonoidalObject C) ↦ X.normalizeObj n) = Y.normalizeObj
⊢ X.normalizeObj n = Y.normalizeObj n

Tactic:
apply @congr_fun _ _ fun n => normalizeObj X n

Premises used: congr_fun
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y X_1 Y_1 Z : F C
f : X_1 ⟶ᵐ Y_1
g : Y_1 ⟶ᵐ Z
f_ih : (fun (n : NormalMonoidalObject C) ↦ X_1.normalizeObj n) = Y_1.normalizeObj
g_ih : (fun (n : NormalMonoidalObject C) ↦ Y_1.normalizeObj n) = Z.normalizeObj
mk : (fun (n : NormalMonoidalObject C) ↦ X_1.normalizeObj n) = Y_1.normalizeObj
mk₁ : Y_1.normalizeObj = Z.normalizeObj
mk₂ : (x : NormalMonoidalObject C) → NormalMonoidalObject C
⊢ (fun (n : NormalMonoidalObject C) ↦ X_1.normalizeObj n) = Z.normalizeObj

Tactic:
apply Eq.trans

Premises used: Eq.trans
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y X_1 Y_1 Z : F C
f : X_1 ⟶ᵐ Y_1
g : Y_1 ⟶ᵐ Z
f_ih : (fun (n : NormalMonoidalObject C) ↦ X_1.normalizeObj n) = Y_1.normalizeObj
g_ih : (fun (n : NormalMonoidalObject C) ↦ Y_1.normalizeObj n) = Z.normalizeObj
⊢ (fun (n : NormalMonoidalObject C) ↦ X_1.normalizeObj n) = Y_1.normalizeObj

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y X_1 Y_1 Z : F C
f : X_1 ⟶ᵐ Y_1
g : Y_1 ⟶ᵐ Z
f_ih : (fun (n : NormalMonoidalObject C) ↦ X_1.normalizeObj n) = Y_1.normalizeObj
g_ih : (fun (n : NormalMonoidalObject C) ↦ Y_1.normalizeObj n) = Z.normalizeObj
⊢ Y_1.normalizeObj = Z.normalizeObj

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y X_1 Y₁ Y₂ : F C
f : Y₁ ⟶ᵐ Y₂
ih : (fun (n : NormalMonoidalObject C) ↦ Y₁.normalizeObj n) = Y₂.normalizeObj
mk : ∀ (x : NormalMonoidalObject C), (X_1.tensor Y₁).normalizeObj x = (X_1.tensor Y₂).normalizeObj x
⊢ (fun (n : NormalMonoidalObject C) ↦ (X_1.tensor Y₁).normalizeObj n) = (X_1.tensor Y₂).normalizeObj

Tactic:
funext
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y X_1 Y₁ Y₂ : F C
f : Y₁ ⟶ᵐ Y₂
ih : (fun (n : NormalMonoidalObject C) ↦ Y₁.normalizeObj n) = Y₂.normalizeObj
x : NormalMonoidalObject C
⊢ (X_1.tensor Y₁).normalizeObj x = (X_1.tensor Y₂).normalizeObj x

Tactic:
apply congr_fun ih

Premises used: congr_fun
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y X₁ X₂ : F C
f : X₁ ⟶ᵐ X₂
Y_1 : F C
ih : (fun (n : NormalMonoidalObject C) ↦ X₁.normalizeObj n) = X₂.normalizeObj
mk : ∀ (x : NormalMonoidalObject C), (X₁.tensor Y_1).normalizeObj x = (X₂.tensor Y_1).normalizeObj x
⊢ (fun (n : NormalMonoidalObject C) ↦ (X₁.tensor Y_1).normalizeObj n) = (X₂.tensor Y_1).normalizeObj

Tactic:
funext