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