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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G F'✝ G' : C ⥤ D
α : F ⟶ G
β : F'✝ ⟶ G'
F' : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (tensorObj F F').map f ≫ α.app Y ▷ F'.obj Y = α.app X ▷ F'.obj X ≫ (tensorObj G F').map f

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
⊢ ∀ {X₁ Y₁ X₂ Y₂ : C ⥤ D} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂), f ⊗ₘ g = f ▷ X₂ ≫ Y₁ ◁ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : CartesianMonoidalCategory C
F : J ⥤ C
j : J
⊢ (λ_ F).inv.app j = (λ_ (F.obj j)).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : CartesianMonoidalCategory C
F : J ⥤ C
j : J
⊢ (ρ_ F).inv.app j = (ρ_ (F.obj j)).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Types

Goal state before:
pp: C✝ : Type v₂
inst✝¹ : Category.{v₁, v₂} C✝
C : Type v₁
inst✝ : SmallCategory C
F : C ⥤ Type v₁
⊢ ∀ (X : Type v₁), PreservesColimits (tensorLeft X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : CartesianMonoidalCategory C
F₁ F₁' F₂ F₂' : J ⥤ C
f : F₁ ⟶ F₁'
g : F₂ ⟶ F₂'
j : J
⊢ (f ⊗ₘ g).app j ≫ fst (F₁'.obj j) (F₂'.obj j) = fst (F₁.obj j) (F₂.obj j) ≫ f.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Types

Goal state before:
pp: C✝ : Type v₂
inst✝¹ : Category.{v₁, v₂} C✝
C : Type v₁
inst✝ : SmallCategory C
F : C ⥤ Type v₁
this : ∀ (X : Type v₁), PreservesColimits (tensorLeft X)
⊢ ∀ {J : Type v₁} [inst : Category.{v₁, v₁} J], PreservesColimitsOfShape J (tensorLeft F)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G H K : C ⥤ D
⊢ (α_ F G H).hom ▷ K ≫ (α_ F (G ⊗ H) K).hom ≫ F ◁ (α_ G H K).hom = (α_ (F ⊗ G) H K).hom ≫ (α_ F G (H ⊗ K)).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : CartesianMonoidalCategory C
F₁ F₁' F₂ F₂' : J ⥤ C
f : F₁ ⟶ F₁'
g : F₂ ⟶ F₂'
j : J
⊢ (f ⊗ₘ g).app j ≫ snd (F₁'.obj j) (F₂'.obj j) = snd (F₁.obj j) (F₂.obj j) ≫ g.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Types

Goal state before:
pp: C✝ : Type v₂
inst✝¹ : Category.{v₁, v₂} C✝
C : Type v₁
inst✝ : SmallCategory C
F : C ⥤ Type v₁
⊢ Closed F

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : CartesianMonoidalCategory C
F₁ F₂ F₂' : J ⥤ C
g : F₂ ⟶ F₂'
j : J
⊢ (F₁ ◁ g).app j ≫ fst (F₁.obj j) (F₂'.obj j) = fst (F₁.obj j) (F₂.obj j)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : CartesianMonoidalCategory C
F₁ F₂ F₂' : J ⥤ C
g : F₂ ⟶ F₂'
j : J
⊢ (F₁ ◁ g).app j ≫ snd (F₁.obj j) (F₂'.obj j) = snd (F₁.obj j) (F₂.obj j) ≫ g.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : CartesianMonoidalCategory C
F₁ F₁' : J ⥤ C
f : F₁ ⟶ F₁'
F₂ : J ⥤ C
j : J
⊢ (f ▷ F₂).app j ≫ fst (F₁'.obj j) (F₂.obj j) = fst (F₁.obj j) (F₂.obj j) ≫ f.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : CartesianMonoidalCategory C
F₁ F₁' : J ⥤ C
f : F₁ ⟶ F₁'
F₂ : J ⥤ C
j : J
⊢ (f ▷ F₂).app j ≫ snd (F₁'.obj j) (F₂.obj j) = snd (F₁.obj j) (F₂.obj j)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : CartesianMonoidalCategory C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ (α_ F₁ F₂ F₃).hom.app j = (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).hom

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F G H : C ⥤ D
⊢ (α_ F G H).hom ≫ (NatIso.ofComponents (fun x ↦ β_ (F.obj x) ((G ⊗ H).obj x)) ⋯).hom ≫ (α_ G H F).hom =
    (NatIso.ofComponents (fun x ↦ β_ (F.obj x) (G.obj x)) ⋯).hom ▷ H ≫
      (α_ G F H).hom ≫ G ◁ (NatIso.ofComponents (fun x ↦ β_ (F.obj x) (H.obj x)) ⋯).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : CartesianMonoidalCategory C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ (α_ F₁ F₂ F₃).inv.app j = (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).inv

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F G H : C ⥤ D
⊢ (α_ F G H).inv ≫ (NatIso.ofComponents (fun x ↦ β_ ((F ⊗ G).obj x) (H.obj x)) ⋯).hom ≫ (α_ H F G).inv =
    F ◁ (NatIso.ofComponents (fun x ↦ β_ (G.obj x) (H.obj x)) ⋯).hom ≫
      (α_ F H G).inv ≫ (NatIso.ofComponents (fun x ↦ β_ (F.obj x) (H.obj x)) ⋯).hom ▷ G

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁸ : Category.{v_1, u_1} J
inst✝⁷ : Category.{v_2, u_2} C
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : Category.{v_4, u_4} E
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory E
K : Type u_5
inst✝² : Category.{v_5, u_5} K
inst✝¹ : HasColimitsOfShape K C
inst✝ : ∀ (X : C), PreservesColimitsOfShape K (tensorLeft X)
F : J ⥤ C
⊢ PreservesColimitsOfShape K (tensorLeft F)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : SymmetricCategory D
F G : C ⥤ D
⊢ (β_ F G).hom ≫ (β_ G F).hom = 𝟙 (F ⊗ G)

Tactic:
by

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

Goal state before:
pp: C✝ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁷ : Category.{v₂, u₂} D✝
inst✝⁶ : MonoidalCategory D✝
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Category.{v_3, u_3} E
inst✝² : MonoidalCategory D
inst✝¹ : MonoidalCategory E
L : D ⥤ E
inst✝ : L.OplaxMonoidal
⊢ ∀ (X : C ⥤ D),
    (λ_ (((Functor.whiskeringRight C D E).obj L).obj X)).inv =
      ((Functor.whiskeringRight C D E).obj L).map (λ_ X).inv ≫
        { app := fun X_1 ↦ δ L ((𝟙_ (C ⥤ D)).obj X_1) (X.obj X_1), naturality := ⋯ } ≫
          { app := fun X ↦ η L, naturality := ⋯ } ▷ ((Functor.whiskeringRight C D E).obj L).obj X

Tactic:
by

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

Goal state before:
pp: C✝ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁷ : Category.{v₂, u₂} D✝
inst✝⁶ : MonoidalCategory D✝
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Category.{v_3, u_3} E
inst✝² : MonoidalCategory D
inst✝¹ : MonoidalCategory E
L : D ⥤ E
inst✝ : L.OplaxMonoidal
⊢ ∀ (X : C ⥤ D),
    (ρ_ (((Functor.whiskeringRight C D E).obj L).obj X)).inv =
      ((Functor.whiskeringRight C D E).obj L).map (ρ_ X).inv ≫
        { app := fun X_1 ↦ δ L (X.obj X_1) ((𝟙_ (C ⥤ D)).obj X_1), naturality := ⋯ } ≫
          ((Functor.whiskeringRight C D E).obj L).obj X ◁ { app := fun X ↦ η L, naturality := ⋯ }

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u_1
inst✝¹ : Category.{v_1, u_1} E
inst✝ : MonoidalCategory E
e : C ≌ D
X Y : D ⥤ E
⊢ Functor.LaxMonoidal.μ e.congrLeft.inverse X Y =
    e.congrLeft.toAdjunction.unit.app (e.congrLeft.inverse.obj X ⊗ e.congrLeft.inverse.obj Y) ≫
      e.congrLeft.inverse.map
        (Functor.OplaxMonoidal.δ e.congrLeft.functor (e.congrLeft.inverse.obj X) (e.congrLeft.inverse.obj Y) ≫
          (e.congrLeft.toAdjunction.counit.app X ⊗ₘ e.congrLeft.toAdjunction.counit.app Y))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁶ : Category.{v_1, u_1} J
inst✝⁵ : Category.{v_2, u_2} C
inst✝⁴ : Category.{v_3, u_3} D
inst✝³ : Category.{v_4, u_4} E
inst✝² : CartesianMonoidalCategory C
inst✝¹ : CartesianMonoidalCategory E
F G : D ⥤ C
H : C ⥤ E
inst✝ : PreservesFiniteProducts H
X Y : D
f : X ⟶ Y
⊢ ((F ⊗ G) ⋙ H).map f ≫ (prodComparisonIso H (F.obj Y) (G.obj Y)).hom =
    (prodComparisonIso H (F.obj X) (G.obj X)).hom ≫ (F ⋙ H ⊗ G ⋙ H).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_4, u_4} E
inst✝¹ : CartesianMonoidalCategory C
inst✝ : CartesianMonoidalCategory E
F G : Cᵒᵖ ⥤ Type v
X Y : C
h₁ : F.RepresentableBy X
h₂ : G.RepresentableBy Y
I W : C
f : I ⟶ W
g : W ⟶ X ⊗ Y
⊢ (homEquivToProd.trans (h₁.homEquiv.prodCongr h₂.homEquiv)) (f ≫ g) =
    (ConcreteCategory.hom ((F ⊗ G).map f.op)) ((homEquivToProd.trans (h₁.homEquiv.prodCongr h₂.homEquiv)) g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Products.Bifunctor

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
W : C
X Y Z : D
f : X ⟶ Y
g : Y ⟶ Z
⊢ F.map (𝟙 W ×ₘ f ≫ g) = F.map (𝟙 W ×ₘ f) ≫ F.map (𝟙 W ×ₘ g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Products.Bifunctor

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
X Y Z : C
W : D
f : X ⟶ Y
g : Y ⟶ Z
⊢ F.map (f ≫ g ×ₘ 𝟙 W) = F.map (f ×ₘ 𝟙 W) ≫ F.map (g ×ₘ 𝟙 W)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Products.Bifunctor

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
X X' : C
f : X ⟶ X'
Y Y' : D
g : Y ⟶ Y'
⊢ F.map (𝟙 X ×ₘ g) ≫ F.map (f ×ₘ 𝟙 Y') = F.map (f ×ₘ g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Products.Bifunctor

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
X X' : C
f : X ⟶ X'
Y Y' : D
g : Y ⟶ Y'
⊢ F.map (f ×ₘ 𝟙 Y) ≫ F.map (𝟙 X' ×ₘ g) = F.map (f ×ₘ g)

Tactic:
by

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

Goal state before:
pp: J₁ : Type u₁
J₂ : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} J₁
inst✝² : Category.{v₂, u₂} J₂
inst✝¹ : Category.{v₃, u₃} C
inst✝ : MonoidalCategory C
x✝ : (J₁ ⥤ C) × (J₁ ⥤ C)
⊢ ∀ {X Y : J₁} (f : X ⟶ Y),
    ((externalProductBifunctor J₁ J₁ C ⋙ (whiskeringLeft J₁ (J₁ × J₁) C).obj (diag J₁)).obj x✝).map f ≫
        (Iso.refl
            (((externalProductBifunctor J₁ J₁ C ⋙ (whiskeringLeft J₁ (J₁ × J₁) C).obj (diag J₁)).obj x✝).obj Y)).hom =
      (Iso.refl
            (((externalProductBifunctor J₁ J₁ C ⋙ (whiskeringLeft J₁ (J₁ × J₁) C).obj (diag J₁)).obj x✝).obj X)).hom ≫
        ((tensor (J₁ ⥤ C)).obj x✝).map f

Tactic:
by

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

Goal state before:
pp: J₁ : Type u₁
J₂ : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} J₁
inst✝² : Category.{v₂, u₂} J₂
inst✝¹ : Category.{v₃, u₃} C
inst✝ : MonoidalCategory C
X✝ Y✝ : (J₁ ⥤ C) × (J₁ ⥤ C)
x✝ : X✝ ⟶ Y✝
⊢ (externalProductBifunctor J₁ J₁ C ⋙ (whiskeringLeft J₁ (J₁ × J₁) C).obj (diag J₁)).map x✝ ≫
      (NatIso.ofComponents
          (fun x ↦
            Iso.refl
              (((externalProductBifunctor J₁ J₁ C ⋙ (whiskeringLeft J₁ (J₁ × J₁) C).obj (diag J₁)).obj Y✝).obj x))
          ⋯).hom =
    (NatIso.ofComponents
          (fun x ↦
            Iso.refl
              (((externalProductBifunctor J₁ J₁ C ⋙ (whiskeringLeft J₁ (J₁ × J₁) C).obj (diag J₁)).obj X✝).obj x))
          ⋯).hom ≫
      (tensor (J₁ ⥤ C)).map x✝

Tactic:
by

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

Goal state before:
pp: J₁ : Type u₁
J₂ : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} J₁
inst✝³ : Category.{v₂, u₂} J₂
inst✝² : Category.{v₃, u₃} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
x✝ : (J₁ ⥤ C) × (J₂ ⥤ C)
⊢ ∀ {X Y : J₂ × J₁} (f : X ⟶ Y),
    ((externalProductBifunctor J₁ J₂ C ⋙ (whiskeringLeft (J₂ × J₁) (J₁ × J₂) C).obj (Prod.swap J₂ J₁)).obj x✝).map f ≫
        (β_ (x✝.1.obj ((Prod.swap J₂ J₁).obj Y).1) (x✝.2.obj ((Prod.swap J₂ J₁).obj Y).2)).hom =
      (β_ (x✝.1.obj ((Prod.swap J₂ J₁).obj X).1) (x✝.2.obj ((Prod.swap J₂ J₁).obj X).2)).hom ≫
        ((Prod.swap (J₁ ⥤ C) (J₂ ⥤ C) ⋙ externalProductBifunctor J₂ J₁ C).obj x✝).map f

Tactic:
by

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

Goal state before:
pp: J₁ : Type u₁
J₂ : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} J₁
inst✝³ : Category.{v₂, u₂} J₂
inst✝² : Category.{v₃, u₃} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X✝ Y✝ : (J₁ ⥤ C) × (J₂ ⥤ C)
x✝ : X✝ ⟶ Y✝
⊢ (externalProductBifunctor J₁ J₂ C ⋙ (whiskeringLeft (J₂ × J₁) (J₁ × J₂) C).obj (Prod.swap J₂ J₁)).map x✝ ≫
      (NatIso.ofComponents (fun x ↦ β_ (Y✝.1.obj ((Prod.swap J₂ J₁).obj x).1) (Y✝.2.obj ((Prod.swap J₂ J₁).obj x).2))
          ⋯).hom =
    (NatIso.ofComponents (fun x ↦ β_ (X✝.1.obj ((Prod.swap J₂ J₁).obj x).1) (X✝.2.obj ((Prod.swap J₂ J₁).obj x).2))
          ⋯).hom ≫
      (Prod.swap (J₁ ⥤ C) (J₂ ⥤ C) ⋙ externalProductBifunctor J₂ J₁ C).map x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsConnected C
s : Cocone (constPUnitFunctor C)
j : C
⊢ (pUnitCocone C).ι.app j ≫ s.ι.app Classical.ofNonempty = s.ι.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsConnected C
s : Cocone (constPUnitFunctor C)
m : (pUnitCocone C).pt ⟶ s.pt
h : ∀ (j : C), (pUnitCocone C).ι.app j ≫ m = s.ι.app j
⊢ m = s.ι.app Classical.ofNonempty

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsPreconnected C
inst✝ : HasColimit (constPUnitFunctor C)
a b : colimit (constPUnitFunctor C)
⊢ a = b

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
c d : (j : C) × F.obj j
h : Relation.EqvGen F.ColimitTypeRel c d
⊢ Zigzag c.fst d.fst

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimit (constPUnitFunctor C)
⊢ IsConnected C ↔ Nonempty (colimit (constPUnitFunctor C) ≅ PUnit.{w + 1})

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ IsConnected C ↔ Nonempty (IsColimit (pUnitCocone C))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Final
⊢ IsConnected C ↔ IsConnected D

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Initial
⊢ IsConnected C ↔ IsConnected D

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
x : C
h : Limits.IsInitial x
⊢ IsConnected C

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
x : C
h : Limits.IsTerminal x
⊢ IsConnected C

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsSifted C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
e : D ≌ C
this : D × D ≌ C × C := e.prod e
c : C
⊢ (e.inverse ⋙ Functor.diag D ⋙ this.functor).obj c ≅ (Functor.diag C).obj c

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsSifted C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
e : D ≌ C
⊢ (Functor.diag D).Final

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsSifted C
c₁ c₂ : C
⊢ (Functor.diag C).Final

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsSifted C
⊢ ∀ (j₁ j₂ : C), ∃ l, List.IsChain Zag (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
⊢ IsSiftedOrEmpty C

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝ : SmallCategory C
X Y : C ⥤ Type u
⊢ (HasColimit.isoOfNatIso ((externalProductCompDiagIso C (Type u)).app (X, Y)).symm).hom ≫
      colimit.pre (X ⊠ Y) (Functor.diag C) ≫
        (PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂ X Y (curriedTensor (Type u))).hom =
    CartesianMonoidalCategory.prodComparison colim X Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
X Y : C ⥤ Type u
inst✝ : IsSifted C
⊢ IsIso (CartesianMonoidalCategory.prodComparison colim X Y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
X Y : C ⥤ Type u
inst✝ : IsSifted C
⊢ PreservesLimitsOfShape (Discrete WalkingPair) colim

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
X Y : C ⥤ Type u
inst✝ : IsSifted C
⊢ PreservesLimit (empty (C ⥤ Type u)) colim

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) colim
⊢ IsSiftedOrEmpty C

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : PreservesLimitsOfShape (Discrete (Fin 0)) colim
connected : IsConnected C
⊢ Nonempty C

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : PreservesLimitsOfShape (Discrete (Fin 0)) colim
⊢ Nonempty C

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝ : SmallCategory C
h : PreservesFiniteProducts colim
⊢ IsSifted C

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝³ : SmallCategory C
D : Type u
inst✝² : SmallCategory D
inst✝¹ : IsSifted C
F : C ⥤ D
inst✝ : F.Final
⊢ IsSifted D

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
h₁ : IsSifted C
F : C ⥤ D
inst✝ : F.Final
⊢ IsSifted D

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
⊢ Nonempty (StructuredArrow d F)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
c : C
t : IsFiltered.max f.right g.right ⟶ c
ht :
  (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right)) ≫ F.map t =
    (g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right)) ≫ F.map t
⊢ g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right ≫ t) =
    (StructuredArrow.mk (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right ≫ t))).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
η μ : f ⟶ g
⊢ g.hom ≫ F.map (IsFiltered.coeqHom (StructuredArrow.Hom.right η) (StructuredArrow.Hom.right μ)) =
    (StructuredArrow.mk
        (f.hom ≫
          F.map
            (StructuredArrow.Hom.right η ≫
              IsFiltered.coeqHom (StructuredArrow.Hom.right η) (StructuredArrow.Hom.right μ)))).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
⊢ IsFiltered (StructuredArrow d F)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (F.obj c ⟶ d)
h₂ : ∀ {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'
⊢ IsCofiltered (CostructuredArrow F d)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
inst✝ : IsCofiltered (CostructuredArrow F d)
c₁ c₂ : C
s₁ : F.obj c₁ ⟶ d
s₂ : F.obj c₂ ⟶ d
⊢ ∃ c t₁ t₂, F.map t₁ ≫ s₁ = F.map t₂ ≫ s₂

Tactic:
by

Goal state after: