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

Goal state before:
pp: q : ℚ
this : Finset.univ.gcd ![q.num, ↑q.den] = 1
⊢ |q.num| ≤ |![q.num, ↑q.den] 0|

Tactic:
by simp

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

Goal state before:
pp: q : ℚ
this : Finset.univ.gcd ![q.num, ↑q.den] = 1
⊢ ↑q.den ≤ |![q.num, ↑q.den] 1|

Tactic:
by simp

Goal state after:
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 : IsAdjoinRootMonic S f
inst✝ : Nontrivial S
x : R
i : ℕ
⊢ Pi.single 0 (x * 1) i = Pi.single 0 x i

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : IsTorsionFree R S
inst✝ : IsIntegrallyClosed R
α : S
hα : IsIntegral R α
hα₂ : R[α] = ⊤
⊢ Function.Surjective ⇑(aeval α)

Tactic:
by
    rw [← Set.range_eq_univ, ← AlgHom.coe_range, ← Algebra.adjoin_singleton_eq_range_aeval,
      hα₂, Algebra.coe_top]

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : IsTorsionFree R S
inst✝ : IsIntegrallyClosed R
α : S
hα : IsIntegral R α
hα₂ : R[α] = ⊤
⊢ RingHom.ker (aeval α) = Ideal.span {minpoly R α}

Tactic:
by
    ext
    simpa [Ideal.mem_span_singleton] using minpoly.isIntegrallyClosed_dvd_iff hα _

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

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝³ : Fintype F
inst✝² : Field F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
ψ : AddChar F R
hχ : 2 ≤ orderOf χ
hψ : ψ.IsPrimitive
this :
  gaussSum χ ψ * gaussSum χ ψ ^ (orderOf χ - 1) =
    gaussSum χ ψ * (gaussSum (χ ^ (orderOf χ - 1)) ψ * ∏ j ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ j))
⊢ gaussSum χ ψ ^ orderOf χ = χ (-1) * ↑(Fintype.card F) * ∏ i ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ i)

Tactic:
← pow_succ',

Goal state after:
F : Type u_1
R : Type u_2
inst✝³ : Fintype F
inst✝² : Field F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
ψ : AddChar F R
hχ : 2 ≤ orderOf χ
hψ : ψ.IsPrimitive
this :
  gaussSum χ ψ ^ (orderOf χ - 1 + 1) =
    gaussSum χ ψ * (gaussSum (χ ^ (orderOf χ - 1)) ψ * ∏ j ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ j))
⊢ gaussSum χ ψ ^ orderOf χ = χ (-1) * ↑(Fintype.card F) * ∏ i ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ i)
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : ↑j.val / ↑N ∈ Set.Icc 0 1
m : ℕ
⊢ Φ j / (↑N * (↑j.val + ↑N * ↑m) / ↑N) ^ s = Φ j / (↑j.val + ↑N * ↑m) ^ s

Tactic:
mul_div_cancel_left₀ _ (Nat.cast_ne_zero.mpr (NeZero.ne N))

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : ↑j.val / ↑N ∈ Set.Icc 0 1
m : ℕ
⊢ Φ j / (↑j.val + ↑N * ↑m) ^ s = Φ j / (↑j.val + ↑N * ↑m) ^ s
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : s ≠ 1
hpc : IsPreconnected {1}ᶜ
hne : 2 ∈ {1}ᶜ
⊢ 1 < re 2

Tactic:
by simp

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

Goal state before:
pp: χ : DirichletCharacter ℂ 1
x✝ : ℂ
⊢ completedLFunction χ x✝ = completedRiemannZeta x✝

Tactic:
rw [completedLFunction, ZMod.completedLFunction_modOne_eq, map_one, one_mul]

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)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
hg : AnalyticOnNhd ℂ g U
h : j = 0
⊢ 1 < Module.rank ℝ ℂ

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ DifferentiableOn ℂ (LFunctionTrivChar₁ n) (Set.univ \ {1}) ∧ ContinuousAt (LFunctionTrivChar₁ n) 1

Tactic:
refine ⟨DifferentiableOn.congr (f := fun s ↦ (s - 1) * LFunctionTrivChar n s)
    (fun _ hs ↦ DifferentiableAt.differentiableWithinAt <| by fun_prop (disch := simp_all))
    fun _ hs ↦ Function.update_of_ne (Set.mem_sdiff_singleton.mp hs).2 ..,
    continuousWithinAt_compl_self.mp ?_⟩

Goal state after:
n : ℕ
inst✝ : NeZero n
⊢ ContinuousWithinAt (LFunctionTrivChar₁ n) {1}ᶜ 1
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)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
hg : AnalyticOnNhd ℂ g U
hUc : IsPreconnected U
⊢ 2 ∈ re ⁻¹' Set.Ioi 1

Tactic:
by simp

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

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this :
  Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)) =
    Polynomial.map ofRealHom (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))
⊢ (algebraMap ℂ ℂ).comp ofRealHom = ofRealHom.comp (algebraMap ℝ ℝ)

Tactic:
by simp

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

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this :
  Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)) =
    Polynomial.map ofRealHom (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))
⊢ (algebraMap ℂ ℂ).comp ofRealHom = ofRealHom.comp (algebraMap ℝ ℝ)

Tactic:
by simp

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

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ Complex.Gamma (2 * ↑k + 1) = Complex.Gamma (↑(2 * k) + 1)

Tactic:
by simp

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta (toAddCircle j) (1 - s) =
      Φ j *
        ((2 * ↑π) ^ (-s) * Gamma s *
          (cexp (-↑π * I * s / 2) * expZeta (toAddCircle j) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle j) s))
C : ℂ
⊢ Φ 0 = 0 → Φ (-0) = 0

Tactic:
simp only [neg_zero, imp_self]

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

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this : ↑(2 * k + 1)! = (2 * ↑k + 1) * Complex.Gamma (2 * ↑k + 1)
⊢ 2 * ↑k + 1 = ↑(2 * k + 1)

Tactic:
by simp

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta (toAddCircle j) (1 - s) =
      Φ j *
        ((2 * ↑π) ^ (-s) * Gamma s *
          (cexp (-↑π * I * s / 2) * expZeta (toAddCircle j) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle j) s))
C : ℂ
⊢ {a | (Equiv.neg (ZMod N)) a ≠ a} ⊆ ↑Finset.univ

Tactic:
by simp

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

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k + 1 ≠ -↑n
h3 : (2 * ↑k + 1).Gammaℂ ≠ 0
⊢ -(2 * ↑k) = 1 - (2 * ↑k + 1)

Tactic:
by simp

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

Goal state before:
pp: ⊢ 1 < 4

Tactic:
by simp

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

Goal state before:
pp: case e_a.e_f.inl
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : s ≠ 0 ∨ Φ 0 = 0
i : ZMod N
hi : i ≠ 0
⊢ Φ i * hurwitzZetaEven (toAddCircle i) s = Φ i * (completedHurwitzZetaEven (toAddCircle i) s / s.Gammaℝ)

pp: case e_a.e_f.inr
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : s ≠ 0 ∨ Φ 0 = 0
⊢ Φ 0 * hurwitzZetaEven (toAddCircle 0) s = Φ 0 * (completedHurwitzZetaEven (toAddCircle 0) s / s.Gammaℝ)

Tactic:
· rw [hurwitzZetaEven_def_of_ne_or_ne (.inl (hi ∘ toAddCircle_eq_zero.mp))]

Goal state after:
case e_a.e_f.inr
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : s ≠ 0 ∨ Φ 0 = 0
⊢ Φ 0 * hurwitzZetaEven (toAddCircle 0) s = Φ 0 * (completedHurwitzZetaEven (toAddCircle 0) s / s.Gammaℝ)
Module: Mathlib.NumberTheory.LSeries.Linearity

Goal state before:
pp: ι : Type u_1
f : ι → ℕ → ℂ
S : Finset ι
s : ℂ
x✝ : ℕ
⊢ term (∑ i ∈ S, f i) s x✝ = (∑ i ∈ S, term (f i) s) x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_5
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)
n : ℤ
⊢ 1 / ↑n ^ k * (fourier n) ↑y = -(2 * ↑π * I) ^ k / ↑k ! * (-↑k ! / (2 * ↑π * I * ↑n) ^ k) • (fourier n) ↑y

Tactic:
rw [smul_eq_mul, ← mul_assoc, mul_div, mul_neg, div_mul_cancel₀, neg_neg, mul_pow _ (n : ℂ),
      ← div_div, div_self]
    · rw [Ne, pow_eq_zero_iff', not_and_or]
      exact Or.inl two_pi_I_ne_zero
    · exact Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero _)

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

Goal state before:
pp: case hg
N : ℕ
inst✝ : NeZero N
B : BadChar N
G : ℂ → ℂ := ⋯
H : ℂ → ℂ := ⋯
this : B.F = G * H
⊢ ContinuousAt H 1

Tactic:
exact (B.χ.differentiableAt_LFunction 1 (.inr B.χ_ne)).hasDerivAt.continuousAt_div

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
U : Set ℂ := {t | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
hUp : IsPreconnected U
hF : AnalyticOnNhd ℂ F U
hG : AnalyticOnNhd ℂ G U
⊢ 2 ∈ re ⁻¹' Set.Ioi 1

Tactic:
by simp

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

Goal state before:
pp: case pos
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit ↑n
⊢ 0 ≤
    3 * (-log (1 - 1 ↑n * ↑n ^ (-↑x))).re + 4 * (-log (1 - χ ↑n * ↑n ^ (-(↑x + I * ↑y)))).re +
      (-log (1 - χ ↑n ^ 2 * ↑n ^ (-(↑x + 2 * I * ↑y)))).re

Tactic:
have hn : (n : ℝ) ^ (-x) < 1 := by
      rw [Real.rpow_neg (Nat.cast_nonneg n), inv_lt_one_iff₀]
      exact .inr <| Real.one_lt_rpow (mod_cast one_lt_two.trans_le hn) <| zero_lt_one.trans hx
    have hz : ‖χ n * (n : ℂ) ^ (-(I * y))‖ = 1 := by
      rw [norm_mul, ← hn'.unit_spec, DirichletCharacter.unit_norm_eq_one χ hn'.unit,
        ← ofReal_natCast, norm_cpow_eq_rpow_re_of_pos (mod_cast by lia)]
      simp only [neg_re, mul_re, I_re, ofReal_re, zero_mul, I_im, ofReal_im, mul_zero, sub_self,
        neg_zero, Real.rpow_zero, one_mul]
    rw [MulChar.one_apply hn', one_mul]
    convert! re_log_comb_nonneg' (by positivity) hn hz using 6
    · simp only [ofReal_cpow n.cast_nonneg (-x), ofReal_natCast, ofReal_neg]
    · congr 2
      rw [neg_add, cpow_add _ _ <| mod_cast by lia, ← ofReal_neg, ofReal_cpow n.cast_nonneg (-x),
        ofReal_natCast, mul_left_comm]
    · rw [neg_add, cpow_add _ _ <| mod_cast by lia, ← ofReal_neg, ofReal_cpow n.cast_nonneg (-x),
        ofReal_natCast, show -(2 * I * y) = (2 : ℕ) * -(I * y) by ring, cpow_nat_mul, mul_pow,
        mul_left_comm]

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * I * completedLFunction (𝓕 Φ) t
hF : Differentiable ℂ F
hG : Differentiable ℂ G
⊢ 2 ∈ re ⁻¹' Set.Ioi 1

Tactic:
by simp

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ 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
H₀ : Summable fun p ↦ -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))
H₁ : Summable fun p ↦ -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))
H₂ : Summable fun p ↦ -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))
hsum₀ : Summable fun i ↦ 3 * (-log (1 - 1 ↑↑i * ↑↑i ^ (-(1 + ↑x)))).re
hsum₁ : Summable fun i ↦ 4 * (-log (1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y)))).re
hsum₂ : Summable fun x_1 ↦ (-log (1 - (χ ^ 2) ↑↑x_1 * ↑↑x_1 ^ (-(1 + ↑x + 2 * I * ↑y)))).re
⊢ ‖L (fun n ↦ 1 ↑n) (1 + ↑x) ^ 3 * L (fun n ↦ χ ↑n) (1 + ↑x + I * ↑y) ^ 4 *
        L (fun n ↦ (χ ^ 2) ↑n) (1 + ↑x + 2 * I * ↑y)‖ ≥
    1

Tactic:
rw [← LSeries_eulerProduct_exp_log _ h₀, ← LSeries_eulerProduct_exp_log χ h₁,
    ← LSeries_eulerProduct_exp_log _ h₂]

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ 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
H₀ : Summable fun p ↦ -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))
H₁ : Summable fun p ↦ -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))
H₂ : Summable fun p ↦ -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))
hsum₀ : Summable fun i ↦ 3 * (-log (1 - 1 ↑↑i * ↑↑i ^ (-(1 + ↑x)))).re
hsum₁ : Summable fun i ↦ 4 * (-log (1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y)))).re
hsum₂ : Summable fun x_1 ↦ (-log (1 - (χ ^ 2) ↑↑x_1 * ↑↑x_1 ^ (-(1 + ↑x + 2 * I * ↑y)))).re
⊢ ‖cexp (∑' (p : Nat.Primes), -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))) ^ 3 *
          cexp (∑' (p : Nat.Primes), -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))) ^ 4 *
        cexp (∑' (p : Nat.Primes), -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y))))‖ ≥
    1
Module: Mathlib.NumberTheory.LSeries.SumCoeff

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

Tactic:
by simp

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

Goal state before:
pp: ⊢ 2 ∈ {1}ᶜ

Tactic:
by simp

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

Goal state before:
pp: ⊢ 1 < Module.rank ℝ ℂ

Tactic:
by simp

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

Goal state before:
pp: ⊢ riemannZetaZerosᶜ ∈ Filter.codiscrete ℂ

Tactic:
have := riemannZetaZeros_codiscreteWithin_compl_one

Goal state after:
this : riemannZetaZerosᶜ ∈ Filter.codiscreteWithin {1}ᶜ
⊢ riemannZetaZerosᶜ ∈ Filter.codiscrete ℂ
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 0
⊢ 2 ^ (2 * k - 1) * 2 ^ 1 = 2 ^ (2 * k)

Tactic:
rw [← pow_add, Nat.sub_add_cancel]

Goal state after:
k : ℕ
hk : k ≠ 0
⊢ 1 ≤ 2 * k
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ↑(∏ x ∈ Ico 1 (p / 2).succ, a * ↑x) = ∏ x ∈ Ico 1 (p / 2).succ, ↑(↑a * ↑x).val

Tactic:
by simp

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

Goal state before:
pp: a b c : ℕ
hb0 : 0 < b
hc : a / b ≤ c
⊢ a / b = #(Ico 1 (a / b).succ)

Tactic:
by simp

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

Goal state before:
pp: 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 : EquivLike.inv e.symm y < 1
hy0 : y ≠ 0
⊢ 1 ≠ 0

Tactic:
by simp

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

Goal state before:
pp: 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 : (EquivLike.inv e.symm y).log < log 1
hy0 : y ≠ 0
⊢ exp (-1) ≠ 0

Tactic:
by simp

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

Goal state before:
pp: case mpr
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) ⋯
x : R
hx : x * ϖ ^ n ∈ I * I ^ n
⊢ x ∈ I

Tactic:
← pow_succ',

Goal state after:
case mpr
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) ⋯
x : R
hx : x * ϖ ^ n ∈ I ^ (n + 1)
⊢ x ∈ I
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case succ.inr
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
h✝ : NeZero b
⊢ J(a | b ^ e * b) = J(a | b) ^ e * J(a | b)

Tactic:
mul_right,

Goal state after:
case succ.inr
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
h✝ : NeZero b
⊢ J(a | b ^ e) * J(a | b) = J(a | b) ^ e * J(a | b)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
b : ℕ
h : J(a | b) = -1
x✝ : IsSquare ↑a
r : ZMod b
ha : a % ↑b = r.valMinAbs ^ 2 % ↑b
⊢ ¬0 ≤ -1

Tactic:
by simp

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

Goal state before:
pp: a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
⊢ 2 ≠ 1

Tactic:
by simp

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

Goal state before:
pp: K : Type u_1
Γ₀ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Valued K Γ₀
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
h : Finite 𝓀[K]
n : ℕ
ih : Finite (↥𝒪[K] ⧸ 𝓂[K] ^ n)
⊢ n ≤ n + 1

Tactic:
by simp

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

Goal state before:
pp: case ind.isFalse.isTrue
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
⊢ fastJacobiSymAux (a / 2) b (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) ⋯ = if flip = true then -J(↑a | b) else J(↑a | b)

Tactic:
rw [IH (a / 2) (a.div_lt_self ha0 (by decide)) hb2 hb1]

Goal state after:
case ind.isFalse.isTrue
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
⊢ (if (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) = true then -J(↑(a / 2) | b) else J(↑(a / 2) | b)) =
    if flip = true then -J(↑a | b) else J(↑a | b)
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: 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}
t : Finset K
ht : ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
i : K
hi : i ∈ ↑t
hi' : ¬v i ≤ ↑↑z
⊢ v i ∈ MonoidHom.mrange (MonoidWithZeroHom.ofClass v)

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
⊢ (fun x_1 ↦ x * x_1) 0 = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x✝ : A
hx1✝ : x✝ ∈ Subring.center A
hx1 : ∀ (g : A), g * x✝ = x✝ * g
hx2 : x✝ ≠ 0
x : A
⊢ (fun x ↦ x✝ * x) (-x) = -(fun x ↦ x✝ * x) x

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun x_1 ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
⊢ x * 1 = x

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: ⊢ Odd (mersenne 0) ↔ 0 ≠ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: k : ℕ
⊢ 1 ≤ 2

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ ↑(s i ^ 2 - 2) = ↑(s i) ^ 2 - 2

Tactic:
by push_cast; rfl

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q x : ℕ
hx : ↑x = 0
⊢ (↑x).2 = 0.2

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ (-1) ^ 2 = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p' : ℕ
w✝ : 1 < p' + 2
hp' : p' = p' + 2 - 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne (p' + 2))
⊢ ¬LucasLehmerTest (p' + 2)

Tactic:
t

Goal state after:
p' : ℕ
w✝ : 1 < p' + 2
hp' : p' = p' + 2 - 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne (p' + 2))
t : LucasLehmerTest (p' + 2)
⊢ False
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p' : ℕ
w : 3 ≤ p' + 2
hp : Nat.Prime (mersenne (p' + 2))
this : Fact (Nat.Prime (mersenne (p' + 2)))
hp' : p' = p' + 2 - 2
⊢ Odd (mersenne (p' + 2))

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ
q k : ℕ
ih : sModNatAux (4 % q) q k = sModNat q k
⊢ sModNatAux (4 % q) q (k + 1) = sModNat q (k + 1)

Tactic:
| succ k ih =>

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ.succ
q✝ i q b k : ℕ
ih : sModNatAux ((b ^ 2 + (q - 2)) % q) q k = (sModNatAux b q k ^ 2 + (q - 2)) % q
⊢ sModNatAux ((b ^ 2 + (q - 2)) % q) q (k + 1) = (sModNatAux b q (k + 1) ^ 2 + (q - 2)) % q

Tactic:
| succ k ih =>

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ
q✝ i q k : ℕ
ih : ∀ (b : ℕ), sModNatTR.go q k b = sModNatAux b q k
b : ℕ
⊢ sModNatTR.go q (k + 1) b = sModNatAux b q (k + 1)

Tactic:
| succ k ih =>

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: n k : ℕ
⊢ 1 * (k / 2 ^ n) + k % 2 ^ n = k / 2 ^ n + k % 2 ^ n

Tactic:
rw [one_mul]

Goal state after:
Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete

Goal state before:
pp: G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
a✝ : Nontrivial G
this : Dense ↑⊤ ∨ ∃ a, zpowers a = ⊤
hA : DiscreteTopology ↥⊤
h : Dense ↑⊤
⊢ DiscreteTopology G

Tactic:
rwa [← (Homeomorph.Set.univ G).discreteTopology_iff]

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

Goal state before:
pp: N : ℕ
⊢ 1 ∈ {g | ↑(↑g 1 0) = 0}

Tactic:
by simp

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

Goal state before:
pp: N✝ N : ℕ
⊢ ↑(↑↑1 1 1) = 1

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
⊢ -1 ∈ 𝒢.adjoinNegOne

Tactic:
by simp

Goal state after: