refactor(Topology/Algebra/Module/LinearMap): adjust statement of coe_mul and coe_pow (leanprover-community#35269)

In `Topology/Algebra/Module/LinearMap`, it seems to be the pattern to have `coe_zero`/`coe_id`/`coe_add`/`coe_neg`/`coe_sub` for the coercions from `ContinuousLinearMap` to `LinearMap` and primed versions `coe_zero'`/`coe_id'`/`coe_add'`/`coe_neg'`/`coe_sub'` for the coercions from `ContinuousLinearMap` to `Function`.

This PR adjusts the statements of `coe_mul` and `coe_pow` to fit this pattern, as well as adding `coe_one`.

Co-authored-by: tb65536 <thomas.l.browning@gmail.com>

Author: tb65536

Mathlib/Analysis/CStarAlgebra/Multiplier.lean

@@ -404,21 +404,16 @@ theorem star_snd (a : 𝓜(𝕜, A)) (b : A) : (star a).snd b = star (a.fst (sta
 
 instance instStarAddMonoid : StarAddMonoid 𝓜(𝕜, A) :=
   { DoubleCentralizer.instStar with
-    star_involutive := fun x => by ext <;> simp only [star_fst, star_snd, star_star]
-    star_add := fun x y => by
-      ext <;>
-        simp only [star_fst, star_snd, add_fst, add_snd, ContinuousLinearMap.add_apply, star_add] }
+    star_involutive _ := by ext <;> simp
+    star_add _ _ := by ext <;> simp }
 
 instance instStarRing : StarRing 𝓜(𝕜, A) :=
   { DoubleCentralizer.instStarAddMonoid with
-    star_mul := fun a b => by
-      ext <;>
-        simp only [star_fst, star_snd, mul_fst, mul_snd, star_star, ContinuousLinearMap.coe_mul,
-          Function.comp_apply] }
+    star_mul _ _ := by ext <;> simp }
 
 instance instStarModule : StarModule 𝕜 𝓜(𝕜, A) :=
   { DoubleCentralizer.instStarAddMonoid (𝕜 := 𝕜) (A := A) with
-    star_smul := fun k a => by ext <;> exact star_smul _ _ }
+    star_smul _ _ := by ext <;> exact star_smul _ _ }
 
 end Star
 

Mathlib/Topology/Algebra/Module/LinearMap.lean

@@ -351,6 +351,10 @@ theorem coe_id : (ContinuousLinearMap.id R₁ M₁ : M₁ →ₗ[R₁] M₁) = L
 theorem coe_id' : ⇑(ContinuousLinearMap.id R₁ M₁) = id :=
   rfl
 
+@[simp, norm_cast]
+theorem coe_one : ((1 : M₁ →L[R₁] M₁) : M₁ →ₗ[R₁] M₁) = 1 :=
+  rfl
+
 @[simp, norm_cast]
 theorem toContinuousAddMonoidHom_id :
     (ContinuousLinearMap.id R₁ M₁ : ContinuousAddMonoidHom M₁ M₁) = .id _ := rfl
@@ -531,8 +535,12 @@ instance instMul : Mul (M₁ →L[R₁] M₁) :=
 theorem mul_def (f g : M₁ →L[R₁] M₁) : f * g = f.comp g :=
   rfl
 
-@[simp]
-theorem coe_mul (f g : M₁ →L[R₁] M₁) : ⇑(f * g) = f ∘ g :=
+@[simp, norm_cast]
+theorem coe_mul (f g : M₁ →L[R₁] M₁) : (↑(f * g) : M₁ →ₗ[R₁] M₁) = f * g :=
+  rfl
+
+@[simp, norm_cast]
+theorem coe_mul' (f g : M₁ →L[R₁] M₁) : ⇑(f * g) = f ∘ g :=
   rfl
 
 theorem mul_apply (f g : M₁ →L[R₁] M₁) (x : M₁) : (f * g) x = f (g x) :=
@@ -545,9 +553,14 @@ instance monoidWithZero : MonoidWithZero (M₁ →L[R₁] M₁) where
   one_mul _ := ext fun _ => rfl
   mul_assoc _ _ _ := ext fun _ => rfl
 
-theorem coe_pow (f : M₁ →L[R₁] M₁) (n : ℕ) : ⇑(f ^ n) = f^[n] :=
+@[simp, norm_cast]
+theorem coe_pow' (f : M₁ →L[R₁] M₁) (n : ℕ) : ⇑(f ^ n) = f^[n] :=
   hom_coe_pow _ rfl (fun _ _ ↦ rfl) _ _
 
+@[simp, norm_cast]
+theorem coe_pow (f : M₁ →L[R₁] M₁) (n : ℕ) : (↑(f ^ n) : M₁ →ₗ[R₁] M₁) = f ^ n :=
+  DFunLike.ext' <| (coe_pow' f n).trans <| .symm <| hom_coe_pow _ rfl (fun _ _ ↦ rfl) _ _
+
 instance instNatCast [ContinuousAdd M₁] : NatCast (M₁ →L[R₁] M₁) where
   natCast n := n • (1 : M₁ →L[R₁] M₁)