diff --git a/src/topology/algebra/group.lean b/src/topology/algebra/group.lean
index a8d6ed3272211..be8d48c3dd34f 100644
--- a/src/topology/algebra/group.lean
+++ b/src/topology/algebra/group.lean
@@ -14,49 +14,49 @@ import topology.homeomorph
 open classical set filter topological_space
 open_locale classical topological_space filter
 
-universes u v w
-variables {α : Type u} {β : Type v} {γ : Type w}
+universes u v w x
+variables {α : Type u} {β : Type v} {G : Type w} {H : Type x}
 
 section topological_group
 
 /-- A topological (additive) group is a group in which the addition and negation operations are
 continuous. -/
-class topological_add_group (α : Type u) [topological_space α] [add_group α]
-  extends has_continuous_add α : Prop :=
-(continuous_neg : continuous (λa:α, -a))
+class topological_add_group (G : Type u) [topological_space G] [add_group G]
+  extends has_continuous_add G : Prop :=
+(continuous_neg : continuous (λa:G, -a))
 
 /-- A topological group is a group in which the multiplication and inversion operations are
 continuous. -/
 @[to_additive]
-class topological_group (α : Type*) [topological_space α] [group α]
-  extends has_continuous_mul α : Prop :=
-(continuous_inv : continuous (λa:α, a⁻¹))
+class topological_group (G : Type*) [topological_space G] [group G]
+  extends has_continuous_mul G : Prop :=
+(continuous_inv : continuous (λa:G, a⁻¹))
 
-variables [topological_space α] [group α]
+variables [topological_space G] [group G]
 
 @[to_additive]
-lemma continuous_inv [topological_group α] : continuous (λx:α, x⁻¹) :=
+lemma continuous_inv [topological_group G] : continuous (λx:G, x⁻¹) :=
 topological_group.continuous_inv
 
 @[to_additive, continuity]
-lemma continuous.inv [topological_group α] [topological_space β] {f : β → α}
+lemma continuous.inv [topological_group G] [topological_space α] {f : α → G}
   (hf : continuous f) : continuous (λx, (f x)⁻¹) :=
 continuous_inv.comp hf
 
 attribute [continuity] continuous.neg
 
 @[to_additive]
-lemma continuous_on_inv [topological_group α] {s : set α} : continuous_on (λx:α, x⁻¹) s :=
+lemma continuous_on_inv [topological_group G] {s : set G} : continuous_on (λx:G, x⁻¹) s :=
 continuous_inv.continuous_on
 
 @[to_additive]
-lemma continuous_on.inv [topological_group α] [topological_space β] {f : β → α} {s : set β}
+lemma continuous_on.inv [topological_group G] [topological_space α] {f : α → G} {s : set α}
   (hf : continuous_on f s) : continuous_on (λx, (f x)⁻¹) s :=
 continuous_inv.comp_continuous_on hf
 
 @[to_additive]
-lemma tendsto_inv {α : Type*} [group α]
-  [topological_space α] [topological_group α] (a : α) :
+lemma tendsto_inv {G : Type*} [group G]
+  [topological_space G] [topological_group G] (a : G) :
   tendsto (λ x, x⁻¹) (nhds a) (nhds (a⁻¹)) :=
 continuous_inv.tendsto a
 
@@ -64,73 +64,73 @@ continuous_inv.tendsto a
 converges to the inverse of this value. For the version in normed fields assuming additionally
 that the limit is nonzero, use `tendsto.inv'`. -/
 @[to_additive]
-lemma filter.tendsto.inv [topological_group α] {f : β → α} {x : filter β} {a : α}
+lemma filter.tendsto.inv [topological_group G] {f : α → G} {x : filter α} {a : G}
   (hf : tendsto f x (𝓝 a)) : tendsto (λx, (f x)⁻¹) x (𝓝 a⁻¹) :=
 tendsto.comp (continuous_iff_continuous_at.mp topological_group.continuous_inv a) hf
 
 @[to_additive]
-lemma continuous_at.inv [topological_group α] [topological_space β] {f : β → α} {x : β}
+lemma continuous_at.inv [topological_group G] [topological_space α] {f : α → G} {x : α}
   (hf : continuous_at f x) : continuous_at (λx, (f x)⁻¹) x :=
 hf.inv
 
 @[to_additive]
-lemma continuous_within_at.inv [topological_group α] [topological_space β] {f : β → α}
-  {s : set β} {x : β} (hf : continuous_within_at f s x) :
+lemma continuous_within_at.inv [topological_group G] [topological_space α] {f : α → G}
+  {s : set α} {x : α} (hf : continuous_within_at f s x) :
   continuous_within_at (λx, (f x)⁻¹) s x :=
 hf.inv
 
 @[to_additive]
-instance [topological_group α] [topological_space β] [group β] [topological_group β] :
-  topological_group (α × β) :=
+instance [topological_group G] [topological_space H] [group H] [topological_group H] :
+  topological_group (G × H) :=
 { continuous_inv := continuous_fst.inv.prod_mk continuous_snd.inv }
 
 attribute [instance] prod.topological_add_group
 
 /-- Multiplication from the left in a topological group as a homeomorphism.-/
 @[to_additive "Addition from the left in a topological additive group as a homeomorphism."]
-protected def homeomorph.mul_left [topological_group α] (a : α) : α ≃ₜ α :=
+protected def homeomorph.mul_left [topological_group G] (a : G) : G ≃ₜ G :=
 { continuous_to_fun  := continuous_const.mul continuous_id,
   continuous_inv_fun := continuous_const.mul continuous_id,
   .. equiv.mul_left a }
 
 @[to_additive]
-lemma is_open_map_mul_left [topological_group α] (a : α) : is_open_map (λ x, a * x) :=
+lemma is_open_map_mul_left [topological_group G] (a : G) : is_open_map (λ x, a * x) :=
 (homeomorph.mul_left a).is_open_map
 
 @[to_additive]
-lemma is_closed_map_mul_left [topological_group α] (a : α) : is_closed_map (λ x, a * x) :=
+lemma is_closed_map_mul_left [topological_group G] (a : G) : is_closed_map (λ x, a * x) :=
 (homeomorph.mul_left a).is_closed_map
 
 /-- Multiplication from the right in a topological group as a homeomorphism.-/
 @[to_additive "Addition from the right in a topological additive group as a homeomorphism."]
 protected def homeomorph.mul_right
-  {α : Type*} [topological_space α] [group α] [topological_group α] (a : α) :
-  α ≃ₜ α :=
+  {G : Type*} [topological_space G] [group G] [topological_group G] (a : G) :
+  G ≃ₜ G :=
 { continuous_to_fun  := continuous_id.mul continuous_const,
   continuous_inv_fun := continuous_id.mul continuous_const,
   .. equiv.mul_right a }
 
 @[to_additive]
-lemma is_open_map_mul_right [topological_group α] (a : α) : is_open_map (λ x, x * a) :=
+lemma is_open_map_mul_right [topological_group G] (a : G) : is_open_map (λ x, x * a) :=
 (homeomorph.mul_right a).is_open_map
 
 @[to_additive]
-lemma is_closed_map_mul_right [topological_group α] (a : α) : is_closed_map (λ x, x * a) :=
+lemma is_closed_map_mul_right [topological_group G] (a : G) : is_closed_map (λ x, x * a) :=
 (homeomorph.mul_right a).is_closed_map
 
 /-- Inversion in a topological group as a homeomorphism.-/
 @[to_additive "Negation in a topological group as a homeomorphism."]
-protected def homeomorph.inv (α : Type*) [topological_space α] [group α] [topological_group α] :
-  α ≃ₜ α :=
+protected def homeomorph.inv (G : Type*) [topological_space G] [group G] [topological_group G] :
+  G ≃ₜ G :=
 { continuous_to_fun  := continuous_inv,
   continuous_inv_fun := continuous_inv,
-  .. equiv.inv α }
+  .. equiv.inv G }
 
 @[to_additive exists_nhds_half]
-lemma exists_nhds_split [topological_group α] {s : set α} (hs : s ∈ 𝓝 (1 : α)) :
-  ∃ V ∈ 𝓝 (1 : α), ∀ v w ∈ V, v * w ∈ s :=
+lemma exists_nhds_split [topological_group G] {s : set G} (hs : s ∈ 𝓝 (1 : G)) :
+  ∃ V ∈ 𝓝 (1 : G), ∀ v w ∈ V, v * w ∈ s :=
 begin
-  have : ((λa:α×α, a.1 * a.2) ⁻¹' s) ∈ 𝓝 ((1, 1) : α × α) :=
+  have : ((λa:G×G, a.1 * a.2) ⁻¹' s) ∈ 𝓝 ((1, 1) : G × G) :=
     tendsto_mul (by simpa using hs),
   rw nhds_prod_eq at this,
   rcases mem_prod_iff.1 this with ⟨V₁, H₁, V₂, H₂, H⟩,
@@ -138,20 +138,20 @@ begin
 end
 
 @[to_additive exists_nhds_half_neg]
-lemma exists_nhds_split_inv [topological_group α] {s : set α} (hs : s ∈ 𝓝 (1 : α)) :
-  ∃ V ∈ 𝓝 (1 : α), ∀ (v ∈ V) (w ∈ V), v * w⁻¹ ∈ s :=
+lemma exists_nhds_split_inv [topological_group G] {s : set G} (hs : s ∈ 𝓝 (1 : G)) :
+  ∃ V ∈ 𝓝 (1 : G), ∀ (v ∈ V) (w ∈ V), v * w⁻¹ ∈ s :=
 begin
-  have : tendsto (λa:α×α, a.1 * (a.2)⁻¹) (𝓝 (1:α) ×ᶠ 𝓝 (1:α)) (𝓝 1),
-  { simpa using (@tendsto_fst α α (𝓝 1) (𝓝 1)).mul tendsto_snd.inv },
-  have : ((λa:α×α, a.1 * (a.2)⁻¹) ⁻¹' s) ∈ 𝓝 (1:α) ×ᶠ 𝓝 (1:α) :=
+  have : tendsto (λa:G×G, a.1 * (a.2)⁻¹) (𝓝 (1:G) ×ᶠ 𝓝 (1:G)) (𝓝 1),
+  { simpa using (@tendsto_fst G G (𝓝 1) (𝓝 1)).mul tendsto_snd.inv },
+  have : ((λa:G×G, a.1 * (a.2)⁻¹) ⁻¹' s) ∈ 𝓝 (1:G) ×ᶠ 𝓝 (1:G) :=
     this (by simpa using hs),
   rcases mem_prod_self_iff.1 this with ⟨V, H, H'⟩,
   exact ⟨V, H, prod_subset_iff.1 H'⟩
 end
 
 @[to_additive exists_nhds_quarter]
-lemma exists_nhds_split4 [topological_group α] {u : set α} (hu : u ∈ 𝓝 (1 : α)) :
-  ∃ V ∈ 𝓝 (1 : α), ∀ {v w s t}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u :=
+lemma exists_nhds_split4 [topological_group G] {u : set G} (hu : u ∈ 𝓝 (1 : G)) :
+  ∃ V ∈ 𝓝 (1 : G), ∀ {v w s t}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u :=
 begin
   rcases exists_nhds_split hu with ⟨W, W_nhd, h⟩,
   rcases exists_nhds_split W_nhd with ⟨V, V_nhd, h'⟩,
@@ -161,26 +161,26 @@ begin
 end
 
 section
-variable (α)
+variable (G)
 @[to_additive]
-lemma nhds_one_symm [topological_group α] : comap (λr:α, r⁻¹) (𝓝 (1 : α)) = 𝓝 (1 : α) :=
+lemma nhds_one_symm [topological_group G] : comap (λr:G, r⁻¹) (𝓝 (1 : G)) = 𝓝 (1 : G) :=
 begin
-  have lim : tendsto (λr:α, r⁻¹) (𝓝 1) (𝓝 1),
-  { simpa using (@tendsto_id α (𝓝 1)).inv },
+  have lim : tendsto (λr:G, r⁻¹) (𝓝 1) (𝓝 1),
+  { simpa using (@tendsto_id G (𝓝 1)).inv },
   refine comap_eq_of_inverse _ _ lim lim,
   { funext x, simp },
 end
 end
 
 @[to_additive]
-lemma nhds_translation_mul_inv [topological_group α] (x : α) :
-  comap (λy:α, y * x⁻¹) (𝓝 1) = 𝓝 x :=
+lemma nhds_translation_mul_inv [topological_group G] (x : G) :
+  comap (λy:G, y * x⁻¹) (𝓝 1) = 𝓝 x :=
 begin
-  refine comap_eq_of_inverse (λy:α, y * x) _ _ _,
+  refine comap_eq_of_inverse (λy:G, y * x) _ _ _,
   { funext x; simp },
-  { suffices : tendsto (λy:α, y * x⁻¹) (𝓝 x) (𝓝 (x * x⁻¹)), { simpa },
+  { suffices : tendsto (λy:G, y * x⁻¹) (𝓝 x) (𝓝 (x * x⁻¹)), { simpa },
     exact tendsto_id.mul tendsto_const_nhds },
-  { suffices : tendsto (λy:α, y * x) (𝓝 1) (𝓝 (1 * x)), { simpa },
+  { suffices : tendsto (λy:G, y * x) (𝓝 1) (𝓝 (1 * x)), { simpa },
     exact tendsto_id.mul tendsto_const_nhds }
 end
 
@@ -193,17 +193,17 @@ eq_of_nhds_eq_nhds $ λ x, by
 end topological_group
 
 section quotient_topological_group
-variables [topological_space α] [group α] [topological_group α] (N : subgroup α) (n : N.normal)
+variables [topological_space G] [group G] [topological_group G] (N : subgroup G) (n : N.normal)
 
 @[to_additive]
-instance {α : Type u} [group α] [topological_space α] (N : subgroup α) :
+instance {G : Type u} [group G] [topological_space G] (N : subgroup G) :
   topological_space (quotient_group.quotient N) :=
 by dunfold quotient_group.quotient; apply_instance
 
 open quotient_group
 @[to_additive]
-lemma quotient_group_saturate {α : Type u} [group α] (N : subgroup α) (s : set α) :
-  (coe : α → quotient N) ⁻¹' ((coe : α → quotient N) '' s) = (⋃ x : N, (λ y, y*x.1) '' s) :=
+lemma quotient_group_saturate {G : Type u} [group G] (N : subgroup G) (s : set G) :
+  (coe : G → quotient N) ⁻¹' ((coe : G → quotient N) '' s) = (⋃ x : N, (λ y, y*x.1) '' s) :=
 begin
   ext x,
   simp only [mem_preimage, mem_image, mem_Union, quotient_group.eq],
@@ -214,10 +214,10 @@ begin
 end
 
 @[to_additive]
-lemma quotient_group.open_coe : is_open_map (coe : α →  quotient N) :=
+lemma quotient_group.open_coe : is_open_map (coe : G →  quotient N) :=
 begin
   intros s s_op,
-  change is_open ((coe : α →  quotient N) ⁻¹' (coe '' s)),
+  change is_open ((coe : G →  quotient N) ⁻¹' (coe '' s)),
   rw quotient_group_saturate N s,
   apply is_open_Union,
   rintro ⟨n, _⟩,
@@ -227,9 +227,9 @@ end
 @[to_additive]
 instance topological_group_quotient (n : N.normal) : topological_group (quotient N) :=
 { continuous_mul := begin
-    have cont : continuous ((coe : α → quotient N) ∘ (λ (p : α × α), p.fst * p.snd)) :=
+    have cont : continuous ((coe : G → quotient N) ∘ (λ (p : G × G), p.fst * p.snd)) :=
       continuous_quot_mk.comp continuous_mul,
-    have quot : quotient_map (λ p : α × α, ((p.1:quotient N), (p.2:quotient N))),
+    have quot : quotient_map (λ p : G × G, ((p.1:quotient N), (p.2:quotient N))),
     { apply is_open_map.to_quotient_map,
       { exact is_open_map.prod (quotient_group.open_coe N) (quotient_group.open_coe N) },
       { exact (continuous_quot_mk.comp continuous_fst).prod_mk
@@ -240,7 +240,7 @@ instance topological_group_quotient (n : N.normal) : topological_group (quotient
   end,
   continuous_inv := begin
     apply continuous_quotient_lift,
-    change continuous ((coe : α → quotient N) ∘ (λ (a : α), a⁻¹)),
+    change continuous ((coe : G → quotient N) ∘ (λ (a : G), a⁻¹)),
     exact continuous_quot_mk.comp continuous_inv
   end }
 
@@ -250,24 +250,24 @@ end quotient_topological_group
 
 
 section topological_add_group
-variables [topological_space α] [add_group α]
+variables [topological_space G] [add_group G]
 
-@[continuity] lemma continuous.sub [topological_add_group α] [topological_space β] {f : β → α} {g : β → α}
+@[continuity] lemma continuous.sub [topological_add_group G] [topological_space α] {f : α → G} {g : α → G}
   (hf : continuous f) (hg : continuous g) : continuous (λx, f x - g x) :=
 by simp [sub_eq_add_neg]; exact hf.add hg.neg
 
-lemma continuous_sub [topological_add_group α] : continuous (λp:α×α, p.1 - p.2) :=
+lemma continuous_sub [topological_add_group G] : continuous (λp:G×G, p.1 - p.2) :=
 continuous_fst.sub continuous_snd
 
-lemma continuous_on.sub [topological_add_group α] [topological_space β] {f : β → α} {g : β → α} {s : set β}
+lemma continuous_on.sub [topological_add_group G] [topological_space α] {f : α → G} {g : α → G} {s : set α}
   (hf : continuous_on f s) (hg : continuous_on g s) : continuous_on (λx, f x - g x) s :=
 continuous_sub.comp_continuous_on (hf.prod hg)
 
-lemma filter.tendsto.sub [topological_add_group α] {f : β → α} {g : β → α} {x : filter β} {a b : α}
+lemma filter.tendsto.sub [topological_add_group G] {f : α → G} {g : α → G} {x : filter α} {a b : G}
   (hf : tendsto f x (𝓝 a)) (hg : tendsto g x (𝓝 b)) : tendsto (λx, f x - g x) x (𝓝 (a - b)) :=
 by simp [sub_eq_add_neg]; exact hf.add hg.neg
 
-lemma nhds_translation [topological_add_group α] (x : α) : comap (λy:α, y - x) (𝓝 0) = 𝓝 x :=
+lemma nhds_translation [topological_add_group G] (x : G) : comap (λy:G, y - x) (𝓝 0) = 𝓝 x :=
 nhds_translation_add_neg x
 
 end topological_add_group
@@ -278,77 +278,77 @@ Only used to construct a topology and uniform space.
 This is currently only available for commutative groups, but it can be extended to
 non-commutative groups too.
 -/
-class add_group_with_zero_nhd (α : Type u) extends add_comm_group α :=
-(Z [] : filter α)
+class add_group_with_zero_nhd (G : Type u) extends add_comm_group G :=
+(Z [] : filter G)
 (zero_Z : pure 0 ≤ Z)
-(sub_Z : tendsto (λp:α×α, p.1 - p.2) (Z ×ᶠ Z) Z)
+(sub_Z : tendsto (λp:G×G, p.1 - p.2) (Z ×ᶠ Z) Z)
 
 namespace add_group_with_zero_nhd
-variables (α) [add_group_with_zero_nhd α]
+variables (G) [add_group_with_zero_nhd G]
 
 local notation `Z` := add_group_with_zero_nhd.Z
 
 @[priority 100] -- see Note [lower instance priority]
-instance : topological_space α :=
-topological_space.mk_of_nhds $ λa, map (λx, x + a) (Z α)
+instance : topological_space G :=
+topological_space.mk_of_nhds $ λa, map (λx, x + a) (Z G)
 
-variables {α}
+variables {G}
 
-lemma neg_Z : tendsto (λa:α, - a) (Z α) (Z α) :=
-have tendsto (λa, (0:α)) (Z α) (Z α),
+lemma neg_Z : tendsto (λa:G, - a) (Z G) (Z G) :=
+have tendsto (λa, (0:G)) (Z G) (Z G),
   by refine le_trans (assume h, _) zero_Z; simp [univ_mem_sets'] {contextual := tt},
-have tendsto (λa:α, 0 - a) (Z α) (Z α), from
+have tendsto (λa:G, 0 - a) (Z G) (Z G), from
   sub_Z.comp (tendsto.prod_mk this tendsto_id),
 by simpa
 
-lemma add_Z : tendsto (λp:α×α, p.1 + p.2) (Z α ×ᶠ Z α) (Z α) :=
-suffices tendsto (λp:α×α, p.1 - -p.2) (Z α ×ᶠ Z α) (Z α),
+lemma add_Z : tendsto (λp:G×G, p.1 + p.2) (Z G ×ᶠ Z G) (Z G) :=
+suffices tendsto (λp:G×G, p.1 - -p.2) (Z G ×ᶠ Z G) (Z G),
   by simpa [sub_eq_add_neg],
 sub_Z.comp (tendsto.prod_mk tendsto_fst (neg_Z.comp tendsto_snd))
 
-lemma exists_Z_half {s : set α} (hs : s ∈ Z α) : ∃ V ∈ Z α, ∀ (v ∈ V) (w ∈ V), v + w ∈ s :=
+lemma exists_Z_half {s : set G} (hs : s ∈ Z G) : ∃ V ∈ Z G, ∀ (v ∈ V) (w ∈ V), v + w ∈ s :=
 begin
-  have : ((λa:α×α, a.1 + a.2) ⁻¹' s) ∈ Z α ×ᶠ Z α := add_Z (by simpa using hs),
+  have : ((λa:G×G, a.1 + a.2) ⁻¹' s) ∈ Z G ×ᶠ Z G := add_Z (by simpa using hs),
   rcases mem_prod_self_iff.1 this with ⟨V, H, H'⟩,
   exact ⟨V, H, prod_subset_iff.1 H'⟩
 end
 
-lemma nhds_eq (a : α) : 𝓝 a = map (λx, x + a) (Z α) :=
+lemma nhds_eq (a : G) : 𝓝 a = map (λx, x + a) (Z G) :=
 topological_space.nhds_mk_of_nhds _ _
   (assume a, calc pure a = map (λx, x + a) (pure 0) : by simp
     ... ≤ _ : map_mono zero_Z)
   (assume b s hs,
     let ⟨t, ht, eqt⟩ := exists_Z_half hs in
-    have t0 : (0:α) ∈ t, by simpa using zero_Z ht,
+    have t0 : (0:G) ∈ t, by simpa using zero_Z ht,
     begin
-      refine ⟨(λx:α, x + b) '' t, image_mem_map ht, _, _⟩,
+      refine ⟨(λx:G, x + b) '' t, image_mem_map ht, _, _⟩,
       { refine set.image_subset_iff.2 (assume b hbt, _),
         simpa using eqt 0 t0 b hbt },
       { rintros _ ⟨c, hb, rfl⟩,
-        refine (Z α).sets_of_superset ht (assume x hxt, _),
+        refine (Z G).sets_of_superset ht (assume x hxt, _),
         simpa [add_assoc] using eqt _ hxt _ hb }
     end)
 
-lemma nhds_zero_eq_Z : 𝓝 0 = Z α := by simp [nhds_eq]; exact filter.map_id
+lemma nhds_zero_eq_Z : 𝓝 0 = Z G := by simp [nhds_eq]; exact filter.map_id
 
 @[priority 100] -- see Note [lower instance priority]
-instance : has_continuous_add α :=
+instance : has_continuous_add G :=
 ⟨ continuous_iff_continuous_at.2 $ assume ⟨a, b⟩,
   begin
     rw [continuous_at, nhds_prod_eq, nhds_eq, nhds_eq, nhds_eq, filter.prod_map_map_eq,
       tendsto_map'_iff],
-    suffices :  tendsto ((λx:α, (a + b) + x) ∘ (λp:α×α,p.1 + p.2)) (Z α ×ᶠ Z α)
-      (map (λx:α, (a + b) + x) (Z α)),
+    suffices :  tendsto ((λx:G, (a + b) + x) ∘ (λp:G×G,p.1 + p.2)) (Z G ×ᶠ Z G)
+      (map (λx:G, (a + b) + x) (Z G)),
     { simpa [(∘), add_comm, add_left_comm] },
     exact tendsto_map.comp add_Z
   end ⟩
 
 @[priority 100] -- see Note [lower instance priority]
-instance : topological_add_group α :=
+instance : topological_add_group G :=
 ⟨continuous_iff_continuous_at.2 $ assume a,
   begin
     rw [continuous_at, nhds_eq, nhds_eq, tendsto_map'_iff],
-    suffices : tendsto ((λx:α, x - a) ∘ (λx:α, -x)) (Z α) (map (λx:α, x - a) (Z α)),
+    suffices : tendsto ((λx:G, x - a) ∘ (λx:G, -x)) (Z G) (map (λx:G, x - a) (Z G)),
     { simpa [(∘), add_comm, sub_eq_add_neg] using this },
     exact tendsto_map.comp neg_Z
   end⟩
@@ -358,40 +358,40 @@ end add_group_with_zero_nhd
 section filter_mul
 
 section
-variables [topological_space α] [group α] [topological_group α]
+variables [topological_space G] [group G] [topological_group G]
 
 @[to_additive]
-lemma is_open_mul_left {s t : set α} : is_open t → is_open (s * t) := λ ht,
+lemma is_open_mul_left {s t : set G} : is_open t → is_open (s * t) := λ ht,
 begin
-  have : ∀a, is_open ((λ (x : α), a * x) '' t),
+  have : ∀a, is_open ((λ (x : G), a * x) '' t),
     assume a, apply is_open_map_mul_left, exact ht,
   rw ← Union_mul_left_image,
   exact is_open_Union (λa, is_open_Union $ λha, this _),
 end
 
 @[to_additive]
-lemma is_open_mul_right {s t : set α} : is_open s → is_open (s * t) := λ hs,
+lemma is_open_mul_right {s t : set G} : is_open s → is_open (s * t) := λ hs,
 begin
-  have : ∀a, is_open ((λ (x : α), x * a) '' s),
+  have : ∀a, is_open ((λ (x : G), x * a) '' s),
     assume a, apply is_open_map_mul_right, exact hs,
   rw ← Union_mul_right_image,
   exact is_open_Union (λa, is_open_Union $ λha, this _),
 end
 
-variables (α)
+variables (G)
 
-lemma topological_group.t1_space (h : @is_closed α _ {1}) : t1_space α :=
+lemma topological_group.t1_space (h : @is_closed G _ {1}) : t1_space G :=
 ⟨assume x, by { convert is_closed_map_mul_right x _ h, simp }⟩
 
-lemma topological_group.regular_space [t1_space α] : regular_space α :=
+lemma topological_group.regular_space [t1_space G] : regular_space G :=
 ⟨assume s a hs ha,
- let f := λ p : α × α, p.1 * (p.2)⁻¹ in
+ let f := λ p : G × G, p.1 * (p.2)⁻¹ in
  have hf : continuous f :=
    continuous_mul.comp (continuous_fst.prod_mk (continuous_inv.comp continuous_snd)),
  -- a ∈ -s implies f (a, 1) ∈ -s, and so (a, 1) ∈ f⁻¹' (-s);
  -- and so can find t₁ t₂ open such that a ∈ t₁ × t₂ ⊆ f⁻¹' (-s)
  let ⟨t₁, t₂, ht₁, ht₂, a_mem_t₁, one_mem_t₂, t_subset⟩ :=
-   is_open_prod_iff.1 (hf _ (is_open_compl_iff.2 hs)) a (1:α) (by simpa [f]) in
+   is_open_prod_iff.1 (hf _ (is_open_compl_iff.2 hs)) a (1:G) (by simpa [f]) in
  begin
    use s * t₂,
    use is_open_mul_left ht₂,
@@ -407,7 +407,7 @@ lemma topological_group.regular_space [t1_space α] : regular_space α :=
 
 local attribute [instance] topological_group.regular_space
 
-lemma topological_group.t2_space [t1_space α] : t2_space α := regular_space.t2_space α
+lemma topological_group.t2_space [t1_space G] : t2_space G := regular_space.t2_space G
 
 end
 
@@ -415,16 +415,16 @@ section
 
 /-! Some results about an open set containing the product of two sets in a topological group. -/
 
-variables [topological_space α] [group α] [topological_group α]
+variables [topological_space G] [group G] [topological_group G]
 /-- Given a open neighborhood `U` of `1` there is a open neighborhood `V` of `1`
   such that `VV ⊆ U`. -/
 @[to_additive "Given a open neighborhood `U` of `0` there is a open neighborhood `V` of `0`
   such that `V + V ⊆ U`."]
-lemma one_open_separated_mul {U : set α} (h1U : is_open U) (h2U : (1 : α) ∈ U) :
-  ∃ V : set α, is_open V ∧ (1 : α) ∈ V ∧ V * V ⊆ U :=
+lemma one_open_separated_mul {U : set G} (h1U : is_open U) (h2U : (1 : G) ∈ U) :
+  ∃ V : set G, is_open V ∧ (1 : G) ∈ V ∧ V * V ⊆ U :=
 begin
   rcases exists_nhds_square (continuous_mul U h1U) (by simp only [mem_preimage, one_mul, h2U] :
-    ((1 : α), (1 : α)) ∈ (λ p : α × α, p.1 * p.2) ⁻¹' U) with ⟨V, h1V, h2V, h3V⟩,
+    ((1 : G), (1 : G)) ∈ (λ p : G × G, p.1 * p.2) ⁻¹' U) with ⟨V, h1V, h2V, h3V⟩,
   refine ⟨V, h1V, h2V, _⟩,
   rwa [← image_subset_iff, image_mul_prod] at h3V
 end
@@ -433,14 +433,14 @@ end
   such that `KV ⊆ U`. -/
 @[to_additive "Given a compact set `K` inside an open set `U`, there is a open neighborhood `V` of `0`
   such that `K + V ⊆ U`."]
-lemma compact_open_separated_mul {K U : set α} (hK : is_compact K) (hU : is_open U) (hKU : K ⊆ U) :
-  ∃ V : set α, is_open V ∧ (1 : α) ∈ V ∧ K * V ⊆ U :=
+lemma compact_open_separated_mul {K U : set G} (hK : is_compact K) (hU : is_open U) (hKU : K ⊆ U) :
+  ∃ V : set G, is_open V ∧ (1 : G) ∈ V ∧ K * V ⊆ U :=
 begin
-  let W : α → set α := λ x, (λ y, x * y) ⁻¹' U,
+  let W : G → set G := λ x, (λ y, x * y) ⁻¹' U,
   have h1W : ∀ x, is_open (W x) := λ x, continuous_mul_left x U hU,
-  have h2W : ∀ x ∈ K, (1 : α) ∈ W x := λ x hx, by simp only [mem_preimage, mul_one, hKU hx],
+  have h2W : ∀ x ∈ K, (1 : G) ∈ W x := λ x hx, by simp only [mem_preimage, mul_one, hKU hx],
   choose V hV using λ x : K, one_open_separated_mul (h1W x) (h2W x.1 x.2),
-  let X : K → set α := λ x, (λ y, (x : α)⁻¹ * y) ⁻¹' (V x),
+  let X : K → set G := λ x, (λ y, (x : G)⁻¹ * y) ⁻¹' (V x),
   cases hK.elim_finite_subcover X (λ x, continuous_mul_left x⁻¹ (V x) (hV x).1) _ with t ht, swap,
   { intros x hx, rw [mem_Union], use ⟨x, hx⟩, rw [mem_preimage], convert (hV _).2.1,
     simp only [mul_left_inv, subtype.coe_mk] },
@@ -448,7 +448,7 @@ begin
   { simp only [mem_Inter], intros x hx, exact (hV x).2.1 },
   rintro _ ⟨x, y, hx, hy, rfl⟩, simp only [mem_Inter] at hy,
   have := ht hx, simp only [mem_Union, mem_preimage] at this, rcases this with ⟨z, h1z, h2z⟩,
-  have : (z : α)⁻¹ * x * y ∈ W z := (hV z).2.2 (mul_mem_mul h2z (hy z h1z)),
+  have : (z : G)⁻¹ * x * y ∈ W z := (hV z).2.2 (mul_mem_mul h2z (hy z h1z)),
   rw [mem_preimage] at this, convert this using 1, simp only [mul_assoc, mul_inv_cancel_left]
 end
 
@@ -456,11 +456,11 @@ end
   with non-empty interior. -/
 @[to_additive "A compact set is covered by finitely many left additive translates of a set
   with non-empty interior."]
-lemma compact_covered_by_mul_left_translates {K V : set α} (hK : is_compact K)
-  (hV : (interior V).nonempty) : ∃ t : finset α, K ⊆ ⋃ g ∈ t, (λ h, g * h) ⁻¹' V :=
+lemma compact_covered_by_mul_left_translates {K V : set G} (hK : is_compact K)
+  (hV : (interior V).nonempty) : ∃ t : finset G, K ⊆ ⋃ g ∈ t, (λ h, g * h) ⁻¹' V :=
 begin
   cases hV with g₀ hg₀,
-  rcases is_compact.elim_finite_subcover hK (λ x : α, interior $ (λ h, x * h) ⁻¹' V) _ _ with ⟨t, ht⟩,
+  rcases is_compact.elim_finite_subcover hK (λ x : G, interior $ (λ h, x * h) ⁻¹' V) _ _ with ⟨t, ht⟩,
   { refine ⟨t, subset.trans ht _⟩,
     apply Union_subset_Union, intro g, apply Union_subset_Union, intro hg, apply interior_subset },
   { intro g, apply is_open_interior },
@@ -472,10 +472,10 @@ end
 end
 
 section
-variables [topological_space α] [comm_group α] [topological_group α]
+variables [topological_space G] [comm_group G] [topological_group G]
 
 @[to_additive]
-lemma nhds_mul (x y : α) : 𝓝 (x * y) = 𝓝 x * 𝓝 y :=
+lemma nhds_mul (x y : G) : 𝓝 (x * y) = 𝓝 x * 𝓝 y :=
 filter_eq $ set.ext $ assume s,
 begin
   rw [← nhds_translation_mul_inv x, ← nhds_translation_mul_inv y, ← nhds_translation_mul_inv (x*y)],
@@ -498,7 +498,7 @@ begin
 end
 
 @[to_additive]
-lemma nhds_is_mul_hom : is_mul_hom (λx:α, 𝓝 x) := ⟨λ_ _, nhds_mul _ _⟩
+lemma nhds_is_mul_hom : is_mul_hom (λx:G, 𝓝 x) := ⟨λ_ _, nhds_mul _ _⟩
 
 end
 
diff --git a/src/topology/algebra/monoid.lean b/src/topology/algebra/monoid.lean
index 106a2c05e3114..a2f20ec9142ac 100644
--- a/src/topology/algebra/monoid.lean
+++ b/src/topology/algebra/monoid.lean
@@ -12,31 +12,31 @@ import algebra.group.prod
 open classical set filter topological_space
 open_locale classical topological_space big_operators
 
-variables {α : Type*} {β : Type*} {γ : Type*}
+variables {α β M N : Type*}
 
 /-- Basic hypothesis to talk about a topological additive monoid or a topological additive
 semigroup. A topological additive monoid over `α`, for example, is obtained by requiring both the
 instances `add_monoid α` and `has_continuous_add α`. -/
-class has_continuous_add (α : Type*) [topological_space α] [has_add α] : Prop :=
-(continuous_add : continuous (λp:α×α, p.1 + p.2))
+class has_continuous_add (M : Type*) [topological_space M] [has_add M] : Prop :=
+(continuous_add : continuous (λ p : M × M, p.1 + p.2))
 
 /-- Basic hypothesis to talk about a topological monoid or a topological semigroup.
 A topological monoid over `α`, for example, is obtained by requiring both the instances `monoid α`
 and `has_continuous_mul α`. -/
 @[to_additive]
-class has_continuous_mul (α : Type*) [topological_space α] [has_mul α] : Prop :=
-(continuous_mul : continuous (λp:α×α, p.1 * p.2))
+class has_continuous_mul (M : Type*) [topological_space M] [has_mul M] : Prop :=
+(continuous_mul : continuous (λ p : M × M, p.1 * p.2))
 
 section has_continuous_mul
 
-variables [topological_space α] [has_mul α] [has_continuous_mul α]
+variables [topological_space M] [has_mul M] [has_continuous_mul M]
 
 @[to_additive]
-lemma continuous_mul : continuous (λp:α×α, p.1 * p.2) :=
+lemma continuous_mul : continuous (λp:M×M, p.1 * p.2) :=
 has_continuous_mul.continuous_mul
 
 @[to_additive, continuity]
-lemma continuous.mul [topological_space β] {f : β → α} {g : β → α}
+lemma continuous.mul [topological_space α] {f : α → M} {g : α → M}
   (hf : continuous f) (hg : continuous g) :
   continuous (λx, f x * g x) :=
 continuous_mul.comp (hf.prod_mk hg)
@@ -44,43 +44,43 @@ continuous_mul.comp (hf.prod_mk hg)
 attribute [continuity] continuous.add
 
 @[to_additive]
-lemma continuous_mul_left (a : α) : continuous (λ b:α, a * b) :=
+lemma continuous_mul_left (a : M) : continuous (λ b:M, a * b) :=
 continuous_const.mul continuous_id
 
 @[to_additive]
-lemma continuous_mul_right (a : α) : continuous (λ b:α, b * a) :=
+lemma continuous_mul_right (a : M) : continuous (λ b:M, b * a) :=
 continuous_id.mul continuous_const
 
 @[to_additive]
-lemma continuous_on.mul [topological_space β] {f : β → α} {g : β → α} {s : set β}
+lemma continuous_on.mul [topological_space α] {f : α → M} {g : α → M} {s : set α}
   (hf : continuous_on f s) (hg : continuous_on g s) :
   continuous_on (λx, f x * g x) s :=
 (continuous_mul.comp_continuous_on (hf.prod hg) : _)
 
 @[to_additive]
-lemma tendsto_mul {a b : α} : tendsto (λp:α×α, p.fst * p.snd) (𝓝 (a, b)) (𝓝 (a * b)) :=
+lemma tendsto_mul {a b : M} : tendsto (λp:M×M, p.fst * p.snd) (𝓝 (a, b)) (𝓝 (a * b)) :=
 continuous_iff_continuous_at.mp has_continuous_mul.continuous_mul (a, b)
 
 @[to_additive]
-lemma filter.tendsto.mul {f : β → α} {g : β → α} {x : filter β} {a b : α}
+lemma filter.tendsto.mul {f : α → M} {g : α → M} {x : filter α} {a b : M}
   (hf : tendsto f x (𝓝 a)) (hg : tendsto g x (𝓝 b)) :
   tendsto (λx, f x * g x) x (𝓝 (a * b)) :=
 tendsto_mul.comp (hf.prod_mk_nhds hg)
 
 @[to_additive]
-lemma continuous_at.mul [topological_space β] {f : β → α} {g : β → α} {x : β}
+lemma continuous_at.mul [topological_space α] {f : α → M} {g : α → M} {x : α}
   (hf : continuous_at f x) (hg : continuous_at g x) :
   continuous_at (λx, f x * g x) x :=
 hf.mul hg
 
 @[to_additive]
-lemma continuous_within_at.mul [topological_space β] {f : β → α} {g : β → α} {s : set β} {x : β}
+lemma continuous_within_at.mul [topological_space α] {f : α → M} {g : α → M} {s : set α} {x : α}
   (hf : continuous_within_at f s x) (hg : continuous_within_at g s x) :
   continuous_within_at (λx, f x * g x) s x :=
 hf.mul hg
 
 @[to_additive]
-instance [topological_space β] [has_mul β] [has_continuous_mul β] : has_continuous_mul (α × β) :=
+instance [topological_space N] [has_mul N] [has_continuous_mul N] : has_continuous_mul (M × N) :=
 ⟨((continuous_fst.comp continuous_fst).mul (continuous_fst.comp continuous_snd)).prod_mk
  ((continuous_snd.comp continuous_fst).mul (continuous_snd.comp continuous_snd))⟩
 
@@ -88,11 +88,11 @@ end has_continuous_mul
 
 section has_continuous_mul
 
-variables [topological_space α] [monoid α] [has_continuous_mul α]
+variables [topological_space M] [monoid M] [has_continuous_mul M]
 
 @[to_additive]
-lemma tendsto_list_prod {f : γ → β → α} {x : filter β} {a : γ → α} :
-  ∀l:list γ, (∀c∈l, tendsto (f c) x (𝓝 (a c))) →
+lemma tendsto_list_prod {f : β → α → M} {x : filter α} {a : β → M} :
+  ∀l:list β, (∀c∈l, tendsto (f c) x (𝓝 (a c))) →
     tendsto (λb, (l.map (λc, f c b)).prod) x (𝓝 ((l.map a).prod))
 | []       _ := by simp [tendsto_const_nhds]
 | (f :: l) h :=
@@ -103,7 +103,7 @@ lemma tendsto_list_prod {f : γ → β → α} {x : filter β} {a : γ → α} :
   end
 
 @[to_additive]
-lemma continuous_list_prod [topological_space β] {f : γ → β → α} (l : list γ)
+lemma continuous_list_prod [topological_space α] {f : β → α → M} (l : list β)
   (h : ∀c∈l, continuous (f c)) :
   continuous (λa, (l.map (λc, f c a)).prod) :=
 continuous_iff_continuous_at.2 $ assume x, tendsto_list_prod l $ assume c hc,
@@ -111,12 +111,12 @@ continuous_iff_continuous_at.2 $ assume x, tendsto_list_prod l $ assume c hc,
 
 -- @[to_additive continuous_smul]
 @[continuity]
-lemma continuous_pow : ∀ n : ℕ, continuous (λ a : α, a ^ n)
+lemma continuous_pow : ∀ n : ℕ, continuous (λ a : M, a ^ n)
 | 0 := by simpa using continuous_const
-| (k+1) := show continuous (λ (a : α), a * a ^ k), from continuous_id.mul (continuous_pow _)
+| (k+1) := show continuous (λ (a : M), a * a ^ k), from continuous_id.mul (continuous_pow _)
 
 @[continuity]
-lemma continuous.pow {f : β → α} [topological_space β] (h : continuous f) (n : ℕ) :
+lemma continuous.pow {f : α → M} [topological_space α] (h : continuous f) (n : ℕ) :
   continuous (λ b, (f b) ^ n) :=
 continuous.comp (continuous_pow n) h
 
@@ -124,35 +124,35 @@ end has_continuous_mul
 
 section
 
-variables [topological_space α] [comm_monoid α]
+variables [topological_space M] [comm_monoid M]
 
 @[to_additive]
-lemma submonoid.mem_nhds_one (β : submonoid α) (oβ : is_open (β : set α)) :
-  (β : set α) ∈ 𝓝 (1 : α) :=
-mem_nhds_sets_iff.2 ⟨β, (by refl), oβ, β.one_mem⟩
+lemma submonoid.mem_nhds_one (S : submonoid M) (oS : is_open (S : set M)) :
+  (S : set M) ∈ 𝓝 (1 : M) :=
+mem_nhds_sets oS S.one_mem
 
-variable [has_continuous_mul α]
+variable [has_continuous_mul M]
 
 @[to_additive]
-lemma tendsto_multiset_prod {f : γ → β → α} {x : filter β} {a : γ → α} (s : multiset γ) :
+lemma tendsto_multiset_prod {f : β → α → M} {x : filter α} {a : β → M} (s : multiset β) :
   (∀c∈s, tendsto (f c) x (𝓝 (a c))) →
     tendsto (λb, (s.map (λc, f c b)).prod) x (𝓝 ((s.map a).prod)) :=
 by { rcases s with ⟨l⟩, simp, exact tendsto_list_prod l }
 
 @[to_additive]
-lemma tendsto_finset_prod {f : γ → β → α} {x : filter β} {a : γ → α} (s : finset γ) :
+lemma tendsto_finset_prod {f : β → α → M} {x : filter α} {a : β → M} (s : finset β) :
   (∀c∈s, tendsto (f c) x (𝓝 (a c))) → tendsto (λb, ∏ c in s, f c b) x (𝓝 (∏ c in s, a c)) :=
 tendsto_multiset_prod _
 
 @[to_additive, continuity]
-lemma continuous_multiset_prod [topological_space β] {f : γ → β → α} (s : multiset γ) :
+lemma continuous_multiset_prod [topological_space α] {f : β → α → M} (s : multiset β) :
   (∀c∈s, continuous (f c)) → continuous (λa, (s.map (λc, f c a)).prod) :=
 by { rcases s with ⟨l⟩, simp, exact continuous_list_prod l }
 
 attribute [continuity] continuous_multiset_sum
 
 @[to_additive, continuity]
-lemma continuous_finset_prod [topological_space β] {f : γ → β → α} (s : finset γ) :
+lemma continuous_finset_prod [topological_space α] {f : β → α → M} (s : finset β) :
   (∀c∈s, continuous (f c)) → continuous (λa, ∏ c in s, f c a) :=
 continuous_multiset_prod _