mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case inr
K : Type u_6
inst✝³ : Field K
ι : Type u_7
ι' : Type u_8
inst✝² : Fintype ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h : ∀ (k : ι), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (M + N)
h✝ : Nonempty ι'
q' : ι × ι' → K := fun a ↦ (eval x) (q a)
H : mulHeight x ^ (M + N) ≤ ↑(Nat.card ι') ^ totalWeight K * mulHeight q' * mulHeight fun j ↦ (eval x) (p j)
⊢ (↑(Nat.card ι') ^ totalWeight K * (max (mulHeightBound q) 1 * mulHeight x ^ M) * mulHeight fun j ↦ (eval x) (p j)) ≤
    (↑(Nat.card ι') ^ totalWeight K * max (mulHeightBound q) 1 * mulHeight fun j ↦ (eval x) (p j)) * mulHeight x ^ M

Tactic:
exact Eq.le (by ring)

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ deriv riemannZeta 0 = -log (2 * ↑π) / 2

Tactic:
by
  rw [funext riemannZeta_eq_mul_completedRiemannZeta₀]
  apply HasDerivAt.deriv
  have h₁ : HasDerivAt ((id * completedRiemannZeta₀ - 1) - id / (1 - id)) _ 0 :=
    .sub
      (.sub (.mul (hasDerivAt_id 0) differentiable_completedZeta₀.differentiableAt.hasDerivAt)
        (hasDerivAt_const 0 1))
      (.div (hasDerivAt_id 0) (.sub (hasDerivAt_const 0 1) (hasDerivAt_id 0)) (by simp))
  have h₂ : HasDerivAt ((fun x : ℂ => 2) * fun (x : ℂ) => (π : ℂ) ^ (-x / 2)) _ 0 :=
    .mul (hasDerivAt_const 0 2) <|
    .cpow (hasDerivAt_const 0 _) (.div_const (.neg <| hasDerivAt_id 0) 2) (by simp [Real.pi_pos])
  have h₃ : HasDerivAt (Gamma ∘ fun x => x / 2 + 1) (deriv Gamma (0 / 2 + 1) * (1 / 2 + 0)) 0 := by
    refine (differentiableAt_Gamma _ ?_).hasDerivAt.comp 0 ?_
    · simp only [zero_div]
      norm_cast
      simp
    · exact ((hasDerivAt_id 0).div_const 2).add (hasDerivAt_const 0 1)
  suffices h : -(log (2 * π) * 2) = γ - log (2 * 2 * π) + (-log π + -γ) by
    norm_num only at h
    convert! h₁.mul ((h₂.mul h₃).inv (by simp)) using 1
    simpa [completedRiemannZeta₀_zero, hasDerivAt_Gamma_one.deriv, field]
  open ComplexOrder in
  repeat rw [log_mul (by positivity) (by positivity) (by simp [arg, LT.lt.le, Real.pi_pos])]
  ring

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

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective ⇑(algebraMap F' FF')
Hχφ : χ' * φ' ≠ 1
Hχφ' : χ'⁻¹ * φ'⁻¹ ≠ 1
Hχ : χ' ≠ 1
Hφ : φ' ≠ 1
Hcard : ↑(Fintype.card F) ≠ 0
H : gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ ≠ 0
⊢ jacobiSum (χ.ringHomComp (algebraMap F' FF')) (φ.ringHomComp (algebraMap F' FF')) *
      jacobiSum (χ⁻¹.ringHomComp (algebraMap F' FF')) (φ⁻¹.ringHomComp (algebraMap F' FF')) =
    (algebraMap F' FF') ↑(Fintype.card F)

Tactic:
apply_fun (gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ * ·)
    using mul_right_injective₀ H

Goal state after:
F : Type u_1
F' : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective ⇑(algebraMap F' FF')
Hχφ : χ' * φ' ≠ 1
Hχφ' : χ'⁻¹ * φ'⁻¹ ≠ 1
Hχ : χ' ≠ 1
Hφ : φ' ≠ 1
Hcard : ↑(Fintype.card F) ≠ 0
H : gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ ≠ 0
⊢ (fun x ↦ gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ * x)
      (jacobiSum (χ.ringHomComp (algebraMap F' FF')) (φ.ringHomComp (algebraMap F' FF')) *
        jacobiSum (χ⁻¹.ringHomComp (algebraMap F' FF')) (φ⁻¹.ringHomComp (algebraMap F' FF'))) =
    (fun x ↦ gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ * x) ((algebraMap F' FF') ↑(Fintype.card F))
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℝ
hs : s > 1
⊢ ↑s ≠ 1

Tactic:
aesop

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

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hn' : n ∣ Fintype.card F - 1
hμ : IsPrimitiveRoot μ n
⊢ ∃ z ∈ ℤ[μ], jacobiSum χ ψ = -1 + z * (μ - 1) ^ 2

Tactic:
obtain ⟨q, hq⟩ := hn'

Goal state after:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F - 1 = n * q
⊢ ∃ z ∈ ℤ[μ], jacobiSum χ ψ = -1 + z * (μ - 1) ^ 2
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: case neg
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
J : Ideal S
hJ : J ∉ normalizedFactors (Ideal.map (algebraMap R S) I)
⊢ Multiset.count J (normalizedFactors (Ideal.map (algebraMap R S) I)) =
    Multiset.count J
      (Multiset.map (fun f ↦ ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f))
        (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach)

Tactic:
rw [Multiset.count_eq_zero.mpr hJ, eq_comm, Multiset.count_eq_zero, Multiset.mem_map]
    simp only [not_exists]
    rintro J' ⟨_, rfl⟩
    exact
      hJ ((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J').prop

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

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

Tactic:
rw [bernoulliFourierCoeff_recurrence 1 hn]
    simp only [Nat.cast_one, tsub_self, neg_mul, one_mul, if_true,
      Nat.factorial_one, pow_one]
    rw [bernoulli_zero_fourier_coeff hn, sub_zero, mul_one, div_neg, neg_div]

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

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

Tactic:
neg_one_mul (-1),

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

Goal state before:
pp: f : ℕ → ℂ
c s a : ℂ
hf : LSeriesHasSum f s a
⊢ LSeriesHasSum (c • f) s (c * a)

Tactic:
simpa [LSeriesHasSum, term_smul] using! hf.const_smul c

Goal state after:
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 < ⊤
F : ℝ → ℕ → ℂ := fun x ↦ {m | n + 1 < m}.indicator fun m ↦ f m / (↑m / (↑n + 1)) ^ ↑x
x : ℝ
m : ℕ
hm : m ≤ n + 1
⊢ F x m = 0

Tactic:
simp [F, not_lt_of_ge hm]

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

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

Tactic:
apply Countable.union <;>
      split_ifs <;>
      simp only [countable_singleton, countable_empty]

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := ⋯
G : ℂ → ℂ := ⋯
U : Set ℂ := ⋯
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
hUp : IsPreconnected U
hF : AnalyticOnNhd ℂ F U
t : ℂ
ht : t ∈ U
⊢ DifferentiableAt ℂ (completedLFunction (𝓕 Φ)) t

Tactic:
apply differentiableAt_completedLFunction _ _ (ht.1.imp_right fun h ↦ dft_apply_zero Φ ▸ h)

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := ⋯
G : ℂ → ℂ := ⋯
U : Set ℂ := ⋯
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
hUp : IsPreconnected U
hF : AnalyticOnNhd ℂ F U
t : ℂ
ht : t ∈ U
⊢ t ≠ 1 ∨ ∑ j, 𝓕 Φ j = 0
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
⊢ ((s - 1) * deriv (LFunctionTrivChar q) s + LFunctionTrivChar q s) /
      Function.update (fun s ↦ (s - 1) * LFunctionTrivChar q s) 1 (∏ p ∈ q.primeFactors, (1 - (↑p)⁻¹)) s =
    deriv (LFunction 1) s / LFunction 1 s + 1 / (s - 1)

Tactic:
Function.update_of_ne hs₁,

Goal state after:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
hs₁ : s ≠ 1
⊢ ((s - 1) * deriv (LFunctionTrivChar q) s + LFunctionTrivChar q s) / ((s - 1) * LFunctionTrivChar q s) =
    deriv (LFunction 1) s / LFunction 1 s + 1 / (s - 1)
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: case e_a
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ L (fun n ↦ ↑(residueClass a n)) ↑x = ↑(L (fun n ↦ ↑(residueClass a n)) ↑x).re

pp: case e_a
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ (↑q.totient)⁻¹ / (↑x - 1) = ↑((↑q.totient)⁻¹ / (↑x - 1)).re

Tactic:
· rw [LSeries, re_tsum <| LSeriesSummable_of_abscissaOfAbsConv_lt_re <|
      (abscissaOfAbsConv_residueClass_le_one a).trans_lt <| by norm_cast]
    push_cast
    refine tsum_congr fun n ↦ ?_
    rcases eq_or_ne n 0 with rfl | hn
    · simp only [term_zero, zero_re, ofReal_zero]
    · simp only [term_of_ne_zero hn, ← ofReal_natCast n, ← ofReal_cpow n.cast_nonneg, ← ofReal_div,
        ofReal_re]

Goal state after:
case e_a
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ (↑q.totient)⁻¹ / (↑x - 1) = ↑((↑q.totient)⁻¹ / (↑x - 1)).re
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: case refine_1
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n ↦ ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n ↦ ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖↑x ^ (-s)‖) t
h₄ : (deriv fun t ↦ ‖↑t ^ (-s)‖) =ᶠ[atTop] fun t ↦ -s.re * t ^ (-(s.re + 1))
⊢ LocallyIntegrableOn (deriv fun t ↦ ‖↑t ^ (-s)‖) (Set.Ici 1) volume

pp: case refine_2
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n ↦ ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n ↦ ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖↑x ^ (-s)‖) t
h₄ : (deriv fun t ↦ ‖↑t ^ (-s)‖) =ᶠ[atTop] fun t ↦ -s.re * t ^ (-(s.re + 1))
⊢ (fun n ↦ ‖↑↑n ^ (-s)‖ * ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun x ↦ 1

pp: case refine_3
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n ↦ ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n ↦ ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖↑x ^ (-s)‖) t
h₄ : (deriv fun t ↦ ‖↑t ^ (-s)‖) =ᶠ[atTop] fun t ↦ -s.re * t ^ (-(s.re + 1))
⊢ (fun t ↦ deriv (fun t ↦ ‖↑t ^ (-s)‖) t * ∑ k ∈ Icc 1 ⌊t⌋₊, ‖f k‖) =O[atTop] fun t ↦ t ^ (-(s.re + 1) + r)

pp: case refine_4
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n ↦ ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n ↦ ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖↑x ^ (-s)‖) t
h₄ : (deriv fun t ↦ ‖↑t ^ (-s)‖) =ᶠ[atTop] fun t ↦ -s.re * t ^ (-(s.re + 1))
⊢ IntegrableAtFilter (fun t ↦ t ^ (-(s.re + 1) + r)) atTop volume

Tactic:
· refine (Iff.mpr integrableOn_Ici_iff_integrableOn_Ioi
      (integrableOn_Ioi_deriv_norm_ofReal_cpow zero_lt_one ?_)).locallyIntegrableOn
    exact neg_re _ ▸ neg_nonpos.mpr <| hr.trans hs.le

Goal state after:
case refine_2
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n ↦ ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n ↦ ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖↑x ^ (-s)‖) t
h₄ : (deriv fun t ↦ ‖↑t ^ (-s)‖) =ᶠ[atTop] fun t ↦ -s.re * t ^ (-(s.re + 1))
⊢ (fun n ↦ ‖↑↑n ^ (-s)‖ * ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun x ↦ 1

case refine_3
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n ↦ ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n ↦ ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖↑x ^ (-s)‖) t
h₄ : (deriv fun t ↦ ‖↑t ^ (-s)‖) =ᶠ[atTop] fun t ↦ -s.re * t ^ (-(s.re + 1))
⊢ (fun t ↦ deriv (fun t ↦ ‖↑t ^ (-s)‖) t * ∑ k ∈ Icc 1 ⌊t⌋₊, ‖f k‖) =O[atTop] fun t ↦ t ^ (-(s.re + 1) + r)

case refine_4
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n ↦ ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n ↦ ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖↑x ^ (-s)‖) t
h₄ : (deriv fun t ↦ ‖↑t ^ (-s)‖) =ᶠ[atTop] fun t ↦ -s.re * t ^ (-(s.re + 1))
⊢ IntegrableAtFilter (fun t ↦ t ^ (-(s.re + 1) + r)) atTop volume
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: case refine_2
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n ↦ ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n ↦ ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖↑x ^ (-s)‖) t
h₄ : (deriv fun t ↦ ‖↑t ^ (-s)‖) =ᶠ[atTop] fun t ↦ -s.re * t ^ (-(s.re + 1))
⊢ (fun n ↦ ‖↑↑n ^ (-s)‖) =O[atTop] fun n ↦ ↑n ^ (-s).re

Tactic:
exact (norm_ofReal_cpow_eventually_eq_atTop _).isBigO.natCast_atTop

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

Goal state before:
pp: f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ↑x ^ (-s)) t
n : ℕ
⊢ 0 ∉ Icc (0 + 1) n

Tactic:
aesop

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

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
e : ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)
⊢ IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean (ValueGroupWithZero R)

Tactic:
let x := e.symm (exp (-1))

Goal state after:
case mp
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
e : ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)
x : ValueGroupWithZero R := e.symm (exp (-1))
⊢ IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean (ValueGroupWithZero R)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
b : ℕ
h : J(a | b) = 0
⊢ b ≠ 0 ∧ a.gcd ↑b ≠ 1

Tactic:
by
    rcases eq_or_ne b 0 with hb | hb
    · rw [hb, zero_right] at h; cases h
    exact ⟨hb, mt jacobiSym.ne_zero <| Classical.not_not.2 h⟩

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

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

Tactic:
convert! ← mul_one (M := ℤ) _

Goal state after:
case e'_2.e'_6
a✝ b : ℕ
ha : Odd a✝
hb : Odd b
a : ℕ
⊢ 1 = J(↑1 | a)

case e'_3
a✝ b : ℕ
ha : Odd a✝
hb : Odd b
a : ℕ
⊢ qrSign 1 a = 1
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
⊢ x * y * a * y = y * x * a * y

Tactic:
by rw [hx1]

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

Tactic:
by rw [hx1]

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
x y z : X q
⊢ x * y * z = x * (y * z)

Tactic:
ext <;> dsimp

Goal state after:
case h₁
q : ℕ
x y z : X q
⊢ (x.1 * y.1 + 3 * x.2 * y.2) * z.1 + 3 * (x.1 * y.2 + x.2 * y.1) * z.2 =
    x.1 * (y.1 * z.1 + 3 * y.2 * z.2) + 3 * x.2 * (y.1 * z.2 + y.2 * z.1)

case h₂
q : ℕ
x y z : X q
⊢ (x.1 * y.1 + 3 * x.2 * y.2) * z.2 + (x.1 * y.2 + x.2 * y.1) * z.1 =
    x.1 * (y.1 * z.2 + y.2 * z.1) + x.2 * (y.1 * z.1 + 3 * y.2 * z.2)
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: n : ℕ
B : ℝ≥0
h_card :
  {p | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff ↑i‖ ≤ ↑(n.choose ↑i) * ↑B}.ncard =
    ∏ i, (2 * ⌊↑(n.choose ↑i) * B⌋₊ + 1)
p : ℤ[X]
hp : p.natDegree ≤ n
hB : (map (castRingHom ℂ) p).mahlerMeasure ≤ ↑B
d : Fin (n + 1)
⊢ ‖p.coeff ↑d‖ = ‖(map (castRingHom ℂ) p).coeff ↑d‖

Tactic:
aesop

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
x y z : X q
⊢ x * (y + z) = x * y + x * z

Tactic:
ext <;> dsimp

Goal state after:
case h₁
q : ℕ
x y z : X q
⊢ x.1 * (y.1 + z.1) + 3 * x.2 * (y.2 + z.2) = x.1 * y.1 + 3 * x.2 * y.2 + (x.1 * z.1 + 3 * x.2 * z.2)

case h₂
q : ℕ
x y z : X q
⊢ x.1 * (y.2 + z.2) + x.2 * (y.1 + z.1) = x.1 * y.2 + x.2 * y.1 + (x.1 * z.2 + x.2 * z.1)
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
x y z : X q
⊢ (x + y) * z = x * z + y * z

Tactic:
ext <;> dsimp

Goal state after:
case h₁
q : ℕ
x y z : X q
⊢ (x.1 + y.1) * z.1 + 3 * (x.2 + y.2) * z.2 = x.1 * z.1 + 3 * x.2 * z.2 + (y.1 * z.1 + 3 * y.2 * z.2)

case h₂
q : ℕ
x y z : X q
⊢ (x.1 + y.1) * z.2 + (x.2 + y.2) * z.1 = x.1 * z.2 + x.2 * z.1 + (y.1 * z.2 + y.2 * z.1)
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
x✝¹ x✝ : X q
⊢ x✝¹ * x✝ = x✝ * x✝¹

Tactic:
ext <;> dsimp

Goal state after:
case h₁
q : ℕ
x✝¹ x✝ : X q
⊢ x✝¹.1 * x✝.1 + 3 * x✝¹.2 * x✝.2 = x✝.1 * x✝¹.1 + 3 * x✝.2 * x✝¹.2

case h₂
q : ℕ
x✝¹ x✝ : X q
⊢ x✝¹.1 * x✝.2 + x✝¹.2 * x✝.1 = x✝.1 * x✝¹.2 + x✝.2 * x✝¹.1
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hX : ¬X ∣ p
hpdeg : p.degree ≠ 0
hpdegC : (map (castRingHom ℂ) p).degree ≠ 0
z : ℂ
h✝ : eval z (map (castRingHom ℂ) p) = 0
hz₀ : z ≠ 0
⊢ z ∈ p.aroots ℂ

Tactic:
aesop

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
exact mod_cast h

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

Goal state before:
pp: n✝ : Type u_1
inst✝¹ : Fintype n✝
inst✝ : DecidableEq n✝
Γ : Subgroup (GL (Fin 2) ℝ)
h : Γ.IsArithmetic
g : GL (Fin 2) ℝ
hg : g ∈ Γ
n : ℕ
hn : 0 < n
left✝ : n ≤ (mapGL ℝ).range.relIndex Γ
hgn : g ^ n ∈ (mapGL ℝ).range ⊓ Γ
this : |↑(GeneralLinearGroup.det g ^ n)| = 1
⊢ |↑(GeneralLinearGroup.det g)| = 1

Tactic:
by simpa [← abs_pow, abs_pow_eq_one _ (Nat.ne_zero_of_lt hn)]

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

Goal state before:
pp: case inl.inl
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
a✝ b✝ : GL n R
ha : a✝ ∈ 𝒢
hb : b✝ ∈ 𝒢
this : a✝ * b✝ ∈ 𝒢
⊢ a✝ * b✝ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}

Tactic:
aesop

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

Goal state before:
pp: case inl.inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
a✝ b✝ : GL n R
ha : a✝ ∈ 𝒢
hb : -b✝ ∈ 𝒢
this : a✝ * -b✝ ∈ 𝒢
⊢ a✝ * b✝ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}

Tactic:
aesop

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

Goal state before:
pp: case inr.inl
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
a✝ b✝ : GL n R
ha : -a✝ ∈ 𝒢
hb : b✝ ∈ 𝒢
this : -a✝ * b✝ ∈ 𝒢
⊢ a✝ * b✝ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}

Tactic:
aesop

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

Goal state before:
pp: case inr.inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
a✝ b✝ : GL n R
ha : -a✝ ∈ 𝒢
hb : -b✝ ∈ 𝒢
this : -a✝ * -b✝ ∈ 𝒢
⊢ a✝ * b✝ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}

Tactic:
aesop

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

Goal state before:
pp: case inl
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
x✝ : GL n R
ha : x✝ ∈ 𝒢
this : x✝⁻¹ ∈ 𝒢
⊢ x✝⁻¹ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}

Tactic:
aesop

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

Goal state before:
pp: case inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
x✝ : GL n R
ha : -x✝ ∈ 𝒢
this : (-x✝)⁻¹ ∈ 𝒢
⊢ x✝⁻¹ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}

Tactic:
aesop

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

Goal state before:
pp: case h
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
b✝ : CuspOrbits 𝒢
g : SL(2, ℤ)
hc : IsCusp ((mapGL ℝ) g • ∞) 𝒢
⊢ cosetToCuspOrbit 𝒢 ⟦g⁻¹⟧ = Quot.mk ⇑(MulAction.orbitRel ↥𝒢 ↥(cuspsSubMulAction 𝒢)) ⟨(mapGL ℝ) g • ∞, hc⟩

Tactic:
aesop

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

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
⊢ 0 ≤ if h : DiscreteTopology ↥𝒢.strictPeriods then |⋯.choose| else 0

Tactic:
aesop

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

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
⊢ 0 ≤ 𝒢.strictWidthInfty

Tactic:
unfold strictWidthInfty; aesop

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

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

Tactic:
have hsp := strictPeriods_Gamma N
  rw [strictPeriods_eq_zmultiples_strictWidthInfty, Eq.comm,
    AddSubgroup.zmultiples_eq_zmultiples_iff
      (not_isOfFinAddOrder_of_isAddTorsionFree (NeZero.ne _))] at hsp
  grind [strictWidthInfty_nonneg, Nat.cast_nonneg]

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

Goal state before:
pp: case pos
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst✝ : SlashInvariantFormClass F Γ k
hΓ : h ∈ Γ.strictPeriods
w : ℂ
hw : 0 < w.im
this : 0 < (w + ↑h).im
⊢ f { coe := w + ↑h, coe_im_pos := this } = f { coe := w, coe_im_pos := hw }

Tactic:
convert! SlashInvariantForm.vAdd_apply_of_mem_strictPeriods f ⟨w, hw⟩ hΓ using 2

Goal state after:
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst✝ : SlashInvariantFormClass F Γ k
hΓ : h ∈ Γ.strictPeriods
w : ℂ
hw : 0 < w.im
this : 0 < (w + ↑h).im
⊢ { coe := w + ↑h, coe_im_pos := this } = h +ᵥ { coe := w, coe_im_pos := hw }
Module: Mathlib.NumberTheory.ModularForms.Petersson

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

Tactic:
zpow_neg,

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