From 868f3499d72c038be8f2e1af09339d67204e6153 Mon Sep 17 00:00:00 2001 From: David Renshaw Date: Wed, 11 Dec 2024 09:46:55 +0000 Subject: [PATCH] chore(Analysis/SpecialFunctions/Integrals): simplify proof of intervalIntegrable_cpow (#19877) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * `have : Ioc c 0 = Ioo c 0 ∪ {(0 : ℝ)} ` is directly proved by `(Ioo_union_right hc).symm` * That shorter proof can then be inlined at its use in the `simp` in the next line. This simplification was found by [`tryAtEachStep`](https://github.com/dwrensha/tryAtEachStep). --- Mathlib/Analysis/SpecialFunctions/Integrals.lean | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/Mathlib/Analysis/SpecialFunctions/Integrals.lean b/Mathlib/Analysis/SpecialFunctions/Integrals.lean index f80d1afa00a62..b3b78b374fb6f 100644 --- a/Mathlib/Analysis/SpecialFunctions/Integrals.lean +++ b/Mathlib/Analysis/SpecialFunctions/Integrals.lean @@ -140,10 +140,7 @@ theorem intervalIntegrable_cpow {r : ℂ} (h : 0 ≤ r.re ∨ (0 : ℝ) ∉ [[a, · -- case `c < 0`: integrand is identically constant, *except* at `x = 0` if `r ≠ 0`. apply IntervalIntegrable.symm rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hc.le] - have : Ioc c 0 = Ioo c 0 ∪ {(0 : ℝ)} := by - rw [← Ioo_union_Icc_eq_Ioc hc (le_refl 0), ← Icc_def] - simp_rw [← le_antisymm_iff, setOf_eq_eq_singleton'] - rw [this, integrableOn_union, and_comm]; constructor + rw [← Ioo_union_right hc, integrableOn_union, and_comm]; constructor · refine integrableOn_singleton_iff.mpr (Or.inr ?_) exact isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure.lt_top_of_isCompact isCompact_singleton