[Merged by Bors] - chore(Geometry/RingedSpace): remove use of `erw` in `stalkSpecializes_stalkMap` by euprunin · Pull Request #27656 · leanprover-community/mathlib4

euprunin · 2025-07-29T22:31:15Z

Show trace profiling of stalkSpecializes_stalkMap

Trace profiling of `stalkSpecializes_stalkMap` before PR 27656

diff --git a/Mathlib/Geometry/RingedSpace/Stalks.lean b/Mathlib/Geometry/RingedSpace/Stalks.lean
index 1440d9f1af..5d9287d34f 100644
--- a/Mathlib/Geometry/RingedSpace/Stalks.lean
+++ b/Mathlib/Geometry/RingedSpace/Stalks.lean
@@ -183,2 +183,3 @@ def stalkIso {X Y : PresheafedSpace.{_, _, v} C} (α : X ≅ Y) (x : X) :
 
+set_option trace.profiler true in
 @[reassoc (attr := simp), elementwise (attr := simp)]

ℹ [1147/1147] Built Mathlib.Geometry.RingedSpace.Stalks
info: Mathlib/Geometry/RingedSpace/Stalks.lean:185:0: [Elab.command] [0.676808] @[reassoc (attr := simp), elementwise (attr := simp)]
    theorem stalkSpecializes_stalkMap {X Y : PresheafedSpace.{_, _, v} C} (f : X ⟶ Y) {x y : X} (h : x ⤳ y) :
        Y.presheaf.stalkSpecializes (f.base.hom.map_specializes h) ≫ f.stalkMap x =
          f.stalkMap y ≫ X.presheaf.stalkSpecializes h :=
      by
      -- Porting note: the original one liner `dsimp [stalkMap]; simp [stalkMap]` doesn't work,
        -- I had to uglify this
      
      dsimp [stalkSpecializes, Hom.stalkMap, stalkFunctor, stalkPushforward]
        -- We can't use `ext` here due to https://github.com/leanprover/std4/pull/159
        
      refine colimit.hom_ext fun j => ?_
      induction j with
      | op j => ?_
      dsimp
      simp only [colimit.ι_desc_assoc, ι_colimMap_assoc, whiskerLeft_app, whiskerRight_app, NatTrans.id_app,
        colimit.ι_pre, assoc, colimit.pre_desc, colimit.map_desc, colimit.ι_desc, Cocones.precompose_obj_ι,
        Cocone.whisker_ι, NatTrans.comp_app]
      erw [X.presheaf.map_id, id_comp]
      rfl
  [Elab.attribute] [0.642492] applying [reassoc (attr := simp)]
  [Elab.attribute] [0.024500] applying [elementwise (attr := simp)]
info: Mathlib/Geometry/RingedSpace/Stalks.lean:185:0: [Elab.async] [0.628340] elaborating proof of AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap
  [Elab.definition.value] [0.623816] AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap
    [Elab.step] [0.620855] 
          dsimp [stalkSpecializes, Hom.stalkMap, stalkFunctor, stalkPushforward]
            -- We can't use `ext` here due to https://github.com/leanprover/std4/pull/159
            
          refine colimit.hom_ext fun j => ?_
          induction j with
          | op j => ?_
          dsimp
          simp only [colimit.ι_desc_assoc, ι_colimMap_assoc, whiskerLeft_app, whiskerRight_app, NatTrans.id_app,
            colimit.ι_pre, assoc, colimit.pre_desc, colimit.map_desc, colimit.ι_desc, Cocones.precompose_obj_ι,
            Cocone.whisker_ι, NatTrans.comp_app]
          erw [X.presheaf.map_id, id_comp]
          rfl
      [Elab.step] [0.620840] 
            dsimp [stalkSpecializes, Hom.stalkMap, stalkFunctor, stalkPushforward]
              -- We can't use `ext` here due to https://github.com/leanprover/std4/pull/159
              
            refine colimit.hom_ext fun j => ?_
            induction j with
            | op j => ?_
            dsimp
            simp only [colimit.ι_desc_assoc, ι_colimMap_assoc, whiskerLeft_app, whiskerRight_app, NatTrans.id_app,
              colimit.ι_pre, assoc, colimit.pre_desc, colimit.map_desc, colimit.ι_desc, Cocones.precompose_obj_ι,
              Cocone.whisker_ι, NatTrans.comp_app]
            erw [X.presheaf.map_id, id_comp]
            rfl
        [Elab.step] [0.059790] dsimp [stalkSpecializes, Hom.stalkMap, stalkFunctor, stalkPushforward]
        [Elab.step] [0.164574] refine colimit.hom_ext fun j => ?_
          [Elab.step] [0.164094] expected type: colimit.desc
                    ((OpenNhds.inclusion ((TopCat.Hom.hom f.base) y)).op ⋙ Y.presheaf)
                    { pt := colimit ((OpenNhds.inclusion ((TopCat.Hom.hom f.base) x)).op ⋙ Y.presheaf),
                      ι :=
                        {
                          app := fun U ↦
                            colimit.ι ((OpenNhds.inclusion ((TopCat.Hom.hom f.base) x)).op ⋙ Y.presheaf)
                              (op { obj := (unop U).obj, property := ⋯ }),
                          naturality := ⋯ } } ≫
                  colimMap ((OpenNhds.inclusion ((ConcreteCategory.hom f.base) x)).op.whiskerLeft f.c) ≫
                    colimMap (whiskerRight (𝟙 (OpenNhds.map f.base x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
                      colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map f.base x).op =
                (colimMap ((OpenNhds.inclusion ((ConcreteCategory.hom f.base) y)).op.whiskerLeft f.c) ≫
                    colimMap (whiskerRight (𝟙 (OpenNhds.map f.base y ⋙ OpenNhds.inclusion y).op) X.presheaf) ≫
                      colimit.pre ((OpenNhds.inclusion y).op ⋙ X.presheaf) (OpenNhds.map f.base y).op) ≫
                  colimit.desc ((OpenNhds.inclusion y).op ⋙ X.presheaf)
                    { pt := colimit ((OpenNhds.inclusion x).op ⋙ X.presheaf),
                      ι :=
                        {
                          app := fun U ↦
                            colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
                              (op { obj := (unop U).obj, property := ⋯ }),
                          naturality := ⋯ } }, term
              colimit.hom_ext fun j => ?_
            [Meta.synthInstance] [0.155453] ✅️ HasColimit
                  (((whiskeringLeft (OpenNhds ((TopCat.Hom.hom f.base) y))ᵒᵖ (Opens ↑↑Y)ᵒᵖ C).obj
                        (OpenNhds.inclusion ((TopCat.Hom.hom f.base) y)).op).obj
                    Y.presheaf)
        [Elab.step] [0.015593] dsimp
        [Elab.step] [0.271306] simp only [colimit.ι_desc_assoc, ι_colimMap_assoc, whiskerLeft_app, whiskerRight_app,
              NatTrans.id_app, colimit.ι_pre, assoc, colimit.pre_desc, colimit.map_desc, colimit.ι_desc,
              Cocones.precompose_obj_ι, Cocone.whisker_ι, NatTrans.comp_app]
          [Meta.isDefEq] [0.011490] ✅️ colimit.ι ?F ?j ≫
                colimit.desc ?F ?c ≫
                  ?h =?= colimit.ι ((OpenNhds.inclusion ((TopCat.Hom.hom f.base) y)).op ⋙ Y.presheaf) (op j) ≫
                colimit.desc ((OpenNhds.inclusion ((TopCat.Hom.hom f.base) y)).op ⋙ Y.presheaf)
                    { pt := colimit ((OpenNhds.inclusion ((TopCat.Hom.hom f.base) x)).op ⋙ Y.presheaf),
                      ι :=
                        {
                          app := fun U ↦
                            colimit.ι ((OpenNhds.inclusion ((TopCat.Hom.hom f.base) x)).op ⋙ Y.presheaf)
                              (op { obj := (unop U).obj, property := ⋯ }),
                          naturality := ⋯ } } ≫
                  colimMap ((OpenNhds.inclusion ((ConcreteCategory.hom f.base) x)).op.whiskerLeft f.c) ≫
                    colimMap (whiskerRight (𝟙 (OpenNhds.map f.base x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
                      colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map f.base x).op
            [Meta.isDefEq] [0.010484] ✅️ colimit.desc ((OpenNhds.inclusion ((TopCat.Hom.hom f.base) y)).op ⋙ Y.presheaf)
                    ?c ≫
                  ?h =?= colimit.desc ((OpenNhds.inclusion ((TopCat.Hom.hom f.base) y)).op ⋙ Y.presheaf)
                    { pt := colimit ((OpenNhds.inclusion ((TopCat.Hom.hom f.base) x)).op ⋙ Y.presheaf),
                      ι :=
                        {
                          app := fun U ↦
                            colimit.ι ((OpenNhds.inclusion ((TopCat.Hom.hom f.base) x)).op ⋙ Y.presheaf)
                              (op { obj := (unop U).obj, property := ⋯ }),
                          naturality := ⋯ } } ≫
                  colimMap ((OpenNhds.inclusion ((ConcreteCategory.hom f.base) x)).op.whiskerLeft f.c) ≫
                    colimMap (whiskerRight (𝟙 (OpenNhds.map f.base x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
                      colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map f.base x).op
          [Meta.isDefEq] [0.010218] ✅️ (whiskerRight ?α ?F).app
                ?X =?= (whiskerRight (𝟙 (OpenNhds.map f.base x ⋙ OpenNhds.inclusion x).op) X.presheaf).app
                (op { obj := j.obj, property := ⋯ })
            [Meta.isDefEq.delta] [0.010185] ✅️ (whiskerRight ?α ?F).app
                  ?X =?= (whiskerRight (𝟙 (OpenNhds.map f.base x ⋙ OpenNhds.inclusion x).op) X.presheaf).app
                  (op { obj := j.obj, property := ⋯ })
          [Meta.isDefEq] [0.010523] ✅️ colimMap ?α ≫
                colimit.desc ?G
                  ?c =?= colimMap (whiskerRight (𝟙 (OpenNhds.map f.base y ⋙ OpenNhds.inclusion y).op) X.presheaf) ≫
                colimit.desc ((OpenNhds.map f.base y).op ⋙ (OpenNhds.inclusion y).op ⋙ X.presheaf)
                  (Cocone.whisker (OpenNhds.map f.base y).op
                    { pt := colimit ((OpenNhds.inclusion x).op ⋙ X.presheaf),
                      ι :=
                        {
                          app := fun U ↦
                            colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
                              (op { obj := (unop U).obj, property := ⋯ }),
                          naturality := ⋯ } })
          [Meta.synthInstance] [0.138911] ✅️ HasColimitsOfShape (OpenNhds ((ConcreteCategory.hom f.base) y))ᵒᵖ C
            [Meta.synthInstance] [0.011998] ❌️ apply @BooleanAlgebra.toBoundedOrder to BoundedOrder
                  (OpenNhds ((ConcreteCategory.hom f.base) y))
              [Meta.synthInstance.tryResolve] [0.011965] ❌️ BoundedOrder
                    (OpenNhds ((ConcreteCategory.hom f.base) y)) ≟ BoundedOrder ?m.61603
                [Meta.isDefEq] [0.011920] ❌️ BoundedOrder
                      (OpenNhds ((ConcreteCategory.hom f.base) y)) =?= BoundedOrder ?m.61603
                  [Meta.isDefEq] [0.011809] ❌️ (OpenNhds.instLattice
                          ((ConcreteCategory.hom f.base)
                            y)).toLE =?= BooleanAlgebra.toDistribLattice.toSemilatticeInf.toLE
            [Meta.synthInstance] [0.015582] ❌️ apply @CoheytingAlgebra.toBoundedOrder to BoundedOrder
                  (OpenNhds ((ConcreteCategory.hom f.base) y))
              [Meta.synthInstance.tryResolve] [0.015536] ❌️ BoundedOrder
                    (OpenNhds ((ConcreteCategory.hom f.base) y)) ≟ BoundedOrder ?m.61642
                [Meta.isDefEq] [0.015487] ❌️ BoundedOrder
                      (OpenNhds ((ConcreteCategory.hom f.base) y)) =?= BoundedOrder ?m.61642
                  [Meta.isDefEq] [0.015310] ❌️ (OpenNhds.instLattice
                          ((ConcreteCategory.hom f.base)
                            y)).toLE =?= CoheytingAlgebra.toGeneralizedCoheytingAlgebra.toSemilatticeInf.toLE
                    [Meta.isDefEq.delta] [0.013448] ❌️ (OpenNhds.instLattice
                            ((ConcreteCategory.hom f.base)
                              y)).toLE =?= CoheytingAlgebra.toGeneralizedCoheytingAlgebra.toSemilatticeInf.toLE
                      [Meta.isDefEq] [0.013425] ❌️ (OpenNhds.instLattice
                              ((ConcreteCategory.hom f.base)
                                y)).toPreorder =?= CoheytingAlgebra.toGeneralizedCoheytingAlgebra.toSemilatticeInf.toPreorder
                        [Meta.isDefEq.delta] [0.010253] ❌️ (OpenNhds.instLattice
                                ((ConcreteCategory.hom f.base)
                                  y)).toPreorder =?= CoheytingAlgebra.toGeneralizedCoheytingAlgebra.toSemilatticeInf.toPreorder
                          [Meta.isDefEq] [0.010240] ❌️ (OpenNhds.instLattice
                                  ((ConcreteCategory.hom f.base)
                                    y)).toPartialOrder =?= CoheytingAlgebra.toGeneralizedCoheytingAlgebra.toSemilatticeInf.toPartialOrder
                            [Meta.isDefEq] [0.010149] ❌️ (OpenNhds.instLattice
                                    ((ConcreteCategory.hom f.base)
                                      y)).toPartialOrder =?= CoheytingAlgebra.toGeneralizedCoheytingAlgebra.toPartialOrder
            [Meta.synthInstance] [0.013427] ❌️ apply @HeytingAlgebra.toOrderBot to OrderBot
                  (OpenNhds ((ConcreteCategory.hom f.base) y))
              [Meta.synthInstance.tryResolve] [0.013405] ❌️ OrderBot
                    (OpenNhds ((ConcreteCategory.hom f.base) y)) ≟ OrderBot ?m.62409
                [Meta.isDefEq] [0.013394] ❌️ OrderBot (OpenNhds ((ConcreteCategory.hom f.base) y)) =?= OrderBot ?m.62409
                  [Meta.isDefEq] [0.013335] ❌️ (OpenNhds.partialOrder
                          ((ConcreteCategory.hom f.base) y)).toLE =?= HeytingAlgebra.toGeneralizedHeytingAlgebra.toLE
                    [Meta.isDefEq.delta] [0.011364] ❌️ (OpenNhds.partialOrder
                            ((ConcreteCategory.hom f.base) y)).toLE =?= HeytingAlgebra.toGeneralizedHeytingAlgebra.toLE
                      [Meta.isDefEq] [0.011348] ❌️ (OpenNhds.partialOrder
                              ((ConcreteCategory.hom f.base)
                                y)).toPreorder =?= HeytingAlgebra.toGeneralizedHeytingAlgebra.toPreorder
                        [Meta.isDefEq.delta] [0.010235] ❌️ (OpenNhds.partialOrder
                                ((ConcreteCategory.hom f.base)
                                  y)).toPreorder =?= HeytingAlgebra.toGeneralizedHeytingAlgebra.toPreorder
                          [Meta.isDefEq] [0.010220] ❌️ OpenNhds.partialOrder
                                ((ConcreteCategory.hom f.base)
                                  y) =?= HeytingAlgebra.toGeneralizedHeytingAlgebra.toPartialOrder
                            [Meta.isDefEq] [0.010176] ❌️ { le := fun U V ↦ U.obj ≤ V.obj, le_refl := ⋯, le_trans := ⋯,
                                  lt_iff_le_not_ge := ⋯,
                                  le_antisymm := ⋯ } =?= HeytingAlgebra.toGeneralizedHeytingAlgebra.toPartialOrder
                              [Meta.isDefEq] [0.010164] ❌️ { le := fun U V ↦ U.obj ≤ V.obj, le_refl := ⋯, le_trans := ⋯,
                                    lt_iff_le_not_ge := ⋯,
                                    le_antisymm := ⋯ } =?= HeytingAlgebra.toGeneralizedHeytingAlgebra.toSemilatticeSup.1
                                [Meta.isDefEq] [0.010046] ❌️ HeytingAlgebra.toGeneralizedHeytingAlgebra.toSemilatticeSup.1.toPreorder =?= {
                                      le := fun U V ↦ U.obj ≤ V.obj, le_refl := ⋯, le_trans := ⋯,
                                      lt_iff_le_not_ge := ⋯ }
                                  [Meta.isDefEq] [0.010033] ❌️ HeytingAlgebra.toGeneralizedHeytingAlgebra.toSemilatticeSup.1.1 =?= {
                                        le := fun U V ↦ U.obj ≤ V.obj, le_refl := ⋯, le_trans := ⋯,
                                        lt_iff_le_not_ge := ⋯ }
        [Elab.step] [0.104614] erw [X.presheaf.map_id, id_comp]
          [Elab.step] [0.102932] rw (transparency✝ := .default✝) [X.presheaf.map_id, id_comp]
            [Elab.step] [0.102923] (rewrite (transparency✝ := .default✝) [X.presheaf.map_id, id_comp];
                  with_annotate_state"]" (try (with_reducible rfl)))
              [Elab.step] [0.102916] rewrite (transparency✝ := .default✝) [X.presheaf.map_id, id_comp];
                    with_annotate_state"]" (try (with_reducible rfl))
                [Elab.step] [0.102910] rewrite (transparency✝ := .default✝) [X.presheaf.map_id, id_comp];
                      with_annotate_state"]" (try (with_reducible rfl))
                  [Elab.step] [0.101366] rewrite (transparency✝ := .default✝) [X.presheaf.map_id, id_comp]
                    [Meta.check] [0.037638] ✅️ fun _a ↦
                          f.c.app
                                ((OpenNhds.inclusion ((ConcreteCategory.hom f.base) x)).op.obj
                                  (op { obj := j.obj, property := ⋯ })) ≫
                              _a ≫
                                colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
                                  ((OpenNhds.map f.base x).op.obj (op { obj := j.obj, property := ⋯ })) =
                            f.c.app ((OpenNhds.inclusion ((ConcreteCategory.hom f.base) y)).op.obj (op j)) ≫
                              _a ≫
                                colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
                                  (op { obj := (unop ((OpenNhds.map f.base y).op.obj (op j))).obj, property := ⋯ })
                    [Meta.check] [0.027742] ✅️ fun _a ↦
                          f.c.app
                                ((OpenNhds.inclusion ((ConcreteCategory.hom f.base) x)).op.obj
                                  (op { obj := j.obj, property := ⋯ })) ≫
                              _a =
                            f.c.app ((OpenNhds.inclusion ((ConcreteCategory.hom f.base) y)).op.obj (op j)) ≫ _a
info: Mathlib/Geometry/RingedSpace/Stalks.lean:186:8: [Elab.async] [0.046946] Lean.addDecl
  [Kernel] [0.046926] typechecking declarations [AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap]
info: Mathlib/Geometry/RingedSpace/Stalks.lean:185:2: [Elab.async] [0.050374] Lean.addDecl
  [Kernel] [0.050355] typechecking declarations [AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap_assoc]
info: Mathlib/Geometry/RingedSpace/Stalks.lean:185:26: [Elab.async] [0.076721] Lean.addDecl
  [Kernel] [0.076693] typechecking declarations [AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap_apply]
Build completed successfully.

Trace profiling of `stalkSpecializes_stalkMap` after PR 27656

diff --git a/Mathlib/Geometry/RingedSpace/Stalks.lean b/Mathlib/Geometry/RingedSpace/Stalks.lean
index 1440d9f1af..115caed2ad 100644
--- a/Mathlib/Geometry/RingedSpace/Stalks.lean
+++ b/Mathlib/Geometry/RingedSpace/Stalks.lean
@@ -183,2 +183,3 @@ def stalkIso {X Y : PresheafedSpace.{_, _, v} C} (α : X ≅ Y) (x : X) :
 
+set_option trace.profiler true in
 @[reassoc (attr := simp), elementwise (attr := simp)]
@@ -199,4 +200,3 @@ theorem stalkSpecializes_stalkMap {X Y : PresheafedSpace.{_, _, v} C}
     Cocone.whisker_ι, NatTrans.comp_app]
-  erw [X.presheaf.map_id, id_comp]
-  rfl
+  tauto

ℹ [1147/1147] Built Mathlib.Geometry.RingedSpace.Stalks
info: Mathlib/Geometry/RingedSpace/Stalks.lean:185:0: [Elab.command] [0.574442] @[reassoc (attr := simp), elementwise (attr := simp)]
    theorem stalkSpecializes_stalkMap {X Y : PresheafedSpace.{_, _, v} C} (f : X ⟶ Y) {x y : X} (h : x ⤳ y) :
        Y.presheaf.stalkSpecializes (f.base.hom.map_specializes h) ≫ f.stalkMap x =
          f.stalkMap y ≫ X.presheaf.stalkSpecializes h :=
      by
      -- Porting note: the original one liner `dsimp [stalkMap]; simp [stalkMap]` doesn't work,
        -- I had to uglify this
      
      dsimp [stalkSpecializes, Hom.stalkMap, stalkFunctor, stalkPushforward]
        -- We can't use `ext` here due to https://github.com/leanprover/std4/pull/159
        
      refine colimit.hom_ext fun j => ?_
      induction j with
      | op j => ?_
      dsimp
      simp only [colimit.ι_desc_assoc, ι_colimMap_assoc, whiskerLeft_app, whiskerRight_app, NatTrans.id_app,
        colimit.ι_pre, assoc, colimit.pre_desc, colimit.map_desc, colimit.ι_desc, Cocones.precompose_obj_ι,
        Cocone.whisker_ι, NatTrans.comp_app]
      tauto
  [Elab.attribute] [0.534843] applying [reassoc (attr := simp)]
  [Elab.attribute] [0.029518] applying [elementwise (attr := simp)]
info: Mathlib/Geometry/RingedSpace/Stalks.lean:185:0: [Elab.async] [0.518954] elaborating proof of AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap
  [Elab.definition.value] [0.515007] AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap
    [Elab.step] [0.513351] 
          dsimp [stalkSpecializes, Hom.stalkMap, stalkFunctor, stalkPushforward]
            -- We can't use `ext` here due to https://github.com/leanprover/std4/pull/159
            
          refine colimit.hom_ext fun j => ?_
          induction j with
          | op j => ?_
          dsimp
          simp only [colimit.ι_desc_assoc, ι_colimMap_assoc, whiskerLeft_app, whiskerRight_app, NatTrans.id_app,
            colimit.ι_pre, assoc, colimit.pre_desc, colimit.map_desc, colimit.ι_desc, Cocones.precompose_obj_ι,
            Cocone.whisker_ι, NatTrans.comp_app]
          tauto
      [Elab.step] [0.513336] 
            dsimp [stalkSpecializes, Hom.stalkMap, stalkFunctor, stalkPushforward]
              -- We can't use `ext` here due to https://github.com/leanprover/std4/pull/159
              
            refine colimit.hom_ext fun j => ?_
            induction j with
            | op j => ?_
            dsimp
            simp only [colimit.ι_desc_assoc, ι_colimMap_assoc, whiskerLeft_app, whiskerRight_app, NatTrans.id_app,
              colimit.ι_pre, assoc, colimit.pre_desc, colimit.map_desc, colimit.ι_desc, Cocones.precompose_obj_ι,
              Cocone.whisker_ι, NatTrans.comp_app]
            tauto
        [Elab.step] [0.064070] dsimp [stalkSpecializes, Hom.stalkMap, stalkFunctor, stalkPushforward]
          [Meta.isDefEq] [0.011951] ✅️ colim.map
                ?α =?= colim.map (whiskerRight (𝟙 (OpenNhds.map f.base x ⋙ OpenNhds.inclusion x).op) X.presheaf)
            [Meta.isDefEq.delta] [0.011888] ✅️ colim.map
                  ?α =?= colim.map (whiskerRight (𝟙 (OpenNhds.map f.base x ⋙ OpenNhds.inclusion x).op) X.presheaf)
              [Meta.isDefEq] [0.011036] ✅️ ?α =?= whiskerRight (𝟙 (OpenNhds.map f.base x ⋙ OpenNhds.inclusion x).op)
                    X.presheaf
                [Meta.isDefEq.assign] [0.011033] ✅️ ?α := whiskerRight
                      (𝟙 (OpenNhds.map f.base x ⋙ OpenNhds.inclusion x).op) X.presheaf
                  [Meta.isDefEq.assign.checkTypes] [0.011000] ✅️ (?α : (OpenNhds.inclusion
                              ((ConcreteCategory.hom f.base) x)).op ⋙
                          (pushforward C f.base).obj X.presheaf ⟶
                        (OpenNhds.map f.base x).op ⋙
                          (OpenNhds.inclusion x).op ⋙
                            X.presheaf) := (whiskerRight (𝟙 (OpenNhds.map f.base x ⋙ OpenNhds.inclusion x).op)
                        X.presheaf : (OpenNhds.inclusion ((ConcreteCategory.hom f.base) x) ⋙ Opens.map f.base).op ⋙
                          X.presheaf ⟶
                        (OpenNhds.map f.base x ⋙ OpenNhds.inclusion x).op ⋙ X.presheaf)
                    [Meta.isDefEq] [0.010995] ✅️ (OpenNhds.inclusion ((ConcreteCategory.hom f.base) x)).op ⋙
                            (pushforward C f.base).obj X.presheaf ⟶
                          (OpenNhds.map f.base x).op ⋙
                            (OpenNhds.inclusion x).op ⋙
                              X.presheaf =?= (OpenNhds.inclusion ((ConcreteCategory.hom f.base) x) ⋙
                                Opens.map f.base).op ⋙
                            X.presheaf ⟶
                          (OpenNhds.map f.base x ⋙ OpenNhds.inclusion x).op ⋙ X.presheaf
                      [Meta.isDefEq] [0.010958] ✅️ category.toQuiver.1
                            ((OpenNhds.inclusion ((ConcreteCategory.hom f.base) x)).op ⋙
                              (pushforward C f.base).obj X.presheaf)
                            ((OpenNhds.map f.base x).op ⋙
                              (OpenNhds.inclusion x).op ⋙
                                X.presheaf) =?= category.toQuiver.1
                            ((OpenNhds.inclusion ((ConcreteCategory.hom f.base) x) ⋙ Opens.map f.base).op ⋙ X.presheaf)
                            ((OpenNhds.map f.base x ⋙ OpenNhds.inclusion x).op ⋙ X.presheaf)
                        [Meta.isDefEq] [0.010828] ✅️ NatTrans
                              ((OpenNhds.inclusion ((ConcreteCategory.hom f.base) x)).op ⋙
                                (pushforward C f.base).obj X.presheaf)
                              ((OpenNhds.map f.base x).op ⋙
                                (OpenNhds.inclusion x).op ⋙
                                  X.presheaf) =?= NatTrans
                              ((OpenNhds.inclusion ((ConcreteCategory.hom f.base) x) ⋙ Opens.map f.base).op ⋙
                                X.presheaf)
                              ((OpenNhds.map f.base x ⋙ OpenNhds.inclusion x).op ⋙ X.presheaf)
        [Elab.step] [0.164481] refine colimit.hom_ext fun j => ?_
          [Elab.step] [0.164004] expected type: colimit.desc
                    ((OpenNhds.inclusion ((TopCat.Hom.hom f.base) y)).op ⋙ Y.presheaf)
                    { pt := colimit ((OpenNhds.inclusion ((TopCat.Hom.hom f.base) x)).op ⋙ Y.presheaf),
                      ι :=
                        {
                          app := fun U ↦
                            colimit.ι ((OpenNhds.inclusion ((TopCat.Hom.hom f.base) x)).op ⋙ Y.presheaf)
                              (op { obj := (unop U).obj, property := ⋯ }),
                          naturality := ⋯ } } ≫
                  colimMap ((OpenNhds.inclusion ((ConcreteCategory.hom f.base) x)).op.whiskerLeft f.c) ≫
                    colimMap (whiskerRight (𝟙 (OpenNhds.map f.base x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
                      colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map f.base x).op =
                (colimMap ((OpenNhds.inclusion ((ConcreteCategory.hom f.base) y)).op.whiskerLeft f.c) ≫
                    colimMap (whiskerRight (𝟙 (OpenNhds.map f.base y ⋙ OpenNhds.inclusion y).op) X.presheaf) ≫
                      colimit.pre ((OpenNhds.inclusion y).op ⋙ X.presheaf) (OpenNhds.map f.base y).op) ≫
                  colimit.desc ((OpenNhds.inclusion y).op ⋙ X.presheaf)
                    { pt := colimit ((OpenNhds.inclusion x).op ⋙ X.presheaf),
                      ι :=
                        {
                          app := fun U ↦
                            colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
                              (op { obj := (unop U).obj, property := ⋯ }),
                          naturality := ⋯ } }, term
              colimit.hom_ext fun j => ?_
            [Meta.synthInstance] [0.159686] ✅️ HasColimit
                  (((whiskeringLeft (OpenNhds ((TopCat.Hom.hom f.base) y))ᵒᵖ (Opens ↑↑Y)ᵒᵖ C).obj
                        (OpenNhds.inclusion ((TopCat.Hom.hom f.base) y)).op).obj
                    Y.presheaf)
              [Meta.synthInstance] [0.013890] ❌️ apply @GeneralizedBooleanAlgebra.toOrderBot to OrderBot
                    (OpenNhds ((TopCat.Hom.hom f.base) y))
                [Meta.synthInstance.tryResolve] [0.013857] ❌️ OrderBot
                      (OpenNhds ((TopCat.Hom.hom f.base) y)) ≟ OrderBot ?m.57320
                  [Meta.isDefEq] [0.013814] ❌️ OrderBot (OpenNhds ((TopCat.Hom.hom f.base) y)) =?= OrderBot ?m.57320
                    [Meta.isDefEq] [0.013706] ❌️ (OpenNhds.instLattice
                            ((TopCat.Hom.hom f.base)
                              y)).toLE =?= GeneralizedBooleanAlgebra.toDistribLattice.toSemilatticeInf.toLE
                      [Meta.isDefEq.delta] [0.012023] ❌️ (OpenNhds.instLattice
                              ((TopCat.Hom.hom f.base)
                                y)).toLE =?= GeneralizedBooleanAlgebra.toDistribLattice.toSemilatticeInf.toLE
                        [Meta.isDefEq] [0.012012] ❌️ (OpenNhds.instLattice
                                ((TopCat.Hom.hom f.base)
                                  y)).toPreorder =?= GeneralizedBooleanAlgebra.toDistribLattice.toSemilatticeInf.toPreorder
              [Meta.synthInstance] [0.010702] ❌️ apply @GeneralizedCoheytingAlgebra.toOrderBot to OrderBot
                    (OpenNhds ((TopCat.Hom.hom f.base) y))
                [Meta.synthInstance.tryResolve] [0.010659] ❌️ OrderBot
                      (OpenNhds ((TopCat.Hom.hom f.base) y)) ≟ OrderBot ?m.57359
                  [Meta.isDefEq] [0.010608] ❌️ OrderBot (OpenNhds ((TopCat.Hom.hom f.base) y)) =?= OrderBot ?m.57359
        [Elab.step] [0.257030] simp only [colimit.ι_desc_assoc, ι_colimMap_assoc, whiskerLeft_app, whiskerRight_app,
              NatTrans.id_app, colimit.ι_pre, assoc, colimit.pre_desc, colimit.map_desc, colimit.ι_desc,
              Cocones.precompose_obj_ι, Cocone.whisker_ι, NatTrans.comp_app]
          [Meta.isDefEq] [0.017085] ✅️ colimMap ?α ≫
                colimit.desc ?G
                  ?c =?= colimMap (whiskerRight (𝟙 (OpenNhds.map f.base y ⋙ OpenNhds.inclusion y).op) X.presheaf) ≫
                colimit.desc ((OpenNhds.map f.base y).op ⋙ (OpenNhds.inclusion y).op ⋙ X.presheaf)
                  (Cocone.whisker (OpenNhds.map f.base y).op
                    { pt := colimit ((OpenNhds.inclusion x).op ⋙ X.presheaf),
                      ι :=
                        {
                          app := fun U ↦
                            colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
                              (op { obj := (unop U).obj, property := ⋯ }),
                          naturality := ⋯ } })
            [Meta.isDefEq] [0.011374] ✅️ colimMap
                  ?α =?= colimMap (whiskerRight (𝟙 (OpenNhds.map f.base y ⋙ OpenNhds.inclusion y).op) X.presheaf)
              [Meta.isDefEq] [0.010653] ✅️ ?α =?= whiskerRight (𝟙 (OpenNhds.map f.base y ⋙ OpenNhds.inclusion y).op)
                    X.presheaf
                [Meta.isDefEq.assign] [0.010649] ✅️ ?α := whiskerRight
                      (𝟙 (OpenNhds.map f.base y ⋙ OpenNhds.inclusion y).op) X.presheaf
                  [Meta.isDefEq.assign.checkTypes] [0.010618] ✅️ (?α : (OpenNhds.inclusion
                              ((ConcreteCategory.hom f.base) y)).op ⋙
                          (pushforward C f.base).obj X.presheaf ⟶
                        (OpenNhds.map f.base y).op ⋙
                          (OpenNhds.inclusion y).op ⋙
                            X.presheaf) := (whiskerRight (𝟙 (OpenNhds.map f.base y ⋙ OpenNhds.inclusion y).op)
                        X.presheaf : (OpenNhds.inclusion ((ConcreteCategory.hom f.base) y) ⋙ Opens.map f.base).op ⋙
                          X.presheaf ⟶
                        (OpenNhds.map f.base y ⋙ OpenNhds.inclusion y).op ⋙ X.presheaf)
                    [Meta.isDefEq] [0.010613] ✅️ (OpenNhds.inclusion ((ConcreteCategory.hom f.base) y)).op ⋙
                            (pushforward C f.base).obj X.presheaf ⟶
                          (OpenNhds.map f.base y).op ⋙
                            (OpenNhds.inclusion y).op ⋙
                              X.presheaf =?= (OpenNhds.inclusion ((ConcreteCategory.hom f.base) y) ⋙
                                Opens.map f.base).op ⋙
                            X.presheaf ⟶
                          (OpenNhds.map f.base y ⋙ OpenNhds.inclusion y).op ⋙ X.presheaf
                      [Meta.isDefEq] [0.010570] ✅️ category.toQuiver.1
                            ((OpenNhds.inclusion ((ConcreteCategory.hom f.base) y)).op ⋙
                              (pushforward C f.base).obj X.presheaf)
                            ((OpenNhds.map f.base y).op ⋙
                              (OpenNhds.inclusion y).op ⋙
                                X.presheaf) =?= category.toQuiver.1
                            ((OpenNhds.inclusion ((ConcreteCategory.hom f.base) y) ⋙ Opens.map f.base).op ⋙ X.presheaf)
                            ((OpenNhds.map f.base y ⋙ OpenNhds.inclusion y).op ⋙ X.presheaf)
                        [Meta.isDefEq] [0.010418] ✅️ NatTrans
                              ((OpenNhds.inclusion ((ConcreteCategory.hom f.base) y)).op ⋙
                                (pushforward C f.base).obj X.presheaf)
                              ((OpenNhds.map f.base y).op ⋙
                                (OpenNhds.inclusion y).op ⋙
                                  X.presheaf) =?= NatTrans
                              ((OpenNhds.inclusion ((ConcreteCategory.hom f.base) y) ⋙ Opens.map f.base).op ⋙
                                X.presheaf)
                              ((OpenNhds.map f.base y ⋙ OpenNhds.inclusion y).op ⋙ X.presheaf)
          [Meta.synthInstance] [0.120468] ✅️ HasColimitsOfShape (OpenNhds ((ConcreteCategory.hom f.base) y))ᵒᵖ C
            [Meta.synthInstance] [0.011075] ❌️ apply @CompleteLattice.toBoundedOrder to BoundedOrder
                  (OpenNhds ((ConcreteCategory.hom f.base) y))
              [Meta.synthInstance.tryResolve] [0.011054] ❌️ BoundedOrder
                    (OpenNhds ((ConcreteCategory.hom f.base) y)) ≟ BoundedOrder ?m.61530
                [Meta.isDefEq] [0.011031] ❌️ BoundedOrder
                      (OpenNhds ((ConcreteCategory.hom f.base) y)) =?= BoundedOrder ?m.61530
            [Meta.synthInstance] [0.016436] ❌️ apply @CompleteLattice.hasColimits_of_completeLattice to HasColimits
                  (OpenNhds ((ConcreteCategory.hom f.base) y))
              [Meta.synthInstance.tryResolve] [0.016392] ❌️ HasColimits
                    (OpenNhds
                      ((ConcreteCategory.hom f.base)
                        y)) ≟ HasColimitsOfSize.{?u.61885, ?u.61886, ?u.61887, ?u.61887} ?m.61890
                [Meta.isDefEq] [0.016370] ❌️ HasColimits
                      (OpenNhds
                        ((ConcreteCategory.hom f.base)
                          y)) =?= HasColimitsOfSize.{?u.61885, ?u.61886, ?u.61887, ?u.61887} ?m.61890
                  [Meta.isDefEq] [0.016339] ❌️ HasColimitsOfSize.{v, v, v, v}
                        (OpenNhds
                          ((ConcreteCategory.hom f.base)
                            y)) =?= HasColimitsOfSize.{?u.61885, ?u.61886, ?u.61887, ?u.61887} ?m.61890
                    [Meta.isDefEq] [0.016255] ❌️ OpenNhds.openNhdsCategory
                          ((ConcreteCategory.hom f.base)
                            y) =?= Preorder.smallCategory (OpenNhds ((ConcreteCategory.hom f.base) y))
                      [Meta.isDefEq] [0.016204] ❌️ inferInstance =?= { Hom := fun U V ↦ ULift.{v, 0} (PLift (U ≤ V)),
                            id := fun X_1 ↦ { down := { down := ⋯ } },
                            comp := fun {X_1 Y_1 Z} f_1 g ↦ { down := { down := ⋯ } }, id_comp := ⋯, comp_id := ⋯,
                            assoc := ⋯ }
                        [Meta.isDefEq] [0.016154] ❌️ Preorder.smallCategory
                              (OpenNhds
                                ((ConcreteCategory.hom f.base)
                                  y)) =?= { Hom := fun U V ↦ ULift.{v, 0} (PLift (U ≤ V)),
                              id := fun X_1 ↦ { down := { down := ⋯ } },
                              comp := fun {X_1 Y_1 Z} f_1 g ↦ { down := { down := ⋯ } }, id_comp := ⋯, comp_id := ⋯,
                              assoc := ⋯ }
                          [Meta.isDefEq] [0.014700] ❌️ { Hom := fun U V ↦ ULift.{v, 0} (PLift (U ≤ V)),
                                id := fun X_1 ↦ { down := { down := ⋯ } },
                                comp := fun {X_1 Y_1 Z} f_1 g ↦ { down := { down := ⋯ } }, id_comp := ⋯, comp_id := ⋯,
                                assoc :=
                                  ⋯ } =?= { Hom := fun U V ↦ ULift.{v, 0} (PLift (U ≤ V)),
                                id := fun X_1 ↦ { down := { down := ⋯ } },
                                comp := fun {X_1 Y_1 Z} f_1 g ↦ { down := { down := ⋯ } }, id_comp := ⋯, comp_id := ⋯,
                                assoc := ⋯ }
                            [Meta.isDefEq] [0.014647] ❌️ { Hom := fun U V ↦ ULift.{v, 0} (PLift (U ≤ V)),
                                  id := fun X_1 ↦ { down := { down := ⋯ } },
                                  comp := fun {X_1 Y_1 Z} f_1 g ↦
                                    {
                                      down :=
                                        {
                                          down :=
                                            ⋯ } } } =?= { Hom := fun U V ↦ ULift.{v, 0} (PLift (U ≤ V)),
                                  id := fun X_1 ↦ { down := { down := ⋯ } },
                                  comp := fun {X_1 Y_1 Z} f_1 g ↦ { down := { down := ⋯ } } }
                              [Meta.isDefEq] [0.014605] ❌️ fun X_1 ↦
                                    { down := { down := ⋯ } } =?= fun X_1 ↦ { down := { down := ⋯ } }
                                [Meta.isDefEq] [0.014589] ❌️ { down := { down := ⋯ } } =?= { down := { down := ⋯ } }
                                  [Meta.isDefEq] [0.014519] ❌️ { down := ⋯ } =?= { down := ⋯ }
                                    [Meta.isDefEq] [0.014425] ❌️ X ≤ X =?= X ≤ X
        [Elab.step] [0.018070] tauto
info: Mathlib/Geometry/RingedSpace/Stalks.lean:186:8: [Elab.async] [0.054797] Lean.addDecl
  [Kernel] [0.054774] typechecking declarations [AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap]
info: Mathlib/Geometry/RingedSpace/Stalks.lean:185:2: [Elab.async] [0.044230] Lean.addDecl
  [Kernel] [0.044215] typechecking declarations [AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap_assoc]
info: Mathlib/Geometry/RingedSpace/Stalks.lean:185:26: [Elab.async] [0.060723] Lean.addDecl
  [Kernel] [0.060702] typechecking declarations [AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap_apply]
Build completed successfully.

…_stalkMap`

github-actions · 2025-07-29T22:32:30Z

PR summary 0465630e7f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

Decrease in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
808	-1	erw

Current commit 0994481add
Reference commit 0465630e7f

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

euprunin · 2025-08-04T12:14:28Z

Added trace profiling results. No notable slowdown (on the contrary: judging from the profiling results, the new version appears slightly faster).

mattrobball · 2025-08-15T12:18:33Z

bors merge

…_stalkMap` (#27656)

mathlib-bors · 2025-08-15T12:32:29Z

Pull request successfully merged into master.

Build succeeded:

CI Success

* origin/master: (508 commits) feat(Logic/Basic): forall_and_index (leanprover-community#27737) feat(Algebra/intNorm): `x` divides `intNorm x` (leanprover-community#28021) feat(RingTheory/MvPolynomial/MonomialOrder): some lemmas about degree (leanprover-community#26000) chore: more elementary Motzkin polynomial proof (leanprover-community#28482) feat: e-seminormed monoid (leanprover-community#27385) feat(RingTheory): ` (⊥ : Ideal R) ^ n = ⊥` (leanprover-community#28171) fix(LinearAlgebra/Dimension/ErdosKaplansky): authorship (leanprover-community#28513) chore: golf entire `X_pow_eq_monomial` (leanprover-community#28504) feat(RingTheory): invertible modules and Picard group (leanprover-community#25337) chore: use delta `deriving` for leanprover-community#380 (leanprover-community#28498) feat: add bilinear maps for vector/matrix products (leanprover-community#28130) feat(Counterexamples): topologists' sine curve (leanprover-community#25833) feat(Analysis/Convex): doubly stochastic matrices have operator norm at most one (leanprover-community#28453) chore(Topology/Compactification): deprecate duplicate `ultrafilter_pure_injective` (leanprover-community#28436) feat: add `@[simp]` to `Multiset.cons_le_cons` and `Finset.insert_subset_insert` (leanprover-community#28285) feat: make `ring` work for semifields (leanprover-community#28494) feat: filtering lists and bounded quantifiers are primitive recursive (leanprover-community#26295) chore(Analysis/Analytic): split `Analytic.Basic` (leanprover-community#26270) refactor: tidy `mulVec` and `vecMul` lemmas about `•` (leanprover-community#28450) feat(Order/WellFounded): Acc and infinite descending chain (leanprover-community#28120) feat(NumberTheory/Padics): {Int,Rat}.padicValuation (leanprover-community#27667) chore(*): address a few timeout-related porting notes (leanprover-community#28483) feat(Algebra): toAlgebra_algebraMap (leanprover-community#28238) feat(Shrink): `IsCancelMul` instance (leanprover-community#28407) chore(Geometry): golf entire `chart_eq'` and `orthogonalProjection_orthogonalProjection` (leanprover-community#28485) feat: shifted geometric series and a `ProbabilityMeasure` version of `measure_iUnion_le` (leanprover-community#28087) chore(LinearAlgebra/PiTensorProduct): `rw` away use of `erw` in `lifts_zero` (leanprover-community#27554) feat(RingTheory): faithfully flat ring maps (leanprover-community#24530) chore(Geometry/RingedSpace): remove use of `erw` in `stalkSpecializes_stalkMap` (leanprover-community#27656) chore: add the Brownian motion project to downstream_repos.yml (leanprover-community#28459) feat(CategoryTheory/Sites/SheafOfTypes): composition of a sheaf with uliftFunctor is still a sheaf (leanprover-community#27816) feat(Valuation/DiscreteValuationRel): val relations with compatible valuations to Zm0 are IsDiscrete (leanprover-community#27213) chore(*): process a bunch of `aesop`-related porting notes (leanprover-community#28402) feat(CategoryTheory): abstract argument for the stability under transfinite compositions (leanprover-community#26030) chore: bump toolchain to v4.23.0-rc2 (leanprover-community#28454) chore(FieldTheory/Finite): fermat's little theorem in Nat form (leanprover-community#27962) feat(Combinatorics/SimpleGraph/Paths): add theorem `SimpleGraph.Walk.IsPath.concat` (leanprover-community#27582) feat(Slope): slope_pos_iff_of_le and related lemmas (leanprover-community#28039) feat: tactic analysis framework (leanprover-community#26683) chore(Data/EReal): deprecate `add_pos_of_nonneg_of_pos` and `add_ne_top_iff_of_ne_bot` (duplicates) (leanprover-community#28424) feat(MathlibTest/FieldSimp): add a few more tests (leanprover-community#28413) chore(RingTheory/HahnSeries): deprecate duplicate `orderTop_add_orderTop_le_orderTop_mul` (leanprover-community#28231) chore(AlgebraicGeometry/IdealSheaf): deprecate duplicate `AlgebraicGeometry.Scheme.IdealSheafData.Scheme.zeroLocus_radical` (leanprover-community#28202) feat(Algebra/Order): ArchimedeanClass ball (leanprover-community#27885) chore(Geometry/RingedSpace): remove use of `erw` in `isUnit_of_isUnit_germ` (leanprover-community#27660) feat(SkewMonoidAlgebra): coeff_mul lemmas (leanprover-community#27255) chore(LinearAlgebra): golf entire `isUnit_det` (leanprover-community#28438) chore(FieldTheory/IntermediateField): golf entire `coe_sum` and `coe_prod` (leanprover-community#28431) feat: separate linter error message for empty doc-strings (leanprover-community#27895) feat(RingTheory/PowerSeries/Binomial): add basic lemmas, golf (leanprover-community#27497) ...

…_stalkMap` (leanprover-community#27656)

chore(Geometry/RingedSpace): remove use of erw in `stalkSpecializes…

0994481

…_stalkMap`

github-actions bot added the t-algebraic-geometry Algebraic geometry label Jul 29, 2025

leanprover-community-bot-assistant assigned mattrobball Aug 15, 2025

ghost added the ready-to-merge This PR has been sent to bors. label Aug 15, 2025

mathlib-bors bot pushed a commit that referenced this pull request Aug 15, 2025

chore(Geometry/RingedSpace): remove use of erw in `stalkSpecializes…

3fb2e06

…_stalkMap` (#27656)

mathlib-bors bot changed the title ~~chore(Geometry/RingedSpace): remove use of erw in stalkSpecializes_stalkMap~~ [Merged by Bors] - chore(Geometry/RingedSpace): remove use of erw in stalkSpecializes_stalkMap Aug 15, 2025

mathlib-bors bot closed this Aug 15, 2025

Paul-Lez pushed a commit to Paul-Lez/mathlib4 that referenced this pull request Aug 23, 2025

chore(Geometry/RingedSpace): remove use of erw in `stalkSpecializes…

027ed18

…_stalkMap` (leanprover-community#27656)

pechersky pushed a commit to pechersky/mathlib4 that referenced this pull request Aug 25, 2025

chore(Geometry/RingedSpace): remove use of erw in `stalkSpecializes…

cc71095

…_stalkMap` (leanprover-community#27656)

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore(Geometry/RingedSpace): remove use of `erw` in `stalkSpecializes_stalkMap`#27656

[Merged by Bors] - chore(Geometry/RingedSpace): remove use of `erw` in `stalkSpecializes_stalkMap`#27656
euprunin wants to merge 1 commit intoleanprover-community:masterfrom
euprunin:erw-15

euprunin commented Jul 29, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Jul 29, 2025

Uh oh!

euprunin commented Aug 4, 2025

Uh oh!

mattrobball commented Aug 15, 2025

Uh oh!

mathlib-bors bot commented Aug 15, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

euprunin commented Jul 29, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Trace profiling of stalkSpecializes_stalkMap before PR 27656

Trace profiling of stalkSpecializes_stalkMap after PR 27656

Uh oh!

github-actions bot commented Jul 29, 2025

PR summary 0465630e7f

Import changes for modified files

Declarations diff

Uh oh!

euprunin commented Aug 4, 2025

Uh oh!

mattrobball commented Aug 15, 2025

Uh oh!

mathlib-bors bot commented Aug 15, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

euprunin commented Jul 29, 2025 •

edited

Loading

Trace profiling of `stalkSpecializes_stalkMap` before PR 27656

Trace profiling of `stalkSpecializes_stalkMap` after PR 27656