perf: make the support of onFinset opaque

Mathlib/Data/Finsupp/Defs.lean

@@ -215,36 +215,40 @@ section OnFinset
 
 variable [Zero M]
 
+private irreducible_def onFinset_support (s : Finset α) (f : α → M) : Finset α :=
+  haveI := Classical.decEq M
+  {a ∈ s | f a ≠ 0}
+
 /-- `Finsupp.onFinset s f hf` is the finsupp function representing `f` restricted to the finset `s`.
 The function must be `0` outside of `s`. Use this when the set needs to be filtered anyways,
 otherwise a better set representation is often available. -/
 def onFinset (s : Finset α) (f : α → M) (hf : ∀ a, f a ≠ 0 → a ∈ s) : α →₀ M where
-  support :=
-    haveI := Classical.decEq M
-    {a ∈ s | f a ≠ 0}
+  support := onFinset_support s f
   toFun := f
-  mem_support_toFun := by classical simpa
+  mem_support_toFun := by classical simpa [onFinset_support_def]
 
 @[simp, norm_cast] lemma coe_onFinset (s : Finset α) (f : α → M) (hf) : onFinset s f hf = f := rfl
 
 @[simp]
 theorem onFinset_apply {s : Finset α} {f : α → M} {hf a} : (onFinset s f hf : α →₀ M) a = f a :=
   rfl
 
+theorem support_onFinset [DecidableEq M] {s : Finset α} {f : α → M}
+    (hf : ∀ a : α, f a ≠ 0 → a ∈ s) :
+    (Finsupp.onFinset s f hf).support = {a ∈ s | f a ≠ 0} := by
+  dsimp [onFinset]; rw [onFinset_support]; congr
+
 @[simp]
 theorem support_onFinset_subset {s : Finset α} {f : α → M} {hf} :
     (onFinset s f hf).support ⊆ s := by
-  classical convert filter_subset (f · ≠ 0) s
+  classical
+  rw [support_onFinset]
+  exact filter_subset (f · ≠ 0) s
 
 theorem mem_support_onFinset {s : Finset α} {f : α → M} (hf : ∀ a : α, f a ≠ 0 → a ∈ s) {a : α} :
     a ∈ (Finsupp.onFinset s f hf).support ↔ f a ≠ 0 := by
   rw [Finsupp.mem_support_iff, Finsupp.onFinset_apply]
 
-theorem support_onFinset [DecidableEq M] {s : Finset α} {f : α → M}
-    (hf : ∀ a : α, f a ≠ 0 → a ∈ s) :
-    (Finsupp.onFinset s f hf).support = {a ∈ s | f a ≠ 0} := by
-  dsimp [onFinset]; congr
-
 end OnFinset
 
 section OfSupportFinite

Mathlib/RingTheory/AlgebraTower.lean

@@ -68,10 +68,15 @@ variable (b : Basis ι R M) (h : Function.Bijective (algebraMap R A))
 
 /-- If `R` and `A` have a bijective `algebraMap R A` and act identically on `M`,
 then a basis for `M` as `R`-module is also a basis for `M` as `R'`-module. -/
-@[simps! repr_apply_support_val repr_apply_toFun]
+@[simps! repr_apply_toFun]
 noncomputable def Basis.algebraMapCoeffs : Basis ι A M :=
   b.mapCoeffs (RingEquiv.ofBijective _ h) fun c x => by simp
 
+@[simp]
+theorem Basis.algebraMapCoeffs_repr (m : M) :
+    (b.algebraMapCoeffs A h).repr m = (b.repr m).mapRange (algebraMap R A) (map_zero _) := by
+  rfl
+
 theorem Basis.algebraMapCoeffs_apply (i : ι) : b.algebraMapCoeffs A h i = b i :=
   b.mapCoeffs_apply _ _ _
 

Mathlib/RingTheory/MvPowerSeries/Basic.lean

@@ -343,7 +343,7 @@ variable (σ) (R)
 def C : R →+* MvPowerSeries σ R :=
   { monomial R (0 : σ →₀ ℕ) with
     map_one' := rfl
-    map_mul' := fun a b => (monomial_mul_monomial 0 0 a b).symm
+    map_mul' := fun a b => Eq.trans (by simp) (monomial_mul_monomial _ _ a b).symm
     map_zero' := (monomial R 0).map_zero }
 
 variable {σ} {R}