Bumping mathlib to 79d0395 would break the build

[github-actions]

An incompatibility has been detected between this project and recent changes in mathlib.
In other words, this project can't advance to the tip of mathlib without breaking.

First incompatible mathlib commit: 79d0395 — chore: bump toolchain to v4.33.0-rc1 (#41779) (2026-07-16 (Garmelon)).

Last-known-good mathlib commit: 3dffaf2 — chore(Combinatorics): restore deprecated pentagonal.lean module (#41397) (2026-07-15 (Weiyi Wang)).

Verified when chrisflav/mathlib-staging was at: 7c17e37 — chore: bump mathlib to 9ef14c7 (#21) (2026-07-06 (github-actions[bot])).
You can reproduce this break by:

• updating the mathlib rev field in your lakefile to 79d0395a1825a6264ad5d269e35e60537518955e
• running lake update mathlib
• running lake build

Build failure log

✖ [1785/1787] Building MathlibStaging.Algebra.Category.ModuleCat.Sheaf.Annihilator (1.8s)
error: MathlibStaging/Algebra/Category/ModuleCat/Sheaf/Annihilator.lean:63:21: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  (ConcreteCategory.hom (?f ≫ ?g)) ?r
in the target expression
  (ConcreteCategory.hom (R.map f ≫ R.map g)) r • m = 0

C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
X Y : Cᵒᵖ
f : X ⟶ Y
r : ↑((unit R).obj X)
hr : r ∈ ⨅ Y, ⨅ f, Ideal.comap (RingCat.Hom.hom (R.map f)) (Module.annihilator ↑(R.obj Y) ↑(M.obj Y))
mem :
  ∀ {W : Cᵒᵖ} (s : ↑(R.obj W)),
    s ∈ ⨅ Z, ⨅ g, Ideal.comap (RingCat.Hom.hom (R.map g)) (Module.annihilator ↑(R.obj Z) ↑(M.obj Z)) ↔
      ∀ ⦃Z : Cᵒᵖ⦄ (g : W ⟶ Z) (m : ↑(M.obj Z)), (ConcreteCategory.hom (R.map g)) s • m = 0
Z : Cᵒᵖ
g : Y ⟶ Z
m : ↑(M.obj Z)
h : (ConcreteCategory.hom (R.map f ≫ R.map g)) r • m = 0
⊢ (ConcreteCategory.hom (R.map g)) ((ConcreteCategory.hom ((unit R).map f)) r) • m = 0

Note: The target expression is not type-correct under the `implicit` transparency level, which may have triggered the failure. This is usually caused by unfolding of semireducible definitions in prior tactic steps. Use `set_option linter.tacticCheckInstances true` to investigate the source of the issue.
Full error:
  Application type mismatch: The argument
    r
  has type
    ↑((unit R).obj X)
  but is expected to have type
    ↑(R.obj X)
  in the application
    (ConcreteCategory.hom (R.map f ≫ R.map g)) r
error: MathlibStaging/Algebra/Category/ModuleCat/Sheaf/Annihilator.lean:49:18: (kernel) declaration has metavariables 'PresheafOfModules.annihilator'
error: MathlibStaging/Algebra/Category/ModuleCat/Sheaf/Annihilator.lean:66:6: (kernel) declaration type mismatch, 'PresheafOfModules.annihilator_obj' has type
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
but it is expected to have type
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
error: MathlibStaging/Algebra/Category/ModuleCat/Sheaf/Annihilator.lean:73:6: (kernel) declaration type mismatch, 'PresheafOfModules.mem_annihilator' has type
  ∀ {C : Type u₁} [inst : Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R}
    {X : Cᵒᵖ} (r : ↑((unit R).obj X)),
    r ∈ ⨅ Y, ⨅ f, Ideal.comap (RingCat.Hom.hom (R.map f)) (Module.annihilator ↑(R.obj Y) ↑(M.obj Y)) ↔
      ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (m : ↑(M.obj Y)), (ConcreteCategory.hom (R.map f)) r • m = 0
but it is expected to have type
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
error: MathlibStaging/Algebra/Category/ModuleCat/Sheaf/Annihilator.lean:136:36: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  (ConcreteCategory.hom ?g) ((ConcreteCategory.hom ?f) ?r)
in the target expression
  (ConcreteCategory.hom (R.obj.map f.op)) ((ConcreteCategory.hom (R.obj.map φ)) s) •
      (ConcreteCategory.hom (M.val.map f.op)) m =
    0

C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
inst✝ : J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)
R : Sheaf J RingCat
M : SheafOfModules R
hsep : Presieve.IsSheaf J (M.val.presheaf ⋙ CategoryTheory.forget AddCommGrpCat)
X : Cᵒᵖ
s : ↑((unit R).val.obj X)
hmem : M.val.annihilator.toSubfunctor.sieveOfSection s ∈ J (unop X)
W : Cᵒᵖ
φ : X ⟶ W
m : ↑(M.val.obj W)
Y : C
f : Y ⟶ unop W
hf : (Sieve.pullback φ.unop (M.val.annihilator.toSubfunctor.sieveOfSection s)).arrows f
hcomp : (f ≫ φ.unop).op = φ ≫ f.op
key : (ConcreteCategory.hom (R.obj.map (φ ≫ f.op))) s ∈ M.val.annihilator.obj (op Y)
error: build failed
h0 : (ConcreteCategory.hom (R.obj.map (φ ≫ f.op))) s • (ConcreteCategory.hom (M.val.map f.op)) m = 0
⊢ (ConcreteCategory.hom (R.obj.map f.op)) ((ConcreteCategory.hom (R.obj.map φ)) s) •
      (ConcreteCategory.hom (M.val.map f.op)) m =
    0

Note: The target expression is not type-correct under the `implicit` transparency level, which may have triggered the failure. This is usually caused by unfolding of semireducible definitions in prior tactic steps. Use `set_option linter.tacticCheckInstances true` to investigate the source of the issue.
Full error:
  Application type mismatch: The argument
    s
  has type
    ↑((unit R).val.obj X)
  but is expected to have type
    ↑(R.obj.obj X)
  in the application
    (ConcreteCategory.hom (R.obj.map φ)) s
error: Lean exited with code 1
Some required targets logged failures:
- MathlibStaging.Algebra.Category.ModuleCat.Sheaf.Annihilator

Managed by hopscotch-action. This issue is updated automatically on each run and closed when the regression is resolved.