mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
inst✝ : Fintype ι
c : R
z : M₂
⊢ MultilinearMap.mkPiRing R ι (c • z) = (RingHom.id R) c • MultilinearMap.mkPiRing R ι z

Tactic:
ext

Goal state after:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
inst✝ : Fintype ι
c : R
z : M₂
⊢ ((MultilinearMap.mkPiRing R ι (c • z)) fun x ↦ 1) = ((RingHom.id R) c • MultilinearMap.mkPiRing R ι z) fun x ↦ 1
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : Cᵒᵖ
s : Cocone (coyoneda.obj X)
Y : C
f : (coyoneda.obj X).obj Y
⊢ (hom ((colimitCocone X).ι.app Y ≫ ↾fun x ↦ (hom (s.ι.app (unop X))) (𝟙 (unop X)))).toFun f = (hom (s.ι.app Y)).toFun f

Tactic:
simpa using congr_hom (s.w f).symm (𝟙 (unop X))

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : Category.{t, w} J
F : J ⥤ C
c : Cocone F
x✝ : (X : C) → IsLimit ((yoneda.obj X).mapCone c.op)
⊢ (fun h x ↦ isLimitOfPreserves (yoneda.obj x) h.op) ((fun h ↦ (yonedaJointlyReflectsLimits F.op c.op h).unop) x✝) = x✝

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : Category.{t, w} J
F : J ⥤ C
c : Cocone F
x✝¹ : (X : C) → IsLimit ((yoneda.obj X).mapCone c.op)
x✝ : C
⊢ (fun h x ↦ isLimitOfPreserves (yoneda.obj x) h.op) ((fun h ↦ (yonedaJointlyReflectsLimits F.op c.op h).unop) x✝¹) x✝ =
    x✝¹ x✝
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : Category.{t, w} J
F : J ⥤ C
c : Cone F
x✝ : (X : Cᵒᵖ) → IsLimit ((coyoneda.obj X).mapCone c)
⊢ (fun h x ↦ isLimitOfPreserves (coyoneda.obj x) h) ((fun h ↦ coyonedaJointlyReflectsLimits F c h) x✝) = x✝

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : Category.{t, w} J
F : J ⥤ C
c : Cone F
x✝¹ : (X : Cᵒᵖ) → IsLimit ((coyoneda.obj X).mapCone c)
x✝ : Cᵒᵖ
⊢ (fun h x ↦ isLimitOfPreserves (coyoneda.obj x) h) ((fun h ↦ coyonedaJointlyReflectsLimits F c h) x✝¹) x✝ = x✝¹ x✝
Module: Mathlib.Algebra.Category.Grp.ForgetCorepresentable

Goal state before:
pp: G : Type u
inst✝ : AddCommGroup G
x y : G
⊢ (uliftZMultiplesHom G) (x + y) = (uliftZMultiplesHom G) x + (uliftZMultiplesHom G) y

Tactic:
ext

Goal state after:
G : Type u
inst✝ : AddCommGroup G
x y : G
x✝ : ULift.{u, 0} ℤ
⊢ ((uliftZMultiplesHom G) (x + y)) x✝ = ((uliftZMultiplesHom G) x + (uliftZMultiplesHom G) y) x✝
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✝ : HasLimitsOfShape J C
i j : K
F : J ⥤ K ⥤ C
f : i ⟶ j
⊢ (limit F).map f ≫ (limitObjIsoLimitCompEvaluation F j).hom =
    (limitObjIsoLimitCompEvaluation F i).hom ≫ limMap (F.whiskerLeft ((evaluation K C).map f))

Tactic:
ext

Goal state after:
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✝ : HasLimitsOfShape J C
i j : K
F : J ⥤ K ⥤ C
f : i ⟶ j
j✝ : J
⊢ ((limit F).map f ≫ (limitObjIsoLimitCompEvaluation F j).hom) ≫ limit.π (F ⋙ (evaluation K C).obj j) j✝ =
    ((limitObjIsoLimitCompEvaluation F i).hom ≫ limMap (F.whiskerLeft ((evaluation K C).map f))) ≫
      limit.π (F ⋙ (evaluation K C).obj j) j✝
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 (op X)
Y Z : Cᵒᵖ
g : Y ⟶ Z
⊢ ((shrinkYoneda.{w, v, u}.obj X).map g ≫
      ↾fun f ↦ (ConcreteCategory.hom (P.map (Quiver.Hom.op ((equivShrink ((yoneda.obj X).obj Z)).symm f)))) x) =
    (↾fun f ↦ (ConcreteCategory.hom (P.map (Quiver.Hom.op ((equivShrink ((yoneda.obj X).obj Y)).symm f)))) x) ≫ P.map g

Tactic:
ext

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 (op X)
Y Z : Cᵒᵖ
g : Y ⟶ Z
x✝ : (shrinkYoneda.{w, v, u}.obj X).obj Y
⊢ (ConcreteCategory.hom
          ((shrinkYoneda.{w, v, u}.obj X).map g ≫
            ↾fun f ↦
              (ConcreteCategory.hom (P.map (Quiver.Hom.op ((equivShrink ((yoneda.obj X).obj Z)).symm f)))) x)).toFun
      x✝ =
    (ConcreteCategory.hom
          ((↾fun f ↦ (ConcreteCategory.hom (P.map (Quiver.Hom.op ((equivShrink ((yoneda.obj X).obj Y)).symm f)))) x) ≫
            P.map g)).toFun
      x✝
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:
ext

Goal state after:
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
j✝ : J
⊢ colimit.ι (F ⋙ (evaluation K C).obj i) j✝ ≫ (colimitObjIsoColimitCompEvaluation F i).inv ≫ (colimit F).map f =
    colimit.ι (F ⋙ (evaluation K C).obj i) j✝ ≫
      colimMap (F.whiskerLeft ((evaluation K C).map f)) ≫ (colimitObjIsoColimitCompEvaluation F j).inv
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:
ext

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:
ext

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✝
⊢ (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:
ext

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✝ 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:
ext

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✝ : (uliftYoneda.{w', v, u}.obj X).obj X✝
⊢ (ConcreteCategory.hom
          ((uliftYoneda.{w', v, u}.obj X).map f ≫ (Equiv.ulift.trans shrinkYonedaObjObjEquiv.symm).toIso.hom)).toFun
      x✝ =
    (ConcreteCategory.hom
          ((Equiv.ulift.trans shrinkYonedaObjObjEquiv.symm).toIso.hom ≫
            (shrinkYoneda.{max w' v, v, u}.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
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:
ext

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

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.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:
ext

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 k k' : J
f : k ⟶ k'
x✝ : ↑(F.obj k)
⊢ (Hom.hom
        (F.map f ≫
          ofHom
            (let __spread.0 := RingCat.Hom.hom (c.ι.app k');
            { toRingHom := __spread.0, commutes' := ⋯ })))
      x✝ =
    (Hom.hom
        (ofHom
            (let __spread.0 := RingCat.Hom.hom (c.ι.app k);
            { toRingHom := __spread.0, commutes' := ⋯ }) ≫
          ((Functor.const J).obj (of R ↑c.pt)).map f))
      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
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:
ext

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
s : Cocone F
k : J
x✝ : ↑(F.obj k)
⊢ (Hom.hom
        ((coconeOfIsFiltered hc j).ι.app k ≫
          ofHom
            (let __spread.0 := RingCat.Hom.hom (hc.desc ((forget₂ (AlgCat R) RingCat).mapCocone s));
            { toRingHom := __spread.0, commutes' := ⋯ })))
      x✝ =
    (Hom.hom (s.ι.app k)) 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
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:
ext

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
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
x✝ : ↑(coconeOfIsFiltered hc j).pt
⊢ (Hom.hom m) x✝ =
    (Hom.hom
        (ofHom
          (let __spread.0 := RingCat.Hom.hom (hc.desc ((forget₂ (AlgCat R) RingCat).mapCocone s));
          { toRingHom := __spread.0, commutes' := ⋯ })))
      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
s : Cocone F
m : (coconeOfIsFiltered hc j✝).pt ⟶ s.pt
hm : ∀ (j : J), (coconeOfIsFiltered hc j✝).ι.app j ≫ m = s.ι.app j
x✝ : ↑(coconeOfIsFiltered hc j✝).pt
j : J
⊢ c.ι.app j ≫ (forget₂ (AlgCat R) RingCat).map m = ((forget₂ (AlgCat R) RingCat).mapCocone s).ι.app j

Tactic:
ext

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
s : Cocone F
m : (coconeOfIsFiltered hc j✝).pt ⟶ s.pt
hm : ∀ (j : J), (coconeOfIsFiltered hc j✝).ι.app j ≫ m = s.ι.app j
x✝¹ : ↑(coconeOfIsFiltered hc j✝).pt
j : J
x✝ : ↑((F ⋙ forget₂ (AlgCat R) RingCat).obj j)
⊢ (RingCat.Hom.hom (c.ι.app j ≫ (forget₂ (AlgCat R) RingCat).map m)) x✝ =
    (RingCat.Hom.hom (((forget₂ (AlgCat R) RingCat).mapCocone s).ι.app j)) 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:
ext

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:
ext

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✝
⊢ (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:
ext

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.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:
ext

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✝ : (uliftCoyoneda.{w', v, u}.obj X).obj X✝
⊢ (ConcreteCategory.hom
          ((uliftCoyoneda.{w', v, u}.obj X).map f ≫ (Equiv.ulift.trans shrinkCoyonedaObjObjEquiv.symm).toIso.hom)).toFun
      x✝ =
    (ConcreteCategory.hom
          ((Equiv.ulift.trans shrinkCoyonedaObjObjEquiv.symm).toIso.hom ≫
            (shrinkCoyoneda.{max w' v, v, u}.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 : 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:
ext
      exact (shrinkCoyoneda_obj_map_shrinkCoyonedaObjObjEquiv_symm _ _).symm

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:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X✝ Y✝ : Cᵒᵖ
g : X✝ ⟶ Y✝
x✝¹ : C
x✝ : (uliftCoyoneda.{w', v, u}.obj X✝).obj x✝¹
⊢ (ConcreteCategory.hom
          ((uliftCoyoneda.{w', v, u}.map g ≫
                (NatIso.ofComponents (fun Y ↦ (Equiv.ulift.trans shrinkCoyonedaObjObjEquiv.symm).toIso) ⋯).hom).app
            x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom
          (((NatIso.ofComponents (fun Y ↦ (Equiv.ulift.trans shrinkCoyonedaObjObjEquiv.symm).toIso) ⋯).hom ≫
                shrinkCoyoneda.{max w' v, v, u}.map g).app
            x✝¹)).toFun
      x✝
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: case refine_1
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
x✝ : J
⊢ ((forget MonCat).mapCone
            { pt := of (Types.Small.limitCone (F ⋙ forget MonCat)).pt,
              π := { app := fun j ↦ ofHom (limitπMonoidHom F j), naturality := ⋯ } }).π.app
      x✝ =
    ((Types.isLimitEquivSections t).trans (equivShrink ↑(F ⋙ forget MonCat).sections)).symm.toIso.hom ≫ c.π.app x✝

Tactic:
ext

Goal state after:
case refine_1
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
x✝¹ : J
x✝ :
  ((Functor.const J).obj
        ((forget MonCat).mapCone
            { pt := of (Types.Small.limitCone (F ⋙ forget MonCat)).pt,
              π := { app := fun j ↦ ofHom (limitπMonoidHom F j), naturality := ⋯ } }).pt).obj
    x✝¹
⊢ (ConcreteCategory.hom
          (((forget MonCat).mapCone
                  { pt := of (Types.Small.limitCone (F ⋙ forget MonCat)).pt,
                    π := { app := fun j ↦ ofHom (limitπMonoidHom F j), naturality := ⋯ } }).π.app
            x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom
          (((Types.isLimitEquivSections t).trans (equivShrink ↑(F ⋙ forget MonCat).sections)).symm.toIso.hom ≫
            c.π.app x✝¹)).toFun
      x✝