fix

erdOne · erdOne · commit 34b2fa77888b · 2025-11-21T01:44:24.000+01:00
diff --git a/Mathlib/GroupTheory/DivisibleHull.lean b/Mathlib/GroupTheory/DivisibleHull.lean
@@ -182,11 +182,13 @@ theorem qsmul_def (a : ℚ) (x : DivisibleHull M) :
 theorem zero_qsmul (x : DivisibleHull M) : (0 : ℚ) • x = 0 := by
   simp [qsmul_def]
 
+attribute [local instance] LocalizedModule.moduleOfIsLocalization in
 theorem qsmul_of_nonneg {a : ℚ} (h : 0 ≤ a) (x : DivisibleHull M) :
     a • x = (show ℚ≥0 from ⟨a, h⟩) • x := by
   have := h.eq_or_lt
   aesop (add simp [qsmul_def, abs_of_pos])
 
+attribute [local instance] LocalizedModule.moduleOfIsLocalization in
 theorem qsmul_of_nonpos {a : ℚ} (h : a ≤ 0) (x : DivisibleHull M) :
     a • x = -((show ℚ≥0 from ⟨-a, Left.nonneg_neg_iff.mpr h⟩) • x) := by
   have := h.eq_or_lt
@@ -205,6 +207,7 @@ theorem qsmul_mk (a : ℚ) (m : M) (s : ℕ+) :
       simpa using h
     simp [nnqsmul_mk, this, ← neg_mk]
 
+attribute [local instance] LocalizedModule.moduleOfIsLocalization in
 noncomputable
 instance : Module ℚ (DivisibleHull M) where
   one_smul x := by
@@ -326,6 +329,7 @@ end LinearOrder
 section OrderedGroup
 variable {M : Type*} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M]
 
+attribute [local instance] LocalizedModule.moduleOfIsLocalization in
 instance : IsStrictOrderedModule ℚ (DivisibleHull M) where
   smul_lt_smul_of_pos_left a ha b c h := by
     simp_rw [qsmul_of_nonneg ha.le]
diff --git a/Mathlib/RingTheory/Localization/BaseChange.lean b/Mathlib/RingTheory/Localization/BaseChange.lean
@@ -46,6 +46,7 @@ given by `m/s ↦ (1/s) ⊗ₜ m`.
 -/
 theorem isLocalizedModule_iff_isBaseChange : IsLocalizedModule S f ↔ IsBaseChange A f := by
   refine ⟨fun _ ↦ IsLocalizedModule.isBaseChange S A f, fun h ↦ ?_⟩
+  letI : Module A (LocalizedModule S M) := LocalizedModule.moduleOfIsLocalization ..
   have : IsBaseChange A (LocalizedModule.mkLinearMap S M) := IsLocalizedModule.isBaseChange S A _
   let e := (this.equiv.symm.trans h.equiv).restrictScalars R
   convert IsLocalizedModule.of_linearEquiv S (LocalizedModule.mkLinearMap S M) e
