chore(Analysis/Distribution/ContDiffMapSupportedIn): remove _apply le… (#31094)

…mmas about instances

#30198 added both a coe_foo and a foo_apply lemma for foo in {zero,add,sub,neg,smul}: remove the apply lemmas again.
- there was no good reason for having both; when in doubt, use coe lemmas
- for simp, the coe lemmas are equally strong (and having both is very unusual at best),
- when rewriting, one can add Pi.zero_apply and friends.

Author: grunweg

Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean

@@ -172,25 +172,17 @@ instance : Zero 𝓓^{n}_{K}(E, F) where
 lemma coe_zero : (0 : 𝓓^{n}_{K}(E, F)) = (0 : E → F) :=
   rfl
 
-@[simp]
-lemma zero_apply (x : E) : (0 : 𝓓^{n}_{K}(E, F)) x = 0 :=
-  rfl
-
 instance : Add 𝓓^{n}_{K}(E, F) where
   add f g := .mk (f + g) (f.contDiff.add g.contDiff) <| by
     rw [← add_zero 0]
     exact f.zero_on_compl.comp_left₂ g.zero_on_compl
 
--- TODO:  can this and the next lemma be auto-generated, e.g. using `simps`?
+-- TODO: can this lemma be auto-generated, e.g. using `simps`?
 -- Investigate the same question for `zero` above and `sub` , `neg` and `smul` below.
 @[simp]
 lemma coe_add (f g : 𝓓^{n}_{K}(E, F)) : (f + g : 𝓓^{n}_{K}(E, F)) = (f : E → F) + g :=
   rfl
 
-@[simp]
-lemma add_apply (f g : 𝓓^{n}_{K}(E, F)) (x : E) : (f + g) x = f x + g x :=
-  rfl
-
 instance : Neg 𝓓^{n}_{K}(E, F) where
   neg f := .mk (-f) (f.contDiff.neg) <| by
     rw [← neg_zero]
@@ -200,10 +192,6 @@ instance : Neg 𝓓^{n}_{K}(E, F) where
 lemma coe_neg (f : 𝓓^{n}_{K}(E, F)) : (-f : 𝓓^{n}_{K}(E, F)) = (-f : E → F) :=
   rfl
 
-@[simp]
-theorem neg_apply {f : 𝓓^{n}_{K}(E, F)} {x : E} : (-f) x = - f x :=
-  rfl
-
 instance instSub : Sub 𝓓^{n}_{K}(E, F) where
   sub f g := .mk (f - g) (f.contDiff.sub g.contDiff) <| by
     rw [← sub_zero 0]
@@ -213,10 +201,6 @@ instance instSub : Sub 𝓓^{n}_{K}(E, F) where
 lemma coe_sub (f g : 𝓓^{n}_{K}(E, F)) : (f - g : 𝓓^{n}_{K}(E, F)) = (f : E → F) - g :=
   rfl
 
-@[simp]
-theorem sub_apply {f g : 𝓓^{n}_{K}(E, F)} {x : E} : (f - g) x = f x - g x :=
-  rfl
-
 instance instSMul {R} [Semiring R] [Module R F] [SMulCommClass ℝ R F] [ContinuousConstSMul R F] :
    SMul R 𝓓^{n}_{K}(E, F) where
   smul c f := .mk (c • (f : E → F)) (f.contDiff.const_smul c) <| by
@@ -228,11 +212,6 @@ lemma coe_smul {R} [Semiring R] [Module R F] [SMulCommClass ℝ R F] [Continuous
     (c : R) (f : 𝓓^{n}_{K}(E, F)) : (c • f : 𝓓^{n}_{K}(E, F)) = c • (f : E → F) :=
   rfl
 
-@[simp]
-lemma smul_apply {R} [Semiring R] [Module R F] [SMulCommClass ℝ R F] [ContinuousConstSMul R F]
-    (c : R) (f : 𝓓^{n}_{K}(E, F)) (x : E) : (c • f) x = c • (f x) :=
-  rfl
-
 instance : AddCommGroup 𝓓^{n}_{K}(E, F) :=
   DFunLike.coe_injective.addCommGroup _ rfl (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ _ ↦ rfl)
     (fun _ _ ↦ rfl) fun _ _ ↦ rfl