From ca0f40d71077582b1268dd611db2d71de50446a4 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sun, 6 Sep 2026 02:44:04 +0000
Subject: [PATCH] fix: mathlib4 monoidal structure on presheaves of modules
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

`downstream: update repo mathlib4` brought in mathlib master's refactor of
`Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean` onto the
`PresheafOfModulesOfCommRing R` abbreviation, whose `obj X` is a
`ModuleCat (R.obj X)` while the underlying `PresheafOfModules.Hom.app X` still
lands in `ModuleCat ((R ⋙ forget₂ CommRingCat RingCat).obj X)` — the same ring
bundled twice. Since `lean4#14624` an instance is only assigned when its type
matches the expected one at `.instances` transparency, and seeing that those two
agree needs `⋙` unfolded, which is `@[implicit_reducible]`; that is the gap the
file's own `#adaptation_note` already describes. So `apply` could no longer infer
`C` in six fields of the `monoidalCategory` instance:

    error: Tactic `apply` failed: could not unify the conclusion of
    `@tensorHom_comp_tensorHom`
      (?f₁ ⊗ₘ ?f₂) ≫ (?g₁ ⊗ₘ ?g₂) = ?f₁ ≫ ?g₁ ⊗ₘ ?f₂ ≫ ?g₂
    with the goal
      ((x✝³ ⊗ₘ x✝²) ≫ (x✝¹ ⊗ₘ x✝)).app X✝ = (x✝³ ≫ x✝¹ ⊗ₘ x✝² ≫ x✝).app X✝

and the resulting instance-with-metavariables took `symmetricCategory`, the
`braiding_*_app` lemmas and the two `PreservesColimitsOfSize` instances with it.

Pass `C` explicitly, as the same instance already does for `whiskerLeft_id` and
`id_whiskerRight`, which upstream needed for the same reason. Attribution
checked, not guessed: `set_option
backward.isDefEq.respectTransparency.instanceSearchTypes false` alone makes the
unmodified file compile, while `backward.isDefEq.respectTransparency` and
`backward.isDefEq.respectTransparency.types` do not.

Verified: `lake build Mathlib Archive Counterexamples Wanted --wfail`,
`lake test --iofail` and `lake lint`.
---
 .../Category/ModuleCat/Presheaf/Monoidal.lean | 24 ++++++++++++++-----
 1 file changed, 18 insertions(+), 6 deletions(-)

diff --git a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean
index 21055447c..7fc429472 100644
--- a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean
+++ b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean
@@ -150,18 +150,30 @@ noncomputable instance monoidalCategory :
     MonoidalCategory (PresheafOfModulesOfCommRing.{u} R) where
   tensorHom_def _ _ := by ext1; apply tensorHom_def
   id_tensorHom_id _ _ := by ext1; apply id_tensorHom_id
-  tensorHom_comp_tensorHom _ _ _ _ := by ext1; apply tensorHom_comp_tensorHom
+  tensorHom_comp_tensorHom _ _ _ _ := by
+    ext1 X
+    apply MonoidalCategory.tensorHom_comp_tensorHom (C := ModuleCat (R.obj X))
   whiskerLeft_id M₁ M₂ := by
     ext1 X
     apply MonoidalCategory.whiskerLeft_id (C := ModuleCat (R.obj X))
   id_whiskerRight _ _ := by
     ext1 X
     apply MonoidalCategory.id_whiskerRight (C := ModuleCat (R.obj X))
-  associator_naturality _ _ _ := by ext1; apply associator_naturality
-  leftUnitor_naturality _ := by ext1; apply leftUnitor_naturality
-  rightUnitor_naturality _ := by ext1; apply rightUnitor_naturality
-  pentagon _ _ _ _ := by ext1; apply pentagon
-  triangle _ _ := by ext1; apply triangle
+  associator_naturality _ _ _ := by
+    ext1 X
+    apply MonoidalCategory.associator_naturality (C := ModuleCat (R.obj X))
+  leftUnitor_naturality _ := by
+    ext1 X
+    apply MonoidalCategory.leftUnitor_naturality (C := ModuleCat (R.obj X))
+  rightUnitor_naturality _ := by
+    ext1 X
+    apply MonoidalCategory.rightUnitor_naturality (C := ModuleCat (R.obj X))
+  pentagon _ _ _ _ := by
+    ext1 X
+    apply MonoidalCategory.pentagon (C := ModuleCat (R.obj X))
+  triangle _ _ := by
+    ext1 X
+    apply MonoidalCategory.triangle (C := ModuleCat (R.obj X))
 
 open BraidedCategory