fix(analysis/normed_space/lp_space): speedup by squeezing simps (#17098)

leanprover-community · Oct 21, 2022 · 2a2e7ae · 2a2e7ae
1 parent 6c6597f
commit 2a2e7ae
Showing 1 changed file with 6 additions and 3 deletions.
diff --git a/src/analysis/normed_space/lp_space.lean b/src/analysis/normed_space/lp_space.lean
@@ -924,11 +924,14 @@ begin
   have hF : ∀ i ∉ s, F i = 0,
   { intros i hi,
     suffices : ∥f i∥ ^ p.to_real - ∥f i - ite (i ∈ s) (f i) 0∥ ^ p.to_real = 0,
-    { simpa [F, coe_fn_sum, lp.single_apply] using this, },
-    simp [if_neg hi] },
+    { simpa only [F, coe_fn_sum, lp.single_apply, coe_fn_sub, pi.sub_apply, finset.sum_apply,
+        finset.sum_dite_eq] using this, },
+    simp only [if_neg hi, sub_zero, sub_self] },
   have hF' : ∀ i ∈ s, F i = ∥f i∥ ^ p.to_real,
   { intros i hi,
-    simp [F, coe_fn_sum, lp.single_apply, if_pos hi, real.zero_rpow hp.ne'] },
+    simp only [F, coe_fn_sum, lp.single_apply, if_pos hi, sub_self, eq_self_iff_true,
+      coe_fn_sub, pi.sub_apply, finset.sum_apply, finset.sum_dite_eq, sub_eq_self],
+    simp [real.zero_rpow hp.ne'], },
   have : has_sum F (∑ i in s, F i) := has_sum_sum_of_ne_finset_zero hF,
   rwa [finset.sum_congr rfl hF'] at this,
 end