From 98e7f848728b4be7a0d22d85ec3a839a08e170d7 Mon Sep 17 00:00:00 2001 From: yuanyi-350 Date: Thu, 23 Apr 2026 16:32:07 +0800 Subject: [PATCH] refactor(NumberTheory): golf AbstractFuncEq --- Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean b/Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean index 0cd81ec05199da..ba9ee75e85b136 100644 --- a/Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean +++ b/Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean @@ -273,15 +273,9 @@ lemma hf_modif_int : fun_prop (discharger := assumption) refine LocallyIntegrableOn.add (fun x hx ↦ ?_) (fun x hx ↦ ?_) · obtain ⟨s, hs, hs'⟩ := P.hf_int.sub (locallyIntegrableOn_const _) x hx - refine ⟨s, hs, ?_⟩ - rw [IntegrableOn, integrable_indicator_iff measurableSet_Ioi, IntegrableOn, - Measure.restrict_restrict measurableSet_Ioi, ← IntegrableOn] - exact hs'.mono_set Set.inter_subset_right + exact ⟨s, hs, hs'.indicator measurableSet_Ioi⟩ · obtain ⟨s, hs, hs'⟩ := P.hf_int.sub this x hx - refine ⟨s, hs, ?_⟩ - rw [IntegrableOn, integrable_indicator_iff measurableSet_Ioo, IntegrableOn, - Measure.restrict_restrict measurableSet_Ioo, ← IntegrableOn] - exact hs'.mono_set Set.inter_subset_right + exact ⟨s, hs, hs'.indicator measurableSet_Ioo⟩ lemma hf_modif_FE (x : ℝ) (hx : 0 < x) : P.f_modif (1 / x) = (P.ε * ↑(x ^ P.k)) • P.g_modif x := by