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

Goal state before:
pp: case b0
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
A : ι' × ι → K
x : ι → K
h✝¹ : Nonempty ι
h✝ : Nonempty ι'
j : ι'
this : ∀ (f : ι → ℝ), ⨆ i, f ↑i = ⨆ i, f i
i : ι
⊢ 0 ≤ ⨆ ji, v (A ji)

pp: case h₁
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
A : ι' × ι → K
x : ι → K
h✝¹ : Nonempty ι
h✝ : Nonempty ι'
j : ι'
this : ∀ (f : ι → ℝ), ⨆ i, f ↑i = ⨆ i, f i
i : ι
⊢ v (A (j, i)) ≤ ⨆ ji, v (A ji)

pp: case h₂
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
A : ι' × ι → K
x : ι → K
h✝¹ : Nonempty ι
h✝ : Nonempty ι'
j : ι'
this : ∀ (f : ι → ℝ), ⨆ i, f ↑i = ⨆ i, f i
i : ι
⊢ v (x i) ≤ ⨆ i, v (x i)

Tactic:
· exact Real.iSup_nonneg_of_nonnegHomClass v _

Goal state after:
case h₁
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
A : ι' × ι → K
x : ι → K
h✝¹ : Nonempty ι
h✝ : Nonempty ι'
j : ι'
this : ∀ (f : ι → ℝ), ⨆ i, f ↑i = ⨆ i, f i
i : ι
⊢ v (A (j, i)) ≤ ⨆ ji, v (A ji)

case h₂
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
A : ι' × ι → K
x : ι → K
h✝¹ : Nonempty ι
h✝ : Nonempty ι'
j : ι'
this : ∀ (f : ι → ℝ), ⨆ i, f ↑i = ⨆ i, f i
i : ι
⊢ v (x i) ≤ ⨆ i, v (x i)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case b0
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
inst✝ : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
s : ι →₀ ℕ
hs₁ : s ∈ p.support
hs₂ : v (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, x i ^ d i) ≤ v (coeff s p * ∏ i ∈ s.support, x i ^ s i)
⊢ 0 ≤ ⨆ s, v (coeff (↑s) p)

pp: case h₁
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
inst✝ : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
s : ι →₀ ℕ
hs₁ : s ∈ p.support
hs₂ : v (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, x i ^ d i) ≤ v (coeff s p * ∏ i ∈ s.support, x i ^ s i)
⊢ v (coeff s p) ≤ ⨆ s, v (coeff (↑s) p)

pp: case h₂
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
inst✝ : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
s : ι →₀ ℕ
hs₁ : s ∈ p.support
hs₂ : v (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, x i ^ d i) ≤ v (coeff s p * ∏ i ∈ s.support, x i ^ s i)
⊢ ∏ x_1 ∈ s.support, v (x x_1) ^ s x_1 ≤ (⨆ i, v (x i)) ^ N

Tactic:
· exact Real.iSup_nonneg_of_nonnegHomClass v _

Goal state after:
case h₁
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
inst✝ : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
s : ι →₀ ℕ
hs₁ : s ∈ p.support
hs₂ : v (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, x i ^ d i) ≤ v (coeff s p * ∏ i ∈ s.support, x i ^ s i)
⊢ v (coeff s p) ≤ ⨆ s, v (coeff (↑s) p)

case h₂
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
inst✝ : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
s : ι →₀ ℕ
hs₁ : s ∈ p.support
hs₂ : v (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, x i ^ d i) ≤ v (coeff s p * ∏ i ∈ s.support, x i ^ s i)
⊢ ∏ x_1 ∈ s.support, v (x x_1) ^ s x_1 ≤ (⨆ i, v (x i)) ^ N
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case e_a
N : ℕ
s : ℝ
hs : 1 < s
⊢ ∑ x ∈ Finset.range N, ↑(x + 1) / s * (1 / ↑(x + 1) ^ s - 1 / (↑(x + 1) + 1) ^ s) =
    1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s)

Tactic:
simp_rw [mul_comm (_ / _), ← mul_div_assoc, div_eq_mul_inv _ s, ← Finset.sum_mul, mul_one]
    congr 1
    induction N with
    | zero => simp
    | succ N hN =>
      simp_rw [Finset.sum_range_succ, hN, Nat.cast_add_one, sub_eq_add_neg, add_assoc]
      congr 1
      ring_nf

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

Goal state before:
pp: case refine_2.refine_2.hf
f : ℂ → ℂ := ⋯
⊢ Tendsto (fun x ↦ f x * (x - 1)) (𝓝[≠] 1) (𝓝 (1 - 1))

Tactic:
simp_rw [mul_comm (f _), f, mul_sub]

Goal state after:
case refine_2.refine_2.hf
f : ℂ → ℂ := fun s ↦ riemannZeta s - 1 / (s - 1)
⊢ Tendsto (fun x ↦ (x - 1) * riemannZeta x - (x - 1) * (1 / (x - 1))) (𝓝[≠] 1) (𝓝 (1 - 1))
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ φ : MulChar F R
h : χ * φ ≠ 1
ψ : AddChar F R
sum_eq : ∀ t ∈ univ \ {0}, (∑ x, χ x * φ (t - x)) * ψ t = (∑ y, χ (t * y) * φ (t - t * y)) * ψ t
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ = ∑ x ∈ univ \ {0}, ∑ x_1, χ x_1 * φ (x - x_1) * ψ x

Tactic:
simp_rw [← sum_mul, sum_congr rfl sum_eq, ← mul_one_sub, map_mul, mul_assoc]

Goal state after:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ φ : MulChar F R
h : χ * φ ≠ 1
ψ : AddChar F R
sum_eq : ∀ t ∈ univ \ {0}, (∑ x, χ x * φ (t - x)) * ψ t = (∑ y, χ (t * y) * φ (t - t * y)) * ψ t
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ = ∑ x ∈ univ \ {0}, (∑ x_1, χ x * (χ x_1 * (φ x * φ (1 - x_1)))) * ψ x
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: case refine_3.refine_2
M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : s ≠ 1
hpc : IsPreconnected {1}ᶜ
hne : 2 ∈ {1}ᶜ
t : ℂ
ht : 1 < t.re
⊢ LFunction ((changeLevel hMN) χ) t = (fun s ↦ LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))) t

Tactic:
simpa [LFunction_eq_LSeries _ ht] using LSeries_changeLevel hMN χ ht

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
⊢ HasDerivAt (bernoulliFun k) (↑k * bernoulliFun (k - 1) x) x

Tactic:
by
  convert! ((Polynomial.bernoulli k).map <| algebraMap ℚ ℝ).hasDerivAt x using 1
  simp only [bernoulliFun, Polynomial.derivative_map, Polynomial.derivative_bernoulli k,
    Polynomial.map_mul, Polynomial.map_natCast, Polynomial.eval_mul, Polynomial.eval_natCast]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case hg
m : ℕ
m0 : m ≠ 0
x✝¹ : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
x : ℝ
i : ℕ
x✝ : i ∈ Finset.range m
⊢ HasDerivAt (fun x ↦ ↑m ^ k * bernoulliFun (k + 1) (x + ↑i / ↑m)) (↑m ^ k * (↑(k + 1) * bernoulliFun k (x + ↑i / ↑m)))
    x

Tactic:
apply HasDerivAt.const_mul

Goal state after:
case hg
m : ℕ
m0 : m ≠ 0
x✝¹ : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := ⋯
k : ℕ
h : ∀ (x : ℝ), f k x = 0
x : ℝ
i : ℕ
x✝ : i ∈ Finset.range m
⊢ HasDerivAt (fun y ↦ bernoulliFun (k + 1) (y + ↑i / ↑m)) (↑(k + 1) * bernoulliFun k (x + ↑i / ↑m)) x
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case neg
k : ℕ
k1 : ¬k = 1
⊢ bernoulliFun k 2⁻¹ = (2 / 2 ^ k - 1) * ↑(bernoulli k)

Tactic:
· have m := bernoulliFun_mul k two_ne_zero 2⁻¹
    simp_rw [Nat.cast_ofNat, mul_inv_cancel₀ (two_ne_zero' ℝ), Finset.sum_range_succ,
      Finset.sum_range_zero, Nat.cast_zero, Nat.cast_one, ← one_div, add_halves,
      bernoulliFun_eval_one, if_neg k1, bernoulliFun_eval_zero, zero_div, add_zero, zero_add] at m
    rw [← inv_mul_eq_iff_eq_mul₀ (by positivity), ← sub_eq_iff_eq_add, ← sub_one_mul, inv_div] at m
    rw [m, one_div]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 0
⊢ fourierCoeffOn bernoulliFourierCoeff._proof_1 (fun x ↦ ↑(bernoulliFun k x)) 0 = 0

Tactic:
fourierCoeffOn_eq_integral,

Goal state after:
k : ℕ
hk : k ≠ 0
⊢ (1 / (1 - 0)) • ∫ (x : ℝ) in 0..1, (fourier (-0)) ↑x • ↑(bernoulliFun k x) = 0
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: 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

Tactic:
refine .mul (by fun_prop) (hs₀.elim ?_ ?_)

Goal state after:
case refine_1.refine_1
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j, Φ j = 0
⊢ s ≠ 0 → DifferentiableAt ℂ (HDiv.hDiv (Φ 0)) s

case refine_1.refine_2
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j, Φ j = 0
⊢ Φ 0 = 0 → DifferentiableAt ℂ (HDiv.hDiv (Φ 0)) s
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
⊢ Summable fun pk ↦ (↑↑pk.1)⁻¹ ^ pk.2 * (↑↑pk.1)⁻¹ ^ (3 / 2)

Tactic:
refine (summable_prod_of_nonneg (fun _ ↦ by positivity)).mpr ⟨(fun p ↦ ?_), ?_⟩

Goal state after:
case refine_1
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
⊢ Summable fun y ↦ (↑↑(p, y).1)⁻¹ ^ (p, y).2 * (↑↑(p, y).1)⁻¹ ^ (3 / 2)

case refine_2
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
⊢ Summable fun x ↦ ∑' (y : ℕ), (↑↑(x, y).1)⁻¹ ^ (x, y).2 * (↑↑(x, y).1)⁻¹ ^ (3 / 2)
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero 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
⊢ ‖LSeries (fun x ↦ 1 ↑x) (1 + ↑x) ^ 3 * LSeries (fun x ↦ χ ↑x) (1 + ↑x + I * ↑y) ^ 4 *
        LSeries (fun x ↦ (χ ^ 2) ↑x) (1 + ↑x + 2 * I * ↑y)‖ ≥
    1

Tactic:
exact norm_LSeries_product_ge_one χ hx y

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
⊢ L (fun n ↦ ↑(residueClass a n)) s = -(↑q.totient)⁻¹ * ∑ χ, χ a⁻¹ * (deriv (LFunction χ) s / LFunction χ s)

Tactic:
simp only [deriv_LFunction_eq_deriv_LSeries _ hs, LFunction_eq_LSeries _ hs, neg_mul, ← mul_neg,
    ← Finset.sum_neg_distrib, ← neg_div, ← LSeries_twist_vonMangoldt_eq _ hs]
  rw [eq_inv_mul_iff_mul_eq₀ <| mod_cast (Nat.totient_pos.mpr q.pos_of_neZero).ne']
  simp_rw [← LSeries_smul,
    ← LSeries_sum <| fun χ _ ↦ (LSeriesSummable_twist_vonMangoldt χ hs).smul _]
  refine LSeries_congr (fun {n} _ ↦ ?_) s
  simp only [Pi.smul_apply, residueClass_apply ha, smul_eq_mul, ← mul_assoc,
    mul_inv_cancel_of_invertible, one_mul, Finset.sum_apply, Pi.mul_apply]

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
| deriv (LFunction 1) s / LFunction 1 s + LFunction 1 s / ((s - 1) * LFunction 1 s)

Tactic:
enter [2, 1]

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
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
⊢ ∃ C, ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x

Tactic:
have H {x : ℝ} (hx : 1 < x) :
      ∑' n, residueClass a n / (n : ℝ) ^ x =
        (LFunctionResidueClassAux a x).re + (q.totient : ℝ)⁻¹ / (x - 1) := by
    refine ofReal_injective ?_
    simp only [ofReal_tsum, ofReal_div, ofReal_cpow (Nat.cast_nonneg _), ofReal_natCast,
      ofReal_add, ofReal_inv, ofReal_sub, ofReal_one]
    simp_rw [← LFunctionResidueClassAux_real ha hx,
      eqOn_LFunctionResidueClassAux ha <| Set.mem_ofPred.mpr (ofReal_re x ▸ hx), sub_add_cancel,
      LSeries, term]
    refine tsum_congr fun n ↦ ?_
    split_ifs with hn
    · simp only [hn, residueClass_apply_zero, ofReal_zero, zero_div]
    · rfl
  have : ContinuousOn (fun x : ℝ ↦ (LFunctionResidueClassAux a x).re) (Set.Icc 1 2) :=
    continuous_re.continuousOn.comp (t := Set.univ) (continuousOn_LFunctionResidueClassAux a)
      (fun ⦃x⦄ a ↦ trivial) |>.comp continuous_ofReal.continuousOn fun x hx ↦ by
        simpa only [Set.mem_ofPred_eq, ofReal_re] using hx.1
  obtain ⟨C, hC⟩ := bddBelow_def.mp <| IsCompact.bddBelow_image isCompact_Icc this
  replace hC {x : ℝ} (hx : x ∈ Set.Icc 1 2) : C ≤ (LFunctionResidueClassAux a x).re :=
    hC (LFunctionResidueClassAux a x).re <|
      Set.mem_image_of_mem (fun x : ℝ ↦ (LFunctionResidueClassAux a x).re) hx
  refine ⟨-C, fun {x} hx ↦ ?_⟩
  rw [H hx.1, add_comm, sub_neg_eq_add, add_le_add_iff_left]
  exact hC <| Set.mem_Icc_of_Ioc hx

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_3
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
⊢ -((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x) * I / 2) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))

Tactic:
have : ∀ α β γ δ : ℂ, α * I * β / γ * δ * I = I ^ 2 * α * β / γ * δ := by intros; ring

Goal state after:
case e'_3
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this✝ :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
this : ∀ (α β γ δ : ℂ), α * I * β / γ * δ * I = I ^ 2 * α * β / γ * δ
⊢ -((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x) * I / 2) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))
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
⊢ LSeries f s = s * ∫ (t : ℝ) in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-(s + 1))

Tactic:
have h₄ : ∀ n, ∑ k ∈ Icc 0 n, f k = ∑ k ∈ Icc 1 n, f k := fun n ↦ by
    rw [← insert_Icc_add_one_left_eq_Icc n.zero_le, sum_insert (by aesop), hf, zero_add, zero_add]

Goal state after:
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
h₄ : ∀ (n : ℕ), ∑ k ∈ Icc 0 n, f k = ∑ k ∈ Icc 1 n, f k
⊢ LSeries f s = s * ∫ (t : ℝ) in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-(s + 1))
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: case inr
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable fun n ↦ (if Nat.Prime n then residueClass a n else 0) / ↑n
key : Summable fun n ↦ residueClass a n / ↑n
C : ℝ := ∑' (n : ℕ), residueClass a n / ↑n
H₁✝ : ∀ {x : ℝ}, 1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x ≤ C
C' : ℝ
hC' : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x
H₁ : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ ≤ (C + C') * (x - 1)
hq : 0 < (↑q.totient)⁻¹
h₀ : 0 < C + C'
⊢ False

Tactic:
· obtain ⟨ξ, hξ₁, hξ₂⟩ : ∃ ξ ∈ Set.Ioc 1 2, (C + C') * (ξ - 1) < (q.totient : ℝ)⁻¹ := by
      refine ⟨min (1 + (q.totient : ℝ)⁻¹ / (C + C') / 2) 2, ⟨?_, min_le_right ..⟩, ?_⟩
      · simpa only [lt_inf_iff, lt_add_iff_pos_right, Nat.ofNat_pos, div_pos_iff_of_pos_right,
          Nat.one_lt_ofNat, and_true] using div_pos hq h₀
      · rw [← min_sub_sub_right, add_sub_cancel_left, ← lt_div_iff₀' h₀]
        exact (min_le_left ..).trans_lt <| div_lt_self (div_pos hq h₀) one_lt_two
    exact ((H₁ hξ₁).trans_lt hξ₂).false

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

Goal state before:
pp: case refine_2
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ : LocallyIntegrableOn (fun t ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume
h₂ : (fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) =O[atTop] fun t ↦ t ^ 1
⊢ IntegrableAtFilter (fun t ↦ t ^ (-s)) atTop volume

Tactic:
rwa [integrableAtFilter_rpow_atTop_iff, neg_lt_neg_iff]

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

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

Tactic:
rintro ⟨x, hx⟩

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

Goal state before:
pp: a : ℤ
n : ℕ
h : J(a | n) = -1
hn₀ : n ≠ 0
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ J(a | p) = -1

Tactic:
have hf₀ (p) (hp : p ∈ n.primeFactorsList) : p ≠ 0 := (Nat.pos_of_mem_primeFactorsList hp).ne.symm

Goal state after:
a : ℤ
n : ℕ
h : J(a | n) = -1
hn₀ : n ≠ 0
hf₀ : ∀ p ∈ n.primeFactorsList, p ≠ 0
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ J(a | p) = -1
Module: Mathlib.NumberTheory.LocalField.Basic

Goal state before:
pp: case inr
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
hr1 : 1 ≤ r
x : K
hx : (valuation K) x ≤ (valuation K) r'
⊢ (valuation K) x < r

Tactic:
exact hx.trans_lt (hr.trans_le hr1)

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: m n : ℕ
h : m < n
⊢ 2 ^ m < 2 ^ n

Tactic:
gcongr; norm_num1

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
hp : p ≠ 0
i : ℕ
⊢ sMod p i < 2 ^ p - 1

Tactic:
by
  rw [← sMod_mod]
  refine (Int.emod_lt_abs _ (mersenne_int_ne_zero p hp)).trans_eq ?_
  exact abs_of_nonneg (mersenne_int_pos hp).le

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

Tactic:
have prop := p.property.2

Goal state after:
case refine_1
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
p : ↑(boxPoly n B₁ B₂)
prop : ∀ (i : Fin (n + 1)), B₁ i ≤ ↑((↑p).coeff ↑i) ∧ ↑((↑p).coeff ↑i) ≤ B₂ i
⊢ (toFn (n + 1)) ↑p ∈ ↑(Finset.Icc (fun x ↦ ⌈B₁ x⌉) fun x ↦ ⌊B₂ x⌋)
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: Γ : Subgroup SL(2, ℤ)
g x : SL(2, ℤ)
⊢ (∃ y ∈ Γ,
      (SpecialLinearGroup.map (Int.castRingHom ℝ)) y = (SpecialLinearGroup.map (Int.castRingHom ℝ)) (g * x * g⁻¹)) ↔
    x ∈ toConjAct g⁻¹ • Γ

Tactic:
map_intCast_injective.eq_iff,

Goal state after:
Γ : Subgroup SL(2, ℤ)
g x : SL(2, ℤ)
⊢ (∃ y ∈ Γ, y = g * x * g⁻¹) ↔ x ∈ toConjAct g⁻¹ • Γ
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⁻¹
⊢ ∃ N, N ≠ 0 ∧ ∀ x ∈ Γ(N), g * (mapGL ℚ) x * g⁻¹ ∈ Subgroup.map (mapGL ℚ) Γ(M)

Tactic:
have hA₁₂ : A₁ * A₂ = 1 := by simp only [← Matrix.GeneralLinearGroup.coe_mul,
    mul_inv_cancel, Matrix.GeneralLinearGroup.coe_one, A₁, A₂]

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
⊢ ∃ N, N ≠ 0 ∧ ∀ x ∈ Γ(N), g * (mapGL ℚ) x * g⁻¹ ∈ Subgroup.map (mapGL ℚ) Γ(M)
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: β : Type u_1
G : Type u_2
α : Type u_3
inst✝² : Group G
inst✝¹ : AddGroup α
inst✝ : SlashAction β G α
k : β
g : G
a : α
⊢ a ∣[k] g = 0 ↔ a = 0

Tactic:
refine ⟨fun h ↦ ?_, by simp +contextual⟩

Goal state after:
β : Type u_1
G : Type u_2
α : Type u_3
inst✝² : Group G
inst✝¹ : AddGroup α
inst✝ : SlashAction β G α
k : β
g : G
a : α
h : a ∣[k] g = 0
⊢ a = 0
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)
⊢ (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:
have hR0 : 0 < R := Real.exp_pos _

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
⊢ (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 := ⋯ }
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case h
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
⊢ ∀ (z : ℍ), g • z = T ^ ↑g 0 1 • z

Tactic:
suffices g = T ^ g 0 1 by intro z; conv_lhs => rw [this]

Goal state after:
case h
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
⊢ g = T ^ ↑g 0 1
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
⊢ IsBoundedAtImInfty (⇑(eisensteinSeriesSIF a k) ∣[k] A)

Tactic:
simp_rw [UpperHalfPlane.isBoundedAtImInfty_iff, eisensteinSeriesSIF] at *

Goal state after:
N : ℕ
inst✝ : NeZero N
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
⊢ ∃ M A_1, ∀ (z : ℍ), A_1 ≤ z.im → ‖(⇑{ toFun := eisensteinSeries a k, slash_action_eq' := ⋯ } ∣[k] A) z‖ ≤ M
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
⊢ Summable fun a ↦ ‖↑(↑a.snd).2 ^ k * r ^ ((↑a.snd).1 * (↑a.snd).2)‖

Tactic:
rw [summable_sigma_of_nonneg (fun a ↦ by positivity)]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
⊢ (∀ (x : ℕ+), Summable fun y ↦ ‖↑(↑⟨x, y⟩.snd).2 ^ k * r ^ ((↑⟨x, y⟩.snd).1 * (↑⟨x, y⟩.snd).2)‖) ∧
    Summable fun x ↦
      ∑' (y : ↥(↑x).divisorsAntidiagonal), ‖↑(↑⟨x, y⟩.snd).2 ^ k * r ^ ((↑⟨x, y⟩.snd).1 * (↑⟨x, y⟩.snd).2)‖
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
⊢ Summable fun c ↦ ↑↑c.2 ^ k * r ^ (↑c.1 * ↑c.2)

Tactic:
simpa [sigmaAntidiagonalEquivProd.summable_iff.symm] using! summable_divisorsAntidiagonal_aux k hr

Goal state after:
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

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

Tactic:
rwa [← (summable_prod_mul_pow k hr).tsum_prod]

Goal state after: