chore: make two arguments of Finsupp.total implicit (#16221)

See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Finsupp.2Etotal.

Author: PatrickMassot

Mathlib/Algebra/Algebra/Subalgebra/Operations.lean

@@ -67,7 +67,7 @@ theorem mem_of_finset_sum_eq_one_of_pow_smul_mem
   exact ⟨⟨_, hn i⟩, rfl⟩
 
 theorem mem_of_span_eq_top_of_smul_pow_mem
-    (s : Set S) (l : s →₀ S) (hs : Finsupp.total s S S (↑) l = 1)
+    (s : Set S) (l : s →₀ S) (hs : Finsupp.total S ((↑) : s → S) l = 1)
     (hs' : s ⊆ S') (hl : ∀ i, l i ∈ S') (x : S) (H : ∀ r : s, ∃ n : ℕ, (r : S) ^ n • x ∈ S') :
     x ∈ S' :=
   mem_of_finset_sum_eq_one_of_pow_smul_mem S' l.support (↑) l hs (fun x => hs' x.2) hl x H

Mathlib/Algebra/Module/FinitePresentation.lean

@@ -57,7 +57,7 @@ and the kernel of the presentation `Rˢ → M` is also finitely generated.
 -/
 class Module.FinitePresentation : Prop where
   out : ∃ (s : Finset M), Submodule.span R (s : Set M) = ⊤ ∧
-    (LinearMap.ker (Finsupp.total s M R Subtype.val)).FG
+    (LinearMap.ker (Finsupp.total R ((↑) : s → M))).FG
 
 instance (priority := 100) [h : Module.FinitePresentation R M] : Module.Finite R M := by
   obtain ⟨s, hs₁, _⟩ := h
@@ -78,7 +78,7 @@ theorem Module.FinitePresentation.equiv_quotient [fp : Module.FinitePresentation
       Module.Free R L ∧ Module.Finite R L ∧ K.FG := by
   obtain ⟨ι, ⟨hι₁, hι₂⟩⟩ := fp
   use ι →₀ R, inferInstance, inferInstance
-  use LinearMap.ker (Finsupp.total { x // x ∈ ι } M R Subtype.val)
+  use LinearMap.ker (Finsupp.total R Subtype.val)
   refine ⟨(LinearMap.quotKerEquivOfSurjective _ ?_).symm, inferInstance, inferInstance, hι₂⟩
   apply LinearMap.range_eq_top.mp
   simpa only [Finsupp.range_total, Subtype.range_coe_subtype, Finset.setOf_mem]
@@ -145,12 +145,12 @@ lemma Module.finitePresentation_of_surjective [h : Module.FinitePresentation R M
   classical
   obtain ⟨s, hs, hs'⟩ := h
   obtain ⟨t, ht⟩ := hl'
-  have H : Function.Surjective (Finsupp.total s M R Subtype.val) :=
+  have H : Function.Surjective (Finsupp.total R ((↑) : s → M)) :=
     LinearMap.range_eq_top.mp (by rw [Finsupp.range_total, Subtype.range_val, ← hs]; rfl)
-  apply Module.finitePresentation_of_free_of_surjective (l ∘ₗ Finsupp.total s M R Subtype.val)
+  apply Module.finitePresentation_of_free_of_surjective (l ∘ₗ Finsupp.total R Subtype.val)
     (hl.comp H)
   choose σ hσ using (show _ from H)
-  have : Finsupp.total s M R Subtype.val '' (σ '' t) = t := by
+  have : Finsupp.total R Subtype.val '' (σ '' t) = t := by
     simp only [Set.image_image, hσ, Set.image_id']
   rw [LinearMap.ker_comp, ← ht, ← this, ← Submodule.map_span, Submodule.comap_map_eq,
     ← Finset.coe_image]
@@ -161,11 +161,11 @@ lemma Module.FinitePresentation.fg_ker [Module.Finite R M]
     (LinearMap.ker l).FG := by
   classical
   obtain ⟨s, hs, hs'⟩ := h
-  have H : Function.Surjective (Finsupp.total s N R Subtype.val) :=
+  have H : Function.Surjective (Finsupp.total R ((↑) : s → N)) :=
     LinearMap.range_eq_top.mp (by rw [Finsupp.range_total, Subtype.range_val, ← hs]; rfl)
-  obtain ⟨f, hf⟩ : ∃ f : (s →₀ R) →ₗ[R] M, l ∘ₗ f = (Finsupp.total s N R Subtype.val) := by
+  obtain ⟨f, hf⟩ : ∃ f : (s →₀ R) →ₗ[R] M, l ∘ₗ f = (Finsupp.total R Subtype.val) := by
     choose f hf using show _ from hl
-    exact ⟨Finsupp.total s M R (fun i ↦ f i), by ext; simp [hf]⟩
+    exact ⟨Finsupp.total R (fun i ↦ f i), by ext; simp [hf]⟩
   have : (LinearMap.ker l).map (LinearMap.range f).mkQ = ⊤ := by
     rw [← top_le_iff]
     rintro x -
@@ -192,7 +192,7 @@ lemma Module.finitePresentation_of_ker [Module.FinitePresentation R N]
     · rw [Submodule.map_top, LinearMap.range_eq_top.mpr hl]; exact Module.Finite.out
     · rw [top_inf_eq, ← Submodule.fg_top]; exact Module.Finite.out
   refine ⟨s, hs, ?_⟩
-  let π := Finsupp.total s M R Subtype.val
+  let π := Finsupp.total R ((↑) : s → M)
   have H : Function.Surjective π :=
     LinearMap.range_eq_top.mp (by rw [Finsupp.range_total, Subtype.range_val, ← hs]; rfl)
   have inst : Module.Finite R (LinearMap.ker (l ∘ₗ π)) := by
@@ -227,23 +227,23 @@ lemma Module.FinitePresentation.exists_lift_of_isLocalizedModule
     [h : Module.FinitePresentation R M] (g : M →ₗ[R] N') :
     ∃ (h : M →ₗ[R] N) (s : S), f ∘ₗ h = s • g := by
   obtain ⟨σ, hσ, τ, hτ⟩ := h
-  let π := Finsupp.total σ M R Subtype.val
+  let π := Finsupp.total R ((↑) : σ → M)
   have hπ : Function.Surjective π :=
     LinearMap.range_eq_top.mp (by rw [Finsupp.range_total, Subtype.range_val, ← hσ]; rfl)
   classical
   choose s hs using IsLocalizedModule.surj S f
   let i : σ → N :=
     fun x ↦ (∏ j ∈ σ.erase x.1, (s (g j)).2) • (s (g x)).1
   let s₀ := ∏ j ∈ σ, (s (g j)).2
-  have hi : f ∘ₗ Finsupp.total σ N R i = (s₀ • g) ∘ₗ π := by
+  have hi : f ∘ₗ Finsupp.total R i = (s₀ • g) ∘ₗ π := by
     ext j
     simp only [LinearMap.coe_comp, Function.comp_apply, Finsupp.lsingle_apply, Finsupp.total_single,
       one_smul, LinearMap.map_smul_of_tower, ← hs, LinearMap.smul_apply, i, s₀, π]
     rw [← mul_smul, Finset.prod_erase_mul]
     exact j.prop
-  have : ∀ x : τ, ∃ s : S, s • (Finsupp.total σ N R i x) = 0 := by
+  have : ∀ x : τ, ∃ s : S, s • (Finsupp.total R i x) = 0 := by
     intros x
-    convert_to ∃ s : S, s • (Finsupp.total σ N R i x) = s • 0
+    convert_to ∃ s : S, s • (Finsupp.total R i x) = s • 0
     · simp only [smul_zero]
     apply IsLocalizedModule.exists_of_eq (S := S) (f := f)
     rw [← LinearMap.comp_apply, map_zero, hi, LinearMap.comp_apply]
@@ -252,7 +252,7 @@ lemma Module.FinitePresentation.exists_lift_of_isLocalizedModule
     exact Submodule.subset_span x.prop
   choose s' hs' using this
   let s₁ := ∏ i : τ, s' i
-  have : LinearMap.ker π ≤ LinearMap.ker (s₁ • Finsupp.total σ N R i) := by
+  have : LinearMap.ker π ≤ LinearMap.ker (s₁ • Finsupp.total R i) := by
     rw [← hτ, Submodule.span_le]
     intro x hxσ
     simp only [s₁]

Mathlib/Algebra/Module/Projective.lean

@@ -72,7 +72,7 @@ open Finsupp
   definitions. -/
 class Module.Projective (R : Type*) [Semiring R] (P : Type*) [AddCommMonoid P] [Module R P] :
     Prop where
-  out : ∃ s : P →ₗ[R] P →₀ R, Function.LeftInverse (Finsupp.total P P R id) s
+  out : ∃ s : P →ₗ[R] P →₀ R, Function.LeftInverse (Finsupp.total R id) s
 
 namespace Module
 
@@ -82,11 +82,11 @@ variable {R : Type*} [Semiring R] {P : Type*} [AddCommMonoid P] [Module R P] {M
   [AddCommMonoid M] [Module R M] {N : Type*} [AddCommMonoid N] [Module R N]
 
 theorem projective_def :
-    Projective R P ↔ ∃ s : P →ₗ[R] P →₀ R, Function.LeftInverse (Finsupp.total P P R id) s :=
+    Projective R P ↔ ∃ s : P →ₗ[R] P →₀ R, Function.LeftInverse (Finsupp.total R id) s :=
   ⟨fun h => h.1, fun h => ⟨h⟩⟩
 
 theorem projective_def' :
-    Projective R P ↔ ∃ s : P →ₗ[R] P →₀ R, Finsupp.total P P R id ∘ₗ s = .id := by
+    Projective R P ↔ ∃ s : P →ₗ[R] P →₀ R, Finsupp.total R id ∘ₗ s = .id := by
   simp_rw [projective_def, DFunLike.ext_iff, Function.LeftInverse, comp_apply, id_apply]
 
 /-- A projective R-module has the property that maps from it lift along surjections. -/
@@ -101,7 +101,7 @@ theorem projective_lifting_property [h : Projective R P] (f : M →ₗ[R] N) (g
     `P →ₗ N` and a random splitting of the surjection `M →ₗ N`, and we get
     a map `φ : (P →₀ R) →ₗ M`.
     -/
-  let φ : (P →₀ R) →ₗ[R] M := Finsupp.total _ _ _ fun p => Function.surjInv hf (g p)
+  let φ : (P →₀ R) →ₗ[R] M := Finsupp.total _ fun p => Function.surjInv hf (g p)
   -- By projectivity we have a map `P →ₗ (P →₀ R)`;
   cases' h.out with s hs
   -- Compose to get `P →ₗ M`. This works.
@@ -117,7 +117,7 @@ theorem Projective.of_lifting_property'' {R : Type u} [Semiring R] {P : Type v}
     [Module R P] (huniv : ∀ (f : (P →₀ R) →ₗ[R] P), Function.Surjective f →
       ∃ h : P →ₗ[R] (P →₀ R), f.comp h = .id) :
     Projective R P :=
-  projective_def'.2 <| huniv (Finsupp.total P P R (id : P → P))
+  projective_def'.2 <| huniv (Finsupp.total R (id : P → P))
     (total_surjective _ Function.surjective_id)
 
 variable {Q : Type*} [AddCommMonoid Q] [Module R Q]
@@ -164,7 +164,7 @@ variable [IsScalarTower R₀ R M] [AddCommGroup N] [Module R₀ N]
 
 theorem Projective.of_split [Module.Projective R M]
     (i : P →ₗ[R] M) (s : M →ₗ[R] P) (H : s.comp i = LinearMap.id) : Module.Projective R P := by
-  obtain ⟨g, hg⟩ := projective_lifting_property (Finsupp.total P P R id) s
+  obtain ⟨g, hg⟩ := projective_lifting_property (Finsupp.total R id) s
     (fun x ↦ ⟨Finsupp.single x 1, by simp⟩)
   refine ⟨g.comp i, fun x ↦ ?_⟩
   rw [LinearMap.comp_apply, ← LinearMap.comp_apply, hg,
@@ -178,7 +178,7 @@ theorem Projective.of_equiv [Module.Projective R M]
 theorem Projective.iff_split : Module.Projective R P ↔
     ∃ (M : Type max u v) (_ : AddCommGroup M) (_ : Module R M) (_ : Module.Free R M)
       (i : P →ₗ[R] M) (s : M →ₗ[R] P), s.comp i = LinearMap.id :=
-  ⟨fun ⟨i, hi⟩ ↦ ⟨P →₀ R, _, _, inferInstance, i, Finsupp.total P P R id, LinearMap.ext hi⟩,
+  ⟨fun ⟨i, hi⟩ ↦ ⟨P →₀ R, _, _, inferInstance, i, Finsupp.total R id, LinearMap.ext hi⟩,
     fun ⟨_, _, _, _, i, s, H⟩ ↦ Projective.of_split i s H⟩
 
 /-- A quotient of a projective module is projective iff it is a direct summand. -/
@@ -197,11 +197,11 @@ instance Projective.tensorProduct [hM : Module.Projective R M] [hN : Module.Proj
     fapply Projective.of_split (R := R) (M := ((M →₀ R) ⊗[R₀] (N →₀ R₀)))
     · exact (AlgebraTensorModule.map sM (LinearMap.id (R := R₀) (M := N →₀ R₀)))
     · exact (AlgebraTensorModule.map
-        (Finsupp.total M M R id) (LinearMap.id (R := R₀) (M := N →₀ R₀)))
+        (Finsupp.total R id) (LinearMap.id (R := R₀) (M := N →₀ R₀)))
     · ext; simp [hsM _]
   fapply Projective.of_split (R := R) (M := (M ⊗[R₀] (N →₀ R₀)))
   · exact (AlgebraTensorModule.map (LinearMap.id (R := R) (M := M)) sN)
-  · exact (AlgebraTensorModule.map (LinearMap.id (R := R) (M := M)) (Finsupp.total N N R₀ id))
+  · exact (AlgebraTensorModule.map (LinearMap.id (R := R) (M := M)) (Finsupp.total R₀ id))
   · ext; simp [hsN _]
 
 end Ring

Mathlib/Analysis/InnerProductSpace/Basic.lean

@@ -829,7 +829,7 @@ theorem orthonormal_subtype_iff_ite [DecidableEq E] {s : Set E} :
 /-- The inner product of a linear combination of a set of orthonormal vectors with one of those
 vectors picks out the coefficient of that vector. -/
 theorem Orthonormal.inner_right_finsupp {v : ι → E} (hv : Orthonormal 𝕜 v) (l : ι →₀ 𝕜) (i : ι) :
-    ⟪v i, Finsupp.total ι E 𝕜 v l⟫ = l i := by
+    ⟪v i, Finsupp.total 𝕜 v l⟫ = l i := by
   classical
   simpa [Finsupp.total_apply, Finsupp.inner_sum, orthonormal_iff_ite.mp hv] using Eq.symm
 
@@ -849,7 +849,7 @@ theorem Orthonormal.inner_right_fintype [Fintype ι] {v : ι → E} (hv : Orthon
 /-- The inner product of a linear combination of a set of orthonormal vectors with one of those
 vectors picks out the coefficient of that vector. -/
 theorem Orthonormal.inner_left_finsupp {v : ι → E} (hv : Orthonormal 𝕜 v) (l : ι →₀ 𝕜) (i : ι) :
-    ⟪Finsupp.total ι E 𝕜 v l, v i⟫ = conj (l i) := by rw [← inner_conj_symm, hv.inner_right_finsupp]
+    ⟪Finsupp.total 𝕜 v l, v i⟫ = conj (l i) := by rw [← inner_conj_symm, hv.inner_right_finsupp]
 
 /-- The inner product of a linear combination of a set of orthonormal vectors with one of those
 vectors picks out the coefficient of that vector. -/
@@ -868,13 +868,13 @@ theorem Orthonormal.inner_left_fintype [Fintype ι] {v : ι → E} (hv : Orthono
 /-- The inner product of two linear combinations of a set of orthonormal vectors, expressed as
 a sum over the first `Finsupp`. -/
 theorem Orthonormal.inner_finsupp_eq_sum_left {v : ι → E} (hv : Orthonormal 𝕜 v) (l₁ l₂ : ι →₀ 𝕜) :
-    ⟪Finsupp.total ι E 𝕜 v l₁, Finsupp.total ι E 𝕜 v l₂⟫ = l₁.sum fun i y => conj y * l₂ i := by
+    ⟪Finsupp.total 𝕜 v l₁, Finsupp.total 𝕜 v l₂⟫ = l₁.sum fun i y => conj y * l₂ i := by
   simp only [l₁.total_apply _, Finsupp.sum_inner, hv.inner_right_finsupp, smul_eq_mul]
 
 /-- The inner product of two linear combinations of a set of orthonormal vectors, expressed as
 a sum over the second `Finsupp`. -/
 theorem Orthonormal.inner_finsupp_eq_sum_right {v : ι → E} (hv : Orthonormal 𝕜 v) (l₁ l₂ : ι →₀ 𝕜) :
-    ⟪Finsupp.total ι E 𝕜 v l₁, Finsupp.total ι E 𝕜 v l₂⟫ = l₂.sum fun i y => conj (l₁ i) * y := by
+    ⟪Finsupp.total 𝕜 v l₁, Finsupp.total 𝕜 v l₂⟫ = l₂.sum fun i y => conj (l₁ i) * y := by
   simp only [l₂.total_apply _, Finsupp.inner_sum, hv.inner_left_finsupp, mul_comm, smul_eq_mul]
 
 /-- The inner product of two linear combinations of a set of orthonormal vectors, expressed as
@@ -900,7 +900,7 @@ theorem Orthonormal.linearIndependent {v : ι → E} (hv : Orthonormal 𝕜 v) :
   rw [linearIndependent_iff]
   intro l hl
   ext i
-  have key : ⟪v i, Finsupp.total ι E 𝕜 v l⟫ = ⟪v i, 0⟫ := by rw [hl]
+  have key : ⟪v i, Finsupp.total 𝕜 v l⟫ = ⟪v i, 0⟫ := by rw [hl]
   simpa only [hv.inner_right_finsupp, inner_zero_right] using key
 
 /-- A subfamily of an orthonormal family (i.e., a composition with an injective map) is an
@@ -932,7 +932,7 @@ theorem Orthonormal.toSubtypeRange {v : ι → E} (hv : Orthonormal 𝕜 v) :
 set. -/
 theorem Orthonormal.inner_finsupp_eq_zero {v : ι → E} (hv : Orthonormal 𝕜 v) {s : Set ι} {i : ι}
     (hi : i ∉ s) {l : ι →₀ 𝕜} (hl : l ∈ Finsupp.supported 𝕜 𝕜 s) :
-    ⟪Finsupp.total ι E 𝕜 v l, v i⟫ = 0 := by
+    ⟪Finsupp.total 𝕜 v l, v i⟫ = 0 := by
   rw [Finsupp.mem_supported'] at hl
   simp only [hv.inner_left_finsupp, hl i hi, map_zero]
 

Mathlib/Analysis/InnerProductSpace/Projection.lean

@@ -1329,7 +1329,7 @@ theorem maximal_orthonormal_iff_orthogonalComplement_eq_bot (hv : Orthonormal 
     intro hxv y hy
     have hxv' : (⟨x, hxu⟩ : u) ∉ ((↑) ⁻¹' v : Set u) := by simp [huv, hxv]
     obtain ⟨l, hl, rfl⟩ :
-      ∃ l ∈ Finsupp.supported 𝕜 𝕜 ((↑) ⁻¹' v : Set u), (Finsupp.total (↥u) E 𝕜 (↑)) l = y := by
+      ∃ l ∈ Finsupp.supported 𝕜 𝕜 ((↑) ⁻¹' v : Set u), (Finsupp.total 𝕜 ((↑) : u → E)) l = y := by
       rw [← Finsupp.mem_span_image_iff_total]
       simp [huv, inter_eq_self_of_subset_right, hy]
     exact hu.inner_finsupp_eq_zero hxv' hl

Mathlib/Data/Finsupp/Weight.lean

@@ -72,7 +72,7 @@ variable [AddCommMonoid M]
 /-- The `weight` of the finitely supported function `f : σ →₀ ℕ`
 with respect to `w : σ → M` is the sum `∑(f i)•(w i)`. -/
 noncomputable def weight : (σ →₀ ℕ) →+ M :=
-  (Finsupp.total σ M ℕ w).toAddMonoidHom
+  (Finsupp.total ℕ w).toAddMonoidHom
 
 @[deprecated weight (since := "2024-07-20")]
 alias _root_.MvPolynomial.weightedDegree := weight

Mathlib/LinearAlgebra/Basis/Basic.lean

@@ -51,7 +51,7 @@ end Coord
 protected theorem linearIndependent : LinearIndependent R b :=
   linearIndependent_iff.mpr fun l hl =>
     calc
-      l = b.repr (Finsupp.total _ _ _ b l) := (b.repr_total l).symm
+      l = b.repr (Finsupp.total _ b l) := (b.repr_total l).symm
       _ = 0 := by rw [hl, LinearEquiv.map_zero]
 
 protected theorem ne_zero [Nontrivial R] (i) : b i ≠ 0 :=
@@ -227,7 +227,7 @@ variable (hli : LinearIndependent R v) (hsp : ⊤ ≤ span R (range v))
 protected noncomputable def mk : Basis ι R M :=
   .ofRepr
     { hli.repr.comp (LinearMap.id.codRestrict _ fun _ => hsp Submodule.mem_top) with
-      invFun := Finsupp.total _ _ _ v
+      invFun := Finsupp.total _ v
       left_inv := fun x => hli.total_repr ⟨x, _⟩
       right_inv := fun _ => hli.repr_eq rfl }
 
@@ -236,7 +236,7 @@ theorem mk_repr : (Basis.mk hli hsp).repr x = hli.repr ⟨x, hsp Submodule.mem_t
   rfl
 
 theorem mk_apply (i : ι) : Basis.mk hli hsp i = v i :=
-  show Finsupp.total _ _ _ v _ = v i by simp
+  show Finsupp.total _ v _ = v i by simp
 
 @[simp]
 theorem coe_mk : ⇑(Basis.mk hli hsp) = v :=

Mathlib/LinearAlgebra/Basis/Cardinality.lean

@@ -103,7 +103,7 @@ theorem union_support_maximal_linearIndependent_eq_range_basis {ι : Type w} (b
     intro l z
     rw [Finsupp.total_option] at z
     simp only [v', Option.elim'] at z
-    change _ + Finsupp.total κ M R v l.some = 0 at z
+    change _ + Finsupp.total R v l.some = 0 at z
     -- We have some linear combination of `b b'` and the `v i`, which we want to show is trivial.
     -- We'll first show the coefficient of `b b'` is zero,
     -- by expressing the `v i` in the basis `b`, and using that the `v i` have no `b b'` term.

Mathlib/LinearAlgebra/Basis/Defs.lean

@@ -134,23 +134,23 @@ theorem repr_self_apply (j) [Decidable (i = j)] : b.repr (b i) j = if i = j then
   rw [repr_self, Finsupp.single_apply]
 
 @[simp]
-theorem repr_symm_apply (v) : b.repr.symm v = Finsupp.total ι M R b v :=
+theorem repr_symm_apply (v) : b.repr.symm v = Finsupp.total R b v :=
   calc
     b.repr.symm v = b.repr.symm (v.sum Finsupp.single) := by simp
     _ = v.sum fun i vi => b.repr.symm (Finsupp.single i vi) := map_finsupp_sum ..
-    _ = Finsupp.total ι M R b v := by simp only [repr_symm_single, Finsupp.total_apply]
+    _ = Finsupp.total R b v := by simp only [repr_symm_single, Finsupp.total_apply]
 
 @[simp]
-theorem coe_repr_symm : ↑b.repr.symm = Finsupp.total ι M R b :=
+theorem coe_repr_symm : ↑b.repr.symm = Finsupp.total R b :=
   LinearMap.ext fun v => b.repr_symm_apply v
 
 @[simp]
-theorem repr_total (v) : b.repr (Finsupp.total _ _ _ b v) = v := by
+theorem repr_total (v) : b.repr (Finsupp.total _ b v) = v := by
   rw [← b.coe_repr_symm]
   exact b.repr.apply_symm_apply v
 
 @[simp]
-theorem total_repr : Finsupp.total _ _ _ b (b.repr x) = x := by
+theorem total_repr : Finsupp.total _ b (b.repr x) = x := by
   rw [← b.coe_repr_symm]
   exact b.repr.symm_apply_apply x
 
@@ -551,7 +551,7 @@ you can recover an `AddEquiv` by setting `S := ℕ`.
 See library note [bundled maps over different rings].
 -/
 def constr : (ι → M') ≃ₗ[S] M →ₗ[R] M' where
-  toFun f := (Finsupp.total M' M' R id).comp <| Finsupp.lmapDomain R R f ∘ₗ ↑b.repr
+  toFun f := (Finsupp.total R id).comp <| Finsupp.lmapDomain R R f ∘ₗ ↑b.repr
   invFun f i := f (b i)
   left_inv f := by
     ext
@@ -567,7 +567,7 @@ def constr : (ι → M') ≃ₗ[S] M →ₗ[R] M' where
     simp
 
 theorem constr_def (f : ι → M') :
-    constr (M' := M') b S f = Finsupp.total M' M' R id ∘ₗ Finsupp.lmapDomain R R f ∘ₗ ↑b.repr :=
+    constr (M' := M') b S f = Finsupp.total R id ∘ₗ Finsupp.lmapDomain R R f ∘ₗ ↑b.repr :=
   rfl
 
 theorem constr_apply (f : ι → M') (x : M) :

Mathlib/LinearAlgebra/DFinsupp.lean

@@ -429,7 +429,7 @@ theorem lsum_comp_mapRange_toSpanSingleton [∀ m : R, Decidable (m ≠ 0)] (p :
         ((mapRange.linearMap fun i => LinearMap.toSpanSingleton R (↥(p i)) ⟨v i, hv i⟩ :
               _ →ₗ[R] _).comp
           (finsuppLequivDFinsupp R : (ι →₀ R) ≃ₗ[R] _).toLinearMap) =
-      Finsupp.total ι N R v := by
+      Finsupp.total R v := by
   ext
   simp