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

Goal state before:
pp: ε : ℝ
εpos : 0 < ε
this : ∀ᶠ (x : ℝ) in atTop, ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖ ≤ ε * ‖x / log x‖
x : ℝ
hx : 2 ≤ x
hx2 : ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖ ≤ ε * ‖x / log x‖
⊢ ↑(π ⌊x⌋₊) ≤ (log 4 + ε) * x / log x

Tactic:
rw [primeCounting_eq_theta_div_log_add_integral hx, add_mul, add_div]

Goal state after:
ε : ℝ
εpos : 0 < ε
this : ∀ᶠ (x : ℝ) in atTop, ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖ ≤ ε * ‖x / log x‖
x : ℝ
hx : 2 ≤ x
hx2 : ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖ ≤ ε * ‖x / log x‖
⊢ θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2) ≤ log 4 * x / log x + ε * x / log x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ε : ℝ
εpos : 0 < ε
⊢ ∀ᶠ (x : ℝ) in atTop, ↑(π ⌊x⌋₊) ≤ (log 4 + ε) * x / log x

Tactic:
by
  have := integral_theta_div_log_sq_isLittleO.bound εpos
  filter_upwards [eventually_ge_atTop 2, this] with x hx hx2
  rw [primeCounting_eq_theta_div_log_add_integral hx, add_mul, add_div]
  have : 0 ≤ log x := by bound
  rw [norm_of_nonneg (show 0 ≤ x / log x by bound), ← mul_div_assoc] at hx2
  grw [theta_le_log4_mul_x (by linarith), ← hx2]
  grind [le_norm_self]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs

Goal state before:
pp: b : Basis (Fin 1) ℤ (𝓞 ℚ) := (Basis.singleton (Fin 1) ℤ).map ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm
⊢ (Algebra.trace ℤ (𝓞 ℚ))
      (ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm ((Basis.singleton (Fin 1) ℤ) default) *
        ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm ((Basis.singleton (Fin 1) ℤ) default)) =
    (Algebra.trace ℤ (𝓞 ℚ)) 1

Tactic:
RingEquiv.toAddEquiv_eq_coe,

Goal state after:
b : Basis (Fin 1) ℤ (𝓞 ℚ) := (Basis.singleton (Fin 1) ℤ).map ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm
⊢ (Algebra.trace ℤ (𝓞 ℚ))
      ((↑ringOfIntegersEquiv).toIntLinearEquiv.symm ((Basis.singleton (Fin 1) ℤ) default) *
        (↑ringOfIntegersEquiv).toIntLinearEquiv.symm ((Basis.singleton (Fin 1) ℤ) default)) =
    (Algebra.trace ℤ (𝓞 ℚ)) 1
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r s : R
⊢ nthHomSeq f_compat (r + s) ≈ nthHomSeq f_compat r + nthHomSeq f_compat s

Tactic:
intro ε hε
  obtain ⟨n, hn⟩ := exists_pow_neg_lt_rat p hε
  use n
  intro j hj
  dsimp [nthHomSeq]
  apply lt_of_le_of_lt _ hn
  rw [← Int.cast_add, ← Int.cast_sub, ← padicNorm.dvd_iff_norm_le, ←
    ZMod.intCast_zmod_eq_zero_iff_dvd]
  dsimp [nthHom]
  simp only [ZMod.natCast_val, map_add, Int.cast_sub, ZMod.intCast_cast, Int.cast_add]
  rw [ZMod.cast_add (show p ^ n ∣ p ^ j from pow_dvd_pow _ hj)]
  simp only [sub_self]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs

Goal state before:
pp: ι : Type u_2
ι' : Type u_3
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq ι'
inst✝² : Fintype ι
inst✝¹ : Fintype ι'
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (b.toMatrix (⇑b') i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (b'.toMatrix (⇑(b.reindex (b.indexEquiv b'))) i j)
hint : IsIntegral ℤ ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det
r : ℤ
hr : (algebraMap ℤ ℚ) r = ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det
this : IsIntegral ℤ (b'.toMatrix ⇑(b.reindex (b.indexEquiv b'))).det
r' : ℤ
hr' : (algebraMap ℤ ℚ) r' = (b'.toMatrix ⇑(b.reindex (b.indexEquiv b'))).det
⊢ Matrix.det 1 = 1

Tactic:
Matrix.det_one

Goal state after:
ι : Type u_2
ι' : Type u_3
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq ι'
inst✝² : Fintype ι
inst✝¹ : Fintype ι'
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (b.toMatrix (⇑b') i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (b'.toMatrix (⇑(b.reindex (b.indexEquiv b'))) i j)
hint : IsIntegral ℤ ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det
r : ℤ
hr : (algebraMap ℤ ℚ) r = ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det
this : IsIntegral ℤ (b'.toMatrix ⇑(b.reindex (b.indexEquiv b'))).det
r' : ℤ
hr' : (algebraMap ℤ ℚ) r' = (b'.toMatrix ⇑(b.reindex (b.indexEquiv b'))).det
⊢ 1 = 1
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case e_a
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
⊢ (-1) ^ (p ^ k * (p - 1) * (p ^ k * (p - 1) - 1) / 2) = (-1) ^ (p ^ k * (p - 1) / 2)

Tactic:
rcases eq_or_ne p 2 with (rfl | hp2)
    · rcases Nat.exists_eq_succ_of_ne_zero (hp2 rfl) with ⟨k, rfl⟩
      rw [succ_sub_succ_eq_sub, tsub_zero, mul_one]; simp only [_root_.pow_succ']
      rw [mul_assoc, Nat.mul_div_cancel_left _ zero_lt_two, Nat.mul_div_cancel_left _ zero_lt_two]
      cases k
      · simp
      · simp_rw [_root_.pow_succ', (even_two.mul_right _).neg_one_pow,
          ((even_two.mul_right _).mul_right _).neg_one_pow]
    · have hpo : Odd p := hp.out.odd_of_ne_two hp2
      obtain ⟨a, ha⟩ := (hp.out.even_sub_one hp2).two_dvd
      rw [ha, mul_left_comm, mul_assoc, Nat.mul_div_cancel_left _ two_pos,
        Nat.mul_div_cancel_left _ two_pos, mul_right_comm, pow_mul, (hpo.pow.mul _).neg_one_pow,
        pow_mul, hpo.pow.neg_one_pow]
      refine Nat.Even.sub_odd ?_ (even_two_mul _) odd_one
      rw [mul_left_comm, ← ha]
      exact one_le_mul (one_le_pow _ _ hp.1.pos) (succ_le_iff.2 <| tsub_pos_of_lt hp.1.one_lt)

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
b : ℤ√↑(d a1)
b1 : 1 ≤ b
hp : IsPell b
n : ℕ
h : b ≤ ↑n
⊢ ↑n ≤ pellZd a1 n

Tactic:
Zsqrtd.natCast_val

Goal state after:
a : ℕ
a1 : 1 < a
b : ℤ√↑(d a1)
b1 : 1 ≤ b
hp : IsPell b
n : ℕ
h : b ≤ ↑n
⊢ { re := ↑n, im := 0 } ≤ pellZd a1 n
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_1
d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe z 1 w d
this : 0 ≤ (↑(d * y * y) - ↑(1 * x * x)) * (↑(d * w * w) - ↑(1 * z * z))
⊢ SqLe (x * w + y * z) d (x * z + d * y * w) 1

Tactic:
refine Int.le_of_ofNat_le_ofNat (le_of_sub_nonneg ?_)

Goal state after:
case refine_1
d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe z 1 w d
this : 0 ≤ (↑(d * y * y) - ↑(1 * x * x)) * (↑(d * w * w) - ↑(1 * z * z))
⊢ 0 ≤ ↑(1 * (x * z + d * y * w) * (x * z + d * y * w)) - ↑(d * (x * w + y * z) * (x * w + y * z))
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_2
d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe w d z 1
this : 0 ≤ (↑(d * y * y) - ↑(1 * x * x)) * (↑(1 * z * z) - ↑(d * w * w))
⊢ SqLe (x * z + d * y * w) 1 (x * w + y * z) d

Tactic:
refine Int.le_of_ofNat_le_ofNat (le_of_sub_nonneg ?_)

Goal state after:
case refine_2
d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe w d z 1
this : 0 ≤ (↑(d * y * y) - ↑(1 * x * x)) * (↑(1 * z * z) - ↑(d * w * w))
⊢ 0 ≤ ↑(d * (x * w + y * z) * (x * w + y * z)) - ↑(1 * (x * z + d * y * w) * (x * z + d * y * w))
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_3
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe z 1 w d
this : 0 ≤ (↑(1 * x * x) - ↑(d * y * y)) * (↑(d * w * w) - ↑(1 * z * z))
⊢ SqLe (x * z + d * y * w) 1 (x * w + y * z) d

Tactic:
refine Int.le_of_ofNat_le_ofNat (le_of_sub_nonneg ?_)

Goal state after:
case refine_3
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe z 1 w d
this : 0 ≤ (↑(1 * x * x) - ↑(d * y * y)) * (↑(d * w * w) - ↑(1 * z * z))
⊢ 0 ≤ ↑(d * (x * w + y * z) * (x * w + y * z)) - ↑(1 * (x * z + d * y * w) * (x * z + d * y * w))
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n k : ℕ
⊢ yn a1 n ∣ yn a1 (n * (k + 1))

Tactic:
Nat.mul_succ,

Goal state after:
a : ℕ
a1 : 1 < a
n k : ℕ
⊢ yn a1 n ∣ yn a1 (n * k + n)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_4
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe w d z 1
this : 0 ≤ (↑(1 * x * x) - ↑(d * y * y)) * (↑(1 * z * z) - ↑(d * w * w))
⊢ SqLe (x * w + y * z) d (x * z + d * y * w) 1

Tactic:
refine Int.le_of_ofNat_le_ofNat (le_of_sub_nonneg ?_)

Goal state after:
case refine_4
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe w d z 1
this : 0 ≤ (↑(1 * x * x) - ↑(d * y * y)) * (↑(1 * z * z) - ↑(d * w * w))
⊢ 0 ≤ ↑(1 * (x * z + d * y * w) * (x * z + d * y * w)) - ↑(d * (x * w + y * z) * (x * w + y * z))
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
x : ℤ√d
h : ↑x.norm.natAbs = ↑1
hx : x.norm ≤ 0
⊢ 1 = x * -star x

Tactic:
Int.ofNat_natAbs_of_nonpos hx,

Goal state after:
d : ℤ
x : ℤ√d
h : -x.norm = ↑1
hx : x.norm ≤ 0
⊢ 1 = x * -star x
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD yn a1 n ^ 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]
L : xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD yn a1 n ^ 2]
R :
  xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n ≡ xn a1 n ^ k * yn a1 n + k * xn a1 n ^ k * yn a1 n [MOD
    yn a1 n ^ 3]
⊢ xn a1 (n * (k + 1)) ≡ xn a1 n ^ (k + 1) [MOD yn a1 n ^ 2] ∧
    yn a1 (n * (k + 1)) ≡ (k + 1) * xn a1 n ^ k * yn a1 n [MOD yn a1 n ^ 3]

Tactic:
Nat.mul_succ,

Goal state after:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD yn a1 n ^ 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]
L : xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD yn a1 n ^ 2]
R :
  xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n ≡ xn a1 n ^ k * yn a1 n + k * xn a1 n ^ k * yn a1 n [MOD
    yn a1 n ^ 3]
⊢ xn a1 (n * k + n) ≡ xn a1 n ^ (k + 1) [MOD yn a1 n ^ 2] ∧
    yn a1 (n * k + n) ≡ (k + 1) * xn a1 n ^ k * yn a1 n [MOD yn a1 n ^ 3]
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case e'_3.e'_6
p : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (cyclotomic p K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
hζ' : IsPrimitiveRoot ζ (p ^ (0 + 1))
⊢ ↑p ^ (p - 2) = ↑p ^ (p ^ 0 * ((p - 1) * (0 + 1) - 1))

Tactic:
_root_.pow_zero,

Goal state after:
case e'_3.e'_6
p : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (cyclotomic p K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
hζ' : IsPrimitiveRoot ζ (p ^ (0 + 1))
⊢ ↑p ^ (p - 2) = ↑p ^ (1 * ((p - 1) * (0 + 1) - 1))
Module: Mathlib.NumberTheory.MulChar.Duality

Goal state before:
pp: M : Type u_1
R : Type u_2
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : Finite M
inst✝ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
H : Subgroup Mˣ
⊢ Nat.card ↥(OrderDual.ofDual ((CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R) H)) = Nat.card (Mˣ ⧸ H)

Tactic:
CommGroup.card_subgroupOrderIsoSubgroupMonoidHom

Goal state after:
M : Type u_1
R : Type u_2
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : Finite M
inst✝ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
H : Subgroup Mˣ
⊢ Nat.card (Mˣ ⧸ H) = Nat.card (Mˣ ⧸ H)
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
j' : ℕ := j % (4 * n)
n4 : 0 < 4 * n
jl : j' < 4 * n
⊢ j ≡ j' [MOD 4 * n]

Tactic:
delta ModEq

Goal state after:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
j' : ℕ := j % (4 * n)
n4 : 0 < 4 * n
jl : j' < 4 * n
⊢ j % (4 * n) = j' % (4 * n)
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case succ
a : ℕ
a1 : 1 < a
i j✝ n : ℕ
ipos : 0 < i
hin : i ≤ n
h : xn a1 j✝ ≡ xn a1 i [MOD xn a1 n]
j' : ℕ := j✝ % (4 * n)
n4 : 0 < 4 * n
jl : j' < 4 * n
jj : j✝ ≡ j' [MOD 4 * n]
j q : ℕ
IH : xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]
⊢ xn a1 (j + 4 * n * (q + 1)) ≡ xn a1 j [MOD xn a1 n]

Tactic:
Nat.mul_succ,

Goal state after:
case succ
a : ℕ
a1 : 1 < a
i j✝ n : ℕ
ipos : 0 < i
hin : i ≤ n
h : xn a1 j✝ ≡ xn a1 i [MOD xn a1 n]
j' : ℕ := j✝ % (4 * n)
n4 : 0 < 4 * n
jl : j' < 4 * n
jj : j✝ ≡ j' [MOD 4 * n]
j q : ℕ
IH : xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]
⊢ xn a1 (j + (4 * n * q + 4 * n)) ≡ xn a1 j [MOD xn a1 n]
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℚ
f : ℚ → ℤ × ℕ := fun q ↦ (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
⊢ Function.Injective f

Tactic:
intro a b hab

Goal state after:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q ↦ (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
a b : ℚ
hab : f a = f b
⊢ a = b
Module: Mathlib.NumberTheory.LSeries.Convergence

Goal state before:
pp: case coe
f : ℕ → ℂ
x : ℝ
h : ∀ (y : ℝ), x < y → LSeriesSummable f ↑y
y : EReal
hy : ∀ (a : ℝ), LSeriesSummable f ↑a → y ≤ ↑a
a₀ : ℝ
⊢ ↑x < ↑a₀ → y ≤ ↑a₀

Tactic:
exact_mod_cast fun ha ↦ hy a₀ (h a₀ ha)

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

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →*₀ F
hsum : Summable fun x ↦ ‖f x‖
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
this :
  Tendsto (fun n ↦ ∏ i ∈ range n, {p | Nat.Prime p}.mulIndicator (fun p ↦ ∑' (e : ℕ), f (p ^ e)) i) atTop
    (𝓝 (∑' (n : ℕ), f n))
H : ∀ (n : ℕ), ∏ p ∈ range n, {p | Nat.Prime p}.mulIndicator (fun p ↦ (1 - f p)⁻¹) p = ∏ p ∈ n.primesBelow, (1 - f p)⁻¹
⊢ Tendsto (fun n ↦ ∏ p ∈ n.primesBelow, (1 - f p)⁻¹) atTop (𝓝 (∑' (n : ℕ), f n))

Tactic:
have H' : {p | Nat.Prime p}.mulIndicator (fun p ↦ (1 - f p)⁻¹) =
              {p | Nat.Prime p}.mulIndicator (fun p ↦ ∑' e : ℕ, f (p ^ e)) :=
    Set.mulIndicator_congr fun p hp ↦ one_sub_inv_eq_geometric_of_summable_norm hp hsum

Goal state after:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →*₀ F
hsum : Summable fun x ↦ ‖f x‖
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
this :
  Tendsto (fun n ↦ ∏ i ∈ range n, {p | Nat.Prime p}.mulIndicator (fun p ↦ ∑' (e : ℕ), f (p ^ e)) i) atTop
    (𝓝 (∑' (n : ℕ), f n))
H : ∀ (n : ℕ), ∏ p ∈ range n, {p | Nat.Prime p}.mulIndicator (fun p ↦ (1 - f p)⁻¹) p = ∏ p ∈ n.primesBelow, (1 - f p)⁻¹
H' : ({p | Nat.Prime p}.mulIndicator fun p ↦ (1 - f p)⁻¹) = {p | Nat.Prime p}.mulIndicator fun p ↦ ∑' (e : ℕ), f (p ^ e)
⊢ Tendsto (fun n ↦ ∏ p ∈ n.primesBelow, (1 - f p)⁻¹) atTop (𝓝 (∑' (n : ℕ), f n))
Module: Mathlib.NumberTheory.LSeries.Positivity

Goal state before:
pp: a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
x : ℝ
hx : abscissaOfAbsConv a < ↑x
⊢ abscissaOfAbsConv a < ↑(↑x).re

Tactic:
by simpa only [ofReal_re] using hx

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x ↦ P.g x - P.g₀) ∘ fun x ↦ x⁻¹) x‖ ≤ C * ‖((fun x ↦ x ^ (-(r + P.k))) ∘ fun x ↦ x⁻¹) x‖
x : ℝ
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0
hC' :
  ‖(P.ε⁻¹ * ↑(x ^ P.k)) • P.f x - (P.ε⁻¹ * ↑(x ^ P.k) * (P.ε⁻¹ * ↑(x ^ P.k))⁻¹) • P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖
⊢ ‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖

Tactic:
mul_smul _ _ P.g₀,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x ↦ P.g x - P.g₀) ∘ fun x ↦ x⁻¹) x‖ ≤ C * ‖((fun x ↦ x ^ (-(r + P.k))) ∘ fun x ↦ x⁻¹) x‖
x : ℝ
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0
hC' :
  ‖(P.ε⁻¹ * ↑(x ^ P.k)) • P.f x - (P.ε⁻¹ * ↑(x ^ P.k)) • (P.ε⁻¹ * ↑(x ^ P.k))⁻¹ • P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖
⊢ ‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case e'_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x ↦ P.g x - P.g₀) ∘ fun x ↦ x⁻¹) x‖ ≤ C * ‖((fun x ↦ x ^ (-(r + P.k))) ∘ fun x ↦ x⁻¹) x‖
x : ℝ
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0
hC' : ‖P.f x - (P.ε⁻¹ * ↑(x ^ P.k))⁻¹ • P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * ↑(x ^ P.k)‖
⊢ ‖P.ε‖ * C * ‖x ^ r‖ = C * ‖x ^ (r + P.k)‖ / (‖P.ε‖⁻¹ * ‖x ^ P.k‖)

Tactic:
norm_of_nonneg (rpow_pos_of_pos hx _).le,

Goal state after:
case e'_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x ↦ P.g x - P.g₀) ∘ fun x ↦ x⁻¹) x‖ ≤ C * ‖((fun x ↦ x ^ (-(r + P.k))) ∘ fun x ↦ x⁻¹) x‖
x : ℝ
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0
hC' : ‖P.f x - (P.ε⁻¹ * ↑(x ^ P.k))⁻¹ • P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * ↑(x ^ P.k)‖
⊢ ‖P.ε‖ * C * x ^ r = C * x ^ (r + P.k) / (‖P.ε‖⁻¹ * x ^ P.k)
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx' : x ≤ 1
hx : 0 < x
⊢ 1 ≤ ‖x ^ (-P.k)‖

Tactic:
norm_of_nonneg (rpow_pos_of_pos hx _).le,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx' : x ≤ 1
hx : 0 < x
⊢ 1 ≤ x ^ (-P.k)
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
step1 : mellin (fun t ↦ P.g (t ^ (-1))) (-s) = mellin P.g (-s / ↑(-1))
⊢ mellin P.f (↑P.k - s) = P.ε • mellin P.g s

Tactic:
ofReal_neg,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
step1 : mellin (fun t ↦ P.g (t ^ (-1))) (-s) = mellin P.g (-s / -↑1)
⊢ mellin P.f (↑P.k - s) = P.ε • mellin P.g s
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
x : ℝ
x✝ : x ∈ Ioc 0 1
hx : 0 < x
right✝ : x ≤ 1
⊢ ↑x ^ (s - 1) • (P.f₀ - (P.ε * ↑x ^ ↑(-P.k)) • P.g₀) = ↑x ^ (s - 1) • P.f₀ - P.ε • ↑x ^ (s - ↑P.k - 1) • P.g₀

Tactic:
ofReal_neg,

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
x : ℝ
x✝ : x ∈ Ioc 0 1
hx : 0 < x
right✝ : x ≤ 1
⊢ ↑x ^ (s - 1) • (P.f₀ - (P.ε * ↑x ^ (-↑P.k)) • P.g₀) = ↑x ^ (s - 1) • P.f₀ - P.ε • ↑x ^ (s - ↑P.k - 1) • P.g₀
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
t : ℝ
ht : t ∈ Ioi 0
| fun i ↦ a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))

Tactic:
i

Goal state after:
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
t : ℝ
ht : t ∈ Ioi 0
i : ι
| a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case inr
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ 1 * -I / (-I * τ) ^ (1 / 2 + 1) * cexp (-↑π * I * z ^ 2 / τ) *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ)) =
    -2 * ↑π / (-I * τ) ^ (3 / 2) * jacobiTheta₂'' z (-1 / τ)

Tactic:
← div_mul_eq_mul_div,

Goal state after:
case inr
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ 1 / (-I * τ) ^ (1 / 2 + 1) * -I * cexp (-↑π * I * z ^ 2 / τ) *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ)) =
    -2 * ↑π / (-I * τ) ^ (3 / 2) * jacobiTheta₂'' z (-1 / τ)
Module: Mathlib.NumberTheory.LSeries.HurwitzZeta

Goal state before:
pp: case refine_1
a b : UnitAddCircle
⊢ Differentiable ℂ (hurwitzZetaOdd a)

pp: case refine_2
a b : UnitAddCircle
⊢ Differentiable ℂ (hurwitzZetaOdd b)

Tactic:
all_goals apply differentiable_hurwitzZetaOdd

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

Goal state before:
pp: ⊢ cosZeta 0 = riemannZeta

Tactic:
by
  simp_rw [cosZeta, riemannZeta, hurwitzZetaEven, if_true, completedHurwitzZetaEven_zero,
    completedCosZeta_zero]

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

Goal state before:
pp: a t : ℝ
ht : 0 < t
h : -2 * ↑π ≠ 0
n : ℤ
⊢ -I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n + ↑(-π) * ↑↑n ^ 2 * ↑t) * (-2 * ↑π) =
    2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * ↑a + ↑π * I * ↑n ^ 2 * (I * ↑t))

Tactic:
ofReal_neg,

Goal state after:
a t : ℝ
ht : 0 < t
h : -2 * ↑π ≠ 0
n : ℤ
⊢ -I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n + -↑π * ↑↑n ^ 2 * ↑t) * (-2 * ↑π) =
    2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * ↑a + ↑π * I * ↑n ^ 2 * (I * ↑t))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a t : ℝ
ht : 0 < t
⊢ HasSum (fun x ↦ ↑(2 * ↑x * Real.sin (2 * π * a * ↑x) * rexp (-π * ↑x ^ 2 * t))) ↑(sinKernel (↑a) t)

Tactic:
have := (hasSum_int_sinKernel a ht).nat_add_neg

Goal state after:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) +
        -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t)))
    (↑(sinKernel (↑a) t) + -I * ↑0 * cexp (2 * ↑π * I * ↑a * ↑0) * ↑(rexp (-π * ↑0 ^ 2 * t)))
⊢ HasSum (fun x ↦ ↑(2 * ↑x * Real.sin (2 * π * a * ↑x) * rexp (-π * ↑x ^ 2 * t))) ↑(sinKernel (↑a) t)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case e_a
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) +
        -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t)))
    ↑(sinKernel (↑a) t)
n : ℕ
⊢ 2 * ↑n * ((cexp (-(2 * ↑π * ↑a * ↑n) * I) - cexp (2 * ↑π * ↑a * ↑n * I)) * I) / 2 =
    -I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n) + -(-I * ↑n) * cexp (-(2 * ↑π * I * ↑a * ↑n))

Tactic:
← div_mul_eq_mul_div,

Goal state after:
case e_a
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) +
        -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t)))
    ↑(sinKernel (↑a) t)
n : ℕ
⊢ 2 * ↑n / 2 * ((cexp (-(2 * ↑π * ↑a * ↑n) * I) - cexp (2 * ↑π * ↑a * ↑n * I)) * I) =
    -I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n) + -(-I * ↑n) * cexp (-(2 * ↑π * I * ↑a * ↑n))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case e_a
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) +
        -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t)))
    ↑(sinKernel (↑a) t)
n : ℕ
⊢ 2 * ↑n / 2 * ((cexp (-(2 * ↑π * ↑a * ↑n) * I) - cexp (2 * ↑π * ↑a * ↑n * I)) * I) =
    -I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n) + -(-I * ↑n) * cexp (-(2 * ↑π * I * ↑a * ↑n))

Tactic:
← div_mul_eq_mul_div,

Goal state after:
case e_a
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) +
        -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t)))
    ↑(sinKernel (↑a) t)
n : ℕ
⊢ 2 / 2 * ↑n * ((cexp (-(2 * ↑π * ↑a * ↑n) * I) - cexp (2 * ↑π * ↑a * ↑n * I)) * I) =
    -I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n) + -(-I * ↑n) * cexp (-(2 * ↑π * I * ↑a * ↑n))