mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
⊢ IsBoundedAtImInfty (⇑(eisensteinSeriesSIF a k) ∣[k] A)

Tactic:
[

Goal state after:
N : ℕ
inst✝ : NeZero N
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
⊢ IsBoundedAtImInfty (⇑(eisensteinSeriesSIF a k) ∣[k] A)
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Γ.IsArithmetic
F : Type u_2
F' : Type u_3
f : F
f' : F'
inst✝³ : FunLike F ℍ ℂ
inst✝² : FunLike F' ℍ ℂ
inst✝¹ : CuspFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
g : SL(2, ℤ)
⊢ Tendsto (fun τ ↦ petersson k (⇑f) (⇑f') (g • τ)) atImInfty (𝓝 0)

Tactic:
[

Goal state after:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Γ.IsArithmetic
F : Type u_2
F' : Type u_3
f : F
f' : F'
inst✝³ : FunLike F ℍ ℂ
inst✝² : FunLike F' ℍ ℂ
inst✝¹ : CuspFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
g : SL(2, ℤ)
⊢ Tendsto (fun τ ↦ petersson k (⇑f) (⇑f') (g • τ)) atImInfty (𝓝 0)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ (↑N * n) • z ∈ verticalStrip (↑N) z.im
hk' : 2 < ↑k
x : Fin 2 → ℤ
⊢ ‖eisSummand k x (ModularGroup.T ^ (↑N * n) • z)‖ ≤
    r { coe := { re := ↑N, im := 2 }, coe_im_pos := ⋯ } ^ (-k) * ‖x‖ ^ (-k)

Tactic:
[

Goal state after:
N : ℕ
inst✝ : NeZero N
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ (↑N * n) • z ∈ verticalStrip (↑N) z.im
hk' : 2 < ↑k
x : Fin 2 → ℤ
⊢ ‖eisSummand k x (ModularGroup.T ^ (↑N * n) • z)‖ ≤
    r { coe := { re := ↑N, im := 2 }, coe_im_pos := ⋯ } ^ (-k) * ‖x‖ ^ (-k)
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
inst✝ : Γ.HasDetPlusMinusOne
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
f : ModularForm Γ k
n : ℕ
⊢ qExpansion h ⇑(f.pow n) = qExpansion h ⇑f ^ n

Tactic:
by
  induction n with
  | zero => simp only [coe_pow, pow_zero, qExpansion_one]
  | succ n ih =>
    rw [coe_pow, pow_succ, ← coe_pow, ← coe_mul, ModularForm.qExpansion_mul hh hΓ, ih,
      pow_succ]

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
hΓ : ∃ h ∈ Γ.strictPeriods, 0 < h
a b : ℤ
f : ModularForm Γ a
g : ModularForm Γ b
hf : f ≠ 0
hg : g ≠ 0
⊢ f.mul g ≠ 0

Tactic:
obtain ⟨h, hΓ, hh⟩ := hΓ

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
a b : ℤ
f : ModularForm Γ a
g : ModularForm Γ b
hf : f ≠ 0
hg : g ≠ 0
h : ℝ
hΓ : h ∈ Γ.strictPeriods
hh : 0 < h
⊢ f.mul g ≠ 0
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: 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

Tactic:
fin_cases j

Goal state after:
case «0».«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
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![1, b; 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«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
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![1, b; 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: 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

Tactic:
fin_cases j

Goal state after:
case «1».«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
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![1, b; 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«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
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![1, b; 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: 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

Tactic:
fin_cases j

Goal state after:
case «0».«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
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![↑g 0 0, -1; 1, 0] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«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
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![↑g 0 0, -1; 1, 0] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: 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

Tactic:
fin_cases j

Goal state after:
case «1».«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
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![↑g 0 0, -1; 1, 0] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«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
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![↑g 0 0, -1; 1, 0] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
r : 𝕜
hr : ‖r‖ < 1
h1 : ∀ (m : ℕ+), ‖r ^ ↑m‖ < 1
m : ℕ+
this : (r ^ ↑m) ^ 0 + ∑' (n : ℕ+), (r ^ ↑m) ^ ↑n = (1 - r ^ ↑m)⁻¹
⊢ ∑' (n : ℕ+), r ^ (↑n * ↑m) = (1 - r ^ ↑m)⁻¹ - 1

Tactic:
[

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
r : 𝕜
hr : ‖r‖ < 1
h1 : ∀ (m : ℕ+), ‖r ^ ↑m‖ < 1
m : ℕ+
this : (r ^ ↑m) ^ 0 + ∑' (n : ℕ+), (r ^ ↑m) ^ ↑n = (1 - r ^ ↑m)⁻¹
⊢ ∑' (n : ℕ+), r ^ (↑n * ↑m) = (1 - r ^ ↑m)⁻¹ - 1
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), ‖f τ‖ ≤ C * max 1 (1 / τ.im ^ k)
⊢ ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-↑k)

Tactic:
[

Goal state after:
k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), ‖f τ‖ ≤ C * max 1 (1 / τ.im ^ k)
⊢ ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-↑k)
Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst✝⁴ : FunLike F ℍ ℂ
inst✝³ : DiscreteTopology ↥Γ
inst✝² : Γ.HasDetPlusMinusOne
inst✝¹ : Fact (IsCusp ∞ Γ)
inst✝ : ModularFormClass F Γ k
f : F
h : valueAtInfty ⇑f = 0
hh : 0 < Γ.strictWidthInfty
hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods
hanal : AnalyticAt ℂ (cuspFunction Γ.strictWidthInfty ⇑f) 0
hper : Function.Periodic (⇑f ∘ ↑ofComplex) ↑Γ.strictWidthInfty
⊢ IsZeroAtImInfty ⇑f

Tactic:
[

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst✝⁴ : FunLike F ℍ ℂ
inst✝³ : DiscreteTopology ↥Γ
inst✝² : Γ.HasDetPlusMinusOne
inst✝¹ : Fact (IsCusp ∞ Γ)
inst✝ : ModularFormClass F Γ k
f : F
h : valueAtInfty ⇑f = 0
hh : 0 < Γ.strictWidthInfty
hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods
hanal : AnalyticAt ℂ (cuspFunction Γ.strictWidthInfty ⇑f) 0
hper : Function.Periodic (⇑f ∘ ↑ofComplex) ↑Γ.strictWidthInfty
⊢ IsZeroAtImInfty ⇑f
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: 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

Tactic:
fin_cases j

Goal state after:
case «0».«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
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![↑g 0 0, -1 + ↑g 0 0; 1, 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«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
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![↑g 0 0, -1 + ↑g 0 0; 1, 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: 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

Tactic:
fin_cases j

Goal state after:
case «1».«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
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![↑g 0 0, -1 + ↑g 0 0; 1, 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«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
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![↑g 0 0, -1 + ↑g 0 0; 1, 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨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
hgeq : g = T ^ ↑g 0 0 * S * T
hnorm : normSq (↑z + 1) ≤ 1
this : normSq (↑z + 1) = normSq ↑z + (2 * z.re + 1)
⊢ normSq ↑z = 1 ∧ z.re = -1 / 2

Tactic:
this

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
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)
⊢ normSq ↑z = 1 ∧ z.re = -1 / 2
Module: Mathlib.NumberTheory.ModularForms.DedekindEta

Goal state before:
pp: q : ℂ
hq : ‖q‖ < 1
⊢ Multipliable fun n ↦ 1 - q ^ (n + 1)

Tactic:
by
  apply multipliable_one_add_of_summable (f := fun n ↦ -q ^ (n + 1))
  simpa using (summable_nat_add_iff 1).mpr (summable_geometric_of_lt_one (norm_nonneg _) hq)

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

Goal state before:
pp: case h
⊢ HasProdLocallyUniformlyOn (fun n q ↦ 1 - q ^ (n + 1)) (fun q ↦ ∏' (n : ℕ), (1 - q ^ (n + 1))) (Metric.ball 0 1)

Tactic:
[

Goal state after:
case h
⊢ HasProdLocallyUniformlyOn (fun n q ↦ 1 - q ^ (n + 1)) (fun q ↦ ∏' (n : ℕ), (1 - q ^ (n + 1))) (Metric.ball 0 1)
Module: Mathlib.NumberTheory.ModularForms.DedekindEta

Goal state before:
pp: K : Set ℂ
hK : K ⊆ Metric.ball 0 1
hcK : IsCompact K
hN : K.Nonempty
q₀ : ℂ
hq₀ : q₀ ∈ K
left✝ : sSup ((fun q ↦ ‖q‖) '' K) = ‖q₀‖
HB : ∀ y ∈ K, ‖y‖ ≤ ‖q₀‖
⊢ ‖?m.238‖ < 1

Tactic:
simpa [Metric.mem_ball, dist_zero_right] using hK hq₀

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

Goal state before:
pp: z : ℂ
n : ℕ
h2 : (fun x ↦ 1 - cexp (2 * ↑π * I * (↑n + 1) * x)) = (fun z ↦ 1 - 1 * cexp z) ∘ fun x ↦ 2 * ↑π * I * (↑n + 1) * x
⊢ logDeriv (fun x ↦ 1 - eta_q n x) z = 2 * ↑π * I * (↑n + 1) * -eta_q n z / (1 - eta_q n z)

Tactic:
[

Goal state after:
z : ℂ
n : ℕ
h2 : (fun x ↦ 1 - cexp (2 * ↑π * I * (↑n + 1) * x)) = (fun z ↦ 1 - 1 * cexp z) ∘ fun x ↦ 2 * ↑π * I * (↑n + 1) * x
⊢ logDeriv (fun x ↦ 1 - eta_q n x) z = 2 * ↑π * I * (↑n + 1) * -eta_q n z / (1 - eta_q n z)
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).det = 1
⊢ ↑g 0 1 = -↑g 0 0 - 1

Tactic:
[

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).det = 1
⊢ ↑g 0 1 = -↑g 0 0 - 1
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: z : ℍ
⊢ Summable fun m ↦ G2Term z m - δ m

Tactic:
[

Goal state after:
z : ℍ
⊢ Summable fun m ↦ G2Term z m - δ m
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: 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

Tactic:
fin_cases j

Goal state after:
case «0».«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
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![↑g 0 0, -1 - ↑g 0 0; 1, -1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«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
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![↑g 0 0, -1 - ↑g 0 0; 1, -1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: 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

Tactic:
fin_cases j

Goal state after:
case «1».«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
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![↑g 0 0, -1 - ↑g 0 0; 1, -1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«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
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![↑g 0 0, -1 - ↑g 0 0; 1, -1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case neg
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : ¬b = 0
⊢ (↑b * ↑z + ↑n + 1)⁻¹ * ((↑b * ↑z + ↑n) ^ 2)⁻¹ + δ ![b, n] + ((↑b * ↑z + ↑n)⁻¹ - (↑b * ↑z + ↑n + 1)⁻¹) =
    ((↑b * ↑z + ↑n) ^ 2)⁻¹

Tactic:
· have h0 : (b : ℂ) * z + n + 1 ≠ 0 := by
        simpa [add_assoc] using linear_ne_zero (cd := ![b, n + 1]) z (by aesop)
      have h1 : (b : ℂ) * z + n ≠ 0 := linear_ne_zero (cd := ![b, n]) z (by aesop)
      simp [δ]
      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
hgeq : g = T ^ ↑g 0 0 * S * T⁻¹
hnorm : normSq (↑z - 1) ≤ 1
this : normSq (↑z - 1) = normSq ↑z + (-2 * z.re + 1)
⊢ (g = S * T⁻¹ ∨ g = T⁻¹ * S * T⁻¹) ∧ z = 1 +ᵥ ρ

Tactic:
this

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
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)
⊢ (g = S * T⁻¹ ∨ g = T⁻¹ * S * T⁻¹) ∧ z = 1 +ᵥ ρ
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: z : ℍ
⊢ (G2 ∣[2] T) z = G2 z

Tactic:
[

Goal state after:
z : ℍ
⊢ (G2 ∣[2] T) z = G2 z
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case inv
γ g : SL(2, ℤ)
hx✝ : g ∈ Subgroup.closure {S, T}
ig : G2 ∣[2] g = G2 - D2 g
H1 : (G2 ∣[2] g) ∣[2] g⁻¹ = (G2 - D2 g) ∣[2] g⁻¹
⊢ G2 ∣[2] g⁻¹ = G2 - D2 g⁻¹

Tactic:
[

Goal state after:
case inv
γ g : SL(2, ℤ)
hx✝ : g ∈ Subgroup.closure {S, T}
ig : G2 ∣[2] g = G2 - D2 g
H1 : (G2 ∣[2] g) ∣[2] g⁻¹ = (G2 - D2 g) ∣[2] g⁻¹
⊢ G2 ∣[2] g⁻¹ = G2 - D2 g⁻¹
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 • ρ
this : (S * T⁻¹) • (1 +ᵥ ρ) = 1 +ᵥ ρ
⊢ g = S * T⁻¹ ∨ g = T⁻¹ * S * T⁻¹

Tactic:
this

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • (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 • ρ
this : (S * T⁻¹) • (1 +ᵥ ρ) = 1 +ᵥ ρ
⊢ g = S * T⁻¹ ∨ g = T⁻¹ * S * T⁻¹
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: k c : ℂ
F : ℍ → ℂ
hF : MDiff F
⊢ serreDerivative k (c • F) = c • serreDerivative k F

Tactic:
by
  ext z
  simp [serreDerivative, normalizedDerivOfComplex_smul c F hF, smul_eq_mul]
  ring_nf

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

Goal state before:
pp: z : ℍ
⊢ Δ (1 +ᵥ z) *
      (↑(↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.T)) 1 0) *
            ↑z +
          ↑(↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.T)) 1
              1)) ^
        (-12) =
    Δ z

Tactic:
ModularGroup.T

Goal state after:
z : ℍ
⊢ Δ (1 +ᵥ z) *
      (↑(↑(Matrix.SpecialLinearGroup.toGL
                    ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ⟨!![1, 1; 0, 1], ModularGroup.T._proof_1⟩))
                1 0) *
            ↑z +
          ↑(↑(Matrix.SpecialLinearGroup.toGL
                  ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ⟨!![1, 1; 0, 1], ModularGroup.T._proof_1⟩))
              1 1)) ^
        (-12) =
    Δ z
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: z : ℍ
this : η (-(↑z)⁻¹) ^ 24 * (↑z ^ 12)⁻¹ = η ↑z ^ 24
⊢ (Δ ∣[12] ModularGroup.S) z = Δ z

Tactic:
rw [SL_slash_apply, UpperHalfPlane.modular_S_smul]

Goal state after:
z : ℍ
this : η (-(↑z)⁻¹) ^ 24 * (↑z ^ 12)⁻¹ = η ↑z ^ 24
⊢ Δ { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } *
      denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S)) ↑z ^
        (-12) =
    Δ z
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: this :
  (Summable fun n ↦ (1 / 2) ^ (n + 1)) →
    (∀ (k : ℕ), Tendsto (fun x ↦ -x ^ (k + 1)) (𝓝 0) (𝓝 0)) →
      (∀ᶠ (n : ℂ) in 𝓝 0, ∀ (k : ℕ), ‖n‖ ^ (k + 1) ≤ (1 / 2) ^ (k + 1)) →
        Tendsto (fun n ↦ ∏' (k : ℕ), (1 + -n ^ (k + 1))) (𝓝 0) (𝓝 1)
⊢ Tendsto (fun q ↦ ∏' (n : ℕ), (1 - q ^ (n + 1))) (𝓝 0) (𝓝 1)

Tactic:
[

Goal state after:
this :
  (Summable fun n ↦ (1 / 2) ^ (n + 1)) →
    (∀ (k : ℕ), Tendsto (fun x ↦ -x ^ (k + 1)) (𝓝 0) (𝓝 0)) →
      (∀ᶠ (n : ℂ) in 𝓝 0, ∀ (k : ℕ), ‖n‖ ^ (k + 1) ≤ (1 / 2) ^ (k + 1)) →
        Tendsto (fun n ↦ ∏' (k : ℕ), (1 + -n ^ (k + 1))) (𝓝 0) (𝓝 1)
⊢ Tendsto (fun q ↦ ∏' (n : ℕ), (1 - q ^ (n + 1))) (𝓝 0) (𝓝 1)
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: A : SL(2, ℤ)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact slash_action_generators_SL2Z discriminant_S_invariant discriminant_T_invariant A

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: case e_a.e_f
z : ℍ
N a : ℕ
H2 :
  ∑' (n : ℤ), ((↑n + ↑z * (↑a + 1)) ^ 2)⁻¹ =
    (I * (↑π * 2)) ^ 2 * ∑' (n : ℕ+), cexp (↑z * (↑a + 1) * (I * (↑π * 2))) ^ ↑n * ↑↑n
⊢ 2 * ∑' (n : ℤ), ((↑n + ↑z * (↑a + 1)) ^ 2)⁻¹ =
    -(8 * (↑π ^ 2 * ∑' (n : ℕ+), cexp (↑z * (I * ↑π) * 2) ^ ↑n * (cexp (↑z * (I * ↑π) * 2) ^ (a * ↑n) * ↑↑n)))

Tactic:
[

Goal state after:
case e_a.e_f
z : ℍ
N a : ℕ
H2 :
  ∑' (n : ℤ), ((↑n + ↑z * (↑a + 1)) ^ 2)⁻¹ =
    (I * (↑π * 2)) ^ 2 * ∑' (n : ℕ+), cexp (↑z * (↑a + 1) * (I * (↑π * 2))) ^ ↑n * ↑↑n
⊢ 2 * ∑' (n : ℤ), ((↑n + ↑z * (↑a + 1)) ^ 2)⁻¹ =
    -(8 * (↑π ^ 2 * ∑' (n : ℕ+), cexp (↑z * (I * ↑π) * 2) ^ ↑n * (cexp (↑z * (I * ↑π) * 2) ^ (a * ↑n) * ↑↑n)))
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℤ
f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
γ : SL(2, ℤ)
hγ :
  Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ) ∈
    (Matrix.SpecialLinearGroup.mapGL ℝ).range
⊢ (⇑f / ⇑discriminant) ∣[k - 12] γ = ⇑f / ⇑discriminant

Tactic:
[

Goal state after:
k : ℤ
f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
γ : SL(2, ℤ)
hγ :
  Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ) ∈
    (Matrix.SpecialLinearGroup.mapGL ℝ).range
⊢ (⇑f / ⇑discriminant) ∣[k - 12] γ = ⇑f / ⇑discriminant
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℤ
c : ℂ
a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext z
    change (c * a z) / Δ z = c * (a z / Δ z)
    rw [mul_div_assoc]

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

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  iteratedDerivWithin k (fun z ↦ ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * z) ^ n) ℍₒ ↑z =
    -(2 * ↑π * I) * ∑' (n : ℕ), iteratedDerivWithin k (fun s ↦ cexp (2 * ↑π * I * s) ^ n) ℍₒ ↑z
⊢ -(2 * ↑π * I * (2 * ↑π * I) ^ k) * ∑' (n : ℕ), ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n =
    -(2 * ↑π * I) * ∑' (n : ℕ), (2 * ↑π * I * ↑n) ^ k * cexp (2 * ↑π * I * ↑z) ^ n

Tactic:
[

Goal state after:
k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  iteratedDerivWithin k (fun z ↦ ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * z) ^ n) ℍₒ ↑z =
    -(2 * ↑π * I) * ∑' (n : ℕ), iteratedDerivWithin k (fun s ↦ cexp (2 * ↑π * I * s) ^ n) ℍₒ ↑z
⊢ -(2 * ↑π * I * (2 * ↑π * I) ^ k) * ∑' (n : ℕ), ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n =
    -(2 * ↑π * I) * ∑' (n : ℕ), (2 * ↑π * I * ↑n) ^ k * cexp (2 * ↑π * I * ↑z) ^ n