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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
B : BadChar N
this : riemannZeta (-2) = 0
⊢ Function.update (fun s ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1) (-2) = 0

Tactic:
Function.update_of_ne (mod_cast (by lia : (-2 : ℤ) ≠ 1)),

Goal state after:
N : ℕ
inst✝ : NeZero N
B : BadChar N
this : riemannZeta (-2) = 0
⊢ riemannZeta (-2) * LFunction B.χ (-2) = 0
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_6
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x) =
    -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x) + 1 / 0 * (fourier 0) ↑x

Tactic:
div_zero,

Goal state after:
case e'_6
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x) = -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x) + 0 * (fourier 0) ↑x
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| I ^ (2 * k)

Tactic:
rw [pow_mul, I_sq]

Goal state after:
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| (-1) ^ k
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
U : Set ℂ := {t | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
hUp : IsPreconnected U
⊢ AnalyticOnNhd ℂ F U

Tactic:
refine DifferentiableOn.analyticOnNhd
      (fun t ht ↦ DifferentiableAt.differentiableWithinAt ?_) hUo

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
U : Set ℂ := {t | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
hUp : IsPreconnected U
t : ℂ
ht : t ∈ U
⊢ DifferentiableAt ℂ F t
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
U : Set ℂ := {t | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
hUp : IsPreconnected U
hF : AnalyticOnNhd ℂ F U
⊢ AnalyticOnNhd ℂ G U

Tactic:
refine DifferentiableOn.analyticOnNhd
      (fun t ht ↦ DifferentiableAt.differentiableWithinAt ?_) hUo

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
U : Set ℂ := {t | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
hUp : IsPreconnected U
hF : AnalyticOnNhd ℂ F U
t : ℂ
ht : t ∈ U
⊢ DifferentiableAt ℂ G t
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: case pos
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
h : χ ^ 2 = 1 ∧ s = 1
⊢ LFunction χ s ≠ 0

pp: case neg
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
h : ¬(χ ^ 2 = 1 ∧ s = 1)
⊢ LFunction χ s ≠ 0

Tactic:
· exact h.2 ▸ LFunction_apply_one_ne_zero_of_quadratic h.1 <| hχs.neg_resolve_right h.2

Goal state after:
case neg
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
h : ¬(χ ^ 2 = 1 ∧ s = 1)
⊢ LFunction χ s ≠ 0
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
h : ¬(χ ^ 2 = 1 ∧ s = 1)
| 1 + ↑s.im * I

Tactic:
mul_comm

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
h : ¬(χ ^ 2 = 1 ∧ s = 1)
| 1 + I * ↑s.im
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
⊢ LSeries f s = s * ∫ (t : ℝ) in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-(s + 1))

Tactic:
by
  rw [← LSeriesSummable_congr' s (f := fun n ↦ if n = 0 then 0 else f n)
    (by filter_upwards [eventually_ne_atTop 0] with n h using if_neg h)] at hS
  have (n : _) : ∑ k ∈ Icc 1 n, (if k = 0 then 0 else f k) = ∑ k ∈ Icc 1 n, f k :=
    Finset.sum_congr rfl fun k hk ↦ by rw [if_neg (zero_lt_one.trans_le (mem_Icc.mp hk).1).ne']
  rw [← LSeries_congr fun _ ↦ if_neg _, LSeries_eq_mul_integral_aux (if_pos rfl) hr hs hS] <;>
  simp_all

Goal state after:
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
⊢ LocallyIntegrableOn (fun t ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume

Tactic:
mul_comm

Goal state after:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
⊢ LocallyIntegrableOn (fun t ↦ ↑t ^ (-↑s - 1) * ∑ k ∈ Icc 1 ⌊t⌋₊, f k) (Set.Ici 1) volume
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
h_lim' : Tendsto (fun t ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / ↑t) atTop (𝓝 l)
t : ℝ
ht₁ : 0 < t
⊢ dist ((∑ k ∈ Icc 1 ⌊t⌋₊, f k) / ↑t) l < ε → ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * ↑t‖ < ε * t

Tactic:
ht₂

Goal state after:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
h_lim' : Tendsto (fun t ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / ↑t) atTop (𝓝 l)
t : ℝ
ht₁ : 0 < t
ht₂ : dist ((∑ k ∈ Icc 1 ⌊t⌋₊, f k) / ↑t) l < ε
⊢ ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * ↑t‖ < ε * t
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case mpr
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : Finite 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
hp' : v ↑p < 1
n : ℕ
hn : ‖↑p‖ ^ n < ε
hF : Finite (↥𝒪[K] ⧸ 𝓂[K] ^ n)
this : {y | v ↑y ≤ v ↑p ^ n} = Metric.closedBall 0 (‖p‖ ^ n)
⊢ ∀ (i : ↥𝒪[K] ⧸ 𝓂[K] ^ n), Metric.closedBall (Quotient.out i) (‖↑p‖ ^ n) ⊆ ⋃ y, Metric.ball y.out ε

Tactic:
intro

Goal state after:
case mpr
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : Finite 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
hp' : v ↑p < 1
n : ℕ
hn : ‖↑p‖ ^ n < ε
hF : Finite (↥𝒪[K] ⧸ 𝓂[K] ^ n)
this : {y | v ↑y ≤ v ↑p ^ n} = Metric.closedBall 0 (‖p‖ ^ n)
i✝ : ↥𝒪[K] ⧸ 𝓂[K] ^ n
⊢ Metric.closedBall (Quotient.out i✝) (‖↑p‖ ^ n) ⊆ ⋃ y, Metric.ball y.out ε
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case inr.inr.inr
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
this✝ : ∀ (z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
hxy : x < y
this : (Set.Icc y⁻¹ x⁻¹).Finite
h : 1 < x
⊢ Set.Icc x y ⊆ Set.Icc x⁻¹⁻¹ y⁻¹⁻¹

Tactic:
intro

Goal state after:
case inr.inr.inr
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
this✝ : ∀ (z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
hxy : x < y
this : (Set.Icc y⁻¹ x⁻¹).Finite
h : 1 < x
a✝ : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
⊢ a✝ ∈ Set.Icc x y → a✝ ∈ Set.Icc x⁻¹⁻¹ y⁻¹⁻¹
Module: Mathlib.NumberTheory.LocalField.Basic

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : ValuativeRel K
inst✝¹ : TopologicalSpace K
inst✝ : IsNonarchimedeanLocalField K
this✝ : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K
⊢ IsTopologicalDivisionRing K

Tactic:
infer_instance

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case ind
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
⊢ J(a | b) =
    if hb0 : b = 0 then 1
    else
      if x : b % 2 = 0 then
        if a % 2 = 0 then 0
        else
          have this := ⋯;
          fastJacobiSym a (b / 2)
      else if b = 1 then 1 else if hab : a % ↑b = 0 then 0 else fastJacobiSymAux (a % ↑b).natAbs b false ⋯

Tactic:
split_ifs with hb0 hb2 ha2 hb1 hab

Goal state after:
case pos
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : b = 0
⊢ J(a | b) = 1

case pos
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : b % 2 = 0
ha2 : a % 2 = 0
⊢ J(a | b) = 0

case neg
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : b % 2 = 0
ha2 : ¬a % 2 = 0
⊢ J(a | b) =
    have this := ⋯;
    fastJacobiSym a (b / 2)

case pos
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : b = 1
⊢ J(a | b) = 1

case pos
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : a % ↑b = 0
⊢ J(a | b) = 0

case neg
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : ¬a % ↑b = 0
⊢ J(a | b) = fastJacobiSymAux (a % ↑b).natAbs b false ⋯
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case mp
K : Type u_1
Γ₀ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Valued K Γ₀
inst✝ : v.RankOne
h : ProperSpace K
⊢ IsCompact (Metric.closedBall 0 1)

pp: case mpr
K : Type u_1
Γ₀ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Valued K Γ₀
inst✝ : v.RankOne
h : IsCompact (Metric.closedBall 0 1)
⊢ ProperSpace K

Tactic:
· exact isCompact_closedBall 0 1

Goal state after:
case mpr
K : Type u_1
Γ₀ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Valued K Γ₀
inst✝ : v.RankOne
h : IsCompact (Metric.closedBall 0 1)
⊢ ProperSpace K
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ
q✝ i q k : ℕ
ih : ∀ (b : ℕ), sModNatTR.go q k b = sModNatAux b q k
b : ℕ
⊢ sModNatTR.go q (k + 1) b = sModNatAux b q (k + 1)

Tactic:
sModNatTR.go,

Goal state after:
case succ
q✝ i q k : ℕ
ih : ∀ (b : ℕ), sModNatTR.go q k b = sModNatAux b q k
b : ℕ
⊢ sModNatTR.go q k ((b ^ 2 + (q - 2)) % q) = sModNatAux b q (k + 1)
Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete

Goal state before:
pp: case mp
G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
a✝ : Nontrivial G
g : G
⊢ DiscreteTopology ↥(zpowers g)

Tactic:
infer_instance

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

Goal state before:
pp: n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
⊢ DiscreteTopology ↥(mapGL ℝ).range

Tactic:
infer_instance

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
k : ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
⊢ (∏ i, f i) ∣[k * ↑(Fintype.card ι)] g = |↑(Matrix.GeneralLinearGroup.det g)| ^ (Fintype.card ι - 1) • ∏ i, f i ∣[k] g

Tactic:
have : 0 < Fintype.card ι := Fintype.card_pos

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
k : ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
this : 0 < Fintype.card ι
⊢ (∏ i, f i) ∣[k * ↑(Fintype.card ι)] g = |↑(Matrix.GeneralLinearGroup.det g)| ^ (Fintype.card ι - 1) • ∏ i, f i ∣[k] g
Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
k : ℤ
inst✝¹ : Γ.HasDetOne
inst✝ : SlashInvariantFormClass F Γ k
f : F
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
z : ℍ
this : f (γ • z) = f z * denom γ ↑z ^ k
⊢ f z * (↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k = (↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k * f z

Tactic:
mul_comm

Goal state after:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
k : ℤ
inst✝¹ : Γ.HasDetOne
inst✝ : SlashInvariantFormClass F Γ k
f : F
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
z : ℍ
this : f (γ • z) = f z * denom γ ↑z ^ k
⊢ (↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k * f z = (↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k * f z
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
hsp : (map (mapGL ℝ) Γ).strictPeriods = AddSubgroup.zmultiples 1
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples 1)

Tactic:
infer_instance

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

Goal state before:
pp: k : ℤ
f f' : ℍ → ℂ
g : GL (Fin 2) ℝ
τ : ℍ
D : ℝ := |↑(Matrix.GeneralLinearGroup.det g)|
hD : ↑D ≠ 0
j : ℂ := denom g ↑τ
⊢ ↑D ^ (k - 2 + k) * (starRingEnd ℂ) ((σ g) (f (g • τ))) * (σ g) (f' (g • τ)) *
      (↑τ.im ^ k * ↑(Complex.normSq j) ^ (-k)) =
    ↑D ^ (k - 2) * ((starRingEnd ℂ) ((σ g) (f (g • τ))) * (σ g) (f' (g • τ)) * (↑D * ↑τ.im / ↑(Complex.normSq j)) ^ k)

Tactic:
rw [div_zpow, mul_zpow, zpow_neg, div_eq_mul_inv, zpow_add₀ hD]
    ring

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
this : Tendsto (fun g ↦ (↑g • z).re) cofinite (cocompact ℝ)
⊢ Tendsto (fun g ↦ |(↑g • z).re|) cofinite atTop

Tactic:
exact tendsto_norm_cocompact_atTop.comp this

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
hR1 : R < 1
⊢ (2 * ↑π * Complex.I)⁻¹ *
      ∫ (θ : ℝ) in 0 * (2 * π / h)..h * (2 * π / h),
        deriv (circleMap 0 R) θ • (cuspFunction h f (circleMap 0 R θ) / circleMap 0 R θ ^ (n + 1)) =
    1 / ↑h * ∫ (u : ℝ) in 0..h, 1 / 𝕢 h (↑u + ↑t * ↑I) ^ n * f { coe := ↑u + ↑t * ↑I, coe_im_pos := ⋯ }

Tactic:
simp_rw [← intervalIntegral.smul_integral_comp_mul_right, real_smul, ← mul_assoc,
    ← intervalIntegral.integral_const_mul]

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
⊢ ∫ (x : ℝ) in 0..h,
      (2 * ↑π * Complex.I)⁻¹ * ↑(2 * π / h) *
        deriv (circleMap 0 R) (x * (2 * π / h)) •
          (cuspFunction h f (circleMap 0 R (x * (2 * π / h))) / circleMap 0 R (x * (2 * π / h)) ^ (n + 1)) =
    ∫ (x : ℝ) in 0..h, 1 / ↑h * (1 / 𝕢 h (↑x + ↑t * ↑I) ^ n * f { coe := ↑x + ↑t * ↑I, coe_im_pos := ⋯ })
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 : |(↑z + ↑(↑g 1 1)).re| ≤ 1
⊢ |↑g 1 1| ≤ 1

Tactic:
rw [add_re, intCast_re, add_comm, coe_re] at 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
⊢ |↑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
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ

Tactic:
have hz' : ‖(z : ℂ)‖ = 1 :=
    le_antisymm (by simpa [denom, hc, hd] using hg') (one_le_normSq_iff.mp hz.1)

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 = 0
hb : ↑g 0 1 = -1
hz' : ‖↑z‖ = 1
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
n : ℕ+
⊢ ∑' (c : ↥(↑n).divisorsAntidiagonal), ↑(↑c).2 ^ k * r ^ ((↑c).1 * (↑c).2) =
    (∑ x ∈ (↑n).divisors, ↑(↑n / x) ^ k) * r ^ ↑n

Tactic:
simpa [tsum_fintype, Finset.sum_mul,
    (n : ℕ).divisorsAntidiagonal.sum_attach fun x : ℕ × ℕ ↦ x.2 ^ k * r ^ (x.1 * x.2),
    sum_divisorsAntidiagonal fun x y ↦ y ^ k * r ^ (x * y)]
      using Finset.sum_congr rfl fun i hi ↦ by rw [Nat.mul_div_cancel' (dvd_of_mem_divisors hi)]

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

Goal state before:
pp: case h
K : Set ℂ
hK : K ⊆ Metric.ball 0 1
⊢ IsCompact K → HasProdUniformlyOn (fun n q ↦ 1 + -q ^ (n + 1)) (fun q ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1))) K

Tactic:
hcK

Goal state after:
case h
K : Set ℂ
hK : K ⊆ Metric.ball 0 1
hcK : IsCompact K
⊢ HasProdUniformlyOn (fun n q ↦ 1 + -q ^ (n + 1)) (fun q ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1))) K
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

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

Tactic:
have hn0 : (n : ℂ) ≠ 0 := by aesop
        have hn1 : (n : ℂ) + 1 ≠ 0 := by norm_cast; grind
        simp [δ, h, hb, hn]
        grind

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

Goal state before:
pp: z : ℍ
⊢ logDeriv η (-(↑z)⁻¹) * deriv (fun x ↦ -x⁻¹) ↑z = (↑z ^ 2)⁻¹ * logDeriv η (-(↑z)⁻¹)

pp: case hf
z : ℍ
⊢ DifferentiableAt ℂ η (-(↑z)⁻¹)

pp: case hg
z : ℍ
⊢ DifferentiableAt ℂ (fun x ↦ -x⁻¹) ↑z

Tactic:
mul_comm

Goal state after:
z : ℍ
⊢ deriv (fun x ↦ -x⁻¹) ↑z * logDeriv η (-(↑z)⁻¹) = (↑z ^ 2)⁻¹ * logDeriv η (-(↑z)⁻¹)

case hf
z : ℍ
⊢ DifferentiableAt ℂ η (-(↑z)⁻¹)

case hg
z : ℍ
⊢ DifferentiableAt ℂ (fun x ↦ -x⁻¹) ↑z
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: case e_a
z : ℍ
⊢ 𝕢 24 ↑z ^ 24 = 𝕢 1 ↑z

pp: case e_a
z : ℍ
⊢ (∏' (n : ℕ), (1 - eta_q n ↑z)) ^ 24 = ∏' (n : ℕ), (1 - eta_q n ↑z) ^ 24

Tactic:
· simp [Periodic.qParam, ← exp_nsmul, nsmul_eq_mul, Nat.cast_ofNat]
    grind

Goal state after:
case e_a
z : ℍ
⊢ (∏' (n : ℕ), (1 - eta_q n ↑z)) ^ 24 = ∏' (n : ℕ), (1 - eta_q n ↑z) ^ 24
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 k))) →
      (∀ᶠ (n : ℂ) in 𝓝 0, ∀ (k : ℕ), ‖-n ^ (k + 1)‖ ≤ (1 / 2) ^ (k + 1)) →
        Tendsto (fun n ↦ ∏' (k : ℕ), (1 + -n ^ (k + 1))) (𝓝 0) (𝓝 (∏' (k : ℕ), (1 + 0 k)))
⊢ Tendsto (fun q ↦ ∏' (n : ℕ), (1 - q ^ (n + 1))) (𝓝 0) (𝓝 1)

Tactic:
simp only [Pi.zero_apply, norm_neg, norm_pow, add_zero, tprod_one] at this

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.LevelOne.DimensionFormula

Goal state before:
pp: case h
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ Submodule.Quotient.mk ((PowerSeries.coeff 0) (qExpansion 1 ⇑f) • E hk) = Submodule.Quotient.mk f

Tactic:
Submodule.Quotient.eq,

Goal state after:
case h
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ (PowerSeries.coeff 0) (qExpansion 1 ⇑f) • E hk - f ∈ cuspFormSubmodule (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
this : ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
⊢ 2 * (rexp (-π * τ.im) / (1 - rexp (-π * τ.im))) = rexp (-π * τ.im) / (1 - rexp (-π * τ.im)) * 2

Tactic:
mul_comm

Goal state after:
τ : ℂ
hτ : 0 < τ.im
this : ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
⊢ rexp (-π * τ.im) / (1 - rexp (-π * τ.im)) * 2 = rexp (-π * τ.im) / (1 - rexp (-π * τ.im)) * 2
Module: Mathlib.NumberTheory.ModularForms.ProperlyDiscontinuous

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
⊢ ProperlyDiscontinuousSMul ↥(SpecialLinearGroup.mapGL ℝ).range ℍ

Tactic:
infer_instance

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

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : 𝒢.IsArithmetic
inst✝ : 𝒢.HasDetOne
f : ModularForm 𝒢 0
⊢ ModularFormClass (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 0) (Matrix.SpecialLinearGroup.mapGL ℝ).range 0

Tactic:
infer_instance

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

Goal state before:
pp: case e'_5
Γ : 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
t : ℝ
ht : 0 < t
this :
  HasSum
    (fun m ↦ (PowerSeries.coeff m) (qExpansion (h Γ) ⇑f) * Function.Periodic.qParam (h Γ) ↑(↑ofComplex (I * ↑t)) ^ m)
    (f (↑ofComplex (I * ↑t)))
n : ℕ
⊢ (if 2 * ↑n / h Γ = 0 then 0 else (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) * ↑(rexp (-π * (2 * ↑n / h Γ) * t))) =
    if n = 0 then 0
    else (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) * Function.Periodic.qParam (h Γ) ↑(↑ofComplex (I * ↑t)) ^ n

pp: case e'_6.e'_6
Γ : 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
t : ℝ
ht : 0 < t
this :
  HasSum
    (fun m ↦ (PowerSeries.coeff m) (qExpansion (h Γ) ⇑f) * Function.Periodic.qParam (h Γ) ↑(↑ofComplex (I * ↑t)) ^ m)
    (f (↑ofComplex (I * ↑t)))
⊢ (weakFEPair hk f).f₀ =
    (PowerSeries.coeff 0) (qExpansion (h Γ) ⇑f) * Function.Periodic.qParam (h Γ) ↑(↑ofComplex (I * ↑t)) ^ 0

Tactic:
· rcases Nat.eq_zero_or_pos n with rfl | hn
      · simp
      · simp [hn.ne', Function.Periodic.qParam, ofComplex_apply_eq_ite, ht, ← exp_nat_mul]
        grind [I_sq]

Goal state after:
case e'_6.e'_6
Γ : 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
t : ℝ
ht : 0 < t
this :
  HasSum
    (fun m ↦ (PowerSeries.coeff m) (qExpansion (h Γ) ⇑f) * Function.Periodic.qParam (h Γ) ↑(↑ofComplex (I * ↑t)) ^ m)
    (f (↑ofComplex (I * ↑t)))
⊢ (weakFEPair hk f).f₀ =
    (PowerSeries.coeff 0) (qExpansion (h Γ) ⇑f) * Function.Periodic.qParam (h Γ) ↑(↑ofComplex (I * ↑t)) ^ 0