feat(order/filter/lift): replace some implications with iffs (#16452)

src/order/filter/lift.lean

@@ -72,6 +72,11 @@ lemma mem_lift_sets (hg : monotone g) {s : set β} :
 (f.basis_sets.mem_lift_iff (λ s, (g s).basis_sets) hg).trans $
   by simp only [id, exists_mem_subset_iff]
 
+lemma sInter_lift_sets (hg : monotone g) :
+  ⋂₀ {s | s ∈ f.lift g} = ⋂ s ∈ f, ⋂₀ {t | t ∈ g s} :=
+by simp only [sInter_eq_bInter, mem_set_of_eq, filter.mem_sets, mem_lift_sets hg,
+  Inter_exists, @Inter_comm _ (set β)]
+
 lemma mem_lift {s : set β} {t : set α} (ht : t ∈ f) (hs : s ∈ g t) :
   s ∈ f.lift g :=
 le_principal_iff.mp $ show f.lift g ≤ 𝓟 s,
@@ -81,9 +86,9 @@ lemma lift_le {f : filter α} {g : set α → filter β} {h : filter β} {s : se
   (hs : s ∈ f) (hg : g s ≤ h) : f.lift g ≤ h :=
 infi₂_le_of_le s hs hg
 
-lemma le_lift {f : filter α} {g : set α → filter β} {h : filter β}
-  (hh : ∀s∈f, h ≤ g s) : h ≤ f.lift g :=
-le_infi₂ hh
+lemma le_lift {f : filter α} {g : set α → filter β} {h : filter β} :
+  h ≤ f.lift g ↔ ∀ s ∈ f, h ≤ g s :=
+le_infi₂_iff
 
 lemma lift_mono (hf : f₁ ≤ f₂) (hg : g₁ ≤ g₂) : f₁.lift g₁ ≤ f₂.lift g₂ :=
 infi_mono $ λ s, infi_mono' $ λ hs, ⟨hf hs, hg s⟩
@@ -141,43 +146,33 @@ le_antisymm
 
 lemma lift_lift_same_le_lift {g : set α → set α → filter β} :
   f.lift (λs, f.lift (g s)) ≤ f.lift (λs, g s s) :=
-le_infi $ assume s, le_infi $ assume hs, infi_le_of_le s $ infi_le_of_le hs $ infi_le_of_le s $
-  infi_le _ hs
+le_lift.2 $ λ s hs, lift_le hs $ lift_le hs le_rfl
 
 lemma lift_lift_same_eq_lift {g : set α → set α → filter β}
   (hg₁ : ∀s, monotone (λt, g s t)) (hg₂ : ∀t, monotone (λs, g s t)) :
   f.lift (λs, f.lift (g s)) = f.lift (λs, g s s) :=
-le_antisymm
-  lift_lift_same_le_lift
-  (le_infi $ assume s, le_infi $ assume hs, le_infi $ assume t, le_infi $ assume ht,
-    infi_le_of_le (s ∩ t) $
-    infi_le_of_le (inter_mem hs ht) $
+lift_lift_same_le_lift.antisymm $
+  le_lift.2 $ λ s hs, le_lift.2 $ λ t ht, lift_le (inter_mem hs ht) $
     calc g (s ∩ t) (s ∩ t) ≤ g s (s ∩ t) : hg₂ (s ∩ t) (inter_subset_left _ _)
-      ... ≤ g s t                        : hg₁ s (inter_subset_right _ _))
+                       ... ≤ g s t       : hg₁ s (inter_subset_right _ _)
 
 lemma lift_principal {s : set α} (hg : monotone g) :
   (𝓟 s).lift g = g s :=
-le_antisymm
-  (infi_le_of_le s $ infi_le _ $ subset.refl _)
-  (le_infi $ assume t, le_infi $ assume hi, hg hi)
+(lift_le (mem_principal_self _) le_rfl).antisymm (le_lift.2 $ λ t ht, hg ht)
 
 theorem monotone_lift [preorder γ] {f : γ → filter α} {g : γ → set α → filter β}
   (hf : monotone f) (hg : monotone g) : monotone (λc, (f c).lift (g c)) :=
 assume a b h, lift_mono (hf h) (hg h)
 
 lemma lift_ne_bot_iff (hm : monotone g) : (ne_bot $ f.lift g) ↔ (∀s∈f, ne_bot (g s)) :=
-begin
-  rw [filter.lift, infi_subtype', infi_ne_bot_iff_of_directed', subtype.forall'],
-  { rintros ⟨s, hs⟩ ⟨t, ht⟩,
-    exact ⟨⟨s ∩ t, inter_mem hs ht⟩, hm (inter_subset_left s t), hm (inter_subset_right s t)⟩ }
-end
+by simp only [ne_bot_iff, ne.def, ← empty_mem_iff_bot, mem_lift_sets hm, not_exists]
 
 @[simp] lemma lift_const {f : filter α} {g : filter β} : f.lift (λx, g) = g :=
-le_antisymm (lift_le univ_mem $ le_refl g) (le_lift $ assume s hs, le_refl g)
+infi_subtype'.trans infi_const
 
 @[simp] lemma lift_inf {f : filter α} {g h : set α → filter β} :
   f.lift (λx, g x ⊓ h x) = f.lift g ⊓ f.lift h :=
-by simp only [filter.lift, infi_inf_eq, eq_self_iff_true]
+by simp only [filter.lift, infi_inf_eq]
 
 @[simp] lemma lift_principal2 {f : filter α} : f.lift 𝓟 = f :=
 le_antisymm
@@ -250,13 +245,17 @@ begin
   simp only [exists_const]
 end
 
-lemma mem_lift'_sets (hh : monotone h) {s : set β} : s ∈ (f.lift' h) ↔ (∃t∈f, h t ⊆ s) :=
+lemma mem_lift'_sets (hh : monotone h) {s : set β} : s ∈ f.lift' h ↔ ∃ t ∈ f, h t ⊆ s :=
 mem_lift_sets $ monotone_principal.comp hh
 
 lemma eventually_lift'_iff (hh : monotone h) {p : β → Prop} :
   (∀ᶠ y in f.lift' h, p y) ↔ (∃ t ∈ f, ∀ y ∈ h t, p y) :=
 mem_lift'_sets hh
 
+lemma sInter_lift'_sets (hh : monotone h) :
+  ⋂₀ {s | s ∈ f.lift' h} = ⋂ s ∈ f, h s :=
+(sInter_lift_sets (monotone_principal.comp hh)).trans $ Inter₂_congr $ λ s hs, cInf_Ici
+
 lemma lift'_le {f : filter α} {g : set α → set β} {h : filter β} {s : set α}
   (hs : s ∈ f) (hg : 𝓟 (g s) ≤ h) : f.lift' g ≤ h :=
 lift_le hs hg
@@ -298,9 +297,11 @@ by rw [← principal_singleton, lift'_principal hh]
 lemma lift'_bot (hh : monotone h) : (⊥ : filter α).lift' h = 𝓟 (h ∅) :=
 by rw [← principal_empty, lift'_principal hh]
 
-lemma principal_le_lift' {t : set β} (hh : ∀s∈f, t ⊆ h s) :
-  𝓟 t ≤ f.lift' h :=
-le_infi $ assume s, le_infi $ assume hs, principal_mono.mpr (hh s hs)
+lemma le_lift' {f : filter α} {h : set α → set β} {g : filter β} :
+  g ≤ f.lift' h ↔ ∀ s ∈ f, h s ∈ g :=
+le_lift.trans $ forall₂_congr $ λ s hs, le_principal_iff
+
+lemma principal_le_lift' {t : set β} : 𝓟 t ≤ f.lift' h ↔ ∀ s ∈ f, t ⊆ h s := le_lift'
 
 theorem monotone_lift' [preorder γ] {f : γ → filter α} {g : γ → set α → set β}
   (hf : monotone f) (hg : monotone g) : monotone (λc, (f c).lift' (g c)) :=
@@ -345,11 +346,6 @@ calc (ne_bot (f.lift' h)) ↔ (∀s∈f, ne_bot (𝓟 (h s))) :
 @[simp] lemma lift'_id {f : filter α} : f.lift' id = f :=
 lift_principal2
 
-lemma le_lift' {f : filter α} {h : set α → set β} {g : filter β}
-  (h_le : ∀s∈f, h s ∈ g) : g ≤ f.lift' h :=
-le_infi $ assume s, le_infi $ assume hs,
-  by simpa only [h_le, le_principal_iff, function.comp_app] using h_le s hs
-
 lemma lift'_infi [nonempty ι] {f : ι → filter α} {g : set α → set β}
   (hg : ∀ s t, g (s ∩ t) = g s ∩ g t) : (infi f).lift' g = (⨅ i, (f i).lift' g) :=
 lift_infi $ λ s t, by rw [inf_principal, (∘), ← hg]

src/topology/basic.lean

@@ -451,7 +451,7 @@ theorem mem_closure_iff {s : set α} {a : α} :
   let ⟨x, hc, hs⟩ := (H _ h₁.is_open_compl nc) in hc (h₂ hs)⟩
 
 lemma filter.le_lift'_closure (l : filter α) : l ≤ l.lift' closure :=
-le_infi₂ $ λ s hs, le_principal_iff.2 $ mem_of_superset hs subset_closure
+le_lift'.2 $ λ s hs, mem_of_superset hs subset_closure
 
 lemma filter.has_basis.lift'_closure {l : filter α} {p : ι → Prop} {s : ι → set α}
   (h : l.has_basis p s) :

src/topology/uniform_space/basic.lean

@@ -384,7 +384,7 @@ lemma filter.tendsto.uniformity_trans {l : filter β} {f₁ f₂ f₃ : β → 
   (h₁₂ : tendsto (λ x, (f₁ x, f₂ x)) l (𝓤 α)) (h₂₃ : tendsto (λ x, (f₂ x, f₃ x)) l (𝓤 α)) :
   tendsto (λ x, (f₁ x, f₃ x)) l (𝓤 α) :=
 begin
-  refine le_trans (le_lift' $ λ s hs, mem_map.2 _) comp_le_uniformity,
+  refine le_trans (le_lift'.2 $ λ s hs, mem_map.2 _) comp_le_uniformity,
   filter_upwards [h₁₂ hs, h₂₃ hs] with x hx₁₂ hx₂₃ using ⟨_, hx₁₂, hx₂₃⟩,
 end
 

src/topology/uniform_space/cauchy.lean

@@ -365,10 +365,8 @@ instance complete_space.prod [uniform_space β] [complete_space α] [complete_sp
     let ⟨x1, hx1⟩ := complete_space.complete $ hf.map uniform_continuous_fst in
     let ⟨x2, hx2⟩ := complete_space.complete $ hf.map uniform_continuous_snd in
     ⟨(x1, x2), by rw [nhds_prod_eq, filter.prod_def];
-      from filter.le_lift (λ s hs, filter.le_lift' $ λ t ht,
-        have H1 : prod.fst ⁻¹' s ∈ f.sets := hx1 hs,
-        have H2 : prod.snd ⁻¹' t ∈ f.sets := hx2 ht,
-        filter.inter_mem H1 H2)⟩ }
+      from filter.le_lift.2 (λ s hs, filter.le_lift'.2 $ λ t ht,
+        inter_mem (hx1 hs) (hx2 ht))⟩ }
 
 /--If `univ` is complete, the space is a complete space -/
 lemma complete_space_of_is_complete_univ (h : is_complete (univ : set α)) : complete_space α :=

src/topology/uniform_space/completion.lean

@@ -126,7 +126,7 @@ calc ((𝓤 α).lift' gen).lift' (λs, comp_rel s s) =
 instance : uniform_space (Cauchy α) :=
 uniform_space.of_core
 { uniformity  := (𝓤 α).lift' gen,
-  refl        := principal_le_lift' $ assume s hs ⟨a, b⟩ (a_eq_b : a = b),
+  refl        := principal_le_lift'.2 $ λ s hs ⟨a, b⟩ (a_eq_b : a = b),
     a_eq_b ▸ a.property.right hs,
   symm        := symm_gen,
   comp        := comp_gen }
@@ -208,7 +208,7 @@ complete_space_extension
   assume f hf,
   let f' : Cauchy α := ⟨f, hf⟩ in
   have map pure_cauchy f ≤ (𝓤 $ Cauchy α).lift' (preimage (prod.mk f')),
-    from le_lift' $ assume s hs,
+    from le_lift'.2 $ assume s hs,
     let ⟨t, ht₁, (ht₂ : gen t ⊆ s)⟩ := (mem_lift'_sets monotone_gen).mp hs in
     let ⟨t', ht', (h : t' ×ˢ t' ⊆ t)⟩ := mem_prod_same_iff.mp (hf.right ht₁) in
     have t' ⊆ { y : α | (f', pure_cauchy y) ∈ gen t },

src/topology/uniform_space/uniform_embedding.lean

@@ -413,16 +413,9 @@ end
 instance complete_space.sum [complete_space α] [complete_space β] :
   complete_space (α ⊕ β) :=
 begin
-  rw complete_space_iff_is_complete_univ,
-  have A : is_complete (range (sum.inl : α → α ⊕ β)) :=
-    uniform_embedding_inl.to_uniform_inducing.is_complete_range,
-  have B : is_complete (range (sum.inr : β → α ⊕ β)) :=
-    uniform_embedding_inr.to_uniform_inducing.is_complete_range,
-  convert A.union B,
-  apply (eq_univ_of_forall (λ x, _)).symm,
-  cases x,
-  { left, exact mem_range_self _ },
-  { right, exact mem_range_self _ }
+  rw [complete_space_iff_is_complete_univ, ← range_inl_union_range_inr],
+  exact uniform_embedding_inl.to_uniform_inducing.is_complete_range.union
+    uniform_embedding_inr.to_uniform_inducing.is_complete_range
 end
 
 end