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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X Y : C
T : D
rw :
  CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (μ F X Y) (δ F X Y) ▷ T =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) T)
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) T)
      (μ F X Y ▷ T) (δ F X Y ▷ T) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) T)
have rw₁ : 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) ▷ T =
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) T)
Tactic: rw [← MonoidalCategory.comp_whiskerRight, μ_δ, id_whiskerRight]
-- 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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X Y : C
T : D
rw :
  CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (μ F X Y) (δ F X Y) ▷ T =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) T)
rw₁ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) ▷ T =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) T)
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) T)
      (μ F X Y ▷ T) (δ F X Y ▷ T) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) T)
have rw₂ : Eq.{v₂ + 1} (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) T ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) T)
  (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) T))
  (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) T))
Tactic: rw [← MonoidalCategory.comp_whiskerRight, μ_δ, id_whiskerRight]
-- 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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X Y : C
T : D
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) T)
      (δ F X Y ▷ T) (μ F X Y ▷ T) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) T)
have rw : CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (δ F X Y) (μ F X Y) ▷ T =
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) T)
Tactic: rw [← MonoidalCategory.comp_whiskerRight, δ_μ, id_whiskerRight]
-- 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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X Y : C
T : D
rw :
  CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (δ F X Y) (μ F X Y) ▷ T =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) T)
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) T)
      (δ F X Y ▷ T) (μ F X Y ▷ T) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) T)
have rw₁ : 𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ▷ T =
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) T)
Tactic: rw [← MonoidalCategory.comp_whiskerRight, δ_μ, id_whiskerRight]
-- 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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X Y : C
T : D
rw :
  CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (δ F X Y) (μ F X Y) ▷ T =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) T)
rw₁ :
  𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ▷ T =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) T)
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) T)
      (δ F X Y ▷ T) (μ F X Y ▷ T) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) T)
have rw₂ : Eq.{v₂ + 1} (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) T ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) T)
  (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) T))
  (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) T))
Tactic: rw [← MonoidalCategory.comp_whiskerRight, δ_μ, id_whiskerRight]
-- 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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
T : D
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (T ◁ ε F)
      (T ◁ η F) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
have rw : T ◁ CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (η F) =
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
Tactic: rw [← MonoidalCategory.whiskerLeft_comp, ε_η, MonoidalCategory.whiskerLeft_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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
T : D
rw :
  T ◁ CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (η F) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (T ◁ ε F)
      (T ◁ η F) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
have rw₁ : T ◁ 𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) =
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
Tactic: rw [← MonoidalCategory.whiskerLeft_comp, ε_η, MonoidalCategory.whiskerLeft_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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
T : D
rw :
  T ◁ CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (η F) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
rw₁ :
  T ◁ 𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (T ◁ ε F)
      (T ◁ η F) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
have rw₂ : Eq.{v₂ + 1} (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
  (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))))
  (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))))
Tactic: rw [← MonoidalCategory.whiskerLeft_comp, ε_η, MonoidalCategory.whiskerLeft_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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
T : D
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) (T ◁ η F)
      (T ◁ ε F) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
have rw : T ◁ CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η F) (ε F) =
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
Tactic: rw [← MonoidalCategory.whiskerLeft_comp, η_ε, MonoidalCategory.whiskerLeft_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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
T : D
rw :
  T ◁ CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η F) (ε F) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) (T ◁ η F)
      (T ◁ ε F) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
have rw₁ : T ◁ 𝟙 (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) =
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
Tactic: rw [← MonoidalCategory.whiskerLeft_comp, η_ε, MonoidalCategory.whiskerLeft_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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
T : D
rw :
  T ◁ CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η F) (ε F) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
rw₁ :
  T ◁ 𝟙 (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) (T ◁ η F)
      (T ◁ ε F) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
have rw₂ : Eq.{v₂ + 1} (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
  (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))))
  (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))))
Tactic: rw [← MonoidalCategory.whiskerLeft_comp, η_ε, MonoidalCategory.whiskerLeft_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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X Y : C
T : D
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
      (T ◁ μ F X Y) (T ◁ δ F X Y) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))
have rw : T ◁ CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (μ F X Y) (δ F X Y) =
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))
Tactic: rw [← MonoidalCategory.whiskerLeft_comp, μ_δ, MonoidalCategory.whiskerLeft_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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X Y : C
T : D
rw :
  T ◁ CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (μ F X Y) (δ F X Y) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
      (T ◁ μ F X Y) (T ◁ δ F X Y) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))
have rw₁ : T ◁ 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) =
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))
Tactic: rw [← MonoidalCategory.whiskerLeft_comp, μ_δ, MonoidalCategory.whiskerLeft_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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X Y : C
T : D
rw :
  T ◁ CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (μ F X Y) (δ F X Y) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))
rw₁ :
  T ◁ 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
      (T ◁ μ F X Y) (T ◁ δ F X Y) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))
have rw₂ : Eq.{v₂ + 1} (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))
  (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))))
  (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))))
Tactic: rw [← MonoidalCategory.whiskerLeft_comp, μ_δ, MonoidalCategory.whiskerLeft_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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X Y : C
T : D
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))
      (T ◁ δ F X Y) (T ◁ μ F X Y) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
have rw : T ◁ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (δ F X Y) (μ F X Y) =
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
Tactic: rw [← MonoidalCategory.whiskerLeft_comp, δ_μ, MonoidalCategory.whiskerLeft_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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X Y : C
T : D
rw :
  T ◁ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (δ F X Y) (μ F X Y) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))
      (T ◁ δ F X Y) (T ◁ μ F X Y) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
have rw₁ : T ◁ 𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) =
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
Tactic: rw [← MonoidalCategory.whiskerLeft_comp, δ_μ, MonoidalCategory.whiskerLeft_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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X Y : C
T : D
rw :
  T ◁ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (δ F X Y) (μ F X Y) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
rw₁ :
  T ◁ 𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))
      (T ◁ δ F X Y) (T ◁ μ F X Y) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
have rw₂ : Eq.{v₂ + 1} (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
  (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))))
  (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))))
Tactic: rw [← MonoidalCategory.whiskerLeft_comp, δ_μ, MonoidalCategory.whiskerLeft_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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X Y Z : C
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    (F.map (Iso.hom (α_ X Y Z)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
      (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
      (δ F X Y ▷ F.obj Z ≫
        Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ F.obj X ◁ μ F Y Z ≫ μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
have rw : Eq (α :=
  F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
  (F.map (Iso.hom (α_ X Y Z)))
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
    (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
    (CategoryStruct.comp (Y :=
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z))
      (δ F X Y ▷ F.obj Z)
      (μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ F.map (Iso.hom (α_ X Y Z)))))
Tactic: rw [← LaxMonoidal.associativity F, whiskerRight_δ_μ_assoc, δ_μ_assoc]
-- 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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X Y Z : C
rw :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    (F.map (Iso.hom (α_ X Y Z)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
      (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
      (CategoryStruct.comp (Y :=
        tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z))
        (δ F X Y ▷ F.obj Z)
        (μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ F.map (Iso.hom (α_ X Y Z)))))
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    (F.map (Iso.hom (α_ X Y Z)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
      (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
      (δ F X Y ▷ F.obj Z ≫
        Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ F.obj X ◁ μ F Y Z ≫ μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
have rw₁ : Eq (α :=
  F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
  (F.map (Iso.hom (α_ X Y Z)))
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
    (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
    (μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ F.map (Iso.hom (α_ X Y Z))))
Tactic: rw [← LaxMonoidal.associativity F, whiskerRight_δ_μ_assoc, δ_μ_assoc]
-- 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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X Y Z : C
rw :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    (F.map (Iso.hom (α_ X Y Z)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
      (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
      (CategoryStruct.comp (Y :=
        tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z))
        (δ F X Y ▷ F.obj Z)
        (μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ F.map (Iso.hom (α_ X Y Z)))))
rw₁ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    (F.map (Iso.hom (α_ X Y Z)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
      (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
      (μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ F.map (Iso.hom (α_ X Y Z))))
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    (F.map (Iso.hom (α_ X Y Z)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
      (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
      (δ F X Y ▷ F.obj Z ≫
        Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ F.obj X ◁ μ F Y Z ≫ μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
have rw₂ : Eq (α :=
  F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
  (F.map (Iso.hom (α_ X Y Z))) (F.map (Iso.hom (α_ X Y Z)))
Tactic: rw [← LaxMonoidal.associativity F, whiskerRight_δ_μ_assoc, δ_μ_assoc]