awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : F.Monoidal
inst_7 : G.Monoidal
inst_8 : (F ⋙ G).Monoidal
X Y : C
⊢ Eq (α := tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X) ((F ⋙ G).obj Y) ⟶ (F ⋙ G).obj Y)
    (CategoryStruct.comp (Y := tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X) ((F ⋙ G).obj Y))
      (CategoryStruct.comp (Y := (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (μ (F ⋙ G) X Y)
        (Iso.inv (μIso (F ⋙ G) X Y)))
      (snd ((F ⋙ G).obj X) ((F ⋙ G).obj Y)))
    (CategoryStruct.comp (Y := tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X) ((F ⋙ G).obj Y))
      (CategoryStruct.comp (Y := (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
        (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))
          (μ G (F.obj X) (F.obj Y)) (G.map (μ F X Y)))
        (Iso.inv (μIso (F ⋙ G) X Y)))
      (snd ((F ⋙ G).obj X) ((F ⋙ G).obj Y)))

Tactic:
simp [← Functor.comp_obj, ← Functor.map_comp]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
inst_5 : PreservesFiniteProducts F
change :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Iso.inv (Iso.symm (εIso F))) (Iso.inv (preservesTerminalIso F))
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F)
    (Iso.inv (preservesTerminalIso F))

Tactic:
change (εIso F).symm.inv = _

Premises used: CategoryTheory.Functor.Monoidal.εIso, CategoryTheory.Iso.symm, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
inst_5 : PreservesFiniteProducts F
e_self :
  Eq (α := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≅ tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (Iso.symm (εIso F))
    (preservesTerminalIso F)
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Iso.inv (Iso.symm (εIso F))) (Iso.inv (preservesTerminalIso F))

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
inst_5 : PreservesFiniteProducts F
⊢ Eq (α := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≅ tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (Iso.symm (εIso F))
    (preservesTerminalIso F)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
inst_5 : PreservesFiniteProducts F
X Y : C
change :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (Iso.inv (Iso.symm (μIso F X Y))) (Iso.inv (prodComparisonIso F X Y))
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (μ F X Y)
    (Iso.inv (prodComparisonIso F X Y))

Tactic:
change (μIso F X Y).symm.inv = _

Premises used: CategoryTheory.Functor.Monoidal.μIso, CategoryTheory.Iso.symm, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
inst_5 : PreservesFiniteProducts F
X Y : C
e_self :
  Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≅ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
    (Iso.symm (μIso F X Y)) (prodComparisonIso F X Y)
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (Iso.inv (Iso.symm (μIso F X Y))) (Iso.inv (prodComparisonIso F X Y))

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
inst_5 : PreservesFiniteProducts F
X Y : C
e_self :
  Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
    (Iso.hom (Iso.symm (μIso F X Y))) (Iso.hom (prodComparisonIso F X Y))
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≅ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
    (Iso.symm (μIso F X Y)) (prodComparisonIso F X Y)

Tactic:
ext : 1
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
inst_5 : PreservesFiniteProducts F
X Y : C
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
    (Iso.hom (Iso.symm (μIso F X Y))) (Iso.hom (prodComparisonIso F X Y))

Tactic:
simpa using δ_of_cartesianMonoidalCategory F X Y

Premises used: CategoryTheory.Functor.OplaxMonoidal.δ_of_cartesianMonoidalCategory
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
X Y Z : C
inst_6 : F.Monoidal
inst_7 : G.Monoidal
inst_8 : PreservesFiniteProducts F
⊢ Subsingleton F.Monoidal

Tactic:
(toOplaxMonoidal_injective F).subsingleton

Premises used: Function.Injective.subsingleton, CategoryTheory.Functor.Monoidal.toOplaxMonoidal_injective
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
X Y Z : C
inst_6 : F.Monoidal
⊢ PreservesFiniteProducts F

Tactic:
have (A B : _) : IsIso (CartesianMonoidalCategory.prodComparison F A B) :=
    δ_of_cartesianMonoidalCategory F A B ▸ inferInstance
  have : IsIso (CartesianMonoidalCategory.terminalComparison F) :=
    η_of_cartesianMonoidalCategory F ▸ inferInstance
  have := preservesLimitsOfShape_discrete_walkingPair_of_isIso_prodComparison F
  have := preservesLimit_empty_of_isIso_terminalComparison F
  have := Limits.preservesLimitsOfShape_pempty_of_preservesTerminal F
  .of_preserves_binary_and_terminal _

Premises used: CategoryTheory.Limits.PreservesFiniteProducts.of_preserves_binary_and_terminal, CategoryTheory.Functor.OplaxMonoidal.η_of_cartesianMonoidalCategory, CategoryTheory.Functor.OplaxMonoidal.δ_of_cartesianMonoidalCategory, Eq.rec, inferInstance, CategoryTheory.CartesianMonoidalCategory.preservesLimitsOfShape_discrete_walkingPair_of_isIso_prodComparison, CategoryTheory.CartesianMonoidalCategory.preservesLimit_empty_of_isIso_terminalComparison, CategoryTheory.Limits.preservesLimitsOfShape_pempty_of_preservesTerminal
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
⊢ Nonempty F.Monoidal ↔ PreservesFiniteProducts F

Tactic:
⟨fun ⟨_⟩ ↦ inferInstance, fun _ ↦ ⟨ofChosenFiniteProducts F⟩⟩

Premises used: CategoryTheory.Functor.Monoidal.ofChosenFiniteProducts, inferInstance, Nonempty.intro, Iff.intro, _private.0.CategoryTheory.Functor.Monoidal.nonempty_monoidal_iff_preservesFiniteProducts.match_1, CategoryTheory.Limits.PreservesFiniteProducts
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
X_1 Y_1 Z : C
inst_6 : BraidedCategory.{v₁, u₁} C
inst_7 : BraidedCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_8 : PreservesFiniteProducts F
X Y : C
rw :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) (μ F X Y ≫ F.map (Iso.hom (β_ X Y)))
      (Iso.inv (Monoidal.μIso F Y X)))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) (Iso.hom (β_ (F.obj X) (F.obj Y)) ≫ μ F Y X)
      (Iso.inv (Monoidal.μIso F Y X)))
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))
    (μ F X Y ≫ F.map (Iso.hom (β_ X Y))) (Iso.hom (β_ (F.obj X) (F.obj Y)) ≫ μ F Y X)

Tactic:
rw [← cancel_mono (Monoidal.μIso _ _ _).inv]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Functor.Monoidal.μIso, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
X_1 Y_1 Z : C
inst_6 : BraidedCategory.{v₁, u₁} C
inst_7 : BraidedCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_8 : PreservesFiniteProducts F
X Y : C
h_fst :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj Y)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X))
      (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) (μ F X Y ≫ F.map (Iso.hom (β_ X Y)))
        (Iso.inv (Monoidal.μIso F Y X)))
      (fst (F.obj Y) (F.obj X)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X))
      (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))
        (Iso.hom (β_ (F.obj X) (F.obj Y)) ≫ μ F Y X) (Iso.inv (Monoidal.μIso F Y X)))
      (fst (F.obj Y) (F.obj X)))
h_snd :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X))
      (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) (μ F X Y ≫ F.map (Iso.hom (β_ X Y)))
        (Iso.inv (Monoidal.μIso F Y X)))
      (snd (F.obj Y) (F.obj X)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X))
      (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))
        (Iso.hom (β_ (F.obj X) (F.obj Y)) ≫ μ F Y X) (Iso.inv (Monoidal.μIso F Y X)))
      (snd (F.obj Y) (F.obj X)))
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) (μ F X Y ≫ F.map (Iso.hom (β_ X Y)))
      (Iso.inv (Monoidal.μIso F Y X)))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) (Iso.hom (β_ (F.obj X) (F.obj Y)) ≫ μ F Y X)
      (Iso.inv (Monoidal.μIso F Y X)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
X_1 Y_1 Z : C
inst_6 : BraidedCategory.{v₁, u₁} C
inst_7 : BraidedCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_8 : PreservesFiniteProducts F
X Y : C
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj Y)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X))
      (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) (μ F X Y ≫ F.map (Iso.hom (β_ X Y)))
        (Iso.inv (Monoidal.μIso F Y X)))
      (fst (F.obj Y) (F.obj X)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X))
      (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))
        (Iso.hom (β_ (F.obj X) (F.obj Y)) ≫ μ F Y X) (Iso.inv (Monoidal.μIso F Y X)))
      (fst (F.obj Y) (F.obj X)))

Tactic:
simp [← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
X_1 Y_1 Z : C
inst_6 : BraidedCategory.{v₁, u₁} C
inst_7 : BraidedCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_8 : PreservesFiniteProducts F
X Y : C
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X))
      (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) (μ F X Y ≫ F.map (Iso.hom (β_ X Y)))
        (Iso.inv (Monoidal.μIso F Y X)))
      (snd (F.obj Y) (F.obj X)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj X))
      (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))
        (Iso.hom (β_ (F.obj X) (F.obj Y)) ≫ μ F Y X) (Iso.inv (Monoidal.μIso F Y X)))
      (snd (F.obj Y) (F.obj X)))

Tactic:
simp [← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
X Y Z : C
inst_6 : BraidedCategory.{v₁, u₁} C
inst_7 : BraidedCategory.{v₂, u₂} D
⊢ Subsingleton F.Braided

Tactic:
(Braided.toMonoidal_injective F).subsingleton

Premises used: Function.Injective.subsingleton, CategoryTheory.Functor.Braided.toMonoidal_injective
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : PreservesFiniteProducts F
X Y : F.EssImageSubcategory
⊢ (tensorObj.{v₂, u₂} (𝒞 := ObjectProperty.FullSubcategory.category F.essImage) X Y).obj (P := F.essImage) =
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (X.obj (P := F.essImage)) (Y.obj (P := F.essImage))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : PreservesFiniteProducts F
T X Y : F.EssImageSubcategory
f : T ⟶ X
g : T ⟶ Y
⊢ Eq (α := T ⟶ tensorObj.{v₂, u₂} (𝒞 := ObjectProperty.FullSubcategory.category F.essImage) X Y) (lift f g)
    (ObjectProperty.homMk (P := F.essImage) (lift f.hom g.hom))

Tactic:
rfl

Premises used: CategoryTheory.CartesianMonoidalCategory.lift, CategoryTheory.ObjectProperty.homMk, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : PreservesFiniteProducts F
X Y Z : F.EssImageSubcategory
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := ObjectProperty.FullSubcategory.category F.essImage)
        (tensorObj.{v₂, u₂} (𝒞 := ObjectProperty.FullSubcategory.category F.essImage) X Y) Z ⟶
      tensorObj.{v₂, u₂} (𝒞 := ObjectProperty.FullSubcategory.category F.essImage) X
        (tensorObj.{v₂, u₂} (𝒞 := ObjectProperty.FullSubcategory.category F.essImage) Y Z))
    (Iso.hom (α_ X Y Z))
    (ObjectProperty.homMk (P := F.essImage)
      (Iso.hom (α_ (X.obj (P := F.essImage)) (Y.obj (P := F.essImage)) (Z.obj (P := F.essImage)))))

Tactic:
rfl

Premises used: CategoryTheory.ObjectProperty.homMk, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : PreservesFiniteProducts F
X Y Z : F.EssImageSubcategory
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := ObjectProperty.FullSubcategory.category F.essImage) X
        (tensorObj.{v₂, u₂} (𝒞 := ObjectProperty.FullSubcategory.category F.essImage) Y Z) ⟶
      tensorObj.{v₂, u₂} (𝒞 := ObjectProperty.FullSubcategory.category F.essImage)
        (tensorObj.{v₂, u₂} (𝒞 := ObjectProperty.FullSubcategory.category F.essImage) X Y) Z)
    (Iso.inv (α_ X Y Z))
    (ObjectProperty.homMk (P := F.essImage)
      (Iso.inv (α_ (X.obj (P := F.essImage)) (Y.obj (P := F.essImage)) (Z.obj (P := F.essImage)))))

Tactic:
rfl

Premises used: CategoryTheory.ObjectProperty.homMk, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : PreservesFiniteProducts F
X : F.EssImageSubcategory
⊢ Eq (α := X ⟶ tensorUnit.{v₂, u₂} F.EssImageSubcategory (𝒞 := ObjectProperty.FullSubcategory.category F.essImage))
    (toUnit X) (ObjectProperty.homMk (P := F.essImage) (toUnit (X.obj (P := F.essImage))))

Tactic:
rfl

Premises used: CategoryTheory.Limits.IsTerminal.from, CategoryTheory.ObjectProperty.homMk, CategoryTheory.SemiCartesianMonoidalCategory.toUnit, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
G_1 : Functor.{v₂, v₃, u₂, u₃} D E
X_1 Y_1 Z : C
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.Monoidal
inst_7 : G.Monoidal
α : F ⟶ G
X Y : C
rw :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
      (μ F X Y ≫ α.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (Iso.inv (Functor.Monoidal.μIso G X Y)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ((α.app X ⊗ₘ α.app Y) ≫ μ G X Y)
      (Iso.inv (Functor.Monoidal.μIso G X Y)))
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (μ F X Y ≫ α.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ((α.app X ⊗ₘ α.app Y) ≫ μ G X Y)

Tactic:
rw [← cancel_mono (Functor.Monoidal.μIso _ _ _).inv]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Functor.Monoidal.μIso, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
G_1 : Functor.{v₂, v₃, u₂, u₃} D E
X_1 Y_1 Z : C
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.Monoidal
inst_7 : G.Monoidal
α : F ⟶ G
X Y : C
rw :
  Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
      (Iso.inv (Functor.Monoidal.μIso F X Y))
      (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
        (μ F X Y ≫ α.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (Iso.inv (Functor.Monoidal.μIso G X Y))))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
      (Iso.inv (Functor.Monoidal.μIso F X Y))
      (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ((α.app X ⊗ₘ α.app Y) ≫ μ G X Y)
        (Iso.inv (Functor.Monoidal.μIso G X Y))))
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
      (μ F X Y ≫ α.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (Iso.inv (Functor.Monoidal.μIso G X Y)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ((α.app X ⊗ₘ α.app Y) ≫ μ G X Y)
      (Iso.inv (Functor.Monoidal.μIso G X Y)))

Tactic:
rw [← cancel_epi (Functor.Monoidal.μIso _ _ _).inv]

Premises used: CategoryTheory.Functor.Monoidal.μIso, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv