mathlib-initiative/mathlib-tactics huggingface dataset:
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 • τ ∈ 𝒟
⊢ 0 < (g • τ).im ^ t

Tactic:
by positivity

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 : ℝ
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 • τ).im ^ t ≤ F
hg : g • τ ∈ 𝒟
⊢ 0 ≤ ‖f τ‖ / (g • τ).im ^ t

Tactic:
by positivity

Goal state after:
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
⊢ 0 < 2 * π * t

Tactic:
by positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: case inr
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k < 0
f : F
hf : ⇑f = Function.const ℍ (UpperHalfPlane.cuspFunction 1 (⇑f) 0)
hf₀ : UpperHalfPlane.cuspFunction 1 (⇑f) 0 = 0
⊢ ⇑f = 0

Tactic:
hf,

Goal state after:
case inr
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k < 0
f : F
hf : ⇑f = Function.const ℍ (UpperHalfPlane.cuspFunction 1 (⇑f) 0)
hf₀ : UpperHalfPlane.cuspFunction 1 (⇑f) 0 = 0
⊢ Function.const ℍ (UpperHalfPlane.cuspFunction 1 (⇑f) 0) = 0
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : CuspFormClass F Γ k
f : F
C : ℝ
τ : ℍ
hC : ‖petersson k (⇑f) (⇑f) τ‖ ≤ C
⊢ 0 ≤ ‖f τ‖

Tactic:
by positivity

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

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : CuspFormClass F Γ k
f : F
C : ℝ
τ : ℍ
hC : ‖petersson k (⇑f) (⇑f) τ‖ ≤ C
⊢ 0 ≤ √C / τ.im ^ (↑k / 2)

Tactic:
by positivity

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
⊢ 0 ≤ ↑k

Tactic:
by positivity

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst✝ : ModularFormClass F Γ ↑k
hC : ‖petersson (↑k) (⇑f) (⇑f) τ‖ ≤ C * max τ.im (1 / τ.im) ^ ↑k
⊢ 0 ≤ ‖petersson (↑k) (⇑f) (⇑f) τ‖ / max τ.im (1 / τ.im) ^ ↑k

Tactic:
by positivity

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst✝ : ModularFormClass F Γ ↑k
hC : ‖petersson (↑k) (⇑f) (⇑f) τ‖ ≤ C * max τ.im (1 / τ.im) ^ ↑k
⊢ 0 < max τ.im (1 / τ.im) ^ ↑k

Tactic:
by positivity

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst✝ : ModularFormClass F Γ ↑k
hC : ‖f τ‖ ^ 2 ≤ C * (max τ.im (1 / τ.im) ^ ↑k / ‖↑τ.im ^ ↑k‖)
hC' : 0 ≤ C
h : 0 < ‖↑τ.im ^ ↑k‖
⊢ 0 ≤ ‖f τ‖

Tactic:
by positivity

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst✝ : ModularFormClass F Γ ↑k
hC : ‖f τ‖ ^ 2 ≤ C * (max τ.im (1 / τ.im) ^ ↑k / ‖↑τ.im ^ ↑k‖)
hC' : 0 ≤ C
h : 0 < ‖↑τ.im ^ ↑k‖
⊢ 0 ≤ √C * max 1 (1 / τ.im ^ ↑k)

Tactic:
by positivity

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

Goal state before:
pp: F : Type u_1
inst✝ : FunLike F ℍ ℂ
h : ℝ
f : F
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h ⇑f) 0
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
⊢ HasFPowerSeriesOnBall (cuspFunction h ⇑f) (qExpansionFormalMultilinearSeries h f) 0 1

Tactic:
have h1 := (hasFPowerSeriesOnBall_cuspFunction hh hfanalytic hf).hasFPowerSeriesAt
  have h2 : HasFPowerSeriesAt (cuspFunction h f) (qExpansionFormalMultilinearSeries h f) 0 := by
    simpa [qExpansionFormalMultilinearSeries, qExpansion_coeff, div_eq_mul_inv, mul_comm]
      using hfanalytic.hasFPowerSeriesAt
  simpa [h1.eq_formalMultilinearSeries h2] using hasFPowerSeriesOnBall_cuspFunction hh hfanalytic hf

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst✝ : ModularFormClass F Γ ↑k
hC : ‖f τ‖ ^ 2 ≤ C * (max τ.im (1 / τ.im) ^ ↑k / ‖↑τ.im ^ ↑k‖)
hC' : 0 ≤ C
h✝ : 0 < ‖↑τ.im ^ ↑k‖
t : NNReal
h : τ.im = ↑t
ht : 0 < t
⊢ 0 ≤ ‖↑(t ^ k)‖₊

Tactic:
by positivity

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

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun r ↦ r⁻¹) ∘ Nat.cast) n → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
⊢ 0 < 1 / ↑n

Tactic:
by positivity

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

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun r ↦ r⁻¹) ∘ Nat.cast) n → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
⊢ 0 ≤ h

Tactic:
by positivity

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

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F✝ : Type u_2
inst✝¹ : FunLike F✝ ℍ ℂ
inst✝ : ModularFormClass F✝ Γ k
f : F✝
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun r ↦ r⁻¹) ∘ Nat.cast) n → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
F : ℝ → ℝ := fun x ↦ ‖1 / ↑h * (1 / 𝕢 h (↑x + 1 / ↑n * I) ^ n * f { coe := ↑x + 1 / ↑n * I, coe_im_pos := ⋯ })‖
⊢ 0 ≤ ↑n ^ e

Tactic:
by positivity

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr.inr
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 : ℤ := ⋯
hgz : g = T ^ (-1)
hre : (g • z).re = ↑b + z.re
hb : b = -1
⊢ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2

Tactic:
rw [hgz, zpow_neg_one, eq_self_iff_true, true_or, true_and]

Goal state after:
case inr.inr
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
hgz : g = T ^ (-1)
hre : (g • z).re = ↑b + z.re
hb : b = -1
⊢ z.re = 1 / 2
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
a : (x : ℕ+) × ↥(↑x).divisorsAntidiagonal
⊢ 0 ≤ ‖↑(↑a.snd).2 ^ k * r ^ ((↑a.snd).1 * (↑a.snd).2)‖

Tactic:
by positivity

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

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F✝ : Type u_2
inst✝¹ : FunLike F✝ ℍ ℂ
inst✝ : ModularFormClass F✝ Γ k
f : F✝
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this✝ : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun r ↦ r⁻¹) ∘ Nat.cast) n → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
F : ℝ → ℝ := fun x ↦ ‖1 / ↑h * (1 / 𝕢 h (↑x + 1 / ↑n * I) ^ n * f { coe := ↑x + 1 / ↑n * I, coe_im_pos := ⋯ })‖
hne : ‖↑n ^ e‖ = ↑n ^ e
this : ∀ (x : ℝ), F x ≤ 1 / h * (1 / Real.exp (-2 * Real.pi / h)) * (C * ↑n ^ e)
⊢ 0 ≤ h

Tactic:
by positivity

Goal state after:
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)
τ : ℍ
hτ : τ.im ≤ 1
⊢ 0 ≤ (τ.im ^ k)⁻¹

Tactic:
by positivity

Goal state after:
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)
τ : ℍ
hτ : τ.im ≤ 1
⊢ 0 < τ.im ^ k

Tactic:
by positivity

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

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : CuspFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), ‖f τ‖ ≤ C / τ.im ^ (↑k / 2)
τ : ℍ
⊢ 0 ≤ τ.im ^ (-(↑k / 2))

Tactic:
by positivity

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hf : Summable f (symmetricIcc ℤ)
hs : Function.Even f
⊢ Tendsto (fun x ↦ ‖f x‖) atTop (𝓝 0)

Tactic:
obtain ⟨L, hL⟩ := hf

Goal state after:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : HasSum f L (symmetricIcc ℤ)
⊢ Tendsto (fun x ↦ ‖f x‖) atTop (𝓝 0)
Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
⊢ 0 ≤ x

Tactic:
by positivity

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

Goal state before:
pp: z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ ∑'[symmetricIcc ℤ] (m : ℤ), e2Summand m z = t

Tactic:
show t = t + 0 by ring,

Goal state after:
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ ∑'[symmetricIcc ℤ] (m : ℤ), e2Summand m z = t + 0
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)
q : ℂ
hq : q ∈ Metric.ball 0 (1 / 2)
⊢ ∀ (k : ℕ), ‖q‖ ^ (k + 1) ≤ (1 / 2) ^ (k + 1)

Tactic:
k

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)
q : ℂ
hq : q ∈ Metric.ball 0 (1 / 2)
k : ℕ
⊢ ‖q‖ ^ (k + 1) ≤ (1 / 2) ^ (k + 1)
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:
zpow_ofNat,

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.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ ∑' (n : ℤ), 1 / (↑z + ↑n) ^ (k + 1) = (-2 * ↑π * I) ^ (k + 1) / ↑k ! * ∑' (n : ℕ), ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n

Tactic:
have : (-1) ^ k * k ! * ∑' n : ℤ, 1 / ((z : ℂ) + n) ^ (k + 1) =
    -(2 * π * I) ^ (k + 1) * ∑' n : ℕ, n ^ k * cexp (2 * π * I * z) ^ n := by
    rw [← iteratedDerivWithin_tsum_exp_aux_eq hk z,
      ← iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow hk (by simpa using z.2)]
    exact iteratedDerivWithin_congr (fun x hx ↦ by (simpa using pi_mul_cot_pi_q_exp ⟨x, hx⟩))
      (by simpa using z.2)

Goal state after:
k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  (-1) ^ k * ↑k ! * ∑' (n : ℤ), 1 / (↑z + ↑n) ^ (k + 1) =
    -(2 * ↑π * I) ^ (k + 1) * ∑' (n : ℕ), ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n
⊢ ∑' (n : ℤ), 1 / (↑z + ↑n) ^ (k + 1) = (-2 * ↑π * I) ^ (k + 1) / ↑k ! * ∑' (n : ℕ), ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case inr.inl
k : ℤ
hk_nonneg : 0 ≤ k
hk_even : Even k
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) < Cardinal.aleph0

Tactic:
lift k to ℕ using hk_nonneg
    rw [dimension_level_one k (mod_cast hk_even)]
    split_ifs <;> exact_mod_cast Cardinal.natCast_lt_aleph0

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case left
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
⊢ 1 < normSq ↑x

Tactic:
one_lt_normSq_iff,

Goal state after:
case left
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
⊢ 1 < ‖↑x‖
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: y : ℝ
z : ℂ
hz : z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
⊢ 0 ≤ √((1 / 2) ^ 2 + y ^ 2)

Tactic:
by positivity

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: y : ℝ
z : ℂ
hz : z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
⊢ 0 ≤ (1 / 2) ^ 2 + y ^ 2

Tactic:
by positivity

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: y : ℝ
z : ℂ
hz : z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
⊢ 0 ≤ z.re ^ 2 + z.im ^ 2

Tactic:
by positivity

Goal state after:
Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup

Goal state before:
pp: Γ : Type u_1
α : Type u_2
inst✝² : Group Γ
inst✝¹ : TopologicalSpace α
inst✝ : SMul Γ α
S : Subgroup Γ
⊢ ProperlyDiscontinuousSMul (↥S) α ↔
    ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ S ∧ (g • K ∩ L).Nonempty}.Finite

Tactic:
by
  rw [properlyDiscontinuousSMul_iff]
  congr! with K L hK hL
  convert! injOn_subtype_val (s := {m : S | (m • K ∩ L).Nonempty}) |>.bijOn_image.finite_iff_finite
  ext g
  simp [Set.subtype_smul_set, and_comm]

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
r : ℝ
hpos : 0 < s.re
hs : r + 1 < s.re
hΛ : Λ hk f s = mellin (fun t ↦ (weakFEPair hk f).f t - (weakFEPair hk f).f₀) s
hcoeff : (fun n ↦ (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f)) =O[atTop] fun n ↦ ↑n ^ r
hh : 0 < h Γ
hΓ : h Γ ∈ Γ.strictPeriods
x✝ : ℕ
⊢ 0 ≤ 2 * ↑x✝ / h Γ

Tactic:
by positivity

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hk : k * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hd' : d ≠ 0
this : {v | (valuation K v) ((algebraMap R K) d) < 1}.Finite
v : HeightOneSpectrum R
hv : v ∈ Support R k
⊢ v ∈ {v | (valuation K v) ((algebraMap R K) d) < 1}

Tactic:
apply_fun v.valuation K at hk

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hd' : d ≠ 0
this : {v | (valuation K v) ((algebraMap R K) d) < 1}.Finite
v : HeightOneSpectrum R
hv : v ∈ Support R k
hk : (valuation K v) (k * (algebraMap R K) ↑(n, ⟨d, hd⟩).2) = (valuation K v) ((algebraMap R K) (n, ⟨d, hd⟩).1)
⊢ v ∈ {v | (valuation K v) ((algebraMap R K) d) < 1}
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: w✝ : ℤ
⊢ (1 + (w✝ * 4 + w✝ ^ 2 * 4)) % 4 = 1

Tactic:
← add_mul,

Goal state after:
w✝ : ℤ
⊢ (1 + (w✝ + w✝ ^ 2) * 4) % 4 = 1
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hxy : p ∣ x + y
hx : ¬p ∣ x
n : ℕ
hn : Odd n
⊢ padicValNat p (x ^ n + y ^ n) = padicValNat p (x + y) + padicValNat p n

Tactic:
by
  rcases y with - | y
  · contradiction
  rw [← Nat.cast_inj (R := ℕ∞), Nat.cast_add]
  iterate 3 rw [padicValNat_eq_emultiplicity]
  · exact Nat.emultiplicity_pow_add_pow hp.out hp1 hxy hx hn
  · exact (Odd.pos hn).ne'
  · simp
  · exact (Nat.lt_add_left _ (pow_pos y.succ_pos _)).ne'

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : polarSpace K
⊢ ((fun w ↦ (x✝.1 ↑w, x✝.2 w)) ∈ Set.univ.pi fun i ↦ Complex.polarCoord.target) ↔
    (x✝.1 ∈ Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0) ∧ x✝.2 ∈ Set.univ.pi fun x ↦ Set.Ioo (-π) π

Tactic:
Set.mem_univ_pi,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : polarSpace K
⊢ (∀ (i : { w // w.IsComplex }), (x✝.1 ↑i, x✝.2 i) ∈ Complex.polarCoord.target) ↔
    (∀ (i : InfinitePlace K), x✝.1 i ∈ if i.IsReal then Set.univ else Set.Ioi 0) ∧
      ∀ (i : { w // w.IsComplex }), x✝.2 i ∈ Set.Ioo (-π) π
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
a : ↑(integerSet K)
⊢ ¬(mixedEmbedding K) ((algebraMap (𝓞 K) K) ⋯.choose) = (mixedEmbedding K) ((algebraMap (𝓞 K) K) 0)

Tactic:
map_zero,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
a : ↑(integerSet K)
⊢ ¬(mixedEmbedding K) ((algebraMap (𝓞 K) K) ⋯.choose) = 0
Module: Mathlib.NumberTheory.NumberField.Completion.LiesOverInstances

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst✝ : w.LiesOver v
x : K
h : (algebraMap K v.Completion) x = { toCompletion := ↑(WithAbs.toAbs (↑v) x) }
⊢ ((algebraMap K w.Completion) x).toCompletion =
    { toCompletion := ↑((algebraMap (WithAbs ↑v) (WithAbs ↑w)) (WithAbs.toAbs (↑v) x)) }.toCompletion

Tactic:
Completion.algebraMap_toCompletion,

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst✝ : w.LiesOver v
x : K
h : (algebraMap K v.Completion) x = { toCompletion := ↑(WithAbs.toAbs (↑v) x) }
⊢ (algebraMap K (↑w).Completion) x =
    { toCompletion := ↑((algebraMap (WithAbs ↑v) (WithAbs ↑w)) (WithAbs.toAbs (↑v) x)) }.toCompletion
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
W₀ : InfinitePlace K := (equivInfinitePlace K).symm w₀
f : { w // w ≠ W₀ } ≃ { w // w ≠ w₀ } := (equivInfinitePlace K).subtypeEquiv ⋯
g : Fin (rank K) ≃ { w // w ≠ W₀ } := ((finCongr ⋯).trans (equivFinRank ↥K⁺)).trans f.symm
i w : { w // w ≠ w₀ }
⊢ ↑(↑(f.symm w)).mult * Real.log (↑(f.symm w) ((algebraMap (𝓞 K) K) ↑(realFundSystem K (g.symm (f.symm i))))) =
    2 * Matrix.of (fun i ↦ (logEmbedding ↥K⁺) (Additive.ofMul (fundSystem (↥K⁺) ((equivFinRank ↥K⁺).symm i)))) i w

Tactic:
show f.symm w = (equivInfinitePlace K).symm w.1 by rfl,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
W₀ : InfinitePlace K := (equivInfinitePlace K).symm w₀
f : { w // w ≠ W₀ } ≃ { w // w ≠ w₀ } := (equivInfinitePlace K).subtypeEquiv ⋯
g : Fin (rank K) ≃ { w // w ≠ W₀ } := ((finCongr ⋯).trans (equivFinRank ↥K⁺)).trans f.symm
i w : { w // w ≠ w₀ }
⊢ ↑((equivInfinitePlace K).symm ↑w).mult *
      Real.log (((equivInfinitePlace K).symm ↑w) ((algebraMap (𝓞 K) K) ↑(realFundSystem K (g.symm (f.symm i))))) =
    2 * Matrix.of (fun i ↦ (logEmbedding ↥K⁺) (Additive.ofMul (fundSystem (↥K⁺) ((equivFinRank ↥K⁺).symm i)))) i w
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ regOfFamily (realFundSystem K) = 2 ^ rank K * regulator ↥K⁺

Tactic:
by
  classical
  let W₀ := (equivInfinitePlace K).symm w₀
  let f : {w : InfinitePlace K // w ≠ W₀} ≃ {w : InfinitePlace K⁺ // w ≠ w₀} :=
    (equivInfinitePlace K).subtypeEquiv fun w ↦ by rw [not_iff_not, Equiv.eq_symm_apply]
  let g := ((finCongr (units_rank_eq_units_rank K).symm).trans (equivFinRank K⁺)).trans f.symm
  rw [show (2 : ℝ) ^ rank K = |∏ w : {w : InfinitePlace K⁺ // w ≠ w₀}, 2| by
    rw [Finset.prod_const, abs_pow, abs_of_pos zero_lt_two, ← units_rank_eq_units_rank K, rank]
    simp]
  rw [regulator_eq_regOfFamily_fundSystem, regOfFamily_eq_det _ W₀ g.symm, regOfFamily_eq_det',
    ← abs_mul, ← Matrix.det_mul_column, ← Matrix.det_reindex_self f, Matrix.reindex_apply]
  congr; ext i w
  rw [Matrix.submatrix_apply, Matrix.of_apply, Matrix.of_apply,
    show f.symm w = (equivInfinitePlace K).symm w.1 by rfl,
    show algebraMap (𝓞 K) K _ = algebraMap K⁺ K _ by rfl, equivInfinitePlace_symm_apply]
  simp [f, g]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ 2 ^ rank K ≠ 0

Tactic:
by positivity

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ¬p ∣ exponent θ ↔ Codisjoint (span {↑p}) (comap (algebraMap ℤ (𝓞 K)) (conductor ℤ θ))

Tactic:
← IsCoatom.not_le_iff_codisjoint,

Goal state after:
K : Type u_1
inst✝¹ : Field K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ¬p ∣ exponent θ ↔ ¬comap (algebraMap ℤ (𝓞 K)) (conductor ℤ θ) ≤ span {↑p}

K : Type u_1
inst✝¹ : Field K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ IsCoatom (span {↑p})