chore(topology/metric_space/baire): review (#3146)

* Simplify some proofs in `topology/metric_space/baire`;
* Allow dependency on `hi : i ∈ S` in some `bUnion`/`bInter` lemmas.

Author: urkud

src/algebraic_geometry/prime_spectrum.lean

@@ -287,7 +287,7 @@ topological_space.of_closed (set.range prime_spectrum.zero_locus)
     intros Zs h,
     rw set.sInter_eq_Inter,
     let f : Zs → set R := λ i, classical.some (h i.2),
-    have hf : ∀ i : Zs, i.1 = zero_locus (f i) := λ i, (classical.some_spec (h i.2)).symm,
+    have hf : ∀ i : Zs, ↑i = zero_locus (f i) := λ i, (classical.some_spec (h i.2)).symm,
     simp only [hf],
     exact ⟨_, zero_locus_Union _⟩
   end

src/data/set/basic.lean

@@ -331,6 +331,9 @@ by simp [ext_iff]
 
 theorem eq_univ_of_forall {s : set α} : (∀ x, x ∈ s) → s = univ := eq_univ_iff_forall.2
 
+lemma eq_univ_of_subset {s t : set α} (h : s ⊆ t) (hs : s = univ) : t = univ :=
+eq_univ_of_univ_subset $ hs ▸ h
+
 @[simp] lemma univ_eq_empty_iff : (univ : set α) = ∅ ↔ ¬ nonempty α :=
 eq_empty_iff_forall_not_mem.trans ⟨λ H ⟨x⟩, H x trivial, λ H x _, H ⟨x⟩⟩
 

src/data/set/countable.lean

@@ -119,8 +119,8 @@ lemma countable_Union {t : α → set β} [encodable α] (ht : ∀a, countable (
 by haveI := (λ a, (ht a).to_encodable);
    rw Union_eq_range_sigma; apply countable_range
 
-lemma countable.bUnion {s : set α} {t : α → set β} (hs : countable s) (ht : ∀a∈s, countable (t a)) :
-  countable (⋃a∈s, t a) :=
+lemma countable.bUnion {s : set α} {t : Π x ∈ s, set β} (hs : countable s) (ht : ∀a∈s, countable (t a ‹_›)) :
+  countable (⋃a∈s, t a ‹_›) :=
 begin
   rw bUnion_eq_Union,
   haveI := hs.to_encodable,

src/data/set/lattice.lean

@@ -283,11 +283,13 @@ theorem bUnion_mono {s : set α} {t t' : α → set β} (h : ∀ x ∈ s, t x 
   (⋃ x ∈ s, t x) ⊆ (⋃ x ∈ s, t' x) :=
 bUnion_subset_bUnion (λ x x_in, ⟨x, x_in, h x x_in⟩)
 
-theorem bUnion_eq_Union (s : set α) (t : α → set β) : (⋃ x ∈ s, t x) = (⋃ x : s, t x.1) :=
-set.ext $ by simp
+theorem bUnion_eq_Union (s : set α) (t : Π x ∈ s, set β) :
+  (⋃ x ∈ s, t x ‹_›) = (⋃ x : s, t x x.2) :=
+supr_subtype'
 
-theorem bInter_eq_Inter (s : set α) (t : α → set β) : (⋂ x ∈ s, t x) = (⋂ x : s, t x.1) :=
-set.ext $ by simp
+theorem bInter_eq_Inter (s : set α) (t : Π x ∈ s, set β) :
+  (⋂ x ∈ s, t x ‹_›) = (⋂ x : s, t x x.2) :=
+infi_subtype'
 
 theorem bInter_empty (u : α → set β) : (⋂ x ∈ (∅ : set α), u x) = univ :=
 show (⨅x ∈ (∅ : set α), u x) = ⊤, -- simplifier should be able to rewrite x ∈ ∅ to false.
@@ -441,9 +443,9 @@ Inf_pair
 
 @[simp] theorem sInter_image (f : α → set β) (s : set α) : ⋂₀ (f '' s) = ⋂ x ∈ s, f x := Inf_image
 
-@[simp] theorem sUnion_range (f : ι → set β) : ⋃₀ (range f) = ⋃ x, f x := Sup_range
+@[simp] theorem sUnion_range (f : ι → set β) : ⋃₀ (range f) = ⋃ x, f x := rfl
 
-@[simp] theorem sInter_range (f : ι → set β) : ⋂₀ (range f) = ⋂ x, f x := Inf_range
+@[simp] theorem sInter_range (f : ι → set β) : ⋂₀ (range f) = ⋂ x, f x := rfl
 
 lemma sUnion_eq_univ_iff {c : set (set α)} :
   ⋃₀ c = @set.univ α ↔ ∀ a, ∃ b ∈ c, a ∈ b :=
@@ -519,16 +521,16 @@ theorem bUnion_subset_Union (s : set α) (t : α → set β) :
 Union_subset_Union $ λ i, Union_subset $ λ h, by refl
 
 lemma sUnion_eq_bUnion {s : set (set α)} : (⋃₀ s) = (⋃ (i : set α) (h : i ∈ s), i) :=
-set.ext $ by simp
+by rw [← sUnion_image, image_id']
 
 lemma sInter_eq_bInter {s : set (set α)} : (⋂₀ s) = (⋂ (i : set α) (h : i ∈ s), i) :=
-set.ext $ by simp
+by rw [← sInter_image, image_id']
 
-lemma sUnion_eq_Union {s : set (set α)} : (⋃₀ s) = (⋃ (i : s), i.1) :=
-set.ext $ λ x, by simp
+lemma sUnion_eq_Union {s : set (set α)} : (⋃₀ s) = (⋃ (i : s), i) :=
+by rw [← sUnion_range, range_coe_subtype]
 
-lemma sInter_eq_Inter {s : set (set α)} : (⋂₀ s) = (⋂ (i : s), i.1) :=
-set.ext $ λ x, by simp
+lemma sInter_eq_Inter {s : set (set α)} : (⋂₀ s) = (⋂ (i : s), i) :=
+by rw [← sInter_range, range_coe_subtype]
 
 lemma union_eq_Union {s₁ s₂ : set α} : s₁ ∪ s₂ = ⋃ b : bool, cond b s₁ s₂ :=
 set.ext $ λ x, by simp [bool.exists_bool, or_comm]
@@ -560,28 +562,28 @@ lemma sUnion_inter_sUnion {s t : set (set α)} :
   (⋃₀s) ∩ (⋃₀t) = (⋃p ∈ set.prod s t, (p : (set α) × (set α )).1 ∩ p.2) :=
 Sup_inf_Sup
 
-lemma sInter_bUnion {S : set (set α)} {T : set α → set (set α)} (hT : ∀s∈S, s = ⋂₀ T s) :
-  ⋂₀ (⋃s∈S, T s) = ⋂₀ S :=
+/-- If `S` is a set of sets, and each `s ∈ S` can be represented as an intersection
+of sets `T s hs`, then `⋂₀ S` is the intersection of the union of all `T s hs`. -/
+lemma sInter_bUnion {S : set (set α)} {T : Π s ∈ S, set (set α)} (hT : ∀s∈S, s = ⋂₀ T s ‹s ∈ S›) :
+  ⋂₀ (⋃s∈S, T s ‹_›) = ⋂₀ S :=
 begin
   ext,
   simp only [and_imp, exists_prop, set.mem_sInter, set.mem_Union, exists_imp_distrib],
   split,
   { assume H s sS,
     rw [hT s sS, mem_sInter],
     assume t tTs,
-    apply H t s sS tTs },
+    exact H t s sS tTs },
   { assume H t s sS tTs,
-    have xs : x ∈ s := H s sS,
-    have : s ⊆ t,
-    { have Z := hT s sS,
-      rw sInter_eq_bInter at Z,
-      rw Z, apply bInter_subset_of_mem,
-      exact tTs },
-    exact this xs }
+    suffices : s ⊆ t, exact this (H s sS),
+    rw [hT s sS, sInter_eq_bInter],
+    exact bInter_subset_of_mem tTs }
 end
 
-lemma sUnion_bUnion {S : set (set α)} {T : set α → set (set α)} (hT : ∀s∈S, s = ⋃₀ T s) :
-  ⋃₀ (⋃s∈S, T s) = ⋃₀ S :=
+/-- If `S` is a set of sets, and each `s ∈ S` can be represented as an union
+of sets `T s hs`, then `⋃₀ S` is the union of the union of all `T s hs`. -/
+lemma sUnion_bUnion {S : set (set α)} {T : Π s ∈ S, set (set α)} (hT : ∀s∈S, s = ⋃₀ T s ‹_›) :
+  ⋃₀ (⋃s∈S, T s ‹_›) = ⋃₀ S :=
 begin
   ext,
   simp only [exists_prop, set.mem_Union, set.mem_set_of_eq],

src/measure_theory/measure_space.lean

@@ -390,7 +390,7 @@ by rw [measure_eq_measure' (h₁.union h₂),
 
 lemma measure_bUnion {s : set β} {f : β → set α} (hs : countable s)
   (hd : pairwise_on s (disjoint on f)) (h : ∀b∈s, is_measurable (f b)) :
-  μ (⋃b∈s, f b) = ∑'p:s, μ (f p.1) :=
+  μ (⋃b∈s, f b) = ∑'p:s, μ (f p) :=
 begin
   haveI := hs.to_encodable,
   rw [← measure_Union, bUnion_eq_Union],
@@ -401,7 +401,7 @@ end
 
 lemma measure_sUnion {S : set (set α)} (hs : countable S)
   (hd : pairwise_on S disjoint) (h : ∀s∈S, is_measurable s) :
-  μ (⋃₀ S) = ∑' s:S, μ s.1 :=
+  μ (⋃₀ S) = ∑' s:S, μ s :=
 by rw [sUnion_eq_bUnion, measure_bUnion hs hd h]
 
 lemma measure_bUnion_finset {s : finset ι} {f : ι → set α} (hd : pairwise_on ↑s (disjoint on f))

src/topology/basic.lean

@@ -386,7 +386,7 @@ by rw [frontier, interior_eq_of_open hs]
 lemma is_closed_frontier {s : set α} : is_closed (frontier s) :=
 by rw frontier_eq_closure_inter_closure; exact is_closed_inter is_closed_closure is_closed_closure
 
-/-- The frontier of a set has no interior point. -/
+/-- The frontier of a closed set has no interior point. -/
 lemma interior_frontier {s : set α} (h : is_closed s) : interior (frontier s) = ∅ :=
 begin
   have A : frontier s = s \ interior s, from h.frontier_eq,

src/topology/metric_space/baire.lean

@@ -25,7 +25,7 @@ open_locale classical
 
 open filter encodable set
 
-variables {α : Type*} {β : Type*} {γ : Type*}
+variables {α : Type*} {β : Type*} {γ : Type*} {ι : Type*}
 
 section is_Gδ
 variable [topological_space α]
@@ -38,43 +38,50 @@ def is_Gδ (s : set α) : Prop :=
 lemma is_open.is_Gδ {s : set α} (h : is_open s) : is_Gδ s :=
 ⟨{s}, by simp [h], countable_singleton _, (set.sInter_singleton _).symm⟩
 
-lemma is_Gδ_bInter_of_open {ι : Type*} {I : set ι} (hI : countable I) {f : ι → set α}
+lemma is_Gδ_univ : is_Gδ (univ : set α) := is_open_univ.is_Gδ
+
+lemma is_Gδ_bInter_of_open {I : set ι} (hI : countable I) {f : ι → set α}
   (hf : ∀i ∈ I, is_open (f i)) : is_Gδ (⋂i∈I, f i) :=
 ⟨f '' I, by rwa ball_image_iff, hI.image _, by rw sInter_image⟩
 
-lemma is_Gδ_Inter_of_open {ι : Type*} [encodable ι] {f : ι → set α}
+lemma is_Gδ_Inter_of_open [encodable ι] {f : ι → set α}
   (hf : ∀i, is_open (f i)) : is_Gδ (⋂i, f i) :=
 ⟨range f, by rwa forall_range_iff, countable_range _, by rw sInter_range⟩
 
 /-- A countable intersection of Gδ sets is a Gδ set. -/
 lemma is_Gδ_sInter {S : set (set α)} (h : ∀s∈S, is_Gδ s) (hS : countable S) : is_Gδ (⋂₀ S) :=
 begin
-  have : ∀s : set α, ∃T : set (set α), s ∈ S → ((∀t ∈ T, is_open t) ∧ countable T ∧ s = (⋂₀ T)),
-  { assume s,
-    by_cases hs : s ∈ S,
-    { simp [hs], exact h s hs },
-    { simp [hs] }},
-  choose T hT using this,
-  refine ⟨⋃s∈S, T s, λt ht, _, _, _⟩,
-  { simp only [exists_prop, set.mem_Union] at ht,
-    rcases ht with ⟨s, hs, tTs⟩,
+  choose T hT using h,
+  refine ⟨_, _, _, (sInter_bUnion (λ s hs, (hT s hs).2.2)).symm⟩,
+  { simp only [mem_Union],
+    rintros t ⟨s, hs, tTs⟩,
     exact (hT s hs).1 t tTs },
   { exact hS.bUnion (λs hs, (hT s hs).2.1) },
-  { exact (sInter_bUnion (λs hs, (hT s hs).2.2)).symm }
 end
 
+lemma is_Gδ_Inter [encodable ι]  {s : ι → set α} (hs : ∀ i, is_Gδ (s i)) : is_Gδ (⋂ i, s i) :=
+is_Gδ_sInter (forall_range_iff.2 hs) $ countable_range s
+
+lemma is_Gδ_bInter {s : set ι} (hs : countable s) {t : Π i ∈ s, set α} (ht : ∀ i ∈ s, is_Gδ (t i ‹_›)) :
+  is_Gδ (⋂ i ∈ s, t i ‹_›) :=
+begin
+  rw [bInter_eq_Inter],
+  haveI := hs.to_encodable,
+  exact is_Gδ_Inter (λ x, ht x x.2)
+end
+
+lemma is_Gδ.inter {s t : set α} (hs : is_Gδ s) (ht : is_Gδ t) : is_Gδ (s ∩ t) :=
+by { rw inter_eq_Inter, exact is_Gδ_Inter (bool.forall_bool.2 ⟨ht, hs⟩) }
+
 /-- The union of two Gδ sets is a Gδ set. -/
 lemma is_Gδ.union {s t : set α} (hs : is_Gδ s) (ht : is_Gδ t) : is_Gδ (s ∪ t) :=
 begin
-  rcases hs with ⟨S, Sopen, Scount, sS⟩,
-  rcases ht with ⟨T, Topen, Tcount, tT⟩,
-  rw [sS, tT, sInter_union_sInter],
+  rcases hs with ⟨S, Sopen, Scount, rfl⟩,
+  rcases ht with ⟨T, Topen, Tcount, rfl⟩,
+  rw [sInter_union_sInter],
   apply is_Gδ_bInter_of_open (countable_prod Scount Tcount),
   rintros ⟨a, b⟩ hab,
-  simp only [set.prod_mk_mem_set_prod_eq] at hab,
-  have aopen : is_open a := Sopen a hab.1,
-  have bopen : is_open b := Topen b hab.2,
-  simp [aopen, bopen, is_open_union]
+  exact is_open_union (Sopen a hab.1) (Topen b hab.2)
 end
 
 end is_Gδ
@@ -224,39 +231,17 @@ theorem dense_sInter_of_Gδ {S : set (set α)} (ho : ∀s∈S, is_Gδ s) (hS : c
 begin
   -- the result follows from the result for a countable intersection of dense open sets,
   -- by rewriting each set as a countable intersection of open sets, which are of course dense.
-  have : ∀s : set α, ∃T : set (set α), s ∈ S → ((∀t ∈ T, is_open t) ∧ countable T ∧ s = (⋂₀ T)),
-  { assume s,
-    by_cases hs : s ∈ S,
-    { simp [hs], exact ho s hs },
-    { simp [hs] }},
-  choose T hT using this,
-  have : ⋂₀ S = ⋂₀ (⋃s∈S, T s) := (sInter_bUnion (λs hs, (hT s hs).2.2)).symm,
+  choose T hT using ho,
+  have : ⋂₀ S = ⋂₀ (⋃s∈S, T s ‹_›) := (sInter_bUnion (λs hs, (hT s hs).2.2)).symm,
   rw this,
-  refine dense_sInter_of_open (λt ht, _) (hS.bUnion (λs hs, (hT s hs).2.1)) (λt ht, _),
+  refine dense_sInter_of_open _ (hS.bUnion (λs hs, (hT s hs).2.1)) _;
+    simp only [set.mem_Union, exists_prop]; rintro t ⟨s, hs, tTs⟩,
   show is_open t,
-  { simp only [exists_prop, set.mem_Union] at ht,
-    rcases ht with ⟨s, hs, tTs⟩,
-    exact (hT s hs).1 t tTs },
+  { exact (hT s hs).1 t tTs },
   show closure t = univ,
-  { simp only [exists_prop, set.mem_Union] at ht,
-    rcases ht with ⟨s, hs, tTs⟩,
-    apply subset.antisymm (subset_univ _),
-    rw ← (hd s hs),
-    apply closure_mono,
-    have := sInter_subset_of_mem tTs,
-    rwa ← (hT s hs).2.2 at this }
-end
-
-/-- Baire theorem: a countable intersection of dense Gδ sets is dense. Formulated here with
-an index set which is a countable set in any type. -/
-theorem dense_bInter_of_Gδ {S : set β} {f : β → set α} (ho : ∀s∈S, is_Gδ (f s))
-  (hS : countable S) (hd : ∀s∈S, closure (f s) = univ) : closure (⋂s∈S, f s) = univ :=
-begin
-  rw ← sInter_image,
-  apply dense_sInter_of_Gδ,
-  { rwa ball_image_iff },
-  { exact hS.image _ },
-  { rwa ball_image_iff }
+  { apply eq_univ_of_univ_subset,
+    rw [← hd s hs, (hT s hs).2.2],
+    exact closure_mono (sInter_subset_of_mem tTs) }
 end
 
 /-- Baire theorem: a countable intersection of dense Gδ sets is dense. Formulated here with
@@ -265,10 +250,26 @@ theorem dense_Inter_of_Gδ [encodable β] {f : β → set α} (ho : ∀s, is_Gδ
   (hd : ∀s, closure (f s) = univ) : closure (⋂s, f s) = univ :=
 begin
   rw ← sInter_range,
-  apply dense_sInter_of_Gδ,
-  { rwa forall_range_iff },
-  { exact countable_range _ },
-  { rwa forall_range_iff }
+  exact dense_sInter_of_Gδ (forall_range_iff.2 ‹_›) (countable_range _) (forall_range_iff.2 ‹_›)
+end
+
+/-- Baire theorem: a countable intersection of dense Gδ sets is dense. Formulated here with
+an index set which is a countable set in any type. -/
+theorem dense_bInter_of_Gδ {S : set β} {f : Π x ∈ S, set α} (ho : ∀s∈S, is_Gδ (f s ‹_›))
+  (hS : countable S) (hd : ∀s∈S, closure (f s ‹_›) = univ) : closure (⋂s∈S, f s ‹_›) = univ :=
+begin
+  rw bInter_eq_Inter,
+  haveI := hS.to_encodable,
+  exact dense_Inter_of_Gδ (λ s, ho s s.2) (λ s, hd s s.2)
+end
+
+/-- Baire theorem: the intersection of two dense Gδ sets is dense. -/
+theorem dense_inter_of_Gδ {s t : set α} (hs : is_Gδ s) (ht : is_Gδ t) (hsc : closure s = univ)
+  (htc : closure t = univ) :
+  closure (s ∩ t) = univ :=
+begin
+  rw [inter_eq_Inter],
+  apply dense_Inter_of_Gδ; simp [bool.forall_bool, *]
 end
 
 /-- Baire theorem: if countably many closed sets cover the whole space, then their interiors
@@ -282,7 +283,7 @@ begin
     show is_open (g s), from is_open_compl_iff.2 is_closed_frontier,
     show closure (g s) = univ,
     { apply subset.antisymm (subset_univ _),
-     simp [g, interior_frontier (hc s hs)] }},
+      simp [interior_frontier (hc s hs)] }},
   have : (⋂s∈S, g s) ⊆ (⋃s∈S, interior (f s)),
   { assume x hx,
     have : x ∈ ⋃s∈S, f s, { have := mem_univ x, rwa ← hU at this },