Trigger CI for leanprover-community/batteries#1099

Mathlib.lean

@@ -1962,6 +1962,7 @@ import Mathlib.CategoryTheory.Limits.Preserves.Grothendieck
 import Mathlib.CategoryTheory.Limits.Preserves.Limits
 import Mathlib.CategoryTheory.Limits.Preserves.Opposites
 import Mathlib.CategoryTheory.Limits.Preserves.Presheaf
+import Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
 import Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
 import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
 import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
@@ -2000,6 +2001,7 @@ import Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
 import Mathlib.CategoryTheory.Limits.Shapes.PiProd
 import Mathlib.CategoryTheory.Limits.Shapes.Preorder.Basic
 import Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
+import Mathlib.CategoryTheory.Limits.Shapes.Preorder.PrincipalSeg
 import Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
 import Mathlib.CategoryTheory.Limits.Shapes.Products
 import Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
@@ -3183,7 +3185,9 @@ import Mathlib.FieldTheory.Perfect
 import Mathlib.FieldTheory.PerfectClosure
 import Mathlib.FieldTheory.PolynomialGaloisGroup
 import Mathlib.FieldTheory.PrimitiveElement
-import Mathlib.FieldTheory.PurelyInseparable
+import Mathlib.FieldTheory.PurelyInseparable.Basic
+import Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
+import Mathlib.FieldTheory.PurelyInseparable.Tower
 import Mathlib.FieldTheory.RatFunc.AsPolynomial
 import Mathlib.FieldTheory.RatFunc.Basic
 import Mathlib.FieldTheory.RatFunc.Defs
@@ -4245,6 +4249,7 @@ import Mathlib.Order.Filter.Ultrafilter.Defs
 import Mathlib.Order.Filter.ZeroAndBoundedAtFilter
 import Mathlib.Order.Fin.Basic
 import Mathlib.Order.Fin.Finset
+import Mathlib.Order.Fin.SuccAboveOrderIso
 import Mathlib.Order.Fin.Tuple
 import Mathlib.Order.FixedPoints
 import Mathlib.Order.GaloisConnection.Basic
@@ -4276,6 +4281,7 @@ import Mathlib.Order.Interval.Set.Defs
 import Mathlib.Order.Interval.Set.Disjoint
 import Mathlib.Order.Interval.Set.Image
 import Mathlib.Order.Interval.Set.Infinite
+import Mathlib.Order.Interval.Set.InitialSeg
 import Mathlib.Order.Interval.Set.IsoIoo
 import Mathlib.Order.Interval.Set.Monotone
 import Mathlib.Order.Interval.Set.OrdConnected
@@ -4592,6 +4598,7 @@ import Mathlib.RingTheory.Ideal.Prime
 import Mathlib.RingTheory.Ideal.Prod
 import Mathlib.RingTheory.Ideal.Quotient.Basic
 import Mathlib.RingTheory.Ideal.Quotient.Defs
+import Mathlib.RingTheory.Ideal.Quotient.Index
 import Mathlib.RingTheory.Ideal.Quotient.Nilpotent
 import Mathlib.RingTheory.Ideal.Quotient.Noetherian
 import Mathlib.RingTheory.Ideal.Quotient.Operations
@@ -4961,6 +4968,7 @@ import Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
 import Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
 import Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
 import Mathlib.Tactic.CategoryTheory.BicategoryCoherence
+import Mathlib.Tactic.CategoryTheory.CheckCompositions
 import Mathlib.Tactic.CategoryTheory.Coherence
 import Mathlib.Tactic.CategoryTheory.Coherence.Basic
 import Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
@@ -5280,6 +5288,7 @@ import Mathlib.Topology.Algebra.Order.Field
 import Mathlib.Topology.Algebra.Order.Floor
 import Mathlib.Topology.Algebra.Order.Group
 import Mathlib.Topology.Algebra.Order.LiminfLimsup
+import Mathlib.Topology.Algebra.Order.Support
 import Mathlib.Topology.Algebra.Order.UpperLower
 import Mathlib.Topology.Algebra.Polynomial
 import Mathlib.Topology.Algebra.PontryaginDual

Mathlib/Algebra/Algebra/Basic.lean

@@ -9,7 +9,6 @@ import Mathlib.Algebra.Module.Equiv.Basic
 import Mathlib.Algebra.Module.Submodule.Ker
 import Mathlib.Algebra.Module.Submodule.RestrictScalars
 import Mathlib.Algebra.Module.ULift
-import Mathlib.Algebra.NoZeroSMulDivisors.Basic
 import Mathlib.Algebra.Ring.Subring.Basic
 import Mathlib.Data.Nat.Cast.Order.Basic
 import Mathlib.Data.Int.CharZero
@@ -22,6 +21,8 @@ This file could usefully be split further.
 
 universe u v w u₁ v₁
 
+open Function
+
 namespace Algebra
 
 variable {R : Type u} {A : Type w}
@@ -243,6 +244,11 @@ instance (priority := 99) Semiring.toNatAlgebra : Algebra ℕ R where
 instance nat_algebra_subsingleton : Subsingleton (Algebra ℕ R) :=
   ⟨fun P Q => by ext; simp⟩
 
+@[simp]
+lemma algebraMap_comp_natCast (R A : Type*) [CommSemiring R] [Semiring A] [Algebra R A] :
+    algebraMap R A ∘ Nat.cast = Nat.cast := by
+  ext; simp
+
 end Nat
 
 section Int
@@ -268,59 +274,105 @@ variable {R}
 instance int_algebra_subsingleton : Subsingleton (Algebra ℤ R) :=
   ⟨fun P Q => Algebra.algebra_ext P Q <| RingHom.congr_fun <| Subsingleton.elim _ _⟩
 
+@[simp]
+lemma algebraMap_comp_intCast (R A : Type*) [CommRing R] [Ring A] [Algebra R A] :
+    algebraMap R A ∘ Int.cast = Int.cast := by
+  ext; simp
+
 end Int
 
-namespace NoZeroSMulDivisors
+section FaithfulSMul
 
-variable {R A : Type*}
+instance (R : Type*) [NonAssocSemiring R] : FaithfulSMul R R := ⟨fun {r₁ r₂} h ↦ by simpa using h 1⟩
 
-open Algebra
+variable (R A : Type*) [CommSemiring R] [Semiring A]
 
-/-- If `algebraMap R A` is injective and `A` has no zero divisors,
-`R`-multiples in `A` are zero only if one of the factors is zero.
+lemma faithfulSMul_iff_injective_smul_one [Module R A] [IsScalarTower R A A] :
+    FaithfulSMul R A ↔ Injective (fun r : R ↦ r • (1 : A)) := by
+  refine ⟨fun ⟨h⟩ {r₁ r₂} hr ↦ h fun a ↦ ?_, fun h ↦ ⟨fun {r₁ r₂} hr ↦ h ?_⟩⟩
+  · simp only at hr
+    rw [← one_mul a, ← smul_mul_assoc, ← smul_mul_assoc, hr]
+  · simpa using hr 1
 
-Cannot be an instance because there is no `Injective (algebraMap R A)` typeclass.
--/
-theorem of_algebraMap_injective [CommSemiring R] [Semiring A] [Algebra R A] [NoZeroDivisors A]
-    (h : Function.Injective (algebraMap R A)) : NoZeroSMulDivisors R A :=
-  ⟨fun hcx => (mul_eq_zero.mp ((smul_def _ _).symm.trans hcx)).imp_left
-    (map_eq_zero_iff (algebraMap R A) h).mp⟩
+variable [Algebra R A]
+
+lemma faithfulSMul_iff_algebraMap_injective : FaithfulSMul R A ↔ Injective (algebraMap R A) := by
+  rw [faithfulSMul_iff_injective_smul_one, Algebra.algebraMap_eq_smul_one']
+
+variable [FaithfulSMul R A]
 
-variable (R A)
+namespace FaithfulSMul
 
-theorem algebraMap_injective [CommRing R] [Ring A] [Nontrivial A] [Algebra R A]
-    [NoZeroSMulDivisors R A] : Function.Injective (algebraMap R A) := by
-  simpa only [algebraMap_eq_smul_one'] using smul_left_injective R one_ne_zero
+lemma algebraMap_injective : Injective (algebraMap R A) :=
+  (faithfulSMul_iff_algebraMap_injective R A).mp inferInstance
+
+@[deprecated (since := "2025-01-31")]
+alias _root_.NoZeroSMulDivisors.algebraMap_injective := algebraMap_injective
 
 @[simp]
-lemma algebraMap_eq_zero_iff [CommRing R] [Ring A] [Nontrivial A] [Algebra R A]
-    [NoZeroSMulDivisors R A] {r : R} : algebraMap R A r = 0 ↔ r = 0 :=
-  map_eq_zero_iff _ <| algebraMap_injective R A
+lemma algebraMap_eq_zero_iff {r : R} : algebraMap R A r = 0 ↔ r = 0 :=
+  map_eq_zero_iff (algebraMap R A) <| algebraMap_injective R A
+
+@[deprecated (since := "2025-01-31")]
+alias _root_.NoZeroSMulDivisors.algebraMap_eq_zero_iff := algebraMap_eq_zero_iff
 
 @[simp]
-lemma algebraMap_eq_one_iff [CommRing R] [Ring A] [Nontrivial A] [Algebra R A]
-    [NoZeroSMulDivisors R A] {r : R} : algebraMap R A r = 1 ↔ r = 1 :=
-  map_eq_one_iff _ <| algebraMap_injective R A
+lemma algebraMap_eq_one_iff {r : R} : algebraMap R A r = 1 ↔ r = 1 :=
+  map_eq_one_iff _ <| FaithfulSMul.algebraMap_injective R A
+
+@[deprecated (since := "2025-01-31")]
+alias _root_.NoZeroSMulDivisors.algebraMap_eq_one_iff := algebraMap_eq_one_iff
 
-theorem _root_.NeZero.of_noZeroSMulDivisors (n : ℕ) [CommRing R] [NeZero (n : R)] [Ring A]
-    [Nontrivial A] [Algebra R A] [NoZeroSMulDivisors R A] : NeZero (n : A) :=
-  NeZero.nat_of_injective <| NoZeroSMulDivisors.algebraMap_injective R A
+theorem _root_.NeZero.of_faithfulSMul (n : ℕ) [NeZero (n : R)] :
+    NeZero (n : A) :=
+  NeZero.nat_of_injective <| FaithfulSMul.algebraMap_injective R A
 
-variable {R A}
+@[deprecated (since := "2025-01-31")]
+alias _root_.NeZero.of_noZeroSMulDivisors := NeZero.of_faithfulSMul
 
-theorem iff_algebraMap_injective [CommRing R] [Ring A] [IsDomain A] [Algebra R A] :
-    NoZeroSMulDivisors R A ↔ Function.Injective (algebraMap R A) :=
-  ⟨@NoZeroSMulDivisors.algebraMap_injective R A _ _ _ _, NoZeroSMulDivisors.of_algebraMap_injective⟩
+end FaithfulSMul
+
+lemma Algebra.charZero_of_charZero [CharZero R] : CharZero A :=
+  have := algebraMap_comp_natCast R A
+  ⟨this ▸ (FaithfulSMul.algebraMap_injective R A).comp CharZero.cast_injective⟩
 
 -- see note [lower instance priority]
-instance (priority := 100) CharZero.noZeroSMulDivisors_nat [Semiring R] [NoZeroDivisors R]
-    [CharZero R] : NoZeroSMulDivisors ℕ R :=
-  NoZeroSMulDivisors.of_algebraMap_injective <| (algebraMap ℕ R).injective_nat
+instance (priority := 100) [CharZero R] : FaithfulSMul ℕ R := by
+  simpa only [faithfulSMul_iff_algebraMap_injective] using (algebraMap ℕ R).injective_nat
 
 -- see note [lower instance priority]
-instance (priority := 100) CharZero.noZeroSMulDivisors_int [Ring R] [NoZeroDivisors R]
-    [CharZero R] : NoZeroSMulDivisors ℤ R :=
-  NoZeroSMulDivisors.of_algebraMap_injective <| (algebraMap ℤ R).injective_int
+instance (priority := 100) (R : Type*) [Ring R] [CharZero R] : FaithfulSMul ℤ R := by
+  simpa only [faithfulSMul_iff_algebraMap_injective] using (algebraMap ℤ R).injective_int
+
+end FaithfulSMul
+
+namespace NoZeroSMulDivisors
+
+-- see Note [lower instance priority]
+instance (priority := 100) instOfFaithfulSMul {R A : Type*}
+    [CommSemiring R] [Semiring A] [Algebra R A] [NoZeroDivisors A] [FaithfulSMul R A] :
+    NoZeroSMulDivisors R A :=
+  ⟨fun hcx => (mul_eq_zero.mp ((Algebra.smul_def _ _).symm.trans hcx)).imp_left
+    (map_eq_zero_iff (algebraMap R A) <| FaithfulSMul.algebraMap_injective R A).mp⟩
+
+@[deprecated (since := "2025-01-31")]
+alias of_algebraMap_injective := instOfFaithfulSMul
+
+variable {R A : Type*} [CommRing R] [Ring A] [Algebra R A]
+
+instance [Nontrivial A] [NoZeroSMulDivisors R A] : FaithfulSMul R A where
+  eq_of_smul_eq_smul {r₁ r₂} h := by
+    specialize h 1
+    rw [← sub_eq_zero, ← sub_smul, smul_eq_zero, sub_eq_zero] at h
+    exact h.resolve_right one_ne_zero
+
+theorem iff_faithfulSMul [IsDomain A] : NoZeroSMulDivisors R A ↔ FaithfulSMul R A :=
+  ⟨fun _ ↦ inferInstance, fun _ ↦ inferInstance⟩
+
+theorem iff_algebraMap_injective [IsDomain A] :
+    NoZeroSMulDivisors R A ↔ Injective (algebraMap R A) := by
+  rw [iff_faithfulSMul]
+  exact faithfulSMul_iff_algebraMap_injective R A
 
 end NoZeroSMulDivisors
 
@@ -338,20 +390,16 @@ theorem algebraMap_smul (r : R) (m : M) : (algebraMap R A) r • m = r • m :=
   (algebra_compatible_smul A r m).symm
 
 /-- If `M` is `A`-torsion free and `algebraMap R A` is injective, `M` is also `R`-torsion free. -/
-lemma NoZeroSMulDivisors.of_algebraMap_injective' {R A M : Type*} [CommSemiring R] [Semiring A]
-    [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M]
-    [NoZeroSMulDivisors A M] (h : Function.Injective (algebraMap R A)) :
-    NoZeroSMulDivisors R M where
+theorem NoZeroSMulDivisors.trans_faithfulSMul (R A M : Type*) [CommRing R] [Ring A] [Algebra R A]
+    [FaithfulSMul R A] [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M]
+    [NoZeroSMulDivisors A M] : NoZeroSMulDivisors R M where
   eq_zero_or_eq_zero_of_smul_eq_zero hx := by
     rw [← algebraMap_smul (A := A)] at hx
-    obtain (hc|hx) := eq_zero_or_eq_zero_of_smul_eq_zero hx
-    · exact Or.inl <| (map_eq_zero_iff _ h).mp hc
-    · exact Or.inr hx
+    simpa only [map_eq_zero_iff _ <| FaithfulSMul.algebraMap_injective R A] using
+      eq_zero_or_eq_zero_of_smul_eq_zero hx
 
-theorem NoZeroSMulDivisors.trans (R A M : Type*) [CommRing R] [Ring A] [IsDomain A] [Algebra R A]
-    [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] [NoZeroSMulDivisors R A]
-    [NoZeroSMulDivisors A M] : NoZeroSMulDivisors R M :=
-  of_algebraMap_injective' (A := A) (NoZeroSMulDivisors.iff_algebraMap_injective.1 inferInstance)
+@[deprecated (since := "2025-01-31")]
+alias NoZeroSMulDivisors.of_algebraMap_injective' := NoZeroSMulDivisors.trans_faithfulSMul
 
 variable {A}
 
@@ -443,15 +491,15 @@ variable {F E : Type*} [CommSemiring F] [Semiring E] [Algebra F E] (b : F →ₗ
 
 /-- If `E` is an `F`-algebra, and there exists an injective `F`-linear map from `F` to `E`,
 then the algebra map from `F` to `E` is also injective. -/
-theorem injective_algebraMap_of_linearMap (hb : Function.Injective b) :
-    Function.Injective (algebraMap F E) := fun x y e ↦ hb <| by
+theorem injective_algebraMap_of_linearMap (hb : Injective b) :
+    Injective (algebraMap F E) := fun x y e ↦ hb <| by
   rw [← mul_one x, ← mul_one y, ← smul_eq_mul, ← smul_eq_mul,
     map_smul, map_smul, Algebra.smul_def, Algebra.smul_def, e]
 
 /-- If `E` is an `F`-algebra, and there exists a surjective `F`-linear map from `F` to `E`,
 then the algebra map from `F` to `E` is also surjective. -/
-theorem surjective_algebraMap_of_linearMap (hb : Function.Surjective b) :
-    Function.Surjective (algebraMap F E) := fun x ↦ by
+theorem surjective_algebraMap_of_linearMap (hb : Surjective b) :
+    Surjective (algebraMap F E) := fun x ↦ by
   obtain ⟨x, rfl⟩ := hb x
   obtain ⟨y, hy⟩ := hb (b 1 * b 1)
   refine ⟨x * y, ?_⟩
@@ -467,14 +515,14 @@ then the algebra map from `F` to `E` is also bijective.
 NOTE: The same result can also be obtained if there are two `F`-linear maps from `F` to `E`,
 one is injective, the other one is surjective. In this case, use
 `injective_algebraMap_of_linearMap` and `surjective_algebraMap_of_linearMap` separately. -/
-theorem bijective_algebraMap_of_linearMap (hb : Function.Bijective b) :
-    Function.Bijective (algebraMap F E) :=
+theorem bijective_algebraMap_of_linearMap (hb : Bijective b) :
+    Bijective (algebraMap F E) :=
   ⟨injective_algebraMap_of_linearMap b hb.1, surjective_algebraMap_of_linearMap b hb.2⟩
 
 /-- If `E` is an `F`-algebra, there exists an `F`-linear isomorphism from `F` to `E` (namely,
 `E` is a free `F`-module of rank one), then the algebra map from `F` to `E` is bijective. -/
 theorem bijective_algebraMap_of_linearEquiv (b : F ≃ₗ[F] E) :
-    Function.Bijective (algebraMap F E) :=
+    Bijective (algebraMap F E) :=
   bijective_algebraMap_of_linearMap _ b.bijective
 
 end algebraMap
@@ -486,7 +534,7 @@ variable {M N} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module S M] [Is
 variable [Module R N] [Module S N] [IsScalarTower R S N]
 
 /-- If `R →+* S` is surjective, then `S`-linear maps between modules are exactly `R`-linear maps. -/
-def LinearMap.extendScalarsOfSurjectiveEquiv (h : Function.Surjective (algebraMap R S)) :
+def LinearMap.extendScalarsOfSurjectiveEquiv (h : Surjective (algebraMap R S)) :
     (M →ₗ[R] N) ≃ₗ[R] (M →ₗ[S] N) where
   toFun f := { __ := f, map_smul' := fun r x ↦ by obtain ⟨r, rfl⟩ := h r; simp }
   map_add' _ _ := rfl
@@ -496,17 +544,17 @@ def LinearMap.extendScalarsOfSurjectiveEquiv (h : Function.Surjective (algebraMa
   right_inv _ := rfl
 
 /-- If `R →+* S` is surjective, then `R`-linear maps are also `S`-linear. -/
-abbrev LinearMap.extendScalarsOfSurjective (h : Function.Surjective (algebraMap R S))
+abbrev LinearMap.extendScalarsOfSurjective (h : Surjective (algebraMap R S))
     (l : M →ₗ[R] N) : M →ₗ[S] N :=
   extendScalarsOfSurjectiveEquiv h l
 
 /-- If `R →+* S` is surjective, then `R`-linear isomorphisms are also `S`-linear. -/
-def LinearEquiv.extendScalarsOfSurjective (h : Function.Surjective (algebraMap R S))
+def LinearEquiv.extendScalarsOfSurjective (h : Surjective (algebraMap R S))
     (f : M ≃ₗ[R] N) : M ≃ₗ[S] N where
   __ := f
   map_smul' r x := by obtain ⟨r, rfl⟩ := h r; simp
 
-variable (h : Function.Surjective (algebraMap R S))
+variable (h : Surjective (algebraMap R S))
 
 @[simp]
 lemma LinearMap.extendScalarsOfSurjective_apply (l : M →ₗ[R] N) (x) :

Mathlib/Algebra/AlgebraicCard.lean

@@ -66,7 +66,7 @@ theorem cardinalMk_lift_of_infinite [Infinite R] :
     Cardinal.lift.{u} #{ x : A // IsAlgebraic R x } = Cardinal.lift.{v} #R :=
   ((cardinalMk_lift_le_max R A).trans_eq (max_eq_left <| aleph0_le_mk _)).antisymm <|
     lift_mk_le'.2 ⟨⟨fun x => ⟨algebraMap R A x, isAlgebraic_algebraMap _⟩, fun _ _ h =>
-      NoZeroSMulDivisors.algebraMap_injective R A (Subtype.ext_iff.1 h)⟩⟩
+      FaithfulSMul.algebraMap_injective R A (Subtype.ext_iff.1 h)⟩⟩
 
 @[deprecated (since := "2024-11-10")]
 alias cardinal_mk_lift_of_infinite := cardinalMk_lift_of_infinite

Mathlib/Algebra/BigOperators/Associated.lean

@@ -188,7 +188,7 @@ variable [CancelCommMonoidWithZero α]
 
 theorem exists_mem_multiset_le_of_prime {s : Multiset (Associates α)} {p : Associates α}
     (hp : Prime p) : p ≤ s.prod → ∃ a ∈ s, p ≤ a :=
-  Multiset.induction_on s (fun ⟨_, Eq⟩ => (hp.ne_one (mul_eq_one.1 Eq.symm).1).elim)
+  Multiset.induction_on s (fun ⟨_, eq⟩ => (hp.ne_one (mul_eq_one.1 eq.symm).1).elim)
     fun a s ih h =>
     have : p ≤ a * s.prod := by simpa using h
     match Prime.le_or_le hp this with

Mathlib/Algebra/Category/Grp/Ulift.lean

@@ -200,6 +200,7 @@ noncomputable instance : PreservesColimitsOfSize.{w', w} uliftFunctor.{v, u} whe
 The functor `uliftFunctor : AddCommGrp.{u} ⥤ AddCommGrp.{max u v}` creates `u`-small colimits.
 -/
 noncomputable instance : CreatesColimitsOfSize.{w, u} uliftFunctor.{v, u} where
-  CreatesColimitsOfShape := { CreatesColimit := fun {_} ↦ createsColimitOfFullyFaithfulOfPreserves }
+  CreatesColimitsOfShape :=
+    { CreatesColimit := fun {_} ↦ createsColimitOfReflectsIsomorphismsOfPreserves }
 
 end AddCommGrp

Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean

@@ -34,7 +34,7 @@ def monoidalClosedHomEquiv (M N P : ModuleCat.{u} R) :
     apply TensorProduct.ext'
     intro m n
     simp only [Hom.hom₂_ofHom₂, LinearMap.comp_apply, hom_comp, MonoidalCategory.tensorLeft_obj]
-    erw [MonoidalCategory.braiding_hom_apply, TensorProduct.lift.tmul]
+    erw [MonoidalCategory.braiding_hom_apply m n, TensorProduct.lift.tmul]
   right_inv _ := rfl
 
 instance : MonoidalClosed (ModuleCat.{u} R) where

Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafify.lean

@@ -32,8 +32,6 @@ namespace CategoryTheory
 
 namespace Presieve.FamilyOfElements
 
-attribute [local instance] HasForget.hasCoeToSort HasForget.instFunLike
-
 section smul
 
 variable {R : Cᵒᵖ ⥤ RingCat.{u}} {M : PresheafOfModules.{v} R} {X : C} {P : Presieve X}