From 17b2f6ff676a84cf9b552d066530cfdffe1091d0 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Fri, 24 Apr 2026 09:00:11 +0800 Subject: [PATCH 1/2] refactor(Analysis): golf IteratedFDeriv --- Mathlib/Analysis/Analytic/IteratedFDeriv.lean | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) diff --git a/Mathlib/Analysis/Analytic/IteratedFDeriv.lean b/Mathlib/Analysis/Analytic/IteratedFDeriv.lean index 3800e8c99e9a1f..a82f6110453b2f 100644 --- a/Mathlib/Analysis/Analytic/IteratedFDeriv.lean +++ b/Mathlib/Analysis/Analytic/IteratedFDeriv.lean @@ -127,17 +127,9 @@ lemma ContinuousMultilinearMap.iteratedFDeriv_comp_diagonal rw [← sum_comp (Equiv.embeddingEquivOfFinite (Fin n))] congr with σ congr with i - have A : ∃ y, σ y = i := by - have : Function.Bijective σ := (Fintype.bijective_iff_injective_and_card _).2 ⟨σ.injective, rfl⟩ - exact this.surjective i - rcases A with ⟨y, rfl⟩ - simp only [EmbeddingLike.apply_eq_iff_eq, exists_eq, ↓reduceDIte, - Function.Embedding.toEquivRange_symm_apply_self, ContinuousLinearMap.coe_pi', - ContinuousLinearMap.coe_id', id_eq, g] - congr 1 - symm + obtain ⟨y, rfl⟩ := σ.equivOfFiniteSelfEmbedding.surjective i simp [inv_apply, Perm.inv_def, - ofBijective_symm_apply_apply, Function.Embedding.equivOfFiniteSelfEmbedding] + ofBijective_symm_apply_apply, Function.Embedding.equivOfFiniteSelfEmbedding, g] private lemma HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum_of_subset (h : HasFPowerSeriesWithinOnBall f p s x r) (h' : AnalyticOn 𝕜 f s) From f85943b72719b7738cffba8906666c2a2ebbc5da Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Fri, 24 Apr 2026 14:21:38 +0800 Subject: [PATCH 2/2] golf --- Mathlib/Analysis/Analytic/IteratedFDeriv.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Analysis/Analytic/IteratedFDeriv.lean b/Mathlib/Analysis/Analytic/IteratedFDeriv.lean index a82f6110453b2f..61168105022f72 100644 --- a/Mathlib/Analysis/Analytic/IteratedFDeriv.lean +++ b/Mathlib/Analysis/Analytic/IteratedFDeriv.lean @@ -128,8 +128,7 @@ lemma ContinuousMultilinearMap.iteratedFDeriv_comp_diagonal congr with σ congr with i obtain ⟨y, rfl⟩ := σ.equivOfFiniteSelfEmbedding.surjective i - simp [inv_apply, Perm.inv_def, - ofBijective_symm_apply_apply, Function.Embedding.equivOfFiniteSelfEmbedding, g] + simp [Function.Embedding.equivOfFiniteSelfEmbedding, g] private lemma HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum_of_subset (h : HasFPowerSeriesWithinOnBall f p s x r) (h' : AnalyticOn 𝕜 f s)