chore(ContDiffSupportedIn): use simps to auto-generate basic API (#30659)

Follow-up to #30198.

Author: grunweg

Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean

@@ -137,9 +137,9 @@ theorem toFun_eq_coe {f : 𝓓^{n}_{K}(E, F)} : f.toFun = (f : E → F) :=
   rfl
 
 /-- See note [custom simps projection]. -/
-def Simps.apply (f : 𝓓^{n}_{K}(E, F)) : E → F := f
+def Simps.coe (f : 𝓓^{n}_{K}(E, F)) : E → F := f
 
-initialize_simps_projections ContDiffMapSupportedIn (toFun → apply)
+initialize_simps_projections ContDiffMapSupportedIn (toFun → coe, as_prefix coe)
 
 @[ext]
 theorem ext {f g : 𝓓^{n}_{K}(E, F)} (h : ∀ a, f a = g a) : f = g :=
@@ -165,53 +165,35 @@ theorem toBoundedContinuousFunction_apply (f : 𝓓^{n}_{K}(E, F)) (x : E) :
 
 section AddCommGroup
 
+@[simps -fullyApplied]
 instance : Zero 𝓓^{n}_{K}(E, F) where
   zero := .mk 0 contDiff_zero_fun fun _ _ ↦ rfl
 
-@[simp]
-lemma coe_zero : (0 : 𝓓^{n}_{K}(E, F)) = (0 : E → F) :=
-  rfl
-
+@[simps -fullyApplied]
 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 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
-
+@[simps -fullyApplied]
 instance : Neg 𝓓^{n}_{K}(E, F) where
   neg f := .mk (-f) (f.contDiff.neg) <| by
     rw [← neg_zero]
     exact f.zero_on_compl.comp_left
 
-@[simp]
-lemma coe_neg (f : 𝓓^{n}_{K}(E, F)) : (-f : 𝓓^{n}_{K}(E, F)) = (-f : E → F) :=
-  rfl
-
+@[simps -fullyApplied]
 instance instSub : Sub 𝓓^{n}_{K}(E, F) where
   sub f g := .mk (f - g) (f.contDiff.sub g.contDiff) <| by
     rw [← sub_zero 0]
     exact f.zero_on_compl.comp_left₂ g.zero_on_compl
 
-@[simp]
-lemma coe_sub (f g : 𝓓^{n}_{K}(E, F)) : (f - g : 𝓓^{n}_{K}(E, F)) = (f : E → F) - g :=
-  rfl
-
+@[simps -fullyApplied]
 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
     rw [← smul_zero c]
     exact f.zero_on_compl.comp_left
 
-@[simp]
-lemma coe_smul {R} [Semiring R] [Module R F] [SMulCommClass ℝ R F] [ContinuousConstSMul R F]
-    (c : R) (f : 𝓓^{n}_{K}(E, F)) : (c • f : 𝓓^{n}_{K}(E, F)) = c • (f : E → F) :=
-  rfl
-
 instance : AddCommGroup 𝓓^{n}_{K}(E, F) :=
   DFunLike.coe_injective.addCommGroup _ rfl (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ _ ↦ rfl)
     (fun _ _ ↦ rfl) fun _ _ ↦ rfl