awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X Y Z : C
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
    (F.map (Iso.inv (α_ X Y Z)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) 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)) ≫ μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
have rw : Eq (α :=
  F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
  (F.map (Iso.hom (α_ X Y Z)) ≫ F.map (Iso.inv (α_ X Y Z)))
  (F.map (Iso.hom (α_ X Y Z)) ≫
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) 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)) ≫ μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
Tactic: rw [← cancel_epi (F.map (α_ X Y Z).hom), Iso.map_hom_inv_id, map_associator,
    assoc, assoc, assoc, assoc, OplaxMonoidal.associativity_inv_assoc,
    whiskerRight_δ_μ_assoc, δ_μ, comp_id, LaxMonoidal.associativity_inv,
    Iso.hom_inv_id_assoc, whiskerRight_δ_μ_assoc, δ_μ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X Y Z : C
rw :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
    (F.map (Iso.hom (α_ X Y Z)) ≫ F.map (Iso.inv (α_ X Y Z)))
    (F.map (Iso.hom (α_ X Y Z)) ≫
      CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) 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)) ≫ μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
    (F.map (Iso.inv (α_ X Y Z)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) 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)) ≫ μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
have rw₁ : 𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)) =
  F.map (Iso.hom (α_ X Y Z)) ≫
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) 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)) ≫ μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
Tactic: rw [← cancel_epi (F.map (α_ X Y Z).hom), Iso.map_hom_inv_id, map_associator,
    assoc, assoc, assoc, assoc, OplaxMonoidal.associativity_inv_assoc,
    whiskerRight_δ_μ_assoc, δ_μ, comp_id, LaxMonoidal.associativity_inv,
    Iso.hom_inv_id_assoc, whiskerRight_δ_μ_assoc, δ_μ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X Y Z : C
rw :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
    (F.map (Iso.hom (α_ X Y Z)) ≫ F.map (Iso.inv (α_ X Y Z)))
    (F.map (Iso.hom (α_ X Y Z)) ≫
      CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) 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)) ≫ μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
rw₁ :
  𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)) =
    F.map (Iso.hom (α_ X Y Z)) ≫
      CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) 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)) ≫ μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
    (F.map (Iso.inv (α_ X Y Z)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) 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)) ≫ μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
have rw₂ : 𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)) =
  CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
      (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
      (δ F X Y ▷ F.obj Z ≫
        Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ F.obj X ◁ μ F Y Z ≫ μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) 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)) ≫ μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
Tactic: rw [← cancel_epi (F.map (α_ X Y Z).hom), Iso.map_hom_inv_id, map_associator,
    assoc, assoc, assoc, assoc, OplaxMonoidal.associativity_inv_assoc,
    whiskerRight_δ_μ_assoc, δ_μ, comp_id, LaxMonoidal.associativity_inv,
    Iso.hom_inv_id_assoc, whiskerRight_δ_μ_assoc, δ_μ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X Y Z : C
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z))
    (Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
      (F.obj X ◁ μ F Y Z)
      (μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y 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 (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z) ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z))
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
      (μ F X Y ▷ F.obj Z)
      (μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫
        F.map (Iso.hom (α_ X Y Z)) ≫ δ 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)))
  (CategoryStruct.comp (Y :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
      (μ F X Y ▷ F.obj Z)
      (μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫
        F.map (Iso.hom (α_ X Y Z)) ≫ δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
      (F.obj X ◁ μ F Y Z)
      (μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
        F.map (Iso.inv (α_ X Y Z)) ≫ δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X Y ▷ F.obj Z)))
Tactic: rw [← cancel_epi (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom, map_associator']
-- 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
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (CategoryTheory.inv (η F))
    (ε F)
have rw : Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (CategoryTheory.inv (η F))
  (Iso.hom (εIso F))
Tactic: rw [← εIso_hom, ← Iso.comp_inv_eq_id, εIso_inv, IsIso.inv_hom_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
rw :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (CategoryTheory.inv (η F))
    (Iso.hom (εIso F))
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (CategoryTheory.inv (η F))
    (ε F)
have rw₁ : CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (CategoryTheory.inv (η F)) (Iso.inv (εIso F)) =
  𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
Tactic: rw [← εIso_hom, ← Iso.comp_inv_eq_id, εIso_inv, IsIso.inv_hom_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
rw :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (CategoryTheory.inv (η F))
    (Iso.hom (εIso F))
rw₁ :
  CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (CategoryTheory.inv (η F)) (Iso.inv (εIso F)) =
    𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (CategoryTheory.inv (η F))
    (ε F)
have rw₂ : CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (CategoryTheory.inv (η F)) (η F) =
  𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
Tactic: rw [← εIso_hom, ← Iso.comp_inv_eq_id, εIso_inv, IsIso.inv_hom_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
rw :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (CategoryTheory.inv (η F))
    (Iso.hom (εIso F))
rw₁ :
  CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (CategoryTheory.inv (η F)) (Iso.inv (εIso F)) =
    𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
rw₂ :
  CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (CategoryTheory.inv (η F)) (η F) =
    𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (CategoryTheory.inv (η F))
    (ε F)
have rw₃ : Eq.{v₂ + 1} (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
  (𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) (𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
Tactic: rw [← εIso_hom, ← Iso.comp_inv_eq_id, εIso_inv, IsIso.inv_hom_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X Y : C
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
    (CategoryTheory.inv (μ F X Y)) (δ F X Y)
have rw : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
  (CategoryTheory.inv (CategoryTheory.inv (μ F X Y))) (CategoryTheory.inv (Iso.inv (μIso F X Y)))
Tactic: rw [← Monoidal.μIso_inv, ← CategoryTheory.IsIso.inv_eq_inv]
-- 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
a b : F.Monoidal
eq : Eq (α := F.LaxMonoidal) toLaxMonoidal toLaxMonoidal
⊢ a = b
have ε : Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (ε F)
Tactic: ext1
-- 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
a b : F.Monoidal
eq : Eq (α := F.LaxMonoidal) toLaxMonoidal toLaxMonoidal
ε :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (LaxMonoidal.ε F)
    (LaxMonoidal.ε F)
⊢ a = b
have μ : Eq (α := (X Y : C) → tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
  (μ F) (μ F)
Tactic: ext1
-- 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
a b : F.Monoidal
eq : Eq (α := F.LaxMonoidal) toLaxMonoidal toLaxMonoidal
ε :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (LaxMonoidal.ε F)
    (LaxMonoidal.ε F)
μ :
  Eq (α :=
    (X Y : C) → tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (LaxMonoidal.μ F) (LaxMonoidal.μ F)
⊢ a = b
have η : Eq (α := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η F) (η F)
Tactic: ext1
-- 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
a b : F.Monoidal
eq : Eq (α := F.LaxMonoidal) toLaxMonoidal toLaxMonoidal
ε :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (LaxMonoidal.ε F)
    (LaxMonoidal.ε F)
μ :
  Eq (α :=
    (X Y : C) → tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (LaxMonoidal.μ F) (LaxMonoidal.μ F)
η :
  Eq (α := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (OplaxMonoidal.η F)
    (OplaxMonoidal.η F)
⊢ a = b
have δ : Eq (α := (X Y : C) → F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
  (δ F) (δ F)
Tactic: ext1
-- 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
a b : F.Monoidal
eq : Eq (α := F.LaxMonoidal) toLaxMonoidal toLaxMonoidal
⊢ Eq (α := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η F) (η F)
have η : Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
  (CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Iso.hom (εIso F)) (η F))
  (CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Iso.hom (εIso F)) (η F))
Tactic: rw [← cancel_epi (εIso _).hom]
-- 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
a b : F.Monoidal
eq : Eq (α := F.LaxMonoidal) toLaxMonoidal toLaxMonoidal
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
    (CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Iso.hom (εIso F)) (η F))
    (CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Iso.hom (εIso F)) (η F))
have η : Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
  (CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Iso.hom (εIso F)) (η F))
  (CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (η F))
Tactic: rw [εIso_hom, ε_η, ← @ε_η _ _ _ _ _ _ _ a, ← εIso_hom]
-- 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
a b : F.Monoidal
eq : Eq (α := F.LaxMonoidal) toLaxMonoidal toLaxMonoidal
⊢ Eq (α :=
    (X Y : C) → F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (δ F)
    (δ F)
have δ : ∀ (x x_1 : C),
  Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1))
    (δ F x x_1) (δ F x x_1)
Tactic: ext
-- 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
a b : F.Monoidal
eq : Eq (α := F.LaxMonoidal) toLaxMonoidal toLaxMonoidal
x x_1 : C
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1))
    (δ F x x_1) (δ F x x_1)
have δ : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (Iso.hom (μIso F x x_1)) (δ F x x_1))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (Iso.hom (μIso F x x_1)) (δ F x x_1))
Tactic: rw [← cancel_epi (μIso F _ _).hom]
-- 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
a b : F.Monoidal
eq : Eq (α := F.LaxMonoidal) toLaxMonoidal toLaxMonoidal
x x_1 : C
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (Iso.hom (μIso F x x_1)) (δ F x x_1))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (Iso.hom (μIso F x x_1)) (δ F x x_1))
have δ : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (Iso.hom (μIso F x x_1)) (δ F x x_1))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (μ F x x_1) (δ F x x_1))
Tactic: rw [μIso_hom, μ_δ, ← @μ_δ _ _ _ _ _ _ _ a, ← μIso_hom]
-- 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
a b : F.Monoidal
eq : Eq (α := F.OplaxMonoidal) toOplaxMonoidal toOplaxMonoidal
⊢ a = b
have ε : Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (ε F)
Tactic: ext1
-- 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
a b : F.Monoidal
eq : Eq (α := F.OplaxMonoidal) toOplaxMonoidal toOplaxMonoidal
ε :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (LaxMonoidal.ε F)
    (LaxMonoidal.ε F)
⊢ a = b
have μ : Eq (α := (X Y : C) → tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
  (μ F) (μ F)
Tactic: ext1
-- 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
a b : F.Monoidal
eq : Eq (α := F.OplaxMonoidal) toOplaxMonoidal toOplaxMonoidal
ε :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (LaxMonoidal.ε F)
    (LaxMonoidal.ε F)
μ :
  Eq (α :=
    (X Y : C) → tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (LaxMonoidal.μ F) (LaxMonoidal.μ F)
⊢ a = b
have η : Eq (α := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η F) (η F)
Tactic: ext1
-- 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
a b : F.Monoidal
eq : Eq (α := F.OplaxMonoidal) toOplaxMonoidal toOplaxMonoidal
ε :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (LaxMonoidal.ε F)
    (LaxMonoidal.ε F)
μ :
  Eq (α :=
    (X Y : C) → tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (LaxMonoidal.μ F) (LaxMonoidal.μ F)
η :
  Eq (α := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (OplaxMonoidal.η F)
    (OplaxMonoidal.η F)
⊢ a = b
have δ : Eq (α := (X Y : C) → F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
  (δ F) (δ F)
Tactic: ext1
-- 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
a b : F.Monoidal
eq : Eq (α := F.OplaxMonoidal) toOplaxMonoidal toOplaxMonoidal
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (ε F)
have ε : Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
  (CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (Iso.inv (εIso F)))
  (CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (Iso.inv (εIso F)))
Tactic: rw [← cancel_mono (εIso _).inv]