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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
i j : K
f : i ⟶ j
⊢ (colimitObjIsoColimitCompEvaluation F i).inv ≫ (colimit F).map f =
    colimMap (F.whiskerLeft ((evaluation K C).map f)) ≫ (colimitObjIsoColimitCompEvaluation F j).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
P : Cᵒᵖ ⥤ Type w
s : P.obj (op X)
Y : C
f : Y ⟶ X
⊢ (ConcreteCategory.hom ((shrinkYonedaEquiv.symm s).app (op Y))) (shrinkYonedaObjObjEquiv.symm f) =
    (ConcreteCategory.hom (P.map f.op)) s

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X✝ Y✝ : C
f : shrinkYoneda.{w, v, u}.obj X✝ ⟶ shrinkYoneda.{w, v, u}.obj Y✝
⊢ shrinkYoneda.{w, v, u}.map (shrinkYonedaObjObjEquiv (shrinkYonedaEquiv f)) = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ shrinkYonedaObjObjEquiv (shrinkYonedaEquiv (shrinkYoneda.{w, v, u}.map f)) = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
i j : K
f : i ⟶ j
⊢ (colimit F).map f ≫ (colimitObjIsoColimitCompEvaluation F j).hom =
    (colimitObjIsoColimitCompEvaluation F i).hom ≫ colimMap (F.whiskerLeft ((evaluation K C).map f))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
⊢ ∀ {X_1 Y : Cᵒᵖ} (f : X_1 ⟶ Y),
    (shrinkYoneda.{v, v, u}.obj X).map f ≫ shrinkYonedaObjObjEquiv.toIso.hom =
      shrinkYonedaObjObjEquiv.toIso.hom ≫ (yoneda.obj X).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
H : J ⥤ K ⥤ C
inst✝ : HasColimitsOfShape J C
k : K
W : C
f g : (colimit H).obj k ⟶ W
w : ∀ (j : J), (colimit.ι H j).app k ≫ f = (colimit.ι H j).app k ≫ g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
G : D ⥤ K
inst✝ : HasColimitsOfShape J C
j : J
⊢ colimit.ι (F ⋙ (whiskeringLeft D K C).obj G) j ≫ (colimitCompWhiskeringLeftIsoCompColimit F G).hom =
    G.whiskerLeft (colimit.ι F j)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
⊢ ∀ {X Y : C} (f : X ⟶ Y),
    shrinkYoneda.{v, v, u}.map f ≫ (NatIso.ofComponents (fun Y_1 ↦ shrinkYonedaObjObjEquiv.toIso) ⋯).hom =
      (NatIso.ofComponents (fun Y ↦ shrinkYonedaObjObjEquiv.toIso) ⋯).hom ≫ yoneda.map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
G : D ⥤ K
inst✝ : HasColimitsOfShape J C
j : J
⊢ G.whiskerLeft (colimit.ι F j) ≫ (colimitCompWhiskeringLeftIsoCompColimit F G).inv =
    colimit.ι (F ⋙ (whiskeringLeft D K C).obj G) j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : LocallySmall.{max w w', v, u} C
X✝ Y✝ : C
x✝ : X✝ ⟶ Y✝
⊢ (shrinkYoneda.{w, v, u} ⋙ (Functor.whiskeringRight Cᵒᵖ (Type w) (Type (max w w'))).obj uliftFunctor.{w', w}).map x✝ ≫
      (FunctorToTypes.shrinkCompUliftFunctorIso (yoneda.obj Y✝)).hom =
    (FunctorToTypes.shrinkCompUliftFunctorIso (yoneda.obj X✝)).hom ≫ shrinkYoneda.{max w w', v, u}.map x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : D ⥤ K ⥤ C
G : J ⥤ D
H : ∀ (k : K), PreservesLimit G (F ⋙ (evaluation K C).obj k)
c : Cone G
hc : IsLimit c
⊢ IsLimit (F.mapCone c)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ (uliftYoneda.{w', v, u}.obj X).map f ≫ (Equiv.ulift.trans shrinkYonedaObjObjEquiv.symm).toIso.hom =
    (Equiv.ulift.trans shrinkYonedaObjObjEquiv.symm).toIso.hom ≫ (shrinkYoneda.{max w' v, v, u}.obj X).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : D ⥤ K ⥤ C
G : J ⥤ D
H : ∀ (k : K), PreservesColimit G (F ⋙ (evaluation K C).obj k)
c : Cocone G
hc : IsColimit c
⊢ IsColimit (F.mapCocone c)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X✝ Y✝ : C
g : X✝ ⟶ Y✝
⊢ uliftYoneda.{w', v, u}.map g ≫
      (NatIso.ofComponents (fun Y ↦ (Equiv.ulift.trans shrinkYonedaObjObjEquiv.symm).toIso) ⋯).hom =
    (NatIso.ofComponents (fun Y ↦ (Equiv.ulift.trans shrinkYonedaObjObjEquiv.symm).toIso) ⋯).hom ≫
      shrinkYoneda.{max w' v, v, u}.map g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
F G : J ⥤ K ⥤ C
η : F ⟶ G
⊢ (flipFunctor J K C ⋙ (whiskeringRight K (J ⥤ C) C).obj lim).map η ≫ (limitIsoFlipCompLim G).symm.hom =
    (limitIsoFlipCompLim F).symm.hom ≫ lim.map η

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
Y : Cᵒᵖ
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ (shrinkYoneda.{w, v, u} ⋙ (evaluation Cᵒᵖ (Type w)).obj Y ⋙ uliftFunctor.{v, w}).map f ≫
      (Equiv.ulift.trans (shrinkYonedaObjObjEquiv.trans Equiv.ulift.symm)).toIso.hom =
    (Equiv.ulift.trans (shrinkYonedaObjObjEquiv.trans Equiv.ulift.symm)).toIso.hom ≫
      (coyoneda.obj Y ⋙ uliftFunctor.{w, v}).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : Cᵒᵖ
x✝ : C
⊢ Small.{w, v} ((coyoneda.obj X).obj x✝)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
F G : K ⥤ J ⥤ C
η : F ⟶ G
⊢ ((whiskeringRight K (J ⥤ C) C).obj lim).map η ≫ (limitFlipIsoCompLim G).symm.hom =
    (limitFlipIsoCompLim F).symm.hom ≫ (flipFunctor K J C ⋙ lim).map η

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : Cᵒᵖ
P : C ⥤ Type w
x : P.obj (unop X)
Y Z : C
g : Y ⟶ Z
⊢ ((shrinkCoyoneda.{w, v, u}.obj X).map g ≫
      ↾fun f ↦ (ConcreteCategory.hom (P.map ((equivShrink (unop X ⟶ Z)).symm f))) x) =
    (↾fun f ↦ (ConcreteCategory.hom (P.map ((equivShrink (unop X ⟶ Y)).symm f))) x) ≫ P.map g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
J : Type u_1
inst✝² : Category.{v_1, u_1} J
F : J ⥤ AlgCat R
inst✝¹ : PreservesColimitsOfShape J (forget RingCat)
c : Cocone (F ⋙ forget₂ (AlgCat R) RingCat)
inst✝ : IsFilteredOrEmpty J
hc : IsColimit c
j : J
⊢ ∀ (c_1 : R) (x : ↑(((Functor.const J).obj c.pt).obj j)),
    ((RingCat.Hom.hom (c.ι.app j)).comp (algebraMap R ↑(F.obj j))) c_1 * x =
      x * ((RingCat.Hom.hom (c.ι.app j)).comp (algebraMap R ↑(F.obj j))) c_1

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F G : J ⥤ K ⥤ C
η : F ⟶ G
⊢ colim.map η ≫ (colimitIsoFlipCompColim G).hom =
    (colimitIsoFlipCompColim F).hom ≫ (flipFunctor J K C ⋙ (whiskeringRight K (J ⥤ C) C).obj colim).map η

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
J : Type u_1
inst✝² : Category.{v_1, u_1} J
F : J ⥤ AlgCat R
inst✝¹ : PreservesColimitsOfShape J (forget RingCat)
c : Cocone (F ⋙ forget₂ (AlgCat R) RingCat)
inst✝ : IsFilteredOrEmpty J
hc : IsColimit c
j k : J
⊢ F.obj k ⟶ ((Functor.const J).obj (of R ↑c.pt)).obj k

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F G : K ⥤ J ⥤ C
η : F ⟶ G
⊢ (flipFunctor K J C ⋙ colim).map η ≫ (colimitFlipIsoCompColim G).hom =
    (colimitFlipIsoCompColim F).hom ≫ ((whiskeringRight K (J ⥤ C) C).obj colim).map η

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : Cᵒᵖ
P : C ⥤ Type w
τ : shrinkCoyoneda.{w, v, u}.obj X ⟶ P
⊢ (fun x ↦
        { app := fun Y ↦ ↾fun f ↦ (ConcreteCategory.hom (P.map ((equivShrink (unop X ⟶ Y)).symm f))) x,
          naturality := ⋯ })
      ((fun τ ↦ (ConcreteCategory.hom (τ.app (unop X))) ((equivShrink ((yoneda.obj (unop X)).obj X)) (𝟙 (unop X)))) τ) =
    τ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
J : Type u_1
inst✝² : Category.{v_1, u_1} J
F : J ⥤ AlgCat R
inst✝¹ : PreservesColimitsOfShape J (forget RingCat)
c : Cocone (F ⋙ forget₂ (AlgCat R) RingCat)
inst✝ : IsFilteredOrEmpty J
hc : IsColimit c
j k k' : J
f : k ⟶ k'
⊢ F.map f ≫
      ofHom
        (let __spread.0 := RingCat.Hom.hom (c.ι.app k');
        { toRingHom := __spread.0, commutes' := ⋯ }) =
    ofHom
        (let __spread.0 := RingCat.Hom.hom (c.ι.app k);
        { toRingHom := __spread.0, commutes' := ⋯ }) ≫
      ((Functor.const J).obj (of R ↑c.pt)).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : Cᵒᵖ
P : C ⥤ Type w
x : P.obj (unop X)
⊢ (fun τ ↦ (ConcreteCategory.hom (τ.app (unop X))) ((equivShrink ((yoneda.obj (unop X)).obj X)) (𝟙 (unop X))))
      ((fun x ↦
          { app := fun Y ↦ ↾fun f ↦ (ConcreteCategory.hom (P.map ((equivShrink (unop X ⟶ Y)).symm f))) x,
            naturality := ⋯ })
        x) =
    x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
J : Type u_1
inst✝² : Category.{v_1, u_1} J
F : J ⥤ AlgCat R
inst✝¹ : PreservesColimitsOfShape J (forget RingCat)
c : Cocone (F ⋙ forget₂ (AlgCat R) RingCat)
inst✝ : IsFilteredOrEmpty J
hc : IsColimit c
j k k' : J
f : k ⟶ k'
⊢ F.map f ≫
      ofHom
        (let __spread.0 := RingCat.Hom.hom (c.ι.app k');
        { toRingHom := __spread.0, commutes' := ⋯ }) =
    ofHom
        (let __spread.0 := RingCat.Hom.hom (c.ι.app k);
        { toRingHom := __spread.0, commutes' := ⋯ }) ≫
      ((Functor.const J).obj (of R ↑c.pt)).map f

Tactic:
by
    ext
    exact c.ι.naturality_apply _ _

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X Y : Cᵒᵖ
P : C ⥤ Type w
f : shrinkCoyoneda.{w, v, u}.obj X ⟶ P
g : Y ⟶ X
⊢ (ConcreteCategory.hom (P.map g.unop)) (shrinkCoyonedaEquiv f) =
    (ConcreteCategory.hom (f.app (unop Y))) (shrinkCoyonedaObjObjEquiv.symm g.unop)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ shrinkCoyonedaEquiv (shrinkCoyoneda.{w, v, u}.map f) = shrinkCoyonedaObjObjEquiv.symm f.unop

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : Cᵒᵖ
P Q : C ⥤ Type w
α : shrinkCoyoneda.{w, v, u}.obj X ⟶ P
β : P ⟶ Q
⊢ shrinkCoyonedaEquiv (α ≫ β) = (ConcreteCategory.hom (β.app (unop X))) (shrinkCoyonedaEquiv α)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
J : Type u_1
inst✝² : Category.{v_1, u_1} J
F : J ⥤ AlgCat R
inst✝¹ : PreservesColimitsOfShape J (forget RingCat)
c : Cocone (F ⋙ forget₂ (AlgCat R) RingCat)
inst✝ : IsFilteredOrEmpty J
hc : IsColimit c
j : J
s : Cocone F
⊢ (coconeOfIsFiltered hc j).pt ⟶ s.pt

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X Y : Cᵒᵖ
P : C ⥤ Type w
f : shrinkCoyoneda.{w, v, u}.obj X ⟶ P
g : Y ⟶ X
⊢ (ConcreteCategory.hom (P.map g.unop)) (shrinkCoyonedaEquiv f) =
    shrinkCoyonedaEquiv (shrinkCoyoneda.{w, v, u}.map g ≫ f)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
J : Type u_1
inst✝² : Category.{v_1, u_1} J
F : J ⥤ AlgCat R
inst✝¹ : PreservesColimitsOfShape J (forget RingCat)
c : Cocone (F ⋙ forget₂ (AlgCat R) RingCat)
inst✝ : IsFilteredOrEmpty J
hc : IsColimit c
j : J
s : Cocone F
k : J
⊢ (coconeOfIsFiltered hc j).ι.app k ≫
      ofHom
        (let __spread.0 := RingCat.Hom.hom (hc.desc ((forget₂ (AlgCat R) RingCat).mapCocone s));
        { toRingHom := __spread.0, commutes' := ⋯ }) =
    s.ι.app k

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X Y : C
f : X ⟶ Y
P : C ⥤ Type w
t : P.obj X
⊢ shrinkCoyonedaEquiv (shrinkCoyonedaEquiv.symm ((ConcreteCategory.hom (P.map f)) t)) =
    shrinkCoyonedaEquiv (shrinkCoyoneda.{w, v, u}.map f.op ≫ shrinkCoyonedaEquiv.symm t)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : Cᵒᵖ
P : C ⥤ Type w
s : P.obj (unop X)
Y : Cᵒᵖ
f : Y ⟶ X
⊢ (ConcreteCategory.hom ((shrinkCoyonedaEquiv.symm s).app (unop Y))) (shrinkCoyonedaObjObjEquiv.symm f.unop) =
    (ConcreteCategory.hom (P.map f.unop)) s

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X✝ Y✝ : Cᵒᵖ
f : shrinkCoyoneda.{w, v, u}.obj X✝ ⟶ shrinkCoyoneda.{w, v, u}.obj Y✝
⊢ shrinkCoyoneda.{w, v, u}.map (shrinkCoyonedaObjObjEquiv (shrinkCoyonedaEquiv f)).op = f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
J : Type u_1
inst✝² : Category.{v_1, u_1} J
F : J ⥤ AlgCat R
inst✝¹ : PreservesColimitsOfShape J (forget RingCat)
c : Cocone (F ⋙ forget₂ (AlgCat R) RingCat)
inst✝ : IsFilteredOrEmpty J
hc : IsColimit c
j : J
s : Cocone F
m : (coconeOfIsFiltered hc j).pt ⟶ s.pt
hm : ∀ (j_1 : J), (coconeOfIsFiltered hc j).ι.app j_1 ≫ m = s.ι.app j_1
⊢ m =
    ofHom
      (let __spread.0 := RingCat.Hom.hom (hc.desc ((forget₂ (AlgCat R) RingCat).mapCocone s));
      { toRingHom := __spread.0, commutes' := ⋯ })

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ (shrinkCoyonedaObjObjEquiv (shrinkCoyonedaEquiv (shrinkCoyoneda.{w, v, u}.map f))).op = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : Cᵒᵖ
⊢ ∀ {X_1 Y : C} (f : X_1 ⟶ Y),
    (shrinkCoyoneda.{v, v, u}.obj X).map f ≫ shrinkCoyonedaObjObjEquiv.toIso.hom =
      shrinkCoyonedaObjObjEquiv.toIso.hom ≫ (coyoneda.obj X).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
⊢ ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    shrinkCoyoneda.{v, v, u}.map f ≫ (NatIso.ofComponents (fun Y_1 ↦ shrinkCoyonedaObjObjEquiv.toIso) ⋯).hom =
      (NatIso.ofComponents (fun Y ↦ shrinkCoyonedaObjObjEquiv.toIso) ⋯).hom ≫ coyoneda.map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : LocallySmall.{max w w', v, u} C
X✝ Y✝ : Cᵒᵖᵒᵖ
x✝ : X✝ ⟶ Y✝
⊢ (shrinkCoyoneda.{w, v, u} ⋙ (Functor.whiskeringRight Cᵒᵖ (Type w) (Type (max w w'))).obj uliftFunctor.{w', w}).map
        x✝ ≫
      (FunctorToTypes.shrinkCompUliftFunctorIso (coyoneda.obj Y✝)).hom =
    (FunctorToTypes.shrinkCompUliftFunctorIso (coyoneda.obj X✝)).hom ≫ shrinkCoyoneda.{max w w', v, u}.map x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : Cᵒᵖ
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ (uliftCoyoneda.{w', v, u}.obj X).map f ≫ (Equiv.ulift.trans shrinkCoyonedaObjObjEquiv.symm).toIso.hom =
    (Equiv.ulift.trans shrinkCoyonedaObjObjEquiv.symm).toIso.hom ≫ (shrinkCoyoneda.{max w' v, v, u}.obj X).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X✝ Y✝ : Cᵒᵖ
g : X✝ ⟶ Y✝
⊢ uliftCoyoneda.{w', v, u}.map g ≫
      (NatIso.ofComponents (fun Y ↦ (Equiv.ulift.trans shrinkCoyonedaObjObjEquiv.symm).toIso) ⋯).hom =
    (NatIso.ofComponents (fun Y ↦ (Equiv.ulift.trans shrinkCoyonedaObjObjEquiv.symm).toIso) ⋯).hom ≫
      shrinkCoyoneda.{max w' v, v, u}.map g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
Y : C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ (shrinkCoyoneda.{w, v, u} ⋙ (evaluation C (Type w)).obj Y ⋙ uliftFunctor.{v, w}).map f ≫
      (Equiv.ulift.trans (shrinkCoyonedaObjObjEquiv.trans Equiv.ulift.symm)).toIso.hom =
    (Equiv.ulift.trans (shrinkCoyonedaObjObjEquiv.trans Equiv.ulift.symm)).toIso.hom ≫
      (yoneda.obj Y ⋙ uliftFunctor.{w, v}).map f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ MonCat
a b : (j : J) → ↑(F.obj j)
ah : a ∈ (F ⋙ forget MonCat).sections
bh : b ∈ (F ⋙ forget MonCat).sections
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom ((F ⋙ forget MonCat).map f)) ((a * b) j) = (a * b) j'

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ MonCat
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom ((F ⋙ forget MonCat).map f)) (1 j) = 1 j'

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
j : J
⊢ (ConcreteCategory.hom ((Types.Small.limitCone (F ⋙ forget MonCat)).π.app j)) 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
j : J
x✝¹ x✝ : (Types.Small.limitCone (F ⋙ forget MonCat)).pt
⊢ (ConcreteCategory.hom ((Types.Small.limitCone (F ⋙ forget MonCat)).π.app j)) (x✝¹ * x✝) =
    (ConcreteCategory.hom ((Types.Small.limitCone (F ⋙ forget MonCat)).π.app j)) x✝¹ *
      (ConcreteCategory.hom ((Types.Small.limitCone (F ⋙ forget MonCat)).π.app j)) x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
⊢ IsLimit (limitCone F)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
c : Cone (F ⋙ forget MonCat)
t : IsLimit c
this : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
s✝ : Cone F
⊢ (ConcreteCategory.hom ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s✝))) 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
⊢ CreatesLimit F (forget MonCat)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ CommMonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget CommMonCat).sections
c' : Cone (F ⋙ forget₂ CommMonCat MonCat)
t : IsLimit c'
⊢ (forget₂ CommMonCat MonCat).mapCone
      { pt := of (Types.Small.limitCone (F ⋙ forget CommMonCat)).pt,
        π := { app := fun j ↦ ofHom (limitπMonoidHom (F ⋙ forget₂ CommMonCat MonCat) j), naturality := ⋯ } } ≅
    c'

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ CommMonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget CommMonCat).sections
⊢ CreatesLimit F (forget CommMonCat)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : Category.{t, v} J
F : J ⥤ ModuleCat R
r : R
s : (j : J) → ↑(F.obj j)
sh : s ∈ (F ⋙ forget (ModuleCat R)).sections
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom ((F ⋙ forget (ModuleCat R)).map f)) ((r • s) j) = (r • s) j'

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ ModuleCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (ModuleCat R)).sections
j : J
x✝¹ x✝ : (Types.Small.limitCone (F ⋙ forget (ModuleCat R))).pt
⊢ (ConcreteCategory.hom ((Types.Small.limitCone (F ⋙ forget (ModuleCat R))).π.app j)) (x✝¹ + x✝) =
    (ConcreteCategory.hom ((Types.Small.limitCone (F ⋙ forget (ModuleCat R))).π.app j)) x✝¹ +
      (ConcreteCategory.hom ((Types.Small.limitCone (F ⋙ forget (ModuleCat R))).π.app j)) x✝

Tactic:
by

Goal state after: