chore: shortcut instances for IntermediateField over an IntermediateF…

…ield (#9291)

Removes [manual letI/haveI](https://github.com/leanprover-community/mathlib4/blob/fe76ea7c2bb0c725ad161755ac158171aa9c545a/Mathlib/FieldTheory/SeparableDegree.lean#L568-L571) that appear in four proofs of #9041



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Mathlib/FieldTheory/IntermediateField.lean

@@ -401,6 +401,14 @@ instance isScalarTower_mid' : IsScalarTower K S L :=
   S.isScalarTower_mid
 #align intermediate_field.is_scalar_tower_mid' IntermediateField.isScalarTower_mid'
 
+section shortcut_instances
+variable {E} [Field E] [Algebra L E] (T : IntermediateField S E) {S}
+instance : Algebra S T := T.algebra
+instance : Module S T := Algebra.toModule
+instance : SMul S T := Algebra.toSMul
+instance [Algebra K E] [IsScalarTower K L E] : IsScalarTower K S T := T.isScalarTower
+end shortcut_instances
+
 /-- Given `f : L →ₐ[K] L'`, `S.comap f` is the intermediate field between `K` and `L`
   such that `f x ∈ S ↔ x ∈ S.comap f`. -/
 def comap (f : L →ₐ[K] L') (S : IntermediateField K L') : IntermediateField K L where