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 : C
rw :
  Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X))
      (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ η F ▷ F.obj X) (Iso.hom (λ_ (F.obj X))))
    (F.map (Iso.hom (λ_ X)))
rw₁ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X))
    (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ η F ▷ F.obj X) (F.map (Iso.hom (λ_ X)) ≫ Iso.inv (λ_ (F.obj X)))
rw₂ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X))
    (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ η F ▷ F.obj X)
    (F.map (Iso.hom (λ_ X)) ≫
      CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
        (F.map (Iso.inv (λ_ X))) (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ η F ▷ F.obj X))
rw₃ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X))
    (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ η F ▷ F.obj X)
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
      (F.map (Iso.hom (λ_ X)) ≫ F.map (Iso.inv (λ_ X))) (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ η F ▷ F.obj X))
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X))
      (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) (η F ▷ F.obj X ≫ Iso.hom (λ_ (F.obj X))))
    (F.map (Iso.hom (λ_ X)))
have rw₄ : Eq (α :=
  F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X))
  (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ η F ▷ F.obj X)
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (F.map (Iso.hom (λ_ X) ≫ Iso.inv (λ_ X))) (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ η F ▷ F.obj X))
Tactic: rw [← Category.assoc, ← Iso.eq_comp_inv, left_unitality, ← Category.assoc,
    ← F.map_comp, Iso.hom_inv_id, F.map_id, 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 : C
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
      (δ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X ◁ η F ≫ Iso.hom (ρ_ (F.obj X))))
    (F.map (Iso.hom (ρ_ X)))
have rw : Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⟶ F.obj X)
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (δ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.obj X ◁ η F) (Iso.hom (ρ_ (F.obj X))))
  (F.map (Iso.hom (ρ_ X)))
Tactic: rw [← Category.assoc, ← Iso.eq_comp_inv, right_unitality, ← Category.assoc,
    ← F.map_comp, Iso.hom_inv_id, F.map_id, 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 : C
rw :
  Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
      (δ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.obj X ◁ η F) (Iso.hom (ρ_ (F.obj X))))
    (F.map (Iso.hom (ρ_ X)))
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
      (δ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X ◁ η F ≫ Iso.hom (ρ_ (F.obj X))))
    (F.map (Iso.hom (ρ_ X)))
have rw₁ : Eq (α :=
  F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
  (δ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.obj X ◁ η F) (F.map (Iso.hom (ρ_ X)) ≫ Iso.inv (ρ_ (F.obj X)))
Tactic: rw [← Category.assoc, ← Iso.eq_comp_inv, right_unitality, ← Category.assoc,
    ← F.map_comp, Iso.hom_inv_id, F.map_id, 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 : C
rw :
  Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
      (δ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.obj X ◁ η F) (Iso.hom (ρ_ (F.obj X))))
    (F.map (Iso.hom (ρ_ X)))
rw₁ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (δ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.obj X ◁ η F) (F.map (Iso.hom (ρ_ X)) ≫ Iso.inv (ρ_ (F.obj X)))
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
      (δ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X ◁ η F ≫ Iso.hom (ρ_ (F.obj X))))
    (F.map (Iso.hom (ρ_ X)))
have rw₂ : Eq (α :=
  F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
  (δ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.obj X ◁ η F)
  (F.map (Iso.hom (ρ_ X)) ≫
    CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
      (F.map (Iso.inv (ρ_ X))) (δ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.obj X ◁ η F))
Tactic: rw [← Category.assoc, ← Iso.eq_comp_inv, right_unitality, ← Category.assoc,
    ← F.map_comp, Iso.hom_inv_id, F.map_id, 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 : C
rw :
  Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
      (δ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.obj X ◁ η F) (Iso.hom (ρ_ (F.obj X))))
    (F.map (Iso.hom (ρ_ X)))
rw₁ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (δ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.obj X ◁ η F) (F.map (Iso.hom (ρ_ X)) ≫ Iso.inv (ρ_ (F.obj X)))
rw₂ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (δ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.obj X ◁ η F)
    (F.map (Iso.hom (ρ_ X)) ≫
      CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
        (F.map (Iso.inv (ρ_ X))) (δ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.obj X ◁ η F))
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
      (δ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X ◁ η F ≫ Iso.hom (ρ_ (F.obj X))))
    (F.map (Iso.hom (ρ_ X)))
have rw₃ : Eq (α :=
  F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
  (δ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.obj X ◁ η F)
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
    (F.map (Iso.hom (ρ_ X)) ≫ F.map (Iso.inv (ρ_ X))) (δ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.obj X ◁ η F))
Tactic: rw [← Category.assoc, ← Iso.eq_comp_inv, right_unitality, ← Category.assoc,
    ← F.map_comp, Iso.hom_inv_id, F.map_id, 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 : C
rw :
  Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
      (δ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.obj X ◁ η F) (Iso.hom (ρ_ (F.obj X))))
    (F.map (Iso.hom (ρ_ X)))
rw₁ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (δ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.obj X ◁ η F) (F.map (Iso.hom (ρ_ X)) ≫ Iso.inv (ρ_ (F.obj X)))
rw₂ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (δ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.obj X ◁ η F)
    (F.map (Iso.hom (ρ_ X)) ≫
      CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
        (F.map (Iso.inv (ρ_ X))) (δ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.obj X ◁ η F))
rw₃ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (δ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.obj X ◁ η F)
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
      (F.map (Iso.hom (ρ_ X)) ≫ F.map (Iso.inv (ρ_ X))) (δ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.obj X ◁ η F))
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
      (δ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X ◁ η F ≫ Iso.hom (ρ_ (F.obj X))))
    (F.map (Iso.hom (ρ_ X)))
have rw₄ : Eq (α :=
  F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
  (δ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.obj X ◁ η F)
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
    (F.map (Iso.hom (ρ_ X) ≫ Iso.inv (ρ_ X))) (δ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.obj X ◁ η F))
Tactic: rw [← Category.assoc, ← Iso.eq_comp_inv, right_unitality, ← Category.assoc,
    ← F.map_comp, Iso.hom_inv_id, F.map_id, 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
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj 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)))
    (F.map (Iso.inv (α_ X Y Z)) ≫ δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X 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) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj 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)))
  (F.map (Iso.inv (α_ X Y Z)) ≫ δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X Y ▷ F.obj Z)
Tactic: rw [← Category.assoc, Iso.comp_inv_eq, Category.assoc, Category.assoc, associativity,
    ← Category.assoc, ← F.map_comp, Iso.inv_hom_id, F.map_id, 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) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj 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)))
    (F.map (Iso.inv (α_ X Y Z)) ≫ δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X Y ▷ F.obj Z)
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj 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)))
    (F.map (Iso.inv (α_ X Y Z)) ≫ δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X 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 (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X Y ▷ F.obj Z) ≫
    Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)))
Tactic: rw [← Category.assoc, Iso.comp_inv_eq, Category.assoc, Category.assoc, associativity,
    ← Category.assoc, ← F.map_comp, Iso.inv_hom_id, F.map_id, 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) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj 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)))
    (F.map (Iso.inv (α_ X Y Z)) ≫ δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X Y ▷ F.obj 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)) ≫ δ 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)))
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj 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)))
    (F.map (Iso.inv (α_ X Y Z)) ≫ δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X 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 (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X Y ▷ F.obj Z) ≫ Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)))
Tactic: rw [← Category.assoc, Iso.comp_inv_eq, Category.assoc, Category.assoc, associativity,
    ← Category.assoc, ← F.map_comp, Iso.inv_hom_id, F.map_id, 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) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj 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)))
    (F.map (Iso.inv (α_ X Y Z)) ≫ δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X Y ▷ F.obj 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)) ≫ δ 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)))
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 (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X Y ▷ F.obj Z) ≫ Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)))
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj 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)))
    (F.map (Iso.inv (α_ X Y Z)) ≫ δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X 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 (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X Y ▷ F.obj Z ≫ Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)))
Tactic: rw [← Category.assoc, Iso.comp_inv_eq, Category.assoc, Category.assoc, associativity,
    ← Category.assoc, ← F.map_comp, Iso.inv_hom_id, F.map_id, 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) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj 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)))
    (F.map (Iso.inv (α_ X Y Z)) ≫ δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X Y ▷ F.obj 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)) ≫ δ 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)))
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 (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X Y ▷ F.obj Z) ≫ Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj 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)) ≫
      δ 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)))
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj 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)))
    (F.map (Iso.inv (α_ X Y Z)) ≫ δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X 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 [← Category.assoc, Iso.comp_inv_eq, Category.assoc, Category.assoc, associativity,
    ← Category.assoc, ← F.map_comp, Iso.inv_hom_id, F.map_id, 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
⊢ 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 ≫ Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)))
Tactic: rw [← associativity_assoc, Iso.hom_inv_id, Category.comp_id]