refactor(NumberTheory): golf Mathlib/NumberTheory/ModularForms/CongruenceSubgroups (#39373)

- simplifies `Gamma_mem` to a single `simp` proof via `Gamma_mem'` and `SpecialLinearGroup.ext_iff`
- shortens `ModularGroup_T_pow_mem_Gamma` and the `Gamma0` closure proofs with direct `simp`/`simpa` arguments

Extracted from #38144

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

Author: yuanyi-350

Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean

@@ -49,15 +49,7 @@ theorem Gamma_mem' {N} {γ : SL(2, ℤ)} : γ ∈ Gamma N ↔ SLMOD(N) γ = 1 :=
 @[simp]
 theorem Gamma_mem {N} {γ : SL(2, ℤ)} : γ ∈ Gamma N ↔ (γ 0 0 : ZMod N) = 1 ∧
     (γ 0 1 : ZMod N) = 0 ∧ (γ 1 0 : ZMod N) = 0 ∧ (γ 1 1 : ZMod N) = 1 := by
-  rw [Gamma_mem']
-  constructor
-  · intro h
-    simp [← SL_reduction_mod_hom_val N γ, h]
-  · intro h
-    ext i j
-    rw [SL_reduction_mod_hom_val N γ]
-    fin_cases i <;> fin_cases j <;> simp only
-    exacts [h.1, h.2.1, h.2.2.1, h.2.2.2]
+  simp [Gamma_mem', SpecialLinearGroup.ext_iff, and_assoc]
 
 theorem Gamma_normal : Subgroup.Normal (Gamma N) :=
   SLMOD(N).normal_ker
@@ -77,11 +69,7 @@ theorem Gamma_zero_bot : Gamma 0 = ⊥ := rfl
 
 lemma ModularGroup_T_pow_mem_Gamma (N M : ℤ) (hNM : N ∣ M) :
     (ModularGroup.T ^ M) ∈ Gamma (Int.natAbs N) := by
-  simp only [Gamma_mem, Fin.isValue, ModularGroup.coe_T_zpow, of_apply, cons_val', cons_val_zero,
-    empty_val', cons_val_fin_one, Int.cast_one, cons_val_one,
-    Int.cast_zero, and_self, and_true, true_and]
-  refine Iff.mpr (ZMod.intCast_zmod_eq_zero_iff_dvd M (Int.natAbs N)) ?_
-  simp only [Int.natCast_natAbs, abs_dvd, hNM]
+  simp [ModularGroup.coe_T_zpow, hNM, ZMod.intCast_zmod_eq_zero_iff_dvd]
 
 instance instFiniteIndexGamma [NeZero N] : (Gamma N).FiniteIndex := Subgroup.finiteIndex_ker _
 
@@ -90,20 +78,12 @@ modulo `N`. -/
 def Gamma0 : Subgroup SL(2, ℤ) where
   carrier := { g | (g 1 0 : ZMod N) = 0 }
   one_mem' := by simp
-  mul_mem' := by
-    intro a b ha hb
-    simp only [Set.mem_setOf_eq]
+  mul_mem' {a} {b} ha hb := by
     have h := (Matrix.two_mul_expl a.1 b.1).2.2.1
     simp only [coe_mul, Set.mem_setOf_eq] at *
-    rw [h]
-    simp [ha, hb]
-  inv_mem' := by
-    intro a ha
-    simp only [Set.mem_setOf_eq]
-    rw [SL2_inv_expl a]
-    simp only [cons_val_zero, cons_val_one,
-      Int.cast_neg, neg_eq_zero, Set.mem_setOf_eq] at *
-    exact ha
+    simp [h, ha, hb]
+  inv_mem' {a} ha := by
+    simpa [SL2_inv_expl a] using ha
 
 @[simp]
 theorem Gamma0_mem {N} {A : SL(2, ℤ)} : A ∈ Gamma0 N ↔ (A 1 0 : ZMod N) = 0 :=