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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * I * completedLFunction (𝓕 Φ) s

Tactic:
suffices ∑ x, Φ x * completedSinZeta (toAddCircle x) s = I * completedLFunction (𝓕 Φ) s by
    simp only [completedLFunction_def_odd hΦ, neg_sub, completedHurwitzZetaOdd_one_sub, this,
      mul_assoc]
  -- reduce to equality with un-completed L-functions:
  suffices ∑ x, Φ x * sinZeta (toAddCircle x) s = I * LFunction (𝓕 Φ) s by
    have hs' : 0 < re (s + 1) := by simp only [add_re, one_re]; linarith
    simpa only [sinZeta, ← mul_div_assoc, ← sum_div, div_left_inj' (Gammaℝ_ne_zero_of_re_pos hs'),
      LFunction_eq_completed_div_gammaFactor_odd (dft_odd_iff.mpr hΦ)]
  -- now calculate:
  calc ∑ x, Φ x * sinZeta (toAddCircle x) s
  _ = (∑ x, Φ x * expZeta (toAddCircle x) s) / (2 * I)
      - (∑ x, Φ x * expZeta (toAddCircle (-x)) s) / (2 * I) := by
    simp only [sinZeta_eq, ← mul_div_assoc, mul_sub, sub_div, sum_sub_distrib, sum_div, map_neg]
  _ = (∑ x, Φ (-x) * expZeta (toAddCircle (-x)) s) / (_) - (_) := by
    congrm ?_ / _ - _
    exact (Fintype.sum_equiv (.neg _) _ _ fun x ↦ by rfl).symm
  _ = -I⁻¹ * LFunction (𝓕 Φ) s := by
    simp only [hΦ _, neg_mul, sum_neg_distrib, LFunction_dft Φ (.inl hΦ.map_zero)]
    ring
  _ = I * LFunction (𝓕 Φ) s := by rw [inv_I, neg_neg]

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

Goal state before:
pp: case neg
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : ¬IsUnit ↑n
⊢ 0 ≤
    3 * (-log (1 - 1 ↑n * ↑n ^ (-↑x))).re + 4 * (-log (1 - χ ↑n * ↑n ^ (-(↑x + I * ↑y)))).re +
      (-log (1 - χ ↑n ^ 2 * ↑n ^ (-(↑x + 2 * I * ↑y)))).re

Tactic:
· simp only [MulChar.map_nonunit _ hn', zero_mul, sub_zero, log_one, neg_zero, zero_re, mul_zero,
      neg_add_rev, add_zero, pow_two, le_refl]

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

Goal state before:
pp: q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / ↑n ≤ F₀ n
⊢ Summable F₀

Tactic:
have hF₀ (p : Nat.Primes) : F₀ p.val = 0 := by
    simp only [p.prop, ↓reduceIte, zero_div, F₀]

Goal state after:
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / ↑n ≤ F₀ n
hF₀ : ∀ (p : Nat.Primes), F₀ ↑p = 0
⊢ Summable F₀
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

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

Tactic:
not_and_or,

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
hs' : s = 1 + I * ↑s.im
⊢ LFunction χ s ≠ 0
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ (fun s ↦ L (fun n ↦ ↑(residueClass a n)) s - (↑q.totient)⁻¹ / (s - 1)) ↑x =
    ↑((fun s ↦ L (fun n ↦ ↑(residueClass a n)) s - (↑q.totient)⁻¹ / (s - 1)) ↑x).re

Tactic:
simp only [sub_re, ofReal_sub]

Goal state after:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ L (fun n ↦ ↑(residueClass a n)) ↑x - (↑q.totient)⁻¹ / (↑x - 1) =
    ↑(L (fun n ↦ ↑(residueClass a n)) ↑x).re - ↑((↑q.totient)⁻¹ / (↑x - 1)).re
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: f : ℕ → ℂ
hf : f ∈ {f | f 0 = 0 ∧ abscissaOfAbsConv f < ⊤}
g : ℕ → ℂ
⊢ g ∈ {f | f 0 = 0 ∧ abscissaOfAbsConv f < ⊤} → LSeries f = LSeries g → f = g

Tactic:
hg

Goal state after:
f : ℕ → ℂ
hf : f ∈ {f | f 0 = 0 ∧ abscissaOfAbsConv f < ⊤}
g : ℕ → ℂ
hg : g ∈ {f | f 0 = 0 ∧ abscissaOfAbsConv f < ⊤}
⊢ LSeries f = LSeries g → f = g
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: ⊢ 1 / 4 ∈ Icc 0 1

Tactic:
· rw [mem_Icc]; constructor
    · linarith
    · linarith

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

Goal state before:
pp: a b c : ℕ
hb0 : 0 < b
hc : a / b ≤ c
x : ℕ
h : x * b ≤ a
⊢ x ≤ a / b

Tactic:
le_div_iff_mul_le hb0

Goal state after:
a b c : ℕ
hb0 : 0 < b
hc : a / b ≤ c
x : ℕ
h : x * b ≤ a
⊢ x * b ≤ a
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: case pos
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
h : IsNontrivial R
H : DenselyOrdered (ValueGroupWithZero R)
⊢ IsDiscrete R

Tactic:
classical
      exfalso
      refine (MonoidWithZeroHom.range_nontrivial
        (ValueGroupWithZero.orderMonoidIso v).toMonoidWithZeroHom).not_subsingleton ?_
      rw [← WithZero.denselyOrdered_set_iff_subsingleton]
      exact (ValueGroupWithZero.embed_strictMono v).denselyOrdered_range

Goal state after:
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
h : Nontrivial (ValueGroupWithZero R)ˣ
H : ¬DenselyOrdered (ValueGroupWithZero R)
⊢ IsDiscrete R

Tactic:
← LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered

Goal state after:
case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
h : Nontrivial (ValueGroupWithZero R)ˣ
H : Nonempty (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ))
⊢ IsDiscrete R
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inr.e_a.e_a
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ J(↑b | a') = J(↑(b % (4 * a)) | a')

Tactic:
· rw [mod_left ↑(b % _), mod_left b, Int.natCast_mod, Int.emod_emod_of_dvd b]
      simp only [ha₂, Nat.cast_mul, ← mul_assoc]
      apply dvd_mul_left

Goal state after:
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
γ : K
hγ : ¬γ = 0
this✝ : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K := isUniformAddGroup_of_addCommGroup
s : Set K
hs : s ∈ nhds 0
hs' : IsCompact s
r : K
hr : r ≠ 0
hr1 : (valuation K) r < 1
H : {x | (valuation K).restrict x ≤ (valuation K).restrict r} ⊆ s
x : K
⊢ 0 < Valued.v.restrict γ

Tactic:
by simp [hγ]

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : ⟨x, hx1✝⟩ ≠ 0
⊢ ∃ b, ⟨x, hx1✝⟩ * b = 1

Tactic:
replace hx2 : x ≠ 0 := by simpa [Subtype.ext_iff] using hx2

Goal state after:
A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
⊢ ∃ b, ⟨x, hx1✝⟩ * b = 1
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Γ : Subgroup (GL (Fin 2) ℝ)
h : Γ.IsArithmetic
g : GL (Fin 2) ℝ
⊢ g ∈ Γ → |↑(GeneralLinearGroup.det g)| = 1

Tactic:
hg

Goal state after:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Γ : Subgroup (GL (Fin 2) ℝ)
h : Γ.IsArithmetic
g : GL (Fin 2) ℝ
hg : g ∈ Γ
⊢ |↑(GeneralLinearGroup.det g)| = 1
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
⊢ ∃ N, N ≠ 0 ∧ ∀ x ∈ Γ(N), g * (mapGL ℚ) x * g⁻¹ ∈ Subgroup.map (mapGL ℚ) Γ(M)

Tactic:
let A₁ := g.1

Goal state after:
g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := ↑g
⊢ ∃ N, N ≠ 0 ∧ ∀ x ∈ Γ(N), g * (mapGL ℚ) x * g⁻¹ ∈ Subgroup.map (mapGL ℚ) Γ(M)
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' : ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod (a₁ * a₂ * M)))) ⟨y, hy⟩) = ↑1
⊢ y.map Int.cast = 1

Tactic:
simpa using! hy'

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

Goal state before:
pp: 𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢' ≤ 𝒢
h𝒢' : 𝒢'.relIndex 𝒢 ≠ 0
c : OnePoint ℝ
x✝ : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
hgp : g.IsParabolic
hgc : g • c = c
n : ℕ
hn : 0 < n
hgn : g ^ n ∈ 𝒢' ⊓ 𝒢
⊢ g ^ n • c = c

Tactic:
rw [Nat.pos_iff_ne_zero] at hn

Goal state after:
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢' ≤ 𝒢
h𝒢' : 𝒢'.relIndex 𝒢 ≠ 0
c : OnePoint ℝ
x✝ : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
hgp : g.IsParabolic
hgc : g • c = c
n : ℕ
hn : n ≠ 0
hgn : g ^ n ∈ 𝒢' ⊓ 𝒢
⊢ g ^ n • c = c
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: case empty
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
x✝ : ℍ
⊢ (1 ∣[0] g) x✝ = (|(↑g).det|⁻¹ • 1) x✝

Tactic:
simp [slash_apply]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h : 𝒢.strictPeriods < 𝒢.periods
u b : R
hu_mem : upperRightHom u ∈ 𝒢 ∨ -upperRightHom u ∈ 𝒢
hu_notMem : upperRightHom u ∉ 𝒢
hb : upperRightHom b ∈ 𝒢 ∨ -upperRightHom b ∈ 𝒢
⊢ upperRightHom b * upperRightHom u ∈ 𝒢 ∨ upperRightHom b ∈ 𝒢

Tactic:
rcases hb with h | h

Goal state after:
case neg.inl
R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h✝ : 𝒢.strictPeriods < 𝒢.periods
u b : R
hu_mem : upperRightHom u ∈ 𝒢 ∨ -upperRightHom u ∈ 𝒢
hu_notMem : upperRightHom u ∉ 𝒢
h : upperRightHom b ∈ 𝒢
⊢ upperRightHom b * upperRightHom u ∈ 𝒢 ∨ upperRightHom b ∈ 𝒢

case neg.inr
R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h✝ : 𝒢.strictPeriods < 𝒢.periods
u b : R
hu_mem : upperRightHom u ∈ 𝒢 ∨ -upperRightHom u ∈ 𝒢
hu_notMem : upperRightHom u ∉ 𝒢
h : -upperRightHom b ∈ 𝒢
⊢ upperRightHom b * upperRightHom u ∈ 𝒢 ∨ upperRightHom b ∈ 𝒢
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
q : ℂ
hq : ‖q‖ < 1
hq1 : q ≠ 0
h1 : 0 < (Periodic.invQParam h q).im
τ : ℍ := { coe := Periodic.invQParam h q, coe_im_pos := h1 }
h2 : Periodic.cuspFunction h (f ∘ ↑ofComplex) q = (f ∘ ↑ofComplex) (Periodic.invQParam h q)
⊢ cuspFunction h f q = f τ

Tactic:
simpa [UpperHalfPlane.ofComplex_apply_of_im_pos h1]
    using! h2

Goal state after:
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 ^ (k - 2) * (σ g) (petersson k (⇑f) (⇑f') (g • τ))‖

Tactic:
one_zpow,

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 ∈ Γ
| ‖1 * (σ g) (petersson k (⇑f) (⇑f') (g • τ))‖
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hp : IsCoprime (↑g 1 0) (↑g 1 1)
nonZ1 : ↑(↑g 1 0) ^ 2 + ↑(↑g 1 1) ^ 2 ≠ 0
this : Int.cast ∘ ↑g 1 ≠ 0
nonZ2 : ↑z * ↑(↑g 1 0) + ↑(↑g 1 1) ≠ 0
H : 1 = ↑(↑g 0 0) * ↑(↑g 1 1) - ↑(↑g 0 1) * ↑(↑g 1 0)
⊢ (↑((algebraMap ℤ ℝ) (↑g 0 0)) * ↑z + ↑((algebraMap ℤ ℝ) (↑g 0 1))) /
      (↑((algebraMap ℤ ℝ) (↑g 1 0)) * ↑z + ↑((algebraMap ℤ ℝ) (↑g 1 1))) =
    ↑((lcRow0 (↑g 1)) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) / (↑(↑g 1 0) ^ 2 + ↑(↑g 1 1) ^ 2) +
      (↑(↑g 1 1) * ↑z - ↑(↑g 1 0)) / ((↑(↑g 1 0) ^ 2 + ↑(↑g 1 1) ^ 2) * (↑(↑g 1 0) * ↑z + ↑(↑g 1 1)))

Tactic:
simp [field]

Goal state after:
g : SL(2, ℤ)
z : ℍ
hp : IsCoprime (↑g 1 0) (↑g 1 1)
nonZ1 : ↑(↑g 1 0) ^ 2 + ↑(↑g 1 1) ^ 2 ≠ 0
this : Int.cast ∘ ↑g 1 ≠ 0
nonZ2 : ↑z * ↑(↑g 1 0) + ↑(↑g 1 1) ≠ 0
H : 1 = ↑(↑g 0 0) * ↑(↑g 1 1) - ↑(↑g 0 1) * ↑(↑g 1 0)
⊢ (↑(↑g 0 0) * ↑z + ↑(↑g 0 1)) * (↑(↑g 1 0) ^ 2 + ↑(↑g 1 1) ^ 2) =
    (↑z * ↑(↑g 1 0) + ↑(↑g 1 1)) * (↑(↑g 0 0) * ↑(↑g 1 0) + ↑(↑g 0 1) * ↑(↑g 1 1)) + (↑z * ↑(↑g 1 1) - ↑(↑g 1 0))
Module: Mathlib.NumberTheory.Modular

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

Tactic:
suffices
    Tendsto (fun g : (fun g : SL(2, ℤ) => g 1) ⁻¹' {p} => ((g : SL(2, ℤ)) • z).re) cofinite
      (cocompact ℝ)
    by exact tendsto_norm_cocompact_atTop.comp this
  have : ((p 0 : ℝ) ^ 2 + (p 1 : ℝ) ^ 2)⁻¹ ≠ 0 := by
    apply inv_ne_zero
    exact mod_cast hp.sq_add_sq_ne_zero
  let f := Homeomorph.mulRight₀ _ this
  let ff := Homeomorph.addRight
    (((p 1 : ℂ) * z - p 0) / (((p 0 : ℂ) ^ 2 + (p 1 : ℂ) ^ 2) * (p 0 * z + p 1))).re
  convert! (f.trans ff).isClosedEmbedding.tendsto_cocompact.comp (tendsto_lcRow0 hp) with _ _ g
  change
    ((g : SL(2, ℤ)) • z).re =
      lcRow0 p ↑(↑g : SL(2, ℝ)) / ((p 0 : ℝ) ^ 2 + (p 1 : ℝ) ^ 2) +
        Complex.re (((p 1 : ℂ) * z - p 0) / (((p 0 : ℂ) ^ 2 + (p 1 : ℂ) ^ 2) * (p 0 * z + p 1)))
  exact mod_cast congr_arg Complex.re (smul_eq_lcRow0_add z hp g.2)

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
⊢ (PowerSeries.coeff n) (qExpansion h f) =
    1 / ↑h * ∫ (u : ℝ) in 0..h, 1 / 𝕢 h (↑u + ↑t * ↑I) ^ n * f { coe := ↑u + ↑t * ↑I, coe_im_pos := ⋯ }

Tactic:
rw [qExpansion_coeff_eq_circleIntegral hh hfper hfhol hfbdd n hR0 hR1, circleIntegral,
    show 2 * π = h * (2 * π / h) by field_simp]

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
⊢ (2 * ↑π * Complex.I)⁻¹ *
      ∫ (θ : ℝ) in 0..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 := ⋯ }
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: case hdb
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
⊢ τ.im ^ 2 ≤ Complex.normSq (↑(↑g 1 0) * ↑τ + ↑(↑g 1 1))

Tactic:
show Complex.normSq ((g 1 0) * τ + (g 1 1)) =
      ((g 1 0) * τ.re + (g 1 1)) ^ 2 + (g 1 0) ^ 2 * τ.im ^ 2 by simp [Complex.normSq_apply]; ring

Goal state after:
case hdb
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
⊢ τ.im ^ 2 ≤ (↑(↑g 1 0) * τ.re + ↑(↑g 1 1)) ^ 2 + ↑(↑g 1 0) ^ 2 * τ.im ^ 2
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|
⊢ z.im / normSq (↑(↑g 1 0) * ↑z + ↑(↑g 1 1)) = z.im / normSq (↑(↑g₀ 1 0) * ↑z + ↑(↑g₀ 1 1))

Tactic:
hg

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|
⊢ z.im / normSq (↑(↑g₀ 1 0) * ↑z + ↑(↑g₀ 1 1)) = z.im / normSq (↑(↑g₀ 1 0) * ↑z + ↑(↑g₀ 1 1))
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 (UpperHalfPlane.mdifferentiableAt_iff.mp <| hfhol ⟨z, hz⟩)

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

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

Tactic:
have : ((toConjAct (g : GL (Fin 2) ℝ)⁻¹) • Γ).IsArithmetic := by
    simpa [(show Rat.castHom ℝ = algebraMap ℚ ℝ by rfl), map_inv, map_mapGL]
      using! Subgroup.IsArithmetic.conj Γ (mapGL ℚ g)⁻¹

Goal state after:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Γ.IsArithmetic
F : Type u_2
F' : Type u_3
f : F
f' : F'
inst✝³ : FunLike F ℍ ℂ
inst✝² : FunLike F' ℍ ℂ
inst✝¹ : CuspFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
g : SL(2, ℤ)
this : (toConjAct (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g))⁻¹ • Γ).IsArithmetic
⊢ Tendsto (fun τ ↦ petersson k (⇑f ∣[k] g) (⇑f' ∣[k] g) τ) atImInfty (𝓝 0)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : 3 * c ^ 2 ≤ 4
⊢ |↑g 1 0| ≤ 1

Tactic:
rw [← Int.cast_pow, ← Int.cast_three, ← Int.cast_four, ← Int.cast_mul, Int.cast_le] at this

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : 3 * c' ^ 2 ≤ 4
⊢ |↑g 1 0| ≤ 1
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: case a
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 : ℝ := ⋯
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 : ℝ → ℝ := ⋯
hne : ‖↑n ^ e‖ = ↑n ^ e
x : ℝ
⊢ -2 * Real.pi / h ≤ ↑n * (-2 * Real.pi * (↑x + 1 / ↑n * I).im / h)

Tactic:
simp [field]

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

Goal state before:
pp: k : ℤ
f g : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hg : (PowerSeries.coeff 0) (qExpansion 1 ⇑g) = 1
⊢ (f - (PowerSeries.coeff 0) (qExpansion 1 ⇑f) • g).IsCuspForm

Tactic:
isCuspForm_iff_coeffZero_eq_zero,

Goal state after:
k : ℤ
f g : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hg : (PowerSeries.coeff 0) (qExpansion 1 ⇑g) = 1
⊢ (PowerSeries.coeff 0) (qExpansion 1 ⇑(f - (PowerSeries.coeff 0) (qExpansion 1 ⇑f) • g)) = 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
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
⊢ -x ∉ {x}

Tactic:
· simp only [disjoint_iff_ne, mem_insert, mem_singleton, mem_Icc]
    omega

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
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
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
⊢ Disjoint (Icc (-(x - 1)) (x - 1)) {-x, x}

Tactic:
· simp only [disjoint_iff_ne, mem_insert, mem_singleton, mem_Icc]
    omega

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

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

Tactic:
tsum_congr (one_sub_eta_logDeriv_eq z),

Goal state after:
z : ℂ
⊢ ∑' (b : ℕ), 2 * ↑π * I * (↑b + 1) * -eta_q b z / (1 - eta_q b z) =
    2 * ↑π * I * ∑' (n : ℕ), (↑n + 1) * -eta_q n z / (1 - eta_q n z)
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: F : ℍ → ℂ
hF : MDiff F
⊢ MDiff (D F)

Tactic:
rw [UpperHalfPlane.mdifferentiable_iff] at hF ⊢

Goal state after:
F : ℍ → ℂ
hF : DifferentiableOn ℂ (F ∘ ↑ofComplex) {z | 0 < z.im}
⊢ DifferentiableOn ℂ (D F ∘ ↑ofComplex) {z | 0 < z.im}
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ ↑ofComplex) ↑z
hGz : DifferentiableAt ℂ (G ∘ ↑ofComplex) ↑z
⊢ (2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex * G ∘ ↑ofComplex) ↑z =
    (2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑z * G z + F z * ((2 * ↑π * I)⁻¹ * deriv (G ∘ ↑ofComplex) ↑z)

Tactic:
deriv_mul hFz hGz

Goal state after:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ ↑ofComplex) ↑z
hGz : DifferentiableAt ℂ (G ∘ ↑ofComplex) ↑z
⊢ (2 * ↑π * I)⁻¹ * (deriv (F ∘ ↑ofComplex) ↑z * (G ∘ ↑ofComplex) ↑z + (F ∘ ↑ofComplex) ↑z * deriv (G ∘ ↑ofComplex) ↑z) =
    (2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑z * G z + F z * ((2 * ↑π * I)⁻¹ * deriv (G ∘ ↑ofComplex) ↑z)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inl.inl.inl
g✝ : SL(2, ℤ)
z✝¹ : ℍ
g : SL(2, ℤ)
z✝ z : ℍ
hz : z ∈ 𝒟
hg : T • z ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) T)) ↑z‖ ≤ 1
hc✝ : 0 ≤ ↑T 1 0
hc : ↑T 1 0 = 0
⊢ (T • z).im = z.im

Tactic:
simp only [← zpow_neg_one, im_T_zpow_smul, im_T_smul, one_smul, SL_neg_smul]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inl.inl.inr
g✝ : SL(2, ℤ)
z✝¹ : ℍ
g : SL(2, ℤ)
z✝ z : ℍ
hz : z ∈ 𝒟
hg : -T • z ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (-T))) ↑z‖ ≤ 1
hc✝ : 0 ≤ ↑(-T) 1 0
hc : ↑(-T) 1 0 = 0
⊢ (-T • z).im = z.im

Tactic:
simp only [← zpow_neg_one, im_T_zpow_smul, im_T_smul, one_smul, SL_neg_smul]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inl.inr.inl.inl
g✝ : SL(2, ℤ)
z✝¹ : ℍ
g : SL(2, ℤ)
z✝ z : ℍ
hz : z ∈ 𝒟
hg : T⁻¹ • z ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) T⁻¹)) ↑z‖ ≤ 1
hc✝ : 0 ≤ ↑T⁻¹ 1 0
hc : ↑T⁻¹ 1 0 = 0
⊢ (T⁻¹ • z).im = z.im

Tactic:
simp only [← zpow_neg_one, im_T_zpow_smul, im_T_smul, one_smul, SL_neg_smul]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inl.inr.inl.inr
g✝ : SL(2, ℤ)
z✝¹ : ℍ
g : SL(2, ℤ)
z✝ z : ℍ
hz : z ∈ 𝒟
hg : -T⁻¹ • z ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (-T⁻¹))) ↑z‖ ≤ 1
hc✝ : 0 ≤ ↑(-T⁻¹) 1 0
hc : ↑(-T⁻¹) 1 0 = 0
⊢ (-T⁻¹ • z).im = z.im

Tactic:
simp only [← zpow_neg_one, im_T_zpow_smul, im_T_smul, one_smul, SL_neg_smul]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inl.inr.inr.inl
g✝ : SL(2, ℤ)
z✝¹ : ℍ
g : SL(2, ℤ)
z✝ z : ℍ
hz : z ∈ 𝒟
hg : 1 • z ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) 1)) ↑z‖ ≤ 1
hc✝ : 0 ≤ ↑1 1 0
hc : ↑1 1 0 = 0
⊢ (1 • z).im = z.im

Tactic:
simp only [← zpow_neg_one, im_T_zpow_smul, im_T_smul, one_smul, SL_neg_smul]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inl.inr.inr.inr
g✝ : SL(2, ℤ)
z✝¹ : ℍ
g : SL(2, ℤ)
z✝ z : ℍ
hz : z ∈ 𝒟
hg : -1 • z ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (-1))) ↑z‖ ≤ 1
hc✝ : 0 ≤ ↑(-1) 1 0
hc : ↑(-1) 1 0 = 0
⊢ (-1 • z).im = z.im

Tactic:
simp only [← zpow_neg_one, im_T_zpow_smul, im_T_smul, one_smul, SL_neg_smul]

Goal state after: