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.OplaxMonoidal
X Y Z : C
rw :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z))
    (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F 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)) ≫ Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)))
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z))
    (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X Y ▷ F.obj Z)
    (F.map (Iso.hom (α_ X Y Z)) ≫
      δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z ≫ Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)))
have rw₁ : Eq (α :=
  F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z))
  (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X Y ▷ F.obj Z)
  (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫
    δ F X Y ▷ F.obj Z ≫
      𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z)))
Tactic: rw [← associativity_assoc, Iso.hom_inv_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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.OplaxMonoidal
X Y Z : C
rw :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z))
    (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F 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)) ≫ Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)))
rw₁ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z))
    (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X Y ▷ F.obj Z)
    (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫
      δ F X Y ▷ F.obj Z ≫
        𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z)))
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z))
    (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X Y ▷ F.obj Z)
    (F.map (Iso.hom (α_ X Y Z)) ≫
      δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z ≫ Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)))
have rw₂ : Eq (α :=
  F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z))
  (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X Y ▷ F.obj Z)
  (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X Y ▷ F.obj Z)
Tactic: rw [← associativity_assoc, Iso.hom_inv_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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.OplaxMonoidal
X Y Z : C
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
    (F.map (Iso.inv (α_ X Y 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)))
have rw : Eq (α :=
  F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
  (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
  (F.map (Iso.inv (α_ X Y Z)) ≫
    F.map (Iso.hom (α_ X Y Z)) ≫ δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
Tactic: rw [associativity, ← F.map_comp_assoc, Iso.inv_hom_id, 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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.OplaxMonoidal
X Y Z : C
rw :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
    (F.map (Iso.inv (α_ X Y Z)) ≫
      F.map (Iso.hom (α_ X Y Z)) ≫ δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
    (F.map (Iso.inv (α_ X Y 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)))
have rw₁ : Eq (α :=
  F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
  (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
  (F.map (Iso.inv (α_ X Y Z) ≫ Iso.hom (α_ X Y Z)) ≫ δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
Tactic: rw [associativity, ← F.map_comp_assoc, Iso.inv_hom_id, 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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.OplaxMonoidal
X Y Z : C
rw :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
    (F.map (Iso.inv (α_ X Y Z)) ≫
      F.map (Iso.hom (α_ X Y Z)) ≫ δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
rw₁ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
    (F.map (Iso.inv (α_ X Y Z) ≫ Iso.hom (α_ X Y Z)) ≫ δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
    (F.map (Iso.inv (α_ X Y 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)))
have rw₂ : Eq (α :=
  F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
  (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
  (F.map (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))) ≫
    δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
Tactic: rw [associativity, ← F.map_comp_assoc, Iso.inv_hom_id, 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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.OplaxMonoidal
X Y Z : C
rw :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
    (F.map (Iso.inv (α_ X Y Z)) ≫
      F.map (Iso.hom (α_ X Y Z)) ≫ δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
rw₁ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
    (F.map (Iso.inv (α_ X Y Z) ≫ Iso.hom (α_ X Y Z)) ≫ δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
rw₂ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
    (F.map (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))) ≫
      δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
    (F.map (Iso.inv (α_ X Y 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)))
have rw₃ : Eq (α :=
  F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
  (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
  (𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))) ≫
    δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
Tactic: rw [associativity, ← F.map_comp_assoc, Iso.inv_hom_id, 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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.OplaxMonoidal
X Y Z : C
rw :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
    (F.map (Iso.inv (α_ X Y Z)) ≫
      F.map (Iso.hom (α_ X Y Z)) ≫ δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
rw₁ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
    (F.map (Iso.inv (α_ X Y Z) ≫ Iso.hom (α_ X Y Z)) ≫ δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
rw₂ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
    (F.map (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))) ≫
      δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
rw₃ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
    (𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))) ≫
      δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
    (F.map (Iso.inv (α_ X Y 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)))
have rw₄ : Eq (α :=
  F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
  (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
  (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
Tactic: rw [associativity, ← F.map_comp_assoc, Iso.inv_hom_id, 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 : 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
⊢ Eq (α :=
    (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X') ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj Y) ((F ⋙ G).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')) ≫
      (F ⋙ G).map f ▷ (F ⋙ G).obj X')
    ((F ⋙ G).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 dsimp : 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')))
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 : C
f : X ⟶ Y
X' : C
⊢ 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 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')))
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 : 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')))
⊢ 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 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')))
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 : 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')))
⊢ 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 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')))
Tactic: rw [assoc, δ_natural_left, ← G.map_comp_assoc, δ_natural_left, map_comp, assoc]