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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
N₁ N₂ : ℕ
h2 : ∀ N ≥ N₂, ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 N, b x (2 * k)
N₃ : ℕ
h3 : ∀ N ≥ N₃, ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 N, b x (3 * k)
N₅ : ℕ
h5 : ∀ N ≥ N₅, ψ (x ^ (↑5)⁻¹) = ∑ k ∈ Icc 1 N, b x (5 * k)
N₇ : ℕ
h7 : ∀ N ≥ N₇, ψ (x ^ (↑7)⁻¹) = ∑ k ∈ Icc 1 N, b x (7 * k)
N : ℕ := N₁ + N₂ + N₃ + N₅ + N₇
h1 : ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 (1 + 6 * N), b x (1 * k)
⊢ ψ x - θ x ≤ ψ (x ^ 2⁻¹) + ψ (x ^ 3⁻¹) + ψ (x ^ 5⁻¹) ∧ ψ (x ^ 2⁻¹) + ψ (x ^ 3⁻¹) + ψ (x ^ 7⁻¹) ≤ ψ x - θ x

Tactic:
specialize h2 (3 * N) (by lia)

Goal state after:
x : ℝ
hx : 0 ≤ x
N₁ N₂ N₃ : ℕ
h3 : ∀ N ≥ N₃, ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 N, b x (3 * k)
N₅ : ℕ
h5 : ∀ N ≥ N₅, ψ (x ^ (↑5)⁻¹) = ∑ k ∈ Icc 1 N, b x (5 * k)
N₇ : ℕ
h7 : ∀ N ≥ N₇, ψ (x ^ (↑7)⁻¹) = ∑ k ∈ Icc 1 N, b x (7 * k)
N : ℕ := N₁ + N₂ + N₃ + N₅ + N₇
h2 : ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 (3 * N), b x (2 * k)
h1 : ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 (1 + 6 * N), b x (1 * k)
⊢ ψ x - θ x ≤ ψ (x ^ 2⁻¹) + ψ (x ^ 3⁻¹) + ψ (x ^ 5⁻¹) ∧ ψ (x ^ 2⁻¹) + ψ (x ^ 3⁻¹) + ψ (x ^ 7⁻¹) ≤ ψ x - θ x
Module: Mathlib.NumberTheory.FunctionField

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F[X] K
inst✝¹ : Algebra F⟮X⟯ K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
⊢ Function.Injective ⇑(algebraMap F[X] K)

Tactic:
rw [IsScalarTower.algebraMap_eq F[X] F⟮X⟯ K]

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F[X] K
inst✝¹ : Algebra F⟮X⟯ K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
⊢ Function.Injective ⇑((algebraMap F⟮X⟯ K).comp (algebraMap F[X] F⟮X⟯))
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ 1
⊢ a 1 = 0

Tactic:
simp [a, not_prime_one]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case hd
a b : ℝ
hab : a ≤ b
one_lt : 1 < a
x : ℝ
x✝ : x ∈ Set.Icc a b
left✝ : a ≤ x
right✝ : x ≤ b
⊢ 0 < log a ^ 2

Tactic:
bound

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case ha
a b : ℝ
hab : a ≤ b
one_lt : 1 < a
x : ℝ
x✝ : x ∈ Set.Icc a b
left✝ : a ≤ x
right✝ : x ≤ b
⊢ 0 ≤ log a

Tactic:
bound

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
⊢ x ≤ x ^ 2

Tactic:
bound

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ 2 ^ 2 * ((x - √x) / log x ^ 2) + (√x - 2) / log 2 ^ 2 ≤ 4 * x / log x ^ 2 + √x / log 2 ^ 2

Tactic:
mul_div_assoc

Goal state after:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ 2 ^ 2 * ((x - √x) / log x ^ 2) + (√x - 2) / log 2 ^ 2 ≤ 4 * (x / log x ^ 2) + √x / log 2 ^ 2
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: A : Type u
B : Type v
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
ι' : Type u_1
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι'
b : Basis ι A B
f : ι ≃ ι'
⊢ ((reindex f f) (traceMatrix A ⇑b)).det = discr A ⇑b

Tactic:
det_reindex_self,

Goal state after:
A : Type u
B : Type v
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
ι' : Type u_1
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι'
b : Basis ι A B
f : ι ≃ ι'
⊢ (traceMatrix A ⇑b).det = discr A ⇑b
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_1
⊢ (fun x ↦ 4 * x / log x ^ 2) =O[atTop] fun x ↦ x / log x ^ 2

Tactic:
mul_div_assoc

Goal state after:
case refine_1
⊢ (fun x ↦ 4 * (x / log x ^ 2)) =O[atTop] fun x ↦ x / log x ^ 2
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‖
⊢ 0 ≤ log x

Tactic:
bound

Goal state after:
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‖
this : 0 ≤ log x
⊢ 0 ≤ x / log x

Tactic:
bound

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case ha
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ log √x

pp: case hbc
x : ℝ
hx : 1 ≤ x
⊢ ↑(#({a ∈ ⌊x⌋₊.primesLE | ↑a ≤ √x})) ≤ √x

Tactic:
· exact log_nonneg (one_le_sqrt.mpr hx)

Goal state after:
case hbc
x : ℝ
hx : 1 ≤ x
⊢ ↑(#({a ∈ ⌊x⌋₊.primesLE | ↑a ≤ √x})) ≤ √x
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : ((minpoly K pb.gen).aroots E).Nodup
σ : L →ₐ[K] E
⊢ (aeval (σ pb.gen)) (minpoly K pb.gen) = 0

pp: K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : ((minpoly K pb.gen).aroots E).Nodup
σ : L →ₐ[K] E
⊢ Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0

Tactic:
aeval_algHom_apply

Goal state after:
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : ((minpoly K pb.gen).aroots E).Nodup
σ : L →ₐ[K] E
⊢ σ ((aeval pb.gen) (minpoly K pb.gen)) = 0

K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : ((minpoly K pb.gen).aroots E).Nodup
σ : L →ₐ[K] E
⊢ Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0
Module: Mathlib.NumberTheory.Cyclotomic.Gal

Goal state before:
pp: n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ✝ : IsPrimitiveRoot μ n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
h : Irreducible (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := zeta_spec n K L
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) n :=
  fun t ↦ IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)
f : L ≃ₐ[K] L
⊢ (fun t ↦ (IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) ⋯)
      ((↑(IsPrimitiveRoot.autToPow K ⋯)).toFun f) =
    f

Tactic:
simp only [MonoidHom.toFun_eq_coe]

Goal state after:
n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ✝ : IsPrimitiveRoot μ n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
h : Irreducible (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := zeta_spec n K L
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) n :=
  fun t ↦ IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)
f : L ≃ₐ[K] L
⊢ (IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) ⋯ = f
Module: Mathlib.NumberTheory.Cyclotomic.Gal

Goal state before:
pp: n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ✝ : IsPrimitiveRoot μ n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
h : Irreducible (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := zeta_spec n K L
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) n :=
  fun t ↦ IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)
x : (ZMod n)ˣ
⊢ (↑(IsPrimitiveRoot.autToPow K ⋯)).toFun
      ((fun t ↦ (IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) ⋯) x) =
    x

Tactic:
simp only [MonoidHom.toFun_eq_coe]

Goal state after:
n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ✝ : IsPrimitiveRoot μ n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
h : Irreducible (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := zeta_spec n K L
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) n :=
  fun t ↦ IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)
x : (ZMod n)ˣ
⊢ (IsPrimitiveRoot.autToPow K ⋯) ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) ⋯) =
    x
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d n : ℤ
⊢ (↑n).re = n

Tactic:
cases n

Goal state after:
case ofNat
d : ℤ
a✝ : ℕ
⊢ (↑(Int.ofNat a✝)).re = Int.ofNat a✝

case negSucc
d : ℤ
a✝ : ℕ
⊢ (↑(Int.negSucc a✝)).re = Int.negSucc a✝
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d n : ℤ
⊢ (↑n).im = 0

Tactic:
cases n

Goal state after:
case ofNat
d : ℤ
a✝ : ℕ
⊢ (↑(Int.ofNat a✝)).im = 0

case negSucc
d : ℤ
a✝ : ℕ
⊢ (↑(Int.negSucc a✝)).im = 0
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
hb : { re := ↑z, im := -↑w }.Nonneg
⊢ ({ re := ↑x, im := -↑y } * { re := ↑z, im := -↑w }).Nonneg

Tactic:
rw [calc
          (⟨x, -y⟩ * ⟨z, -w⟩ : ℤ√d) = ⟨_, _⟩ := rfl
          _ = ⟨x * z + d * y * w, -(x * w + y * z)⟩ := by simp [add_comm]]
    exact
        nonnegg_pos_neg.2
          (sqLe_mul.right.right.right (nonnegg_pos_neg.1 ha) (nonnegg_pos_neg.1 hb))

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (cyclotomic (p ^ k) K)
⊢ ∃ u n, (-1) ^ (φ (p ^ k) / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1)) = ↑↑u * ↑p ^ n

Tactic:
by_cases heven : Even ((p ^ k).totient / 2)

Goal state after:
case pos
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (cyclotomic (p ^ k) K)
heven : Even (φ (p ^ k) / 2)
⊢ ∃ u n, (-1) ^ (φ (p ^ k) / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1)) = ↑↑u * ↑p ^ n

case neg
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (cyclotomic (p ^ k) K)
heven : ¬Even (φ (p ^ k) / 2)
⊢ ∃ u n, (-1) ^ (φ (p ^ k) / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1)) = ↑↑u * ↑p ^ n
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
⊢ 2 * n - (n + 1) = n - 1

Tactic:
rw [two_mul, tsub_add_eq_tsub_tsub, add_tsub_cancel_right]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
d : ℤ
f : ℤ√d →+* R
⊢ (fun r ↦ { toFun := fun a ↦ ↑a.re + ↑a.im * ↑r, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })
      ((fun f ↦ ⟨f sqrtd, ⋯⟩) f) =
    f

Tactic:
ext
    simp

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

Goal state before:
pp: ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m ↦ ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
j k : ℤ
| |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)

Tactic:
rw [mul_comm, le_div_iff₀ hn, ← abs_of_pos hn, ← abs_mul]

Goal state after:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m ↦ ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
j k : ℤ
| |(ξ * ↑k - ↑j) * (↑n + 1)| ≤ 1
Module: Mathlib.NumberTheory.DirichletCharacter.Bounds

Goal state before:
pp: case neg
F : Type u_1
inst✝ : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : ZMod n
h : ¬IsUnit a
⊢ ‖χ a‖ ≤ 1

Tactic:
rw [χ.map_nonunit h, norm_zero]

Goal state after:
case neg
F : Type u_1
inst✝ : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : ZMod n
h : ¬IsUnit a
⊢ 0 ≤ 1
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
hξ : Irrational ξ
q : ℚ
⊢ ∃ q', |ξ - ↑q'| < 1 / ↑q'.den ^ 2 ∧ |ξ - ↑q'| < |ξ - ↑q|

Tactic:
have h := abs_pos.mpr (sub_ne_zero.mpr <| Irrational.ne_rat hξ q)
  obtain ⟨m, hm⟩ := exists_nat_gt (1 / |ξ - q|)
  have m_pos : (0 : ℝ) < m := (one_div_pos.mpr h).trans hm
  obtain ⟨q', hbd, hden⟩ := exists_rat_abs_sub_le_and_den_le ξ (Nat.cast_pos.mp m_pos)
  have den_pos : (0 : ℝ) < q'.den := Nat.cast_pos.mpr q'.pos
  have md_pos := mul_pos (add_pos m_pos zero_lt_one) den_pos
  refine
    ⟨q', lt_of_le_of_lt hbd ?_,
      lt_of_le_of_lt hbd <|
        (one_div_lt md_pos h).mpr <|
          hm.trans <|
            lt_of_lt_of_le (lt_add_one _) <|
              (le_mul_iff_one_le_right <| add_pos m_pos zero_lt_one).mpr <|
                mod_cast (q'.pos : 1 ≤ q'.den)⟩
  rw [sq, one_div_lt_one_div md_pos (mul_pos den_pos den_pos), mul_lt_mul_iff_left₀ den_pos]
  exact lt_add_of_le_of_pos (Nat.cast_le.mpr hden) zero_lt_one

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

Goal state before:
pp: ξ : ℤ
n : ℕ
⊢ (↑ξ).convergent n = ↑ξ

Tactic:
cases n

Goal state after:
case zero
ξ : ℤ
⊢ (↑ξ).convergent 0 = ↑ξ

case succ
ξ : ℤ
n✝ : ℕ
⊢ (↑ξ).convergent (n✝ + 1) = ↑ξ
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: case right
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
hpm : ¬p ∣ m
⊢ List.filter (fun x ↦ decide (x ∈ s)) ((p ^ e).primeFactorsList ++ m.primeFactorsList) ~ m.primeFactorsList

Tactic:
filter_append,

Goal state after:
case right
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
hpm : ¬p ∣ m
⊢ List.filter (fun x ↦ decide (x ∈ s)) (p ^ e).primeFactorsList ++
      List.filter (fun x ↦ decide (x ∈ s)) m.primeFactorsList ~
    m.primeFactorsList
Module: Mathlib.NumberTheory.LSeries.Convolution

Goal state before:
pp: case inr
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
hp₁ : p.1 ≠ 0
hp₂ : p.2 ≠ 0
⊢ f p.1 * g p.2 / ↑n ^ s = f p.1 * (g p.2 / ↑p.2 ^ s / ↑p.1 ^ s)

Tactic:
div_div,

Goal state after:
case inr
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
hp₁ : p.1 ≠ 0
hp₂ : p.2 ≠ 0
⊢ f p.1 * g p.2 / ↑n ^ s = f p.1 * (g p.2 / (↑p.2 ^ s * ↑p.1 ^ s))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: case e'_6
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
⊢ rexp (-π * a ^ 2 * t) * rexp (-π * t) / (1 - rexp (-π * t)) ^ 2 =
    rexp (-π * a ^ 2 * t) * (rexp (-π * t) / (1 - rexp (-π * t)) ^ 2)

Tactic:
mul_div_assoc

Goal state after:
case e'_6
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
⊢ rexp (-π * a ^ 2 * t) * (rexp (-π * t) / (1 - rexp (-π * t)) ^ 2) =
    rexp (-π * a ^ 2 * t) * (rexp (-π * t) / (1 - rexp (-π * t)) ^ 2)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a : UnitAddCircle
t : ℝ
⊢ Function.Periodic (fun b ↦ ∑' (n : ℤ), f_int k b t n) 1

Tactic:
intro b
    simp_rw [← (Equiv.addRight (1 : ℤ)).tsum_eq (f := fun n ↦ f_int k b t n)]
    simp only [f_int, ← add_assoc, add_comm, Equiv.coe_addRight, Int.cast_add, Int.cast_one]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a : ℝ
ha : a ∈ Icc 0 1
t : ℝ
ht : 0 < t
n : ℤ
⊢ f_int k a t n = Int.rec (f_nat k a t) (f_nat k (1 - a) t) n

Tactic:
cases n

Goal state after:
case ofNat
k : ℕ
a : ℝ
ha : a ∈ Icc 0 1
t : ℝ
ht : 0 < t
a✝ : ℕ
⊢ f_int k a t (Int.ofNat a✝) = Int.rec (f_nat k a t) (f_nat k (1 - a) t) (Int.ofNat a✝)

case negSucc
k : ℕ
a : ℝ
ha : a ∈ Icc 0 1
t : ℝ
ht : 0 < t
a✝ : ℕ
⊢ f_int k a t (Int.negSucc a✝) = Int.rec (f_nat k a t) (f_nat k (1 - a) t) (Int.negSucc a✝)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun n p ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun n p ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ := fun n ↦ 3 * π * ↑|n| ^ 2 * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
n : ℤ
p : ℂ × ℂ
hp : p ∈ V
⊢ ‖jacobiTheta₂_term n p.1 p.2‖ ≤ rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))

Tactic:
exact norm_jacobiTheta₂_term_le hT (le_of_lt hp.1) (le_of_lt hp.2) n

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
hP : IsStrongFEPair P
s : ℂ
⊢ ∀ᵐ (x : ℝ),
    x ∈ Ioi 0 →
      (fun t ↦ ↑t ^ (s - 1) • (((Ioi 1).indicator fun x ↦ P.f x) + (Ioo 0 1).indicator fun x ↦ P.f x) t) x =
        (fun t ↦ ↑t ^ (s - 1) • P.f t) x

Tactic:
filter_upwards [compl_mem_ae_iff.mpr (Subsingleton.measure_zero (s := {1}) (by simp) _)]
    with t (ht₁ : t ≠ 1) (ht₀ : 0 < t)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hP : IsStrongFEPair P
s : ℂ
t : ℝ
ht₁ : t ≠ 1
ht₀ : 0 < t
⊢ ↑t ^ (s - 1) • (((Ioi 1).indicator fun x ↦ P.f x) + (Ioo 0 1).indicator fun x ↦ P.f x) t = ↑t ^ (s - 1) • P.f t
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i = 0 then 0 else 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))
i : ι
h : r i ≠ 0
⊢ ‖a i * ↑(r i)‖ / |r i| ^ (s.re + 1) = ‖a i‖ / |r i| ^ s.re

Tactic:
rpow_add (abs_pos.mpr h),

Goal state after:
case inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i = 0 then 0 else 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))
i : ι
h : r i ≠ 0
⊢ ‖a i * ↑(r i)‖ / (|r i| ^ s.re * |r i| ^ 1) = ‖a i‖ / |r i| ^ s.re
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case e_a
a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) * (1 / (s / 2) / 2) =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s

Tactic:
div_div,

Goal state after:
case e_a
a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) * (1 / (s / 2 * 2)) =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case e_a
a : UnitAddCircle
s : ℂ
⊢ 1 / ((1 - s) / 2) / 2 = 1 / (1 - s)

Tactic:
div_div,

Goal state after:
case e_a
a : UnitAddCircle
s : ℂ
⊢ 1 / ((1 - s) / 2 * 2) = 1 / (1 - s)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a x : ℝ
hx : 0 < x
⊢ HasSum (fun x_1 ↦ ↑((↑x_1 + a) * rexp (-π * (↑x_1 + a) ^ 2 * x))) ↑(oddKernel (↑a) x)

Tactic:
oddKernel_def' a x

Goal state after:
a x : ℝ
hx : 0 < x
⊢ HasSum (fun x_1 ↦ ↑((↑x_1 + a) * rexp (-π * (↑x_1 + a) ^ 2 * x)))
    (cexp (-↑π * ↑a ^ 2 * ↑x) *
      (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x)))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case e_a
a : UnitAddCircle
s : ℂ
⊢ (if a = 0 then 1 else 0) * (1 / (1 / 2 - s / 2) / 2) = (if a = 0 then 1 else 0) / (1 - s)

Tactic:
div_div,

Goal state after:
case e_a
a : UnitAddCircle
s : ℂ
⊢ (if a = 0 then 1 else 0) * (1 / ((1 / 2 - s / 2) * 2)) = (if a = 0 then 1 else 0) / (1 - s)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
h1 : Tendsto (fun s ↦ (s - 1 / 2) * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] (1 / 2)) (𝓝 1)
s : ℂ
⊢ (s - 1) * (hurwitzEvenFEPair a).Λ (s / 2) / 2 = (s - 1) * ((hurwitzEvenFEPair a).Λ (s / 2) / 2)

Tactic:
mul_div_assoc

Goal state after:
a : UnitAddCircle
h1 : Tendsto (fun s ↦ (s - 1 / 2) * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] (1 / 2)) (𝓝 1)
s : ℂ
⊢ (s - 1) * ((hurwitzEvenFEPair a).Λ (s / 2) / 2) = (s - 1) * ((hurwitzEvenFEPair a).Λ (s / 2) / 2)
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: N : ℕ
R : Type u_1
inst✝ : CommMonoidWithZero R
χ : DirichletCharacter R N
n : ℕ
hn : n ≠ 0
⊢ χ ↑n = (toArithmeticFunction fun x ↦ χ ↑x) n

Tactic:
simp [toArithmeticFunction, hn]

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

Goal state before:
pp: case refine_2
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ cexp (2 * ↑π * I * ↑a * ↑n) / 2
hF :
  ∀ (t : ℝ),
    0 < t → HasSum (fun n ↦ if ↑n = 0 then 0 else c n * ↑(rexp (-π * ↑n ^ 2 * t))) ((↑(cosKernel (↑a) t) - 1) / 2)
n : ℤ
⊢ s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2 = s.Gammaℝ * c n / ↑|↑n| ^ s

Tactic:
· simp [c, ← Int.cast_abs, div_right_comm, mul_div_assoc]

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

Goal state before:
pp: ⊢ (abscissaOfAbsConv fun n ↦ ↑(ζ n)) = 1

Tactic:
abscissaOfAbsConv_congr (g := 1) fun hn ↦ by simp [hn],

Goal state after:
⊢ abscissaOfAbsConv 1 = 1
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: case inr
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (fun n ↦ χ ↑n) s
hs' : (abscissaOfAbsConv fun n ↦ χ ↑n) < ↑s.re
hΛ : LSeriesSummable ((fun n ↦ χ ↑n) * fun n ↦ ↑(Λ n)) s
⊢ L ((fun n ↦ χ ↑n) * fun n ↦ ↑(Λ n)) s = -deriv (L fun n ↦ χ ↑n) s / L (fun n ↦ χ ↑n) s

Tactic:
rw [eq_div_iff <| LSeries_ne_zero_of_one_lt_re χ hs, ← LSeries_convolution' hΛ hχ,
    convolution_twist_vonMangoldt, LSeries_deriv hs', neg_neg]

Goal state after:
case inr
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (fun n ↦ χ ↑n) s
hs' : (abscissaOfAbsConv fun n ↦ χ ↑n) < ↑s.re
hΛ : LSeriesSummable ((fun n ↦ χ ↑n) * fun n ↦ ↑(Λ n)) s
⊢ L ((fun n ↦ χ ↑n) * fun n ↦ Complex.log ↑n) s = L (logMul fun n ↦ χ ↑n) s
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: s : ℂ
hs : 1 < s.re
this : deriv (L 1) s = deriv riemannZeta s
⊢ L (fun n ↦ ↑(Λ n)) s = -deriv riemannZeta s / riemannZeta s

Tactic:
rw [LSeries_vonMangoldt_eq hs, ← LSeries_one_eq_riemannZeta hs, this]

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

Goal state before:
pp: case hf
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
⊢ Multipliable ({p | Nat.Prime p}.mulIndicator fun p ↦ (1 - χ ↑p * ↑p ^ (-s))⁻¹)

Tactic:
exact multipliable_subtype_iff_mulIndicator.mp
      (DirichletCharacter.LSeries_eulerProduct_hasProd χ hs).multipliable

Goal state after: