refactor: use smul_algebraMap to simply proof of FixedPoints.intermed…

…iateField.algebraMap_mem' (#11025)

Uses `smul_algebraMap` to simplify the proof of `FixedPoints.intermediateField.algebraMap_mem'`.

Amusingly, the current tactic-mode proof is very nearly identical to the body of `smul_algebraMap`:
https://github.com/leanprover-community/mathlib4/blob/bb9eaa6b041bc19ca8615a24fa48e463c672c150/Mathlib/Algebra/Algebra/Basic.lean#L403-L405

After making this simplificiation, I observe the time reported by `trace.profiler` to drop from 0.13 to 0.12 seconds.

Mathlib/FieldTheory/Galois.lean

@@ -186,7 +186,7 @@ def FixedPoints.intermediateField (M : Type*) [Monoid M] [MulSemiringAction M E]
     [SMulCommClass M F E] : IntermediateField F E :=
   { FixedPoints.subfield M E with
     carrier := MulAction.fixedPoints M E
-    algebraMap_mem' := fun a g => by rw [Algebra.algebraMap_eq_smul_one, smul_comm, smul_one] }
+    algebraMap_mem' := fun a g => smul_algebraMap g a }
 #align fixed_points.intermediate_field FixedPoints.intermediateField
 
 namespace IntermediateField