mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k ≤ 0
f : F
τ : ℍ
γ : SL(2, ℤ)
hγ : 1 / 2 ≤ (γ • τ).im
hdenom : ‖denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ‖ ≤ 1
this : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(1)) k
⊢ ‖f τ‖ ≤ ‖f (γ • τ)‖

Tactic:
simpa using

Goal state after:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k ≤ 0
f : F
τ : ℍ
γ : SL(2, ℤ)
hγ : 1 / 2 ≤ (γ • τ).im
hdenom : ‖denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ‖ ≤ 1
this : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(1)) k
⊢ ‖f τ‖ ≤
    ‖denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ‖ ^ k * ‖f τ‖
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
f : F
c : ℂ
hf : ⇑f = Function.const ℍ c
this✝ : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(1)) k
hI : c = ↑UpperHalfPlane.I ^ k * c
h2I2 : c = ↑(⟨2, ⋯⟩ • UpperHalfPlane.I) ^ k * c
this : 2 ^ k = 1 ↔ k = 0
⊢ k = 0 ∨ c = 0

Tactic:
simpa using

Goal state after:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
f : F
c : ℂ
hf : ⇑f = Function.const ℍ c
this✝ : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(1)) k
hI : c = ↑UpperHalfPlane.I ^ k * c
h2I2 : c = ↑(⟨2, ⋯⟩ • UpperHalfPlane.I) ^ k * c
this : 2 ^ k = 1 ↔ k = 0
⊢ k = 0 ∨ c = 0
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
H1 : HasFPowerSeriesOnBall (update (cuspFunction h f) 0 (c 0)) (FormalMultilinearSeries.ofScalars ℂ c) 0 1
L1 : ContinuousAt (update (cuspFunction h f) 0 (c 0)) 0
L2 : ContinuousAt (cuspFunction h f) 0
this : update (cuspFunction h f) 0 (c 0) =ᶠ[𝓝 0] cuspFunction h f
⊢ c 0 = cuspFunction h f 0

Tactic:
simpa using

Goal state after:
h : ℝ
f : ℍ → ℂ
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
H1 : HasFPowerSeriesOnBall (update (cuspFunction h f) 0 (c 0)) (FormalMultilinearSeries.ofScalars ℂ c) 0 1
L1 : ContinuousAt (update (cuspFunction h f) 0 (c 0)) 0
L2 : ContinuousAt (cuspFunction h f) 0
this : update (cuspFunction h f) 0 (c 0) =ᶠ[𝓝 0] cuspFunction h f
⊢ c 0 = cuspFunction h f 0
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
f : F
c : ℂ
hf : ⇑f = Function.const ℍ c
this : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(1)) k
hI : c = ↑UpperHalfPlane.I ^ k * c
h2I2 : c = ↑(⟨2, ⋯⟩ • UpperHalfPlane.I) ^ k * c
⊢ 2 ^ k = 1 ↔ k = 0

Tactic:
simpa using

Goal state after:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
f : F
c : ℂ
hf : ⇑f = Function.const ℍ c
this : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(1)) k
hI : c = ↑UpperHalfPlane.I ^ k * c
h2I2 : c = ↑(⟨2, ⋯⟩ • UpperHalfPlane.I) ^ k * c
⊢ 2 ^ k = 1 ↔ k = 0
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 : f =O[atImInfty] fun z ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hF𝒟 : ‖f (g • τ)‖ ≤ F * (g • τ).im ^ t
hg : g • τ ∈ 𝒟
⊢ ‖f τ‖ ≤ F * max τ.im (1 / τ.im) ^ t

Tactic:
hf_inv g τ

Goal state after:
E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
hg : g • τ ∈ 𝒟
⊢ ‖f τ‖ ≤ F * max τ.im (1 / τ.im) ^ t
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k ≤ 0
f : F
hq : 0 ∈ Metric.ball 0 1
⊢ ‖0‖ ≤ rexp (-π)

Tactic:
simpa using

Goal state after:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k ≤ 0
f : F
hq : 0 ∈ Metric.ball 0 1
⊢ 0 ≤ rexp (-π)
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k ≤ 0
f : F
q : ℂ
hq : q ∈ Metric.ball 0 1
hq' : q ≠ 0
ξ : ℍ
hξ : 1 / 2 ≤ ξ.im
hξ₂ : ‖f { coe := invQParam 1 q, coe_im_pos := ⋯ }‖ ≤ ‖f ξ‖
⊢ ‖UpperHalfPlane.cuspFunction 1 (⇑f) q‖ ≤ ‖UpperHalfPlane.cuspFunction 1 (⇑f) (𝕢 1 ↑ξ)‖

Tactic:
simpa using

Goal state after:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k ≤ 0
f : F
q : ℂ
hq : q ∈ Metric.ball 0 1
hq' : q ≠ 0
ξ : ℍ
hξ : 1 / 2 ≤ ξ.im
hξ₂ : ‖f { coe := invQParam 1 q, coe_im_pos := ⋯ }‖ ≤ ‖f ξ‖
⊢ ‖UpperHalfPlane.cuspFunction 1 (⇑f) q‖ ≤ ‖UpperHalfPlane.cuspFunction 1 (⇑f) (𝕢 1 ↑ξ)‖
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
⊢ (T • z).re = z.re + 1

Tactic:
simpa using

Goal state after:
z : ℍ
⊢ (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) T) • z).re = z.re + 1
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
⊢ (T • z).im = z.im

Tactic:
simpa using

Goal state after:
z : ℍ
⊢ (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) T) • z).im = z.im
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k ≤ 0
f : F
z : ℍ
⊢ 𝕢 1 ↑z ∈ Metric.ball 0 1

Tactic:
simpa using

Goal state after:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k ≤ 0
f : F
z : ℍ
⊢ ‖𝕢 1 ↑z‖ < 1
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
⊢ (T⁻¹ • z).im = z.im

Tactic:
simpa using

Goal state after:
z : ℍ
⊢ ((toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) T))⁻¹ • z).im = z.im
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k ≤ 0
f : F
z : ℍ
hQ : 𝕢 1 ↑z ∈ Metric.ball 0 1
⊢ f z = Function.const ℍ (UpperHalfPlane.cuspFunction 1 (⇑f) 0) z

Tactic:
simpa using

Goal state after:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k ≤ 0
f : F
z : ℍ
hQ : 𝕢 1 ↑z ∈ Metric.ball 0 1
⊢ UpperHalfPlane.cuspFunction 1 (⇑f) (𝕢 1 ↑z) = UpperHalfPlane.cuspFunction 1 (⇑f) 0
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: k : ℤ
F : Type u_1
inst✝ : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f✝ : F
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
u : ℝ
⊢ 0 < (↑u + ↑t * ↑I).im

Tactic:
simpa using

Goal state after:
k : ℤ
F : Type u_1
inst✝ : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f✝ : F
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
u : ℝ
⊢ 0 < t
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
⊢ -2 * π * t / h < 0

Tactic:
simpa using

Goal state after:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
⊢ 0 < 2 * π * t / h
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: k : ℤ
hk : k < 0
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
⊢ 1 • f = 0

Tactic:
simpa using

Goal state after:
k : ℤ
hk : k < 0
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
⊢ ⇑f = 0
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 : f =O[atImInfty] fun z ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
hg✝ : g • τ ∈ 𝒟
hg : ↑g 1 0 = 0
hg' : ↑g 1 1 = 0
⊢ 0 = 1

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
hg✝ : g • τ ∈ 𝒟
hg : ↑g 1 0 = 0
hg' : ↑g 1 1 = 0
⊢ 0 = 1
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: case pos
E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
hg✝ : g • τ ∈ 𝒟
hg : ↑g 1 0 = 0
this✝ : ↑g 1 1 ≠ 0
this : 1 ≤ ↑(↑g 1 1) ^ 2
⊢ τ.im / ↑(↑g 1 1) ^ 2 ≤ τ.im

Tactic:
simpa using

Goal state after:
case pos
E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
hg✝ : g • τ ∈ 𝒟
hg : ↑g 1 0 = 0
this✝ : ↑g 1 1 ≠ 0
this : 1 ≤ ↑(↑g 1 1) ^ 2
⊢ (↑(↑g 1 1) ^ 2)⁻¹ ≤ 1
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: 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
this : g = -T ^ (-↑g 0 1)
z : ℍ
⊢ g • z = T ^ (-↑g 0 1) • z

Tactic:
conv_lhs => rw [this, SL_neg_smul]

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, ℤ)
hvr : v = r • (v / ↑r)
⊢ finGcdMap (r • (v / ↑r) ᵥ* ↑A) = r

Tactic:
simpa using

Goal state after:
r : ℕ
inst✝ : NeZero r
v : Fin 2 → ℤ
hab : finGcdMap v = r
A : SL(2, ℤ)
hvr : v = r • (v / ↑r)
⊢ finGcdMap (↑r * (v / ↑r) ᵥ* ↑A) = r
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
hR1 : R < 1
u : ℝ
⊢ 0 < (↑u + ↑t * ↑I).im

Tactic:
simpa using

Goal state after:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
hR1 : R < 1
u : ℝ
⊢ 0 < t
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
h : 1 < normSq ↑z
⊢ normSq
      ((↑((algebraMap ℤ ℝ) (↑S 0 0)) * ↑z + ↑((algebraMap ℤ ℝ) (↑S 0 1))) /
        (↑((algebraMap ℤ ℝ) (↑S 1 0)) * ↑z + ↑((algebraMap ℤ ℝ) (↑S 1 1)))) <
    1

Tactic:
simpa using

Goal state after:
z : ℍ
h : 1 < normSq ↑z
⊢ (normSq ↑z)⁻¹ < 1
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
h : z ∈ 𝒟ᵒ
⊢ 1 < z.re * z.re + z.im * z.im

Tactic:
simpa using

Goal state after:
z : ℍ
h : z ∈ 𝒟ᵒ
⊢ 1 < z.re * z.re + z.im * z.im
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: τ : ℍ
h : τ ∈ 𝒟
⊢ 1 ≤ τ.re * τ.re + τ.im * τ.im

Tactic:
simpa using

Goal state after:
τ : ℍ
h : τ ∈ 𝒟
⊢ 1 ≤ τ.re * τ.re + τ.im * τ.im
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg' : ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |(g • z).re| ≤ |(g' • z).re|
hg'' : (g • z).im = (g₀ • z).im
⊢ ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im

Tactic:
simpa using

Goal state after:
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg' : ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |(g • z).re| ≤ |(g' • z).re|
hg'' : (g • z).im = (g₀ • z).im
⊢ ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
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 τ
f' : ℍ → SL(2, ℤ) ⧸ Γ → E := fun τ ↦ Quotient.lift (fun g ↦ f (g⁻¹ • τ)) ⋯
hf'_cont : ∀ (γ : SL(2, ℤ) ⧸ Γ), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ f' x γ
hf'_inv : ∀ (τ : ℍ) (g : SL(2, ℤ)) (γ : SL(2, ℤ) ⧸ Γ), f' (g • τ) (g • γ) = f' τ γ
hf'_infty : ∀ (γ : SL(2, ℤ) ⧸ Γ), (fun x ↦ f' x γ) =O[atImInfty] fun z ↦ z.im ^ t
this : Fintype (SL(2, ℤ) ⧸ Γ)
C : ℝ
hC : ∀ (τ : ℍ), ‖∑ c, ‖f' τ c‖‖ ≤ C * max τ.im (1 / τ.im) ^ t
τ : ℍ
⊢ ‖f τ‖ ≤ ‖∑ c, ‖f' τ c‖‖

Tactic:
simpa using

Goal state after:
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 τ
f' : ℍ → SL(2, ℤ) ⧸ Γ → E := fun τ ↦ Quotient.lift (fun g ↦ f (g⁻¹ • τ)) ⋯
hf'_cont : ∀ (γ : SL(2, ℤ) ⧸ Γ), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ f' x γ
hf'_inv : ∀ (τ : ℍ) (g : SL(2, ℤ)) (γ : SL(2, ℤ) ⧸ Γ), f' (g • τ) (g • γ) = f' τ γ
hf'_infty : ∀ (γ : SL(2, ℤ) ⧸ Γ), (fun x ↦ f' x γ) =O[atImInfty] fun z ↦ z.im ^ t
this : Fintype (SL(2, ℤ) ⧸ Γ)
C : ℝ
hC : ∀ (τ : ℍ), ‖∑ c, ‖f' τ c‖‖ ≤ C * max τ.im (1 / τ.im) ^ t
τ : ℍ
⊢ ‖f τ‖ ≤ ∑ x, ‖Quotient.lift (fun g ↦ f (g⁻¹ • τ)) ⋯ x‖
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
h :
  ∀ (a b c d u v : ℂ),
    c * ↑z + d ≠ 0 →
      (u * ((a * ↑z + b) / (c * ↑z + d)) + v) ^ (-k) =
        (c * ↑z + d) ^ k * ((u * a + v * c) * ↑z + (u * b + v * d)) ^ (-k)
⊢ (↑(i 0) *
          ((↑((algebraMap ℤ ℝ) (↑A 0 0)) * ↑z + ↑((algebraMap ℤ ℝ) (↑A 0 1))) /
            (↑((algebraMap ℤ ℝ) (↑A 1 0)) * ↑z + ↑((algebraMap ℤ ℝ) (↑A 1 1)))) +
        ↑(i 1)) ^
      (-k) =
    (↑(↑(SpecialLinearGroup.toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) A)) 1 0) * ↑z +
          ↑(↑(SpecialLinearGroup.toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) A)) 1 1)) ^
        k *
      (↑(i 0 * ↑A 0 0 + i 1 * ↑A 1 0) * ↑z + ↑(i 0 * ↑A 0 1 + i 1 * ↑A 1 1)) ^ (-k)

Tactic:
simpa using

Goal state after:
k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
h :
  ∀ (a b c d u v : ℂ),
    c * ↑z + d ≠ 0 →
      (u * ((a * ↑z + b) / (c * ↑z + d)) + v) ^ (-k) =
        (c * ↑z + d) ^ k * ((u * a + v * c) * ↑z + (u * b + v * d)) ^ (-k)
⊢ ((↑(i 0) * ((↑(↑A 0 0) * ↑z + ↑(↑A 0 1)) / (↑(↑A 1 0) * ↑z + ↑(↑A 1 1))) + ↑(i 1)) ^ k)⁻¹ =
    (↑(↑A 1 0) * ↑z + ↑(↑A 1 1)) ^ k *
      (((↑(i 0) * ↑(↑A 0 0) + ↑(i 1) * ↑(↑A 1 0)) * ↑z + (↑(i 0) * ↑(↑A 0 1) + ↑(i 1) * ↑(↑A 1 1))) ^ k)⁻¹
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
hk : 0 ≤ 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✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
g : SL(2, ℤ)
⊢ (fun τ ↦ ‖petersson k (⇑f ∣[k] g) (⇑f' ∣[k] g) τ‖) =O[atImInfty] fun z ↦ z.im ^ k

Tactic:
simpa using

Goal state after:
k : ℤ
hk : 0 ≤ 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✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
g : SL(2, ℤ)
⊢ (fun τ ↦ ‖(⇑f ∣[k] g) τ‖ * ‖(⇑f' ∣[k] g) τ‖ * τ.im ^ k) =O[atImInfty] fun z ↦ z.im ^ k
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
this : (f ∘ ↑ofComplex) =O[I∞] (1 ∘ ↑ofComplex)
z : ℂ
hz : z ∈ Complex.im ⁻¹' Ioi 0
⊢ DifferentiableAt ℂ (f ∘ ↑ofComplex) z

Tactic:
simpa using

Goal state after:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
this : (f ∘ ↑ofComplex) =O[I∞] (1 ∘ ↑ofComplex)
z : ℂ
hz : z ∈ Complex.im ⁻¹' Ioi 0
⊢ DifferentiableAt ℂ (f ∘ ↑ofComplex) z
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: case e'_7
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
this : (f ∘ ↑ofComplex) =O[I∞] (1 ∘ ↑ofComplex)
x✝ : ℍ
⊢ f x✝ - valueAtInfty f =
    ((fun z ↦ (f ∘ ↑ofComplex) z - Periodic.cuspFunction h (f ∘ ↑ofComplex) 0) ∘ UpperHalfPlane.coe) x✝

Tactic:
simpa using

Goal state after:
case e'_7
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
this : (f ∘ ↑ofComplex) =O[I∞] (1 ∘ ↑ofComplex)
x✝ : ℍ
⊢ valueAtInfty f = Periodic.cuspFunction h (f ∘ ↑ofComplex) 0
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hf : IsZeroAtImInfty f
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
⊢ f =O[atImInfty] fun τ ↦ rexp (-2 * π * τ.im / h)

Tactic:
simpa using

Goal state after:
h : ℝ
f : ℍ → ℂ
hf : IsZeroAtImInfty f
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
⊢ f =O[atImInfty] fun τ ↦ rexp (-(2 * π * τ.im) / h)
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst✝ : ModularFormClass F Γ k
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
n : ℕ
t : ℝ
ht : 0 < t
u : ℝ
⊢ 0 < (↑u + ↑t * I).im

Tactic:
simpa using

Goal state after:
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst✝ : ModularFormClass F Γ k
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
n : ℕ
t : ℝ
ht : 0 < t
u : ℝ
⊢ 0 < t
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: k : ℤ
F : Type u_1
inst✝⁴ : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
f : F
inst✝³ : ModularFormClass F Γ k
inst✝² : Γ.HasDetPlusMinusOne
inst✝¹ : DiscreteTopology ↥Γ
inst✝ : Fact (IsCusp OnePoint.infty Γ)
hf : IsZeroAtImInfty ⇑f
⊢ ∃ c > 0, ⇑f =O[atImInfty] fun τ ↦ rexp (-c * τ.im)

Tactic:
simpa using

Goal state after:
k : ℤ
F : Type u_1
inst✝⁴ : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
f : F
inst✝³ : ModularFormClass F Γ k
inst✝² : Γ.HasDetPlusMinusOne
inst✝¹ : DiscreteTopology ↥Γ
inst✝ : Fact (IsCusp OnePoint.infty Γ)
hf : IsZeroAtImInfty ⇑f
⊢ ∃ c, 0 < c ∧ ⇑f =O[atImInfty] fun τ ↦ rexp (-(c * τ.im))
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✝¹ : ModularFormClass F Γ k
inst✝ : CuspFormClass F' Γ k
⊢ ∃ C, ∀ (τ : ℍ), ‖petersson k (⇑f) (⇑f') τ‖ ≤ C

Tactic:
simpa using

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✝¹ : ModularFormClass F Γ k
inst✝ : CuspFormClass F' Γ k
⊢ ∃ C, ∀ (τ : ℍ), ‖petersson k (⇑f) (⇑f') τ‖ ≤ C
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f g : ℂ → ℂ
hfcts : ContinuousAt (Periodic.cuspFunction h f) 0
hgcts : ContinuousAt (Periodic.cuspFunction h g) 0
⊢ Periodic.cuspFunction h (f * g) 0 = Periodic.cuspFunction h f 0 * Periodic.cuspFunction h g 0

Tactic:
by
  rw [Periodic.cuspFunction, update_self]
  exact (Periodic.tendsto_nhds_zero hfcts).mul (Periodic.tendsto_nhds_zero hgcts) |>.limUnder_eq

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

Goal state before:
pp: k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : 2 < ↑k
p_sum : Summable fun x ↦ ‖↑x‖ ^ (-k)
K : Set ℍ
hK : IsCompact K
A B : ℝ
hB : 0 < B
HABK : K ⊆ verticalStrip A B
p : ↑(gammaSet N 1 a)
z : ℍ
hz : z ∈ verticalStrip A B
⊢ ‖eisSummand k (↑p) z‖ ≤ r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-↑k) * ‖↑p‖ ^ (-k)

Tactic:
simpa using

Goal state after:
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : 2 < ↑k
p_sum : Summable fun x ↦ ‖↑x‖ ^ (-k)
K : Set ℍ
hK : IsCompact K
A B : ℝ
hB : 0 < B
HABK : K ⊆ verticalStrip A B
p : ↑(gammaSet N 1 a)
z : ℍ
hz : z ∈ verticalStrip A B
⊢ ‖↑(↑p 0) * ↑z + ↑(↑p 1)‖ ^ (-↑k) ≤ r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-↑k) * ‖↑p‖ ^ (-↑k)
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
⊢ qExpansion h (-f) = -qExpansion h f

Tactic:
simpa using

Goal state after:
h : ℝ
f : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
⊢ qExpansion h (-f) = -qExpansion h f
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
⊢ AnalyticAt ℂ (cuspFunction h (-g)) 0

Tactic:
simpa using

Goal state after:
h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
⊢ AnalyticAt ℂ (cuspFunction h g) 0
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
hg' : AnalyticAt ℂ (cuspFunction h (-g)) 0
⊢ qExpansion h (f - g) = qExpansion h f - qExpansion h g

Tactic:
simpa using

Goal state after:
h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
hg' : AnalyticAt ℂ (cuspFunction h (-g)) 0
⊢ qExpansion h (f + -g) = qExpansion h f + -qExpansion h g
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: case mpr
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
H : f = 0
⊢ qExpansion h f = 0

Tactic:
simpa using

Goal state after:
case mpr
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
H : f = 0
⊢ qExpansion h 0 = 0
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
inst✝ : Γ.HasDetPlusMinusOne
⊢ qExpansion h ⇑1 = 1

Tactic:
simp [qExpansion_one]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ},
    z ∈ 𝒟 →
      g • z ∈ 𝒟 →
        ↑g 1 0 = 0 →
          0 ≤ ↑g 1 1 → (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
hd : ¬0 ≤ ↑g 1 1
⊢ ↑(-g) 1 0 = 0

Tactic:
simpa using

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ},
    z ∈ 𝒟 →
      g • z ∈ 𝒟 →
        ↑g 1 0 = 0 →
          0 ≤ ↑g 1 1 → (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
hd : ¬0 ≤ ↑g 1 1
⊢ ↑g 1 0 = 0