From a548273680cd9c324996f79165ed5f8426bc1968 Mon Sep 17 00:00:00 2001
From: yuanyi-350 <kysyy1@126.com>
Date: Sat, 25 Apr 2026 19:43:35 +0800
Subject: [PATCH 1/2] refactor(Analysis): golf \

---
 Mathlib/Analysis/Analytic/OfScalars.lean | 23 +++++++----------------
 1 file changed, 7 insertions(+), 16 deletions(-)

diff --git a/Mathlib/Analysis/Analytic/OfScalars.lean b/Mathlib/Analysis/Analytic/OfScalars.lean
index b84df5d936ab81..712002e39cf022 100644
--- a/Mathlib/Analysis/Analytic/OfScalars.lean
+++ b/Mathlib/Analysis/Analytic/OfScalars.lean
@@ -64,15 +64,9 @@ theorem ofScalars_series_of_subsingleton [Subsingleton E] : ofScalars E c = 0 :=
 
 variable (𝕜) in
 theorem ofScalars_series_injective [Nontrivial E] : Function.Injective (ofScalars E (𝕜 := 𝕜)) := by
-  intro _ _
-  refine Function.mtr fun h ↦ ?_
-  simp_rw [FormalMultilinearSeries.ext_iff, ofScalars, ContinuousMultilinearMap.ext_iff,
-    ContinuousMultilinearMap.smul_apply]
-  push Not
-  obtain ⟨n, hn⟩ := Function.ne_iff.1 h
-  refine ⟨n, fun _ ↦ 1, ?_⟩
-  simp only [mkPiAlgebraFin_apply, List.ofFn_const, List.prod_replicate, one_pow, ne_eq]
-  exact (smul_left_injective 𝕜 one_ne_zero).ne hn
+  intro c c' h
+  funext n
+  simpa [ofScalars] using congrArg (fun p => p n fun _ ↦ (1 : E)) h
 
 variable (c)
 
@@ -91,19 +85,16 @@ lemma coeff_ofScalars {𝕜 : Type*} [NontriviallyNormedField 𝕜] {p : ℕ →
     (FormalMultilinearSeries.ofScalars 𝕜 p).coeff n = p n := by
   simp [FormalMultilinearSeries.coeff, FormalMultilinearSeries.ofScalars, List.prod_ofFn]
 
-set_option backward.isDefEq.respectTransparency false in
 theorem ofScalars_add (c' : ℕ → 𝕜) : ofScalars E (c + c') = ofScalars E c + ofScalars E c' := by
-  unfold ofScalars
-  simp_rw [Pi.add_apply, Pi.add_def _ _]
-  exact funext fun n ↦ Module.add_smul (c n) (c' n) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E)
+  ext n x
+  simp [ofScalars, add_smul]
 
 lemma ofScalars_sub (c' : ℕ → 𝕜) : ofScalars E (c - c') = ofScalars E c - ofScalars E c' := by
   ext; simp [ofScalars, sub_smul]
 
-set_option backward.isDefEq.respectTransparency false in
 theorem ofScalars_smul (x : 𝕜) : ofScalars E (x • c) = x • ofScalars E c := by
-  unfold ofScalars
-  simp [Pi.smul_def x _, smul_smul]
+  ext n y
+  simp [ofScalars, smul_smul]
 
 theorem ofScalars_comp_neg_id :
     (ofScalars E c).compContinuousLinearMap (-ContinuousLinearMap.id _ _) =

From 8b14f261d99692f7e1f3422ea7946266ee7494ae Mon Sep 17 00:00:00 2001
From: "Yi.Yuan" <kysyy1@126.com>
Date: Sat, 25 Apr 2026 19:51:15 +0800
Subject: [PATCH 2/2] Update OfScalars.lean

---
 Mathlib/Analysis/Analytic/OfScalars.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Analysis/Analytic/OfScalars.lean b/Mathlib/Analysis/Analytic/OfScalars.lean
index 712002e39cf022..8a91ddbc4edb93 100644
--- a/Mathlib/Analysis/Analytic/OfScalars.lean
+++ b/Mathlib/Analysis/Analytic/OfScalars.lean
@@ -66,7 +66,7 @@ variable (𝕜) in
 theorem ofScalars_series_injective [Nontrivial E] : Function.Injective (ofScalars E (𝕜 := 𝕜)) := by
   intro c c' h
   funext n
-  simpa [ofScalars] using congrArg (fun p => p n fun _ ↦ (1 : E)) h
+  simpa [ofScalars] using congrArg (fun p ↦ p n fun _ ↦ (1 : E)) h
 
 variable (c)