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 : ℂ
⊢ ∑ j, Φ j * completedHurwitzZetaEven (toAddCircle j) s = 0

Tactic:
refine (hΦ.mul_even fun j ↦ ?_).sum_eq_zero

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
j : ZMod N
⊢ completedHurwitzZetaEven (toAddCircle (-j)) s = completedHurwitzZetaEven (toAddCircle j) s
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j, Φ j = 0
⊢ DifferentiableAt ℂ (fun x ↦ completedLFunction₀ Φ x - ↑N ^ (-x) * (Φ 0 / x) - ↑N ^ (-x) * ((∑ j, Φ j) / (1 - x))) s

Tactic:
refine ((differentiable_completedLFunction₀ _ _).sub ?_).sub ?_

Goal state after:
case refine_1
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j, Φ j = 0
⊢ DifferentiableAt ℂ (fun x ↦ ↑N ^ (-x) * (Φ 0 / x)) s

case refine_2
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j, Φ j = 0
⊢ DifferentiableAt ℂ (fun x ↦ ↑N ^ (-x) * ((∑ j, Φ j) / (1 - x))) s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: case inl
⊢ -1 / 2 = -(↑1 / ↑2)

Tactic:
Rat.cast_one,

Goal state after:
case inl
⊢ -1 / 2 = -(1 / ↑2)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
⊢ -↑(bernoulli' (k + 1)) / (↑k + 1) = (-1) ^ k * ((-↑1) ^ (k + 1) * ↑(bernoulli' (k + 1))) / (↑k + 1)

Tactic:
Rat.cast_one,

Goal state after:
k : ℕ
⊢ -↑(bernoulli' (k + 1)) / (↑k + 1) = (-1) ^ k * ((-1) ^ (k + 1) * ↑(bernoulli' (k + 1))) / (↑k + 1)
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: case e_a
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑n + 1) ^ ↑x * (↑m ^ ↑x)⁻¹ = ((↑m * (↑n + 1)⁻¹) ^ ↑x)⁻¹

Tactic:
rw [show (n + 1 : ℂ)⁻¹ = (n + 1 : ℝ)⁻¹ by simp,
    show (n + 1 : ℂ) = (n + 1 : ℝ) by norm_cast, show (m : ℂ) = (m : ℝ) by norm_cast,
    mul_cpow_ofReal_nonneg m.cast_nonneg Hn, mul_inv, mul_comm]

Goal state after:
case e_a
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑↑m ^ ↑x)⁻¹ * ↑(↑n + 1) ^ ↑x = (↑↑m ^ ↑x)⁻¹ * (↑(↑n + 1)⁻¹ ^ ↑x)⁻¹
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
⊢ Tendsto (fun x ↦ (↑n + 1) ^ ↑x * LSeries f ↑x) atTop (nhds (f (n + 1)))

Tactic:
let F := fun (x : ℝ) ↦ {m | n + 1 < m}.indicator (fun m ↦ f m / (m / (n + 1) : ℂ) ^ (x : ℂ))

Goal state after:
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x ↦ {m | n + 1 < m}.indicator fun m ↦ f m / (↑m / (↑n + 1)) ^ ↑x
⊢ Tendsto (fun x ↦ (↑n + 1) ^ ↑x * LSeries f ↑x) atTop (nhds (f (n + 1)))
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:
by
  -- strip down to the key equality:
  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: N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
⊢ DifferentiableAt ℂ B.F s

Tactic:
rcases ne_or_eq s 1 with hs | rfl

Goal state after:
case inl
N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : s ≠ 1
⊢ DifferentiableAt ℂ B.F s

case inr
N : ℕ
inst✝ : NeZero N
B : BadChar N
⊢ DifferentiableAt ℂ B.F 1
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: case hg
N : ℕ
inst✝ : NeZero N
B : BadChar N
G : ℂ → ℂ := ⋯
H : ℂ → ℂ := ⋯
this : B.F = G * H
⊢ ContinuousAt H 1

Tactic:
· exact (B.χ.differentiableAt_LFunction 1 (.inr B.χ_ne)).hasDerivAt.continuousAt_div

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
⊢ 1 + I * ↑y ≠ 1 ∨ χ ≠ 1

Tactic:
simpa only [ne_eq, add_eq_left, _root_.mul_eq_zero, I_ne_zero, ofReal_eq_zero, false_or]
    using hy

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

Goal state before:
pp: q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
hs₁ : s ≠ 1
| LFunction 1 s

Tactic:
rw [← mul_one (LFunction ..)]

Goal state after:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
hs₁ : s ≠ 1
| LFunction 1 s * 1
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: case neg.refine_1
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x ↦ LSeries f ↑x) =ᶠ[atTop] 0
⊢ ∀ (n : ℕ), ¬n = 0 → f n = 0

pp: case neg.refine_2
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : ∀ (n : ℕ), ¬n = 0 → f n = 0
x : ℝ
⊢ (fun x ↦ LSeries f ↑x) x = 0 x

Tactic:
· let F (n : ℕ) : ℂ := if n = 0 then 0 else f n
      have hF₀ : F 0 = 0 := rfl
      have hF {n : ℕ} (hn : n ≠ 0) : F n = f n := if_neg hn
      suffices ∀ n, F n = 0 from fun n hn ↦ (hF hn).symm.trans (this n)
      have ha : ¬ abscissaOfAbsConv F = ⊤ := abscissaOfAbsConv_congr hF ▸ h
      have h' (x : ℝ) : LSeries F x = LSeries f x := LSeries_congr hF x
      have H' (n : ℕ) : (fun x : ℝ ↦ n ^ (x : ℂ) * LSeries F x) =ᶠ[atTop] fun _ ↦ 0 := by
        simp only [h']
        rw [eventuallyEq_iff_exists_mem] at H ⊢
        obtain ⟨s, hs⟩ := H
        exact ⟨s, hs.1, fun x hx ↦ by simp [hs.2 hx]⟩
      intro n
      induction n using Nat.strongRecOn with | ind n ih =>
      -- it suffices to show that `n ^ x * LSeries F x` tends to `F n` as `x` tends to `∞`
      suffices Tendsto (fun x : ℝ ↦ n ^ (x : ℂ) * LSeries F x) atTop (nhds (F n)) by
        replace this := this.congr' <| H' n
        simp only [tendsto_const_nhds_iff] at this
        exact this.symm
      cases n with
      | zero => exact Tendsto.congr' (H' 0).symm <| by simp [hF₀]
      | succ n =>
          simpa using! LSeries.tendsto_cpow_mul_atTop (fun m hm ↦ ih m <| lt_succ_of_le hm) <|
            Ne.lt_top ha

Goal state after:
case neg.refine_2
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : ∀ (n : ℕ), ¬n = 0 → f n = 0
x : ℝ
⊢ (fun x ↦ LSeries f ↑x) x = 0 x
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
⊢ (s - 1) * ∫ (t : ℝ) in Set.Ioi T, ε * t ^ (-s) ≤ ε * ((s - 1) * ∫ (t : ℝ) in Set.Ioi 1, t ^ (-s))

Tactic:
rw [integral_const_mul, ← mul_assoc, ← mul_assoc, mul_comm ε]
      refine mul_le_mul_of_nonneg_left (setIntegral_mono_set ?_ ?_
        (Set.Ioi_subset_Ioi hT₁).eventuallyLE) (mul_nonneg (sub_pos_of_lt hs).le hε.le)
      · exact integrableOn_Ioi_rpow_of_lt (neg_lt_neg_iff.mpr hs) zero_lt_one
      · exact (ae_restrict_iff' measurableSet_Ioi).mpr <| univ_mem' fun t ht ↦
        Real.rpow_nonneg (zero_le_one.trans ht.le) _

Goal state after:
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]
⊢ Finite 𝓀[K] → TotallyBounded Set.univ

Tactic:
intro H
    rw [Metric.totallyBounded_iff]
    intro ε εpos
    obtain ⟨p, hp⟩ := IsDiscreteValuationRing.exists_irreducible 𝒪[K]
    have hp' := Valuation.integer.v_irreducible_lt_one hp
    obtain ⟨n, hn⟩ : ∃ n : ℕ, ‖(p : K)‖ ^ n < ε := exists_pow_lt_of_lt_one εpos
      (toNormedField.norm_lt_one_iff.mpr hp')
    have hF := finite_quotient_maximalIdeal_pow_of_finite_residueField H n
    refine ⟨Quotient.out '' (Set.univ (α := 𝒪[K] ⧸ (𝓂[K] ^ n))), Set.toFinite _, ?_⟩
    have : {y : 𝒪[K] | v (y : K) ≤ v (p : K) ^ n} = Metric.closedBall 0 (‖p‖ ^ n) := by
      ext
      simp [← norm_pow]
    simp only [Ideal.univ_eq_iUnion_image_add (𝓂[K] ^ n),
      hp.maximalIdeal_pow_eq_setOfPred_le_v_coe_pow,
      this, AddSubgroupClass.coe_norm, Set.image_univ, Set.mem_range, Set.iUnion_exists,
      Set.iUnion_iUnion_eq', Set.iUnion_subset_iff, Metric.vadd_closedBall, vadd_eq_add, add_zero]
    intro
    exact (Metric.closedBall_subset_ball hn).trans (Set.subset_iUnion_of_subset _ le_rfl)

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

Goal state before:
pp: ⊢ jacobiSym = fastJacobiSym

Tactic:
ext a b

Goal state after:
a : ℤ
b : ℕ
⊢ J(a | b) = fastJacobiSym a b
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 ≠ 0
⊢ ∀ {x_1 y : A}, (y ∈ Set.range fun x_2 ↦ x * x_2) → x_1 * y ∈ Set.range fun x_2 ↦ x * x_2

Tactic:
by rintro a _ ⟨c, rfl⟩; exact ⟨a * c, by dsimp; rw [← mul_assoc, ← hx1, mul_assoc]⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: K : Type u_3
Γ : Type u_4
inst✝¹ : Field K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
⊢ (∃ x, x ≠ 0 ∧ v x < 1) ↔ ¬∀ ⦃x : ↥v.integer⦄, x ∈ IsLocalRing.maximalIdeal ↥v.integer → x = 0

Tactic:
not_forall,

Goal state after:
K : Type u_3
Γ : Type u_4
inst✝¹ : Field K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
⊢ (∃ x, x ≠ 0 ∧ v x < 1) ↔ ∃ x, ∃ (_ : x ∈ IsLocalRing.maximalIdeal ↥v.integer), ¬x = 0
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: case refine_1
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
p : ↑(boxPoly n B₁ B₂)
⊢ (toFn (n + 1)) ↑p ∈ ↑(Finset.Icc (fun x ↦ ⌈B₁ x⌉) fun x ↦ ⌊B₂ x⌋)

pp: case refine_2
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
p : ↑↑(Finset.Icc (fun x ↦ ⌈B₁ x⌉) fun x ↦ ⌊B₂ x⌋)
⊢ (ofFn (n + 1)) ↑p ∈ boxPoly n B₁ B₂

pp: case refine_3
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
⊢ Function.LeftInverse (fun p ↦ ⟨(ofFn (n + 1)) ↑p, ⋯⟩) fun p ↦ ⟨(toFn (n + 1)) ↑p, ⋯⟩

pp: case refine_4
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
⊢ Function.RightInverse (fun p ↦ ⟨(ofFn (n + 1)) ↑p, ⋯⟩) fun p ↦ ⟨(toFn (n + 1)) ↑p, ⋯⟩

Tactic:
· have prop := p.property.2
      simpa using ⟨fun i ↦ ceil_le.mpr (prop i).1, fun i ↦ le_floor.mpr (prop i).2⟩

Goal state after:
case refine_2
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
p : ↑↑(Finset.Icc (fun x ↦ ⌈B₁ x⌉) fun x ↦ ⌊B₂ x⌋)
⊢ (ofFn (n + 1)) ↑p ∈ boxPoly n B₁ B₂

case refine_3
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
⊢ Function.LeftInverse (fun p ↦ ⟨(ofFn (n + 1)) ↑p, ⋯⟩) fun p ↦ ⟨(toFn (n + 1)) ↑p, ⋯⟩

case refine_4
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
⊢ Function.RightInverse (fun p ↦ ⟨(ofFn (n + 1)) ↑p, ⋯⟩) fun p ↦ ⟨(toFn (n + 1)) ↑p, ⋯⟩
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: case refine_2
f : ℕ → ℝ
l : ℝ
hf : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hf' : ∀ (n : ℕ), 0 ≤ f n
s : ℝ
hs : 1 < s
⊢ LSeriesSummable (fun n ↦ ↑(f n)) ↑s

Tactic:
refine LSeriesSummable_of_sum_norm_bigO_and_nonneg ?_ hf' zero_le_one hs

Goal state after:
case refine_2
f : ℕ → ℝ
l : ℝ
hf : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hf' : ∀ (n : ℕ), 0 ≤ f n
s : ℝ
hs : 1 < s
⊢ (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ 1
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: Γ : Subgroup SL(2, ℤ)
⊢ (map (mapGL ℝ) Γ).IsArithmetic ↔ Γ.FiniteIndex

Tactic:
constructor <;>
  · refine fun ⟨h⟩ ↦ ⟨?_⟩
    simpa [Commensurable, MonoidHom.range_eq_map, ← relIndex_comap,
      comap_map_eq_self_of_injective mapGL_injective] using h

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₂
hz_det : z.det = 1
i j : Fin 2
⊢ (1 + (M • (A₁.num * k * A₂.num)).map ⇑(Int.castRingHom (ZMod M))) i j = ↑1 i j

Tactic:
Int.coe_castRingHom,

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₂
hz_det : z.det = 1
i j : Fin 2
⊢ (1 + (M • (A₁.num * k * A₂.num)).map fun x ↦ ↑x) i j = ↑1 i j
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: β : Type u_1
G : Type u_2
H : Type u_3
α : Type u_4
inst✝³ : Monoid G
inst✝² : AddMonoid α
inst✝¹ : Monoid H
inst✝ : SlashAction β G α
h : H →* G
k : β
a : α
⊢ a ∣[k] h 1 = a

Tactic:
simp only [map_one, SlashAction.slash_one]

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

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

Tactic:
Eq.comm,

Goal state after:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
hsp : AddSubgroup.zmultiples 1 = AddSubgroup.zmultiples (map (mapGL ℝ) Γ).strictWidthInfty
this : DiscreteTopology ↥(map (mapGL ℝ) Γ).strictPeriods
⊢ (map (mapGL ℝ) Γ).strictWidthInfty = 1
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
hsp : AddSubgroup.zmultiples (Subgroup.map (mapGL ℝ) Γ(N)).strictWidthInfty = AddSubgroup.zmultiples ↑N
⊢ (Subgroup.map (mapGL ℝ) Γ(N)).strictWidthInfty = ↑N

Tactic:
Eq.comm,

Goal state after:
N : ℕ
inst✝ : NeZero N
hsp : AddSubgroup.zmultiples ↑N = AddSubgroup.zmultiples (Subgroup.map (mapGL ℝ) Γ(N)).strictWidthInfty
⊢ (Subgroup.map (mapGL ℝ) Γ(N)).strictWidthInfty = ↑N
Module: Mathlib.NumberTheory.ModularForms.Petersson

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝⁶ : FunLike F ℍ ℂ
inst✝⁵ : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Fact (IsCusp OnePoint.infty Γ)
inst✝³ : Γ.HasDetPlusMinusOne
inst✝² : DiscreteTopology ↥Γ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty ⇑f
f' : F'
b : ℝ
hb : b > 0
hbf : ⇑f =O[atImInfty] fun τ ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
⊢ ∃ a > 0, petersson k ⇑f ⇑f' =O[atImInfty] fun τ ↦ Real.exp (-a * τ.im)

Tactic:
use a, ha

Goal state after:
case right
F : Type u_1
F' : Type u_2
inst✝⁶ : FunLike F ℍ ℂ
inst✝⁵ : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Fact (IsCusp OnePoint.infty Γ)
inst✝³ : Γ.HasDetPlusMinusOne
inst✝² : DiscreteTopology ↥Γ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty ⇑f
f' : F'
b : ℝ
hb : b > 0
hbf : ⇑f =O[atImInfty] fun τ ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
⊢ petersson k ⇑f ⇑f' =O[atImInfty] fun τ ↦ Real.exp (-a * τ.im)
Module: Mathlib.NumberTheory.ModularForms.Petersson

Goal state before:
pp: E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℍ → E
hf : ∃ c > 0, f =O[atImInfty] fun τ ↦ Real.exp (-c * τ.im)
⊢ IsZeroAtImInfty f

Tactic:
obtain ⟨a, ha, ha'⟩ := hf
  refine ha'.trans_tendsto <| (Real.tendsto_exp_atBot.comp ?_).comp tendsto_comap
  exact tendsto_id.const_mul_atTop_of_neg (neg_lt_zero.mpr ha)

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

Goal state before:
pp: k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
⊢ (↑(i 0) *
          ((↑((algebraMap ℤ ℝ) (↑A 0 0)) * ↑z + ↑((algebraMap ℤ ℝ) (↑A 0 1))) /
            (↑((algebraMap ℤ ℝ) (↑A 1 0)) * ↑z + ↑((algebraMap ℤ ℝ) (↑A 1 1)))) +
        ↑(i 1)) ^
      (-k) =
    (↑(↑(SpecialLinearGroup.toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) A)) 1 0) * ↑z +
          ↑(↑(SpecialLinearGroup.toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) A)) 1 1)) ^
        k *
      (↑(i 0 * ↑A 0 0 + i 1 * ↑A 1 0) * ↑z + ↑(i 0 * ↑A 0 1 + i 1 * ↑A 1 1)) ^ (-k)

Tactic:
have h (a b c d u v : ℂ) (hc : c * z + d ≠ 0) : (u * ((a * z + b) / (c * z + d)) + v) ^ (-k) =
      (c * z + d) ^ k * ((u * a + v * c) * z + (u * b + v * d)) ^ (-k) := by
    replace hc : z * c + d ≠ 0 := by convert! hc using 1; ring
    field_simp
    simp [div_zpow]
    ring_nf

Goal state after:
k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
h :
  ∀ (a b c d u v : ℂ),
    c * ↑z + d ≠ 0 →
      (u * ((a * ↑z + b) / (c * ↑z + d)) + v) ^ (-k) =
        (c * ↑z + d) ^ k * ((u * a + v * c) * ↑z + (u * b + v * d)) ^ (-k)
⊢ (↑(i 0) *
          ((↑((algebraMap ℤ ℝ) (↑A 0 0)) * ↑z + ↑((algebraMap ℤ ℝ) (↑A 0 1))) /
            (↑((algebraMap ℤ ℝ) (↑A 1 0)) * ↑z + ↑((algebraMap ℤ ℝ) (↑A 1 1)))) +
        ↑(i 1)) ^
      (-k) =
    (↑(↑(SpecialLinearGroup.toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) A)) 1 0) * ↑z +
          ↑(↑(SpecialLinearGroup.toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) A)) 1 1)) ^
        k *
      (↑(i 0 * ↑A 0 0 + i 1 * ↑A 1 0) * ↑z + ↑(i 0 * ↑A 0 1 + i 1 * ↑A 1 1)) ^ (-k)
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✝ : ℕ
⊢ ∑ 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)

Tactic:
refine Finset.sum_congr rfl fun i hi ↦ ?_

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

Goal state before:
pp: case succ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
inst✝ : Γ.HasDetPlusMinusOne
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
f : ModularForm Γ k
n : ℕ
ih : qExpansion h ⇑(f.pow n) = qExpansion h ⇑f ^ n
⊢ qExpansion h ⇑(f.pow (n + 1)) = qExpansion h ⇑f ^ (n + 1)

Tactic:
rw [coe_pow, pow_succ, ← coe_pow, ← coe_mul, ModularForm.qExpansion_mul hh hΓ, ih,
      pow_succ]

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
x : ℝ
⊢ 1 / h * (1 / ‖𝕢 h (↑x + 1 / ↑n * I)‖ ^ n * ‖f { coe := ↑x + 1 / ↑n * I, coe_im_pos := ⋯ }‖) ≤
    1 / h * (1 / Real.exp (-2 * Real.pi / h) * (C * ↑n ^ e))

Tactic:
Function.Periodic.norm_qParam,

Goal state after:
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
x : ℝ
⊢ 1 / h *
      (1 / Real.exp (-2 * Real.pi * (↑x + 1 / ↑n * I).im / h) ^ n * ‖f { coe := ↑x + 1 / ↑n * I, coe_im_pos := ⋯ }‖) ≤
    1 / h * (1 / Real.exp (-2 * Real.pi / h) * (C * ↑n ^ e))
Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule

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

Tactic:
by
  refine ⟨fun ⟨g, hg⟩ ↦ ?_, fun h ↦ (isCuspForm_iff f).mpr (isZeroAt_of_coeffZero_eq_zero f h)⟩
  rw [← hg, qExpansion_coeff_zero one_pos
    (ModularFormClass.analyticAt_cuspFunction_zero _ one_pos one_mem_strictPeriods_SL)
    (periodic_comp_ofComplex _ one_mem_strictPeriods_SL)]
  exact (CuspFormClass.zero_at_infty g).valueAtInfty_eq_zero

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

Goal state before:
pp: z : ℍ
⊢ D2 ModularGroup.S z = 2 * ↑π * I / ↑z

Tactic:
by
  simp [D2, ModularGroup.S, ModularGroup.denom_apply]

Goal state after:
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

Goal state after:
case neg
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : b = 0
hn : ¬n = -1
hn0 : ↑n ≠ 0
⊢ (↑b * ↑z + ↑n + 1)⁻¹ * ((↑b * ↑z + ↑n) ^ 2)⁻¹ + δ ![b, n] + ((↑b * ↑z + ↑n)⁻¹ - (↑b * ↑z + ↑n + 1)⁻¹) =
    ((↑b * ↑z + ↑n) ^ 2)⁻¹
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : ¬b = 0
⊢ ↑b * ↑z + ↑n + 1 ≠ 0

Tactic:
simpa [add_assoc] using linear_ne_zero (cd := ![b, n + 1]) z (by aesop)

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

Goal state before:
pp: hη : DifferentiableOn ℂ η upperHalfPlaneSet
hlog : DifferentiableOn ℂ (logDeriv η) upperHalfPlaneSet
z : ℂ
hz : z ∈ upperHalfPlaneSet
⊢ (E2 ∘ ↑ofComplex) z = (↑π * I / 12)⁻¹ * logDeriv η z

Tactic:
simp [ofComplex_apply_of_im_pos hz, logDeriv_eta_eq_E2 ⟨z, hz⟩]

Goal state after:
hη : DifferentiableOn ℂ η upperHalfPlaneSet
hlog : DifferentiableOn ℂ (logDeriv η) upperHalfPlaneSet
z : ℂ
hz : z ∈ upperHalfPlaneSet
⊢ E2 { coe := z, coe_im_pos := hz } = 12 / (↑π * I) * (↑π * I / 12 * E2 { coe := z, coe_im_pos := hz })