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 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_7 : F.OplaxMonoidal
inst_8 : G.OplaxMonoidal
X Y : C
f : X ⟶ Y
X' : C
rw :
  Eq (α :=
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X')) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj Y)) (G.obj (F.obj X')))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj X'))) (G.map (δ F X X'))
      (δ G (F.obj X) (F.obj X') ≫ G.map (F.map f) ▷ G.obj (F.obj X')))
    (G.map (F.map (f ▷ X')) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X'))) (G.map (δ F Y X'))
        (δ G (F.obj Y) (F.obj X')))
rw₁ :
  Eq (α :=
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X')) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj Y)) (G.obj (F.obj X')))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj X'))) (G.map (δ F X X'))
      (G.map (F.map f ▷ F.obj X') ≫ δ G (F.obj Y) (F.obj X')))
    (G.map (F.map (f ▷ X')) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X'))) (G.map (δ F Y X'))
        (δ G (F.obj Y) (F.obj X')))
rw₂ :
  Eq (α :=
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X')) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj Y)) (G.obj (F.obj X')))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X')))
      (G.map (δ F X X' ≫ F.map f ▷ F.obj X')) (δ G (F.obj Y) (F.obj X')))
    (G.map (F.map (f ▷ X')) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X'))) (G.map (δ F Y X'))
        (δ G (F.obj Y) (F.obj X')))
⊢ Eq (α :=
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X')) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj Y)) (G.obj (F.obj X')))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj X'))) (G.map (δ F X X'))
        (δ G (F.obj X) (F.obj X')) ≫
      G.map (F.map f) ▷ G.obj (F.obj X'))
    (G.map (F.map (f ▷ X')) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X'))) (G.map (δ F Y X'))
        (δ G (F.obj Y) (F.obj X')))
have rw₃ : Eq (α :=
  G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X')) ⟶
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj Y)) (G.obj (F.obj X')))
  (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X')))
    (G.map (F.map (f ▷ X') ≫ δ F Y X')) (δ G (F.obj Y) (F.obj X')))
  (G.map (F.map (f ▷ X')) ≫
    CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X'))) (G.map (δ F Y X'))
      (δ G (F.obj Y) (F.obj X')))
Tactic: rw [assoc, δ_natural_left, ← G.map_comp_assoc, δ_natural_left, map_comp, 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
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 E
inst_7 : F.OplaxMonoidal
inst_8 : G.OplaxMonoidal
X Y x : C
x_1 : X ⟶ Y
⊢ Eq (α :=
    (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x X) ⟶ tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj x) ((F ⋙ G).obj Y))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (G.map (δ F x X))
        (δ G (F.obj x) (F.obj X)) ≫
      (F ⋙ G).obj x ◁ (F ⋙ G).map x_1)
    ((F ⋙ G).map (x ◁ x_1) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (G.map (δ F x Y))
        (δ G (F.obj x) (F.obj Y)))
have dsimp : Eq (α :=
  G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x X)) ⟶
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj Y)))
  (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (G.map (δ F x X))
      (δ G (F.obj x) (F.obj X)) ≫
    G.obj (F.obj x) ◁ G.map (F.map x_1))
  (G.map (F.map (x ◁ x_1)) ≫
    CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (G.map (δ F x Y))
      (δ G (F.obj x) (F.obj Y)))
Tactic: dsimp
-- 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 E
inst_7 : F.OplaxMonoidal
inst_8 : G.OplaxMonoidal
X Y x : C
x_1 : X ⟶ Y
⊢ Eq (α :=
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x X)) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj Y)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (G.map (δ F x X))
        (δ G (F.obj x) (F.obj X)) ≫
      G.obj (F.obj x) ◁ G.map (F.map x_1))
    (G.map (F.map (x ◁ x_1)) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (G.map (δ F x Y))
        (δ G (F.obj x) (F.obj Y)))
have rw : Eq (α :=
  G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x X)) ⟶
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj Y)))
  (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (G.map (δ F x X))
    (δ G (F.obj x) (F.obj X) ≫ G.obj (F.obj x) ◁ G.map (F.map x_1)))
  (G.map (F.map (x ◁ x_1)) ≫
    CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (G.map (δ F x Y))
      (δ G (F.obj x) (F.obj Y)))
Tactic: rw [assoc, δ_natural_right, ← G.map_comp_assoc, δ_natural_right, map_comp, 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
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 E
inst_7 : F.OplaxMonoidal
inst_8 : G.OplaxMonoidal
X Y x : C
x_1 : X ⟶ Y
rw :
  Eq (α :=
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x X)) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj Y)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (G.map (δ F x X))
      (δ G (F.obj x) (F.obj X) ≫ G.obj (F.obj x) ◁ G.map (F.map x_1)))
    (G.map (F.map (x ◁ x_1)) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (G.map (δ F x Y))
        (δ G (F.obj x) (F.obj Y)))
⊢ Eq (α :=
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x X)) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj Y)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (G.map (δ F x X))
        (δ G (F.obj x) (F.obj X)) ≫
      G.obj (F.obj x) ◁ G.map (F.map x_1))
    (G.map (F.map (x ◁ x_1)) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (G.map (δ F x Y))
        (δ G (F.obj x) (F.obj Y)))
have rw₁ : Eq (α :=
  G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x X)) ⟶
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj Y)))
  (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (G.map (δ F x X))
    (G.map (F.obj x ◁ F.map x_1) ≫ δ G (F.obj x) (F.obj Y)))
  (G.map (F.map (x ◁ x_1)) ≫
    CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (G.map (δ F x Y))
      (δ G (F.obj x) (F.obj Y)))
Tactic: rw [assoc, δ_natural_right, ← G.map_comp_assoc, δ_natural_right, map_comp, 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
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 E
inst_7 : F.OplaxMonoidal
inst_8 : G.OplaxMonoidal
X Y x : C
x_1 : X ⟶ Y
rw :
  Eq (α :=
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x X)) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj Y)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (G.map (δ F x X))
      (δ G (F.obj x) (F.obj X) ≫ G.obj (F.obj x) ◁ G.map (F.map x_1)))
    (G.map (F.map (x ◁ x_1)) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (G.map (δ F x Y))
        (δ G (F.obj x) (F.obj Y)))
rw₁ :
  Eq (α :=
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x X)) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj Y)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (G.map (δ F x X))
      (G.map (F.obj x ◁ F.map x_1) ≫ δ G (F.obj x) (F.obj Y)))
    (G.map (F.map (x ◁ x_1)) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (G.map (δ F x Y))
        (δ G (F.obj x) (F.obj Y)))
⊢ Eq (α :=
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x X)) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj Y)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (G.map (δ F x X))
        (δ G (F.obj x) (F.obj X)) ≫
      G.obj (F.obj x) ◁ G.map (F.map x_1))
    (G.map (F.map (x ◁ x_1)) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (G.map (δ F x Y))
        (δ G (F.obj x) (F.obj Y)))
have rw₂ : Eq (α :=
  G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x X)) ⟶
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj Y)))
  (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y)))
    (G.map (δ F x X ≫ F.obj x ◁ F.map x_1)) (δ G (F.obj x) (F.obj Y)))
  (G.map (F.map (x ◁ x_1)) ≫
    CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (G.map (δ F x Y))
      (δ G (F.obj x) (F.obj Y)))
Tactic: rw [assoc, δ_natural_right, ← G.map_comp_assoc, δ_natural_right, map_comp, 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
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 E
inst_7 : F.OplaxMonoidal
inst_8 : G.OplaxMonoidal
X Y x : C
x_1 : X ⟶ Y
rw :
  Eq (α :=
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x X)) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj Y)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (G.map (δ F x X))
      (δ G (F.obj x) (F.obj X) ≫ G.obj (F.obj x) ◁ G.map (F.map x_1)))
    (G.map (F.map (x ◁ x_1)) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (G.map (δ F x Y))
        (δ G (F.obj x) (F.obj Y)))
rw₁ :
  Eq (α :=
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x X)) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj Y)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (G.map (δ F x X))
      (G.map (F.obj x ◁ F.map x_1) ≫ δ G (F.obj x) (F.obj Y)))
    (G.map (F.map (x ◁ x_1)) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (G.map (δ F x Y))
        (δ G (F.obj x) (F.obj Y)))
rw₂ :
  Eq (α :=
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x X)) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj Y)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y)))
      (G.map (δ F x X ≫ F.obj x ◁ F.map x_1)) (δ G (F.obj x) (F.obj Y)))
    (G.map (F.map (x ◁ x_1)) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (G.map (δ F x Y))
        (δ G (F.obj x) (F.obj Y)))
⊢ Eq (α :=
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x X)) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj Y)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X))) (G.map (δ F x X))
        (δ G (F.obj x) (F.obj X)) ≫
      G.obj (F.obj x) ◁ G.map (F.map x_1))
    (G.map (F.map (x ◁ x_1)) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (G.map (δ F x Y))
        (δ G (F.obj x) (F.obj Y)))
have rw₃ : Eq (α :=
  G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x X)) ⟶
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj Y)))
  (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y)))
    (G.map (F.map (x ◁ x_1) ≫ δ F x Y)) (δ G (F.obj x) (F.obj Y)))
  (G.map (F.map (x ◁ x_1)) ≫
    CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) (G.map (δ F x Y))
      (δ G (F.obj x) (F.obj Y)))
Tactic: rw [assoc, δ_natural_right, ← G.map_comp_assoc, δ_natural_right, map_comp, 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
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 E
inst_7 : F.OplaxMonoidal
inst_8 : G.OplaxMonoidal
X Y Z : C
⊢ Eq (α :=
    (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X)
        (tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj Y) ((F ⋙ G).obj Z)))
    (CategoryStruct.comp (Y :=
        G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z)))
        (G.map (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
        (δ G (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z)) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))) (G.map (δ F X Y))
            (δ G (F.obj X) (F.obj Y)) ▷
          (F ⋙ G).obj Z ≫
        Iso.hom (α_ ((F ⋙ G).obj X) ((F ⋙ G).obj Y) ((F ⋙ G).obj Z)))
    ((F ⋙ G).map (Iso.hom (α_ X Y Z)) ≫
      CategoryStruct.comp (Y :=
          G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))))
          (G.map (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
          (δ G (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))) ≫
        (F ⋙ G).obj X ◁
          CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z))) (G.map (δ F Y Z))
            (δ G (F.obj Y) (F.obj Z)))
have dsimp : Eq (α :=
  G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)) ⟶
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj X))
      (tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj Y)) (G.obj (F.obj Z))))
  (CategoryStruct.comp (Y :=
      G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z)))
      (G.map (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
      (δ G (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z)) ≫
    CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))) (G.map (δ F X Y))
          (δ G (F.obj X) (F.obj Y)) ▷
        G.obj (F.obj Z) ≫
      Iso.hom (α_ (G.obj (F.obj X)) (G.obj (F.obj Y)) (G.obj (F.obj Z))))
  (G.map (F.map (Iso.hom (α_ X Y Z))) ≫
    CategoryStruct.comp (Y :=
        G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))))
        (G.map (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
        (δ G (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))) ≫
      G.obj (F.obj X) ◁
        CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z))) (G.map (δ F Y Z))
          (δ G (F.obj Y) (F.obj Z)))
Tactic: dsimp
-- 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) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) T) (ε F ▷ T)
      (η F ▷ T) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) T)
have rw : CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (η F) ▷ T =
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) 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
rw :
  CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (η F) ▷ T =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) T)
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) T) (ε F ▷ T)
      (η F ▷ T) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) T)
have rw₁ : 𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ▷ T =
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) 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
rw :
  CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (η F) ▷ T =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) T)
rw₁ :
  𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ▷ T =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) T)
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) T) (ε F ▷ T)
      (η F ▷ T) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) T)
have rw₂ : Eq.{v₂ + 1} (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) T ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) T)
  (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) T))
  (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) 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) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) T) (η F ▷ T)
      (ε F ▷ T) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) T)
have rw : CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η F) (ε F) ▷ T =
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) 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
rw :
  CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η F) (ε F) ▷ T =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) T)
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) T) (η F ▷ T)
      (ε F ▷ T) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) T)
have rw₁ : 𝟙 (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ T =
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) 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
rw :
  CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η F) (ε F) ▷ T =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) T)
rw₁ :
  𝟙 (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ T =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) T)
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) T) (η F ▷ T)
      (ε F ▷ T) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) T)
have rw₂ : Eq.{v₂ + 1} (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) T ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) T)
  (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) T))
  (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) 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) (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 : 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)
Tactic: rw [← MonoidalCategory.comp_whiskerRight, μ_δ, id_whiskerRight]