mathlib-initiative/mathlib-tactics huggingface dataset:
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✝
⊢ (shrinkYoneda.{v, v, u}.obj X).map f✝ ≫ shrinkYonedaObjObjEquiv.toIso.hom =
    shrinkYonedaObjObjEquiv.toIso.hom ≫ (yoneda.obj X).map f✝

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
X✝ Y✝ : Cᵒᵖ
f✝ : X✝ ⟶ Y✝
⊢ (shrinkYoneda.{v, v, u}.obj X).map f✝ ≫ shrinkYonedaObjObjEquiv.toIso.hom =
    shrinkYonedaObjObjEquiv.toIso.hom ≫ (yoneda.obj X).map f✝
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✝
x✝ : (shrinkYoneda.{v, v, u}.obj X).obj X✝
⊢ (ConcreteCategory.hom ((shrinkYoneda.{v, v, u}.obj X).map f✝ ≫ shrinkYonedaObjObjEquiv.toIso.hom)).toFun x✝ =
    (ConcreteCategory.hom (shrinkYonedaObjObjEquiv.toIso.hom ≫ (yoneda.obj X).map f✝)).toFun x✝

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
X✝ Y✝ : Cᵒᵖ
f✝ : X✝ ⟶ Y✝
x✝ : (shrinkYoneda.{v, v, u}.obj X).obj X✝
⊢ (ConcreteCategory.hom ((shrinkYoneda.{v, v, u}.obj X).map f✝ ≫ shrinkYonedaObjObjEquiv.toIso.hom)).toFun x✝ =
    (ConcreteCategory.hom (shrinkYonedaObjObjEquiv.toIso.hom ≫ (yoneda.obj X).map f✝)).toFun x✝
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 ↦ shrinkYonedaObjObjEquiv.toIso) ⋯).hom =
    (NatIso.ofComponents (fun Y ↦ shrinkYonedaObjObjEquiv.toIso) ⋯).hom ≫ yoneda.map f✝

Tactic:
;

Goal state after:
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 ↦ shrinkYonedaObjObjEquiv.toIso) ⋯).hom =
    (NatIso.ofComponents (fun Y ↦ shrinkYonedaObjObjEquiv.toIso) ⋯).hom ≫ yoneda.map f✝
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✝
x✝¹ : Cᵒᵖ
x✝ : (shrinkYoneda.{v, v, u}.obj X✝).obj x✝¹
⊢ (ConcreteCategory.hom
          ((shrinkYoneda.{v, v, u}.map f✝ ≫ (NatIso.ofComponents (fun Y ↦ shrinkYonedaObjObjEquiv.toIso) ⋯).hom).app
            x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom
          (((NatIso.ofComponents (fun Y ↦ shrinkYonedaObjObjEquiv.toIso) ⋯).hom ≫ yoneda.map f✝).app x✝¹)).toFun
      x✝

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
x✝¹ : Cᵒᵖ
x✝ : (shrinkYoneda.{v, v, u}.obj X✝).obj x✝¹
⊢ (ConcreteCategory.hom
          ((shrinkYoneda.{v, v, u}.map f✝ ≫ (NatIso.ofComponents (fun Y ↦ shrinkYonedaObjObjEquiv.toIso) ⋯).hom).app
            x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom
          (((NatIso.ofComponents (fun Y ↦ shrinkYonedaObjObjEquiv.toIso) ⋯).hom ≫ yoneda.map f✝).app x✝¹)).toFun
      x✝
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✝
x✝¹ : Cᵒᵖ
x✝ :
  ((shrinkYoneda.{w, v, u} ⋙ (Functor.whiskeringRight Cᵒᵖ (Type w) (Type (max w w'))).obj uliftFunctor.{w', w}).obj
        X✝).obj
    x✝¹
⊢ (ConcreteCategory.hom
          (((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).app
            x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom
          (((FunctorToTypes.shrinkCompUliftFunctorIso (yoneda.obj X✝)).hom ≫ shrinkYoneda.{max w w', v, u}.map x✝²).app
            x✝¹)).toFun
      x✝

Tactic:
;

Goal state after:
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✝
x✝¹ : Cᵒᵖ
x✝ :
  ((shrinkYoneda.{w, v, u} ⋙ (Functor.whiskeringRight Cᵒᵖ (Type w) (Type (max w w'))).obj uliftFunctor.{w', w}).obj
        X✝).obj
    x✝¹
⊢ (ConcreteCategory.hom
          (((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).app
            x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom
          (((FunctorToTypes.shrinkCompUliftFunctorIso (yoneda.obj X✝)).hom ≫ shrinkYoneda.{max w w', v, u}.map x✝²).app
            x✝¹)).toFun
      x✝
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} (unop X ⟶ x✝)

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : Cᵒᵖ
x✝ : C
⊢ Small.{w, v} (unop X ⟶ x✝)
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:
intro r

Goal state after:
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
r : R
⊢ ∀ (x : ↑(((Functor.const J).obj c.pt).obj j)),
    ((RingCat.Hom.hom (c.ι.app j)).comp (algebraMap R ↑(F.obj j))) r * x =
      x * ((RingCat.Hom.hom (c.ι.app j)).comp (algebraMap R ↑(F.obj j))) r
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
x✝ : (shrinkCoyoneda.{w, v, u}.obj X).obj Y
⊢ (ConcreteCategory.hom
          ((shrinkCoyoneda.{w, v, u}.obj X).map g ≫
            ↾fun f ↦ (ConcreteCategory.hom (P.map ((equivShrink (unop X ⟶ Z)).symm f))) x)).toFun
      x✝ =
    (ConcreteCategory.hom
          ((↾fun f ↦ (ConcreteCategory.hom (P.map ((equivShrink (unop X ⟶ Y)).symm f))) x) ≫ P.map g)).toFun
      x✝

Tactic:
;

Goal state after:
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
x✝ : (shrinkCoyoneda.{w, v, u}.obj X).obj Y
⊢ (ConcreteCategory.hom
          ((shrinkCoyoneda.{w, v, u}.obj X).map g ≫
            ↾fun f ↦ (ConcreteCategory.hom (P.map ((equivShrink (unop X ⟶ Z)).symm f))) x)).toFun
      x✝ =
    (ConcreteCategory.hom
          ((↾fun f ↦ (ConcreteCategory.hom (P.map ((equivShrink (unop X ⟶ Y)).symm f))) x) ≫ P.map g)).toFun
      x✝
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✝
⊢ (shrinkCoyoneda.{v, v, u}.obj X).map f✝ ≫ shrinkCoyonedaObjObjEquiv.toIso.hom =
    shrinkCoyonedaObjObjEquiv.toIso.hom ≫ (coyoneda.obj X).map f✝

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : Cᵒᵖ
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ (shrinkCoyoneda.{v, v, u}.obj X).map f✝ ≫ shrinkCoyonedaObjObjEquiv.toIso.hom =
    shrinkCoyonedaObjObjEquiv.toIso.hom ≫ (coyoneda.obj X).map f✝
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✝
x✝ : (shrinkCoyoneda.{v, v, u}.obj X).obj X✝
⊢ (ConcreteCategory.hom ((shrinkCoyoneda.{v, v, u}.obj X).map f✝ ≫ shrinkCoyonedaObjObjEquiv.toIso.hom)).toFun x✝ =
    (ConcreteCategory.hom (shrinkCoyonedaObjObjEquiv.toIso.hom ≫ (coyoneda.obj X).map f✝)).toFun x✝

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : Cᵒᵖ
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
x✝ : (shrinkCoyoneda.{v, v, u}.obj X).obj X✝
⊢ (ConcreteCategory.hom ((shrinkCoyoneda.{v, v, u}.obj X).map f✝ ≫ shrinkCoyonedaObjObjEquiv.toIso.hom)).toFun x✝ =
    (ConcreteCategory.hom (shrinkCoyonedaObjObjEquiv.toIso.hom ≫ (coyoneda.obj X).map f✝)).toFun x✝
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 ↦ shrinkCoyonedaObjObjEquiv.toIso) ⋯).hom =
    (NatIso.ofComponents (fun Y ↦ shrinkCoyonedaObjObjEquiv.toIso) ⋯).hom ≫ coyoneda.map f✝

Tactic:
;

Goal state after:
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 ↦ shrinkCoyonedaObjObjEquiv.toIso) ⋯).hom =
    (NatIso.ofComponents (fun Y ↦ shrinkCoyonedaObjObjEquiv.toIso) ⋯).hom ≫ coyoneda.map f✝
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✝
x✝¹ : C
x✝ : (shrinkCoyoneda.{v, v, u}.obj X✝).obj x✝¹
⊢ (ConcreteCategory.hom
          ((shrinkCoyoneda.{v, v, u}.map f✝ ≫ (NatIso.ofComponents (fun Y ↦ shrinkCoyonedaObjObjEquiv.toIso) ⋯).hom).app
            x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom
          (((NatIso.ofComponents (fun Y ↦ shrinkCoyonedaObjObjEquiv.toIso) ⋯).hom ≫ coyoneda.map f✝).app x✝¹)).toFun
      x✝

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X✝ Y✝ : Cᵒᵖ
f✝ : X✝ ⟶ Y✝
x✝¹ : C
x✝ : (shrinkCoyoneda.{v, v, u}.obj X✝).obj x✝¹
⊢ (ConcreteCategory.hom
          ((shrinkCoyoneda.{v, v, u}.map f✝ ≫ (NatIso.ofComponents (fun Y ↦ shrinkCoyonedaObjObjEquiv.toIso) ⋯).hom).app
            x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom
          (((NatIso.ofComponents (fun Y ↦ shrinkCoyonedaObjObjEquiv.toIso) ⋯).hom ≫ coyoneda.map f✝).app x✝¹)).toFun
      x✝
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✝
x✝¹ : Cᵒᵖ
x✝ :
  ((shrinkCoyoneda.{w, v, u} ⋙ (Functor.whiskeringRight Cᵒᵖ (Type w) (Type (max w w'))).obj uliftFunctor.{w', w}).obj
        X✝).obj
    x✝¹
⊢ (ConcreteCategory.hom
          (((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).app
            x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom
          (((FunctorToTypes.shrinkCompUliftFunctorIso (coyoneda.obj X✝)).hom ≫
                shrinkCoyoneda.{max w w', v, u}.map x✝²).app
            x✝¹)).toFun
      x✝

Tactic:
;

Goal state after:
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✝
x✝¹ : Cᵒᵖ
x✝ :
  ((shrinkCoyoneda.{w, v, u} ⋙ (Functor.whiskeringRight Cᵒᵖ (Type w) (Type (max w w'))).obj uliftFunctor.{w', w}).obj
        X✝).obj
    x✝¹
⊢ (ConcreteCategory.hom
          (((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).app
            x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom
          (((FunctorToTypes.shrinkCompUliftFunctorIso (coyoneda.obj X✝)).hom ≫
                shrinkCoyoneda.{max w w', v, u}.map x✝²).app
            x✝¹)).toFun
      x✝
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
⊢ ↑1 j = 1

Tactic:
;

Goal state after:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
j : J
⊢ ↑1 j = 1
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
⊢ ↑((equivShrink ↑(F ⋙ forget MonCat).sections).symm x✝¹ * (equivShrink ↑(F ⋙ forget MonCat).sections).symm x✝) j =
    ↑((equivShrink ↑(F ⋙ forget MonCat).sections).symm x✝¹) j * ↑((equivShrink ↑(F ⋙ forget MonCat).sections).symm x✝) j

Tactic:
;

Goal state after:
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
⊢ ↑((equivShrink ↑(F ⋙ forget MonCat).sections).symm x✝¹ * (equivShrink ↑(F ⋙ forget MonCat).sections).symm x✝) j =
    ↑((equivShrink ↑(F ⋙ forget MonCat).sections).symm x✝¹) j * ↑((equivShrink ↑(F ⋙ forget MonCat).sections).symm x✝) j
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
⊢ (equivShrink ↑(F ⋙ forget MonCat).sections) ⟨fun j ↦ 1, ⋯⟩ = 1

Tactic:
;

Goal state after:
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
⊢ (equivShrink ↑(F ⋙ forget MonCat).sections) ⟨fun j ↦ 1, ⋯⟩ = 1
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
⊢ ↑((equivShrink ↑(F ⋙ forget (ModuleCat R)).sections).symm x✝¹ +
          (equivShrink ↑(F ⋙ forget (ModuleCat R)).sections).symm x✝)
      j =
    ↑((equivShrink ↑(F ⋙ forget (ModuleCat R)).sections).symm x✝¹) j +
      ↑((equivShrink ↑(F ⋙ forget (ModuleCat R)).sections).symm x✝) j

Tactic:
;

Goal state after:
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
⊢ ↑((equivShrink ↑(F ⋙ forget (ModuleCat R)).sections).symm x✝¹ +
          (equivShrink ↑(F ⋙ forget (ModuleCat R)).sections).symm x✝)
      j =
    ↑((equivShrink ↑(F ⋙ forget (ModuleCat R)).sections).symm x✝¹) j +
      ↑((equivShrink ↑(F ⋙ forget (ModuleCat R)).sections).symm x✝) j
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✝¹ : R
x✝ : (Types.Small.limitCone (F ⋙ forget (ModuleCat R))).pt
⊢ ↑(x✝¹ • (equivShrink ↑(F ⋙ forget (ModuleCat R)).sections).symm x✝) j =
    x✝¹ • ↑((equivShrink ↑(F ⋙ forget (ModuleCat R)).sections).symm x✝) j

Tactic:
;

Goal state after:
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✝¹ : R
x✝ : (Types.Small.limitCone (F ⋙ forget (ModuleCat R))).pt
⊢ ↑(x✝¹ • (equivShrink ↑(F ⋙ forget (ModuleCat R)).sections).symm x✝) j =
    x✝¹ • ↑((equivShrink ↑(F ⋙ forget (ModuleCat R)).sections).symm x✝) j
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: case refine_2
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
s : Cone F
⊢ ∀ (m : R) (x : ↑s.1),
    {
            toFun :=
              ⇑(ConcreteCategory.hom
                  ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift ((forget (ModuleCat R)).mapCone s))),
            map_add' := ⋯ }.toFun
        (m • x) =
      (RingHom.id R) m •
        {
              toFun :=
                ⇑(ConcreteCategory.hom
                    ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift
                      ((forget (ModuleCat R)).mapCone s))),
              map_add' := ⋯ }.toFun
          x

Tactic:
intro r

Goal state after:
case refine_2
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
s : Cone F
r : R
⊢ ∀ (x : ↑s.1),
    {
            toFun :=
              ⇑(ConcreteCategory.hom
                  ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift ((forget (ModuleCat R)).mapCone s))),
            map_add' := ⋯ }.toFun
        (r • x) =
      (RingHom.id R) r •
        {
              toFun :=
                ⇑(ConcreteCategory.hom
                    ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift
                      ((forget (ModuleCat R)).mapCone s))),
              map_add' := ⋯ }.toFun
          x
Module: Mathlib.Algebra.Category.AlgCat.Limits

Goal state before:
pp: case refine_5
R : Type u
inst✝² : CommRing R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ AlgCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (AlgCat R)).sections
s : Cone F
⊢ ∀ (r : R),
    EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) ((algebraMap R ↑s.1) r), ⋯⟩ =
      (algebraMap R (Types.Small.limitCone (F ⋙ forget (AlgCat R))).pt) r

Tactic:
intro r

Goal state after:
case refine_5
R : Type u
inst✝² : CommRing R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ AlgCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (AlgCat R)).sections
s : Cone F
r : R
⊢ EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
      ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) ((algebraMap R ↑s.1) r), ⋯⟩ =
    (algebraMap R (Types.Small.limitCone (F ⋙ forget (AlgCat R))).pt) r
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategoryStruct C
id_tensorHom_id : ∀ (X₁ X₂ : C), 𝟙 X₁ ⊗ₘ 𝟙 X₂ = 𝟙 (X₁ ⊗ X₂)
id_tensorHom : ∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂), 𝟙 X ⊗ₘ f = X ◁ f
tensorHom_id : ∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C), f ⊗ₘ 𝟙 Y = f ▷ Y
tensorHom_comp_tensorHom :
  ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂
associator_naturality :
  ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
    ((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃)
leftUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), (𝟙 (𝟙_ C) ⊗ₘ f) ≫ (λ_ Y).hom = (λ_ X).hom ≫ f
rightUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), (f ⊗ₘ 𝟙 (𝟙_ C)) ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f
pentagon :
  ∀ (W X Y Z : 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
triangle : ∀ (X Y : C), (α_ X (𝟙_ C) Y).hom ≫ (𝟙 X ⊗ₘ (λ_ Y).hom) = (ρ_ X).hom ⊗ₘ 𝟙 Y
X₁✝ Y₁✝ X₂✝ Y₂✝ : C
f✝ : X₁✝ ⟶ Y₁✝
g✝ : X₂✝ ⟶ Y₂✝
⊢ f✝ ⊗ₘ g✝ = f✝ ▷ X₂✝ ≫ Y₁✝ ◁ g✝

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategoryStruct C
id_tensorHom_id : ∀ (X₁ X₂ : C), 𝟙 X₁ ⊗ₘ 𝟙 X₂ = 𝟙 (X₁ ⊗ X₂)
id_tensorHom : ∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂), 𝟙 X ⊗ₘ f = X ◁ f
tensorHom_id : ∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C), f ⊗ₘ 𝟙 Y = f ▷ Y
tensorHom_comp_tensorHom :
  ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂
associator_naturality :
  ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
    ((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃)
leftUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), (𝟙 (𝟙_ C) ⊗ₘ f) ≫ (λ_ Y).hom = (λ_ X).hom ≫ f
rightUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), (f ⊗ₘ 𝟙 (𝟙_ C)) ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f
pentagon :
  ∀ (W X Y Z : 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
triangle : ∀ (X Y : C), (α_ X (𝟙_ C) Y).hom ≫ (𝟙 X ⊗ₘ (λ_ Y).hom) = (ρ_ X).hom ⊗ₘ 𝟙 Y
X₁✝ Y₁✝ X₂✝ Y₂✝ : C
f✝ : X₁✝ ⟶ Y₁✝
g✝ : X₂✝ ⟶ Y₂✝
⊢ f✝ ⊗ₘ g✝ = f✝ ▷ X₂✝ ≫ Y₁✝ ◁ g✝
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
G H : AddCommGrpCat
f : G ⟶ H
x : ↑(of ↥(Hom.hom f).ker)
⊢ (Hom.hom (ofHom (Hom.hom f).ker.subtype ≫ f)) x = (Hom.hom 0) x

Tactic:
;

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
G H : AddCommGrpCat
f : G ⟶ H
x : ↑(of ↥(Hom.hom f).ker)
⊢ (Hom.hom (ofHom (Hom.hom f).ker.subtype ≫ f)) x = (Hom.hom 0) x
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
x✝ : ↑(kernel f)
⊢ (Hom.hom ((kernelIsoKer f).hom ≫ ofHom (Hom.hom f).ker.subtype)) x✝ = (Hom.hom (kernel.ι f)) x✝

Tactic:
;

Goal state after:
G H : AddCommGrpCat
f : G ⟶ H
x✝ : ↑(kernel f)
⊢ (Hom.hom ((kernelIsoKer f).hom ≫ ofHom (Hom.hom f).ker.subtype)) x✝ = (Hom.hom (kernel.ι f)) x✝
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategoryStruct C
id_tensorHom_id : ∀ (X₁ X₂ : C), 𝟙 X₁ ⊗ₘ 𝟙 X₂ = 𝟙 (X₁ ⊗ X₂)
id_tensorHom : ∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂), 𝟙 X ⊗ₘ f = X ◁ f
tensorHom_id : ∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C), f ⊗ₘ 𝟙 Y = f ▷ Y
tensorHom_comp_tensorHom :
  ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂
associator_naturality :
  ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
    ((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃)
leftUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), (𝟙 (𝟙_ C) ⊗ₘ f) ≫ (λ_ Y).hom = (λ_ X).hom ≫ f
rightUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), (f ⊗ₘ 𝟙 (𝟙_ C)) ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f
pentagon :
  ∀ (W X Y Z : 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
triangle : ∀ (X Y : C), (α_ X (𝟙_ C) Y).hom ≫ (𝟙 X ⊗ₘ (λ_ Y).hom) = (ρ_ X).hom ⊗ₘ 𝟙 Y
X✝ Y✝ : C
⊢ X✝ ◁ 𝟙 Y✝ = 𝟙 (X✝ ⊗ Y✝)

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategoryStruct C
id_tensorHom_id : ∀ (X₁ X₂ : C), 𝟙 X₁ ⊗ₘ 𝟙 X₂ = 𝟙 (X₁ ⊗ X₂)
id_tensorHom : ∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂), 𝟙 X ⊗ₘ f = X ◁ f
tensorHom_id : ∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C), f ⊗ₘ 𝟙 Y = f ▷ Y
tensorHom_comp_tensorHom :
  ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂
associator_naturality :
  ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
    ((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃)
leftUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), (𝟙 (𝟙_ C) ⊗ₘ f) ≫ (λ_ Y).hom = (λ_ X).hom ≫ f
rightUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), (f ⊗ₘ 𝟙 (𝟙_ C)) ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f
pentagon :
  ∀ (W X Y Z : 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
triangle : ∀ (X Y : C), (α_ X (𝟙_ C) Y).hom ≫ (𝟙 X ⊗ₘ (λ_ Y).hom) = (ρ_ X).hom ⊗ₘ 𝟙 Y
X✝ Y✝ : C
⊢ X✝ ◁ 𝟙 Y✝ = 𝟙 (X✝ ⊗ Y✝)