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
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_6 : F.OplaxMonoidal
inst_7 : G.OplaxMonoidal
X Y : C
⊢ Eq (α :=
    ((F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).1 ⟶
      (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj X) ((F.prod' G).obj Y)).1)
    (δ (F.prod' G) X Y).1 (δ F X Y)
have change : Eq (α :=
  F.obj (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).1 ⟶
    (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.map (𝟙 (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorObj.{v₁, u₁} (𝒞 := inst) X 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: 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
X Y : C
⊢ Eq (α :=
    F.obj (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).1 ⟶
      (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.map (𝟙 (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorObj.{v₁, u₁} (𝒞 := inst) X 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)
have rw : Eq (α :=
  F.obj (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).1 ⟶
    (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.prod G) (obj.{v₁, v₁, u₁, u₁} (diag C) X) (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).1 :
    ((F.prod G).obj
          (tensorObj.{v₁, u₁} (𝒞 := uniformProd C C) (obj.{v₁, v₁, u₁, u₁} (diag C) X)
            (obj.{v₁, v₁, u₁, u₁} (diag C) Y))).1 ⟶
      (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 X Y)
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
X Y : C
⊢ Eq (α :=
    ((F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).2 ⟶
      (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj X) ((F.prod' G).obj Y)).2)
    (δ (F.prod' G) X Y).2 (δ G X Y)
have change : Eq (α :=
  G.obj (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).2 ⟶
    (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.map (𝟙 (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorObj.{v₁, u₁} (𝒞 := inst) X 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: 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
X Y : C
⊢ Eq (α :=
    G.obj (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).2 ⟶
      (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.map (𝟙 (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorObj.{v₁, u₁} (𝒞 := inst) X 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)
have rw : Eq (α :=
  G.obj (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).2 ⟶
    (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((diag C ⋙ F.prod G).obj X)
        ((diag C ⋙ F.prod G).obj Y)).2)
  ((δ (F.prod G) (obj.{v₁, v₁, u₁, u₁} (diag C) X) (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).2 :
    ((F.prod 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 ⟶
      (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 X Y)
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
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₃} C E
inst_7 : F.Monoidal
inst_8 : G.Monoidal
⊢ Eq (α :=
    Quiver.Hom (V := D × E) ((𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E))
      ((𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E)))
    (CategoryStruct.comp (Y := (F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε (F.prod' G)) (η (F.prod' G)))
    (𝟙 ((𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E)))
have h₁ : Eq (α :=
  Quiver.Hom.{v₂, u₂} (V := D) (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1)
  (CategoryStruct.comp (Y := (F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε (F.prod' G)) (η (F.prod' G))).1
  (𝟙 ((𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D 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₃} C E
inst_7 : F.Monoidal
inst_8 : G.Monoidal
h₁ :
  Eq (α :=
    Quiver.Hom.{v₂, u₂} (V := D) (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1
      (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1)
    (CategoryStruct.comp (Y := (F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε (F.prod' G)) (η (F.prod' G))).1
    (𝟙 ((𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E))).1
⊢ Eq (α :=
    Quiver.Hom (V := D × E) ((𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E))
      ((𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E)))
    (CategoryStruct.comp (Y := (F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε (F.prod' G)) (η (F.prod' G)))
    (𝟙 ((𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E)))
have h₂ : Eq (α :=
  Quiver.Hom.{v₃, u₃} (V := E) (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2)
  (CategoryStruct.comp (Y := (F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε (F.prod' G)) (η (F.prod' G))).2
  (𝟙 ((𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D 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₃} C E
inst_7 : F.Monoidal
inst_8 : G.Monoidal
⊢ CategoryStruct.comp (Y := (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E)) (η (F.prod' G))
      (ε (F.prod' G)) =
    𝟙 ((F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
have h₁ : Eq (α :=
  ((F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1 ⟶ ((F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
  (CategoryStruct.comp (Y := (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E)) (η (F.prod' G))
      (ε (F.prod' G))).1
  (𝟙 ((F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))).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₃} C E
inst_7 : F.Monoidal
inst_8 : G.Monoidal
h₁ :
  Eq (α :=
    ((F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1 ⟶ ((F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
    (CategoryStruct.comp (Y := (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E)) (η (F.prod' G))
        (ε (F.prod' G))).1
    (𝟙 ((F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))).1
⊢ CategoryStruct.comp (Y := (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E)) (η (F.prod' G))
      (ε (F.prod' G)) =
    𝟙 ((F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
have h₂ : Eq (α :=
  ((F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2 ⟶ ((F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2)
  (CategoryStruct.comp (Y := (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E)) (η (F.prod' G))
      (ε (F.prod' G))).2
  (𝟙 ((F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))).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₃} C E
inst_7 : F.Monoidal
inst_8 : G.Monoidal
x x_1 : C
⊢ CategoryStruct.comp (Y := (F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (μ (F.prod' G) x x_1)
      (δ (F.prod' G) x x_1) =
    𝟙 (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj x) ((F.prod' G).obj x_1))
have h₁ : Eq (α :=
  (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj x) ((F.prod' G).obj x_1)).1 ⟶
    (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj x) ((F.prod' G).obj x_1)).1)
  (CategoryStruct.comp (Y := (F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (μ (F.prod' G) x x_1)
      (δ (F.prod' G) x x_1)).1
  (𝟙 (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((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₃} C E
inst_7 : F.Monoidal
inst_8 : G.Monoidal
x x_1 : C
h₁ :
  Eq (α :=
    (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj x) ((F.prod' G).obj x_1)).1 ⟶
      (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj x) ((F.prod' G).obj x_1)).1)
    (CategoryStruct.comp (Y := (F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (μ (F.prod' G) x x_1)
        (δ (F.prod' G) x x_1)).1
    (𝟙 (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj x) ((F.prod' G).obj x_1))).1
⊢ CategoryStruct.comp (Y := (F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (μ (F.prod' G) x x_1)
      (δ (F.prod' G) x x_1) =
    𝟙 (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj x) ((F.prod' G).obj x_1))
have h₂ : Eq (α :=
  (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj x) ((F.prod' G).obj x_1)).2 ⟶
    (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj x) ((F.prod' G).obj x_1)).2)
  (CategoryStruct.comp (Y := (F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (μ (F.prod' G) x x_1)
      (δ (F.prod' G) x x_1)).2
  (𝟙 (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((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₃} C E
inst_7 : F.Monoidal
inst_8 : G.Monoidal
x x_1 : C
⊢ CategoryStruct.comp (Y :=
      tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((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.{v₁, u₁} (𝒞 := inst) x x_1))
have h₁ : Eq (α :=
  ((F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)).1 ⟶
    ((F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)).1)
  (CategoryStruct.comp (Y :=
      tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((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.{v₁, u₁} (𝒞 := inst) 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₃} C E
inst_7 : F.Monoidal
inst_8 : G.Monoidal
x x_1 : C
h₁ :
  Eq (α :=
    ((F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)).1 ⟶
      ((F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)).1)
    (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((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.{v₁, u₁} (𝒞 := inst) x x_1))).1
⊢ CategoryStruct.comp (Y :=
      tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((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.{v₁, u₁} (𝒞 := inst) x x_1))
have h₂ : Eq (α :=
  ((F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)).2 ⟶
    ((F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)).2)
  (CategoryStruct.comp (Y :=
      tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((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.{v₁, u₁} (𝒞 := inst) 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
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_7 : F.OplaxMonoidal
X Y : D
f : X ⟶ Y
X' : D
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X') ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y X'))
    (G.map f ▷ G.obj X' ≫
      ((adj.homEquiv (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj X')) (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y X') :
            Equiv.{v₂ + 1, v₁ + 1}
              (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj X')) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) Y X')
              (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj X') ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y X'))) :
          (a : F.obj (G.obj Y ⊗ G.obj X') ⟶ Y ⊗ X') → G.obj Y ⊗ G.obj X' ⟶ G.obj (Y ⊗ X'))
        (δ F (G.obj Y) (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X')))
    (((adj.homEquiv (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) (tensorObj.{v₂, u₂} (𝒞 := inst_2) X X') :
            Equiv.{v₂ + 1, v₁ + 1}
              (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) X X')
              (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X') ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X X'))) :
          (a : F.obj (G.obj X ⊗ G.obj X') ⟶ X ⊗ X') → G.obj X ⊗ G.obj X' ⟶ G.obj (X ⊗ X'))
        (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X')) ≫
      G.map (f ▷ X'))
have simp : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X') ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y X'))
  (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ≫
    G.map (δ F (G.obj X) (G.obj X') ≫ F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X')))
  (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ≫
    G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X'))
Tactic: simp only [Adjunction.homEquiv_apply, ← adj.unit_naturality_assoc, ← G.map_comp, assoc,
      ← δ_natural_left_assoc F]
-- 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 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_7 : F.OplaxMonoidal
X Y : D
f : X ⟶ Y
X' : D
this :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (G.obj X)) (F.obj (G.obj X')) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) Y X')
    (F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X'))
    ((adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X')
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X') ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y X'))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X')))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X'))
have rw : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X') ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y X'))
  (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ≫
    G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X'))
  (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ≫
    G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X'))
Tactic: rw [this]
-- 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 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_7 : F.OplaxMonoidal
X Y : D
f : X ⟶ Y
X' : D
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X') ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y X'))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X')))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X'))
have suffices : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (G.obj X)) (F.obj (G.obj X')) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) Y X')
  (F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X'))
  ((adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X')
Tactic: suffices F.map (G.map f) ▷ F.obj (G.obj X') ≫ _ =
      (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ _ by rw [this]
-- 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 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_7 : F.OplaxMonoidal
X' Y' X : D
g : X' ⟶ Y'
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X') ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y'))
    (G.obj X ◁ G.map g ≫
      ((adj.homEquiv (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y')) (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y') :
            Equiv.{v₂ + 1, v₁ + 1}
              (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y')) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y')
              (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y') ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y'))) :
          (a : F.obj (G.obj X ⊗ G.obj Y') ⟶ X ⊗ Y') → G.obj X ⊗ G.obj Y' ⟶ G.obj (X ⊗ Y'))
        (δ F (G.obj X) (G.obj Y') ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y')))
    (((adj.homEquiv (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) (tensorObj.{v₂, u₂} (𝒞 := inst_2) X X') :
            Equiv.{v₂ + 1, v₁ + 1}
              (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) X X')
              (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X') ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X X'))) :
          (a : F.obj (G.obj X ⊗ G.obj X') ⟶ X ⊗ X') → G.obj X ⊗ G.obj X' ⟶ G.obj (X ⊗ X'))
        (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X')) ≫
      G.map (X ◁ g))
have simp : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X') ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y'))
  (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ≫
    G.map (δ F (G.obj X) (G.obj X') ≫ F.obj (G.obj X) ◁ F.map (G.map g) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y')))
  (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ≫
    G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ X ◁ g))
Tactic: simp only [Adjunction.homEquiv_apply, ← adj.unit_naturality_assoc, ← G.map_comp,
      assoc, ← δ_natural_right_assoc F]