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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ ContinuousOn (fun s ↦ -deriv (LFunctionTrivChar₁ n) s / LFunctionTrivChar₁ n s)
    {s | s = 1 ∨ LFunctionTrivChar n s ≠ 0}

Tactic:
simp_rw [neg_div]

Goal state after:
n : ℕ
inst✝ : NeZero n
⊢ ContinuousOn (fun s ↦ -(deriv (LFunctionTrivChar₁ n) s / LFunctionTrivChar₁ n s))
    {s | s = 1 ∨ LFunctionTrivChar n s ≠ 0}
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
mem_norm_factors :
  normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈
    normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
y : Ideal S
hy : normalizedFactors (Ideal.map (algebraMap R S) I) = {y}
⊢ Ideal.map (algebraMap R S) I ≠ 0

Tactic:
rwa [← bot_eq_zero, Ne,
            map_eq_bot_iff_of_injective (FaithfulSMul.algebraMap_injective R S)]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case inr.refine_2
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
⊢ 1 / (-2 * ↑π * I * ↑n) * (0 - ↑(k + 1) * bernoulliFourierCoeff k n) = -↑(k + 1)! / (2 * ↑π * I * ↑n) ^ (k + 1)

Tactic:
h'k,

Goal state after:
case inr.refine_2
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
⊢ 1 / (-2 * ↑π * I * ↑n) * (0 - ↑(k + 1) * (-↑k ! / (2 * ↑π * I * ↑n) ^ k)) = -↑(k + 1)! / (2 * ↑π * I * ↑n) ^ (k + 1)
Module: Mathlib.NumberTheory.LSeries.Injectivity

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

Tactic:
← cpow_neg,

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

Goal state before:
pp: case inr.refine_2
N : ℕ
inst✝ : NeZero N
B : BadChar N
G : ℂ → ℂ := Function.update (fun s ↦ (s - 1) * riemannZeta s) 1 1
H : ℂ → ℂ := Function.update (fun s ↦ (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1 (deriv (LFunction B.χ) 1)
this : B.F = G * H
⊢ ContinuousAt (G * H) 1

Tactic:
apply ContinuousAt.mul

Goal state after:
case inr.refine_2.hf
N : ℕ
inst✝ : NeZero N
B : BadChar N
G : ℂ → ℂ := ⋯
H : ℂ → ℂ := ⋯
this : B.F = G * H
⊢ ContinuousAt G 1

case hg
N : ℕ
inst✝ : NeZero N
B : BadChar N
G : ℂ → ℂ := ⋯
H : ℂ → ℂ := ⋯
this : B.F = G * H
⊢ ContinuousAt H 1
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
χ_ne : χ ≠ 1
hL : LFunction χ 1 = 0
B : BadChar N := { χ := χ, χ_ne := χ_ne, χ_sq := hχ, hχ := hL }
⊢ LSeries.abscissaOfAbsConv ⇑χ.zetaMul ≤ ↑1

Tactic:
exact LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable
    fun _ a ↦ χ.LSeriesSummable_zetaMul a

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
H₀ : Summable fun p ↦ -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))
H₁ : Summable fun p ↦ -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))
H₂ : Summable fun p ↦ -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))
hsum₀ : Summable fun i ↦ 3 * (-log (1 - 1 ↑↑i * ↑↑i ^ (-(1 + ↑x)))).re
hsum₁ : Summable fun i ↦ 4 * (-log (1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y)))).re
hsum₂ : Summable fun x_1 ↦ (-log (1 - (χ ^ 2) ↑↑x_1 * ↑↑x_1 ^ (-(1 + ↑x + 2 * I * ↑y)))).re
⊢ 0 ≤
    3 * (∑' (p : Nat.Primes), -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))).re +
        4 * (∑' (p : Nat.Primes), -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))).re +
      (∑' (p : Nat.Primes), -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))).re

Tactic:
re_tsum H₀,

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
H₀ : Summable fun p ↦ -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))
H₁ : Summable fun p ↦ -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))
H₂ : Summable fun p ↦ -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))
hsum₀ : Summable fun i ↦ 3 * (-log (1 - 1 ↑↑i * ↑↑i ^ (-(1 + ↑x)))).re
hsum₁ : Summable fun i ↦ 4 * (-log (1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y)))).re
hsum₂ : Summable fun x_1 ↦ (-log (1 - (χ ^ 2) ↑↑x_1 * ↑↑x_1 ^ (-(1 + ↑x + 2 * I * ↑y)))).re
⊢ 0 ≤
    3 * ∑' (a : Nat.Primes), (-log (1 - 1 ↑↑a * ↑↑a ^ (-(1 + ↑x)))).re +
        4 * (∑' (p : Nat.Primes), -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))).re +
      (∑' (p : Nat.Primes), -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))).re
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⁻¹
⊢ deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s + ∑ χ ∈ {1}ᶜ, χ a⁻¹ * deriv (LFunction χ) s / LFunction χ s =
    ∑ χ, χ a⁻¹ * (deriv (LFunction χ) s / LFunction χ s) + 1 / (s - 1)

Tactic:
Fintype.sum_eq_add_sum_compl 1,

Goal state after:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
⊢ deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s + ∑ χ ∈ {1}ᶜ, χ a⁻¹ * deriv (LFunction χ) s / LFunction χ s =
    1 a⁻¹ * (deriv (LFunction 1) s / LFunction 1 s) + ∑ i ∈ {1}ᶜ, i a⁻¹ * (deriv (LFunction i) s / LFunction i s) +
      1 / (s - 1)
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: ⊢ π ^ 4 / 90 = (-1) ^ 3 * 2 ^ 3 * π ^ 4 * ↑(-1 / 30) / ↑4!

Tactic:
simp [Nat.factorial]; ring

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

Goal state before:
pp: case convert_3
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
⊢ (fun t ↦ deriv (fun x ↦ ↑x ^ (-s)) t * ∑ k ∈ Icc 0 ⌊t⌋₊, f k) =O[atTop] fun x ↦ x ^ ((-s - 1).re + r)

Tactic:
· refine .mul_atTop_rpow_of_isBigO_rpow (-(s + 1).re) r _ ?_ ?_ (by rw [← neg_re, neg_add'])
    · simpa [-neg_add_rev, neg_add'] using! isBigO_deriv_ofReal_cpow_const_atTop _
    · exact (hO.comp_tendsto tendsto_nat_floor_atTop).trans <|
        isEquivalent_nat_floor.isBigO.rpow hr (eventually_ge_atTop 0)

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

Goal state before:
pp: a : ℤ
e b x✝ : ℕ
ih : J(a ^ x✝ | b) = J(a | b) ^ x✝
⊢ J(a ^ x✝.succ | b) = J(a | b) ^ x✝.succ

Tactic:
by
    rw [_root_.pow_succ, _root_.pow_succ, mul_left, ih]

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

Goal state before:
pp: m₁ m₂ n : ℕ
⊢ J(χ₄ ↑m₁ * χ₄ ↑m₂ | n) = J(χ₄ ↑m₁ | n) * J(χ₄ ↑m₂ | n)

Tactic:
jacobiSym.mul_left

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

Goal state before:
pp: a✝ b : ℕ
ha : Odd a✝
hb : Odd b
a x y : ℕ
⊢ qrSign (x * y) a * J(↑(x * y) | a) = qrSign x a * J(↑x | a) * (qrSign y a * J(↑y | a))

Tactic:
by
        simp_rw [qrSign.mul_left x y a, Nat.cast_mul, mul_left, mul_mul_mul_comm]

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

Goal state before:
pp: a : ℤ
b : ℕ
hb : Odd b
⊢ J(a | b) = J(a | b % (4 * a.natAbs))

Tactic:
rcases Int.natAbs_eq a with ha | ha <;> nth_rw 2 [ha] <;> nth_rw 1 [ha]

Goal state after:
case inl
a : ℤ
b : ℕ
hb : Odd b
ha : a = ↑a.natAbs
⊢ J(↑a.natAbs | b) = J(↑a.natAbs | b % (4 * a.natAbs))

case inr
a : ℤ
b : ℕ
hb : Odd b
ha : a = -↑a.natAbs
⊢ J(-↑a.natAbs | b) = J(-↑a.natAbs | b % (4 * a.natAbs))
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 : ValueGroupWithZero K
hr : r ≠ 0
hrs : {x | (valuation K) x < r} ⊆ s
⊢ ∃ r', r' ≠ 0 ∧ (valuation K) r' < 1 ∧ {x | (valuation K) x ≤ (valuation K) r'} ⊆ s

Tactic:
obtain ⟨r', hr', hr⟩ := Valuation.IsNontrivial.exists_lt_one (v := valuation K)

Goal state after:
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 : ValueGroupWithZero K
hr✝ : r ≠ 0
hrs : {x | (valuation K) x < r} ⊆ s
r' : K
hr' : r' ≠ 0
hr : (valuation K) r' < 1
⊢ ∃ r', r' ≠ 0 ∧ (valuation K) r' < 1 ∧ {x | (valuation K) x ≤ (valuation K) r'} ⊆ s
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case neg
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
z0 : 0 < ↑↑z
a0 : 0 < v a
U : K → Set K := fun y ↦ if v y ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v y}
this : (∀ (i : K), IsOpen (U i)) → ↑𝒪[K] ⊆ ⋃ i, U i → ∃ t, ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
w : K
hw : ↑↑z < v w
⊢ ¬v w = v 0

Tactic:
refine (hw.trans' ?_).ne'

Goal state after:
case neg
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
z0 : 0 < ↑↑z
a0 : 0 < v a
U : K → Set K := fun y ↦ if v y ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v y}
this : (∀ (i : K), IsOpen (U i)) → ↑𝒪[K] ⊆ ⋃ i, U i → ∃ t, ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
w : K
hw : ↑↑z < v w
⊢ v 0 < ↑↑z
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
I : TwoSidedIdeal A := mk' (Set.range fun x_1 ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
a : A
⊢ y * (a * x * y) = y * (a * (x * y))

Tactic:
mul_assoc a x y

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
I : TwoSidedIdeal A := mk' (Set.range fun x_1 ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
a : A
⊢ y * (a * (x * y)) = y * (a * (x * y))
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case zero
p' : ℕ
⊢ sZMod (p' + 2) 0 = ↑(s 0)

Tactic:
dsimp [s, sZMod]

Goal state after:
case zero
p' : ℕ
⊢ 4 = ↑4
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case mp
p : ℕ
w : 1 < p
h : ↑(sMod p (p - 2)) = 0
⊢ sMod p (p - 2) = 0

Tactic:
apply Int.eq_zero_of_dvd_of_nonneg_of_lt _ _
      (by simpa [ZMod.intCast_zmod_eq_zero_iff_dvd] using h)

Goal state after:
p : ℕ
w : 1 < p
h : ↑(sMod p (p - 2)) = 0
⊢ 0 ≤ sMod p (p - 2)

p : ℕ
w : 1 < p
h : ↑(sMod p (p - 2)) = 0
⊢ sMod p (p - 2) < 2 ^ p - 1
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
simpa [leg3, mul_add_div, eq_comm] using legendreSym.eq_pow (2 * k + 1) 3

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: k : ℕ
inst✝ : Fact (Nat.Prime (2 * k + 1))
leg3 : legendreSym (2 * k + 1) 3 = -1
q : ℕ := 2 * k + 1
this : 3 ^ k = -1
⊢ 3 = (ZMod.castHom ⋯ (X q)) 3

Tactic:
rw [map_ofNat]

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
pow2 : 2 ^ ((q + 1) / 2) = 2
this : 2 ^ ((q + 1) / 2) * ω ^ ((q + 1) / 2) = -2
⊢ 2 = (ZMod.castHom ⋯ (X q)) 2

Tactic:
rw [map_ofNat]

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)
| A₁ * ((a₁ * a₂ * M) • k).map Int.cast * A₂

Tactic:
rw [← A₁.inv_denom_smul_num, ← A₂.inv_denom_smul_num, Matrix.map_smul _ _ (by simp)]

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)
| (↑A₁.den)⁻¹ • A₁.num.map Int.cast * (a₁ * a₂ * M) • k.map Int.cast * (↑A₂.den)⁻¹ • A₂.num.map Int.cast
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case h
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
h₀ : w 1 = 0
this : w 0 ≠ 0
i : Fin 2
⊢ ((w 0)⁻¹ • w) i = ![1, 0] i

Tactic:
fin_cases i <;> simp_all

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

Goal state before:
pp: ι : Type u_1
k : ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
s : Finset ι
⊢ k * ↑(#s) = ∑ i ∈ s, k

Tactic:
rw [Finset.sum_const, nsmul_eq_mul']

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

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
g : GL (Fin 2) ℝ
hg : g • OnePoint.infty = c✝
⊢ IsZeroAtImInfty (SlashInvariantForm.toFun 0 ∣[k] g)

Tactic:
by simpa using! Filter.zero_zeroAtFilter _

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

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
m : ℕ
⊢ (PowerSeries.coeff m) (qExpansion h f) = (↑m.factorial)⁻¹ * iteratedDeriv m (cuspFunction h f) 0

Tactic:
simp [qExpansion]

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

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
c : ℕ → ℂ
hh : 0 < h
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
⊢ IsBoundedAtImInfty f

Tactic:
have hfeq : f = fun τ : ℍ ↦ update (cuspFunction h f) 0 (c 0) (𝕢 h τ) := by
    funext τ
    rw [update_of_ne (Periodic.qParam_ne_zero _)]
    exact (hf τ).unique (hasSum_cuspFunction_of_hasSum_punctured hh hf
      (Periodic.norm_qParam_lt_one hh τ.im_pos) (exp_ne_zero _))
  have htend : Tendsto f atImInfty (𝓝 (c 0)) := by
    rw [hfeq]
    simpa [update_self, Function.comp_def] using
      (hasFPowerSeriesOnBall_update hh hf).hasFPowerSeriesAt.continuousAt.tendsto.comp
        (qParam_tendsto_atImInfty hh)
  -- `IsBoundedAtImInfty f = BoundedAtFilter atImInfty f = (f =O[atImInfty] 1)` by definition.
  exact htend.isBigO_one ℝ

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
⊢ ∃ g, ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im

Tactic:
obtain ⟨p, hp_coprime, hp⟩ :=
    Filter.Tendsto.exists_within_forall_le hs (tendsto_normSq_coprime_pair z)

Goal state after:
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ a ∈ s, normSq (↑(p 0) * ↑z + ↑(p 1)) ≤ normSq (↑(a 0) * ↑z + ↑(a 1))
⊢ ∃ g, ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr.inl
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
hgz : g = T ^ 1
hre : (g • z).re = 1 + z.re
hb : b = 1
⊢ z.re = -1 / 2

Tactic:
linarith [(le_abs_self _).trans (abs_neg z.re ▸ hz.2), (le_abs_self _).trans hg.2]

Goal state after:
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
⊢ |↑g 1 1| ≤ 1

Tactic:
by
  have : ‖(z : ℂ) + g 1 1‖ ≤ 1 := by simpa [denom, hc] using hg'
  have := (abs_re_le_norm _).trans this
  rw [add_re, intCast_re, add_comm, coe_re] at this
  have := (abs_sub_abs_le_abs_add ..).trans this
  grw [sub_le_iff_le_add, hz.2, ← Int.cast_abs, ← Int.le_floor] at this
  convert! this
  rw [eq_comm, Int.floor_eq_iff]
  norm_num

Goal state after:
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

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

Tactic:
simpa using! le_of_dvd b.2 (div_dvd_of_dvd (dvd_of_mem_divisors hi))

Goal state after:
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
r : 𝕜
hr : ‖r‖ < 1
k : ℕ
this : ∀ (m : ℕ) [NeZero m], ∑' (n : ℕ), (r ^ m) ^ n = (1 - r ^ m)⁻¹
h00 : ∑' (d : ℕ+) (c : ℕ+), ↑↑c ^ k * r ^ (↑d * ↑c) = ∑' (e : ℕ+), ↑((σ k) ↑e) * r ^ ↑e
⊢ Summable (Function.uncurry fun c d ↦ ↑↑c ^ k * r ^ (↑d * ↑c))

Tactic:
apply (summable_prod_mul_pow k hr).prod_symm

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst✝⁴ : FunLike F ℍ ℂ
inst✝³ : DiscreteTopology ↥Γ
inst✝² : Γ.HasDetPlusMinusOne
inst✝¹ : Fact (IsCusp ∞ Γ)
inst✝ : ModularFormClass F Γ k
f : F
h : valueAtInfty ⇑f = 0
⊢ IsZeroAtImInfty ⇑f

Tactic:
by
  have hh : 0 < Γ.strictWidthInfty := Γ.strictWidthInfty_pos_iff.mpr Fact.out
  have hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods := Γ.strictWidthInfty_mem_strictPeriods
  have hanal := ModularFormClass.analyticAt_cuspFunction_zero f hh hΓ
  have hper := periodic_comp_ofComplex f hΓ
  simp_rw [IsZeroAtImInfty, ZeroAtFilter, ← h, ← cuspFunction_apply_zero hh hanal hper]
  exact (hanal.continuousAt.tendsto.comp (qParam_tendsto_atImInfty hh)).congr
    (fun τ ↦ SlashInvariantFormClass.eq_cuspFunction f τ hΓ hh.ne')

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

Goal state before:
pp: G✝ : Type u_1
inst✝⁹ : Neg G✝
inst✝⁸ : Preorder G✝
inst✝⁷ : LocallyFiniteOrder G✝
inst✝⁶ : atTop.NeBot
G : Type u_2
inst✝⁵ : AddCommGroup G
inst✝⁴ : PartialOrder G
inst✝³ : IsOrderedAddMonoid G
inst✝² : LocallyFiniteOrder G
inst✝¹ : NoTopOrder G
inst✝ : NoBotOrder G
⊢ (symmetricIoo G).filter ≤ atTop

Tactic:
rw [symmetricIoo, map_le_iff_le_comap, ← @tendsto_iff_comap]

Goal state after:
G✝ : Type u_1
inst✝⁹ : Neg G✝
inst✝⁸ : Preorder G✝
inst✝⁷ : LocallyFiniteOrder G✝
inst✝⁶ : atTop.NeBot
G : Type u_2
inst✝⁵ : AddCommGroup G
inst✝⁴ : PartialOrder G
inst✝³ : IsOrderedAddMonoid G
inst✝² : LocallyFiniteOrder G
inst✝¹ : NoTopOrder G
inst✝ : NoBotOrder G
⊢ Tendsto (fun g ↦ Ioo (-g) g) atTop atTop
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case hnorm
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 = 1
hre : z.re = -1 / 2
⊢ √(normSq ↑z) = ‖↑ρ‖

Tactic:
hnorm,

Goal state after:
case hnorm
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 = 1
hre : z.re = -1 / 2
⊢ √1 = ‖↑ρ‖
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: ⊢ δ =ᶠ[cofinite] 0

Tactic:
by
  filter_upwards [eventually_cofinite_ne ![0, 0], eventually_cofinite_ne ![0, -1]] with x hx hx'
  simp_all [δ]

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

Goal state before:
pp: z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ ∑'[symmetricIcc ℤ] (m : ℤ), e2Summand m z =
    ∑' (b : ℤ),
      (∑' (n : ℤ), G2Term z ![b, n] + ∑'[symmetricIco ℤ] (n : ℤ), (1 / (↑b * ↑z + ↑n) - 1 / (↑b * ↑z + ↑n + 1)))

Tactic:
rw [← tsum_eq_of_summable_unconditional (L := symmetricIcc ℤ)]
    · congr with a
      rw [e2Summand, tsum_eq_of_summable_unconditional
        (summable_right_one_div_linear_sub_one_div_linear_succ z a), ← Summable.tsum_add
        ((G2Term_prod_summable z).prod_factor _)
        (summable_right_one_div_linear_sub_one_div_linear_succ z a)]
      exact tsum_congr (fun b ↦ by simp [eisSummand, G2Term, aux_identity z a b, zpow_ofNat])
    · simpa only [tsum_symmetricIco_linear_sub_linear_add_one_eq_zero z, add_zero]
        using (G2Term_prod_summable z).prod

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

Goal state before:
pp: case hg
z : ℍ
N : ℤ
⊢ Summable fun m ↦ 1 / (↑m * ↑z + ↑N) - 1 / (↑m * ↑z + ↑N + 1)

Tactic:
· simpa [add_assoc] using! summable_left_one_div_linear_sub_one_div_linear z N (N + 1)

Goal state after:
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
⊢ (PowerSeries.coeff 0) (qExpansion 1 ⇑f) • Submodule.Quotient.mk (E hk) = Submodule.Quotient.mk f

Tactic:
← Submodule.Quotient.mk_smul,

Goal state after:
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
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: case hg
z : ℍ
d : ℕ+
⊢ Summable fun n ↦ (-↑↑d - ↑z * ↑↑n)⁻¹ - (↑↑d - ↑z * ↑↑n)⁻¹

Tactic:
apply (summable_pnat_iff_summable_nat.mpr ((summable_int_iff_summable_nat_and_neg.mp
        (summable_left_one_div_linear_sub_one_div_linear z (-d) d)).2)).congr

Goal state after:
case hg
z : ℍ
d : ℕ+
⊢ ∀ (b : ℕ+), 1 / (↑(-↑↑b) * ↑z + ↑(-↑↑d)) - 1 / (↑(-↑↑b) * ↑z + ↑↑↑d) = (-↑↑d - ↑z * ↑↑b)⁻¹ - (↑↑d - ↑z * ↑↑b)⁻¹
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
i : ℕ
⊢ ↑p ^ 2 ∣ (↑p * b) ^ 2

Tactic:
by simp only [mul_pow, dvd_mul_right]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : v.IsReal
⊢ Function.Surjective ⇑(extensionEmbeddingOfIsReal hv)

Tactic:
by
  rw [← RingHom.fieldRange_eq_top_iff, ← Real.subfield_eq_of_closed]
  exact isClosed_image_extensionEmbeddingOfIsReal hv

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ emultiplicity (↑p) ((x ^ p ^ multiplicity p (n + 1)) ^ k - (y ^ p ^ multiplicity p (n + 1)) ^ k) =
    emultiplicity (↑p) (x - y) + emultiplicity p (n + 1)

Tactic:
Nat.prime_iff_prime_int

Goal state after:
case succ
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ emultiplicity (↑p) ((x ^ p ^ multiplicity p (n + 1)) ^ k - (y ^ p ^ multiplicity p (n + 1)) ^ k) =
    emultiplicity (↑p) (x - y) + emultiplicity p (n + 1)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Set.univ ×ˢ ((Pi.map fun x ↦ ↑polarCoord.symm) '' Set.univ.pi fun x ↦ polarCoord.target) =ᵐ[volume.prod volume]
    Set.univ ×ˢ Set.univ

Tactic:
exact set_prod_ae_eq .rfl pi_polarCoord_symm_target_ae_eq_univ

Goal state after: