refactor(*): place map_map in the functor namespace (#3309)

Renames `_root_.map_map` to `functor.map_map` and `filter.comap_comap_comp` to `filter.comap_comap` (which is consistent with `filter.map_map`).

src/control/basic.lean

@@ -17,7 +17,7 @@ variables {f : Type u → Type v} [functor f] [is_lawful_functor f]
 run_cmd mk_simp_attr `functor_norm
 run_cmd tactic.add_doc_string `simp_attr.functor_norm "Simp set for functor_norm"
 
-@[functor_norm] protected theorem map_map (m : α → β) (g : β → γ) (x : f α) :
+@[functor_norm] theorem functor.map_map (m : α → β) (g : β → γ) (x : f α) :
   g <$> (m <$> x) = (g ∘ m) <$> x :=
 (comp_map _ _ _).symm
 
@@ -196,6 +196,8 @@ class is_comm_applicative (m : Type* → Type*) [applicative m] extends is_lawfu
 (commutative_prod : ∀{α β} (a : m α) (b : m β), prod.mk <$> a <*> b = (λb a, (a, b)) <$> b <*> a)
 end prio
 
+open functor
+
 lemma is_comm_applicative.commutative_map
   {m : Type* → Type*} [applicative m] [is_comm_applicative m]
   {α β γ} (a : m α) (b : m β) {f : α → β → γ} :

src/order/filter/basic.lean

@@ -1386,7 +1386,7 @@ begin
     simp [univ_mem_sets] },
 end
 
-lemma comap_comap_comp {m : γ → β} {n : β → α} : comap m (comap n f) = comap (n ∘ m) f :=
+lemma comap_comap {m : γ → β} {n : β → α} : comap m (comap n f) = comap (n ∘ m) f :=
 le_antisymm
   (assume c ⟨b, hb, (h : preimage (n ∘ m) b ⊆ c)⟩, ⟨preimage n b, preimage_mem_comap hb, h⟩)
   (assume c ⟨b, ⟨a, ha, (h₁ : preimage n a ⊆ b)⟩, (h₂ : preimage m b ⊆ c)⟩,
@@ -1535,7 +1535,7 @@ lemma subtype_coe_map_comap_prod (s : set α) (f : filter (α × α)) :
 let φ (x : s × s) : s.prod s := ⟨⟨x.1.1, x.2.1⟩, ⟨x.1.2, x.2.2⟩⟩ in
 begin
   rw show (coe : s × s → α × α) = coe ∘ φ, by ext x; cases x; refl,
-  rw [← filter.map_map, ← filter.comap_comap_comp],
+  rw [← filter.map_map, ← filter.comap_comap],
   rw map_comap_of_surjective,
   exact subtype_coe_map_comap _ _,
   exact λ ⟨⟨a, b⟩, ⟨ha, hb⟩⟩, ⟨⟨⟨a, ha⟩, ⟨b, hb⟩⟩, rfl⟩
@@ -1975,7 +1975,7 @@ lemma comap_eq_of_inverse {f : filter α} {g : filter β} {φ : α → β} (ψ :
   (eq : ψ ∘ φ = id) (hφ : tendsto φ f g) (hψ : tendsto ψ g f) : comap φ g = f :=
 begin
   refine le_antisymm (le_trans (comap_mono $ map_le_iff_le_comap.1 hψ) _) (map_le_iff_le_comap.1 hφ),
-  rw [comap_comap_comp, eq, comap_id],
+  rw [comap_comap, eq, comap_id],
   exact le_refl _
 end
 
@@ -2095,7 +2095,7 @@ end
 
 lemma comap_prod (f : α → β × γ) (b : filter β) (c : filter γ) :
   comap f (b ×ᶠ c) = (comap (prod.fst ∘ f) b) ⊓ (comap (prod.snd ∘ f) c) :=
-by erw [comap_inf, filter.comap_comap_comp, filter.comap_comap_comp]
+by erw [comap_inf, filter.comap_comap, filter.comap_comap]
 
 lemma eventually_prod_iff {p : α × β → Prop} {f : filter α} {g : filter β} :
   (∀ᶠ x in f ×ᶠ g, p x) ↔ ∃ (pa : α → Prop) (ha : ∀ᶠ x in f, pa x)
@@ -2148,10 +2148,10 @@ inf_le_inf (comap_mono hf) (comap_mono hg)
 lemma prod_comap_comap_eq {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x}
   {f₁ : filter α₁} {f₂ : filter α₂} {m₁ : β₁ → α₁} {m₂ : β₂ → α₂} :
   (comap m₁ f₁) ×ᶠ (comap m₂ f₂) = comap (λp:β₁×β₂, (m₁ p.1, m₂ p.2)) (f₁ ×ᶠ f₂) :=
-by simp only [filter.prod, comap_comap_comp, eq_self_iff_true, comap_inf]
+by simp only [filter.prod, comap_comap, eq_self_iff_true, comap_inf]
 
 lemma prod_comm' : f ×ᶠ g = comap (prod.swap) (g ×ᶠ f) :=
-by simp only [filter.prod, comap_comap_comp, (∘), inf_comm, prod.fst_swap,
+by simp only [filter.prod, comap_comap, (∘), inf_comm, prod.fst_swap,
   eq_self_iff_true, prod.snd_swap, comap_inf]
 
 lemma prod_comm : f ×ᶠ g = map (λp:β×α, (p.2, p.1)) (g ×ᶠ f) :=

src/topology/algebra/uniform_group.lean

@@ -96,7 +96,7 @@ section
 variables (α)
 lemma uniformity_eq_comap_nhds_zero : 𝓤 α = comap (λx:α×α, x.2 - x.1) (𝓝 (0:α)) :=
 begin
-  rw [nhds_eq_comap_uniformity, filter.comap_comap_comp],
+  rw [nhds_eq_comap_uniformity, filter.comap_comap],
   refine le_antisymm (filter.map_le_iff_le_comap.1 _) _,
   { assume s hs,
     rcases mem_uniformity_of_uniform_continuous_invariant uniform_continuous_sub hs with ⟨t, ht, hts⟩,

src/topology/dense_embedding.lean

@@ -277,7 +277,7 @@ protected lemma subtype (p : α → Prop) : dense_embedding (subtype_emb p e) :=
     end,
   inj     := assume ⟨x, hx⟩ ⟨y, hy⟩ h, subtype.eq $ de.inj $ @@congr_arg subtype.val h,
   induced := (induced_iff_nhds_eq _).2 (assume ⟨x, hx⟩,
-    by simp [subtype_emb, nhds_subtype_eq_comap, de.to_inducing.nhds_eq_comap, comap_comap_comp, (∘)]) }
+    by simp [subtype_emb, nhds_subtype_eq_comap, de.to_inducing.nhds_eq_comap, comap_comap, (∘)]) }
 
 end dense_embedding
 

src/topology/metric_space/basic.lean

@@ -1078,7 +1078,7 @@ theorem filter.tendsto.dist {f g : β → α} {x : filter β} {a b : α}
 
 lemma nhds_comap_dist (a : α) : (𝓝 (0 : ℝ)).comap (λa', dist a' a) = 𝓝 a :=
 by simp only [@nhds_eq_comap_uniformity α, metric.uniformity_eq_comap_nhds_zero,
-  comap_comap_comp, (∘), dist_comm]
+  comap_comap, (∘), dist_comm]
 
 lemma tendsto_iff_dist_tendsto_zero {f : β → α} {x : filter β} {a : α} :
   (tendsto f x (𝓝 a)) ↔ (tendsto (λb, dist (f b) a) x (𝓝 0)) :=

src/topology/uniform_space/basic.lean

@@ -1026,9 +1026,9 @@ by { rw h, refl }
 lemma uniform_space_comap_id {α : Type*} : uniform_space.comap (id : α → α) = id :=
 by ext u ; dsimp [uniform_space.comap] ; rw [prod.id_prod, filter.comap_id]
 
-lemma uniform_space.comap_comap_comp {α β γ} [uγ : uniform_space γ] {f : α → β} {g : β → γ} :
+lemma uniform_space.comap_comap {α β γ} [uγ : uniform_space γ] {f : α → β} {g : β → γ} :
   uniform_space.comap (g ∘ f) uγ = uniform_space.comap f (uniform_space.comap g uγ) :=
-by ext ; dsimp [uniform_space.comap] ; rw filter.comap_comap_comp
+by ext ; dsimp [uniform_space.comap] ; rw filter.comap_comap
 
 lemma uniform_continuous_iff {α β} [uα : uniform_space α] [uβ : uniform_space β] {f : α → β} :
   uniform_continuous f ↔ uα ≤ uβ.comap f :=
@@ -1165,7 +1165,7 @@ have map (λp:(α×α)×(β×β), ((p.1.1, p.2.1), (p.1.2, p.2.2))) =
   comap (λp:(α×β)×(α×β), ((p.1.1, p.2.1), (p.1.2, p.2.2))),
   from funext $ assume f, map_eq_comap_of_inverse
     (funext $ assume ⟨⟨_, _⟩, ⟨_, _⟩⟩, rfl) (funext $ assume ⟨⟨_, _⟩, ⟨_, _⟩⟩, rfl),
-by rw [this, uniformity_prod, filter.prod, comap_inf, comap_comap_comp, comap_comap_comp]
+by rw [this, uniformity_prod, filter.prod, comap_inf, comap_comap, comap_comap]
 
 lemma mem_map_sets_iff' {α : Type*} {β : Type*} {f : filter α} {m : α → β} {t : set β} :
   t ∈ (map m f).sets ↔ (∃s∈f, m '' s ⊆ t) :=

src/topology/uniform_space/cauchy.lean

@@ -208,7 +208,7 @@ lemma cauchy_prod [uniform_space β] {f : filter α} {g : filter β} :
 | ⟨f_proper, hf⟩ ⟨g_proper, hg⟩ := ⟨filter.prod_ne_bot.2 ⟨f_proper, g_proper⟩,
   let p_α := λp:(α×β)×(α×β), (p.1.1, p.2.1), p_β := λp:(α×β)×(α×β), (p.1.2, p.2.2) in
   suffices (f.prod f).comap p_α ⊓ (g.prod g).comap p_β ≤ (𝓤 α).comap p_α ⊓ (𝓤 β).comap p_β,
-    by simpa [uniformity_prod, filter.prod, filter.comap_inf, filter.comap_comap_comp, (∘),
+    by simpa [uniformity_prod, filter.prod, filter.comap_inf, filter.comap_comap, (∘),
         inf_assoc, inf_comm, inf_left_comm],
   inf_le_inf (filter.comap_mono hf) (filter.comap_mono hg)⟩
 

src/topology/uniform_space/completion.lean

@@ -345,7 +345,7 @@ begin
   have : (λx:α×α, ((x.1 : completion α), (x.2 : completion α))) =
     (λx:(Cauchy α)×(Cauchy α), (⟦x.1⟧, ⟦x.2⟧)) ∘ (λx:α×α, (pure_cauchy x.1, pure_cauchy x.2)),
   { ext ⟨a, b⟩; simp; refl },
-  rw [this, ← filter.comap_comap_comp],
+  rw [this, ← filter.comap_comap],
   change filter.comap _ (filter.comap _ (𝓤 $ quotient $ separation_setoid $ Cauchy α)) = 𝓤 α,
   rw [comap_quotient_eq_uniformity, uniform_embedding_pure_cauchy.comap_uniformity]
 end

src/topology/uniform_space/uniform_embedding.lean

@@ -28,7 +28,7 @@ lemma uniform_inducing.comp {g : β → γ} (hg : uniform_inducing g)
   {f : α → β} (hf : uniform_inducing f) : uniform_inducing (g ∘ f) :=
 ⟨ by rw [show (λ (x : α × α), ((g ∘ f) x.1, (g ∘ f) x.2)) =
          (λ y : β × β, (g y.1, g y.2)) ∘ (λ x : α × α, (f x.1, f x.2)), by ext ; simp,
-        ← filter.comap_comap_comp, hg.1, hf.1]⟩
+        ← filter.comap_comap, hg.1, hf.1]⟩
 
 structure uniform_embedding (f : α → β) extends uniform_inducing f : Prop :=
 (inj : function.injective f)
@@ -45,7 +45,7 @@ uniform_embedding_subtype_val
 lemma uniform_embedding_set_inclusion {s t : set α} (hst : s ⊆ t) :
   uniform_embedding (inclusion hst) :=
 { comap_uniformity :=
-    by { erw [uniformity_subtype, uniformity_subtype, comap_comap_comp], congr },
+    by { erw [uniformity_subtype, uniformity_subtype, comap_comap], congr },
   inj := inclusion_injective hst }
 
 lemma uniform_embedding.comp {g : β → γ} (hg : uniform_embedding g)
@@ -96,7 +96,7 @@ lemma uniform_inducing.prod {α' : Type*} {β' : Type*} [uniform_space α'] [uni
   {e₁ : α → α'} {e₂ : β → β'} (h₁ : uniform_inducing e₁) (h₂ : uniform_inducing e₂) :
   uniform_inducing (λp:α×β, (e₁ p.1, e₂ p.2)) :=
 ⟨by simp [(∘), uniformity_prod, h₁.comap_uniformity.symm, h₂.comap_uniformity.symm,
-           comap_inf, comap_comap_comp]⟩
+           comap_inf, comap_comap]⟩
 
 lemma uniform_inducing.dense_inducing {f : α → β} (h : uniform_inducing f) (hd : dense_range f) :
   dense_inducing f :=
@@ -150,7 +150,7 @@ have ∀b', (b, b') ∈ t → b' ∈ closure (e '' {a' | (a, a') ∈ s}),
 
 lemma uniform_embedding_subtype_emb (p : α → Prop) {e : α → β} (ue : uniform_embedding e)
   (de : dense_embedding e) : uniform_embedding (dense_embedding.subtype_emb p e) :=
-{ comap_uniformity := by simp [comap_comap_comp, (∘), dense_embedding.subtype_emb,
+{ comap_uniformity := by simp [comap_comap, (∘), dense_embedding.subtype_emb,
            uniformity_subtype, ue.comap_uniformity.symm],
   inj := (de.subtype p).inj }
 
@@ -346,9 +346,9 @@ let ⟨c, (hc : tendsto (f ∘ subtype.val) (comap (dense_embedding.subtype_emb
   uniformly_extend_exists ue'.to_uniform_inducing de'.dense hf _ in
 begin
   rw [nhds_subtype_eq_comap] at hc,
-  simp [comap_comap_comp] at hc,
+  simp [comap_comap] at hc,
   change (tendsto (f ∘ @subtype.val α p) (comap (e ∘ @subtype.val α p) (𝓝 b)) (𝓝 c)) at hc,
-  rw [←comap_comap_comp, tendsto_comap'_iff] at hc,
+  rw [←comap_comap, tendsto_comap'_iff] at hc,
   exact ⟨c, hc⟩,
   exact ⟨_, hb, assume x,
     begin