mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case e'_3
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g ↦ (↑g).map Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix : Tendsto (fun m ↦ m.map Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₁ : Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
g : SL(2, ℤ)
hcd : IsCoprime (↑g 1 0) (↑g 1 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t ↦ of ![![t, -↑1], Int.cast ∘ ↑g 1]
hmB : Continuous mB
hf₂ : IsClosedEmbedding ⇑(lcRow0Extend hcd)
i j : Fin 2
⊢ (mB ∘ fun g_1 ↦ (lcRow0 (↑g 1)) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g_1)) ⟨g, ⋯⟩ i j =
    (⇑(lcRow0Extend hcd) ∘ f₁ ∘ fun a ↦ ↑a) ⟨g, ⋯⟩ i j

Tactic:
fin_cases i

Goal state after:
case e'_3.«0»
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g ↦ (↑g).map Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix : Tendsto (fun m ↦ m.map Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₁ : Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
g : SL(2, ℤ)
hcd : IsCoprime (↑g 1 0) (↑g 1 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t ↦ of ![![t, -↑1], Int.cast ∘ ↑g 1]
hmB : Continuous mB
hf₂ : IsClosedEmbedding ⇑(lcRow0Extend hcd)
j : Fin 2
⊢ (mB ∘ fun g_1 ↦ (lcRow0 (↑g 1)) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g_1)) ⟨g, ⋯⟩ ((fun i ↦ i) ⟨0, ⋯⟩) j =
    (⇑(lcRow0Extend hcd) ∘ f₁ ∘ fun a ↦ ↑a) ⟨g, ⋯⟩ ((fun i ↦ i) ⟨0, ⋯⟩) j

case e'_3.«1»
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g ↦ (↑g).map Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix : Tendsto (fun m ↦ m.map Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₁ : Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
g : SL(2, ℤ)
hcd : IsCoprime (↑g 1 0) (↑g 1 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t ↦ of ![![t, -↑1], Int.cast ∘ ↑g 1]
hmB : Continuous mB
hf₂ : IsClosedEmbedding ⇑(lcRow0Extend hcd)
j : Fin 2
⊢ (mB ∘ fun g_1 ↦ (lcRow0 (↑g 1)) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g_1)) ⟨g, ⋯⟩ ((fun i ↦ i) ⟨1, ⋯⟩) j =
    (⇑(lcRow0Extend hcd) ∘ f₁ ∘ fun a ↦ ↑a) ⟨g, ⋯⟩ ((fun i ↦ i) ⟨1, ⋯⟩) j
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
inst✝ : CuspFormClass F Γ k
g : GL (Fin 2) ℝ
c : OnePoint ℝ
hc : IsCusp c (toConjAct g⁻¹ • Γ)
γ : GL (Fin 2) ℝ
hγ : γ • ∞ = c
⊢ IsZeroAtImInfty ((ModularForm.translate f g).toFun ∣[k] γ)

Tactic:
rw [SlashInvariantForm.toFun_eq_coe, ModularForm.toSlashInvariantForm_coe,
      ModularForm.coe_translate, ← SlashAction.slash_mul, ← isZeroAt_infty_iff,
      ← OnePoint.IsZeroAt.smul_iff]

Goal state after:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
inst✝ : CuspFormClass F Γ k
g : GL (Fin 2) ℝ
c : OnePoint ℝ
hc : IsCusp c (toConjAct g⁻¹ • Γ)
γ : GL (Fin 2) ℝ
hγ : γ • ∞ = c
⊢ ((g * γ) • ∞).IsZeroAt (⇑f) k
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
q : ℂ
hq : ‖q‖ < 1
hq1 : q ≠ 0
⊢ HasSum (fun m ↦ c m • q ^ m) (cuspFunction h f q)

Tactic:
have h1 := Periodic.im_invQParam_pos_of_norm_lt_one hh hq hq1
  let τ : ℍ := ⟨Periodic.invQParam h q, h1⟩
  have h2 := (Periodic.cuspFunction_eq_of_nonzero h (f ∘ ofComplex) hq1)
  have : cuspFunction h f q = f τ := by simpa [UpperHalfPlane.ofComplex_apply_of_im_pos h1]
    using! h2
  grind [hf τ, Periodic.qParam_right_inv]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
hf_infinity✝ : f =O[atImInfty] fun z ↦ z.im ^ t
D : ℝ
hD : D > 0
hf_infinity : ∀ᶠ (x : ℍ) in atImInfty, ‖f x‖ ≤ D * ‖x.im ^ t‖
⊢ ∃ F, ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t

Tactic:
atImInfty,

Goal state after:
E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
hf_infinity✝ : f =O[atImInfty] fun z ↦ z.im ^ t
D : ℝ
hD : D > 0
hf_infinity : ∀ᶠ (x : ℍ) in comap im atTop, ‖f x‖ ≤ D * ‖x.im ^ t‖
⊢ ∃ F, ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case h
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
i j : Fin 2
⊢ ↑g i j = ↑(T ^ ↑g 0 1) i j

Tactic:
fin_cases i

Goal state after:
case h.«0»
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
j : Fin 2
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) j = ↑(T ^ ↑g 0 1) ((fun i ↦ i) ⟨0, ⋯⟩) j

case h.«1»
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
j : Fin 2
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) j = ↑(T ^ ↑g 0 1) ((fun i ↦ i) ⟨1, ⋯⟩) j
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: r : ℕ
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
i : Fin 2
⊢ ↑r ∣ v i

Tactic:
fin_cases i

Goal state after:
case «0»
r : ℕ
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
⊢ ↑r ∣ v ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
r : ℕ
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
⊢ ↑r ∣ v ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case h
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
i j : Fin 2
⊢ ↑g i j = ↑(-T ^ (-↑g 0 1)) i j

Tactic:
fin_cases i

Goal state after:
case h.«0»
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
j : Fin 2
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) j = ↑(-T ^ (-↑g 0 1)) ((fun i ↦ i) ⟨0, ⋯⟩) j

case h.«1»
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
j : Fin 2
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) j = ↑(-T ^ (-↑g 0 1)) ((fun i ↦ i) ⟨1, ⋯⟩) j
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: case pos
r : ℕ
v : Fin 2 → ℤ
hv✝ : v ∈ gammaSet 1 0 0
hr : True
hv : v 0 = 0 ∧ v 1 = 0
i : Fin 2
⊢ v i = 0 i

Tactic:
fin_cases i

Goal state after:
case pos.«_@».Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs.1971615608._hygCtx._hyg.42.«0»
r : ℕ
v : Fin 2 → ℤ
hv✝ : v ∈ gammaSet 1 0 0
hr : True
hv : v 0 = 0 ∧ v 1 = 0
⊢ v ((fun i ↦ i) ⟨0, ⋯⟩) = 0 ((fun i ↦ i) ⟨0, ⋯⟩)

case pos.«_@».Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs.1971615608._hygCtx._hyg.42.«1»
r : ℕ
v : Fin 2 → ℤ
hv✝ : v ∈ gammaSet 1 0 0
hr : True
hv : v 0 = 0 ∧ v 1 = 0
⊢ v ((fun i ↦ i) ⟨1, ⋯⟩) = 0 ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
⊢ ∃ n, ∀ (z : ℍ), g • z = T ^ n • z

Tactic:
· use -(g 0 1)
    suffices g = -T ^ (-(g 0 1)) by intro z; conv_lhs => rw [this, SL_neg_smul]
    ext i j; fin_cases i <;> fin_cases j <;>
      simp [ha, hc, hd, coe_T_zpow, show (1 : Fin (0 + 2)) = (1 : Fin 2) from rfl]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: r : ℕ
inst✝ : NeZero r
v : Fin 2 → ℤ
hab : finGcdMap v = r
A : SL(2, ℤ)
i : Fin 2
⊢ ↑r ∣ v i

Tactic:
fin_cases i

Goal state after:
case «0»
r : ℕ
inst✝ : NeZero r
v : Fin 2 → ℤ
hab : finGcdMap v = r
A : SL(2, ℤ)
⊢ ↑r ∣ v ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
r : ℕ
inst✝ : NeZero r
v : Fin 2 → ℤ
hab : finGcdMap v = r
A : SL(2, ℤ)
⊢ ↑r ∣ v ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : ∀ (g : SL(2, ℤ)), (fun τ ↦ f (g • τ)) =O[atImInfty] fun z ↦ z.im ^ t
Γ : Subgroup SL(2, ℤ)
inst✝ : Γ.FiniteIndex
hf_inv : ∀ g ∈ Γ, ∀ (τ : ℍ), f (g • τ) = f τ
τ : ℍ
g h : SL(2, ℤ)
hgh : g ≈ h
⊢ f (g⁻¹ • τ) = f (h⁻¹ • τ)

Tactic:
obtain ⟨j, hj, hj'⟩ : ∃ j ∈ Γ, h = g * j := by
      rw [← Quotient.eq_iff_equiv, Quotient.eq, QuotientGroup.leftRel_apply] at hgh
      exact ⟨g⁻¹ * h, hgh, (mul_inv_cancel_left g h).symm⟩
    simp [-sl_moeb, hj', mul_smul, hf_inv j⁻¹ (inv_mem hj)]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty

Goal state before:
pp: N : ℕ
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
z : ℍ
⊢ ‖eisensteinSeries a k z‖ ≤ ∑' (x : Fin 2 → ℤ), ‖eisSummand k x z‖

Tactic:
simp_rw [eisensteinSeries]
  apply le_trans (norm_tsum_le_tsum_norm ((summable_norm_eisSummand hk z).subtype _))
    (Summable.tsum_subtype_le (fun (x : Fin 2 → ℤ) ↦ ‖(eisSummand k x z)‖) _ (fun _ ↦ norm_nonneg _)
      (summable_norm_eisSummand hk z))

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
i j : Fin 2
⊢ ↑g i j = !![1, b; 0, 1] i j

Tactic:
fin_cases i

Goal state after:
case «0»
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
j : Fin 2
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) j = !![1, b; 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) j

case «1»
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
j : Fin 2
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) j = !![1, b; 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) j
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
⊢ Summable fun n ↦ ↑n ^ k * r ^ n * (1 / (1 - r ^ n))

Tactic:
apply Summable.mul_tendsto_const (c := 1 / (1 - 0))
    (by simpa using! summable_norm_pow_mul_geometric_of_norm_lt_one k hr)

Goal state after:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
⊢ Tendsto (fun n ↦ 1 / (1 - r ^ n)) cofinite (𝓝 (1 / (1 - 0)))
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
this✝ : ‖↑z + ↑(↑g 1 1)‖ ≤ 1
this : |↑(↑g 1 1) + z.re| ≤ 1
⊢ |↑g 1 1| ≤ 1

Tactic:
have := (abs_sub_abs_le_abs_add ..).trans this

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
this✝¹ : ‖↑z + ↑(↑g 1 1)‖ ≤ 1
this✝ : |↑(↑g 1 1) + z.re| ≤ 1
this : |↑(↑g 1 1)| - |z.re| ≤ 1
⊢ |↑g 1 1| ≤ 1
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
hb : ↑g 0 1 = -1
hz' : ‖↑z‖ = 1
i j : Fin 2
⊢ ↑g i j = !![↑g 0 0, -1; 1, 0] i j

Tactic:
fin_cases i

Goal state after:
case «0»
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
hb : ↑g 0 1 = -1
hz' : ‖↑z‖ = 1
j : Fin 2
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) j = !![↑g 0 0, -1; 1, 0] ((fun i ↦ i) ⟨0, ⋯⟩) j

case «1»
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
hb : ↑g 0 1 = -1
hz' : ‖↑z‖ = 1
j : Fin 2
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) j = !![↑g 0 0, -1; 1, 0] ((fun i ↦ i) ⟨1, ⋯⟩) j
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs

Goal state before:
pp: A B : SL(2, ℤ)
z : ℍ
⊢ ↑((↑A * ↑B) 1 0) * denom (toGL (φ B)) ↑z - ↑(↑B 1 0) * denom (toGL (φ A) * toGL (φ B)) ↑z = ↑(↑A 1 0)

Tactic:
simpa [sub_eq_iff_eq_add] using denom_aux A B z

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr.inr.inr.inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • S • z ∈ 𝒟
hg'✝ : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
hb : ↑g 0 1 = -1
hz' : ‖↑z‖ = 1
hg' : g = T ^ ↑g 0 0 * S
hSre : (S • z).re = -z.re
h : ↑g 0 0 = -1
this : |↑(-1) + -z.re| ≤ 1 / 2
hzre : z.re = -(1 / 2)
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ

Tactic:
rw [h, zpow_neg_one] at hg'

Goal state after:
case inr.inr.inr.inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • S • z ∈ 𝒟
hg'✝ : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
hb : ↑g 0 1 = -1
hz' : ‖↑z‖ = 1
hg' : g = T⁻¹ * S
hSre : (S • z).re = -z.re
h : ↑g 0 0 = -1
this : |↑(-1) + -z.re| ≤ 1 / 2
hzre : z.re = -(1 / 2)
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
i j : Fin 2
⊢ ↑g i j = !![↑g 0 0, -1 + ↑g 0 0; 1, 1] i j

Tactic:
fin_cases i

Goal state after:
case «0»
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
j : Fin 2
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) j = !![↑g 0 0, -1 + ↑g 0 0; 1, 1] ((fun i ↦ i) ⟨0, ⋯⟩) j

case «1»
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
j : Fin 2
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) j = !![↑g 0 0, -1 + ↑g 0 0; 1, 1] ((fun i ↦ i) ⟨1, ⋯⟩) j
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
⊢ (g = S * T ∨ g = T * S * T) ∧ z = ρ

Tactic:
by
  have hgeq : g = T ^ g 0 0 * S * T := by
    refine Subtype.ext ?_
    rw [coe_mul, coe_mul, coe_T_zpow, coe_S, coe_T, mul_fin_two, mul_fin_two]
    ring_nf
    ext i j
    fin_cases i <;> fin_cases j <;> [tauto; simp; tauto; tauto]
    grind [g.property, det_fin_two]
  rw [hgeq]
  obtain ⟨hnorm, hre⟩ : normSq z = 1 ∧ z.re = -1 / 2 := by
    have hnorm : normSq ((z : ℂ) + 1) ≤ 1 := by simpa [denom, hc, hd, norm_def] using hg'
    have : normSq (z + 1) = normSq z + (2 * z.re + 1) := by simp [normSq]; ring
    rw [this] at hnorm
    constructor <;> linarith [hz.1, show 0 ≤ 2 * z.re + 1 by linarith [(neg_le_abs _).trans hz.2]]
  have hρ : z = ρ := by
    apply eq_of_re_of_norm
    · simp [hre, ρ]
    · rw [norm_def, hnorm, norm_ρ, Real.sqrt_one]
  refine ⟨?_, hρ⟩
  have hSTρ : (S * T) • ρ = ρ := by
    rw [mul_smul, ← SL_neg_smul S, ← S_inv, inv_smul_eq_iff, eq_comm, UpperHalfPlane.ext_iff,
      modular_S_smul, modular_T_smul, UpperHalfPlane.coe_mk, coe_vadd,
      ← mul_one (_ : ℂ)⁻¹, inv_mul_eq_iff_eq_mul₀ (neg_ne_zero.mpr ρ.ne_zero)]
    grind [ρ_sq, ofReal_one]
  rw [hgeq, hρ, mul_assoc, mul_smul, hSTρ] at hg
  suffices g 0 0 = 0 ∨ g 0 0 = 1 by rcases this with h | h <;> simp [h]
  have hgzre := hg.2
  simp only [Fin.isValue, ρ, neg_div, one_div, ← coe_re, coe_T_zpow_smul_eq, add_re, intCast_re,
    abs_le, le_add_iff_nonneg_right, Int.cast_nonneg_iff, neg_add_le_iff_le_add,
    show (2⁻¹ : ℝ) + 2⁻¹ = 1 by norm_num] at hgzre
  rw [← Int.cast_one (R := ℝ), Int.cast_le] at hgzre
  grind

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this : ↑g 0 1 = -↑g 0 0 - 1
⊢ ↑g = !![1, ↑g 0 0; 0, 1] * !![0, -1; 1, 0] * ↑T⁻¹

Tactic:
← zpow_neg_one,

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this : ↑g 0 1 = -↑g 0 0 - 1
⊢ ↑g = !![1, ↑g 0 0; 0, 1] * !![0, -1; 1, 0] * ↑(T ^ (-1))
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this : ↑g 0 1 = -↑g 0 0 - 1
i j : Fin 2
⊢ ↑g i j = !![↑g 0 0, -1 - ↑g 0 0; 1, -1] i j

Tactic:
fin_cases i

Goal state after:
case «0»
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this : ↑g 0 1 = -↑g 0 0 - 1
j : Fin 2
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) j = !![↑g 0 0, -1 - ↑g 0 0; 1, -1] ((fun i ↦ i) ⟨0, ⋯⟩) j

case «1»
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this : ↑g 0 1 = -↑g 0 0 - 1
j : Fin 2
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) j = !![↑g 0 0, -1 - ↑g 0 0; 1, -1] ((fun i ↦ i) ⟨1, ⋯⟩) j
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case mul
γ g h : SL(2, ℤ)
hx✝ : g ∈ Subgroup.closure {S, T}
hy✝ : h ∈ Subgroup.closure {S, T}
ig : G2 ∣[2] g = G2 - D2 g
ih : G2 ∣[2] h = G2 - D2 h
⊢ G2 - D2 h + (-D2 g) ∣[2] h = G2 - (D2 g ∣[2] h + D2 h)

Tactic:
grind [SlashAction.neg_slash, SL_slash]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • (S * T⁻¹) • (1 +ᵥ ρ) ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this✝¹ : ↑g 0 1 = -↑g 0 0 - 1
hgeq : g = T ^ ↑g 0 0 * S * T⁻¹
hnorm : normSq ↑z + (-2 * z.re + 1) ≤ 1
this✝ : normSq (↑z - 1) = normSq ↑z + (-2 * z.re + 1)
h : normSq ↑z = 1
h' : z.re = 1 / 2
hρ : z = 1 +ᵥ ρ
this : S • ρ = T • ρ
⊢ T⁻¹ • (1 +ᵥ ρ) = S • (1 +ᵥ ρ)

Tactic:
← zpow_neg_one,

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • (S * T⁻¹) • (1 +ᵥ ρ) ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this✝¹ : ↑g 0 1 = -↑g 0 0 - 1
hgeq : g = T ^ ↑g 0 0 * S * T⁻¹
hnorm : normSq ↑z + (-2 * z.re + 1) ≤ 1
this✝ : normSq (↑z - 1) = normSq ↑z + (-2 * z.re + 1)
h : normSq ↑z = 1
h' : z.re = 1 / 2
hρ : z = 1 +ᵥ ρ
this : S • ρ = T • ρ
⊢ T ^ (-1) • (1 +ᵥ ρ) = S • (1 +ᵥ ρ)
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: k : ℤ
F : ℍ → ℂ
hF : MDiff F
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
hdet : ↑(Matrix.GeneralLinearGroup.det g) = (↑g).det
hdetℂ : ↑(↑g).det ≠ 0
hσ : ∀ (x : ℂ), (σ g) x = x
z : ℍ
hz : denom g ↑z ≠ 0
h_smul : HasDerivAt (fun w ↦ ↑(g • ↑ofComplex w)) (↑(↑g).det / denom g ↑z ^ 2) ↑z
h_F : HasDerivAt (F ∘ ↑ofComplex) (deriv (F ∘ ↑ofComplex) ↑(g • ↑ofComplex ↑z)) ↑(g • ↑ofComplex ↑z)
h_denom : HasDerivAt (fun w ↦ denom g w ^ (-k)) (-↑k * ↑(↑g 1 0) * denom g ↑z ^ (-k - 1)) ↑z
w : ℂ
hw : 0 < w.im
⊢ (F ∣[k] g ∘ ↑ofComplex) w = ↑(↑g).det ^ (k - 1) * ((F ∘ ↑ofComplex) ↑(g • ↑ofComplex w) * denom g w ^ (-k))

Tactic:
grind [ofComplex_apply_of_im_pos, ofComplex_apply, ModularForm.slash_apply]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: k : ℤ
F : ℍ → ℂ
hF : MDiff F
γ : SL(2, ℤ)
hdet : (↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ))).det = 1
z : ℍ
⊢ D (F ∣[k] γ) z =
    (D F ∣[k + 2] γ - fun z ↦
        ↑k * (2 * ↑π * I)⁻¹ *
            (↑(↑γ 1 0) /
              denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z) *
          (F ∣[k] γ) z)
      z

Tactic:
have := congrFun
    (normalizedDerivOfComplex_slash (k := k) hF (g := (γ : GL (Fin 2) ℝ)) (by grind)) z

Goal state after:
k : ℤ
F : ℍ → ℂ
hF : MDiff F
γ : SL(2, ℤ)
hdet : (↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ))).det = 1
z : ℍ
this :
  D (F ∣[k] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) z =
    (↑(↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ))).det)⁻¹ *
        (D F ∣[k + 2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) z -
      ↑k * (2 * ↑π * I)⁻¹ *
          (↑(↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) 1 0) /
            denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z) *
        (F ∣[k] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) z
⊢ D (F ∣[k] γ) z =
    (D F ∣[k + 2] γ - fun z ↦
        ↑k * (2 * ↑π * I)⁻¹ *
            (↑(↑γ 1 0) /
              denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z) *
          (F ∣[k] γ) z)
      z
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case h
k : ℕ
hk : 3 ≤ k
hk2 : Even k
⊢ ∀
    (w :
      ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k ⧸
        cuspFormSubmodule (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k),
    ∃ c, c • Submodule.Quotient.mk (E hk) = w

Tactic:
refine (Submodule.Quotient.forall _).mpr fun f ↦ ⟨(qExpansion 1 f).coeff 0, ?_⟩
    rw [← Submodule.Quotient.mk_smul, Submodule.Quotient.eq, mem_cuspFormSubmodule_iff,
      isCuspForm_iff_coeffZero_eq_zero, FunLike.coe_sub, ModularForm.qExpansion_sub,
      FunLike.coe_smul, ModularForm.qExpansion_smul, map_sub,
      PowerSeries.coeff_smul, E_qExpansion_coeff_zero hk hk2, smul_eq_mul, mul_one, sub_self]
    all_goals simp

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : (g • z).im = z.im
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ},
    z ∈ 𝒟 →
      g • z ∈ 𝒟 →
        (g • z).im = z.im →
          0 ≤ ↑g 1 0 →
            (g = 1 ∨ g = -1) ∨
              (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨
                (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨
                  (g = S ∨ g = -S) ∧ ‖↑z‖ = 1 ∨
                    (g = T * S ∨ g = -(T * S)) ∧ z = 1 +ᵥ ρ ∨
                      (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
                        (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
                          (g = S * T ∨ g = -(S * T)) ∧ z = ρ ∨
                            (g = T * S * T ∨ g = -(T * S * T)) ∧ z = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ z = ρ
hc : ¬0 ≤ ↑g 1 0
⊢ (g = 1 ∨ g = -1) ∨
    (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨
      (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨
        (g = S ∨ g = -S) ∧ ‖↑z‖ = 1 ∨
          (g = T * S ∨ g = -(T * S)) ∧ z = 1 +ᵥ ρ ∨
            (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
              (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
                (g = S * T ∨ g = -(S * T)) ∧ z = ρ ∨
                  (g = T * S * T ∨ g = -(T * S * T)) ∧ z = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ z = ρ

Tactic:
simpa [neg_eq_iff_eq_neg, or_comm] using @this (-g) z hz (by simpa using hg)
      (by simpa using him) (by simpa using (not_le.mp hc).le)

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
⊢ ↑π * I * ↑n ^ 2 * τ = ↑(π * ↑n ^ 2) * (τ * I)

Tactic:
push_cast; ring

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: x : ℂ
⊢ x ∈ UpperHalfPlane.coe '' 𝒟ᵒ ↔ x ∈ {z | 0 < z.im ∧ 1 < ‖z‖ ∧ |z.re| < 1 / 2}

Tactic:
refine ⟨?_, fun ⟨hxim, hxnorm, hxre⟩ ↦ ⟨⟨x, hxim⟩, ⟨one_lt_normSq_iff.mpr hxnorm, hxre⟩, rfl⟩⟩

Goal state after:
x : ℂ
⊢ x ∈ UpperHalfPlane.coe '' 𝒟ᵒ → x ∈ {z | 0 < z.im ∧ 1 < ‖z‖ ∧ |z.re| < 1 / 2}
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case h.refine_2
x : ℍ
hxnorm : 1 < ‖↑x‖
hxre : |x.re| ≤ 1 / 2
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[<] 1, |(↑ofComplex (↑x_1 * ↑x)).re| < 1 / 2

Tactic:
· simp only [eventually_nhdsWithin_iff]
      filter_upwards [eventually_gt_nhds zero_lt_one] with a ha ha'
      rw [← coe_re, ofComplex_apply_of_im_pos (by simpa using mul_pos ha x.coe_im_pos)]
      suffices a * |x.re| < 1 / 2 by simpa [abs_of_pos ha]
      nlinarith [Set.mem_Iio.mp ha']

Goal state after: