feat(NumberTheory/ModularForms): add @[simp] coe_cast + cast_apply

Function-level and pointwise simp lemmas for `heq ▸ f` cast.

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

Author: CBirkbeck

Mathlib/NumberTheory/ModularForms/Basic.lean

@@ -565,8 +565,18 @@ 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