chore: remove unused instances (#41013)

thorimur · thorimur · commit f8fd74f95c7a · 2026-06-25T07:54:34.000Z
Removes unused instances in theorems found by fixing the unused arguments linter to handle theorems in leanprover-community/batteries#1879.
diff --git a/Mathlib/Algebra/Module/Submodule/Map.lean b/Mathlib/Algebra/Module/Submodule/Map.lean
@@ -697,8 +697,8 @@ theorem map_restrict [RingHomSurjective σ₂₁] {p : Submodule R₂ M₂} {q :
     map (f.restrict h) p' = comap q.subtype (map f (map p.subtype p')) := by
   rw [restrict_eq_codRestrict_domRestrict, map_codRestrict, map_domRestrict]
 
-theorem comap_restrict [RingHomSurjective σ₂₁] {p : Submodule R₂ M₂} {q : Submodule R M}
-    {f : M₂ →ₛₗ[σ₂₁] M} (h : ∀ x ∈ p, f x ∈ q) (p') :
+theorem comap_restrict {p : Submodule R₂ M₂} {q : Submodule R M} {f : M₂ →ₛₗ[σ₂₁] M}
+    (h : ∀ x ∈ p, f x ∈ q) (p') :
     comap (f.restrict h) p' = comap p.subtype (comap f (map q.subtype p')) := by
   rw [restrict_eq_codRestrict_domRestrict, comap_codRestrict, comap_domRestrict]
 
diff --git a/Mathlib/Algebra/Module/Submodule/RestrictScalars.lean b/Mathlib/Algebra/Module/Submodule/RestrictScalars.lean
@@ -56,7 +56,7 @@ theorem restrictScalars_self (V : Submodule R M) : V.restrictScalars R = V :=
   SetLike.coe_injective rfl
 
 @[simp] theorem restrictScalars_restrictScalars
-    (T : Type*) [Semiring T] [SMul T R] [SMul S T] [IsScalarTower S T R]
+    (T : Type*) [Semiring T] [SMul T R] [SMul S T]
     [Module T M] [IsScalarTower S T M] [IsScalarTower T R M]
     (V : Submodule R M) :
     (V.restrictScalars T).restrictScalars S = V.restrictScalars S :=
diff --git a/Mathlib/Algebra/Module/Torsion/Basic.lean b/Mathlib/Algebra/Module/Torsion/Basic.lean
@@ -577,7 +577,7 @@ theorem IsTorsionBy.mk_smul [(Ideal.span {r}).IsTwoSided] (hM : IsTorsionBy R M
 def IsTorsionBySet.module [I.IsTwoSided] (hM : IsTorsionBySet R M I) : Module (R ⧸ I) M :=
   letI := hM.hasSMul; fast_instance% I.mkQ_surjective.moduleLeft _ (IsTorsionBySet.mk_smul hM)
 
-instance IsTorsionBySet.isScalarTower [I.IsTwoSided] (hM : IsTorsionBySet R M I)
+instance IsTorsionBySet.isScalarTower (hM : IsTorsionBySet R M I)
     {S : Type*} [SMul S R] [SMul S M] [IsScalarTower S R M] [IsScalarTower S R R] :
     @IsScalarTower S (R ⧸ I) M _ hM.hasSMul _ :=
   -- Porting note: still needed to be fed the Module R / I M instance
diff --git a/Mathlib/Algebra/Order/Ring/IsNonarchimedean.lean b/Mathlib/Algebra/Order/Ring/IsNonarchimedean.lean
@@ -118,7 +118,7 @@ theorem add_eq_max_of_ne {F α : Type*} [AddGroup α] [FunLike F α R]
 /- TODO: Remove the funlike conditions on the lemmas required for add_max_of_ne, this will allow us
   to remove the CommGroup part in the below which is unnecessary. -/
 
-lemma add_eq_max_of_ne' {α S : Type*} [Semiring S] [LinearOrder S] [AddCommGroup α]
+lemma add_eq_max_of_ne' {α S : Type*} [LinearOrder S] [AddCommGroup α]
     (f : α → S) (fna : IsNonarchimedean f) (Neg : ∀ a, f a = f (-a)) {a b : α}
     (hne : f a ≠ f b) : f (a + b) = max (f a) (f b) := by
   wlog hab : f a > f b generalizing a b with H
@@ -223,6 +223,7 @@ theorem finset_powerset_image_add [IsStrictOrderedRing R]
     g (powersetCard (s.card - m) s)
   exact ⟨⟨b, hb_in (powersetCard_nonempty.mpr (Nat.sub_le s.card m))⟩, hb⟩
 
+omit [Semiring R] in
 lemma apply_sum_eq_of_lt {α β : Type*} [AddCommGroup α] {f : α → R} (fna : IsNonarchimedean f)
     (f_neg : ∀ a, f a = f (-a)) {s : Finset β} {l : β → α} {k : β} (hk : k ∈ s)
     (hmax : ∀ j ∈ s, j ≠ k → f (l j) < f (l k)) : f (∑ i ∈ s, l i) = f (l k) := by
diff --git a/Mathlib/Algebra/SkewPolynomial/Basic.lean b/Mathlib/Algebra/SkewPolynomial/Basic.lean
@@ -173,8 +173,7 @@ def monomial : R →ₗ[R] SkewPolynomial R := lsingle R (ofAdd n)
 
 lemma monomial_zero_right : monomial n (0 : R) = 0 := single_zero _
 
-lemma monomial_zero_one [MulSemiringAction (Multiplicative ℕ) R] : monomial 0 (1 : R) = 1 :=
-  rfl
+lemma monomial_zero_one : monomial 0 (1 : R) = 1 := rfl
 
 lemma monomial_def (a : R) : monomial n a = single (ofAdd n) a := rfl
 
@@ -348,8 +347,7 @@ lemma coeff_monomial : coeff (monomial n a) m = if n = m then a else 0 :=
 
 @[simp] lemma coeff_zero (n : ℕ) : coeff (0 : SkewPolynomial R) n = 0 := rfl
 
-@[simp] lemma coeff_one_zero [MulSemiringAction (Multiplicative ℕ) R] :
-    coeff (1 : SkewPolynomial R) 0 = 1 := coeff_monomial
+@[simp] lemma coeff_one_zero : coeff (1 : SkewPolynomial R) 0 = 1 := coeff_monomial
 
 lemma coeff_one [MulSemiringAction (Multiplicative ℕ) R] (n : ℕ) :
     coeff (1 : SkewPolynomial R) n = if 0 = n then 1 else 0 := by
diff --git a/Mathlib/AlgebraicGeometry/Morphisms/Finite.lean b/Mathlib/AlgebraicGeometry/Morphisms/Finite.lean
@@ -154,8 +154,7 @@ instance {U V X : Scheme.{u}} (f : U ⟶ X) (g : V ⟶ X) [IsFinite f] [IsFinite
 
 end IsFinite
 
-lemma Scheme.Hom.finite_appTop {X Y : Scheme.{u}} (f : X ⟶ Y) [IsAffine X] [IsAffine Y]
-    [IsFinite f] :
+lemma Scheme.Hom.finite_appTop {X Y : Scheme.{u}} (f : X ⟶ Y) [IsAffine Y] [IsFinite f] :
     f.appTop.hom.Finite :=
   (HasAffineProperty.iff_of_isAffine (P := @IsFinite).mp inferInstance).2
 
diff --git a/Mathlib/Analysis/LocallyConvex/HahnBanach.lean b/Mathlib/Analysis/LocallyConvex/HahnBanach.lean
@@ -68,8 +68,8 @@ variable [TopologicalSpace E]
 
 /-- **Hahn-Banach theorem** for linear functionals dominated by a continuous seminorm on
 polynormable spaces over `ℝ`. -/
-theorem Module.Dual.exists_continuous_extension_of_le_seminorm_real [IsTopologicalAddGroup E]
-    [Module ℝ E] [ContinuousSMul ℝ E] [PolynormableSpace ℝ E] (S : Subspace ℝ E) (f : Dual ℝ S)
+theorem Module.Dual.exists_continuous_extension_of_le_seminorm_real
+    [Module ℝ E] [PolynormableSpace ℝ E] (S : Subspace ℝ E) (f : Dual ℝ S)
     {p : Seminorm ℝ E} (hp_cont : Continuous p) (hp : ∀ x, f x ≤ p x) :
     ∃ g : StrongDual ℝ E, (∀ x : S, g x = f x) ∧ ∀ x, |g x| ≤ p x := by
   obtain ⟨g, hg, hl⟩ := f.exists_extension_of_le_seminorm_real S hp
diff --git a/Mathlib/Analysis/Normed/Operator/NormedSpace.lean b/Mathlib/Analysis/Normed/Operator/NormedSpace.lean
@@ -438,7 +438,7 @@ lemma ContinuousLinearMap.norm_inl [SeminormedAddCommGroup E] [NontrivialTopolog
     ‖ContinuousLinearMap.inl 𝕜 E F‖ = 1 :=
   (LinearIsometry.inl 𝕜 E F).norm_toContinuousLinearMap
 
-lemma ContinuousLinearMap.norm_inr [SeminormedAddCommGroup E] [NontrivialTopology E]
+lemma ContinuousLinearMap.norm_inr [SeminormedAddCommGroup E]
     [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [NontrivialTopology F] :
     ‖ContinuousLinearMap.inr 𝕜 E F‖ = 1 :=
   (LinearIsometry.inr 𝕜 E F).norm_toContinuousLinearMap
diff --git a/Mathlib/Analysis/Seminorm.lean b/Mathlib/Analysis/Seminorm.lean
@@ -1175,7 +1175,7 @@ theorem continuous_of_le [TopologicalSpace E] [IsTopologicalAddGroup E]
   exact isOpen_lt hq continuous_const
 
 /-- The sum over a finite set of continuous seminorms is continuous. -/
-theorem continuous_finsetSum [TopologicalSpace E] [IsTopologicalAddGroup E]
+theorem continuous_finsetSum [TopologicalSpace E]
     {p : ι → Seminorm 𝕝 E} {s : Finset ι} (hp : ∀ i ∈ s, Continuous (p i)) :
     Continuous ((∑ i ∈ s, p i : Seminorm 𝕝 E) : E → ℝ) := by
   change Continuous (fun x ↦ coeFnAddMonoidHom _ _ (∑ i ∈ s, p i) x)
diff --git a/Mathlib/CategoryTheory/LiftingProperties/PushoutProduct.lean b/Mathlib/CategoryTheory/LiftingProperties/PushoutProduct.lean
@@ -68,7 +68,7 @@ lemma hasLiftingProperty_mk_iff' [HasPushouts C] [HasPullbacks C]
 
 set_option backward.defeqAttrib.useBackward true in
 /-- `(∅ ⟶ B) □ g` lifts against `X ⟶ Y` if and only if `g` lifts against `B ⟹ X ⟶ B ⟹ Y`. -/
-lemma hasLiftingProperty_mk_isInitial_iff [HasPushouts C] [HasPullbacks C]
+lemma hasLiftingProperty_mk_isInitial_iff [HasPushouts C]
     [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C]
     {A B K L X Y : C} {g : K ⟶ L} {h : X ⟶ Y}
     (i : IsInitial A) :
@@ -80,7 +80,7 @@ lemma hasLiftingProperty_mk_isInitial_iff [HasPushouts C] [HasPullbacks C]
   exact Adjunction.hasLiftingProperty_iff (ihom.adjunction B) g h
 
 /-- `f □ (∅ ⟶ L)` lifts against `X ⟶ Y` if and only if `f` lifts against `L ⟹ X ⟶ L ⟹ Y`. -/
-lemma hasLiftingProperty_mk_isInitial_iff' [HasPushouts C] [HasPullbacks C]
+lemma hasLiftingProperty_mk_isInitial_iff' [HasPushouts C]
     [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C]
     {A B K L X Y : C} {f : A ⟶ B} {h : X ⟶ Y}
     (i : IsInitial K) :
@@ -100,7 +100,7 @@ lemma hasLiftingProperty_mk_isTerminal_iff [HasPushouts C] [HasPullbacks C]
   exact HasLiftingProperty.iff_of_arrow_iso_right g (PullbackHom.isTerminalIso _ t)
 
 /-- `(∅ ⟶ B) □ g` lifts against `X ⟶ ⋆` if and only if `g` lifts against `(B ⟹ X) ⟶ ⋆`. -/
-lemma hasLiftingProperty_mk_isInitial_isTerminal_iff [HasPushouts C] [HasPullbacks C]
+lemma hasLiftingProperty_mk_isInitial_isTerminal_iff [HasPushouts C]
     [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C]
     {A B K L X Y : C} {g : K ⟶ L}
     (i : IsInitial A) (t : IsTerminal Y) :
@@ -112,7 +112,7 @@ lemma hasLiftingProperty_mk_isInitial_isTerminal_iff [HasPushouts C] [HasPullbac
       (t.hom_ext _ _))
 
 /-- `f □ (∅ ⟶ L)` lifts against `X ⟶ ⋆` if and only if `f` lifts against `(L ⟹ X) ⟶ ⋆`. -/
-lemma hasLiftingProperty_mk_isInitial_isTerminal_iff' [HasPushouts C] [HasPullbacks C]
+lemma hasLiftingProperty_mk_isInitial_isTerminal_iff' [HasPushouts C]
     [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C]
     {A B K L X Y : C} {f : A ⟶ B}
     (i : IsInitial K) (t : IsTerminal Y) :
diff --git a/Mathlib/FieldTheory/Galois/Basic.lean b/Mathlib/FieldTheory/Galois/Basic.lean
@@ -181,7 +181,7 @@ instance isGalois_bot : IsGalois F (⊥ : IntermediateField F E) :=
   (IntermediateField.botEquiv F E).transfer_galois.mpr (IsGalois.self F)
 
 theorem IsGalois.of_equiv_equiv {M N : Type*} [Field N] [Field M] [Algebra M N]
-    [Algebra.IsAlgebraic F E] [h : IsGalois F E] {f : F ≃+* M} {g : E ≃+* N}
+    [h : IsGalois F E] {f : F ≃+* M} {g : E ≃+* N}
     (hcomp : (algebraMap M N).comp f = (g : E →+* N).comp (algebraMap F E)) :
     IsGalois M N :=
   isGalois_iff.mpr ⟨Algebra.IsSeparable.of_equiv_equiv f g hcomp, Normal.of_equiv_equiv hcomp⟩
diff --git a/Mathlib/FieldTheory/Galois/IsGaloisGroup.lean b/Mathlib/FieldTheory/Galois/IsGaloisGroup.lean
@@ -317,7 +317,7 @@ theorem fixedPoints_fixingSubgroup [Finite G] :
 
 /-- If `G` acts as a Galois group on `L/K` and the subgroup `H` acts as a Galois group on `L/B`,
 then the fixed points of `H` equals the range of `algebraMap B L`. -/
-theorem fixedPoints_eq_range_algebraMap [Finite G] (B : Type*)
+theorem fixedPoints_eq_range_algebraMap (B : Type*)
     [CommSemiring B] [Algebra B L] [IsGaloisGroup H B L] :
     (FixedPoints.intermediateField H : IntermediateField K L) = Set.range (algebraMap B L) := by
   ext
diff --git a/Mathlib/Geometry/Manifold/Algebra/SMul.lean b/Mathlib/Geometry/Manifold/Algebra/SMul.lean
@@ -173,8 +173,7 @@ instance {n : ℕ∞ω} : ContMDiffSMul 𝓘(𝕜) 𝓘(𝕜, E) n 𝕜 E where
     exact contDiff_smul.contMDiff.comp h
 
 /-- The monoid `E →L[𝕜] E` of continuous linear endomorphisms of `E` acts smoothly on `E`. -/
-instance [CompleteSpace E] {n : ℕ∞ω} :
-    ContMDiffSMul 𝓘(𝕜, E →L[𝕜] E) 𝓘(𝕜, E) n (E →L[𝕜] E) E where
+instance {n : ℕ∞ω} : ContMDiffSMul 𝓘(𝕜, E →L[𝕜] E) 𝓘(𝕜, E) n (E →L[𝕜] E) E where
   contMDiff_smul := by
     have h : ContMDiff (𝓘(𝕜, E →L[𝕜] E).prod 𝓘(𝕜, E)) 𝓘(𝕜, (E →L[𝕜] E) × E) n
         (@id ((E →L[𝕜] E) × E)) := by
diff --git a/Mathlib/Geometry/Manifold/MFDeriv/Basic.lean b/Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
@@ -242,7 +242,7 @@ variable {e : OpenPartialHomeomorph M H} {e' : OpenPartialHomeomorph M' H'}
 open IsManifold
 
 theorem mdifferentiableWithinAt_iff_source_of_mem_maximalAtlas
-    [IsManifold I 1 M] (he : e ∈ maximalAtlas I 1 M) (hx : x ∈ e.source) :
+    (he : e ∈ maximalAtlas I 1 M) (hx : x ∈ e.source) :
     MDifferentiableWithinAt I I' f s x ↔
       MDifferentiableWithinAt 𝓘(𝕜, E) I' (f ∘ (e.extend I).symm) ((e.extend I).symm ⁻¹' s ∩ range I)
         (e.extend I x) := by
diff --git a/Mathlib/LinearAlgebra/AffineSpace/Simplex/Basic.lean b/Mathlib/LinearAlgebra/AffineSpace/Simplex/Basic.lean
@@ -643,7 +643,7 @@ theorem closedInterior_face_ssubset_closedInterior [Nontrivial k] [ZeroLEOneClas
   apply (Set.ssubset_iff_of_subset (s.closedInterior_face_subset_closedInterior h)).mpr
   exact ⟨s.points a, s.point_mem_closedInterior a, fun hs ↦ ha (by simpa using hs)⟩
 
-theorem disjoint_interior_closedInterior_face [Nontrivial k] [ZeroLEOneClass k] {n : ℕ}
+theorem disjoint_interior_closedInterior_face {n : ℕ}
     (s : Simplex k P n) {fs : Finset (Fin (n + 1))} (hfs : fs ≠ .univ) {m : ℕ} (h : #fs = m + 1) :
     Disjoint s.interior (s.face h).closedInterior := by
   refine Set.disjoint_left.mpr fun p hleft hright ↦ ?_
@@ -669,8 +669,8 @@ theorem closedInterior_faceOpposite_ssubset_closedInterior [Nontrivial k] [ZeroL
     (s.faceOpposite i).closedInterior ⊂ s.closedInterior :=
   s.closedInterior_face_ssubset_closedInterior (by simp) _
 
-theorem disjoint_interior_closedInterior_faceOpposite [Nontrivial k] [ZeroLEOneClass k] {n : ℕ}
-    [NeZero n] (s : Simplex k P n) (i : Fin (n + 1)) :
+theorem disjoint_interior_closedInterior_faceOpposite {n : ℕ} [NeZero n]
+    (s : Simplex k P n) (i : Fin (n + 1)) :
     Disjoint s.interior (s.faceOpposite i).closedInterior :=
   s.disjoint_interior_closedInterior_face (by simp) _
 
@@ -705,7 +705,7 @@ theorem closedInterior_eq_interior_union [IsOrderedAddMonoid k] [ZeroLEOneClass
   · refine Set.union_subset s.interior_subset_closedInterior (Set.iUnion_subset fun i ↦ ?_)
     exact s.closedInterior_faceOpposite_subset_closedInterior i
 
-theorem closedInterior_sdiff_interior [Nontrivial k] [IsOrderedAddMonoid k] [ZeroLEOneClass k]
+theorem closedInterior_sdiff_interior [IsOrderedAddMonoid k] [ZeroLEOneClass k]
     {n : ℕ} [NeZero n] (s : Simplex k P n) :
     s.closedInterior \ s.interior = ⋃ i : Fin (n + 1), (s.faceOpposite i).closedInterior := by
   simpa [closedInterior_eq_interior_union] using
diff --git a/Mathlib/MeasureTheory/Constructions/BorelSpace/Metrizable.lean b/Mathlib/MeasureTheory/Constructions/BorelSpace/Metrizable.lean
@@ -103,7 +103,7 @@ theorem measurable_of_tendsto_metrizable_ae {μ : Measure α} [μ.IsComplete] {f
   aemeasurable_iff_measurable.mp
     (aemeasurable_of_tendsto_metrizable_ae' (fun i => (hf i).aemeasurable) h_ae_tendsto)
 
-theorem measurable_limit_of_tendsto_metrizable_ae {ι} [Countable ι] [Nonempty ι] {μ : Measure α}
+theorem measurable_limit_of_tendsto_metrizable_ae {ι} [Nonempty ι] {μ : Measure α}
     {f : ι → α → β} {L : Filter ι} [L.IsCountablyGenerated] (hf : ∀ n, AEMeasurable (f n) μ)
     (h_ae_tendsto : ∀ᵐ x ∂μ, ∃ l : β, Tendsto (fun n => f n x) L (𝓝 l)) :
     ∃ f_lim : α → β, Measurable f_lim ∧ ∀ᵐ x ∂μ, Tendsto (fun n => f n x) L (𝓝 (f_lim x)) := by
diff --git a/Mathlib/ModelTheory/Satisfiability.lean b/Mathlib/ModelTheory/Satisfiability.lean
@@ -196,7 +196,7 @@ variable (L)
 into `M`, but is not by type a substructure of `M`, and thus can be chosen to belong to the universe
 of the cardinal `κ`.
 -/
-theorem exists_elementaryEmbedding_card_eq_of_le (M : Type w') [L.Structure M] [Nonempty M]
+theorem exists_elementaryEmbedding_card_eq_of_le (M : Type w') [L.Structure M]
     (κ : Cardinal.{w}) (h1 : ℵ₀ ≤ κ) (h2 : lift.{w} L.card ≤ Cardinal.lift.{max u v} κ)
     (h3 : lift.{w'} κ ≤ Cardinal.lift.{w} #M) :
     ∃ N : Bundled L.Structure, Nonempty (N ↪ₑ[L] M) ∧ #N = κ := by
diff --git a/Mathlib/NumberTheory/NumberField/Discriminant/Different.lean b/Mathlib/NumberTheory/NumberField/Discriminant/Different.lean
@@ -87,7 +87,7 @@ lemma discr_mem_differentIdeal : ↑(discr K) ∈ differentIdeal ℤ 𝒪 := by
 
 attribute [local instance] FractionRing.liftAlgebra in
 theorem natAbs_discr_eq_absNorm_differentIdeal_mul_natAbs_discr_pow (L 𝒪' : Type*) [Field L]
-    [NumberField L] [CommRing 𝒪'] [Algebra 𝒪' L] [IsFractionRing 𝒪' L] [IsIntegralClosure 𝒪' ℤ L]
+    [NumberField L] [CommRing 𝒪'] [Algebra 𝒪' L] [IsFractionRing 𝒪' L]
     [IsDedekindDomain 𝒪'] [CharZero 𝒪'] [Algebra K L] [Algebra 𝒪 𝒪'] [Algebra 𝒪 L]
     [IsScalarTower 𝒪 K L] [IsScalarTower 𝒪 𝒪' L] [IsTorsionFree 𝒪 𝒪'] [Free ℤ 𝒪']
     [Module.Finite ℤ 𝒪'] [Module.Finite 𝒪 𝒪'] :
diff --git a/Mathlib/Probability/HasCondDistrib.lean b/Mathlib/Probability/HasCondDistrib.lean
@@ -49,7 +49,7 @@ lemma HasCondDistrib.aemeasurable_fst (h : HasCondDistrib Y X κ P) :
 lemma HasCondDistrib.aemeasurable_snd (h : HasCondDistrib Y X κ P) :
     AEMeasurable Y P := h.aemeasurable.snd
 
-lemma HasLaw.prodMk_of_hasCondDistrib {Q : Measure 𝓧} [IsSFiniteKernel κ]
+lemma HasLaw.prodMk_of_hasCondDistrib {Q : Measure 𝓧}
     (h1 : HasLaw X Q P) (h2 : HasCondDistrib Y X κ P) :
     HasLaw (fun ω ↦ (X ω, Y ω)) (Q ⊗ₘ κ) P := by rwa [← h1.map_eq]
 
diff --git a/Mathlib/Probability/Independence/Basic.lean b/Mathlib/Probability/Independence/Basic.lean
@@ -1036,7 +1036,7 @@ theorem iIndepSet.iIndepFun_indicator [Zero β] [One β] {m : MeasurableSpace β
   Kernel.iIndepSet.iIndepFun_indicator hs
 
 lemma Indep.indicator_indepFun {m : MeasurableSpace Ω} {M 𝓧 : Type*}
-    [Zero M] [MeasurableSpace M] (c : M) [NeZero c] {m𝓧 : MeasurableSpace 𝓧} {A : Set Ω}
+    [Zero M] [MeasurableSpace M] (c : M) {m𝓧 : MeasurableSpace 𝓧} {A : Set Ω}
     {X : Ω → 𝓧} (hA : MeasurableSet[m] A) (h : Indep m (m𝓧.comap X) μ) :
     (A.indicator (fun _ ↦ c)) ⟂ᵢ[μ] X :=
   Kernel.Indep.indicator_const_indepFun c hA h
diff --git a/Mathlib/Probability/Independence/Integration.lean b/Mathlib/Probability/Independence/Integration.lean
@@ -312,11 +312,11 @@ theorem IndepFun.integral_bilin_comp_comp'
 /-- If `X` and `Y` are independent and integrable random variables and `B`
 is a continuous bilinear map, then `∫ ω, B (X ω) (Y ω) ∂μ = B μ[X] μ[Y].` -/
 theorem IndepFun.integral_bilin
-    [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace 𝕜 E] [CompleteSpace E]
+    [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
     [MeasurableSpace E] [BorelSpace E]
-    [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [CompleteSpace F]
+    [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F]
     [MeasurableSpace F] [BorelSpace F]
-    [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedSpace 𝕜 G] [CompleteSpace G]
+    [NormedAddCommGroup G] [NormedSpace ℝ G] [CompleteSpace G]
     {X : Ω → E} {Y : Ω → F} (hXY : X ⟂ᵢ[μ] Y) (hX : Integrable X μ) (hY : Integrable Y μ)
     (B : E →L[ℝ] F →L[ℝ] G) :
     ∫ ω, B (X ω) (Y ω) ∂μ = B μ[X] μ[Y] :=
@@ -333,11 +333,11 @@ The assumption on `B` allows to drop the integrability condition in
 `IndepFun.integral_bilin'`, which is useful for the versions where `B` is the scalar
 multiplication or the multiplication. -/
 theorem IndepFun.integral_bilin'
-    [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace 𝕜 E] [CompleteSpace E]
+    [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
     [MeasurableSpace E] [BorelSpace E]
-    [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [CompleteSpace F]
+    [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F]
     [MeasurableSpace F] [BorelSpace F]
-    [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedSpace 𝕜 G] [CompleteSpace G]
+    [NormedAddCommGroup G] [NormedSpace ℝ G] [CompleteSpace G]
     {X : Ω → E} {Y : Ω → F} (hXY : X ⟂ᵢ[μ] Y) (hX : AEStronglyMeasurable X μ)
     (hY : AEStronglyMeasurable Y μ)
     (B : E →L[ℝ] F →L[ℝ] G) (c : ℝ≥0) (hc : c ≠ 0) (hB : ∀ x y, c * ‖x‖ * ‖y‖ ≤ ‖B x y‖) :
@@ -405,7 +405,7 @@ lemma IndepFun.integral_smul_eq_smul_integral
     (hX : AEStronglyMeasurable X μ) (hY : AEStronglyMeasurable Y μ) :
     μ[X • Y] = μ[X] • μ[Y] := by
   by_cases hE : CompleteSpace E
-  · exact hXY.integral_bilin' (𝕜 := 𝕜) hX hY (.lsmul ℝ 𝕜) 1 (by simp) (by simp [norm_smul])
+  · exact hXY.integral_bilin' hX hY (.lsmul ℝ 𝕜) 1 (by simp) (by simp [norm_smul])
   · simp [integral, hE]
 
 lemma IndepFun.integral_mul_eq_mul_integral
diff --git a/Mathlib/Probability/Independence/Kernel/IndepFun.lean b/Mathlib/Probability/Independence/Kernel/IndepFun.lean
@@ -695,7 +695,7 @@ theorem iIndepSet.iIndepFun_indicator [Zero β] [One β] {m : MeasurableSpace β
   · exact @MeasurableSet.empty _ (generateFrom {s i})
 
 lemma Indep.indicator_const_indepFun {m : MeasurableSpace Ω} {M 𝓧 : Type*}
-    [Zero M] [MeasurableSpace M] (c : M) [NeZero c] {m𝓧 : MeasurableSpace 𝓧} {A : Set Ω}
+    [Zero M] [MeasurableSpace M] (c : M) {m𝓧 : MeasurableSpace 𝓧} {A : Set Ω}
     {X : Ω → 𝓧} (hA : MeasurableSet[m] A) (h : Indep m (m𝓧.comap X) κ μ) :
     IndepFun (A.indicator (fun _ ↦ c)) X κ μ :=
   indep_of_indep_of_le_left h (measurable_const.indicator hA).comap_le
diff --git a/Mathlib/Probability/Martingale/Centering.lean b/Mathlib/Probability/Martingale/Centering.lean
@@ -99,8 +99,8 @@ lemma Submartingale.predictablePart_nonneg
   filter_upwards [hf.monotone_predictablePart] with ω hω n
   simpa [predictablePart_zero] using hω (Nat.zero_le n)
 
-lemma IsStronglyPredictable.predictablePart_eq [SecondCountableTopology E] [MeasurableSpace E]
-    [BorelSpace E] [SigmaFiniteFiltration μ ℱ] (hf : IsStronglyPredictable ℱ f)
+lemma IsStronglyPredictable.predictablePart_eq
+    [SigmaFiniteFiltration μ ℱ] (hf : IsStronglyPredictable ℱ f)
     (hfint : ∀ n, Integrable (f n) μ) (n : ℕ) :
     predictablePart f ℱ μ n =ᵐ[μ] f n - f 0 := by
   simp only [predictablePart, ← Finset.sum_range_sub]
@@ -148,8 +148,7 @@ lemma Martingale.martingalePart_eq [CompleteSpace E] (hf : Martingale f ℱ μ)
   filter_upwards [hf.predictablePart_eq_zero n] with ω hω
   simp [martingalePart, hω]
 
-lemma IsPredictable.martingalePart_eq [SecondCountableTopology E] [MeasurableSpace E]
-    [BorelSpace E] [SigmaFiniteFiltration μ ℱ] (hf : IsStronglyPredictable ℱ f)
+lemma IsPredictable.martingalePart_eq [SigmaFiniteFiltration μ ℱ] (hf : IsStronglyPredictable ℱ f)
     (hfint : ∀ n, Integrable (f n) μ) (n : ℕ) :
     martingalePart f ℱ μ n =ᵐ[μ] f 0 := by
   filter_upwards [hf.predictablePart_eq (μ := μ) hfint n] with ω hω
diff --git a/Mathlib/RingTheory/Ideal/Operations.lean b/Mathlib/RingTheory/Ideal/Operations.lean
diff --git a/Mathlib/RingTheory/IsGaloisGroup/Basic.lean b/Mathlib/RingTheory/IsGaloisGroup/Basic.lean
diff --git a/Mathlib/RingTheory/MvPowerSeries/GaussNorm.lean b/Mathlib/RingTheory/MvPowerSeries/GaussNorm.lean
diff --git a/Mathlib/RingTheory/RamificationInertia/Basic.lean b/Mathlib/RingTheory/RamificationInertia/Basic.lean
diff --git a/Mathlib/RingTheory/TwoSidedIdeal/BigOperators.lean b/Mathlib/RingTheory/TwoSidedIdeal/BigOperators.lean
diff --git a/Mathlib/Topology/Algebra/Module/Complement.lean b/Mathlib/Topology/Algebra/Module/Complement.lean
diff --git a/Mathlib/Topology/Algebra/Order/Floor.lean b/Mathlib/Topology/Algebra/Order/Floor.lean
diff --git a/Mathlib/Topology/Order/Completion.lean b/Mathlib/Topology/Order/Completion.lean
diff --git a/Mathlib/Topology/Order/ScottTopology.lean b/Mathlib/Topology/Order/ScottTopology.lean
diff --git a/Mathlib/Topology/UniformSpace/ProdApproximation.lean b/Mathlib/Topology/UniformSpace/ProdApproximation.lean
