feat(order/filter/pi): define filter.pi and prove some properties (#…

…10323)

src/analysis/box_integral/box/subbox_induction.lean

@@ -144,7 +144,7 @@ begin
       ⟨I.upper, λ x ⟨m, hm⟩, hm ▸ (hJl_mem m).2⟩,
   have hJuz : tendsto (λ m, (J m).upper) at_top (𝓝 z),
   { suffices : tendsto (λ m, (J m).upper - (J m).lower) at_top (𝓝 0), by simpa using hJlz.add this,
-    refine tendsto_pi.2 (λ i, _),
+    refine tendsto_pi_nhds.2 (λ i, _),
     simpa [hJsub] using tendsto_const_nhds.div_at_top
       (tendsto_pow_at_top_at_top_of_one_lt (@one_lt_two ℝ _ _)) },
   replace hJlz : tendsto (λ m, (J m).lower) at_top (𝓝[Icc I.lower I.upper] z),

src/analysis/calculus/tangent_cone.lean

@@ -197,7 +197,7 @@ begin
     exact ⟨z - x j, by simpa using hzs, by simpa using hz⟩ },
   choose! d' hd's hcd',
   refine ⟨c, λ n, function.update (d' n) i (d n), hd.mono (λ n hn j hj', _), hc,
-    tendsto_pi.2 $ λ j, _⟩,
+    tendsto_pi_nhds.2 $ λ j, _⟩,
   { rcases em (j = i) with rfl|hj; simp * },
   { rcases em (j = i) with rfl|hj,
     { simp [hy] },

src/measure_theory/constructions/borel_space.lean

@@ -1649,7 +1649,7 @@ lemma measurable_of_tendsto_nnreal' {ι} {f : ι → α → ℝ≥0} {g : α →
   measurable g :=
 begin
   rcases u.exists_seq_tendsto with ⟨x, hx⟩,
-  rw [tendsto_pi] at lim, rw [← measurable_coe_nnreal_ennreal_iff],
+  rw [tendsto_pi_nhds] at lim, rw [← measurable_coe_nnreal_ennreal_iff],
   have : ∀ y, liminf at_top (λ n, (f (x n) y : ℝ≥0∞)) = (g y : ℝ≥0∞) :=
     λ y, ((ennreal.continuous_coe.tendsto (g y)).comp $ (lim y).comp hx).liminf_eq,
   simp only [← this],
@@ -1674,7 +1674,7 @@ begin
   have : measurable (λ x, inf_nndist (g x) s),
   { suffices : tendsto (λ i x, inf_nndist (f i x) s) u (𝓝 (λ x, inf_nndist (g x) s)),
       from measurable_of_tendsto_nnreal' u (λ i, (hf i).inf_nndist) this,
-    rw [tendsto_pi] at lim ⊢, intro x,
+    rw [tendsto_pi_nhds] at lim ⊢, intro x,
     exact ((continuous_inf_nndist_pt s).tendsto (g x)).comp (lim x) },
   have h4s : g ⁻¹' s = (λ x, inf_nndist (g x) s) ⁻¹' {0},
   { ext x, simp [h1s, ← h1s.mem_iff_inf_dist_zero h2s, ← nnreal.coe_eq_zero] },
@@ -1698,7 +1698,7 @@ begin
   refine ⟨ae_seq_lim, _, (ite_ae_eq_of_measure_compl_zero g (λ x, (⟨f 0 x⟩ : nonempty β).some)
     (ae_seq_set hf p) (ae_seq.measure_compl_ae_seq_set_eq_zero hf hp)).symm⟩,
   refine measurable_of_tendsto_metric (@ae_seq.measurable α β _ _ _ f μ hf p) _,
-  refine tendsto_pi.mpr (λ x, _),
+  refine tendsto_pi_nhds.mpr (λ x, _),
   simp_rw [ae_seq, ae_seq_lim],
   split_ifs with hx,
   { simp_rw ae_seq.mk_eq_fun_of_mem_ae_seq_set hf hx,
@@ -1741,7 +1741,8 @@ begin
   { refine le_antisymm (le_of_eq (measure_mono_null _ hμ_compl)) (zero_le _),
     exact set.compl_subset_compl.mpr (λ x hx, hf_lim_conv x hx), },
   have h_f_lim_meas : measurable f_lim,
-    from measurable_of_tendsto_metric (ae_seq.measurable hf p) (tendsto_pi.mpr (λ x, hf_lim x)),
+    from measurable_of_tendsto_metric (ae_seq.measurable hf p)
+      (tendsto_pi_nhds.mpr (λ x, hf_lim x)),
   exact ⟨f_lim, h_f_lim_meas, h_ae_tendsto_f_lim⟩,
 end
 

src/measure_theory/constructions/pi.lean

@@ -407,9 +407,7 @@ variable {μ}
 lemma tendsto_eval_ae_ae {i : ι} : tendsto (eval i) (measure.pi μ).ae (μ i).ae :=
 λ s hs, pi_eval_preimage_null μ hs
 
--- TODO: should we introduce `filter.pi` and prove some basic facts about it?
--- The same combinator appears here and in `nhds_pi`
-lemma ae_pi_le_infi_comap : (measure.pi μ).ae ≤ ⨅ i, filter.comap (eval i) (μ i).ae :=
+lemma ae_pi_le_pi : (measure.pi μ).ae ≤ filter.pi (λ i, (μ i).ae) :=
 le_infi $ λ i, tendsto_eval_ae_ae.le_comap
 
 lemma ae_eq_pi {β : ι → Type*} {f f' : Π i, α i → β i} (h : ∀ i, f i =ᵐ[μ i] f' i) :

src/measure_theory/constructions/prod.lean

@@ -268,7 +268,7 @@ begin
     apply measurable_measure_prod_mk_left,
     exact (s n).measurable_set_fiber x },
   have h2f' : tendsto f' at_top (𝓝 (λ (x : α), ∫ (y : β), f x y ∂ν)),
-  { rw [tendsto_pi], intro x,
+  { rw [tendsto_pi_nhds], intro x,
     by_cases hfx : integrable (f x) ν,
     { have : ∀ n, integrable (s' n x) ν,
       { intro n, apply (hfx.norm.add hfx.norm).mono' (s' n x).measurable.ae_measurable,

src/measure_theory/function/strongly_measurable.lean

@@ -167,7 +167,7 @@ hf.fin_strongly_measurable_of_set_sigma_finite measurable_set.univ (by simp)
 protected lemma measurable [measurable_space α] [metric_space β] [measurable_space β]
   [borel_space β] (hf : strongly_measurable f) :
   measurable f :=
-measurable_of_tendsto_metric (λ n, (hf.approx n).measurable) (tendsto_pi.mpr hf.tendsto_approx)
+measurable_of_tendsto_metric (λ n, (hf.approx n).measurable) (tendsto_pi_nhds.mpr hf.tendsto_approx)
 
 section arithmetic
 variables [measurable_space α] [topological_space β]
@@ -270,7 +270,7 @@ end
 protected lemma measurable [metric_space β] [measurable_space β] [borel_space β]
   (hf : fin_strongly_measurable f μ) :
   measurable f :=
-measurable_of_tendsto_metric (λ n, (hf.some n).measurable) (tendsto_pi.mpr hf.some_spec.2)
+measurable_of_tendsto_metric (λ n, (hf.some n).measurable) (tendsto_pi_nhds.mpr hf.some_spec.2)
 
 protected lemma add {β} [topological_space β] [add_monoid β] [has_continuous_add β] {f g : α → β}
   (hf : fin_strongly_measurable f μ) (hg : fin_strongly_measurable g μ) :

src/measure_theory/measure/haar_lebesgue.lean

@@ -36,10 +36,8 @@ universe u
 def topological_space.positive_compacts.pi_Icc01 (ι : Type*) [fintype ι] :
   positive_compacts (ι → ℝ) :=
 ⟨set.pi set.univ (λ i, Icc 0 1), is_compact_univ_pi (λ i, is_compact_Icc),
-begin
-  rw interior_pi_set,
-  simp only [interior_Icc, univ_pi_nonempty_iff, nonempty_Ioo, implies_true_iff, zero_lt_one],
-end⟩
+by simp only [interior_pi_set, finite.of_fintype, interior_Icc, univ_pi_nonempty_iff, nonempty_Ioo,
+  implies_true_iff, zero_lt_one]⟩
 
 namespace measure_theory
 

src/order/filter/basic.lean

@@ -2718,71 +2718,6 @@ map_prod_map_coprod_le.trans (coprod_mono hf hg)
 
 end coprod
 
-/-! ### `n`-ary coproducts of filters -/
-
-section Coprod
-variables {δ : Type*} {κ : δ → Type*}  -- {f : Π d, filter (κ d)}
-
-/-- Coproduct of filters. -/
-protected def Coprod (f : Π d, filter (κ d)) : filter (Π d, κ d) :=
-⨆ d : δ, (f d).comap (λ k, k d)
-
-lemma mem_Coprod_iff {s : set (Π d, κ d)} {f : Π d, filter (κ d)} :
-  (s ∈ (filter.Coprod f)) ↔ (∀ d : δ, (∃ t₁ ∈ f d, (λ k : (Π d, κ d), k d) ⁻¹' t₁ ⊆ s)) :=
-by simp [filter.Coprod]
-
-lemma compl_mem_Coprod_iff {s : set (Π d, κ d)} {f : Π d, filter (κ d)} :
-  sᶜ ∈ filter.Coprod f ↔ ∃ t : Π d, set (κ d), (∀ d, (t d)ᶜ ∈ f d) ∧ s ⊆ set.pi univ t :=
-begin
-  rw [(surjective_pi_map (λ d, @compl_surjective (set (κ d)) _)).exists],
-  simp_rw [mem_Coprod_iff, classical.skolem, exists_prop, @subset_compl_comm _ _ s,
-    ← preimage_compl, ← subset_Inter_iff, ← univ_pi_eq_Inter, compl_compl]
-end
-
-lemma Coprod_ne_bot_iff' {f : Π d, filter (κ d)} :
-  ne_bot (filter.Coprod f) ↔ (∀ d, nonempty (κ d)) ∧ ∃ d, ne_bot (f d) :=
-by simp only [filter.Coprod, supr_ne_bot, ← exists_and_distrib_left, ← comap_eval_ne_bot_iff']
-
-@[simp] lemma Coprod_ne_bot_iff [∀ d, nonempty (κ d)] {f : Π d, filter (κ d)} :
-  ne_bot (filter.Coprod f) ↔ ∃ d, ne_bot (f d) :=
-by simp [Coprod_ne_bot_iff', *]
-
-lemma ne_bot.Coprod [∀ d, nonempty (κ d)] {f : Π d, filter (κ d)} {d : δ} (h : ne_bot (f d)) :
-  ne_bot (filter.Coprod f) :=
-Coprod_ne_bot_iff.2 ⟨d, h⟩
-
-@[instance] lemma Coprod_ne_bot [∀ d, nonempty (κ d)] [nonempty δ] (f : Π d, filter (κ d))
-  [H : ∀ d, ne_bot (f d)] : ne_bot (filter.Coprod f) :=
-(H (classical.arbitrary δ)).Coprod
-
-@[mono] lemma Coprod_mono {f₁ f₂ : Π d, filter (κ d)} (hf : ∀ d, f₁ d ≤ f₂ d) :
-  filter.Coprod f₁ ≤ filter.Coprod f₂ :=
-supr_le_supr $ λ d, comap_mono (hf d)
-
-lemma map_pi_map_Coprod_le {μ : δ → Type*}
-  {f : Π d, filter (κ d)} {m : Π d, κ d → μ d} :
-  map (λ (k : Π d, κ d), λ d, m d (k d)) (filter.Coprod f) ≤ filter.Coprod (λ d, map (m d) (f d)) :=
-begin
-  intros s h,
-  rw [mem_map', mem_Coprod_iff],
-  intros d,
-  rw mem_Coprod_iff at h,
-  obtain ⟨t, H, hH⟩ := h d,
-  rw mem_map at H,
-  refine ⟨{x : κ d | m d x ∈ t}, H, _⟩,
-  intros x hx,
-  simp only [mem_set_of_eq, preimage_set_of_eq] at hx,
-  rw mem_set_of_eq,
-  exact set.mem_of_subset_of_mem hH (mem_preimage.mpr hx),
-end
-
-lemma tendsto.pi_map_Coprod {μ : δ → Type*} {f : Π d, filter (κ d)} {m : Π d, κ d → μ d}
-  {g : Π d, filter (μ d)} (hf : ∀ d, tendsto (m d) (f d) (g d)) :
-  tendsto (λ (k : Π d, κ d), λ d, m d (k d)) (filter.Coprod f) (filter.Coprod g) :=
-map_pi_map_Coprod_le.trans (Coprod_mono hf)
-
-end Coprod
-
 end filter
 
 open_locale filter

src/order/filter/cofinite.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Jeremy Avigad, Yury Kudryashov
 -/
 import order.filter.at_top_bot
+import order.filter.pi
 
 /-!
 # The cofinite filter

src/order/filter/pi.lean

@@ -0,0 +1,191 @@
+/-
+Copyright (c) 2021 Yury G. Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury G. Kudryashov, Alex Kontorovich
+-/
+import order.filter.bases
+
+/-!
+# (Co)product of a family of filters
+
+In this file we define two filters on `Π i, α i` and prove some basic properties of these filters.
+
+* `filter.pi (f : Π i, filter (α i))` to be the maximal filter on `Π i, α i` such that
+  `∀ i, filter.tendsto (function.eval i) (filter.pi f) (f i)`. It is defined as
+  `Π i, filter.comap (function.eval i) (f i)`. This is a generalization of `filter.prod` to indexed
+  products.
+
+* `filter.Coprod (f : Π i, filter (α i))`: a generalization of `filter.coprod`; it is the supremum
+  of `comap (eval i) (f i)`.
+-/
+
+open set function
+open_locale classical filter
+
+namespace filter
+
+variables {ι : Type*} {α : ι → Type*} {f f₁ f₂ : Π i, filter (α i)} {s : Π i, set (α i)}
+
+section pi
+
+/-- The product of an indexed family of filters. -/
+def pi (f : Π i, filter (α i)) : filter (Π i, α i) := ⨅ i, comap (eval i) (f i)
+
+lemma tendsto_eval_pi (f : Π i, filter (α i)) (i : ι) :
+  tendsto (eval i) (pi f) (f i) :=
+tendsto_infi' i tendsto_comap
+
+lemma tendsto_pi {β : Type*} {m : β → Π i, α i} {l : filter β} :
+  tendsto m l (pi f) ↔ ∀ i, tendsto (λ x, m x i) l (f i) :=
+by simp only [pi, tendsto_infi, tendsto_comap_iff]
+
+lemma le_pi {g : filter (Π i, α i)} : g ≤ pi f ↔ ∀ i, tendsto (eval i) g (f i) := tendsto_pi
+
+@[mono] lemma pi_mono (h : ∀ i, f₁ i ≤ f₂ i) : pi f₁ ≤ pi f₂ :=
+infi_le_infi $ λ i, comap_mono $ h i
+
+lemma mem_pi_of_mem (i : ι) {s : set (α i)} (hs : s ∈ f i) :
+  eval i ⁻¹' s ∈ pi f :=
+mem_infi_of_mem i $ preimage_mem_comap hs
+
+lemma pi_mem_pi {I : set ι} (hI : finite I) (h : ∀ i ∈ I, s i ∈ f i) :
+  I.pi s ∈ pi f :=
+begin
+  rw [pi_def, bInter_eq_Inter],
+  refine mem_infi_of_Inter hI (λ i, _) subset.rfl,
+  exact preimage_mem_comap (h i i.2)
+end
+
+lemma mem_pi {s : set (Π i, α i)} : s ∈ pi f ↔
+  ∃ (I : set ι), finite I ∧ ∃ t : Π i, set (α i), (∀ i, t i ∈ f i) ∧ I.pi t ⊆ s :=
+begin
+  split,
+  { simp only [pi, mem_infi', mem_comap, pi_def],
+    rintro ⟨I, If, V, hVf, hVI, rfl, -⟩, choose t htf htV using hVf,
+    exact ⟨I, If, t, htf, bInter_mono (λ i _, htV i)⟩ },
+  { rintro ⟨I, If, t, htf, hts⟩,
+    exact mem_of_superset (pi_mem_pi If $ λ i _, htf i) hts }
+end
+
+lemma mem_pi' {s : set (Π i, α i)} : s ∈ pi f ↔
+  ∃ (I : finset ι), ∃ t : Π i, set (α i), (∀ i, t i ∈ f i) ∧ set.pi ↑I t ⊆ s :=
+mem_pi.trans exists_finite_iff_finset
+
+lemma mem_of_pi_mem_pi [∀ i, ne_bot (f i)] {I : set ι} (h : I.pi s ∈ pi f) {i : ι} (hi : i ∈ I) :
+  s i ∈ f i :=
+begin
+  rcases mem_pi.1 h with ⟨I', I'f, t, htf, hts⟩,
+  refine mem_of_superset (htf i) (λ x hx, _),
+  have : ∀ i, (t i).nonempty, from λ i, nonempty_of_mem (htf i),
+  choose g hg,
+  have : update g i x ∈ I'.pi t,
+  { intros j hj, rcases eq_or_ne j i with (rfl|hne); simp * },
+  simpa using hts this i hi
+end
+
+@[simp] lemma pi_mem_pi_iff [∀ i, ne_bot (f i)] {I : set ι} (hI : finite I) :
+  I.pi s ∈ pi f ↔ ∀ i ∈ I, s i ∈ f i :=
+⟨λ h i hi, mem_of_pi_mem_pi h hi, pi_mem_pi hI⟩
+
+@[simp] lemma pi_inf_principal_univ_pi_eq_bot :
+  pi f ⊓ 𝓟 (set.pi univ s) = ⊥ ↔ ∃ i, f i ⊓ 𝓟 (s i) = ⊥ :=
+begin
+  split,
+  { simp only [inf_principal_eq_bot, mem_pi], contrapose!,
+    rintros (hsf : ∀ i, ∃ᶠ x in f i, x ∈ s i) I If t htf hts,
+    have : ∀ i, (s i ∩ t i).nonempty, from λ i, ((hsf i).and_eventually (htf i)).exists,
+    choose x hxs hxt,
+    exact hts (λ i hi, hxt i) (mem_univ_pi.2 hxs) },
+  { simp only [inf_principal_eq_bot],
+    rintro ⟨i, hi⟩,
+    filter_upwards [mem_pi_of_mem i hi],
+    exact λ x, mt (λ h, h i trivial) }
+end
+
+@[simp] lemma pi_inf_principal_pi_eq_bot [Π i, ne_bot (f i)] {I : set ι} :
+  pi f ⊓ 𝓟 (set.pi I s) = ⊥ ↔ ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥ :=
+begin
+  rw [← univ_pi_piecewise I, pi_inf_principal_univ_pi_eq_bot],
+  refine exists_congr (λ i, _),
+  by_cases hi : i ∈ I; simp [hi, (‹Π i, ne_bot (f i)› i).ne]
+end
+
+@[simp] lemma pi_inf_principal_univ_pi_ne_bot :
+  ne_bot (pi f ⊓ 𝓟 (set.pi univ s)) ↔ ∀ i, ne_bot (f i ⊓ 𝓟 (s i)) :=
+by simp [ne_bot_iff]
+
+@[simp] lemma pi_inf_principal_pi_ne_bot [Π i, ne_bot (f i)] {I : set ι} :
+  ne_bot (pi f ⊓ 𝓟 (I.pi s)) ↔ ∀ i ∈ I, ne_bot (f i ⊓ 𝓟 (s i)) :=
+by simp [ne_bot_iff]
+
+instance pi_inf_principal_pi.ne_bot [h : ∀ i, ne_bot (f i ⊓ 𝓟 (s i))] {I : set ι} :
+  ne_bot (pi f ⊓ 𝓟 (I.pi s)) :=
+(pi_inf_principal_univ_pi_ne_bot.2 ‹_›).mono $ inf_le_inf_left _ $ principal_mono.2 $
+  λ x hx i hi, hx i trivial
+
+@[simp] lemma pi_eq_bot : pi f = ⊥ ↔ ∃ i, f i = ⊥ :=
+by simpa using @pi_inf_principal_univ_pi_eq_bot ι α f (λ _, univ)
+
+@[simp] lemma pi_ne_bot : ne_bot (pi f) ↔ ∀ i, ne_bot (f i) := by simp [ne_bot_iff]
+
+instance [∀ i, ne_bot (f i)] : ne_bot (pi f) := pi_ne_bot.2 ‹_›
+
+end pi
+
+/-! ### `n`-ary coproducts of filters -/
+
+section Coprod
+
+/-- Coproduct of filters. -/
+protected def Coprod (f : Π i, filter (α i)) : filter (Π i, α i) :=
+⨆ i : ι, comap (eval i) (f i)
+
+lemma mem_Coprod_iff {s : set (Π i, α i)} :
+  (s ∈ filter.Coprod f) ↔ (∀ i : ι, (∃ t₁ ∈ f i, eval i ⁻¹' t₁ ⊆ s)) :=
+by simp [filter.Coprod]
+
+lemma compl_mem_Coprod_iff {s : set (Π i, α i)} :
+  sᶜ ∈ filter.Coprod f ↔ ∃ t : Π i, set (α i), (∀ i, (t i)ᶜ ∈ f i) ∧ s ⊆ set.pi univ (λ i, t i) :=
+begin
+  rw [(surjective_pi_map (λ i, @compl_surjective (set (α i)) _)).exists],
+  simp_rw [mem_Coprod_iff, classical.skolem, exists_prop, @subset_compl_comm _ _ s,
+    ← preimage_compl, ← subset_Inter_iff, ← univ_pi_eq_Inter, compl_compl]
+end
+
+lemma Coprod_ne_bot_iff' :
+  ne_bot (filter.Coprod f) ↔ (∀ i, nonempty (α i)) ∧ ∃ d, ne_bot (f d) :=
+by simp only [filter.Coprod, supr_ne_bot, ← exists_and_distrib_left, ← comap_eval_ne_bot_iff']
+
+@[simp] lemma Coprod_ne_bot_iff [∀ i, nonempty (α i)] :
+  ne_bot (filter.Coprod f) ↔ ∃ d, ne_bot (f d) :=
+by simp [Coprod_ne_bot_iff', *]
+
+lemma ne_bot.Coprod [∀ i, nonempty (α i)] {i : ι} (h : ne_bot (f i)) :
+  ne_bot (filter.Coprod f) :=
+Coprod_ne_bot_iff.2 ⟨i, h⟩
+
+@[instance] lemma Coprod_ne_bot [∀ i, nonempty (α i)] [nonempty ι] (f : Π i, filter (α i))
+  [H : ∀ i, ne_bot (f i)] : ne_bot (filter.Coprod f) :=
+(H (classical.arbitrary ι)).Coprod
+
+@[mono] lemma Coprod_mono (hf : ∀ i, f₁ i ≤ f₂ i) : filter.Coprod f₁ ≤ filter.Coprod f₂ :=
+supr_le_supr $ λ i, comap_mono (hf i)
+
+variables {β : ι → Type*} {m : Π i, α i → β i}
+
+lemma map_pi_map_Coprod_le :
+  map (λ (k : Π i, α i), λ i, m i (k i)) (filter.Coprod f) ≤ filter.Coprod (λ i, map (m i) (f i)) :=
+begin
+  simp only [le_def, mem_map, mem_Coprod_iff],
+  intros s h i,
+  obtain ⟨t, H, hH⟩ := h i,
+  exact ⟨{x : α i | m i x ∈ t}, H, λ x hx, hH hx⟩
+end
+
+lemma tendsto.pi_map_Coprod {g : Π i, filter (β i)} (h : ∀ i, tendsto (m i) (f i) (g i)) :
+  tendsto (λ (k : Π i, α i), λ i, m i (k i)) (filter.Coprod f) (filter.Coprod g) :=
+map_pi_map_Coprod_le.trans (Coprod_mono h)
+
+end Coprod
+
+end filter

src/topology/algebra/infinite_sum.lean

@@ -552,7 +552,7 @@ variables {ι : Type*} {π : α → Type*} [∀ x, add_comm_monoid (π x)] [∀
 
 lemma pi.has_sum {f : ι → ∀ x, π x} {g : ∀ x, π x} :
   has_sum f g ↔ ∀ x, has_sum (λ i, f i x) (g x) :=
-by simp only [has_sum, tendsto_pi, sum_apply]
+by simp only [has_sum, tendsto_pi_nhds, sum_apply]
 
 lemma pi.summable {f : ι → ∀ x, π x} : summable f ↔ ∀ x, summable (λ i, f i x) :=
 by simp only [summable, pi.has_sum, skolem]

src/topology/algebra/ordered/basic.lean

@@ -709,7 +709,7 @@ instance tendsto_Icc_class_nhds_pi {ι : Type*} {α : ι → Type*}
   tendsto_Ixx_class Icc (𝓝 f) (𝓝 f) :=
 begin
   constructor,
-  conv in ((𝓝 f).lift' powerset) { rw [nhds_pi] },
+  conv in ((𝓝 f).lift' powerset) { rw [nhds_pi, filter.pi] },
   simp only [lift'_infi_powerset, comap_lift'_eq2 monotone_powerset, tendsto_infi, tendsto_lift',
     mem_powerset_iff, subset_def, mem_preimage],
   intros i s hs,