fix: add some robustness to fragile declarations (#6177)

These declarations broke when I tweaked instances a little bit (in a separate branch that is not ready yet), and I think these declarations can use some extra robustness (usually by providing some extra information explicitly).

Mathlib/Algebra/Lie/TensorProduct.lean

@@ -207,11 +207,8 @@ open TensorProduct.LieModule
 open LieModule
 
 variable {L : Type v} {M : Type w}
-
 variable [LieRing L] [LieAlgebra R L]
-
 variable [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M]
-
 variable (I : LieIdeal R L) (N : LieSubmodule R L M)
 
 /-- A useful alternative characterisation of Lie ideal operations on Lie submodules.
@@ -221,7 +218,7 @@ applying the action of `L` on `M`, we obtain morphism of Lie modules `f : I ⊗
 
 This lemma states that `⁅I, N⁆ = range f`. -/
 theorem lieIdeal_oper_eq_tensor_map_range :
-    ⁅I, N⁆ = ((toModuleHom R L M).comp (mapIncl I N : (↥I) ⊗ (↥N) →ₗ⁅R,L⁆ L ⊗ M)).range := by
+    ⁅I, N⁆ = ((toModuleHom R L M).comp (mapIncl I N : (↥I) ⊗[R] (↥N) →ₗ⁅R,L⁆ L ⊗[R] M)).range := by
   rw [← coe_toSubmodule_eq_iff, lieIdeal_oper_eq_linear_span, LieModuleHom.coeSubmodule_range,
     LieModuleHom.coe_linearMap_comp, LinearMap.range_comp, mapIncl_def, coe_linearMap_map,
     TensorProduct.map_range_eq_span_tmul, Submodule.map_span]

Mathlib/CategoryTheory/Monoidal/CommMon_.lean

@@ -166,8 +166,8 @@ namespace EquivLaxBraidedFunctorPunit
 /-- Implementation of `CommMon_.equivLaxBraidedFunctorPunit`. -/
 @[simps]
 def laxBraidedToCommMon : LaxBraidedFunctor (Discrete PUnit.{u + 1}) C ⥤ CommMon_ C where
-  obj F := (F.mapCommMon : CommMon_ _ ⥤ CommMon_ C).obj (trivial (Discrete PUnit))
-  map α := ((mapCommMonFunctor (Discrete PUnit) C).map α).app _
+  obj F := (F.mapCommMon : CommMon_ _ ⥤ CommMon_ C).obj (trivial (Discrete PUnit.{u+1}))
+  map α := ((mapCommMonFunctor (Discrete PUnit.{u+1}) C).map α).app _
 set_option linter.uppercaseLean3 false in
 #align CommMon_.equiv_lax_braided_functor_punit.lax_braided_to_CommMon CommMon_.EquivLaxBraidedFunctorPunit.laxBraidedToCommMon
 

Mathlib/Data/Finsupp/Multiset.lean

@@ -70,7 +70,7 @@ theorem toMultiset_single (a : α) (n : ℕ) : toMultiset (single a n) = n • {
 
 theorem toMultiset_sum {f : ι → α →₀ ℕ} (s : Finset ι) :
     Finsupp.toMultiset (∑ i in s, f i) = ∑ i in s, Finsupp.toMultiset (f i) :=
-  map_sum _ _ _
+  map_sum Finsupp.toMultiset _ _
 #align finsupp.to_multiset_sum Finsupp.toMultiset_sum
 
 theorem toMultiset_sum_single (s : Finset ι) (n : ℕ) :

Mathlib/LinearAlgebra/Finsupp.lean

@@ -530,8 +530,8 @@ end LComapDomain
 
 section Total
 
-variable (α) {α' : Type _} (M) {M' : Type _} (R) [Semiring R] [AddCommMonoid M'] [AddCommMonoid M]
-  [Module R M'] [Module R M] (v : α → M) {v' : α' → M'}
+variable (α) (M) (R)
+variable {α' : Type _} {M' : Type _} [AddCommMonoid M'] [Module R M'] (v : α → M) {v' : α' → M'}
 
 /-- Interprets (l : α →₀ R) as linear combination of the elements in the family (v : α → M) and
     evaluates this linear combination. -/

Mathlib/Order/CompleteLattice.lean

@@ -20,9 +20,9 @@ import Mathlib.Mathport.Notation
 * `sSup` and `sInf` are the supremum and the infimum of a set;
 * `iSup (f : ι → α)` and `iInf (f : ι → α)` are indexed supremum and infimum of a function,
   defined as `sSup` and `sInf` of the range of this function;
-* `class CompleteLattice`: a bounded lattice such that `sSup s` is always the least upper boundary
+* class `CompleteLattice`: a bounded lattice such that `sSup s` is always the least upper boundary
   of `s` and `sInf s` is always the greatest lower boundary of `s`;
-* `class CompleteLinearOrder`: a linear ordered complete lattice.
+* class `CompleteLinearOrder`: a linear ordered complete lattice.
 
 ## Naming conventions
 

Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean

@@ -620,8 +620,8 @@ theorem forget₂ToModuleCatHomotopyEquiv_f_0_eq :
     simp only [Iso.symm_hom, eqToIso.inv, HomologicalComplex.eqToHom_f, eqToHom_refl]
   trans (Finsupp.total _ _ _ fun _ => (1 : k)).comp ((ModuleCat.free k).map (terminal.from _))
   · dsimp
-    erw [@Finsupp.lmapDomain_total (Fin 1 → G) k k (⊤_ Type u) k _ _ _ _ _ (fun _ => (1 : k))
-        (fun _ => (1 : k))
+    erw [Finsupp.lmapDomain_total (α := Fin 1 → G) (R := k) (α' := ⊤_ Type u)
+        (v := fun _ => (1 : k)) (v' := fun _ => (1 : k))
         (terminal.from
           ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk 0))).V)
         LinearMap.id fun i => rfl,

Mathlib/Tactic/Positivity/Core.lean

@@ -124,7 +124,7 @@ lemma nz_of_isNegNat [StrictOrderedRing A]
   simpa using w
 
 lemma pos_of_isRat [LinearOrderedRing A] :
-    (NormNum.IsRat e n d) → (decide (0 < n)) → (0 < (e : A))
+    (NormNum.IsRat e n d) → (decide (0 < n)) → ((0 : A) < (e : A))
   | ⟨inv, eq⟩, h => by
     have pos_invOf_d : (0 < ⅟ (d : A)) := pos_invOf_of_invertible_cast d
     have pos_n : (0 < (n : A)) := Int.cast_pos (n := n) |>.2 (of_decide_eq_true h)