chore(field_theory/intermediate_field): fix timeout (#14725)

+ Remove `@[simps]` from `intermediate_field_map` to reduce `decl post-processing of intermediate_field_map` from 18.3s to 46.4ms (on my machine).

+ Manually provide the two `simp` lemmas previously auto-generated by `@[simps]`. Mathlib compiles even without the two simp lemmas (see commit 1f5a7f1), but I am inclined to keep them in case some other branches/projects are using them.

[Zulip reports](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/deterministic.20timeout/near/285792556) about `intermediate_field_map` causing timeout in two separate branches

Author: alreadydone

src/field_theory/intermediate_field.lean

@@ -280,10 +280,18 @@ set_like.coe_injective $ set.image_image _ _ _
 /-- Given an equivalence `e : L ≃ₐ[K] L'` of `K`-field extensions and an intermediate
 field `E` of `L/K`, `intermediate_field_equiv_map e E` is the induced equivalence
 between `E` and `E.map e` -/
-@[simps] def intermediate_field_map (e : L ≃ₐ[K] L') (E : intermediate_field K L) :
+def intermediate_field_map (e : L ≃ₐ[K] L') (E : intermediate_field K L) :
   E ≃ₐ[K] (E.map e.to_alg_hom) :=
 e.subalgebra_map E.to_subalgebra
 
+/- We manually add these two simp lemmas because `@[simps]` before `intermediate_field_map`
+  led to a timeout. -/
+@[simp] lemma intermediate_field_map_apply_coe (e : L ≃ₐ[K] L') (E : intermediate_field K L)
+  (a : E) : ↑(intermediate_field_map e E a) = e a := rfl
+
+@[simp] lemma intermediate_field_map_symm_apply_coe (e : L ≃ₐ[K] L') (E : intermediate_field K L)
+  (a : E.map e.to_alg_hom) : ↑((intermediate_field_map e E).symm a) = e.symm a := rfl
+
 /-- The embedding from an intermediate field of `L / K` to `L`. -/
 def val : S →ₐ[K] L :=
 S.to_subalgebra.val