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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ ↑(padicNorm 2 (harmonic n)) = 2 ^ Nat.log 2 n

Tactic:
padicNorm.eq_zpow_of_nonzero (harmonic_pos hn).ne',

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ ↑(↑2 ^ (-padicValRat 2 (harmonic n))) = 2 ^ Nat.log 2 n
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : 2 ≤ S.multiplicity
h : λ ^ (3 * S.multiplicity - 2) ∣ (S.a + S.b) * S.y * S.z
⊢ λ ^ (3 * S.multiplicity - 2) ∣ S.y * (S.z * (S.a + S.b))

Tactic:
show (S.a + S.b) * y S * z S = y S * (z S * (S.a + S.b)) by ring

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : 2 ≤ S.multiplicity
h : λ ^ (3 * S.multiplicity - 2) ∣ S.y * (S.z * (S.a + S.b))
⊢ λ ^ (3 * S.multiplicity - 2) ∣ S.y * (S.z * (S.a + S.b))
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.X ^ 3 * ↑S.u₁ * λ ^ (3 * S.multiplicity - 2) + S.Y ^ 3 * ↑S.u₂ * λ * ↑η + S.Z ^ 3 * ↑S.u₃ * λ * ↑η ^ 2 = 0

Tactic:
rw [X_u₁_spec, Y_u₂_spec, Z_u₃_spec, mul_comm S.x, ← x_spec, mul_comm S.y, ← y_spec, mul_comm S.z,
    ← z_spec, eta_sq]
  calc _ = S.a+S.b+η^2*S.b-S.a+η^2*S.b+2*η*S.b+S.b := by ring
  _ = 0 := by rw [eta_sq]; ring

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ mulHeight ![x, y] = mulHeight ![y, x]

Tactic:
let e : Fin 2 ≃ Fin 2 := Equiv.swap 0 1
  rw [show ![x, y] = ![y, x] ∘ e from List.ofFn_inj.mp rfl]
  exact mulHeight_comp_equiv e ![y, x]

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

Goal state before:
pp: n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
⊢ ↑n ≤ ↑n + 1

Tactic:
linarith

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

Goal state before:
pp: n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Icc (↑n) (↑n + 1)
⊢ 0 ≤ s + 1

Tactic:
linarith

Goal state after:
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case inr
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h✝ : Nonempty ι'
j : ι'
⊢ ∑ i, v (A (j, i) * x i) ≤ (↑(Nat.card ι) * ⨆ ji, v (A ji)) * ⨆ i, v (x i)

Tactic:
simp only [map_mul]

Goal state after:
case inr
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h✝ : Nonempty ι'
j : ι'
⊢ ∑ x_1, v (A (j, x_1)) * v (x x_1) ≤ (↑(Nat.card ι) * ⨆ ji, v (A ji)) * ⨆ i, v (x i)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case inr.inr
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 : ι'
⊢ ⨆ i, v (A (j, ↑i) * x ↑i) ≤ (⨆ ji, v (A ji)) * ⨆ i, v (x i)

Tactic:
simp only [map_mul]

Goal state after:
case inr.inr
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 : ι'
⊢ ⨆ i, v (A (j, ↑i)) * v (x ↑i) ≤ (⨆ ji, v (A ji)) * ⨆ i, v (x i)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case hf.refine_2
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ 0 < ↑n + 1

Tactic:
linarith

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

Goal state before:
pp: case hg.refine_2
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ 0 < ↑n + 1

Tactic:
linarith

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

Goal state before:
pp: n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
this : 0 ∉ uIcc (↑n) (↑n + 1)
⊢ -s ≠ -1

Tactic:
linarith

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

Goal state before:
pp: n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
this : 0 ∉ uIcc (↑n) (↑n + 1)
⊢ -(s + 1) ≠ -1

Tactic:
linarith

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

Goal state before:
pp: n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
this : 0 ∉ uIcc (↑n) (↑n + 1)
⊢ 0 ≤ ↑n + 1

Tactic:
linarith

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

Goal state before:
pp: s : ℝ
hs : 1 < s
⊢ 0 < s - 1

Tactic:
linarith

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

Goal state before:
pp: s : ℝ
hs : 1 < s
⊢ s - 1 ≠ 0

Tactic:
linarith

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

Goal state before:
pp: s : ℝ
hs : 1 < s
⊢ 0 ≤ s - 1

Tactic:
linarith

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

Goal state before:
pp: case hab
s : ℝ
hs : 1 < s
n : ℕ
⊢ ↑n ≤ ↑n + 1

Tactic:
linarith

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

Goal state before:
pp: s : ℝ
hs : 1 < s
Z : ℝ
⊢ s - 1 ≠ 0

Tactic:
linarith

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

Goal state before:
pp: n : ℕ
⊢ ↑(n + 1) ≤ ↑(n + 1) + 1

Tactic:
linarith

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

Goal state before:
pp: case hyz
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
this : 1 < x
⊢ 2 ≤ s + 1

Tactic:
linarith

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

Goal state before:
pp: n : ℕ
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
s : ℝ
hs : 1 ≤ s
⊢ 0 < s + 1

Tactic:
linarith

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

Goal state before:
pp: n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ ↑(n + 1) ≤ ↑(n + 1) + 1

Tactic:
linarith

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

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ riemannZeta s - 1 / (s - 1)
t : ℂ
ht : t ∈ {1}ᶜ
ht' : t = 1
⊢ f t - f 1 = 0

Tactic:
tauto

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]
        apply riemannZeta_residue_one.sub
        refine Tendsto.congr' ?_ (tendsto_const_nhds.mono_left nhdsWithin_le_nhds)
        filter_upwards [self_mem_nhdsWithin] with x hx
        field [sub_ne_zero.mpr <| mem_compl_singleton_iff.mp hx]

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

Goal state before:
pp: case refine_2
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
y : F
hy : y ∈ univ \ {-1}
⊢ y / (1 + y) ∈ univ \ {1}

Tactic:
simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hy ⊢

Goal state after:
case refine_2
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
y : F
hy : ¬y = -1
⊢ ¬y / (1 + y) = 1
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ deriv (fun s ↦ 1 + (s - 1) * riemannZeta₀ s) 1 = ↑γ

Tactic:
rw [deriv_const_add, deriv_fun_mul (by fun_prop) (by fun_prop)]

Goal state after:
⊢ deriv (fun s ↦ s - 1) 1 * riemannZeta₀ 1 + (1 - 1) * deriv riemannZeta₀ 1 = ↑γ
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h h' : IsAdjoinRoot S f
eq : ∀ (x : R[X]), h.map x = h'.map x
⊢ h = h'

Tactic:
cases h

Goal state after:
case mk
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h' : IsAdjoinRoot S f
map✝ : R[X] →ₐ[R] S
map_surjective✝ : Function.Surjective ⇑map✝
ker_map✝ : RingHom.ker map✝ = Ideal.span {f}
eq : ∀ (x : R[X]), { map := map✝, map_surjective := map_surjective✝, ker_map := ker_map✝ }.map x = h'.map x
⊢ { map := map✝, map_surjective := map_surjective✝, ker_map := ker_map✝ } = h'
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
z : S
w y : R[X]
hy : h.repr z - w = f * y
⊢ eval₂ i x (f * y) = 0

Tactic:
eval₂_mul,

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
z : S
w y : R[X]
hy : h.repr z - w = f * y
⊢ eval₂ i x f * eval₂ i x y = 0
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
x : K
n : ℕ
hn₀ : n ≠ 0
hn₁ : ↑n ≤ mulHeight₁ x
hn : IsIntegral ℤ (↑n * x)
h : mulHeight₁ x ≤ B
⊢ n - 1 < ⌊B⌋₊

Tactic:
by grind [Nat.le_floor <| hn₁.trans h]

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
⊢ Tendsto (fun s ↦ ∑ i, (s - 1) * (↑N ^ (-s) * (Φ i * hurwitzZeta (toAddCircle i) s))) (𝓝[≠] 1) (𝓝 (∑ j, Φ j / ↑N))

Tactic:
refine tendsto_finsetSum _ fun j _ ↦ ?_

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
j : ZMod N
x✝ : j ∈ Finset.univ
⊢ Tendsto (fun s ↦ (s - 1) * (↑N ^ (-s) * (Φ j * hurwitzZeta (toAddCircle j) s))) (𝓝[≠] 1) (𝓝 (Φ j / ↑N))
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
⊢ LSeries (fun x ↦ 𝕖 (j * ↑x)) s = ∑' (b : ℕ), cexp (2 * ↑π * I * ↑(↑j.val / ↑N) * ↑b) / ↑b ^ s

Tactic:
LSeries

Goal state after:
N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
⊢ ∑' (n : ℕ), LSeries.term (fun x ↦ 𝕖 (j * ↑x)) s n = ∑' (b : ℕ), cexp (2 * ↑π * I * ↑(↑j.val / ↑N) * ↑b) / ↑b ^ s
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs₀ : s ≠ 0 ∨ N ≠ 1
hs₁ : s ≠ 1 ∨ χ ≠ 1
this : N ≠ 1 → χ 0 = 0
⊢ s ≠ 0 ∨ χ 0 = 0

Tactic:
tauto

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs₀ : s ≠ 0 ∨ N ≠ 1
hs₁ : s ≠ 1 ∨ χ ≠ 1
this : χ ≠ 1 → ∑ a, χ a = 0
⊢ s ≠ 1 ∨ ∑ j, χ j = 0

Tactic:
tauto

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z | z ≠ 1} else Set.univ
V : Set ℂ := {z | 1 < z.re}
hUo : IsOpen U
f : ℂ → ℂ := LFunction fun k ↦ 𝕖 (j * k)
g : ℂ → ℂ := expZeta (toAddCircle j)
u : ℂ
⊢ j = 0 → u ∈ {z | z ≠ 1} ↔ u ≠ 1 ∨ j ≠ 0

Tactic:
tauto

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
h : j = 0 ∧ s = 1
⊢ Φ 0 = 0

Tactic:
tauto

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
h : bernoulliFun (2 * k + 1) (1 / 2) = -bernoulliFun (2 * k + 1) (1 / 2)
⊢ bernoulliFun (2 * k + 1) 2⁻¹ = 0

Tactic:
linarith

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: n : ℤ
hn : n ≠ 0
⊢ bernoulliFourierCoeff 0 n = 0

Tactic:
simpa using bernoulliFourierCoeff_recurrence 0 hn

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

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ hurwitzZeta (↑x) (-(2 * ↑k)) =
    -1 / (2 * ↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))

Tactic:
suffices hurwitzZetaEven x (-(2 * k)) = 0 by
    rw [hurwitzZeta, this, zero_add, hurwitzZetaOdd_neg_two_mul_nat hk hx]

Goal state after:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ hurwitzZetaEven (↑x) (-(2 * ↑k)) = 0
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
this : ∑ x, Φ x * sinZeta (toAddCircle x) s = I * LFunction (𝓕 Φ) s
⊢ 0 < s.re + 1

Tactic:
linarith

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 : HasSum (fun i ↦ (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • (fourier i) ↑y) (B ↑y)
⊢ y ∈ Ico 0 (0 + 1)

Tactic:
rwa [zero_add]

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

Goal state before:
pp: a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
⊢ 0 ≤ 3 * (-log (1 - ↑a)).re + 4 * (-log (1 - ↑a * z)).re + (-log (1 - ↑a * z ^ 2)).re

Tactic:
by
  have hac₀ : ‖(a : ℂ)‖ < 1 := by
    simp only [Complex.norm_of_nonneg ha₀, ha₁]
  have hac₁ : ‖a * z‖ < 1 := by rwa [norm_mul, hz, mul_one]
  have hac₂ : ‖a * z ^ 2‖ < 1 := by rwa [norm_mul, norm_pow, hz, one_pow, mul_one]
  rw [← ((hasSum_re <| hasSum_taylorSeries_neg_log hac₀).mul_left 3).add
    ((hasSum_re <| hasSum_taylorSeries_neg_log hac₁).mul_left 4) |>.add
    (hasSum_re <| hasSum_taylorSeries_neg_log hac₂) |>.tsum_eq]
  refine tsum_nonneg fun n ↦ ?_
  simp only [← ofReal_pow, div_natCast_re, ofReal_re, mul_pow, mul_re, ofReal_im, zero_mul,
    sub_zero]
  rcases n.eq_zero_or_pos with rfl | hn
  · simp
  · simp only [← mul_div_assoc, ← add_div]
    refine div_nonneg ?_ n.cast_nonneg
    rw [← pow_mul, pow_mul', sq, mul_re, ← sq, ← sq, ← sq_norm_sub_sq_re, norm_pow, hz]
    convert! (show 0 ≤ 2 * a ^ n * ((z ^ n).re + 1) ^ 2 by positivity) using 1
    ring

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

Goal state before:
pp: case refine_1
q : ℕ
a : ZMod q
inst✝ : NeZero q
s : ℂ
hs : s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), ¬LFunction χ s = 0
⊢ s ∈ {s | s = 1 ∨ LFunctionTrivChar q s ≠ 0}

Tactic:
tauto

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

Goal state before:
pp: f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
⊢ Tendsto (fun x ↦ LSeries f ↑x) atTop (nhds (f 1))

Tactic:
let F (n : ℕ) : ℂ := if n = 0 then 0 else f n

Goal state after:
f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : ℕ → ℂ := fun n ↦ if n = 0 then 0 else f n
⊢ Tendsto (fun x ↦ LSeries f ↑x) atTop (nhds (f 1))
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: case neg.refine_1
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x ↦ LSeries f ↑x) =ᶠ[atTop] 0
⊢ ∀ (n : ℕ), ¬n = 0 → f n = 0

Tactic:
let F (n : ℕ) : ℂ := if n = 0 then 0 else f n

Goal state after:
case neg.refine_1
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x ↦ LSeries f ↑x) =ᶠ[atTop] 0
F : ℕ → ℂ := fun n ↦ if n = 0 then 0 else f n
⊢ ∀ (n : ℕ), ¬n = 0 → f n = 0
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: r : ℝ
s : ℂ
f : ℕ → ℝ
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
hf : ∀ (n : ℕ), 0 ≤ f n
hr : 0 ≤ r
hs : r < s.re
⊢ (fun n ↦ ∑ k ∈ Icc 1 n, ‖↑(f k)‖) =O[atTop] fun n ↦ ↑n ^ r

Tactic:
simpa [abs_of_nonneg (hf _)]

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
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))

Tactic:
simp_rw [← h₄] at hO

Goal state after:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ↑x ^ (-s)) t
h₄ : ∀ (n : ℕ), ∑ k ∈ Icc 0 n, f k = ∑ k ∈ Icc 1 n, f k
hO : (fun n ↦ ∑ k ∈ Icc 0 n, f k) =O[atTop] fun n ↦ ↑n ^ r
⊢ LSeries f s = s * ∫ (t : ℝ) in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-(s + 1))
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: this : 1 / 4 = (algebraMap ℚ ℝ) (1 / 4)
⊢ (-1) ^ (1 + 1) * (2 ^ (2 * 1 + 1) * π ^ (2 * 1 + 1)) / 2 / ↑(2 * 1 + 1)! *
      (algebraMap ℚ ℝ) (Polynomial.eval (1 / 4) (Polynomial.bernoulli (2 * 1 + 1))) =
    π ^ 3 / 32

Tactic:
(by decide : 2 * 1 + 1 = 3),

Goal state after:
this : 1 / 4 = (algebraMap ℚ ℝ) (1 / 4)
⊢ (-1) ^ (1 + 1) * (2 ^ 3 * π ^ 3) / 2 / ↑3! * (algebraMap ℚ ℝ) (Polynomial.eval (1 / 4) (Polynomial.bernoulli 3)) =
    π ^ 3 / 32
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case left
⊢ 0 ≤ 1 / 4

Tactic:
linarith

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case right
⊢ 1 / 4 ≤ 1

Tactic:
linarith

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

Goal state before:
pp: case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * ↑x).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
⊢ (a * ↑(↑b / a).valMinAbs.natAbs).valMinAbs.natAbs = b

Tactic:
rw [natCast_natAbs_valMinAbs]

Goal state after:
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * ↑x).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
⊢ (a * if (↑b / a).val ≤ p / 2 then ↑b / a else -(↑b / a)).valMinAbs.natAbs = b
Module: Mathlib.NumberTheory.LSeries.SumCoeff

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

Tactic:
linarith

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ↑(p / 2)! ≠ 0

Tactic:
rw [Ne, CharP.cast_eq_zero_iff (ZMod p) p, hp.1.dvd_factorial, not_le]
    exact Nat.div_lt_self hp.1.pos (by decide)

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

Goal state before:
pp: a b c : ℕ
hb0 : 0 < b
hc : a / b ≤ c
x : ℕ
this : x * b ≤ a → x ≤ c
⊢ x * b ≤ a → 1 ≤ x → x ≤ c

Tactic:
tauto

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

Goal state before:
pp: 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
⊢ 1 + (-s - 1) ≤ -s

Tactic:
linarith

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

Goal state before:
pp: case mp.inr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
e : ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)
x : ValueGroupWithZero R := e.symm (exp (-1))
hx0 : x ≠ 0
hx1 : x < 1
y : ValueGroupWithZero R
hy : (e y).log < 0
hy0 : y ≠ 0
⊢ (e y).log ≤ -1

Tactic:
linarith

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

Goal state before:
pp: p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  #({x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p}) =
    #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
hdisj :
  Disjoint ({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q})
    ({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
x : ℕ × ℕ
this : x.2 * p ≤ x.1 * q ∨ x.1 * q ≤ x.2 * p
⊢ ((1 ≤ x.1 ∧ x.1 < (p / 2).succ) ∧ 1 ≤ x.2 ∧ x.2 < (q / 2).succ) ∧ x.2 * p ≤ x.1 * q ∨
      ((1 ≤ x.1 ∧ x.1 < (p / 2).succ) ∧ 1 ≤ x.2 ∧ x.2 < (q / 2).succ) ∧ x.1 * q ≤ x.2 * p ↔
    (1 ≤ x.1 ∧ x.1 < (p / 2).succ) ∧ 1 ≤ x.2 ∧ x.2 < (q / 2).succ

Tactic:
tauto

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

Goal state before:
pp: case inl
a : ℤ
b : ℕ
h : 1 = 0
hb : b = 0
⊢ b ≠ 0 ∧ a.gcd ↑b ≠ 1

Tactic:
cases h

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

Goal state before:
pp: l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
⊢ -s + 1 ≠ 0

Tactic:
linarith

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

Goal state before:
pp: a : ℤ
R : Type u_1
inst✝ : Semiring R
χ : R →* ℤ
hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = χ ↑p
b : ℕ
hb : Odd b
⊢ J(a | b) = χ ↑b

Tactic:
by
  conv_rhs => rw [← prod_primeFactorsList hb.pos.ne', cast_list_prod, map_list_prod χ]
  rw [jacobiSym, List.map_map, ← List.pmap_eq_map
    fun _ => prime_of_mem_primeFactorsList]
  congr 1; apply List.pmap_congr_left
  exact fun p h pp _ => hp p pp (hb.ne_two_of_dvd_nat <| dvd_of_mem_primeFactorsList h)

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

Goal state before:
pp: m n : ℕ
hm : Odd m
hn : Odd n
⊢ qrSign m n ^ 2 = 1

Tactic:
rw [neg_one_pow hm hn, ← pow_mul, mul_comm, pow_mul, neg_one_sq, one_pow]

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case zero
K : Type u_1
Γ₀ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Valued K Γ₀
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
h : Finite 𝓀[K]
⊢ Finite (↥𝒪[K] ⧸ 𝓂[K] ^ 0)

Tactic:
simp only [pow_zero, Ideal.one_eq_top]
    exact Finite.of_fintype (↥𝒪[K] ⧸ ⊤)

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

Goal state before:
pp: a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
ha1 : ¬a = 1
hba : b % a = 0
this : J(↑a | b) = 0
⊢ 0 = if flip = true then -J(↑a | b) else J(↑a | b)

Tactic:
simp [this]

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

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

Tactic:
← v.restrict_inj

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