awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F_1 F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₃, v₁', u₃, u₁'} E C'
inst_7 : MonoidalCategory.{v₁', u₁'} C'
inst_8 : F.Monoidal
inst_9 : G.Monoidal
h₁ :
  Eq (α :=
    Quiver.Hom.{v₂, u₂} (V := D) (𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C').1
      (𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C').1)
    (CategoryStruct.comp (Y := (F.prod G).obj ((𝟙_ (C × E)) (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E)))
        (ε (F.prod G)) (η (F.prod G))).1
    (𝟙 ((𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C'))).1
⊢ Eq (α :=
    Quiver.Hom (V := D × C') ((𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C'))
      ((𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C')))
    (CategoryStruct.comp (Y := (F.prod G).obj ((𝟙_ (C × E)) (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E)))
      (ε (F.prod G)) (η (F.prod G)))
    (𝟙 ((𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C')))
have h₂ : Eq (α :=
  Quiver.Hom.{v₁', u₁'} (V := C') (𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C').2
    (𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C').2)
  (CategoryStruct.comp (Y := (F.prod G).obj ((𝟙_ (C × E)) (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E)))
      (ε (F.prod G)) (η (F.prod G))).2
  (𝟙 ((𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C'))).2
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F_1 F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₃, v₁', u₃, u₁'} E C'
inst_7 : MonoidalCategory.{v₁', u₁'} C'
inst_8 : F.Monoidal
inst_9 : G.Monoidal
⊢ CategoryStruct.comp (Y := (𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C')) (η (F.prod G))
      (ε (F.prod G)) =
    𝟙 ((F.prod G).obj ((𝟙_ (C × E)) (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E)))
have h₁ : Eq (α :=
  ((F.prod G).obj ((𝟙_ (C × E)) (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E))).1 ⟶
    ((F.prod G).obj ((𝟙_ (C × E)) (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E))).1)
  (CategoryStruct.comp (Y := (𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C')) (η (F.prod G))
      (ε (F.prod G))).1
  (𝟙 ((F.prod G).obj ((𝟙_ (C × E)) (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E)))).1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F_1 F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₃, v₁', u₃, u₁'} E C'
inst_7 : MonoidalCategory.{v₁', u₁'} C'
inst_8 : F.Monoidal
inst_9 : G.Monoidal
h₁ :
  Eq (α :=
    ((F.prod G).obj ((𝟙_ (C × E)) (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E))).1 ⟶
      ((F.prod G).obj ((𝟙_ (C × E)) (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E))).1)
    (CategoryStruct.comp (Y := (𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C')) (η (F.prod G))
        (ε (F.prod G))).1
    (𝟙 ((F.prod G).obj ((𝟙_ (C × E)) (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E)))).1
⊢ CategoryStruct.comp (Y := (𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C')) (η (F.prod G))
      (ε (F.prod G)) =
    𝟙 ((F.prod G).obj ((𝟙_ (C × E)) (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E)))
have h₂ : Eq (α :=
  ((F.prod G).obj ((𝟙_ (C × E)) (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E))).2 ⟶
    ((F.prod G).obj ((𝟙_ (C × E)) (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E))).2)
  (CategoryStruct.comp (Y := (𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C')) (η (F.prod G))
      (ε (F.prod G))).2
  (𝟙 ((F.prod G).obj ((𝟙_ (C × E)) (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E)))).2
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F_1 F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₃, v₁', u₃, u₁'} E C'
inst_7 : MonoidalCategory.{v₁', u₁'} C'
inst_8 : F.Monoidal
inst_9 : G.Monoidal
x x_1 : C × E
⊢ CategoryStruct.comp (Y := (F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1))
      (μ (F.prod G) x x_1) (δ (F.prod G) x x_1) =
    𝟙 (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1))
have h₁ : Eq (α :=
  (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1)).1 ⟶
    (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1)).1)
  (CategoryStruct.comp (Y := (F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1))
      (μ (F.prod G) x x_1) (δ (F.prod G) x x_1)).1
  (𝟙 (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1))).1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F_1 F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₃, v₁', u₃, u₁'} E C'
inst_7 : MonoidalCategory.{v₁', u₁'} C'
inst_8 : F.Monoidal
inst_9 : G.Monoidal
x x_1 : C × E
h₁ :
  Eq (α :=
    (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1)).1 ⟶
      (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1)).1)
    (CategoryStruct.comp (Y := (F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1))
        (μ (F.prod G) x x_1) (δ (F.prod G) x x_1)).1
    (𝟙 (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1))).1
⊢ CategoryStruct.comp (Y := (F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1))
      (μ (F.prod G) x x_1) (δ (F.prod G) x x_1) =
    𝟙 (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1))
have h₂ : Eq (α :=
  (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1)).2 ⟶
    (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1)).2)
  (CategoryStruct.comp (Y := (F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1))
      (μ (F.prod G) x x_1) (δ (F.prod G) x x_1)).2
  (𝟙 (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1))).2
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F_1 F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₃, v₁', u₃, u₁'} E C'
inst_7 : MonoidalCategory.{v₁', u₁'} C'
inst_8 : F.Monoidal
inst_9 : G.Monoidal
x x_1 : C × E
⊢ CategoryStruct.comp (Y :=
      tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1))
      (δ (F.prod G) x x_1) (μ (F.prod G) x x_1) =
    𝟙 ((F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1))
have h₁ : Eq (α :=
  ((F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1)).1 ⟶
    ((F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1)).1)
  (CategoryStruct.comp (Y :=
      tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1))
      (δ (F.prod G) x x_1) (μ (F.prod G) x x_1)).1
  (𝟙 ((F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1))).1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F_1 F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₃, v₁', u₃, u₁'} E C'
inst_7 : MonoidalCategory.{v₁', u₁'} C'
inst_8 : F.Monoidal
inst_9 : G.Monoidal
x x_1 : C × E
h₁ :
  Eq (α :=
    ((F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1)).1 ⟶
      ((F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1)).1)
    (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1))
        (δ (F.prod G) x x_1) (μ (F.prod G) x x_1)).1
    (𝟙 ((F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1))).1
⊢ CategoryStruct.comp (Y :=
      tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1))
      (δ (F.prod G) x x_1) (μ (F.prod G) x x_1) =
    𝟙 ((F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1))
have h₂ : Eq (α :=
  ((F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1)).2 ⟶
    ((F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1)).2)
  (CategoryStruct.comp (Y :=
      tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1))
      (δ (F.prod G) x x_1) (μ (F.prod G) x x_1)).2
  (𝟙 ((F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1))).2
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_6 : F.LaxMonoidal
inst_7 : G.LaxMonoidal
⊢ Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
      ((F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
    (ε (F.prod' G)).1 (ε F)
have change : Eq (α :=
  (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
    F.obj tensorUnit.{v₁, u₁} (C × C) (𝒞 := uniformProd C C).1)
  ((ε (F.prod G)).1 ≫ F.map (𝟙 tensorUnit.{v₁, u₁} (C × C) (𝒞 := uniformProd C C).1)) (ε F)
Tactic: change _ ≫ F.map (𝟙 _) = _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_6 : F.LaxMonoidal
inst_7 : G.LaxMonoidal
⊢ Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
      F.obj tensorUnit.{v₁, u₁} (C × C) (𝒞 := uniformProd C C).1)
    ((ε (F.prod G)).1 ≫ F.map (𝟙 tensorUnit.{v₁, u₁} (C × C) (𝒞 := uniformProd C C).1)) (ε F)
have rw : Eq (α :=
  (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
    F.obj tensorUnit.{v₁, u₁} (C × C) (𝒞 := uniformProd C C).1)
  (ε (F.prod G)).1 (ε F)
Tactic: rw [Functor.map_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_6 : F.LaxMonoidal
inst_7 : G.LaxMonoidal
⊢ Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2 ⟶
      ((F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2)
    (ε (F.prod' G)).2 (ε G)
have change : Eq (α :=
  (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2 ⟶
    G.obj tensorUnit.{v₁, u₁} (C × C) (𝒞 := uniformProd C C).2)
  ((ε (F.prod G)).2 ≫ G.map (𝟙 tensorUnit.{v₁, u₁} (C × C) (𝒞 := uniformProd C C).2)) (ε G)
Tactic: change _ ≫ G.map (𝟙 _) = _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_6 : F.LaxMonoidal
inst_7 : G.LaxMonoidal
⊢ Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2 ⟶
      G.obj tensorUnit.{v₁, u₁} (C × C) (𝒞 := uniformProd C C).2)
    ((ε (F.prod G)).2 ≫ G.map (𝟙 tensorUnit.{v₁, u₁} (C × C) (𝒞 := uniformProd C C).2)) (ε G)
have rw : Eq (α :=
  (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2 ⟶
    G.obj tensorUnit.{v₁, u₁} (C × C) (𝒞 := uniformProd C C).2)
  (ε (F.prod G)).2 (ε G)
Tactic: rw [Functor.map_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_6 : F.LaxMonoidal
inst_7 : G.LaxMonoidal
X Y : C
⊢ Eq (α :=
    (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj X) ((F.prod' G).obj Y)).1 ⟶
      ((F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).1)
    (μ (F.prod' G) X Y).1 (μ F X Y)
have change : Eq (α :=
  (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((diag C ⋙ F.prod G).obj X)
        ((diag C ⋙ F.prod G).obj Y)).1 ⟶
    F.obj
      (tensorObj.{v₁, u₁} (𝒞 := uniformProd C C) (obj.{v₁, v₁, u₁, u₁} (diag C) X) (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).1)
  ((μ (F.prod G) (obj.{v₁, v₁, u₁, u₁} (diag C) X) (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).1 ≫
    F.map
      (𝟙
        (tensorObj.{v₁, u₁} (𝒞 := uniformProd C C) (obj.{v₁, v₁, u₁, u₁} (diag C) X)
            (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).1))
  (μ F X Y)
Tactic: change _ ≫ F.map (𝟙 _) = _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_6 : F.LaxMonoidal
inst_7 : G.LaxMonoidal
X Y : C
⊢ Eq (α :=
    (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((diag C ⋙ F.prod G).obj X)
          ((diag C ⋙ F.prod G).obj Y)).1 ⟶
      F.obj
        (tensorObj.{v₁, u₁} (𝒞 := uniformProd C C) (obj.{v₁, v₁, u₁, u₁} (diag C) X)
            (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).1)
    ((μ (F.prod G) (obj.{v₁, v₁, u₁, u₁} (diag C) X) (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).1 ≫
      F.map
        (𝟙
          (tensorObj.{v₁, u₁} (𝒞 := uniformProd C C) (obj.{v₁, v₁, u₁, u₁} (diag C) X)
              (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).1))
    (μ F X Y)
have rw : Eq (α :=
  (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((diag C ⋙ F.prod G).obj X)
        ((diag C ⋙ F.prod G).obj Y)).1 ⟶
    F.obj
      (tensorObj.{v₁, u₁} (𝒞 := uniformProd C C) (obj.{v₁, v₁, u₁, u₁} (diag C) X) (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).1)
  (μ (F.prod G) (obj.{v₁, v₁, u₁, u₁} (diag C) X) (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).1 (μ F X Y)
Tactic: rw [Functor.map_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_6 : F.LaxMonoidal
inst_7 : G.LaxMonoidal
X Y : C
⊢ Eq (α :=
    (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj X) ((F.prod' G).obj Y)).2 ⟶
      ((F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).2)
    (μ (F.prod' G) X Y).2 (μ G X Y)
have change : Eq (α :=
  (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((diag C ⋙ F.prod G).obj X)
        ((diag C ⋙ F.prod G).obj Y)).2 ⟶
    G.obj
      (tensorObj.{v₁, u₁} (𝒞 := uniformProd C C) (obj.{v₁, v₁, u₁, u₁} (diag C) X) (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).2)
  ((μ (F.prod G) (obj.{v₁, v₁, u₁, u₁} (diag C) X) (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).2 ≫
    G.map
      (𝟙
        (tensorObj.{v₁, u₁} (𝒞 := uniformProd C C) (obj.{v₁, v₁, u₁, u₁} (diag C) X)
            (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).2))
  (μ G X Y)
Tactic: change _ ≫ G.map (𝟙 _) = _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_6 : F.LaxMonoidal
inst_7 : G.LaxMonoidal
X Y : C
⊢ Eq (α :=
    (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((diag C ⋙ F.prod G).obj X)
          ((diag C ⋙ F.prod G).obj Y)).2 ⟶
      G.obj
        (tensorObj.{v₁, u₁} (𝒞 := uniformProd C C) (obj.{v₁, v₁, u₁, u₁} (diag C) X)
            (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).2)
    ((μ (F.prod G) (obj.{v₁, v₁, u₁, u₁} (diag C) X) (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).2 ≫
      G.map
        (𝟙
          (tensorObj.{v₁, u₁} (𝒞 := uniformProd C C) (obj.{v₁, v₁, u₁, u₁} (diag C) X)
              (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).2))
    (μ G X Y)
have rw : Eq (α :=
  (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((diag C ⋙ F.prod G).obj X)
        ((diag C ⋙ F.prod G).obj Y)).2 ⟶
    G.obj
      (tensorObj.{v₁, u₁} (𝒞 := uniformProd C C) (obj.{v₁, v₁, u₁, u₁} (diag C) X) (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).2)
  (μ (F.prod G) (obj.{v₁, v₁, u₁, u₁} (diag C) X) (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).2 (μ G X Y)
Tactic: rw [Functor.map_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_6 : F.OplaxMonoidal
inst_7 : G.OplaxMonoidal
⊢ Eq (α :=
    ((F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1 ⟶
      (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1)
    (η (F.prod' G)).1 (η F)
have change : Eq (α :=
  F.obj (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1 ⟶
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1)
  (F.map (𝟙 (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1) ≫ (η (F.prod G)).1) (η F)
Tactic: change F.map (𝟙 _) ≫ _ = _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_6 : F.OplaxMonoidal
inst_7 : G.OplaxMonoidal
⊢ Eq (α :=
    F.obj (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1 ⟶
      (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1)
    (F.map (𝟙 (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1) ≫ (η (F.prod G)).1) (η F)
have rw : Eq (α :=
  F.obj (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1 ⟶
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1)
  ((η (F.prod G)).1 :
    ((F.prod G).obj (tensorUnit.{v₁, u₁} (C × C) (𝒞 := uniformProd C C))).1 ⟶
      (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1)
  (η F)
Tactic: rw [Functor.map_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_6 : F.OplaxMonoidal
inst_7 : G.OplaxMonoidal
⊢ Eq (α :=
    ((F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2 ⟶
      (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2)
    (η (F.prod' G)).2 (η G)
have change : Eq (α :=
  G.obj (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2 ⟶
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2)
  (G.map (𝟙 (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2) ≫ (η (F.prod G)).2) (η G)
Tactic: change G.map (𝟙 _) ≫ _ = _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_6 : F.OplaxMonoidal
inst_7 : G.OplaxMonoidal
⊢ Eq (α :=
    G.obj (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2 ⟶
      (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2)
    (G.map (𝟙 (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2) ≫ (η (F.prod G)).2) (η G)
have rw : Eq (α :=
  G.obj (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2 ⟶
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2)
  ((η (F.prod G)).2 :
    ((F.prod G).obj (tensorUnit.{v₁, u₁} (C × C) (𝒞 := uniformProd C C))).2 ⟶
      (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2)
  (η G)
Tactic: rw [Functor.map_id, Category.id_comp]