diff --git a/src/analysis/fourier.lean b/src/analysis/fourier.lean
index 89c31c8098ea9..651ca554eca83 100644
--- a/src/analysis/fourier.lean
+++ b/src/analysis/fourier.lean
@@ -85,7 +85,7 @@ section monomials
 continuous maps from `circle` to `ℂ`. -/
 @[simps] def fourier (n : ℤ) : C(circle, ℂ) :=
 { to_fun := λ z, z ^ n,
-  continuous_to_fun := continuous_subtype_coe.zpow n $ λ z, or.inl (ne_zero_of_mem_circle z) }
+  continuous_to_fun := continuous_subtype_coe.zpow₀ n $ λ z, or.inl (ne_zero_of_mem_circle z) }
 
 @[simp] lemma fourier_zero {z : circle} : fourier 0 z = 1 := rfl
 
diff --git a/src/analysis/special_functions/integrals.lean b/src/analysis/special_functions/integrals.lean
index 1c8b788600973..d588831d4ecd4 100644
--- a/src/analysis/special_functions/integrals.lean
+++ b/src/analysis/special_functions/integrals.lean
@@ -46,7 +46,7 @@ lemma interval_integrable_pow : interval_integrable (λ x, x^n) μ a b :=
 
 lemma interval_integrable_zpow {n : ℤ} (h : 0 ≤ n ∨ (0 : ℝ) ∉ [a, b]) :
   interval_integrable (λ x, x ^ n) μ a b :=
-(continuous_on_id.zpow n $ λ x hx, h.symm.imp (ne_of_mem_of_not_mem hx) id).interval_integrable
+(continuous_on_id.zpow₀ n $ λ x hx, h.symm.imp (ne_of_mem_of_not_mem hx) id).interval_integrable
 
 lemma interval_integrable_rpow {r : ℝ} (h : 0 ≤ r ∨ (0 : ℝ) ∉ [a, b]) :
   interval_integrable (λ x, x ^ r) μ a b :=
diff --git a/src/analysis/specific_limits.lean b/src/analysis/specific_limits.lean
index d7d6d1046a1b2..3ad31d1552fa8 100644
--- a/src/analysis/specific_limits.lean
+++ b/src/analysis/specific_limits.lean
@@ -101,7 +101,7 @@ end
 @[simp] lemma continuous_at_zpow {𝕜 : Type*} [nondiscrete_normed_field 𝕜] {m : ℤ} {x : 𝕜} :
   continuous_at (λ x, x ^ m) x ↔ x ≠ 0 ∨ 0 ≤ m :=
 begin
-  refine ⟨_, continuous_at_zpow _ _⟩,
+  refine ⟨_, continuous_at_zpow₀ _ _⟩,
   contrapose!, rintro ⟨rfl, hm⟩ hc,
   exact not_tendsto_at_top_of_tendsto_nhds (hc.tendsto.mono_left nhds_within_le_nhds).norm
       (tendsto_norm_zpow_nhds_within_0_at_top hm)
diff --git a/src/measure_theory/integral/circle_integral.lean b/src/measure_theory/integral/circle_integral.lean
index c155a91924c11..965deaefb28cc 100644
--- a/src/measure_theory/integral/circle_integral.lean
+++ b/src/measure_theory/integral/circle_integral.lean
@@ -260,7 +260,7 @@ begin
     refine (zpow_strict_anti this.1 this.2).le_iff_le.2 (int.lt_add_one_iff.1 _), exact hn },
   { rintro (rfl|H),
     exacts [circle_integrable_zero_radius,
-      ((continuous_on_id.sub continuous_on_const).zpow _ $ λ z hz, H.symm.imp_left $
+      ((continuous_on_id.sub continuous_on_const).zpow₀ _ $ λ z hz, H.symm.imp_left $
         λ hw, sub_ne_zero.2 $ ne_of_mem_of_not_mem hz hw).circle_integrable'] },
 end
 
diff --git a/src/topology/algebra/group.lean b/src/topology/algebra/group.lean
index dcc0d96dc5fb1..f4f42e5a7eeab 100644
--- a/src/topology/algebra/group.lean
+++ b/src/topology/algebra/group.lean
@@ -250,6 +250,48 @@ hf.inv
 lemma is_compact.inv {s : set G} (hs : is_compact s) : is_compact (s⁻¹) :=
 by { rw [← image_inv], exact hs.image continuous_inv }
 
+section zpow
+
+@[continuity, to_additive]
+lemma continuous_zpow : ∀ z : ℤ, continuous (λ a : G, a ^ z)
+| (int.of_nat n) := by simpa using continuous_pow n
+| -[1+n] := by simpa using (continuous_pow (n + 1)).inv
+
+@[continuity, to_additive]
+lemma continuous.zpow {f : α → G} (h : continuous f) (z : ℤ) :
+  continuous (λ b, (f b) ^ z) :=
+(continuous_zpow z).comp h
+
+@[to_additive]
+lemma continuous_on_zpow {s : set G} (z : ℤ) : continuous_on (λ x, x ^ z) s :=
+(continuous_zpow z).continuous_on
+
+@[to_additive]
+lemma continuous_at_zpow (x : G) (z : ℤ) : continuous_at (λ x, x ^ z) x :=
+(continuous_zpow z).continuous_at
+
+@[to_additive]
+lemma filter.tendsto.zpow {α} {l : filter α} {f : α → G} {x : G} (hf : tendsto f l (𝓝 x)) (z : ℤ) :
+  tendsto (λ x, f x ^ z) l (𝓝 (x ^ z)) :=
+(continuous_at_zpow _ _).tendsto.comp hf
+
+@[to_additive]
+lemma continuous_within_at.zpow {f : α → G} {x : α} {s : set α} (hf : continuous_within_at f s x)
+  (z : ℤ) : continuous_within_at (λ x, f x ^ z) s x :=
+hf.zpow z
+
+@[to_additive]
+lemma continuous_at.zpow {f : α → G} {x : α} (hf : continuous_at f x) (z : ℤ) :
+  continuous_at (λ x, f x ^ z) x :=
+hf.zpow z
+
+@[to_additive continuous_on.zsmul]
+lemma continuous_on.zpow {f : α → G} {s : set α} (hf : continuous_on f s) (z : ℤ) :
+  continuous_on (λ x, f x ^ z) s :=
+λ x hx, (hf x hx).zpow z
+
+end zpow
+
 section ordered_comm_group
 
 variables [topological_space H] [ordered_comm_group H] [topological_group H]
diff --git a/src/topology/algebra/group_with_zero.lean b/src/topology/algebra/group_with_zero.lean
index 91620671d73a6..a6534011d81f8 100644
--- a/src/topology/algebra/group_with_zero.lean
+++ b/src/topology/algebra/group_with_zero.lean
@@ -235,7 +235,7 @@ section zpow
 variables [group_with_zero G₀] [topological_space G₀] [has_continuous_inv₀ G₀]
   [has_continuous_mul G₀]
 
-lemma continuous_at_zpow (x : G₀) (m : ℤ) (h : x ≠ 0 ∨ 0 ≤ m) : continuous_at (λ x, x ^ m) x :=
+lemma continuous_at_zpow₀ (x : G₀) (m : ℤ) (h : x ≠ 0 ∨ 0 ≤ m) : continuous_at (λ x, x ^ m) x :=
 begin
   cases m,
   { simpa only [zpow_of_nat] using continuous_at_pow x m },
@@ -244,30 +244,30 @@ begin
     exact (continuous_at_pow x (m + 1)).inv₀ (pow_ne_zero _ hx) }
 end
 
-lemma continuous_on_zpow (m : ℤ) : continuous_on (λ x : G₀, x ^ m) {0}ᶜ :=
-λ x hx, (continuous_at_zpow _ _ (or.inl hx)).continuous_within_at
+lemma continuous_on_zpow₀ (m : ℤ) : continuous_on (λ x : G₀, x ^ m) {0}ᶜ :=
+λ x hx, (continuous_at_zpow₀ _ _ (or.inl hx)).continuous_within_at
 
-lemma filter.tendsto.zpow {f : α → G₀} {l : filter α} {a : G₀} (hf : tendsto f l (𝓝 a)) (m : ℤ)
+lemma filter.tendsto.zpow₀ {f : α → G₀} {l : filter α} {a : G₀} (hf : tendsto f l (𝓝 a)) (m : ℤ)
   (h : a ≠ 0 ∨ 0 ≤ m) :
   tendsto (λ x, (f x) ^ m) l (𝓝 (a ^ m)) :=
-(continuous_at_zpow _ m h).tendsto.comp hf
+(continuous_at_zpow₀ _ m h).tendsto.comp hf
 
 variables {X : Type*} [topological_space X] {a : X} {s : set X} {f : X → G₀}
 
-lemma continuous_at.zpow (hf : continuous_at f a) (m : ℤ) (h : f a ≠ 0 ∨ 0 ≤ m) :
+lemma continuous_at.zpow₀ (hf : continuous_at f a) (m : ℤ) (h : f a ≠ 0 ∨ 0 ≤ m) :
   continuous_at (λ x, (f x) ^ m) a :=
-hf.zpow m h
+hf.zpow₀ m h
 
-lemma continuous_within_at.zpow (hf : continuous_within_at f s a) (m : ℤ) (h : f a ≠ 0 ∨ 0 ≤ m) :
+lemma continuous_within_at.zpow₀ (hf : continuous_within_at f s a) (m : ℤ) (h : f a ≠ 0 ∨ 0 ≤ m) :
   continuous_within_at (λ x, f x ^ m) s a :=
-hf.zpow m h
+hf.zpow₀ m h
 
-lemma continuous_on.zpow (hf : continuous_on f s) (m : ℤ) (h : ∀ a ∈ s, f a ≠ 0 ∨ 0 ≤ m) :
+lemma continuous_on.zpow₀ (hf : continuous_on f s) (m : ℤ) (h : ∀ a ∈ s, f a ≠ 0 ∨ 0 ≤ m) :
   continuous_on (λ x, f x ^ m) s :=
-λ a ha, (hf a ha).zpow m (h a ha)
+λ a ha, (hf a ha).zpow₀ m (h a ha)
 
-@[continuity] lemma continuous.zpow (hf : continuous f) (m : ℤ) (h0 : ∀ a, f a ≠ 0 ∨ 0 ≤ m) :
+@[continuity] lemma continuous.zpow₀ (hf : continuous f) (m : ℤ) (h0 : ∀ a, f a ≠ 0 ∨ 0 ≤ m) :
   continuous (λ x, (f x) ^ m) :=
-continuous_iff_continuous_at.2 $ λ x, (hf.tendsto x).zpow m (h0 x)
+continuous_iff_continuous_at.2 $ λ x, (hf.tendsto x).zpow₀ m (h0 x)
 
 end zpow
diff --git a/src/topology/category/Top/basic.lean b/src/topology/category/Top/basic.lean
index 5e29277543f53..59a22e0dd3533 100644
--- a/src/topology/category/Top/basic.lean
+++ b/src/topology/category/Top/basic.lean
@@ -26,7 +26,7 @@ def Top : Type (u+1) := bundled topological_space
 namespace Top
 
 instance bundled_hom : bundled_hom @continuous_map :=
-⟨@continuous_map.to_fun, @continuous_map.id, @continuous_map.comp, @continuous_map.coe_inj⟩
+⟨@continuous_map.to_fun, @continuous_map.id, @continuous_map.comp, @continuous_map.coe_injective⟩
 
 attribute [derive [large_category, concrete_category]] Top
 
diff --git a/src/topology/category/Top/limits.lean b/src/topology/category/Top/limits.lean
index a0e6bd6a6f116..d59cd11dfa5bd 100644
--- a/src/topology/category/Top/limits.lean
+++ b/src/topology/category/Top/limits.lean
@@ -56,8 +56,8 @@ def limit_cone_infi (F : J ⥤ Top.{u}) : cone F :=
   π :=
   { app := λ j, ⟨(types.limit_cone (F ⋙ forget)).π.app j,
                  continuous_iff_le_induced.mpr (infi_le _ _)⟩,
-    naturality' := λ j j' f,
-                   continuous_map.coe_inj ((types.limit_cone (F ⋙ forget)).π.naturality f) } }
+    naturality' := λ j j' f, continuous_map.coe_injective
+      ((types.limit_cone (F ⋙ forget)).π.naturality f) } }
 
 /--
 The chosen cone `Top.limit_cone F` for a functor `F : J ⥤ Top` is a limit cone.
@@ -100,8 +100,8 @@ def colimit_cocone (F : J ⥤ Top.{u}) : cocone F :=
   ι :=
   { app := λ j, ⟨(types.colimit_cocone (F ⋙ forget)).ι.app j,
                  continuous_iff_coinduced_le.mpr (le_supr _ j)⟩,
-    naturality' := λ j j' f,
-                   continuous_map.coe_inj ((types.colimit_cocone (F ⋙ forget)).ι.naturality f) } }
+    naturality' := λ j j' f, continuous_map.coe_injective
+      ((types.colimit_cocone (F ⋙ forget)).ι.naturality f) } }
 
 /--
 The chosen cocone `Top.colimit_cocone F` for a functor `F : J ⥤ Top` is a colimit cocone.
diff --git a/src/topology/continuous_function/algebra.lean b/src/topology/continuous_function/algebra.lean
index 5f242d44fcb96..735efe4b87b34 100644
--- a/src/topology/continuous_function/algebra.lean
+++ b/src/topology/continuous_function/algebra.lean
@@ -38,7 +38,8 @@ instance : has_coe_to_fun {f : α → β | continuous f} (λ _, α → β) :=  
 end continuous_functions
 
 namespace continuous_map
-variables {α : Type*} {β : Type*} [topological_space α] [topological_space β]
+variables {α : Type*} {β : Type*} {γ : Type*}
+variables [topological_space α] [topological_space β] [topological_space γ]
 
 @[to_additive]
 instance has_mul [has_mul β] [has_continuous_mul β] : has_mul C(α, β) :=
@@ -48,23 +49,79 @@ instance has_mul [has_mul β] [has_continuous_mul β] : has_mul C(α, β) :=
 lemma coe_mul [has_mul β] [has_continuous_mul β] (f g : C(α, β)) :
   ((f * g : C(α, β)) : α → β) = (f : α → β) * (g : α → β) := rfl
 
+@[simp, to_additive] lemma mul_comp [has_mul γ] [has_continuous_mul γ]
+  (f₁ f₂ : C(β, γ)) (g : C(α, β)) :
+  (f₁ * f₂).comp g = f₁.comp g * f₂.comp g :=
+rfl
+
 @[to_additive]
 instance [has_one β] : has_one C(α, β) := ⟨const (1 : β)⟩
 
 @[simp, norm_cast, to_additive]
-lemma coe_one [has_one β]  :
-  ((1 : C(α, β)) : α → β) = (1 : α → β) := rfl
-
-@[simp, to_additive] lemma mul_comp {α : Type*} {β : Type*} {γ : Type*}
-  [topological_space α] [topological_space β] [topological_space γ]
-  [semigroup γ] [has_continuous_mul γ] (f₁ f₂ : C(β, γ)) (g : C(α, β)) :
-  (f₁ * f₂).comp g = f₁.comp g * f₂.comp g :=
-by { ext, simp, }
+lemma coe_one [has_one β] : ((1 : C(α, β)) : α → β) = (1 : α → β) := rfl
 
-@[simp, to_additive] lemma one_comp {α : Type*} {β : Type*} {γ : Type*}
-  [topological_space α] [topological_space β] [topological_space γ] [has_one γ] (g : C(α, β)) :
+@[simp, to_additive] lemma one_comp [has_one γ] (g : C(α, β)) :
   (1 : C(β, γ)).comp g = 1 :=
-by { ext, simp, }
+rfl
+instance has_nsmul [add_monoid β] [has_continuous_add β] : has_scalar ℕ C(α, β) :=
+⟨λ n f, ⟨n • f, f.continuous.nsmul n⟩⟩
+
+@[to_additive has_nsmul]
+instance has_pow [monoid β] [has_continuous_mul β] : has_pow C(α, β) ℕ :=
+⟨λ f n, ⟨f ^ n, f.continuous.pow n⟩⟩
+
+@[simp, norm_cast, to_additive coe_nsmul]
+lemma coe_pow [monoid β] [has_continuous_mul β] (f : C(α, β)) (n : ℕ) :
+  ⇑(f ^ n) = f ^ n := rfl
+
+@[simp, to_additive nsmul_comp] lemma pow_comp [monoid γ] [has_continuous_mul γ]
+  (f : C(β, γ)) (n : ℕ) (g : C(α, β)) :
+  (f^n).comp g = (f.comp g)^n :=
+rfl
+
+@[to_additive]
+instance [group β] [topological_group β] : has_inv C(α, β) :=
+{ inv := λ f, ⟨f⁻¹, f.continuous.inv⟩ }
+
+@[simp, norm_cast, to_additive]
+lemma coe_inv [group β] [topological_group β] (f : C(α, β)) :
+  ⇑(f⁻¹) = f⁻¹ :=
+rfl
+
+@[simp, to_additive] lemma inv_comp [group γ] [topological_group γ] (f : C(β, γ)) (g : C(α, β)) :
+  (f⁻¹).comp g = (f.comp g)⁻¹ :=
+rfl
+
+@[to_additive]
+instance [has_div β] [has_continuous_div β] : has_div C(α, β) :=
+{ div := λ f g, ⟨f / g, f.continuous.div' g.continuous⟩ }
+
+@[simp, norm_cast, to_additive]
+lemma coe_div [has_div β] [has_continuous_div β] (f g : C(α, β)) : ⇑(f / g) = f / g :=
+rfl
+
+@[simp, to_additive] lemma div_comp [has_div γ] [has_continuous_div γ]
+  (f g : C(β, γ)) (h : C(α, β)) :
+  (f / g).comp h = (f.comp h) / (g.comp h) :=
+rfl
+
+instance has_zsmul [add_group β] [topological_add_group β] : has_scalar ℤ C(α, β) :=
+{ smul := λ z f, ⟨z • f, f.continuous.zsmul z⟩ }
+
+@[to_additive]
+instance has_zpow [group β] [topological_group β] :
+  has_pow C(α, β) ℤ :=
+{ pow := λ f z, ⟨f ^ z, f.continuous.zpow z⟩ }
+
+@[simp, norm_cast, to_additive]
+lemma coe_zpow [group β] [topological_group β] (f : C(α, β)) (z : ℤ) :
+  ⇑(f ^ z) = f ^ z :=
+rfl
+
+@[simp, to_additive]
+lemma zpow_comp [group γ] [topological_group γ] (f : C(β, γ)) (z : ℤ) (g : C(α, β)) :
+  (f^z).comp g = (f.comp g)^z :=
+rfl
 
 end continuous_map
 
@@ -102,16 +159,39 @@ namespace continuous_map
 @[to_additive]
 instance {α : Type*} {β : Type*} [topological_space α]
   [topological_space β] [semigroup β] [has_continuous_mul β] : semigroup C(α, β) :=
-{ mul_assoc := λ a b c, by ext; exact mul_assoc _ _ _,
-  ..continuous_map.has_mul}
+coe_injective.semigroup _ coe_mul
+
+@[to_additive]
+instance {α : Type*} {β : Type*} [topological_space α]
+  [topological_space β] [comm_semigroup β] [has_continuous_mul β] : comm_semigroup C(α, β) :=
+coe_injective.comm_semigroup _ coe_mul
+
+@[to_additive]
+instance {α : Type*} {β : Type*} [topological_space α]
+  [topological_space β] [mul_one_class β] [has_continuous_mul β] : mul_one_class C(α, β) :=
+coe_injective.mul_one_class _ coe_one coe_mul
+
+instance {α : Type*} {β : Type*} [topological_space α]
+  [topological_space β] [mul_zero_class β] [has_continuous_mul β] : mul_zero_class C(α, β) :=
+coe_injective.mul_zero_class _ coe_zero coe_mul
 
 @[to_additive]
 instance {α : Type*} {β : Type*} [topological_space α] [topological_space β]
   [monoid β] [has_continuous_mul β] : monoid C(α, β) :=
-{ one_mul := λ a, by ext; exact one_mul _,
-  mul_one := λ a, by ext; exact mul_one _,
-  ..continuous_map.semigroup,
-  ..continuous_map.has_one }
+coe_injective.monoid_pow _ coe_one coe_mul coe_pow
+
+instance {α : Type*} {β : Type*} [topological_space α] [topological_space β]
+  [monoid_with_zero β] [has_continuous_mul β] : monoid_with_zero C(α, β) :=
+{ ..continuous_map.monoid, ..continuous_map.mul_zero_class }
+
+@[to_additive]
+instance {α : Type*} {β : Type*} [topological_space α]
+  [topological_space β] [comm_monoid β] [has_continuous_mul β] : comm_monoid C(α, β) :=
+{ ..continuous_map.comm_semigroup, ..continuous_map.monoid }
+
+instance {α : Type*} {β : Type*} [topological_space α] [topological_space β]
+  [comm_monoid_with_zero β] [has_continuous_mul β] : comm_monoid_with_zero C(α, β) :=
+{ ..continuous_map.comm_monoid, ..continuous_map.monoid_with_zero }
 
 /-- Coercion to a function as an `monoid_hom`. Similar to `monoid_hom.coe_fn`. -/
 @[to_additive "Coercion to a function as an `add_monoid_hom`. Similar to `add_monoid_hom.coe_fn`.",
@@ -137,30 +217,9 @@ protected def _root_.monoid_hom.comp_left_continuous (α : Type*) {β : Type*} {
 `add_monoid_hom.comp_hom'`.", simps]
 def comp_monoid_hom' {α : Type*} {β : Type*} {γ : Type*}
   [topological_space α] [topological_space β] [topological_space γ]
-  [monoid γ] [has_continuous_mul γ] (g : C(α, β)) : C(β, γ) →* C(α, γ) :=
+  [mul_one_class γ] [has_continuous_mul γ] (g : C(α, β)) : C(β, γ) →* C(α, γ) :=
 { to_fun := λ f, f.comp g, map_one' := one_comp g, map_mul' := λ f₁ f₂, mul_comp f₁ f₂ g }
 
-@[simp, norm_cast]
-lemma coe_pow {α : Type*} {β : Type*} [topological_space α] [topological_space β]
-  [monoid β] [has_continuous_mul β] (f : C(α, β)) (n : ℕ) :
-  ((f^n : C(α, β)) : α → β) = (f : α → β)^n :=
-(coe_fn_monoid_hom : C(α, β) →* _).map_pow f n
-
-@[simp] lemma pow_comp {α : Type*} {β : Type*} {γ : Type*}
-  [topological_space α] [topological_space β] [topological_space γ]
-  [monoid γ] [has_continuous_mul γ] (f : C(β, γ)) (n : ℕ) (g : C(α, β)) :
-  (f^n).comp g = (f.comp g)^n :=
-(comp_monoid_hom' g).map_pow f n
-
-@[to_additive]
-instance {α : Type*} {β : Type*} [topological_space α]
-[topological_space β] [comm_monoid β] [has_continuous_mul β] : comm_monoid C(α, β) :=
-{ one_mul := λ a, by ext; exact one_mul _,
-  mul_one := λ a, by ext; exact mul_one _,
-  mul_comm := λ a b, by ext; exact mul_comm _ _,
-  ..continuous_map.semigroup,
-  ..continuous_map.has_one }
-
 open_locale big_operators
 @[simp, to_additive] lemma coe_prod {α : Type*} {β : Type*} [comm_monoid β]
   [topological_space α] [topological_space β] [has_continuous_mul β]
@@ -178,33 +237,7 @@ by simp
 @[to_additive]
 instance {α : Type*} {β : Type*} [topological_space α] [topological_space β]
   [group β] [topological_group β] : group C(α, β) :=
-{ inv := λ f, ⟨λ x, (f x)⁻¹, continuous_inv.comp f.continuous⟩,
-  mul_left_inv := λ a, by ext; exact mul_left_inv _,
-  ..continuous_map.monoid }
-
-@[simp, norm_cast, to_additive]
-lemma coe_inv {α : Type*} {β : Type*} [topological_space α] [topological_space β]
-  [group β] [topological_group β] (f : C(α, β)) :
-  ((f⁻¹ : C(α, β)) : α → β) = (f⁻¹ : α → β) :=
-rfl
-
-@[simp, norm_cast, to_additive]
-lemma coe_div {α : Type*} {β : Type*} [topological_space α] [topological_space β]
-  [group β] [topological_group β] (f g : C(α, β)) :
-  ((f / g : C(α, β)) : α → β) = (f : α → β) / (g : α → β) :=
-by { simp only [div_eq_mul_inv], refl, }
-
-@[simp, to_additive] lemma inv_comp {α : Type*} {β : Type*} {γ : Type*}
-  [topological_space α] [topological_space β] [topological_space γ]
-  [group γ] [topological_group γ] (f : C(β, γ)) (g : C(α, β)) :
-  (f⁻¹).comp g = (f.comp g)⁻¹ :=
-by { ext, simp, }
-
-@[simp, to_additive] lemma div_comp {α : Type*} {β : Type*} {γ : Type*}
-  [topological_space α] [topological_space β] [topological_space γ]
-  [group γ] [topological_group γ] (f g : C(β, γ)) (h : C(α, β)) :
-  (f / g).comp h = (f.comp h) / (g.comp h) :=
-by { ext, simp, }
+coe_injective.group_pow _ coe_one coe_mul coe_inv coe_div coe_pow coe_zpow
 
 @[to_additive]
 instance {α : Type*} {β : Type*} [topological_space α]
@@ -251,13 +284,13 @@ section subtype
 def continuous_subsemiring (α : Type*) (R : Type*) [topological_space α] [topological_space R]
   [semiring R] [topological_ring R] : subsemiring (α → R) :=
 { ..continuous_add_submonoid α R,
-  ..continuous_submonoid α R }.
+  ..continuous_submonoid α R }
 
 /-- The subring of continuous maps `α → β`. -/
 def continuous_subring (α : Type*) (R : Type*) [topological_space α] [topological_space R]
   [ring R] [topological_ring R] : subring (α → R) :=
 { ..continuous_subsemiring α R,
-  ..continuous_add_subgroup α R }.
+  ..continuous_add_subgroup α R }
 
 end subtype
 
@@ -267,10 +300,8 @@ instance {α : Type*} {β : Type*} [topological_space α] [topological_space β]
   [semiring β] [topological_ring β] : semiring C(α, β) :=
 { left_distrib := λ a b c, by ext; exact left_distrib _ _ _,
   right_distrib := λ a b c, by ext; exact right_distrib _ _ _,
-  zero_mul := λ a, by ext; exact zero_mul _,
-  mul_zero := λ a, by ext; exact mul_zero _,
   ..continuous_map.add_comm_monoid,
-  ..continuous_map.monoid }
+  ..continuous_map.monoid_with_zero }
 
 instance {α : Type*} {β : Type*} [topological_space α] [topological_space β]
   [ring β] [topological_ring β] : ring C(α, β) :=
@@ -278,10 +309,14 @@ instance {α : Type*} {β : Type*} [topological_space α] [topological_space β]
   ..continuous_map.add_comm_group, }
 
 instance {α : Type*} {β : Type*} [topological_space α]
-  [topological_space β] [comm_ring β] [topological_ring β] : comm_ring C(α, β) :=
+  [topological_space β] [comm_semiring β] [topological_ring β] : comm_semiring C(α, β) :=
 { ..continuous_map.semiring,
-  ..continuous_map.add_comm_group,
-  ..continuous_map.comm_monoid,}
+  ..continuous_map.comm_monoid, }
+
+instance {α : Type*} {β : Type*} [topological_space α]
+  [topological_space β] [comm_ring β] [topological_ring β] : comm_ring C(α, β) :=
+{ ..continuous_map.comm_semiring,
+  ..continuous_map.ring, }
 
 /-- Composition on the left by a (continuous) homomorphism of topological rings, as a `ring_hom`.
 Similar to `ring_hom.comp_left`. -/
@@ -318,55 +353,71 @@ topological semiring `R` inherit the structure of a module.
 section subtype
 
 variables (α : Type*) [topological_space α]
-variables (R : Type*) [semiring R] [topological_space R]
+variables (R : Type*) [semiring R]
 variables (M : Type*) [topological_space M] [add_comm_group M]
-variables [module R M] [has_continuous_smul R M] [topological_add_group M]
+variables [module R M] [has_continuous_const_smul R M] [topological_add_group M]
 
 /-- The `R`-submodule of continuous maps `α → M`. -/
 def continuous_submodule : submodule R (α → M) :=
 { carrier := { f : α → M | continuous f },
-  smul_mem' := λ c f hf, continuous_smul.comp
-    (continuous.prod_mk (continuous_const : continuous (λ x, c)) hf),
+  smul_mem' := λ c f hf, hf.const_smul c,
   ..continuous_add_subgroup α M }
 
 end subtype
 
 namespace continuous_map
-variables {α : Type*} [topological_space α]
-  {R : Type*} [semiring R] [topological_space R]
-  {M : Type*} [topological_space M] [add_comm_monoid M]
-  {M₂ : Type*} [topological_space M₂] [add_comm_monoid M₂]
+variables {α β : Type*} [topological_space α] [topological_space β]
+  {R R₁ : Type*}
+  {M : Type*} [topological_space M]
+  {M₂ : Type*} [topological_space M₂]
 
-instance
-  [module R M] [has_continuous_smul R M] :
-  has_scalar R C(α, M) :=
+@[to_additive continuous_map.has_vadd]
+instance [has_scalar R M] [has_continuous_const_smul R M] : has_scalar R C(α, M) :=
 ⟨λ r f, ⟨r • f, f.continuous.const_smul r⟩⟩
 
-@[simp, norm_cast]
-lemma coe_smul [module R M] [has_continuous_smul R M]
+@[simp, to_additive, norm_cast]
+lemma coe_smul [has_scalar R M] [has_continuous_const_smul R M]
   (c : R) (f : C(α, M)) : ⇑(c • f) = c • f := rfl
 
-lemma smul_apply [module R M] [has_continuous_smul R M]
+@[to_additive]
+lemma smul_apply [has_scalar R M] [has_continuous_const_smul R M]
   (c : R) (f : C(α, M)) (a : α) : (c • f) a = c • (f a) :=
-by simp
+rfl
 
-@[simp] lemma smul_comp {α : Type*} {β : Type*}
-  [topological_space α] [topological_space β]
-   [module R M] [has_continuous_smul R M] (r : R) (f : C(β, M)) (g : C(α, β)) :
+@[simp, to_additive] lemma smul_comp [has_scalar R M] [has_continuous_const_smul R M]
+  (r : R) (f : C(β, M)) (g : C(α, β)) :
   (r • f).comp g = r • (f.comp g) :=
-by { ext, simp, }
+rfl
+
+@[to_additive]
+instance [has_scalar R M] [has_continuous_const_smul R M]
+  [has_scalar R₁ M] [has_continuous_const_smul R₁ M]
+  [smul_comm_class R R₁ M] : smul_comm_class R R₁ C(α, M) :=
+{ smul_comm := λ _ _ _, ext $ λ _, smul_comm _ _ _ }
+
+instance [has_scalar R M] [has_continuous_const_smul R M]
+  [has_scalar R₁ M] [has_continuous_const_smul R₁ M]
+  [has_scalar R R₁] [is_scalar_tower R R₁ M] : is_scalar_tower R R₁ C(α, M) :=
+{ smul_assoc := λ _ _ _, ext $ λ _, smul_assoc _ _ _ }
 
-variables [has_continuous_add M] [module R M] [has_continuous_smul R M]
-variables [has_continuous_add M₂] [module R M₂] [has_continuous_smul R M₂]
+instance [has_scalar R M] [has_scalar Rᵐᵒᵖ M] [has_continuous_const_smul R M]
+  [is_central_scalar R M] : is_central_scalar R C(α, M) :=
+{ op_smul_eq_smul := λ _ _, ext $ λ _, op_smul_eq_smul _ _ }
+
+instance [monoid R] [mul_action R M] [has_continuous_const_smul R M] : mul_action R C(α, M) :=
+function.injective.mul_action _ coe_injective coe_smul
+
+instance [monoid R] [add_monoid M] [distrib_mul_action R M]
+  [has_continuous_add M] [has_continuous_const_smul R M] :
+  distrib_mul_action R C(α, M) :=
+function.injective.distrib_mul_action coe_fn_add_monoid_hom coe_injective coe_smul
+
+variables [semiring R] [add_comm_monoid M] [add_comm_monoid M₂]
+variables [has_continuous_add M] [module R M] [has_continuous_const_smul R M]
+variables [has_continuous_add M₂] [module R M₂] [has_continuous_const_smul R M₂]
 
 instance module : module R C(α, M) :=
-{ smul     := (•),
-  smul_add := λ c f g, by { ext, exact smul_add c (f x) (g x) },
-  add_smul := λ c₁ c₂ f, by { ext, exact add_smul c₁ c₂ (f x) },
-  mul_smul := λ c₁ c₂ f, by { ext, exact mul_smul c₁ c₂ (f x) },
-  one_smul := λ f, by { ext, exact one_smul R (f x) },
-  zero_smul := λ f, by { ext, exact zero_smul _ _ },
-  smul_zero := λ r, by { ext, exact smul_zero _ } }
+function.injective.module R coe_fn_add_monoid_hom coe_injective coe_smul
 
 variables (R)
 
@@ -433,7 +484,7 @@ def continuous_map.C : R →+* C(α, A) :=
 @[simp] lemma continuous_map.C_apply (r : R) (a : α) : continuous_map.C r a = algebra_map R A r :=
 rfl
 
-variables [topological_space R] [has_continuous_smul R A] [has_continuous_smul R A₂]
+variables [has_continuous_const_smul R A] [has_continuous_const_smul R A₂]
 
 instance continuous_map.algebra : algebra R C(α, A) :=
 { to_ring_hom := continuous_map.C,
@@ -461,9 +512,6 @@ def continuous_map.coe_fn_alg_hom : C(α, A) →ₐ[R] (α → A) :=
   map_add' := continuous_map.coe_add,
   map_mul' := continuous_map.coe_mul }
 
-instance: is_scalar_tower R A C(α, A) :=
-{ smul_assoc := λ _ _ _, by { ext, simp } }
-
 variables {R}
 
 /--
diff --git a/src/topology/continuous_function/basic.lean b/src/topology/continuous_function/basic.lean
index 3d681aeaacc74..4573ed6f292b2 100644
--- a/src/topology/continuous_function/basic.lean
+++ b/src/topology/continuous_function/basic.lean
@@ -58,8 +58,8 @@ lemma ext_iff : f = g ↔ ∀ x, f x = g x :=
 instance [inhabited β] : inhabited C(α, β) :=
 ⟨{ to_fun := λ _, default, }⟩
 
-lemma coe_inj ⦃f g : C(α, β)⦄ (h : (f : α → β) = g) : f = g :=
-by cases f; cases g; cases h; refl
+lemma coe_injective : @function.injective (C(α, β)) (α → β) coe_fn :=
+λ f g h, by cases f; cases g; congr'
 
 @[simp] lemma coe_mk (f : α → β) (h : continuous f) :
   ⇑(⟨f, h⟩ : continuous_map α β) = f := rfl
diff --git a/src/topology/continuous_function/bounded.lean b/src/topology/continuous_function/bounded.lean
index 8d4d3a916ac85..fb297342314cf 100644
--- a/src/topology/continuous_function/bounded.lean
+++ b/src/topology/continuous_function/bounded.lean
@@ -508,6 +508,9 @@ variables [topological_space α] [metric_space β] [has_one β]
 
 @[simp, to_additive] lemma coe_one : ((1 : α →ᵇ β) : α → β) = 1 := rfl
 
+@[simp, to_additive]
+lemma mk_of_compact_one [compact_space α] : mk_of_compact (1 : C(α, β)) = 1 := rfl
+
 @[to_additive] lemma forall_coe_one_iff_one (f : α →ᵇ β) : (∀x, f x = 1) ↔ f = 1 :=
 (@ext_iff _ _ _ _ f 1).symm
 
@@ -529,7 +532,6 @@ trivial inconvenience, but in any case there are no obvious applications of the
 version. -/
 
 variables [topological_space α] [metric_space β] [add_monoid β]
-
 variables [has_lipschitz_add β]
 variables (f g : α →ᵇ β) {x : α} {C : ℝ}
 
@@ -551,6 +553,9 @@ instance : has_add (α →ᵇ β) :=
 @[simp] lemma coe_add : ⇑(f + g) = f + g := rfl
 lemma add_apply : (f + g) x = f x + g x := rfl
 
+@[simp] lemma mk_of_compact_add [compact_space α] (f g : C(α, β)) :
+  mk_of_compact (f + g) = mk_of_compact f + mk_of_compact g := rfl
+
 lemma add_comp_continuous [topological_space γ] (h : C(γ, α)) :
   (g + f).comp_continuous h = g.comp_continuous h + f.comp_continuous h := rfl
 
@@ -758,6 +763,12 @@ lemma neg_apply : (-f) x = -f x := rfl
 @[simp] lemma coe_sub : ⇑(f - g) = f - g := rfl
 lemma sub_apply : (f - g) x = f x - g x := rfl
 
+@[simp] lemma mk_of_compact_neg [compact_space α] (f : C(α, β)) :
+  mk_of_compact (-f) = -mk_of_compact f := rfl
+
+@[simp] lemma mk_of_compact_sub [compact_space α] (f g : C(α, β)) :
+  mk_of_compact (f - g) = mk_of_compact f - mk_of_compact g := rfl
+
 instance : add_comm_group (α →ᵇ β) :=
 coe_injective.add_comm_group _ coe_zero coe_add coe_neg coe_sub
 
diff --git a/src/topology/continuous_function/compact.lean b/src/topology/continuous_function/compact.lean
index a21adb7821893..6f201f7a333a0 100644
--- a/src/topology/continuous_function/compact.lean
+++ b/src/topology/continuous_function/compact.lean
@@ -148,12 +148,8 @@ rfl
 open bounded_continuous_function
 
 instance : normed_group C(α, E) :=
-{ dist_eq := λ x y,
-  begin
-    rw [← norm_mk_of_compact, ← dist_mk_of_compact, dist_eq_norm],
-    congr' 1,
-    exact ((add_equiv_bounded_of_compact α E).map_sub _ _).symm
-  end, }
+{ dist_eq := λ x y, by
+    rw [← norm_mk_of_compact, ← dist_mk_of_compact, dist_eq_norm, mk_of_compact_sub] }
 
 section
 variables (f : C(α, E))
diff --git a/src/topology/tietze_extension.lean b/src/topology/tietze_extension.lean
index 4d07a03ba980b..823585dab5c05 100644
--- a/src/topology/tietze_extension.lean
+++ b/src/topology/tietze_extension.lean
@@ -378,7 +378,7 @@ lemma exists_restrict_eq_forall_mem_of_closed {s : set Y} (f : C(s, ℝ)) {t : s
   ∃ g : C(Y, ℝ), (∀ y, g y ∈ t) ∧ g.restrict s = f :=
 let ⟨g, hgt, hgf⟩ := exists_extension_forall_mem_of_closed_embedding f ht hne
   (closed_embedding_subtype_coe hs)
-in ⟨g, hgt, coe_inj hgf⟩
+in ⟨g, hgt, coe_injective hgf⟩
 
 /-- **Tietze extension theorem** for real-valued continuous maps, a version for a closed set. Let
 `s` be a closed set in a normal topological space `Y`. Let `f` be a continuous real-valued function