mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁ X₂ X₃ Y₁ : LocalizedMonoidal L W ε
f₁ : X₁ ⟶ Y₁
⊢ f₁ ▷ X₂ ▷ X₃ ≫ (α_ Y₁ X₂ X₃).hom = (α_ X₁ X₂ X₃).hom ≫ f₁ ▷ (X₂ ⊗ X₃)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁ X₂ X₃ Y₂ : LocalizedMonoidal L W ε
f₂ : X₂ ⟶ Y₂
⊢ (X₁ ◁ f₂) ▷ X₃ ≫ (α_ X₁ Y₂ X₃).hom = (α_ X₁ X₂ X₃).hom ≫ X₁ ◁ f₂ ▷ X₃

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁ X₂ X₃ Y₃ : LocalizedMonoidal L W ε
f₃ : X₃ ⟶ Y₃
⊢ (X₁ ⊗ X₂) ◁ f₃ ≫ (α_ X₁ X₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ X₁ ◁ X₂ ◁ f₃

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁ X₂ X₃ Y₁ : LocalizedMonoidal L W ε
i : X₁ ≅ Y₁
⊢ i.hom ▷ X₂ ▷ X₃ ≫ (α_ Y₁ X₂ X₃).hom ≫ i.inv ▷ (X₂ ⊗ X₃) = (α_ X₁ X₂ X₃).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁ X₂ X₃ Y₂ : LocalizedMonoidal L W ε
i : X₂ ≅ Y₂
⊢ (X₁ ◁ i.hom) ▷ X₃ ≫ (α_ X₁ Y₂ X₃).hom ≫ X₁ ◁ i.inv ▷ X₃ = (α_ X₁ X₂ X₃).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁ X₂ X₃ Y₃ : LocalizedMonoidal L W ε
i : X₃ ≅ Y₃
⊢ (X₁ ⊗ X₂) ◁ i.hom ≫ (α_ X₁ X₂ Y₃).hom ≫ X₁ ◁ X₂ ◁ i.inv = (α_ X₁ X₂ X₃).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X : Dial C
⊢ (tensorUnitImpl.tensorObjImpl X).rel =
    (Subobject.pullback (prod.map (Limits.prod.leftUnitor X.src).hom (Limits.prod.leftUnitor X.tgt).hom)).obj X.rel

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X : Dial C
⊢ (X.tensorObjImpl tensorUnitImpl).rel =
    (Subobject.pullback (prod.map (Limits.prod.rightUnitor X.src).hom (Limits.prod.rightUnitor X.tgt).hom)).obj X.rel

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y Z : Dial C
⊢ ((X.tensorObjImpl Y).tensorObjImpl Z).rel =
    (Subobject.pullback (prod.map (prod.associator X.src Y.src Z.src).hom (prod.associator X.tgt Y.tgt Z.tgt).hom)).obj
      (X.tensorObjImpl (Y.tensorObjImpl Z)).rel

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ : Dial C
⊢ 𝟙 X₁ ⊗ₘ 𝟙 X₂ = 𝟙 (X₁ ⊗ X₂)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalLeftDistrib C
X Y Z : C
⊢ (∂L X Y Z).hom = coprod.desc (X ◁ coprod.inl) (X ◁ coprod.inr)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalLeftDistrib C
X Y Z : C
⊢ coprod.inl ≫ (∂L X Y Z).hom = X ◁ coprod.inl

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalLeftDistrib C
X Y Z : C
⊢ coprod.inr ≫ (∂L X Y Z).hom = X ◁ coprod.inr

Tactic:
rw [leftDistrib_hom, coprod.inr_desc]

Goal state after:
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalLeftDistrib C
X Y Z : C
⊢ coprod.inr ≫ (∂L X Y Z).hom = X ◁ coprod.inr

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalLeftDistrib C
X Y Z : C
⊢ X ◁ coprod.inl ≫ (∂L X Y Z).inv = coprod.inl

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalLeftDistrib C
X Y Z : C
⊢ X ◁ coprod.inr ≫ (∂L X Y Z).inv = coprod.inr

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalRightDistrib C
X Y Z : C
⊢ (∂R X Y Z).hom = coprod.desc (coprod.inl ▷ X) (coprod.inr ▷ X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalRightDistrib C
X Y Z : C
⊢ coprod.inl ≫ (∂R X Y Z).hom = coprod.inl ▷ X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
Y : D
f : inl X ⟶ inr Y
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
Y : D
f : inr X ⟶ inl Y
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalRightDistrib C
X Y Z : C
⊢ coprod.inr ≫ (∂R X Y Z).hom = coprod.inr ▷ X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalRightDistrib C
X Y Z : C
⊢ coprod.inl ▷ X ≫ (∂R X Y Z).inv = coprod.inl

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Basic

Goal state before:
pp: A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : A ⥤ C
G : B ⥤ C
x : A ⊕ B
⊢ Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (𝟙 x) =
    𝟙
      (match x with
      | inl X => F.obj X
      | inr X => G.obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalRightDistrib C
X Y Z : C
⊢ coprod.inr ▷ X ≫ (∂R X Y Z).inv = coprod.inr

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : BraidedCategory C
X Y Z : C
⊢ coprodComparison (tensorLeft X) Y Z ≫ (β_ X (Y ⨿ Z)).hom =
    coprod.map (β_ X Y).hom (β_ X Z).hom ≫ coprodComparison (tensorRight X) Y Z

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : SymmetricCategory C
X Y Z : C
⊢ coprodComparison (tensorRight X) Y Z ≫ (β_ (Y ⨿ Z) X).hom =
    coprod.map (β_ Y X).hom (β_ Z X).hom ≫ coprodComparison (tensorLeft X) Y Z

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v, u_1} C
inst✝³ : MonoidalCategory C
inst✝² : HasBinaryCoproducts C
inst✝¹ : SymmetricCategory C
inst✝ : IsMonoidalDistrib C
X Y Z : C
⊢ ∂R X Y Z = coprod.mapIso (β_ Y X) (β_ Z X) ≪≫ ∂L X Y Z ≪≫ β_ X (Y ⨿ Z)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : MonoidalClosed C
X : C
⊢ PreservesColimitsOfShape (Discrete WalkingPair) (tensorLeft X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ ((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v, u_1} C
inst✝³ : MonoidalCategory C
inst✝² : HasBinaryCoproducts C
inst✝¹ : SymmetricCategory C
inst✝ : MonoidalClosed C
⊢ IsMonoidalDistrib C

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Basic

Goal state before:
pp: A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : A ⥤ C
G : B ⥤ C
x y z : A ⊕ B
f : x ⟶ y
g : y ⟶ z
⊢ Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (f ≫ g) =
    Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) f ≫
      Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this : Pentagon (L'.obj X₁) (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)
⊢ ((α_ Y₁ Y₂ Y₃).hom ⊗ₘ 𝟙 Y₄) ≫ (α_ Y₁ (Y₂ ⊗ Y₃) Y₄).hom ≫ (𝟙 Y₁ ⊗ₘ (α_ Y₂ Y₃ Y₄).hom) =
    (((e₁.inv ⊗ₘ e₂.inv) ⊗ₘ e₃.inv) ⊗ₘ e₄.inv) ≫
      ((α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃)).hom ⊗ₘ 𝟙 (L'.obj X₄)) ≫
        (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫
          (e₁.hom ≫ 𝟙 Y₁ ⊗ₘ ((e₂.hom ⊗ₘ e₃.hom) ⊗ₘ e₄.hom) ≫ (α_ Y₂ Y₃ Y₄).hom)

Tactic:
tensor_comp,

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this : Pentagon (L'.obj X₁) (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)
⊢ ((α_ Y₁ Y₂ Y₃).hom ⊗ₘ 𝟙 Y₄) ≫ (α_ Y₁ (Y₂ ⊗ Y₃) Y₄).hom ≫ (𝟙 Y₁ ⊗ₘ (α_ Y₂ Y₃ Y₄).hom) =
    (((e₁.inv ⊗ₘ e₂.inv) ⊗ₘ e₃.inv) ⊗ₘ e₄.inv) ≫
      ((α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃)).hom ⊗ₘ 𝟙 (L'.obj X₄)) ≫
        (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫
          (e₁.hom ⊗ₘ (e₂.hom ⊗ₘ e₃.hom) ⊗ₘ e₄.hom) ≫ (𝟙 Y₁ ⊗ₘ (α_ Y₂ Y₃ Y₄).hom)
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : MonoidalClosed C
X Y Z : C
⊢ (∂L X Y Z).inv = uncurry (coprod.desc (curry coprod.inl) (curry coprod.inr))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Basic

Goal state before:
pp: A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : A ⥤ B
G : C ⥤ D
a a' : A
f : a ⟶ a'
⊢ (F.sum G).map ((Sum.inl_ A C).map f) = (Sum.inl_ B D).map (F.map f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Basic

Goal state before:
pp: A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : A ⥤ B
G : C ⥤ D
c c' : C
f : c ⟶ c'
⊢ (F.sum G).map ((Sum.inr_ A C).map f) = (Sum.inr_ B D).map (G.map f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Distributive.Cartesian

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsCartesianDistributive C
A B Z : C
f g : Z ⟶ (pair A B).obj { as := WalkingPair.left }
he : f ≫ (BinaryCofan.mk coprod.inl coprod.inr).inl = g ≫ (BinaryCofan.mk coprod.inl coprod.inr).inl
ι : A ⟶ A ⨿ B := coprod.inl
this : Mono (Z ◁ ι)
⊢ lift (𝟙 Z) f = lift (𝟙 Z) g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Distributive.Cartesian

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsCartesianDistributive C
A B Z : C
f g : Z ⟶ (pair A B).obj { as := WalkingPair.left }
he : f ≫ (BinaryCofan.mk coprod.inl coprod.inr).inl = g ≫ (BinaryCofan.mk coprod.inl coprod.inr).inl
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
c : Cofan X
hc : IsColimit c
π : (a : α) → X a ⟶ B
inst✝ : EffectiveEpiFamily X π
W✝ : C
e : c.pt ⟶ W✝
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ c.pt), g₁ ≫ hc.desc (Cofan.mk B π) = g₂ ≫ hc.desc (Cofan.mk B π) → g₁ ≫ e = g₂ ≫ e
Z✝ : C
a₁ a₂ : α
g₁ : Z✝ ⟶ X a₁
g₂ : Z✝ ⟶ X a₂
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
⊢ (g₁ ≫ c.ι.app { as := a₁ }) ≫ hc.desc (Cofan.mk B π) = (g₂ ≫ c.ι.app { as := a₂ }) ≫ hc.desc (Cofan.mk B π)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
c : Cofan X
hc : IsColimit c
π : (a : α) → X a ⟶ B
inst✝ : EffectiveEpiFamily X π
W✝ : C
e : c.pt ⟶ W✝
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ c.pt), g₁ ≫ hc.desc (Cofan.mk B π) = g₂ ≫ hc.desc (Cofan.mk B π) → g₁ ≫ e = g₂ ≫ e
Z✝ : C
a₁ a₂ : α
g₁ : Z✝ ⟶ X a₁
g₂ : Z✝ ⟶ X a₂
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
⊢ g₁ ≫ c.ι.app { as := a₁ } ≫ e = g₂ ≫ c.ι.app { as := a₂ } ≫ e

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
c : Cofan X
hc : IsColimit c
π : (a : α) → X a ⟶ B
inst✝ : EffectiveEpiFamily X π
W✝ : C
e : c.pt ⟶ W✝
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ c.pt), g₁ ≫ hc.desc (Cofan.mk B π) = g₂ ≫ hc.desc (Cofan.mk B π) → g₁ ≫ e = g₂ ≫ e
x✝ : Discrete α
j : α
⊢ c.ι.app { as := j } ≫ hc.desc (Cofan.mk B π) ≫ EffectiveEpiFamily.desc X π (fun a ↦ c.ι.app { as := a } ≫ e) ⋯ =
    c.ι.app { as := j } ≫ e

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
c : Cofan X
hc : IsColimit c
π : (a : α) → X a ⟶ B
inst✝ : EffectiveEpiFamily X π
W✝ : C
e : c.pt ⟶ W✝
x✝⁴ : ∀ {Z : C} (g₁ g₂ : Z ⟶ c.pt), g₁ ≫ hc.desc (Cofan.mk B π) = g₂ ≫ hc.desc (Cofan.mk B π) → g₁ ≫ e = g₂ ≫ e
m : (Cofan.mk B π).pt ⟶ W✝
hm : hc.desc (Cofan.mk B π) ≫ m = e
Z✝ : C
x✝³ x✝² : α
x✝¹ : Z✝ ⟶ X x✝³
x✝ : Z✝ ⟶ X x✝²
hg : x✝¹ ≫ π x✝³ = x✝ ≫ π x✝²
⊢ x✝¹ ≫ c.ι.app { as := x✝³ } ≫ e = x✝ ≫ c.ι.app { as := x✝² } ≫ e

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
c : Cofan X
hc : IsColimit c
π : (a : α) → X a ⟶ B
inst✝ : EffectiveEpiFamily X π
W✝ : C
e : c.pt ⟶ W✝
x✝¹ : ∀ {Z : C} (g₁ g₂ : Z ⟶ c.pt), g₁ ≫ hc.desc (Cofan.mk B π) = g₂ ≫ hc.desc (Cofan.mk B π) → g₁ ≫ e = g₂ ≫ e
m : (Cofan.mk B π).pt ⟶ W✝
hm : hc.desc (Cofan.mk B π) ≫ m = e
x✝ : α
⊢ π x✝ ≫ m = c.ι.app { as := x✝ } ≫ e

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝¹ : HasCoproduct X
inst✝ : EffectiveEpiFamily X π
⊢ EffectiveEpi (Sigma.desc π)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ (𝟙 (𝟙_ (Dial C)) ⊗ₘ f) ≫ (λ_ Y).hom = (λ_ X).hom ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Basic

Goal state before:
pp: A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F G : A ⊕ B ⥤ C
e₁ : Sum.inl_ A B ⋙ F ≅ Sum.inl_ A B ⋙ G
e₂ : Sum.inr_ A B ⋙ F ≅ Sum.inr_ A B ⋙ G
x y : A ⊕ B
f : x ⟶ y
⊢ F.map f ≫
      (match y with
        | inl x => e₁.app x
        | inr x => e₂.app x).hom =
    (match x with
        | inl x => e₁.app x
        | inr x => e₂.app x).hom ≫
      G.map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ (f ⊗ₘ 𝟙 (𝟙_ (Dial C))) ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Basic

Goal state before:
pp: A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F G : A ⥤ C
H I : B ⥤ C
α : F ⟶ G
β : H ⟶ I
X Y : A ⊕ B
f : X ⟶ Y
⊢ ((F.sum' H).map f ≫
      match Y with
      | inl X => α.app X
      | inr X => β.app X) =
    (match X with
      | inl X => α.app X
      | inr X => β.app X) ≫
      (G.sum' I).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
W X Y Z : Dial C
⊢ ((α_ W X Y).hom ⊗ₘ 𝟙 Z) ≫ (α_ W (X ⊗ Y) Z).hom ≫ (𝟙 W ⊗ₘ (α_ X Y Z).hom) = (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
⊢ (α_ X (𝟙_ (Dial C)) Y).hom ≫ (𝟙 X ⊗ₘ (λ_ Y).hom) = (ρ_ X).hom ⊗ₘ 𝟙 Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
⊢ (X ⊗ Y).rel =
    (Subobject.pullback (prod.map (prod.braiding X.src Y.src).hom (prod.braiding X.tgt Y.tgt).hom)).obj (Y ⊗ X).rel

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
⊢ (X.braiding Y).hom ≫ (Y.braiding X).hom = 𝟙 (X ⊗ Y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y Z : Dial C
f : Y ⟶ Z
⊢ (𝟙 X ⊗ₘ f) ≫ (X.braiding Z).hom = (X.braiding Y).hom ≫ (f ⊗ₘ 𝟙 X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
Z : Dial C
⊢ (f ⊗ₘ 𝟙 Z) ≫ (Y.braiding Z).hom = (X.braiding Z).hom ≫ (𝟙 Z ⊗ₘ f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y Z : Dial C
⊢ (α_ X Y Z).hom ≫ (X.braiding (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom =
    ((X.braiding Y).hom ⊗ₘ 𝟙 Z) ≫ (α_ Y X Z).hom ≫ (𝟙 Y ⊗ₘ (X.braiding Z).hom)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y Z : Dial C
⊢ (α_ X Y Z).inv ≫ ((X ⊗ Y).braiding Z).hom ≫ (α_ Z X Y).inv =
    (𝟙 X ⊗ₘ (Y.braiding Z).hom) ≫ (α_ X Z Y).inv ≫ ((X.braiding Z).hom ⊗ₘ 𝟙 Y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Basic

Goal state before:
pp: A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : A ⊕ C
f : X ⟶ Y
⊢ ((F.sum H).map f ≫
      match Y with
      | inl X => (Sum.inl_ B D).map (α.app X)
      | inr X => (Sum.inr_ B D).map (β.app X)) =
    (match X with
      | inl X => (Sum.inl_ B D).map (α.app X)
      | inr X => (Sum.inr_ B D).map (β.app X)) ≫
      (G.sum I).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sums.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
⊢ (equivalence C D).functor.IsEquivalence

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Extensive

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
α : Type
inst✝ : Finite α
B : C
X : α → C
π : (a : α) → X a ⟶ B
⊢ EffectiveEpi (Sigma.desc π) ↔ EffectiveEpiFamily X π

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Extensive

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : FinitaryPreExtensive C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
inst✝² : FinitaryPreExtensive D
F : C ⥤ D
inst✝¹ : PreservesFiniteCoproducts F
inst✝ : F.ReflectsEffectiveEpis
α : Type
x✝ : Finite α
B : C
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily (fun a ↦ F.obj (X a)) fun a ↦ F.map (π a)
⊢ EffectiveEpiFamily X π

Tactic:
by

Goal state after: