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

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

Tactic:
zpow_natCast,

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ ↑(↑2 ^ Nat.log 2 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 : (S.multiplicity - 1) * 3 + 1 = 3 * S.multiplicity - 2
⊢ S.X ^ 3 * (↑S.u₂ * ↑S.u₂⁻¹) * (↑η ^ 3 * ↑S.u₁) * (λ ^ ((S.multiplicity - 1) * 3) * λ) =
    S.X ^ 3 * ↑S.u₁ * λ ^ (3 * S.multiplicity - 2)

Tactic:
simp [hζ.toInteger_cube_eq_one, ← pow_succ, this]

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

Goal state before:
pp: case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
c : K
hc : c ≠ 0
hx : x ≠ 0
this : Nonempty ι
hcx : c • x ≠ 0
⊢ (Multiset.map (fun i ↦ i c) archAbsVal).prod * (Multiset.map (fun i ↦ ⨆ i_1, i (x i_1)) archAbsVal).prod *
      ∏ᶠ (v : ↑nonarchAbsVal), ↑v c * ⨆ i, ↑v (x i) =
    (Multiset.map (fun i ↦ ⨆ i_1, i (x i_1)) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)

Tactic:
rw [finprod_mul_distrib (by fun_prop) (by fun_prop),
    mul_mul_mul_comm, product_formula hc, one_mul]

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

Goal state before:
pp: case inl
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f = 0
⊢ mulHeight (x ∘ f) ≤ mulHeight x

Tactic:
simpa [h₀] using one_le_mulHeight _

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

Goal state before:
pp: n : ℕ
hn : 0 < n
⊢ term n 1 = log (↑n + 1) - log ↑n - 1 / (↑n + 1)

Tactic:
have hv : ∀ x ∈ uIcc (n : ℝ) (n + 1), 0 < x := by
    intro x hx
    rw [uIcc_of_le (by simp only [le_add_iff_nonneg_right, zero_le_one])] at hx
    exact (Nat.cast_pos.mpr hn).trans_le hx.1
  calc term n 1
    _ = ∫ x : ℝ in n..(n + 1), (x - n) / x ^ 2 := by
      simp_rw [term, one_add_one_eq_two, ← Nat.cast_two (R := ℝ), rpow_natCast]
    _ = ∫ x : ℝ in n..(n + 1), (1 / x - n / x ^ 2) :=
      intervalIntegral.integral_congr (fun x hx ↦ by field)
    _ = (∫ x : ℝ in n..(n + 1), 1 / x) - n * ∫ x : ℝ in n..(n + 1), 1 / x ^ 2 := by
      simp_rw [← mul_one_div (n : ℝ)]
      rw [intervalIntegral.integral_sub]
      · simp_rw [intervalIntegral.integral_const_mul]
      · exact intervalIntegral.intervalIntegrable_one_div (fun x hx ↦ (hv x hx).ne') (by fun_prop)
      · exact (intervalIntegral.intervalIntegrable_one_div
          (fun x hx ↦ (sq_pos_of_pos (hv x hx)).ne') (by fun_prop)).const_mul _
    _ = (log (↑n + 1) - log ↑n) - n * ∫ x : ℝ in n..(n + 1), 1 / x ^ 2 := by
      congr 1
      rw [integral_one_div_of_pos, log_div]
      all_goals positivity
    _ = (log (↑n + 1) - log ↑n) - n * ∫ x : ℝ in n..(n + 1), x ^ (-2 : ℝ) := by
      congr 2
      refine intervalIntegral.integral_congr (fun x hx ↦ ?_)
      rw [rpow_neg, one_div, ← Nat.cast_two (R := ℝ), rpow_natCast]
      exact (hv x hx).le
    _ = log (↑n + 1) - log ↑n - n * (1 / n - 1 / (n + 1)) := by
      rw [integral_rpow]
      · simp_rw [sub_div, (by norm_num : (-2 : ℝ) + 1 = -1), div_neg, div_one, neg_sub_neg,
          rpow_neg_one, ← one_div]
      · refine Or.inr ⟨by simp, notMem_uIcc_of_lt ?_ ?_⟩
        all_goals positivity
    _ = log (↑n + 1) - log ↑n - 1 / (↑n + 1) := by
      congr 1
      simp [field]

Goal state after:
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.Height.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
n : ℕ
⊢ mulHeight₁ (x ^ ↑n) = mulHeight₁ x ^ (↑n).natAbs

Tactic:
zpow_natCast,

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
n : ℕ
⊢ mulHeight₁ (x ^ n) = mulHeight₁ x ^ (↑n).natAbs
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
n : ℤ
h : n < 0
⊢ mulHeight₁ (x ^ ↑n.natAbs) = mulHeight₁ x ^ n.natAbs

Tactic:
zpow_natCast,

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
n : ℤ
h : n < 0
⊢ mulHeight₁ (x ^ n.natAbs) = mulHeight₁ x ^ n.natAbs
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
n : ℤ
⊢ mulHeight₁ (x ^ n) = mulHeight₁ x ^ n.natAbs

Tactic:
by
  rcases le_or_gt 0 n with h | h
  · lift n to ℕ using h
    rw [zpow_natCast, mulHeight₁_pow, Int.natAbs_natCast]
  · nth_rewrite 1 [show n = -n.natAbs by grind]
    rw [zpow_neg, mulHeight₁_inv, zpow_natCast, mulHeight₁_pow]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : span {x} ≠ 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v | x ∈ v.asIdeal}
h_fin₀ : t₀.Finite
t₁ : Set (HeightOneSpectrum (𝓞 K)) := mulSupport fun v ↦ ‖(embedding v) ↑x‖
t₂ : Set (HeightOneSpectrum (𝓞 K)) := mulSupport fun v ↦ ↑(absNorm (v.maxPowDividing (span {x})))
h_fin₁ : t₁.Finite
v : HeightOneSpectrum (𝓞 K)
hv : ↑(absNorm (v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk (span {x})).factors)) ≠ 1
⊢ v.asIdeal ∣ span {x}

Tactic:
simp only [map_pow, Nat.cast_pow, ← pow_zero (absNorm v.asIdeal : ℝ)] at hv

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : span {x} ≠ 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v | x ∈ v.asIdeal}
h_fin₀ : t₀.Finite
t₁ : Set (HeightOneSpectrum (𝓞 K)) := mulSupport fun v ↦ ‖(embedding v) ↑x‖
t₂ : Set (HeightOneSpectrum (𝓞 K)) := mulSupport fun v ↦ ↑(absNorm (v.maxPowDividing (span {x})))
h_fin₁ : t₁.Finite
v : HeightOneSpectrum (𝓞 K)
hv :
  ↑(absNorm v.asIdeal) ^ (Associates.mk v.asIdeal).count (Associates.mk (span {x})).factors ≠ ↑(absNorm v.asIdeal) ^ 0
⊢ v.asIdeal ∣ span {x}
Module: Mathlib.NumberTheory.NumberField.ProductFormula

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
hb : b ≠ 0
ha : a ≠ 0
hb₀ : ↑((Algebra.norm ℤ) b) ≠ 0
⊢ (Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b * ↑b) = (Algebra.norm ℚ) ↑a

Tactic:
div_mul_cancel₀ _ (RingOfIntegers.coe_ne_zero_iff.mpr hb)

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
hb : b ≠ 0
ha : a ≠ 0
hb₀ : ↑((Algebra.norm ℤ) b) ≠ 0
⊢ (Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a) = (Algebra.norm ℚ) ↑a
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℝ
hs : 1 < s
⊢ Summable fun i ↦ 1 / (↑i + 1) ^ s

Tactic:
exact_mod_cast (summable_nat_add_iff 1).mpr (summable_one_div_nat_rpow.mpr hs)

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

Goal state before:
pp: s : ℝ
hs : 1 < s
n : ℕ
⊢ (↑n + 1) / (↑n + 1) ^ s = ↑(n + 1) * (↑(n + 1))⁻¹ ^ s

pp: case hx
s : ℝ
hs : 1 < s
n : ℕ
⊢ 1 / ↑(n + 1) ≠ 0

Tactic:
inv_rpow,

Goal state after:
s : ℝ
hs : 1 < s
n : ℕ
⊢ (↑n + 1) / (↑n + 1) ^ s = ↑(n + 1) * (↑(n + 1) ^ s)⁻¹

case hx
s : ℝ
hs : 1 < s
n : ℕ
⊢ 0 ≤ ↑(n + 1)

case hx
s : ℝ
hs : 1 < s
n : ℕ
⊢ 1 / ↑(n + 1) ≠ 0
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: ⊢ Tendsto (fun s ↦ riemannZeta ↑s - 1 / (↑s - 1)) (𝓝[>] 1) (𝓝 ↑γ)

Tactic:
suffices Tendsto (fun s : ℝ ↦ (∑' n : ℕ, 1 / (n + 1 : ℝ) ^ s) - 1 / (s - 1))
    (𝓝[>] 1) (𝓝 γ) by
    apply ((Complex.continuous_ofReal.tendsto _).comp this).congr'
    filter_upwards [self_mem_nhdsWithin] with s hs
    simp only [Function.comp_apply, Complex.ofReal_sub, Complex.ofReal_div,
      Complex.ofReal_one, sub_left_inj, Complex.ofReal_tsum]
    rw [zeta_eq_tsum_one_div_nat_add_one_cpow (by simpa using hs)]
    congr 1 with n
    rw [Complex.ofReal_cpow (by positivity)]
    norm_cast
  suffices aux2 : Tendsto (fun s : ℝ ↦ (∑' n : ℕ, 1 / (n + 1 : ℝ) ^ s) - 1 / (s - 1))
    (𝓝[>] 1) (𝓝 (1 - termTSum 1)) by
    have := term_tsum_one.tsum_eq
    rw [← termTSum, eq_sub_iff_add_eq, ← eq_sub_iff_add_eq'] at this
    simpa only [this] using aux2
  apply Tendsto.congr'
  · filter_upwards [self_mem_nhdsWithin] with s hs using (zeta_limit_aux1 hs).symm
  · apply tendsto_const_nhds.sub
    rw [← one_mul (termTSum 1)]
    apply (tendsto_id.mono_left nhdsWithin_le_nhds).mul
    have := continuousOn_termTSum.continuousWithinAt self_mem_Ici
    exact Tendsto.mono_left this (nhdsWithin_mono _ Ioi_subset_Ici_self)

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

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ riemannZeta s - 1 / (s - 1)
s : ℂ
hs : s ∈ {1}ᶜ
⊢ DifferentiableAt ℂ f s

Tactic:
refine (differentiableAt_riemannZeta hs).sub ((differentiableAt_const _).div ?_ ?_)

Goal state after:
case refine_1
f : ℂ → ℂ := fun s ↦ riemannZeta s - 1 / (s - 1)
s : ℂ
hs : s ∈ {1}ᶜ
⊢ DifferentiableAt ℂ (fun s ↦ s - 1) s

case refine_2
f : ℂ → ℂ := fun s ↦ riemannZeta s - 1 / (s - 1)
s : ℂ
hs : s ∈ {1}ᶜ
⊢ s - 1 ≠ 0
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ ∑ x, χ x + ∑ i, ψ i - ∑ x, 1 + ∑ x, (χ x - 1) * (ψ (1 - x) - 1) =
    ∑ x, χ x + ∑ x, ψ x - ∑ x, 1 + ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1)

Tactic:
sum_sdiff_eq_sub (subset_univ _),

Goal state after:
F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ ∑ x, χ x + ∑ i, ψ i - ∑ x, 1 + ∑ x, (χ x - 1) * (ψ (1 - x) - 1) =
    ∑ x, χ x + ∑ x, ψ x - ∑ x, 1 + (∑ x, (χ x - 1) * (ψ (1 - x) - 1) - ∑ x ∈ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1))
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case inr
s : ℂ
hs : s ≠ 1
hg_an : AnalyticOnNhd ℂ (fun z ↦ (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z))) {1}ᶜ
hgz : ∀ (z : ℂ), 1 < z.re → (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z)) = riemannZeta z
⊢ riemannZeta ((starRingEnd ℂ) s) = (starRingEnd ℂ) (riemannZeta s)

Tactic:
have heq : EqOn (fun z ↦ conj (riemannZeta (conj z))) riemannZeta {1}ᶜ :=
      hg_an.eqOn_of_preconnected_of_eventuallyEq analyticOn_riemannZeta
        (isConnected_compl_singleton_of_one_lt_rank (by simp) 1).isPreconnected
        (by norm_num : (2 : ℂ) ∈ _)
        (eventuallyEq_of_mem
          ((isOpen_lt continuous_const continuous_re).mem_nhds (by norm_num)) hgz)

Goal state after:
case inr
s : ℂ
hs : s ≠ 1
hg_an : AnalyticOnNhd ℂ (fun z ↦ (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z))) {1}ᶜ
hgz : ∀ (z : ℂ), 1 < z.re → (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z)) = riemannZeta z
heq : EqOn (fun z ↦ (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z))) riemannZeta {1}ᶜ
⊢ riemannZeta ((starRingEnd ℂ) s) = (starRingEnd ℂ) (riemannZeta s)
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: case a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : ¬n = 0
a : 𝓞 K
Hw : 0 < absNorm (span {↑n})
⊢ absNorm (span (Set.range ![a, ↑n])) ≤ absNorm (span {↑n})

Tactic:
exact Nat.le_of_dvd Hw <| absNorm_dvd_absNorm_of_le <| span_mono <| by simp

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

Goal state before:
pp: s : ℂ
hs : s ≠ 1
this : s - 1 ≠ 0
⊢ s - 1 ≠ 0

Tactic:
by exact this

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
⊢ {a | mulHeight ![↑a, ↑n] ≤ B} ⊆ {a | ∏ v, (⨆ i, v (![↑a, ↑n] i)) ^ v.mult ≤ ↑n ^ totalWeight K * B}

Tactic:
refine Set.ofPred_subset_ofPred_of_imp fun a ha ↦ ?_

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
a : 𝓞 K
ha : mulHeight ![↑a, ↑n] ≤ B
⊢ ∏ v, (⨆ i, v (![↑a, ↑n] i)) ^ v.mult ≤ ↑n ^ totalWeight K * B
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
n : ℕ
hn : n < f.natDegree
i : ℕ
hi : i < f.natDegree
⊢ Pi.single (↑⟨n, hn⟩) 1 ↑⟨i, hi⟩ = Pi.single n 1 i

Tactic:
by rw [Fin.val_mk, Fin.val_mk]

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

Goal state before:
pp: case succ
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
n✝ n : ℕ
hn : Nat.succ 0 ≤ n
hn₂ : n + 1 < orderOf χ
gauss_rw : gaussSum (χ ^ n) ψ * gaussSum χ ψ = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ
ih : gaussSum χ ψ ^ n * gaussSum χ ψ = (gaussSum (χ ^ n) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)) * gaussSum χ ψ
⊢ gaussSum χ ψ ^ (n + 1) = gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 (n + 1), jacobiSum χ (χ ^ j)

Tactic:
mul_right_comm,

Goal state after:
case succ
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
n✝ n : ℕ
hn : Nat.succ 0 ≤ n
hn₂ : n + 1 < orderOf χ
gauss_rw : gaussSum (χ ^ n) ψ * gaussSum χ ψ = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ
ih : gaussSum χ ψ ^ n * gaussSum χ ψ = gaussSum (χ ^ n) ψ * gaussSum χ ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)
⊢ gaussSum χ ψ ^ (n + 1) = gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 (n + 1), jacobiSum χ (χ ^ j)
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
⊢ Tendsto (fun s ↦ (s - 1) * LFunctionTrivChar N s) (𝓝[≠] 1) (𝓝 (∏ p ∈ N.primeFactors, (1 - (↑p)⁻¹)))

Tactic:
have H : (fun s ↦ (s - 1) * LFunctionTrivChar N s) =ᶠ[𝓝[≠] 1]
        fun s ↦ (∏ p ∈ N.primeFactors, (1 - (p : ℂ) ^ (-s))) * ((s - 1) * riemannZeta s) := by
    refine Set.EqOn.eventuallyEq_nhdsWithin fun s hs ↦ ?_
    rw [mul_left_comm, LFunctionTrivChar_eq_mul_riemannZeta hs]

Goal state after:
N : ℕ
inst✝ : NeZero N
H :
  (fun s ↦ (s - 1) * LFunctionTrivChar N s) =ᶠ[𝓝[≠] 1] fun s ↦
    (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)
⊢ Tendsto (fun s ↦ (s - 1) * LFunctionTrivChar N s) (𝓝[≠] 1) (𝓝 (∏ p ∈ N.primeFactors, (1 - (↑p)⁻¹)))
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: case neg
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}
h : ¬j = 0
⊢ IsOpen U

Tactic:
simp only [h, ↓reduceIte, isOpen_univ, U]

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

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

Tactic:
cosZeta_two_mul_nat hk hx

Goal state after:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / 2 / ↑(2 * k)! *
      Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k))) =
    (-1) ^ (k + 1) / (2 * ↑k) / (2 * ↑k).Gammaℂ *
      Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: case e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this : ↑(2 * k)! = 2 * ↑k * Complex.Gamma (2 * ↑k)
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / 2 / 2 / ↑k / Complex.Gamma (2 * ↑k) =
    (-1) ^ (k + 1) / 2 / ↑k / 2 / ((2 * ↑π) ^ (2 * ↑k))⁻¹ / Complex.Gamma (2 * ↑k)

Tactic:
div_inv_eq_mul,

Goal state after:
case e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this : ↑(2 * k)! = 2 * ↑k * Complex.Gamma (2 * ↑k)
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / 2 / 2 / ↑k / Complex.Gamma (2 * ↑k) =
    (-1) ^ (k + 1) / 2 / ↑k / 2 * (2 * ↑π) ^ (2 * ↑k) / Complex.Gamma (2 * ↑k)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: case e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this : ↑(2 * k + 1)! = (2 * ↑k + 1) * Complex.Gamma (2 * ↑k + 1)
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / (2 * ↑k + 1) / Complex.Gamma (2 * ↑k + 1) =
    (-1) ^ (k + 1) / (2 * ↑k + 1) / 2 / ((2 * ↑π) ^ (2 * ↑k + 1))⁻¹ / Complex.Gamma (2 * ↑k + 1)

Tactic:
div_inv_eq_mul,

Goal state after:
case e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this : ↑(2 * k + 1)! = (2 * ↑k + 1) * Complex.Gamma (2 * ↑k + 1)
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / (2 * ↑k + 1) / Complex.Gamma (2 * ↑k + 1) =
    (-1) ^ (k + 1) / (2 * ↑k + 1) / 2 * (2 * ↑π) ^ (2 * ↑k + 1) / Complex.Gamma (2 * ↑k + 1)
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case inr.refine_2
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
⊢ 1 / (-2 * ↑π * I * ↑n) * (0 - ↑(k + 1) * bernoulliFourierCoeff (k + 1 - 1) n) =
    -↑(k + 1)! / (2 * ↑π * I * ↑n) ^ (k + 1)

Tactic:
Nat.add_sub_cancel k 1,

Goal state after:
case inr.refine_2
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
⊢ 1 / (-2 * ↑π * I * ↑n) * (0 - ↑(k + 1) * bernoulliFourierCoeff k n) = -↑(k + 1)! / (2 * ↑π * I * ↑n) ^ (k + 1)
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
n : ℕ
⊢ 0 ≤ χ.zetaMul n

Tactic:
rcases eq_or_ne n 0 with rfl | hn
  · simp only [ArithmeticFunction.map_zero, le_refl]
  · simpa only [χ.isMultiplicative_zetaMul.multiplicative_factorization _ hn] using!
      Finset.prod_nonneg
        fun p hp ↦ zetaMul_prime_pow_nonneg hχ (Nat.prime_of_mem_primeFactors hp) _

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

Goal state before:
pp: p : Nat.Primes
k : ℕ
⊢ F'' (p, k) = Real.log ↑↑p * (↑↑p)⁻¹ ^ (k + 2)

Tactic:
by
      simp only [F'', Function.comp_apply, F', F₀, Prod.map_apply, id_eq, le_add_iff_nonneg_left,
        zero_le, Nat.Prime.not_prime_pow, ↓reduceIte, vonMangoldt_apply_prime p.prop,
        vonMangoldt_apply_pow (Nat.zero_ne_add_one _).symm, Nat.cast_pow, div_eq_mul_inv,
        inv_pow (p : ℝ) (k + 2)]

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

Goal state before:
pp: case refine_1.refine_2
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / ↑n ≤ F₀ n
hF₀ : ∀ (p : Nat.Primes), F₀ ↑p = 0
hFF' : F₀ ∘ Subtype.val = F' ∘ ⇑prodNatEquiv.symm
hF'₀ : ∀ (p : Nat.Primes), F' (p, 0) = 0
hF'₁ : F'' = F' ∘ Prod.map id fun x ↦ x + 1
u : Nat.Primes × ℕ
hu : u ∉ Set.range (Prod.map id fun x ↦ x + 1)
⊢ F' u = 0

Tactic:
simp only [Set.range_prodMap, Set.range_id, Set.mem_prod, Set.mem_univ, Set.mem_range,
      Nat.exists_add_one_eq, true_and, not_lt, nonpos_iff_eq_zero] at hu
    rw [← hF'₀ u.1, ← hu]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

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

pp: case right
⊢ 1 / 4 ≤ 1

Tactic:
· linarith

Goal state after:
case right
⊢ 1 / 4 ≤ 1
Module: Mathlib.NumberTheory.ZetaValues

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

Tactic:
· linarith

Goal state after:
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.JacobiSymbol

Goal state before:
pp: a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ (List.pmap (fun p pp ↦ legendreSym p a) b₁.primeFactorsList ⋯ ++
        List.pmap (fun p pp ↦ legendreSym p a) b₂.primeFactorsList ⋯).prod =
    J(a | b₁) * J(a | b₂)

pp: a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ ∀ a ∈ b₁.primeFactorsList ++ b₂.primeFactorsList, Nat.Prime a

Tactic:
List.prod_append

Goal state after:
a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ (List.pmap (fun p pp ↦ legendreSym p a) b₁.primeFactorsList ⋯).prod *
      (List.pmap (fun p pp ↦ legendreSym p a) b₂.primeFactorsList ⋯).prod =
    J(a | b₁) * J(a | b₂)

a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ ∀ a ∈ b₁.primeFactorsList ++ b₂.primeFactorsList, Nat.Prime a
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : s ∈ Set.Ioi 1
⊢ ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖ ≤ (s - 1) * s * C + s * ε

Tactic:
Set.mem_Ioi

Goal state after:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
⊢ ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖ ≤ (s - 1) * s * C + s * ε
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case mpr
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : Finite 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
hp' : v ↑p < 1
n : ℕ
hn : ‖↑p‖ ^ n < ε
hF : Finite (↥𝒪[K] ⧸ 𝓂[K] ^ n)
this : {y | v ↑y ≤ v ↑p ^ n} = Metric.closedBall 0 (‖p‖ ^ n)
i✝ : ↥𝒪[K] ⧸ 𝓂[K] ^ n
⊢ Metric.closedBall (Quotient.out i✝) (‖↑p‖ ^ n) ⊆ ⋃ y, Metric.ball y.out ε

Tactic:
exact (Metric.closedBall_subset_ball hn).trans (Set.subset_iUnion_of_subset _ le_rfl)

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

Goal state before:
pp: case inr
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
⊢ (Set.Icc z 1).Finite

Tactic:
have z0' : 0 < (z : MonoidHom.mrange (MonoidWithZeroHom.ofClass (Valued.v (R := K)))) := by simp

Goal state after:
case inr
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
⊢ (Set.Icc z 1).Finite