refactor(order/filter/bases): turn is_countably_generated into a cl…

…ass (#9838)

## API changes

### Filters

* turn `filter.is_countably_generated` into a class, turn some lemmas into instances;
* remove definition/lemmas (all were in the `filter.is_countably_generated` namespace): `generating_set`, `countable_generating_set`, `eq_generate`, `countable_filter_basis`, `filter_basis_filter`, `has_countable_basis`, `exists_countable_infi_principal`, `exists_seq`;
* rename `filter.is_countably_generated.exists_antitone_subbasis` to `filter.has_basis.exists_antitone_subbasis`;
* rename `filter.is_countably_generated.exists_antitone_basis` to `filter.exists_antitone_basis`;
* rename `filter.is_countably_generated.exists_antitone_seq'` to `filter.exists_antitone_seq`;
* rename `filter.is_countably_generated.exists_seq` to `filter.exists_antitone_eq_infi_principal`;
* rename `filter.is_countably_generated.tendsto_iff_seq_tendsto` to `filter.tendsto_iff_seq_tendsto`;
* rename `filter.is_countably_generated.tendsto_of_seq_tendsto` to `filter.tendsto_of_seq_tendsto`;
* slightly generalize `is_countably_generated_at_top` and `is_countably_generated_at_bot`;
* add `filter.generate_eq_binfi`;

### Topology

* merge `is_closed.is_Gδ` with `is_closed.is_Gδ'`;
* merge `is_Gδ_set_of_continuous_at_of_countably_generated_uniformity` with `is_Gδ_set_of_continuous_at`;
* merge `is_lub.exists_seq_strict_mono_tendsto_of_not_mem'` with `is_lub.exists_seq_strict_mono_tendsto_of_not_mem`;
* merge `is_lub.exists_seq_monotone_tendsto'` with `is_lub.exists_seq_monotone_tendsto`;
* merge `is_glb.exists_seq_strict_anti_tendsto_of_not_mem'` with `is_glb.exists_seq_strict_anti_tendsto_of_not_mem`;
* merge `is_glb.exists_seq_antitone_tendsto'` with `is_glb.exists_seq_antitone_tendsto`;
* drop `emetric.first_countable_topology`, turn `uniform_space.first_countable_topology` into an instance;
* drop `emetric.second_countable_of_separable`, use `uniform_space.second_countable_of_separable` instead;
* drop `metric.compact_iff_seq_compact`, use `uniform_space.compact_iff_seq_compact` instead;
* drop `metric.compact_space_iff_seq_compact_space`, use `uniform_space.compact_space_iff_seq_compact_space` instead;

## Measure theory and integrals

Various lemmas assume `[is_countably_generated l]` instead of `(h : is_countably_generated l)`.

docs/overview.yaml

@@ -229,7 +229,7 @@ Topology:
   Metric spaces:
     metric space: 'metric_space'
     ball: 'metric.ball'
-    sequential compactness is equivalent to compactness (Bolzano-Weierstrass): 'metric.compact_iff_seq_compact'
+    sequential compactness is equivalent to compactness (Bolzano-Weierstrass): 'uniform_space.compact_iff_seq_compact'
     Heine-Borel theorem (proper metric space version): 'metric.compact_iff_closed_bounded'
     Lipschitz continuity: 'lipschitz_with'
     Hölder continuity: 'holder_with'

docs/undergrad.yaml

@@ -402,7 +402,7 @@ Topology:
     continuous functions: 'continuous'
     homeomorphisms: 'homeomorph'
     compactness in terms of open covers (Borel-Lebesgue): 'is_compact_iff_finite_subcover'
-    sequential compactness is equivalent to compactness (Bolzano-Weierstrass): 'metric.compact_iff_seq_compact'
+    sequential compactness is equivalent to compactness (Bolzano-Weierstrass): 'uniform_space.compact_iff_seq_compact'
     connectedness: 'connected_space'
     connected components: 'connected_component'
     path connectedness: 'is_path_connected'

src/analysis/calculus/parametric_integral.lean

@@ -107,7 +107,6 @@ begin
   rw [has_fderiv_at_iff_tendsto, tendsto_congr' this, ← tendsto_zero_iff_norm_tendsto_zero,
       ← show ∫ (a : α), ∥x₀ - x₀∥⁻¹ • (F x₀ a - F x₀ a - (F' a) (x₀ - x₀)) ∂μ = 0, by simp],
   apply tendsto_integral_filter_of_dominated_convergence,
-  { apply is_countably_generated_nhds },
   { filter_upwards [h_ball],
     intros x x_in,
     apply ae_measurable.const_smul,

src/measure_theory/function/ae_eq_of_integral.lean

@@ -138,7 +138,7 @@ begin
   push_neg at H h,
   obtain ⟨u, u_mono, u_lt, u_lim, -⟩ : ∃ (u : ℕ → β), strict_mono u ∧ (∀ (n : ℕ), u n < c)
       ∧ tendsto u at_top (nhds c) ∧ ∀ (n : ℕ), u n ∈ set.Iio c :=
-    H.exists_seq_strict_mono_tendsto_of_not_mem h (lt_irrefl c),
+    H.exists_seq_strict_mono_tendsto_of_not_mem (lt_irrefl c) h,
   have h_Union : {x | f x < c} = ⋃ (n : ℕ), {x | f x ≤ u n},
   { ext1 x,
     simp_rw [set.mem_Union, set.mem_set_of_eq],

src/measure_theory/integral/bochner.lean

@@ -861,34 +861,34 @@ end
 
 /-- Lebesgue dominated convergence theorem for filters with a countable basis -/
 lemma tendsto_integral_filter_of_dominated_convergence {ι} {l : filter ι}
+  [l.is_countably_generated]
   {F : ι → α → E} {f : α → E} (bound : α → ℝ)
-  (hl_cb : l.is_countably_generated)
   (hF_meas : ∀ᶠ n in l, ae_measurable (F n) μ)
   (f_measurable : ae_measurable f μ)
   (h_bound : ∀ᶠ n in l, ∀ᵐ a ∂μ, ∥F n a∥ ≤ bound a)
   (bound_integrable : integrable bound μ)
   (h_lim : ∀ᵐ a ∂μ, tendsto (λ n, F n a) l (𝓝 (f a))) :
   tendsto (λn, ∫ a, F n a ∂μ) l (𝓝 $ ∫ a, f a ∂μ) :=
 begin
-  rw hl_cb.tendsto_iff_seq_tendsto,
-  { intros x xl,
-    have hxl, { rw tendsto_at_top' at xl, exact xl },
-    have h := inter_mem hF_meas h_bound,
-    replace h := hxl _ h,
-    rcases h with ⟨k, h⟩,
-    rw ← tendsto_add_at_top_iff_nat k,
-    refine tendsto_integral_of_dominated_convergence _ _ _ _ _ _,
-    { exact bound },
-    { intro, refine (h _ _).1, exact nat.le_add_left _ _ },
+  rw tendsto_iff_seq_tendsto,
+  intros x xl,
+  have hxl, { rw tendsto_at_top' at xl, exact xl },
+  have h := inter_mem hF_meas h_bound,
+  replace h := hxl _ h,
+  rcases h with ⟨k, h⟩,
+  rw ← tendsto_add_at_top_iff_nat k,
+  refine tendsto_integral_of_dominated_convergence _ _ _ _ _ _,
+  { exact bound },
+  { intro, refine (h _ _).1, exact nat.le_add_left _ _ },
+  { assumption },
+  { assumption },
+  { intro, refine (h _ _).2, exact nat.le_add_left _ _ },
+  { filter_upwards [h_lim],
+    assume a h_lim,
+    apply @tendsto.comp _ _ _ (λn, x (n + k)) (λn, F n a),
     { assumption },
-    { assumption },
-    { intro, refine (h _ _).2, exact nat.le_add_left _ _ },
-    { filter_upwards [h_lim],
-      assume a h_lim,
-      apply @tendsto.comp _ _ _ (λn, x (n + k)) (λn, F n a),
-      { assumption },
-      rw tendsto_add_at_top_iff_nat,
-      assumption } },
+    rw tendsto_add_at_top_iff_nat,
+    assumption }
 end
 
 variables {X : Type*} [topological_space X] [first_countable_topology X]
@@ -898,9 +898,7 @@ lemma continuous_at_of_dominated {F : X → α → E} {x₀ : X} {bound : α →
   (h_bound : ∀ᶠ x in 𝓝 x₀, ∀ᵐ a ∂μ, ∥F x a∥ ≤ bound a)
   (bound_integrable : integrable bound μ) (h_cont : ∀ᵐ a ∂μ, continuous_at (λ x, F x a) x₀) :
   continuous_at (λ x, ∫ a, F x a ∂μ) x₀ :=
-tendsto_integral_filter_of_dominated_convergence bound
-  (first_countable_topology.nhds_generated_countable x₀) ‹_›
-    (mem_of_mem_nhds hF_meas : _) ‹_› ‹_› ‹_›
+tendsto_integral_filter_of_dominated_convergence bound ‹_› (mem_of_mem_nhds hF_meas : _) ‹_› ‹_› ‹_›
 
 lemma continuous_of_dominated {F : X → α → E} {bound : α → ℝ}
   (hF_meas : ∀ x, ae_measurable (F x) μ) (h_bound : ∀ x, ∀ᵐ a ∂μ, ∥F x a∥ ≤ bound a)

src/measure_theory/integral/integral_eq_improper.lean

@@ -239,22 +239,22 @@ begin
   exact tendsto_of_tendsto_of_tendsto_of_le_of_le lim₁ lim₂ le₁ le₂
 end
 
-lemma ae_cover.lintegral_tendsto_of_countably_generated {φ : ι → set α}
-  (hφ : ae_cover μ l φ) (hcg : l.is_countably_generated) {f : α → ℝ≥0∞}
+lemma ae_cover.lintegral_tendsto_of_countably_generated [l.is_countably_generated]
+  {φ : ι → set α} (hφ : ae_cover μ l φ) {f : α → ℝ≥0∞}
   (hfm : ae_measurable f μ) : tendsto (λ i, ∫⁻ x in φ i, f x ∂μ) l (𝓝 $ ∫⁻ x, f x ∂μ) :=
-hcg.tendsto_of_seq_tendsto (λ u hu, (hφ.comp_tendsto hu).lintegral_tendsto_of_nat hfm)
+tendsto_of_seq_tendsto (λ u hu, (hφ.comp_tendsto hu).lintegral_tendsto_of_nat hfm)
 
-lemma ae_cover.lintegral_eq_of_tendsto [l.ne_bot] {φ : ι → set α} (hφ : ae_cover μ l φ)
-  (hcg : l.is_countably_generated) {f : α → ℝ≥0∞} (I : ℝ≥0∞)
+lemma ae_cover.lintegral_eq_of_tendsto [l.ne_bot] [l.is_countably_generated]
+  {φ : ι → set α} (hφ : ae_cover μ l φ) {f : α → ℝ≥0∞} (I : ℝ≥0∞)
   (hfm : ae_measurable f μ) (htendsto : tendsto (λ i, ∫⁻ x in φ i, f x ∂μ) l (𝓝 I)) :
   ∫⁻ x, f x ∂μ = I :=
-tendsto_nhds_unique (hφ.lintegral_tendsto_of_countably_generated hcg hfm) htendsto
+tendsto_nhds_unique (hφ.lintegral_tendsto_of_countably_generated hfm) htendsto
 
-lemma ae_cover.supr_lintegral_eq_of_countably_generated [nonempty ι] [l.ne_bot] {φ : ι → set α}
-  (hφ : ae_cover μ l φ) (hcg : l.is_countably_generated) {f : α → ℝ≥0∞}
+lemma ae_cover.supr_lintegral_eq_of_countably_generated [nonempty ι] [l.ne_bot]
+  [l.is_countably_generated] {φ : ι → set α} (hφ : ae_cover μ l φ) {f : α → ℝ≥0∞}
   (hfm : ae_measurable f μ) : (⨆ (i : ι), ∫⁻ x in φ i, f x ∂μ) = ∫⁻ x, f x ∂μ :=
 begin
-  have := hφ.lintegral_tendsto_of_countably_generated hcg hfm,
+  have := hφ.lintegral_tendsto_of_countably_generated hfm,
   refine csupr_eq_of_forall_le_of_forall_lt_exists_gt
     (λ i, lintegral_mono' measure.restrict_le_self (le_refl _)) (λ w hw, _),
   rcases exists_between hw with ⟨m, hm₁, hm₂⟩,
@@ -269,33 +269,33 @@ section integrable
 variables {α ι E : Type*} [measurable_space α] {μ : measure α} {l : filter ι}
   [normed_group E] [measurable_space E] [opens_measurable_space E]
 
-lemma ae_cover.integrable_of_lintegral_nnnorm_tendsto [l.ne_bot] {φ : ι → set α}
-  (hφ : ae_cover μ l φ) (hcg : l.is_countably_generated) {f : α → E} (I : ℝ)
+lemma ae_cover.integrable_of_lintegral_nnnorm_tendsto [l.ne_bot] [l.is_countably_generated]
+  {φ : ι → set α} (hφ : ae_cover μ l φ) {f : α → E} (I : ℝ)
   (hfm : ae_measurable f μ)
   (htendsto : tendsto (λ i, ∫⁻ x in φ i, nnnorm (f x) ∂μ) l (𝓝 $ ennreal.of_real I)) :
   integrable f μ :=
 begin
   refine ⟨hfm, _⟩,
   unfold has_finite_integral,
-  rw hφ.lintegral_eq_of_tendsto hcg _ (measurable_nnnorm.comp_ae_measurable hfm).coe_nnreal_ennreal
+  rw hφ.lintegral_eq_of_tendsto _ (measurable_nnnorm.comp_ae_measurable hfm).coe_nnreal_ennreal
     htendsto,
   exact ennreal.of_real_lt_top
 end
 
-lemma ae_cover.integrable_of_lintegral_nnnorm_tendsto' [l.ne_bot] {φ : ι → set α}
-  (hφ : ae_cover μ l φ) (hcg : l.is_countably_generated) {f : α → E} (I : ℝ≥0)
+lemma ae_cover.integrable_of_lintegral_nnnorm_tendsto' [l.ne_bot] [l.is_countably_generated]
+  {φ : ι → set α} (hφ : ae_cover μ l φ) {f : α → E} (I : ℝ≥0)
   (hfm : ae_measurable f μ)
   (htendsto : tendsto (λ i, ∫⁻ x in φ i, nnnorm (f x) ∂μ) l (𝓝 $ ennreal.of_real I)) :
   integrable f μ :=
-hφ.integrable_of_lintegral_nnnorm_tendsto hcg I hfm htendsto
+hφ.integrable_of_lintegral_nnnorm_tendsto I hfm htendsto
 
-lemma ae_cover.integrable_of_integral_norm_tendsto [l.ne_bot] {φ : ι → set α}
-  (hφ : ae_cover μ l φ) (hcg : l.is_countably_generated) {f : α → E}
+lemma ae_cover.integrable_of_integral_norm_tendsto [l.ne_bot] [l.is_countably_generated]
+  {φ : ι → set α} (hφ : ae_cover μ l φ) {f : α → E}
   (I : ℝ) (hfm : ae_measurable f μ) (hfi : ∀ i, integrable_on f (φ i) μ)
   (htendsto : tendsto (λ i, ∫ x in φ i, ∥f x∥ ∂μ) l (𝓝 I)) :
   integrable f μ :=
 begin
-  refine hφ.integrable_of_lintegral_nnnorm_tendsto hcg I hfm _,
+  refine hφ.integrable_of_lintegral_nnnorm_tendsto I hfm _,
   conv at htendsto in (integral _ _)
   { rw integral_eq_lintegral_of_nonneg_ae (ae_of_all _ (λ x, @norm_nonneg E _ (f x)))
     hfm.norm.restrict },
@@ -306,12 +306,12 @@ begin
   exact ne_top_of_lt (hfi i).2
 end
 
-lemma ae_cover.integrable_of_integral_tendsto_of_nonneg_ae [l.ne_bot] {φ : ι → set α}
-  (hφ : ae_cover μ l φ) (hcg : l.is_countably_generated) {f : α → ℝ} (I : ℝ)
+lemma ae_cover.integrable_of_integral_tendsto_of_nonneg_ae [l.ne_bot] [l.is_countably_generated]
+  {φ : ι → set α} (hφ : ae_cover μ l φ) {f : α → ℝ} (I : ℝ)
   (hfm : ae_measurable f μ) (hfi : ∀ i, integrable_on f (φ i) μ) (hnng : ∀ᵐ x ∂μ, 0 ≤ f x)
   (htendsto : tendsto (λ i, ∫ x in φ i, f x ∂μ) l (𝓝 I)) :
   integrable f μ :=
-hφ.integrable_of_integral_norm_tendsto hcg I hfm hfi
+hφ.integrable_of_integral_norm_tendsto I hfm hfi
   (htendsto.congr $ λ i, integral_congr_ae $ ae_restrict_of_ae $ hnng.mono $
     λ x hx, (real.norm_of_nonneg hx).symm)
 
@@ -323,34 +323,34 @@ variables {α ι E : Type*} [measurable_space α] {μ : measure α} {l : filter
   [normed_group E] [normed_space ℝ E] [measurable_space E] [borel_space E]
   [complete_space E] [second_countable_topology E]
 
-lemma ae_cover.integral_tendsto_of_countably_generated {φ : ι → set α} (hφ : ae_cover μ l φ)
-  (hcg : l.is_countably_generated) {f : α → E} (hfm : ae_measurable f μ)
+lemma ae_cover.integral_tendsto_of_countably_generated [l.is_countably_generated]
+  {φ : ι → set α} (hφ : ae_cover μ l φ) {f : α → E} (hfm : ae_measurable f μ)
   (hfi : integrable f μ) :
   tendsto (λ i, ∫ x in φ i, f x ∂μ) l (𝓝 $ ∫ x, f x ∂μ) :=
 suffices h : tendsto (λ i, ∫ (x : α), (φ i).indicator f x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ)),
 by { convert h, ext n, rw integral_indicator (hφ.measurable n) },
-tendsto_integral_filter_of_dominated_convergence (λ x, ∥f x∥) hcg
+tendsto_integral_filter_of_dominated_convergence (λ x, ∥f x∥)
   (eventually_of_forall $ λ i, hfm.indicator $ hφ.measurable i) hfm
   (eventually_of_forall $ λ i, ae_of_all _ $ λ x, norm_indicator_le_norm_self _ _)
   hfi.norm hφ.ae_tendsto_indicator
 
 /-- Slight reformulation of
     `measure_theory.ae_cover.integral_tendsto_of_countably_generated`. -/
-lemma ae_cover.integral_eq_of_tendsto [l.ne_bot] {φ : ι → set α} (hφ : ae_cover μ l φ)
-  (hcg : l.is_countably_generated) {f : α → E}
+lemma ae_cover.integral_eq_of_tendsto [l.ne_bot] [l.is_countably_generated]
+  {φ : ι → set α} (hφ : ae_cover μ l φ) {f : α → E}
   (I : E) (hfm : ae_measurable f μ) (hfi : integrable f μ)
   (h : tendsto (λ n, ∫ x in φ n, f x ∂μ) l (𝓝 I)) :
   ∫ x, f x ∂μ = I :=
-tendsto_nhds_unique (hφ.integral_tendsto_of_countably_generated hcg hfm hfi) h
+tendsto_nhds_unique (hφ.integral_tendsto_of_countably_generated hfm hfi) h
 
-lemma ae_cover.integral_eq_of_tendsto_of_nonneg_ae [l.ne_bot] {φ : ι → set α}
-  (hφ : ae_cover μ l φ) (hcg : l.is_countably_generated) {f : α → ℝ} (I : ℝ)
+lemma ae_cover.integral_eq_of_tendsto_of_nonneg_ae [l.ne_bot] [l.is_countably_generated]
+  {φ : ι → set α} (hφ : ae_cover μ l φ) {f : α → ℝ} (I : ℝ)
   (hnng : 0 ≤ᵐ[μ] f) (hfm : ae_measurable f μ) (hfi : ∀ n, integrable_on f (φ n) μ)
   (htendsto : tendsto (λ n, ∫ x in φ n, f x ∂μ) l (𝓝 I)) :
   ∫ x, f x ∂μ = I :=
 have hfi' : integrable f μ,
-  from hφ.integrable_of_integral_tendsto_of_nonneg_ae hcg I hfm hfi hnng htendsto,
-hφ.integral_eq_of_tendsto hcg I hfm hfi' htendsto
+  from hφ.integrable_of_integral_tendsto_of_nonneg_ae I hfm hfi hnng htendsto,
+hφ.integral_eq_of_tendsto I hfm hfi' htendsto
 
 end integral
 
@@ -359,11 +359,11 @@ section integrable_of_interval_integral
 variables {α ι E : Type*}
           [topological_space α] [linear_order α] [order_closed_topology α]
           [measurable_space α] [opens_measurable_space α] {μ : measure α}
-          {l : filter ι} [filter.ne_bot l] (hcg : l.is_countably_generated)
+          {l : filter ι} [filter.ne_bot l] [is_countably_generated l]
           [measurable_space E] [normed_group E] [borel_space E]
           {a b : ι → α} {f : α → E} (hfm : ae_measurable f μ)
 
-include hcg hfm
+include hfm
 
 lemma integrable_of_interval_integral_norm_tendsto [no_bot_order α] [nonempty α]
   (I : ℝ) (hfi : ∀ i, integrable_on f (Ioc (a i) (b i)) μ)
@@ -374,7 +374,7 @@ begin
   let φ := λ n, Ioc (a n) (b n),
   let c : α := classical.choice ‹_›,
   have hφ : ae_cover μ l φ := ae_cover_Ioc ha hb,
-  refine hφ.integrable_of_integral_norm_tendsto hcg _ hfm hfi (h.congr' _),
+  refine hφ.integrable_of_integral_norm_tendsto _ hfm hfi (h.congr' _),
   filter_upwards [ha.eventually (eventually_le_at_bot c), hb.eventually (eventually_ge_at_top c)],
   intros i hai hbi,
   exact interval_integral.integral_of_le (hai.trans hbi)
@@ -391,7 +391,7 @@ begin
   { intro i,
     rw [integrable_on, measure.restrict_restrict (hφ.measurable i)],
     exact hfi i },
-  refine hφ.integrable_of_integral_norm_tendsto hcg _ hfm.restrict hfi (h.congr' _),
+  refine hφ.integrable_of_integral_norm_tendsto _ hfm.restrict hfi (h.congr' _),
   filter_upwards [ha.eventually (eventually_le_at_bot b)],
   intros i hai,
   rw [interval_integral.integral_of_le hai, measure.restrict_restrict (hφ.measurable i)],
@@ -409,7 +409,7 @@ begin
   { intro i,
     rw [integrable_on, measure.restrict_restrict (hφ.measurable i), inter_comm],
     exact hfi i },
-  refine hφ.integrable_of_integral_norm_tendsto hcg _ hfm.restrict hfi (h.congr' _),
+  refine hφ.integrable_of_integral_norm_tendsto _ hfm.restrict hfi (h.congr' _),
   filter_upwards [hb.eventually (eventually_ge_at_top $ a)],
   intros i hbi,
   rw [interval_integral.integral_of_le hbi, measure.restrict_restrict (hφ.measurable i),
@@ -424,12 +424,12 @@ section integral_of_interval_integral
 variables {α ι E : Type*}
           [topological_space α] [linear_order α] [order_closed_topology α]
           [measurable_space α] [opens_measurable_space α] {μ : measure α}
-          {l : filter ι} (hcg : l.is_countably_generated)
+          {l : filter ι} [is_countably_generated l]
           [measurable_space E] [normed_group E] [normed_space ℝ E] [borel_space E]
           [complete_space E] [second_countable_topology E]
           {a b : ι → α} {f : α → E} (hfm : ae_measurable f μ)
 
-include hcg hfm
+include hfm
 
 lemma interval_integral_tendsto_integral [no_bot_order α] [nonempty α]
   (hfi : integrable f μ) (ha : tendsto a l at_bot) (hb : tendsto b l at_top) :
@@ -438,7 +438,7 @@ begin
   let φ := λ i, Ioc (a i) (b i),
   let c : α := classical.choice ‹_›,
   have hφ : ae_cover μ l φ := ae_cover_Ioc ha hb,
-  refine (hφ.integral_tendsto_of_countably_generated hcg hfm hfi).congr' _,
+  refine (hφ.integral_tendsto_of_countably_generated hfm hfi).congr' _,
   filter_upwards [ha.eventually (eventually_le_at_bot c), hb.eventually (eventually_ge_at_top c)],
   intros i hai hbi,
   exact (interval_integral.integral_of_le (hai.trans hbi)).symm
@@ -450,7 +450,7 @@ lemma interval_integral_tendsto_integral_Iic [no_bot_order α] (b : α)
 begin
   let φ := λ i, Ioi (a i),
   have hφ : ae_cover (μ.restrict $ Iic b) l φ := ae_cover_Ioi ha,
-  refine (hφ.integral_tendsto_of_countably_generated hcg hfm.restrict hfi).congr' _,
+  refine (hφ.integral_tendsto_of_countably_generated hfm.restrict hfi).congr' _,
   filter_upwards [ha.eventually (eventually_le_at_bot $ b)],
   intros i hai,
   rw [interval_integral.integral_of_le hai, measure.restrict_restrict (hφ.measurable i)],
@@ -463,7 +463,7 @@ lemma interval_integral_tendsto_integral_Ioi (a : α)
 begin
   let φ := λ i, Iic (b i),
   have hφ : ae_cover (μ.restrict $ Ioi a) l φ := ae_cover_Iic hb,
-  refine (hφ.integral_tendsto_of_countably_generated hcg hfm.restrict hfi).congr' _,
+  refine (hφ.integral_tendsto_of_countably_generated hfm.restrict hfi).congr' _,
   filter_upwards [hb.eventually (eventually_ge_at_top $ a)],
   intros i hbi,
   rw [interval_integral.integral_of_le hbi, measure.restrict_restrict (hφ.measurable i),

src/measure_theory/integral/interval_integral.lean

@@ -890,15 +890,14 @@ lemma continuous_within_at_of_dominated_interval
   (h_cont : ∀ᵐ t ∂(μ.restrict $ Ι a b), continuous_within_at (λ x, F x t) s x₀) :
   continuous_within_at (λ x, ∫ t in a..b, F x t ∂μ) s x₀ :=
 begin
-  have gcs := is_countably_generated_nhds_within x₀ s,
   cases bound_integrable,
   cases le_or_lt a b with hab hab;
   [{ rw interval_oc_of_le hab at *,
      simp_rw interval_integral.integral_of_le hab },
    { rw interval_oc_of_lt hab at *,
      simp_rw interval_integral.integral_of_ge hab.le,
      refine tendsto.neg _ }];
-  apply tendsto_integral_filter_of_dominated_convergence bound gcs hF_meas hF_meas₀ h_bound,
+  apply tendsto_integral_filter_of_dominated_convergence bound hF_meas hF_meas₀ h_bound,
   exacts [bound_integrable_left, h_cont, bound_integrable_right, h_cont]
 end
 

src/measure_theory/integral/lebesgue.lean

@@ -1762,31 +1762,31 @@ end
 
 /-- Dominated convergence theorem for filters with a countable basis -/
 lemma tendsto_lintegral_filter_of_dominated_convergence {ι} {l : filter ι}
+  [l.is_countably_generated]
   {F : ι → α → ℝ≥0∞} {f : α → ℝ≥0∞} (bound : α → ℝ≥0∞)
-  (hl_cb : l.is_countably_generated)
   (hF_meas : ∀ᶠ n in l, measurable (F n))
   (h_bound : ∀ᶠ n in l, ∀ᵐ a ∂μ, F n a ≤ bound a)
   (h_fin : ∫⁻ a, bound a ∂μ ≠ ∞)
   (h_lim : ∀ᵐ a ∂μ, tendsto (λ n, F n a) l (𝓝 (f a))) :
   tendsto (λn, ∫⁻ a, F n a ∂μ) l (𝓝 $ ∫⁻ a, f a ∂μ) :=
 begin
-  rw hl_cb.tendsto_iff_seq_tendsto,
-  { intros x xl,
-    have hxl, { rw tendsto_at_top' at xl, exact xl },
-    have h := inter_mem hF_meas h_bound,
-    replace h := hxl _ h,
-    rcases h with ⟨k, h⟩,
-    rw ← tendsto_add_at_top_iff_nat k,
-    refine tendsto_lintegral_of_dominated_convergence _ _ _ _ _,
-    { exact bound },
-    { intro, refine (h _ _).1, exact nat.le_add_left _ _ },
-    { intro, refine (h _ _).2, exact nat.le_add_left _ _ },
+  rw tendsto_iff_seq_tendsto,
+  intros x xl,
+  have hxl, { rw tendsto_at_top' at xl, exact xl },
+  have h := inter_mem hF_meas h_bound,
+  replace h := hxl _ h,
+  rcases h with ⟨k, h⟩,
+  rw ← tendsto_add_at_top_iff_nat k,
+  refine tendsto_lintegral_of_dominated_convergence _ _ _ _ _,
+  { exact bound },
+  { intro, refine (h _ _).1, exact nat.le_add_left _ _ },
+  { intro, refine (h _ _).2, exact nat.le_add_left _ _ },
+  { assumption },
+  { refine h_lim.mono (λ a h_lim, _),
+    apply @tendsto.comp _ _ _ (λn, x (n + k)) (λn, F n a),
     { assumption },
-    { refine h_lim.mono (λ a h_lim, _),
-      apply @tendsto.comp _ _ _ (λn, x (n + k)) (λn, F n a),
-      { assumption },
-      rw tendsto_add_at_top_iff_nat,
-      assumption } },
+    rw tendsto_add_at_top_iff_nat,
+    assumption }
 end
 
 section