chore(topology/continuous_function/bounded): golf algebra instances (#…

…12082)

Using the `function.injective.*` lemmas saves a lot of proofs.

This also adds a few missing lemmas about `one` that were already present for `zero`.

src/topology/continuous_function/bounded.lean

@@ -500,6 +500,22 @@ end
 
 end arzela_ascoli
 
+section has_one
+
+variables [topological_space α] [metric_space β] [has_one β]
+
+@[to_additive] instance : has_one (α →ᵇ β) := ⟨const α 1⟩
+
+@[simp, to_additive] lemma coe_one : ((1 : α →ᵇ β) : α → β) = 1 := rfl
+
+@[to_additive] lemma forall_coe_one_iff_one (f : α →ᵇ β) : (∀x, f x = 1) ↔ f = 1 :=
+(@ext_iff _ _ _ _ f 1).symm
+
+@[simp, to_additive] lemma one_comp_continuous [topological_space γ] (f : C(γ, α)) :
+  (1 : α →ᵇ β).comp_continuous f = 1 := rfl
+
+end has_one
+
 section has_lipschitz_add
 /- In this section, if `β` is an `add_monoid` whose addition operation is Lipschitz, then we show
 that the space of bounded continuous functions from `α` to `β` inherits a topological `add_monoid`
@@ -514,15 +530,6 @@ version. -/
 
 variables [topological_space α] [metric_space β] [add_monoid β]
 
-instance : has_zero (α →ᵇ β) := ⟨const α 0⟩
-
-@[simp] lemma coe_zero : ((0 : α →ᵇ β) : α → β) = 0 := rfl
-
-lemma forall_coe_zero_iff_zero (f : α →ᵇ β) : (∀x, f x = 0) ↔ f = 0 := (@ext_iff _ _ _ _ f 0).symm
-
-@[simp] lemma zero_comp_continuous [topological_space γ] (f : C(γ, α)) :
-  (0 : α →ᵇ β).comp_continuous f = 0 := rfl
-
 variables [has_lipschitz_add β]
 variables (f g : α →ᵇ β) {x : α} {C : ℝ}
 
@@ -548,11 +555,7 @@ lemma add_comp_continuous [topological_space γ] (h : C(γ, α)) :
   (g + f).comp_continuous h = g.comp_continuous h + f.comp_continuous h := rfl
 
 instance : add_monoid (α →ᵇ β) :=
-{ add_assoc      := assume f g h, by ext; simp [add_assoc],
-  zero_add       := assume f, by ext; simp,
-  add_zero       := assume f, by ext; simp,
-  .. bounded_continuous_function.has_add,
-  .. bounded_continuous_function.has_zero }
+coe_injective.add_monoid _ coe_zero coe_add
 
 instance : has_lipschitz_add (α →ᵇ β) :=
 { lipschitz_add := ⟨has_lipschitz_add.C β, begin
@@ -752,17 +755,12 @@ instance : has_sub (α →ᵇ β) :=
 @[simp] lemma coe_neg : ⇑(-f) = -f := rfl
 lemma neg_apply : (-f) x = -f x := rfl
 
-instance : add_comm_group (α →ᵇ β) :=
-{ add_left_neg   := assume f, by ext; simp,
-  add_comm       := assume f g, by ext; simp [add_comm],
-  sub_eq_add_neg := assume f g, by { ext, apply sub_eq_add_neg },
-  ..bounded_continuous_function.add_monoid,
-  ..bounded_continuous_function.has_neg,
-  ..bounded_continuous_function.has_sub }
-
 @[simp] lemma coe_sub : ⇑(f - g) = f - g := rfl
 lemma sub_apply : (f - g) x = f x - g x := rfl
 
+instance : add_comm_group (α →ᵇ β) :=
+coe_injective.add_comm_group _ coe_zero coe_add coe_neg coe_sub
+
 instance : normed_group (α →ᵇ β) :=
 { dist_eq := λ f g, by simp only [norm_eq, dist_eq, dist_eq_norm, sub_apply] }
 
@@ -914,21 +912,17 @@ pointwise operations and checking that they are compatible with the uniform dist
 
 variables [topological_space α] {R : Type*} [normed_ring R]
 
-instance : ring (α →ᵇ R) :=
-{ one := const α 1,
-  mul := λ f g, of_normed_group (f * g) (f.continuous.mul g.continuous) (∥f∥ * ∥g∥) $ λ x,
+instance : has_mul (α →ᵇ R) :=
+{ mul := λ f g, of_normed_group (f * g) (f.continuous.mul g.continuous) (∥f∥ * ∥g∥) $ λ x,
     le_trans (normed_ring.norm_mul (f x) (g x)) $
-      mul_le_mul (f.norm_coe_le_norm x) (g.norm_coe_le_norm x) (norm_nonneg _) (norm_nonneg _),
-  one_mul := λ f, ext $ λ x, one_mul (f x),
-  mul_one := λ f, ext $ λ x, mul_one (f x),
-  mul_assoc := λ f₁ f₂ f₃, ext $ λ x, mul_assoc _ _ _,
-  left_distrib := λ f₁ f₂ f₃, ext $ λ x, left_distrib _ _ _,
-  right_distrib := λ f₁ f₂ f₃, ext $ λ x, right_distrib _ _ _,
-  .. bounded_continuous_function.add_comm_group }
+      mul_le_mul (f.norm_coe_le_norm x) (g.norm_coe_le_norm x) (norm_nonneg _) (norm_nonneg _) }
 
 @[simp] lemma coe_mul (f g : α →ᵇ R) : ⇑(f * g) = f * g := rfl
 lemma mul_apply (f g : α →ᵇ R) (x : α) : (f * g) x = f x * g x := rfl
 
+instance : ring (α →ᵇ R) :=
+coe_injective.ring _ coe_zero coe_one coe_add coe_mul coe_neg coe_sub
+
 instance : normed_ring (α →ᵇ R) :=
 { norm_mul := λ f g, norm_of_normed_group_le _ (mul_nonneg (norm_nonneg _) (norm_nonneg _)) _,
   .. bounded_continuous_function.normed_group }