awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x : NormalMonoidalObject C
⊢ (X₁.tensor Y_1).normalizeObj x = (X₂.tensor Y_1).normalizeObj x

Tactic:
apply congr_arg₂ _ rfl (congr_fun ih _)

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

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

Tactic:
simp [congr_fun ih₁ n, congr_fun ih₂ (normalizeObj Y n)]

Premises used: CategoryTheory.FreeMonoidalCategory.normalizeObj, congr_fun
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y X_1 : F C
mk : ∀ (x : NormalMonoidalObject C), X_1.normalizeObj x = X_1.normalizeObj x
⊢ (fun (n : NormalMonoidalObject C) ↦ X_1.normalizeObj n) = X_1.normalizeObj

Tactic:
funext
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y X_1 : F C
x : NormalMonoidalObject C
⊢ X_1.normalizeObj x = X_1.normalizeObj x

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y X_1 Y_1 Z : F C
mk :
  ∀ (x : NormalMonoidalObject C),
    ((X_1.tensor Y_1).tensor Z).normalizeObj x = (X_1.tensor (Y_1.tensor Z)).normalizeObj x
⊢ (fun (n : NormalMonoidalObject C) ↦ ((X_1.tensor Y_1).tensor Z).normalizeObj n) =
    (X_1.tensor (Y_1.tensor Z)).normalizeObj

Tactic:
funext
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y X_1 Y_1 Z : F C
x : NormalMonoidalObject C
⊢ ((X_1.tensor Y_1).tensor Z).normalizeObj x = (X_1.tensor (Y_1.tensor Z)).normalizeObj x

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y X_1 Y_1 Z : F C
mk :
  ∀ (x : NormalMonoidalObject C),
    (X_1.tensor (Y_1.tensor Z)).normalizeObj x = ((X_1.tensor Y_1).tensor Z).normalizeObj x
⊢ (fun (n : NormalMonoidalObject C) ↦ (X_1.tensor (Y_1.tensor Z)).normalizeObj n) =
    ((X_1.tensor Y_1).tensor Z).normalizeObj

Tactic:
funext
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y X_1 Y_1 Z : F C
x : NormalMonoidalObject C
⊢ (X_1.tensor (Y_1.tensor Z)).normalizeObj x = ((X_1.tensor Y_1).tensor Z).normalizeObj x

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y X_1 : F C
mk : ∀ (x : NormalMonoidalObject C), (tensor unit X_1).normalizeObj x = X_1.normalizeObj x
⊢ (fun (n : NormalMonoidalObject C) ↦ (tensor unit X_1).normalizeObj n) = X_1.normalizeObj

Tactic:
funext
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y X_1 : F C
x : NormalMonoidalObject C
⊢ (tensor unit X_1).normalizeObj x = X_1.normalizeObj x

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y X_1 : F C
mk : ∀ (x : NormalMonoidalObject C), X_1.normalizeObj x = (tensor unit X_1).normalizeObj x
⊢ (fun (n : NormalMonoidalObject C) ↦ X_1.normalizeObj n) = (tensor unit X_1).normalizeObj

Tactic:
funext
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y X_1 : F C
x : NormalMonoidalObject C
⊢ X_1.normalizeObj x = (tensor unit X_1).normalizeObj x

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y X_1 : F C
mk : ∀ (x : NormalMonoidalObject C), (X_1.tensor unit).normalizeObj x = X_1.normalizeObj x
⊢ (fun (n : NormalMonoidalObject C) ↦ (X_1.tensor unit).normalizeObj n) = X_1.normalizeObj

Tactic:
funext
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y X_1 : F C
x : NormalMonoidalObject C
⊢ (X_1.tensor unit).normalizeObj x = X_1.normalizeObj x

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y X_1 : F C
mk : ∀ (x : NormalMonoidalObject C), X_1.normalizeObj x = (X_1.tensor unit).normalizeObj x
⊢ (fun (n : NormalMonoidalObject C) ↦ X_1.normalizeObj n) = (X_1.tensor unit).normalizeObj

Tactic:
funext
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y X_1 : F C
x : NormalMonoidalObject C
⊢ X_1.normalizeObj x = (X_1.tensor unit).normalizeObj x

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y : F C
f' : X ⟶ᵐ Y
mk :
  ∀ {X Y Z : F C} (f : X ⟶ᵐ Y) (g : Y ⟶ᵐ Z),
    (fun (n : NormalMonoidalObject C) ↦ X.normalizeObj n) = Y.normalizeObj →
      (fun (n : NormalMonoidalObject C) ↦ Y.normalizeObj n) = Z.normalizeObj →
        (fun (n : NormalMonoidalObject C) ↦ X.normalizeObj n) = Z.normalizeObj
mk₁ :
  ∀ (X : F C) {Y₁ Y₂ : F C} (f : Y₁ ⟶ᵐ Y₂)
    (ih : (fun (n : NormalMonoidalObject C) ↦ Y₁.normalizeObj n) = Y₂.normalizeObj),
    (fun (n : NormalMonoidalObject C) ↦ (X.tensor Y₁).normalizeObj n) = (X.tensor Y₂).normalizeObj
mk₂ :
  ∀ {X₁ X₂ : F C} (f : X₁ ⟶ᵐ X₂) (Y : F C)
    (ih : (fun (n : NormalMonoidalObject C) ↦ X₁.normalizeObj n) = X₂.normalizeObj),
    (fun (n : NormalMonoidalObject C) ↦ (X₁.tensor Y).normalizeObj n) = (X₂.tensor Y).normalizeObj
mk₃ :
  ∀ {W X Y Z : F C} (f : W ⟶ᵐ Y) (g : X ⟶ᵐ Z)
    (ih₁ : (fun (n : NormalMonoidalObject C) ↦ W.normalizeObj n) = Y.normalizeObj)
    (ih₂ : (fun (n : NormalMonoidalObject C) ↦ X.normalizeObj n) = Z.normalizeObj),
    (fun (n : NormalMonoidalObject C) ↦ (W.tensor X).normalizeObj n) = (Y.tensor Z).normalizeObj
mk₄ : ∀ (X : F C), (fun (n : NormalMonoidalObject C) ↦ X.normalizeObj n) = X.normalizeObj
mk₅ :
  ∀ (X Y Z : F C),
    (fun (n : NormalMonoidalObject C) ↦ ((X.tensor Y).tensor Z).normalizeObj n) = (X.tensor (Y.tensor Z)).normalizeObj
mk₆ :
  ∀ (X Y Z : F C),
    (fun (n : NormalMonoidalObject C) ↦ (X.tensor (Y.tensor Z)).normalizeObj n) = ((X.tensor Y).tensor Z).normalizeObj
mk₇ : ∀ (X : F C), (fun (n : NormalMonoidalObject C) ↦ (tensor unit X).normalizeObj n) = X.normalizeObj
mk₈ : ∀ (X : F C), (fun (n : NormalMonoidalObject C) ↦ X.normalizeObj n) = (tensor unit X).normalizeObj
mk₉ : ∀ (X : F C), (fun (n : NormalMonoidalObject C) ↦ (X.tensor unit).normalizeObj n) = X.normalizeObj
mk₁₀ : ∀ (X : F C), (fun (n : NormalMonoidalObject C) ↦ X.normalizeObj n) = (X.tensor unit).normalizeObj
⊢ (fun (n : NormalMonoidalObject C) ↦ X.normalizeObj n) = Y.normalizeObj

Tactic:
induction f' with
  | comp _ _ _ _ => apply Eq.trans <;> assumption
  | whiskerLeft _ _ ih => funext; apply congr_fun ih
  | whiskerRight _ _ ih => funext; apply congr_arg₂ _ rfl (congr_fun ih _)
  | @tensor W X Y Z _ _ ih₁ ih₂ =>
      funext n
      simp [congr_fun ih₁ n, congr_fun ih₂ (normalizeObj Y n)]
  | _ => funext; rfl

Premises used: CategoryTheory.Functor.comp, Eq.trans, CategoryTheory.FreeMonoidalCategory.tensor
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
n : NormalMonoidalObject C
X Y : F C
f : X ⟶ Y
revert :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ map inclusion (eqToHom ⋯)
⊢ inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ map inclusion (eqToHom ⋯)

Tactic:
revert n
-- 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
ihf :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y_1 n).hom = (normalizeIsoApp' C X_1 n).hom ≫ map inclusion (eqToHom ⋯)
ihg :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ g ≫ (normalizeIsoApp' C Z n).hom = (normalizeIsoApp' C Y_1 n).hom ≫ map inclusion (eqToHom ⋯)
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ (f ≫ g) ≫ (normalizeIsoApp' C Z n).hom = (normalizeIsoApp' C X_1 n).hom ≫ map inclusion (eqToHom ⋯)

Tactic:
simp [ihg, reassoc_of% (ihf _)]
-- 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
h :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y_1 n).hom = (normalizeIsoApp' C X_1 n).hom ≫ map inclusion (eqToHom ⋯)
h_1 :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ g ≫ (normalizeIsoApp' C Z n).hom = (normalizeIsoApp' C Y_1 n).hom ≫ map inclusion (eqToHom ⋯)
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ (f ≫ g) ≫ (normalizeIsoApp' C Z n).hom = (normalizeIsoApp' C X_1 n).hom ≫ map inclusion (eqToHom ⋯)

Tactic:
case comp f g ihf ihg => simp [ihg, reassoc_of% (ihf _)]

Premises used: CategoryTheory.Functor.comp
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X_1 Y_1 X' X Y : F C
f : X ⟶ Y
ih :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ map inclusion (eqToHom ⋯)
n : NormalMonoidalObject C
dsimp :
  inclusionObj n ◁ X' ◁ f ≫
      Iso.inv (α_ (inclusionObj n) X' Y) ≫
        (normalizeIsoApp' C X' n).hom ▷ Y ≫ Iso.hom (normalizeIsoApp' C Y (X'.normalizeObj n)) =
    (Iso.inv (α_ (inclusionObj n) X' X) ≫
        (normalizeIsoApp' C X' n).hom ▷ X ≫ Iso.hom (normalizeIsoApp' C X (X'.normalizeObj n))) ≫
      map inclusion (eqToHom ⋯)
⊢ Eq (α :=
    tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n)
        (tensorObj (𝒞 := categoryFreeMonoidalCategory) X' X) ⟶
      inclusionObj ((tensorObj (𝒞 := categoryFreeMonoidalCategory) X' Y).normalizeObj n))
    (inclusionObj n ◁ X' ◁ f ≫ Iso.hom (normalizeIsoApp' C (tensorObj (𝒞 := categoryFreeMonoidalCategory) X' Y) n))
    (Iso.hom (normalizeIsoApp' C (tensorObj (𝒞 := categoryFreeMonoidalCategory) X' X) n) ≫ map inclusion (eqToHom ⋯))

Tactic:
dsimp only [normalizeObj_tensor, normalizeIsoApp', tensor_eq_tensor, Iso.trans_hom,
      Iso.symm_hom, whiskerRightIso_hom, Function.comp_apply, inclusion_obj]

Premises used: CategoryTheory.FreeMonoidalCategory.inclusion_obj, CategoryTheory.FreeMonoidalCategory.tensor_eq_tensor, CategoryTheory.FreeMonoidalCategory.normalizeObj_tensor, CategoryTheory.Iso.symm_hom, CategoryTheory.FreeMonoidalCategory.normalizeIsoApp', CategoryTheory.Iso.trans_hom, CategoryTheory.MonoidalCategory.whiskerRightIso_hom, Function.comp_apply
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X_1 Y_1 X' X Y : F C
f : X ⟶ Y
ih :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ map inclusion (eqToHom ⋯)
n : NormalMonoidalObject C
rw :
  Eq (α :=
    tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n)
        (tensorObj (𝒞 := categoryFreeMonoidalCategory) X' X) ⟶
      inclusionObj (Y.normalizeObj (X'.normalizeObj n)))
    (Iso.inv (α_ (inclusionObj n) X' X) ≫
      (normalizeIsoApp' C X' n).hom ▷ X ≫
        Iso.hom (normalizeIsoApp' C X (X'.normalizeObj n)) ≫ map inclusion (eqToHom ⋯))
    ((Iso.inv (α_ (inclusionObj n) X' X) ≫
        (normalizeIsoApp' C X' n).hom ▷ X ≫ Iso.hom (normalizeIsoApp' C X (X'.normalizeObj n))) ≫
      map inclusion (eqToHom ⋯))
⊢ inclusionObj n ◁ X' ◁ f ≫
      Iso.inv (α_ (inclusionObj n) X' Y) ≫
        (normalizeIsoApp' C X' n).hom ▷ Y ≫ Iso.hom (normalizeIsoApp' C Y (X'.normalizeObj n)) =
    (Iso.inv (α_ (inclusionObj n) X' X) ≫
        (normalizeIsoApp' C X' n).hom ▷ X ≫ Iso.hom (normalizeIsoApp' C X (X'.normalizeObj n))) ≫
      map inclusion (eqToHom ⋯)

Tactic:
rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc, ih]

Premises used: CategoryTheory.MonoidalCategory.associator_inv_naturality_right_assoc, CategoryTheory.MonoidalCategory.whisker_exchange_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X_1 Y_1 X' X Y : F C
f : X ⟶ Y
ih :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ map inclusion (eqToHom ⋯)
n : NormalMonoidalObject C
⊢ Eq (α :=
    tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n)
        (tensorObj (𝒞 := categoryFreeMonoidalCategory) X' X) ⟶
      inclusionObj (Y.normalizeObj (X'.normalizeObj n)))
    (Iso.inv (α_ (inclusionObj n) X' X) ≫
      (normalizeIsoApp' C X' n).hom ▷ X ≫
        Iso.hom (normalizeIsoApp' C X (X'.normalizeObj n)) ≫ map inclusion (eqToHom ⋯))
    ((Iso.inv (α_ (inclusionObj n) X' X) ≫
        (normalizeIsoApp' C X' n).hom ▷ X ≫ Iso.hom (normalizeIsoApp' C X (X'.normalizeObj n))) ≫
      map inclusion (eqToHom ⋯))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y X_1 Y_1 Z : F C
f : Y_1 ⟶ Z
h :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ f ≫ (normalizeIsoApp' C Z n).hom = (normalizeIsoApp' C Y_1 n).hom ≫ map inclusion (eqToHom ⋯)
⊢ ∀ (n : NormalMonoidalObject C),
    Eq (α :=
      tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n)
          (tensorObj (𝒞 := categoryFreeMonoidalCategory) X_1 Y_1) ⟶
        inclusionObj ((tensorObj (𝒞 := categoryFreeMonoidalCategory) X_1 Z).normalizeObj n))
      (inclusionObj n ◁ X_1 ◁ f ≫ Iso.hom (normalizeIsoApp' C (tensorObj (𝒞 := categoryFreeMonoidalCategory) X_1 Z) n))
      (Iso.hom (normalizeIsoApp' C (tensorObj (𝒞 := categoryFreeMonoidalCategory) X_1 Y_1) n) ≫
        map inclusion (eqToHom ⋯))

Tactic:
case whiskerLeft X' X Y f ih =>
    intro n
    dsimp only [normalizeObj_tensor, normalizeIsoApp', tensor_eq_tensor, Iso.trans_hom,
      Iso.symm_hom, whiskerRightIso_hom, Function.comp_apply, inclusion_obj]
    rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc, ih]
    simp

Premises used: CategoryTheory.FreeMonoidalCategory.inclusion_obj, CategoryTheory.MonoidalCategory.associator_inv_naturality_right_assoc, CategoryTheory.FreeMonoidalCategory.tensor_eq_tensor, CategoryTheory.FreeMonoidalCategory.normalizeObj_tensor, CategoryTheory.Iso.symm_hom, CategoryTheory.FreeMonoidalCategory.normalizeIsoApp', CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.Iso.trans_hom, CategoryTheory.MonoidalCategory.whiskerRightIso_hom, Function.comp_apply
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X_1 Y_1 X Y : F C
h : X ⟶ Y
η' : F C
ih :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ h ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ map inclusion (eqToHom ⋯)
n : NormalMonoidalObject C
dsimp :
  inclusionObj n ◁ h ▷ η' ≫
      Iso.inv (α_ (inclusionObj n) Y η') ≫
        (normalizeIsoApp' C Y n).hom ▷ η' ≫ Iso.hom (normalizeIsoApp' C η' (Y.normalizeObj n)) =
    (Iso.inv (α_ (inclusionObj n) X η') ≫
        (normalizeIsoApp' C X n).hom ▷ η' ≫ Iso.hom (normalizeIsoApp' C η' (X.normalizeObj n))) ≫
      map inclusion (eqToHom ⋯)
⊢ Eq (α :=
    tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n)
        (tensorObj (𝒞 := categoryFreeMonoidalCategory) X η') ⟶
      inclusionObj ((tensorObj (𝒞 := categoryFreeMonoidalCategory) Y η').normalizeObj n))
    (inclusionObj n ◁ h ▷ η' ≫ Iso.hom (normalizeIsoApp' C (tensorObj (𝒞 := categoryFreeMonoidalCategory) Y η') n))
    (Iso.hom (normalizeIsoApp' C (tensorObj (𝒞 := categoryFreeMonoidalCategory) X η') n) ≫ map inclusion (eqToHom ⋯))

Tactic:
dsimp only [normalizeObj_tensor, normalizeIsoApp', tensor_eq_tensor, Iso.trans_hom,
      Iso.symm_hom, whiskerRightIso_hom, Function.comp_apply, inclusion_obj]

Premises used: CategoryTheory.FreeMonoidalCategory.inclusion_obj, CategoryTheory.FreeMonoidalCategory.tensor_eq_tensor, CategoryTheory.FreeMonoidalCategory.normalizeObj_tensor, CategoryTheory.Iso.symm_hom, CategoryTheory.FreeMonoidalCategory.normalizeIsoApp', CategoryTheory.Iso.trans_hom, CategoryTheory.MonoidalCategory.whiskerRightIso_hom, Function.comp_apply
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X_1 Y_1 X Y : F C
h : X ⟶ Y
η' : F C
ih :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ h ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ map inclusion (eqToHom ⋯)
n : NormalMonoidalObject C
rw :
  Eq (α :=
    tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n)
        (tensorObj (𝒞 := categoryFreeMonoidalCategory) X η') ⟶
      inclusionObj (η'.normalizeObj (Y.normalizeObj n)))
    (Iso.inv (α_ (inclusionObj n) X η') ≫
      ((normalizeIsoApp' C X n).hom ≫ map inclusion (eqToHom ⋯)) ▷ η' ≫
        Iso.hom (normalizeIsoApp' C η' (Y.normalizeObj n)))
    ((Iso.inv (α_ (inclusionObj n) X η') ≫
        (normalizeIsoApp' C X n).hom ▷ η' ≫ Iso.hom (normalizeIsoApp' C η' (X.normalizeObj n))) ≫
      map inclusion (eqToHom ⋯))
⊢ inclusionObj n ◁ h ▷ η' ≫
      Iso.inv (α_ (inclusionObj n) Y η') ≫
        (normalizeIsoApp' C Y n).hom ▷ η' ≫ Iso.hom (normalizeIsoApp' C η' (Y.normalizeObj n)) =
    (Iso.inv (α_ (inclusionObj n) X η') ≫
        (normalizeIsoApp' C X n).hom ▷ η' ≫ Iso.hom (normalizeIsoApp' C η' (X.normalizeObj n))) ≫
      map inclusion (eqToHom ⋯)

Tactic:
rw [associator_inv_naturality_middle_assoc, ← comp_whiskerRight_assoc, ih]

Premises used: CategoryTheory.MonoidalCategory.associator_inv_naturality_middle_assoc, CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X_1 Y_1 X Y : F C
h : X ⟶ Y
η' : F C
ih :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ h ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ map inclusion (eqToHom ⋯)
n : NormalMonoidalObject C
⊢ Eq (α :=
    tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj (X.normalizeObj n)) η' ⟶
      inclusionObj (η'.normalizeObj (X.normalizeObj n)))
    (Iso.hom (normalizeIsoApp' C η' (X.normalizeObj n)))
    (CategoryStruct.comp (Y := tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj (Y.normalizeObj n)) η')
      (eqToHom ⋯) (Iso.hom (normalizeIsoApp' C η' (Y.normalizeObj n)) ≫ eqToHom ⋯))

Tactic:
have := dcongr_arg (fun x => (normalizeIsoApp' C η' x).hom) (normalizeObj_congr n h)
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X_1 Y_1 X Y : F C
h : X ⟶ Y
η' : F C
ih :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ h ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ map inclusion (eqToHom ⋯)
n : NormalMonoidalObject C
this :
  Eq (α :=
    tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj (X.normalizeObj n)) η' ⟶
      inclusionObj (η'.normalizeObj (X.normalizeObj n)))
    (Iso.hom (normalizeIsoApp' C η' (X.normalizeObj n)))
    (CategoryStruct.comp (Y := tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj (Y.normalizeObj n)) η')
      (eqToHom ⋯) (Iso.hom (normalizeIsoApp' C η' (Y.normalizeObj n)) ≫ eqToHom ⋯))
⊢ Eq (α :=
    tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n)
        (tensorObj (𝒞 := categoryFreeMonoidalCategory) X η') ⟶
      inclusionObj (η'.normalizeObj (Y.normalizeObj n)))
    (Iso.inv (α_ (inclusionObj n) X η') ≫
      ((normalizeIsoApp' C X n).hom ≫ map inclusion (eqToHom ⋯)) ▷ η' ≫
        Iso.hom (normalizeIsoApp' C η' (Y.normalizeObj n)))
    ((Iso.inv (α_ (inclusionObj n) X η') ≫
        (normalizeIsoApp' C X n).hom ▷ η' ≫ Iso.hom (normalizeIsoApp' C η' (X.normalizeObj n))) ≫
      map inclusion (eqToHom ⋯))

Tactic:
simp [this]
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y X_1 Y_1 : F C
f : X_1 ⟶ Y_1
Z : F C
h :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y_1 n).hom = (normalizeIsoApp' C X_1 n).hom ≫ map inclusion (eqToHom ⋯)
⊢ ∀ (n : NormalMonoidalObject C),
    Eq (α :=
      tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n)
          (tensorObj (𝒞 := categoryFreeMonoidalCategory) X_1 Z) ⟶
        inclusionObj ((tensorObj (𝒞 := categoryFreeMonoidalCategory) Y_1 Z).normalizeObj n))
      (inclusionObj n ◁ f ▷ Z ≫ Iso.hom (normalizeIsoApp' C (tensorObj (𝒞 := categoryFreeMonoidalCategory) Y_1 Z) n))
      (Iso.hom (normalizeIsoApp' C (tensorObj (𝒞 := categoryFreeMonoidalCategory) X_1 Z) n) ≫ map inclusion (eqToHom ⋯))

Tactic:
case whiskerRight X Y h η' ih =>
    intro n
    dsimp only [normalizeObj_tensor, normalizeIsoApp', tensor_eq_tensor, Iso.trans_hom,
      Iso.symm_hom, whiskerRightIso_hom, Function.comp_apply, inclusion_obj]
    rw [associator_inv_naturality_middle_assoc, ← comp_whiskerRight_assoc, ih]
    have := dcongr_arg (fun x => (normalizeIsoApp' C η' x).hom) (normalizeObj_congr n h)
    simp [this]

Premises used: CategoryTheory.FreeMonoidalCategory.inclusion_obj, CategoryTheory.FreeMonoidalCategory.tensor_eq_tensor, CategoryTheory.FreeMonoidalCategory.normalizeObj_tensor, CategoryTheory.Iso.symm_hom, CategoryTheory.FreeMonoidalCategory.normalizeIsoApp', CategoryTheory.MonoidalCategory.associator_inv_naturality_middle_assoc, CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc, CategoryTheory.Iso.trans_hom, CategoryTheory.MonoidalCategory.whiskerRightIso_hom, Function.comp_apply
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y X_1 : F C
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ 𝟙 X_1 ≫ (normalizeIsoApp' C X_1 n).hom = (normalizeIsoApp' C X_1 n).hom ≫ map inclusion (eqToHom ⋯)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y X_1 Y_1 Z : F C
⊢ ∀ (n : NormalMonoidalObject C),
    Eq (α :=
      tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n)
          (tensorObj (𝒞 := categoryFreeMonoidalCategory) (tensorObj (𝒞 := categoryFreeMonoidalCategory) X_1 Y_1) Z) ⟶
        inclusionObj
          ((tensorObj (𝒞 := categoryFreeMonoidalCategory) X_1
                (tensorObj (𝒞 := categoryFreeMonoidalCategory) Y_1 Z)).normalizeObj
            n))
      (inclusionObj n ◁ Iso.hom (α_ X_1 Y_1 Z) ≫
        Iso.hom
          (normalizeIsoApp' C
            (tensorObj (𝒞 := categoryFreeMonoidalCategory) X_1 (tensorObj (𝒞 := categoryFreeMonoidalCategory) Y_1 Z))
            n))
      (Iso.hom
          (normalizeIsoApp' C
            (tensorObj (𝒞 := categoryFreeMonoidalCategory) (tensorObj (𝒞 := categoryFreeMonoidalCategory) X_1 Y_1) Z)
            n) ≫
        map inclusion (eqToHom ⋯))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y X_1 Y_1 Z : F C
⊢ ∀ (n : NormalMonoidalObject C),
    Eq (α :=
      tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n)
          (tensorObj (𝒞 := categoryFreeMonoidalCategory) X_1 (tensorObj (𝒞 := categoryFreeMonoidalCategory) Y_1 Z)) ⟶
        inclusionObj
          ((tensorObj (𝒞 := categoryFreeMonoidalCategory) (tensorObj (𝒞 := categoryFreeMonoidalCategory) X_1 Y_1)
                Z).normalizeObj
            n))
      (inclusionObj n ◁ Iso.inv (α_ X_1 Y_1 Z) ≫
        Iso.hom
          (normalizeIsoApp' C
            (tensorObj (𝒞 := categoryFreeMonoidalCategory) (tensorObj (𝒞 := categoryFreeMonoidalCategory) X_1 Y_1) Z)
            n))
      (Iso.hom
          (normalizeIsoApp' C
            (tensorObj (𝒞 := categoryFreeMonoidalCategory) X_1 (tensorObj (𝒞 := categoryFreeMonoidalCategory) Y_1 Z))
            n) ≫
        map inclusion (eqToHom ⋯))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence
Goal:
C : Type u
X Y X_1 : F C
⊢ ∀ (n : NormalMonoidalObject C),
    Eq (α :=
      tensorObj (𝒞 := categoryFreeMonoidalCategory) (inclusionObj n)
          (tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X_1) ⟶
        inclusionObj (X_1.normalizeObj n))
      (inclusionObj n ◁ Iso.hom (λ_ X_1) ≫ (normalizeIsoApp' C X_1 n).hom)
      (Iso.hom
          (normalizeIsoApp' C
            (tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X_1) n) ≫
        map inclusion (eqToHom ⋯))

Tactic:
simp