revert speculative coe_cast/cast_apply @[simp] additions

These were added speculatively to clean up a proof downstream but the
defeq unification trick the original uses can't be cleanly abstracted
by these lemmas. Remove until there's a concrete use case.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: CBirkbeck

Mathlib/NumberTheory/ModularForms/Basic.lean

@@ -565,18 +565,8 @@ def mcast {a b : ℤ} {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} (h : a = b) (f : Modu
   holo' := f.holo'
   bdd_at_cusps' hc := h ▸ f.bdd_at_cusps' (hΓ ▸ hc)
 
-/-- Transporting a `ModularForm` along an equality of weights does not change its underlying
-function. -/
-@[simp]
-theorem coe_cast {Γ : Subgroup (GL (Fin 2) ℝ)} {k₁ k₂ : ℤ}
-    (heq : k₁ = k₂) (f : ModularForm Γ k₁) :
-    ((heq ▸ f : ModularForm Γ k₂) : ℍ → ℂ) = (f : ℍ → ℂ) := by
-  subst heq
-  rfl
-
 /-- Transporting a `ModularForm` along an equality of weights does not change its pointwise
 values. -/
-@[simp]
 theorem cast_apply {Γ : Subgroup (GL (Fin 2) ℝ)} {k₁ k₂ : ℤ}
     (heq : k₁ = k₂) (f : ModularForm Γ k₁) (z : ℍ) :
     (heq ▸ f : ModularForm Γ k₂) z = f z := by