Bumping mathlib to 79d0395 would break the build

✖ [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)
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
error: build failed
    ↑((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