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

Goal state before:
pp: case e'_5
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ↑x ^ (-s)) t
h₄ : ∀ (n : ℕ), ∑ k ∈ Icc 0 n, f k = ∑ k ∈ Icc 1 n, f k
hO : (fun n ↦ ∑ k ∈ Icc 0 n, f k) =O[atTop] fun n ↦ ↑n ^ r
⊢ ∫ (a : ℝ) in Set.Ioi 1, s * ((∑ k ∈ Icc 1 ⌊a⌋₊, f k) * ↑a ^ (-(s + 1))) =
    0 - ∫ (t : ℝ) in Set.Ioi 1, deriv (fun x ↦ ↑x ^ (-s)) t * ∑ k ∈ Icc 0 ⌊t⌋₊, f k

Tactic:
zero_sub,

Goal state after:
case e'_5
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ↑x ^ (-s)) t
h₄ : ∀ (n : ℕ), ∑ k ∈ Icc 0 n, f k = ∑ k ∈ Icc 1 n, f k
hO : (fun n ↦ ∑ k ∈ Icc 0 n, f k) =O[atTop] fun n ↦ ↑n ^ r
⊢ ∫ (a : ℝ) in Set.Ioi 1, s * ((∑ k ∈ Icc 1 ⌊a⌋₊, f k) * ↑a ^ (-(s + 1))) =
    -∫ (t : ℝ) in Set.Ioi 1, deriv (fun x ↦ ↑x ^ (-s)) t * ∑ k ∈ Icc 0 ⌊t⌋₊, f k
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: a b c : ℕ
hb0 : 0 < b
hc : a / b ≤ c
x : ℕ
⊢ x ∈ Ico 1 (a / b).succ ↔ x ∈ {x ∈ Ico 1 c.succ | x * b ≤ a}

Tactic:
have : x * b ≤ a → x ≤ c := fun h => le_trans (by rwa [le_div_iff_mul_le hb0]) hc

Goal state after:
a b c : ℕ
hb0 : 0 < b
hc : a / b ≤ c
x : ℕ
this : x * b ≤ a → x ≤ c
⊢ x ∈ Ico 1 (a / b).succ ↔ x ∈ {x ∈ Ico 1 c.succ | x * b ≤ a}
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: a b c : ℕ
hb0 : 0 < b
hc : a / b ≤ c
x : ℕ
⊢ x ∈ Ico 1 (a / b).succ ↔ x ∈ {x ∈ Ico 1 c.succ | x * b ≤ a}

Tactic:
have : x * b ≤ a → x ≤ c := fun h => le_trans (by rwa [le_div_iff_mul_le hb0]) hc
        simp [le_div_iff_mul_le hb0]; tauto

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

Goal state before:
pp: p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  #({x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p}) =
    #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
x : ℕ × ℕ
hx : x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ
hpq : x.2 * p ≤ x.1 * q
hqp : x.1 * q ≤ x.2 * p
⊢ False

Tactic:
have hxp : x.1 < p := lt_of_le_of_lt (b := p / 2)
      (by grind) (Nat.div_lt_self hp.1.pos (by decide))

Goal state after:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  #({x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p}) =
    #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
x : ℕ × ℕ
hx : x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ
hpq : x.2 * p ≤ x.1 * q
hqp : x.1 * q ≤ x.2 * p
hxp : x.1 < p
⊢ False
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
ht₂ : ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - ↑t * l‖ / t < ε
⊢ ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * ↑t‖ < ε * t

Tactic:
mul_comm,

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₂ : ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * ↑t‖ / t < ε
⊢ ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * ↑t‖ < ε * t
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
b : ℕ
⊢ {0, 1, -1} = ↑(MonoidHom.mrange ↑SignType.castHom)

Tactic:
rw [Set.pair_comm]
    exact (SignType.range_eq SignType.castHom).symm

Goal state after:
Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x y : R
hy : x * ϖ ^ n = ϖ ^ (n + 1) * y
⊢ x ∈ I

Tactic:
mul_comm,

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x y : R
hy : ϖ ^ n * x = ϖ ^ (n + 1) * y
⊢ x ∈ I
Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
⊢ (R ⧸ I) ≃ₗ[R] ↥(I ^ n) ⧸ I • ⊤

Tactic:
have : I = LinearMap.ker (f.comp g) := by
    ext x
    simp only [LinearMap.codRestrict, LinearMap.pow_mulRight, LinearMap.mulRight_apply,
      LinearMap.mem_ker, LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply,
      Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero, Submodule.mem_smul_top_iff, smul_eq_mul,
      f, g]
    constructor <;> intro hx
    · exact Submodule.mul_mem_mul hx hϖ
    · rw [← pow_succ', hI, Ideal.span_singleton_pow, Ideal.mem_span_singleton] at hx
      obtain ⟨y, hy⟩ := hx
      rw [mul_comm, pow_succ, mul_assoc, mul_right_inj' (pow_ne_zero _ _)] at hy
      · rw [hI, Ideal.mem_span_singleton]
        exact ⟨y, hy⟩
      · contrapose h'
        rw [hI, h', Ideal.span_singleton_eq_bot]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
this : I = (f ∘ₗ g).ker
⊢ (R ⧸ I) ≃ₗ[R] ↥(I ^ n) ⧸ I • ⊤
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha2 : 2 * a % 2 = 0
⊢ (if b % 8 = 3 ∨ b % 8 = 5 then -J(a | b) else J(a | b)) = J(2 | b) * J(a | b)

Tactic:
jacobiSym.at_two (Nat.odd_iff.mpr hb2),

Goal state after:
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha2 : 2 * a % 2 = 0
⊢ (if b % 8 = 3 ∨ b % 8 = 5 then -J(a | b) else J(a | b)) = χ₈ ↑b * J(a | b)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: m n : ℕ
hm : Odd m
hn : Odd n
⊢ (-1) ^ (m / 2 * (n / 2) * 2) = 1

Tactic:
mul_comm,

Goal state after:
m n : ℕ
hm : Odd m
hn : Odd n
⊢ (-1) ^ (2 * (m / 2 * (n / 2))) = 1
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: m n : ℕ
hm : Odd m
hn : Odd n
⊢ (-1) ^ (m / 2 * (n / 2)) = qrSign n m

Tactic:
neg_one_pow hn hm,

Goal state after:
m n : ℕ
hm : Odd m
hn : Odd n
⊢ (-1) ^ (m / 2 * (n / 2)) = (-1) ^ (n / 2 * (m / 2))
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: K : Type u_1
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
ϖ : ↥𝒪[K]
h : Irreducible ϖ
⊢ ↑𝓂[K] = Metric.closedBall 0 ‖ϖ‖

Tactic:
by
  simp [h.maximalIdeal_eq_setOfPred_le_v_coe, Set.ext_iff, ← NNReal.coe_le_coe]

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
⊢ ωb * ω = 1

Tactic:
mul_comm,

Goal state after:
q : ℕ
⊢ ω * ωb = 1
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
⊢ (1 - α) * (1 + α) = -2

Tactic:
mul_comm,

Goal state after:
q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
⊢ (1 + α) * (1 - α) = -2
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case h
p' : ℕ
k : ℤ
h : ω ^ 2 ^ (p' + 1) + 1 = ω ^ 2 ^ p' * ↑((2 ^ (p' + 2) - 1) * k)
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1

Tactic:
mul_comm,

Goal state after:
case h
p' : ℕ
k : ℤ
h : ω ^ 2 ^ (p' + 1) + 1 = ↑((2 ^ (p' + 2) - 1) * k) * ω ^ 2 ^ p'
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ
p : ℕ
hp : 2 ≤ p
n✝ : ℕ
a✝ : ↑(sModNat (2 ^ p - 1) n✝) = sMod p n✝
this : 2 ^ 2 ≤ 2 ^ p
⊢ ↑(sModNat (2 ^ p - 1) (n✝ + 1)) = sMod p (n✝ + 1)

Tactic:
grind [sModNat, sMod, Int.emod_eq_add_self_emod]

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

Goal state before:
pp: g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := ↑g
A₂ : Matrix (Fin 2) (Fin 2) ℚ := ↑g⁻¹
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x✝ : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : ⟨y, hy⟩ ∈ Γ(a₁ * a₂ * M)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
hz_coe : z.map Int.cast = A₁ * y.map Int.cast * A₂
this : ↑z.det = 1 * ↑y.det
⊢ z.det = 1

Tactic:
one_mul,

Goal state after:
g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := ↑g
A₂ : Matrix (Fin 2) (Fin 2) ℚ := ↑g⁻¹
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x✝ : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : ⟨y, hy⟩ ∈ Γ(a₁ * a₂ * M)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
hz_coe : z.map Int.cast = A₁ * y.map Int.cast * A₂
this : ↑z.det = ↑y.det
⊢ z.det = 1
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: ι : Type u_1
k : ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
s : Finset ι
this : k * ↑(#s) = ∑ i ∈ s, k
⊢ (∏ i ∈ s, f i) ∣[∑ i ∈ s, k] g = |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#s) - 1) • ∏ i ∈ s, f i ∣[k] g

Tactic:
exact prod_slash_sum_weights

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

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
a b : SL(2, ℤ)
hab : (QuotientGroup.leftRel (Subgroup.comap (mapGL ℝ) 𝒢)) a b
⊢ ⟦⟨(mapGL ℝ) a⁻¹ • ∞, ⋯⟩⟧ = ⟦⟨(mapGL ℝ) b⁻¹ • ∞, ⋯⟩⟧

Tactic:
QuotientGroup.leftRel_apply

Goal state after:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
a b : SL(2, ℤ)
hab : a⁻¹ * b ∈ Subgroup.comap (mapGL ℝ) 𝒢
⊢ ⟦⟨(mapGL ℝ) a⁻¹ • ∞, ⋯⟩⟧ = ⟦⟨(mapGL ℝ) b⁻¹ • ∞, ⋯⟩⟧
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
x : ℂ
inst✝ : Γ.HasDetOne
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
g : GL (Fin 2) ℝ
hg : g • OnePoint.infty = c✝
⊢ IsBoundedAtImInfty ((SlashInvariantForm.const x).toFun ∣[0] g)

Tactic:
simpa only [coe_const, slash_def, SlashInvariantForm.toFun_eq_coe,
      Function.const_apply, neg_zero, zpow_zero] using! atImInfty.const_boundedAtFilter _

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
⊢ Tendsto (fun g ↦ (lcRow0 cd) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) cofinite (cocompact ℝ)

Tactic:
let mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => of ![![t, (-(1 : ℤ) : ℝ)], (↑) ∘ cd]

Goal state after:
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t ↦ of ![![t, -↑1], Int.cast ∘ cd]
⊢ Tendsto (fun g ↦ (lcRow0 cd) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) cofinite (cocompact ℝ)
Module: Mathlib.NumberTheory.ModularForms.Petersson

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝⁴ : FunLike F ℍ ℂ
inst✝³ : FunLike F' ℍ ℂ
k : ℤ
g : GL (Fin 2) ℝ
τ : ℍ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.HasDetPlusMinusOne
inst✝¹ : SlashInvariantFormClass F Γ k
f : F
inst✝ : SlashInvariantFormClass F' Γ k
f' : F'
hg : g ∈ Γ
| ‖1 * (σ g) (petersson k (⇑f) (⇑f') (g • τ))‖

Tactic:
one_mul,

Goal state after:
F : Type u_1
F' : Type u_2
inst✝⁴ : FunLike F ℍ ℂ
inst✝³ : FunLike F' ℍ ℂ
k : ℤ
g : GL (Fin 2) ℝ
τ : ℍ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.HasDetPlusMinusOne
inst✝¹ : SlashInvariantFormClass F Γ k
f : F
inst✝ : SlashInvariantFormClass F' Γ k
f' : F'
hg : g ∈ Γ
| ‖(σ g) (petersson k (⇑f) (⇑f') (g • τ))‖
Module: Mathlib.NumberTheory.ModularForms.Petersson

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝⁴ : FunLike F ℍ ℂ
inst✝³ : FunLike F' ℍ ℂ
k : ℤ
g : GL (Fin 2) ℝ
τ : ℍ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.HasDetPlusMinusOne
inst✝¹ : SlashInvariantFormClass F Γ k
f : F
inst✝ : SlashInvariantFormClass F' Γ k
f' : F'
hg : g ∈ Γ
⊢ ‖petersson k (⇑f) (⇑f') (g • τ)‖ = ‖petersson k (⇑f) (⇑f') τ‖

Tactic:
by
  conv_rhs => rw [← slash_action_eq f _ hg, ← slash_action_eq f' _ hg, petersson_slash,
    Subgroup.HasDetPlusMinusOne.abs_det hg, Complex.ofReal_one, one_zpow, one_mul, norm_σ]

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 : ℕ
R : ℝ
hR : 0 < R
hR' : R < 1
this :
  ∮ (z : ℂ) in C(0, R), (1 / (z - 0) ^ (n + 1)) • cuspFunction h f z =
    2 * ↑π * Complex.I * ((↑n.factorial)⁻¹ * iteratedDeriv n (cuspFunction h f) 0)
⊢ (PowerSeries.coeff n) (qExpansion h f) =
    (2 * ↑π * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)

Tactic:
mul_comm,

Goal state after:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
R : ℝ
hR : 0 < R
hR' : R < 1
this :
  ∮ (z : ℂ) in C(0, R), (1 / (z - 0) ^ (n + 1)) • cuspFunction h f z =
    (↑n.factorial)⁻¹ * iteratedDeriv n (cuspFunction h f) 0 * (2 * ↑π * Complex.I)
⊢ (PowerSeries.coeff n) (qExpansion h f) =
    (2 * ↑π * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)
Module: Mathlib.NumberTheory.ModularForms.Bounds

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

Tactic:
QuotientGroup.leftRel_apply

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 τ
τ : ℍ
g h : SL(2, ℤ)
hgh : g⁻¹ * h ∈ Γ
⊢ ∃ j ∈ Γ, h = g * j
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
h : z ∈ 𝒟ᵒ
⊢ |z.re| < 1 / 2

Tactic:
exact h.2

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

Goal state before:
pp: h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
n✝ : ℕ
⊢ (PowerSeries.coeff n✝) (qExpansion h (f * g)) = (PowerSeries.coeff n✝) (qExpansion h f * qExpansion h g)

Tactic:
simp only [qExpansion_coeff, cuspFunction_mul hf.continuousAt hg.continuousAt,
    iteratedDeriv_mul hf.contDiffAt hg.contDiffAt, Finset.mul_sum, PowerSeries.coeff_mul,
    Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, Nat.succ_eq_add_one]

Goal state after:
h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
n✝ : ℕ
⊢ ∑ i ∈ Finset.range (n✝ + 1),
      (↑n✝.factorial)⁻¹ *
        (↑(n✝.choose i) * iteratedDeriv i (cuspFunction h f) 0 * iteratedDeriv (n✝ - i) (cuspFunction h g) 0) =
    ∑ x ∈ Finset.range (n✝ + 1),
      (↑x.factorial)⁻¹ * iteratedDeriv x (cuspFunction h f) 0 *
        ((↑(n✝ - x).factorial)⁻¹ * iteratedDeriv (n✝ - x) (cuspFunction h g) 0)
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

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

Tactic:
simpa using! summable_norm_pow_mul_geometric_of_norm_lt_one k hr

Goal state after:
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: case h₂
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
b : ℕ+
i : ℕ
hi : i ∈ (↑b).divisors
⊢ ‖r‖ ^ (i * (↑b / i)) ≤ ‖r‖ ^ ↑b

Tactic:
mul_comm,

Goal state after:
case h₂
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
b : ℕ+
i : ℕ
hi : i ∈ (↑b).divisors
⊢ ‖r‖ ^ (↑b / i * i) ≤ ‖r‖ ^ ↑b
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
this : ∑' (c : ℕ+ × ℕ+), ↑↑c.2 ^ k * r ^ (↑c.1 * ↑c.2) = ∑' (e : ℕ+), ↑((σ k) ↑e) * r ^ ↑e
⊢ ∑' (d : ℕ+) (c : ℕ+), ↑↑c ^ k * r ^ (↑d * ↑c) = ∑' (e : ℕ+), ↑((σ k) ↑e) * r ^ ↑e

Tactic:
← (summable_prod_mul_pow k hr).tsum_prod

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
this : ∑' (c : ℕ+ × ℕ+), ↑↑c.2 ^ k * r ^ (↑c.1 * ↑c.2) = ∑' (e : ℕ+), ↑((σ k) ↑e) * r ^ ↑e
⊢ ∑' (p : ℕ+ × ℕ+), ↑↑p.2 ^ k * r ^ (↑p.1 * ↑p.2) = ∑' (e : ℕ+), ↑((σ k) ↑e) * r ^ ↑e
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) = ∑' (n : ℕ+), (r ^ ↑m) ^ ↑n

Tactic:
mul_comm,

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 ^ (↑m * ↑n) = ∑' (n : ℕ+), (r ^ ↑m) ^ ↑n
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 + (2 * z.re + 1) ≤ 1
this : normSq (↑z + 1) = normSq ↑z + (2 * z.re + 1)
⊢ 0 ≤ 2 * z.re + 1

Tactic:
linarith [(neg_le_abs _).trans hz.2]

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

Goal state before:
pp: h : ℝ
z : ℂ
this : 𝕢 h = cexp ∘ fun x ↦ 2 * ↑π * I / ↑h * x
⊢ logDeriv cexp (2 * ↑π * I / ↑h * z) * (2 * ↑π * I / ↑h) = 2 * ↑π * I / ↑h

Tactic:
simp [logDeriv_exp]

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

Goal state before:
pp: γ : SL(2, ℤ)
⊢ G2 ∣[2] γ = G2 - D2 γ

Tactic:
have : γ ∈ Subgroup.closure {S, T} := by simp [SpecialLinearGroup.SL2Z_generators]

Goal state after:
γ : SL(2, ℤ)
this : γ ∈ Subgroup.closure {S, T}
⊢ G2 ∣[2] γ = G2 - D2 γ
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: z : ℍ
hE2 :
  E2 { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * (↑z ^ 2)⁻¹ =
    E2 z - 6 / ↑π ^ 2 * 2⁻¹ * (2 * ↑π * I * ↑(↑ModularGroup.S 1 0) / ↑z)
⊢ (↑z ^ 2)⁻¹ * (↑π * I / 12) * E2 { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } =
    ↑z ^ (-1 / 2) / 2 * (↑z).sqrt⁻¹ + ↑π * I / 12 * E2 z

Tactic:
mul_comm,

Goal state after:
z : ℍ
hE2 :
  E2 { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * (↑z ^ 2)⁻¹ =
    E2 z - 6 / ↑π ^ 2 * 2⁻¹ * (2 * ↑π * I * ↑(↑ModularGroup.S 1 0) / ↑z)
⊢ E2 { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * ((↑z ^ 2)⁻¹ * (↑π * I / 12)) =
    ↑z ^ (-1 / 2) / 2 * (↑z).sqrt⁻¹ + ↑π * I / 12 * E2 z
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℤ
f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
c : OnePoint ℝ
hc : IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range
γ : SL(2, ℤ)
a✝ : (Matrix.SpecialLinearGroup.mapGL ℝ) γ • ∞ = c
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
BoundedAtFilter

Goal state after:
k : ℤ
f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
c : OnePoint ℝ
hc : IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range
γ : SL(2, ℤ)
a✝ : (Matrix.SpecialLinearGroup.mapGL ℝ) γ • ∞ = c
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
⊢ 1 / (↑m * ↑z + ↑a) - 1 / (↑m * ↑z + ↑b) = (↑b - ↑a) * (1 / ((↑m * ↑z + ↑a) * (↑m * ↑z + ↑b)))

Tactic:
← one_div_mul_sub_mul_one_div_eq_one_div_add_one_div

Goal state after:
z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
⊢ 1 / (↑m * ↑z + ↑a) * (↑m * ↑z + ↑b - (↑m * ↑z + ↑a)) * (1 / (↑m * ↑z + ↑b)) =
    (↑b - ↑a) * (1 / ((↑m * ↑z + ↑a) * (↑m * ↑z + ↑b)))

case ha
z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
⊢ ↑m * ↑z + ↑a ≠ 0

case hb
z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
⊢ ↑m * ↑z + ↑b ≠ 0
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℍ
h0 : ↑τ ≠ 0
h1 : (-I * ↑τ) ^ (1 / 2) ≠ 0
⊢ jacobiTheta₂ 0 (-↑τ)⁻¹ = 1 * jacobiTheta₂ 0 (-1 / ↑τ)

Tactic:
one_mul,

Goal state after:
τ : ℍ
h0 : ↑τ ≠ 0
h1 : (-I * ↑τ) ^ (1 / 2) ≠ 0
⊢ jacobiTheta₂ 0 (-↑τ)⁻¹ = jacobiTheta₂ 0 (-1 / ↑τ)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
⊢ z = g • z

Tactic:
by
  rcases eq_one_or_neg_one_of_mem_fdo_mem_fdo hz hg with rfl | rfl <;> simp

Goal state after:
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‖ * ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ = 2 * ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖

Tactic:
Complex.norm_two

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

Goal state before:
pp: x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
a : ℝ≥0
ha : 0 < a
this : 1 < ‖↑x‖ ^ 2 + ↑a ^ 2 + 2 * ↑a * x.im
⊢ 1 < ‖↑{ coe := ↑x + ↑↑a * Complex.I, coe_im_pos := ⋯ }‖

Tactic:
rw [← one_lt_normSq_iff]

Goal state after:
x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
a : ℝ≥0
ha : 0 < a
this : 1 < ‖↑x‖ ^ 2 + ↑a ^ 2 + 2 * ↑a * x.im
⊢ 1 < normSq ↑{ coe := ↑x + ↑↑a * Complex.I, coe_im_pos := ⋯ }
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
⊢ 1 - 2 * ↑k / ↑(bernoulli k) * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑↑n =
    1 +
      (riemannZeta ↑k)⁻¹ * (-2 * ↑π * I) ^ k / ↑(k - 1)! * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑↑n

Tactic:
rw [eisensteinSeries_coeff_identity hk2 (by grind), neg_mul, ← sub_eq_add_neg]

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

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F 𝒢 k
q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ
τ : ℍ
h h' : ↥ℋ
hhh' : (QuotientGroup.leftRel (𝒢.subgroupOf ℋ)) h h'
⊢ ∃ g ∈ 𝒢, ↑h' = ↑h * g

Tactic:
QuotientGroup.leftRel_apply

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F 𝒢 k
q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ
τ : ℍ
h h' : ↥ℋ
hhh' : h⁻¹ * h' ∈ 𝒢.subgroupOf ℋ
⊢ ∃ g ∈ 𝒢, ↑h' = ↑h * g