feat(topology/constructions): more convenient lemmas (#13423)

* Define `continuous.fst'` and friends and `continuous.comp₂` and friends for convenience (and to help with elaborator issues)
* Cleanup in `topology/constructions`
* Define `set.preimage_inl_image_inr` and `set.preimage_inr_image_inl` and prove the `range` versions in terms of these. This required reordering some lemmas (moving general lemmas about `range` above the lemmas of interactions with `range` and specific functions).
* From the sphere eversion project

src/data/set/basic.lean

@@ -1751,51 +1751,6 @@ eq_univ_iff_forall
 
 alias range_iff_surjective ↔ _ function.surjective.range_eq
 
-@[simp] theorem range_id : range (@id α) = univ := range_iff_surjective.2 surjective_id
-
-@[simp] theorem range_id' : range (λ (x : α), x) = univ := range_id
-
-@[simp] theorem _root_.prod.range_fst [nonempty β] : range (prod.fst : α × β → α) = univ :=
-prod.fst_surjective.range_eq
-
-@[simp] theorem _root_.prod.range_snd [nonempty α] : range (prod.snd : α × β → β) = univ :=
-prod.snd_surjective.range_eq
-
-@[simp] theorem range_eval {ι : Type*} {α : ι → Sort*} [Π i, nonempty (α i)] (i : ι) :
-  range (eval i : (Π i, α i) → α i) = univ :=
-(surjective_eval i).range_eq
-
-theorem is_compl_range_inl_range_inr : is_compl (range $ @sum.inl α β) (range sum.inr) :=
-⟨by { rintro y ⟨⟨x₁, rfl⟩, ⟨x₂, _⟩⟩, cc },
-  by { rintro (x|y) -; [left, right]; exact mem_range_self _ }⟩
-
-@[simp] theorem range_inl_union_range_inr : range (sum.inl : α → α ⊕ β) ∪ range sum.inr = univ :=
-is_compl_range_inl_range_inr.sup_eq_top
-
-@[simp] theorem range_inl_inter_range_inr : range (sum.inl : α → α ⊕ β) ∩ range sum.inr = ∅ :=
-is_compl_range_inl_range_inr.inf_eq_bot
-
-@[simp] theorem range_inr_union_range_inl : range (sum.inr : β → α ⊕ β) ∪ range sum.inl = univ :=
-is_compl_range_inl_range_inr.symm.sup_eq_top
-
-@[simp] theorem range_inr_inter_range_inl : range (sum.inr : β → α ⊕ β) ∩ range sum.inl = ∅ :=
-is_compl_range_inl_range_inr.symm.inf_eq_bot
-
-@[simp] theorem preimage_inl_range_inr : sum.inl ⁻¹' range (sum.inr : β → α ⊕ β) = ∅ :=
-by { ext, simp }
-
-@[simp] theorem preimage_inr_range_inl : sum.inr ⁻¹' range (sum.inl : α → α ⊕ β) = ∅ :=
-by { ext, simp }
-
-@[simp] lemma compl_range_inl : (range (sum.inl : α → α ⊕ β))ᶜ = range (sum.inr : β → α ⊕ β) :=
-is_compl_range_inl_range_inr.compl_eq
-
-@[simp] lemma compl_range_inr : (range (sum.inr : β → α ⊕ β))ᶜ = range (sum.inl : α → α ⊕ β) :=
-is_compl_range_inl_range_inr.symm.compl_eq
-
-@[simp] theorem range_quot_mk (r : α → α → Prop) : range (quot.mk r) = univ :=
-(surjective_quot_mk r).range_eq
-
 @[simp] theorem image_univ {f : α → β} : f '' univ = range f :=
 by { ext, simp [image, range] }
 
@@ -1851,12 +1806,6 @@ lemma image_preimage_eq_of_subset {f : α → β} {s : set β} (hs : s ⊆ range
   f '' (f ⁻¹' s) = s :=
 by rw [image_preimage_eq_inter_range, inter_eq_self_of_subset_left hs]
 
-instance set.can_lift [can_lift α β] : can_lift (set α) (set β) :=
-{ coe := λ s, can_lift.coe '' s,
-  cond := λ s, ∀ x ∈ s, can_lift.cond β x,
-  prf := λ s hs, ⟨can_lift.coe ⁻¹' s, image_preimage_eq_of_subset $
-    λ x hx, can_lift.prf _ (hs x hx)⟩ }
-
 lemma image_preimage_eq_iff {f : α → β} {s : set β} : f '' (f ⁻¹' s) = s ↔ s ⊆ range f :=
 ⟨by { intro h, rw [← h], apply image_subset_range }, image_preimage_eq_of_subset⟩
 
@@ -1887,10 +1836,67 @@ theorem preimage_image_preimage {f : α → β} {s : set β} :
   f ⁻¹' (f '' (f ⁻¹' s)) = f ⁻¹' s :=
 by rw [image_preimage_eq_inter_range, preimage_inter_range]
 
+@[simp] theorem range_id : range (@id α) = univ := range_iff_surjective.2 surjective_id
+
+@[simp] theorem range_id' : range (λ (x : α), x) = univ := range_id
+
+@[simp] theorem _root_.prod.range_fst [nonempty β] : range (prod.fst : α × β → α) = univ :=
+prod.fst_surjective.range_eq
+
+@[simp] theorem _root_.prod.range_snd [nonempty α] : range (prod.snd : α × β → β) = univ :=
+prod.snd_surjective.range_eq
+
+@[simp] theorem range_eval {ι : Type*} {α : ι → Sort*} [Π i, nonempty (α i)] (i : ι) :
+  range (eval i : (Π i, α i) → α i) = univ :=
+(surjective_eval i).range_eq
+
+theorem is_compl_range_inl_range_inr : is_compl (range $ @sum.inl α β) (range sum.inr) :=
+⟨by { rintro y ⟨⟨x₁, rfl⟩, ⟨x₂, _⟩⟩, cc },
+  by { rintro (x|y) -; [left, right]; exact mem_range_self _ }⟩
+
+@[simp] theorem range_inl_union_range_inr : range (sum.inl : α → α ⊕ β) ∪ range sum.inr = univ :=
+is_compl_range_inl_range_inr.sup_eq_top
+
+@[simp] theorem range_inl_inter_range_inr : range (sum.inl : α → α ⊕ β) ∩ range sum.inr = ∅ :=
+is_compl_range_inl_range_inr.inf_eq_bot
+
+@[simp] theorem range_inr_union_range_inl : range (sum.inr : β → α ⊕ β) ∪ range sum.inl = univ :=
+is_compl_range_inl_range_inr.symm.sup_eq_top
+
+@[simp] theorem range_inr_inter_range_inl : range (sum.inr : β → α ⊕ β) ∩ range sum.inl = ∅ :=
+is_compl_range_inl_range_inr.symm.inf_eq_bot
+
+@[simp] theorem preimage_inl_image_inr (s : set β) : sum.inl ⁻¹' (@sum.inr α β '' s) = ∅ :=
+by { ext, simp }
+
+@[simp] theorem preimage_inr_image_inl (s : set α) : sum.inr ⁻¹' (@sum.inl α β '' s) = ∅ :=
+by { ext, simp }
+
+@[simp] theorem preimage_inl_range_inr : sum.inl ⁻¹' range (sum.inr : β → α ⊕ β) = ∅ :=
+by rw [← image_univ, preimage_inl_image_inr]
+
+@[simp] theorem preimage_inr_range_inl : sum.inr ⁻¹' range (sum.inl : α → α ⊕ β) = ∅ :=
+by rw [← image_univ, preimage_inr_image_inl]
+
+@[simp] lemma compl_range_inl : (range (sum.inl : α → α ⊕ β))ᶜ = range (sum.inr : β → α ⊕ β) :=
+is_compl_range_inl_range_inr.compl_eq
+
+@[simp] lemma compl_range_inr : (range (sum.inr : β → α ⊕ β))ᶜ = range (sum.inl : α → α ⊕ β) :=
+is_compl_range_inl_range_inr.symm.compl_eq
+
+@[simp] theorem range_quot_mk (r : α → α → Prop) : range (quot.mk r) = univ :=
+(surjective_quot_mk r).range_eq
+
+instance set.can_lift [can_lift α β] : can_lift (set α) (set β) :=
+{ coe := λ s, can_lift.coe '' s,
+  cond := λ s, ∀ x ∈ s, can_lift.cond β x,
+  prf := λ s hs, ⟨can_lift.coe ⁻¹' s, image_preimage_eq_of_subset $
+    λ x hx, can_lift.prf _ (hs x hx)⟩ }
+
 @[simp] theorem quot_mk_range_eq [setoid α] : range (λx : α, ⟦x⟧) = univ :=
 range_iff_surjective.2 quot.exists_rep
 
-lemma range_const_subset {c : α} : range (λx:ι, c) ⊆ {c} :=
+lemma range_const_subset {c : α} : range (λ x : ι, c) ⊆ {c} :=
 range_subset_iff.2 $ λ x, rfl
 
 @[simp] lemma range_const : ∀ [nonempty ι] {c : α}, range (λx:ι, c) = {c}

src/topology/constructions.lean

@@ -36,8 +36,8 @@ noncomputable theory
 open topological_space set filter
 open_locale classical topological_space filter
 
-universes u v w x
-variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x}
+universes u v
+variables {α : Type u} {β : Type v} {γ δ ε ζ : Type*}
 
 section constructions
 
@@ -172,43 +172,94 @@ end constructions
 
 section prod
 variables [topological_space α] [topological_space β] [topological_space γ] [topological_space δ]
+  [topological_space ε] [topological_space ζ]
 
 @[continuity] lemma continuous_fst : continuous (@prod.fst α β) :=
 continuous_inf_dom_left continuous_induced_dom
 
-lemma continuous_at_fst {p : α × β} : continuous_at prod.fst p :=
-continuous_fst.continuous_at
-
+/-- Postcomposing `f` with `prod.fst` is continuous -/
 lemma continuous.fst {f : α → β × γ} (hf : continuous f) : continuous (λ a : α, (f a).1) :=
 continuous_fst.comp hf
 
+/-- Precomposing `f` with `prod.fst` is continuous -/
+lemma continuous.fst' {f : α → γ} (hf : continuous f) : continuous (λ x : α × β, f x.fst) :=
+hf.comp continuous_fst
+
+lemma continuous_at_fst {p : α × β} : continuous_at prod.fst p :=
+continuous_fst.continuous_at
+
+/-- Postcomposing `f` with `prod.fst` is continuous at `x` -/
 lemma continuous_at.fst {f : α → β × γ} {x : α} (hf : continuous_at f x) :
   continuous_at (λ a : α, (f a).1) x :=
 continuous_at_fst.comp hf
 
+/-- Precomposing `f` with `prod.fst` is continuous at `(x, y)` -/
+lemma continuous_at.fst' {f : α → γ} {x : α} {y : β} (hf : continuous_at f x) :
+  continuous_at (λ x : α × β, f x.fst) (x, y) :=
+continuous_at.comp hf continuous_at_fst
+
+/-- Precomposing `f` with `prod.fst` is continuous at `x : α × β` -/
+lemma continuous_at.fst'' {f : α → γ} {x : α × β} (hf : continuous_at f x.fst) :
+  continuous_at (λ x : α × β, f x.fst) x :=
+hf.comp continuous_at_fst
+
 @[continuity] lemma continuous_snd : continuous (@prod.snd α β) :=
 continuous_inf_dom_right continuous_induced_dom
 
-lemma continuous_at_snd {p : α × β} : continuous_at prod.snd p :=
-continuous_snd.continuous_at
-
+/-- Postcomposing `f` with `prod.snd` is continuous -/
 lemma continuous.snd {f : α → β × γ} (hf : continuous f) : continuous (λ a : α, (f a).2) :=
 continuous_snd.comp hf
 
+/-- Precomposing `f` with `prod.snd` is continuous -/
+lemma continuous.snd' {f : β → γ} (hf : continuous f) : continuous (λ x : α × β, f x.snd) :=
+hf.comp continuous_snd
+
+lemma continuous_at_snd {p : α × β} : continuous_at prod.snd p :=
+continuous_snd.continuous_at
+
+/-- Postcomposing `f` with `prod.snd` is continuous at `x` -/
 lemma continuous_at.snd {f : α → β × γ} {x : α} (hf : continuous_at f x) :
   continuous_at (λ a : α, (f a).2) x :=
 continuous_at_snd.comp hf
 
+/-- Precomposing `f` with `prod.snd` is continuous at `(x, y)` -/
+lemma continuous_at.snd' {f : β → γ} {x : α} {y : β} (hf : continuous_at f y) :
+  continuous_at (λ x : α × β, f x.snd) (x, y) :=
+continuous_at.comp hf continuous_at_snd
+
+/-- Precomposing `f` with `prod.snd` is continuous at `x : α × β` -/
+lemma continuous_at.snd'' {f : β → γ} {x : α × β} (hf : continuous_at f x.snd) :
+  continuous_at (λ x : α × β, f x.snd) x :=
+hf.comp continuous_at_snd
+
 @[continuity] lemma continuous.prod_mk {f : γ → α} {g : γ → β}
   (hf : continuous f) (hg : continuous g) : continuous (λx, (f x, g x)) :=
 continuous_inf_rng (continuous_induced_rng hf) (continuous_induced_rng hg)
 
-@[continuity] lemma continuous.prod.mk (a : α) : continuous (prod.mk a : β → α × β) :=
+@[continuity] lemma continuous.prod.mk (a : α) : continuous (λ b : β, (a, b)) :=
 continuous_const.prod_mk continuous_id'
 
+@[continuity] lemma continuous.prod.mk_left (b : β) : continuous (λ a : α, (a, b)) :=
+continuous_id'.prod_mk continuous_const
+
+lemma continuous.comp₂ {g : α × β → γ} (hg : continuous g) {e : δ → α} (he : continuous e)
+  {f : δ → β} (hf : continuous f) : continuous (λ x, g (e x, f x)) :=
+hg.comp $ he.prod_mk hf
+
+lemma continuous.comp₃ {g : α × β × γ → ε} (hg : continuous g)
+  {e : δ → α} (he : continuous e) {f : δ → β} (hf : continuous f)
+  {k : δ → γ} (hk : continuous k) : continuous (λ x, g (e x, f x, k x)) :=
+hg.comp₂ he $ hf.prod_mk hk
+
+lemma continuous.comp₄ {g : α × β × γ × ζ → ε} (hg : continuous g)
+  {e : δ → α} (he : continuous e) {f : δ → β} (hf : continuous f)
+  {k : δ → γ} (hk : continuous k) {l : δ → ζ} (hl : continuous l) :
+  continuous (λ x, g (e x, f x, k x, l x)) :=
+hg.comp₃ he hf $ hk.prod_mk hl
+
 lemma continuous.prod_map {f : γ → α} {g : δ → β} (hf : continuous f) (hg : continuous g) :
   continuous (λ x : γ × δ, (f x.1, g x.2)) :=
-(hf.comp continuous_fst).prod_mk (hg.comp continuous_snd)
+hf.fst'.prod_mk hg.snd'
 
 /-- A version of `continuous_inf_dom_left` for binary functions -/
 lemma continuous_inf_dom_left₂ {α β γ} {f : α → β → γ}
@@ -279,7 +330,7 @@ show continuous (g ∘ (λ b, (a, b))), from h.comp (by continuity)
 
 lemma is_open.prod {s : set α} {t : set β} (hs : is_open s) (ht : is_open t) :
   is_open (s ×ˢ t) :=
-is_open.inter (hs.preimage continuous_fst) (ht.preimage continuous_snd)
+(hs.preimage continuous_fst).inter (ht.preimage continuous_snd)
 
 lemma nhds_prod_eq {a : α} {b : β} : 𝓝 (a, b) = 𝓝 a ×ᶠ 𝓝 b :=
 by rw [filter.prod, prod.topological_space, nhds_inf, nhds_induced, nhds_induced]
@@ -361,47 +412,41 @@ hf.prod_mk_nhds hg
 lemma continuous_at.prod_map {f : α → γ} {g : β → δ} {p : α × β}
   (hf : continuous_at f p.fst) (hg : continuous_at g p.snd) :
   continuous_at (λ p : α × β, (f p.1, g p.2)) p :=
-(hf.comp continuous_at_fst).prod (hg.comp continuous_at_snd)
+hf.fst''.prod hg.snd''
 
 lemma continuous_at.prod_map' {f : α → γ} {g : β → δ} {x : α} {y : β}
   (hf : continuous_at f x) (hg : continuous_at g y) :
   continuous_at (λ p : α × β, (f p.1, g p.2)) (x, y) :=
-have hf : continuous_at f (x, y).fst, from hf,
-have hg : continuous_at g (x, y).snd, from hg,
-hf.prod_map hg
+hf.fst'.prod hg.snd'
 
 lemma prod_generate_from_generate_from_eq {α β : Type*} {s : set (set α)} {t : set (set β)}
   (hs : ⋃₀ s = univ) (ht : ⋃₀ t = univ) :
   @prod.topological_space α β (generate_from s) (generate_from t) =
-  generate_from {g | ∃u∈s, ∃v∈t, g = u ×ˢ v} :=
-let G := generate_from {g | ∃u∈s, ∃v∈t, g = u ×ˢ v} in
+  generate_from {g | ∃ u ∈ s, ∃ v ∈ t, g = u ×ˢ v} :=
+let G := generate_from {g | ∃ u ∈ s, ∃ v ∈ t, g = u ×ˢ v} in
 le_antisymm
-  (le_generate_from $ assume g ⟨u, hu, v, hv, g_eq⟩, g_eq.symm ▸
+  (le_generate_from $ λ g ⟨u, hu, v, hv, g_eq⟩, g_eq.symm ▸
     @is_open.prod _ _ (generate_from s) (generate_from t) _ _
       (generate_open.basic _ hu) (generate_open.basic _ hv))
   (le_inf
-    (coinduced_le_iff_le_induced.mp $ le_generate_from $ assume u hu,
-      have (⋃v∈t, u ×ˢ v) = prod.fst ⁻¹' u,
-        from calc (⋃v∈t, u ×ˢ v) = u ×ˢ (univ : set β) :
-            set.ext $ assume ⟨a, b⟩, by rw ← ht; simp [and.left_comm] {contextual:=tt}
-          ... = prod.fst ⁻¹' u : set.prod_univ,
+    (coinduced_le_iff_le_induced.mp $ le_generate_from $ λ u hu,
+      have (⋃ v ∈ t, u ×ˢ v) = prod.fst ⁻¹' u,
+      by simp_rw [← prod_Union, ← sUnion_eq_bUnion, ht, prod_univ],
       show G.is_open (prod.fst ⁻¹' u),
-        from this ▸ @is_open_Union _ _ G _ $ assume v, @is_open_Union _ _ G _ $ assume hv,
-          generate_open.basic _ ⟨_, hu, _, hv, rfl⟩)
-    (coinduced_le_iff_le_induced.mp $ le_generate_from $ assume v hv,
-      have (⋃u∈s, u ×ˢ v) = prod.snd ⁻¹' v,
-        from calc (⋃u∈s, u ×ˢ v) = (univ : set α) ×ˢ v:
-            set.ext $ assume ⟨a, b⟩, by rw [←hs]; by_cases b ∈ v; simp [h] {contextual:=tt}
-          ... = prod.snd ⁻¹' v : set.univ_prod,
+      by { rw [← this], exactI is_open_Union (λ v, is_open_Union $ λ hv,
+        generate_open.basic _ ⟨_, hu, _, hv, rfl⟩) })
+    (coinduced_le_iff_le_induced.mp $ le_generate_from $ λ v hv,
+      have (⋃ u ∈ s, u ×ˢ v) = prod.snd ⁻¹' v,
+      by simp_rw [← Union_prod_const, ← sUnion_eq_bUnion, hs, univ_prod],
       show G.is_open (prod.snd ⁻¹' v),
-        from this ▸ @is_open_Union _ _ G _ $ assume u, @is_open_Union _ _ G _ $ assume hu,
-          generate_open.basic _ ⟨_, hu, _, hv, rfl⟩))
+      by { rw [← this], exactI is_open_Union (λ u, is_open_Union $ λ hu,
+          generate_open.basic _ ⟨_, hu, _, hv, rfl⟩) }))
 
 lemma prod_eq_generate_from :
   prod.topological_space =
   generate_from {g | ∃(s:set α) (t:set β), is_open s ∧ is_open t ∧ g = s ×ˢ t} :=
 le_antisymm
-  (le_generate_from $ assume g ⟨s, t, hs, ht, g_eq⟩, g_eq.symm ▸ hs.prod ht)
+  (le_generate_from $ λ g ⟨s, t, hs, ht, g_eq⟩, g_eq.symm ▸ hs.prod ht)
   (le_inf
     (ball_image_of_ball $ λt ht, generate_open.basic _ ⟨t, univ, by simpa [set.prod_eq] using ht⟩)
     (ball_image_of_ball $ λt ht, generate_open.basic _ ⟨univ, t, by simpa [set.prod_eq] using ht⟩))
@@ -420,16 +465,7 @@ end
 lemma prod_induced_induced {α γ : Type*} (f : α → β) (g : γ → δ) :
   @prod.topological_space α γ (induced f ‹_›) (induced g ‹_›) =
   induced (λ p, (f p.1, g p.2)) prod.topological_space :=
-begin
-  set fxg := (λ p : α × γ, (f p.1, g p.2)),
-  have key1 : f ∘ (prod.fst : α × γ → α) = (prod.fst : β × δ → β) ∘ fxg, from rfl,
-  have key2 : g ∘ (prod.snd : α × γ → γ) = (prod.snd : β × δ → δ) ∘ fxg, from rfl,
-  unfold prod.topological_space,
-  conv_lhs
-  { rw [induced_compose, induced_compose, key1, key2],
-    congr, rw ← induced_compose, skip, rw ← induced_compose, },
-  rw induced_inf
-end
+by simp_rw [prod.topological_space, induced_inf, induced_compose]
 
 lemma continuous_uncurry_of_discrete_topology_left [discrete_topology α]
   {f : α → β → γ} (h : ∀ a, continuous (f a)) : continuous (function.uncurry f) :=
@@ -568,11 +604,11 @@ begin
 end
 
 protected lemma open_embedding.prod {f : α → β} {g : γ → δ}
-  (hf : open_embedding f) (hg : open_embedding g) : open_embedding (λx:α×γ, (f x.1, g x.2)) :=
+  (hf : open_embedding f) (hg : open_embedding g) : open_embedding (λ x : α × γ, (f x.1, g x.2)) :=
 open_embedding_of_embedding_open (hf.1.prod_mk hg.1)
   (hf.is_open_map.prod hg.is_open_map)
 
-lemma embedding_graph {f : α → β} (hf : continuous f) : embedding (λx, (x, f x)) :=
+lemma embedding_graph {f : α → β} (hf : continuous f) : embedding (λ x, (x, f x)) :=
 embedding_of_embedding_compose (continuous_id.prod_mk hf) continuous_fst embedding_id
 
 end prod
@@ -622,10 +658,7 @@ lemma embedding_inl : embedding (@inl α β) :=
         (is_open (inl ⁻¹' (@inl α β '' u)) ∧
          is_open (inr ⁻¹' (@inl α β '' u))) ∧
         inl ⁻¹' (inl '' u) = u,
-      have : inl ⁻¹' (@inl α β '' u) = u :=
-        preimage_image_eq u (λ _ _, inl.inj_iff.mp), rw this,
-      have : inr ⁻¹' (@inl α β '' u) = ∅ :=
-        eq_empty_iff_forall_not_mem.mpr (assume a ⟨b, _, h⟩, inl_ne_inr h), rw this,
+      rw [preimage_image_eq u sum.inl_injective, preimage_inr_image_inl],
       exact ⟨⟨hu, is_open_empty⟩, rfl⟩ }
   end,
   inj := λ _ _, inl.inj_iff.mp }
@@ -640,10 +673,7 @@ lemma embedding_inr : embedding (@inr α β) :=
         (is_open (inl ⁻¹' (@inr α β '' u)) ∧
          is_open (inr ⁻¹' (@inr α β '' u))) ∧
         inr ⁻¹' (inr '' u) = u,
-      have : inl ⁻¹' (@inr α β '' u) = ∅ :=
-        eq_empty_iff_forall_not_mem.mpr (assume b ⟨a, _, h⟩, inr_ne_inl h), rw this,
-      have : inr ⁻¹' (@inr α β '' u) = u :=
-        preimage_image_eq u (λ _ _, inr.inj_iff.mp), rw this,
+      rw [preimage_inl_image_inr, preimage_image_eq u sum.inr_injective],
       exact ⟨⟨is_open_empty, hu⟩, rfl⟩ }
   end,
   inj := λ _ _, inr.inj_iff.mp }