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

Goal state before:
pp: case e_a
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ∫ (x : ℝ) in ↑n..↑n + 1, 1 / x = log (↑n + 1) - log ↑n

Tactic:
integral_one_div_of_pos,

Goal state after:
case e_a
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ log ((↑n + 1) / ↑n) = log (↑n + 1) - log ↑n

case e_a.ha
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ 0 < ↑n

case e_a.hb
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ 0 < ↑n + 1
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
hx : x ≠ 0
H : x • ![x⁻¹, 1] = ![1, x]
⊢ mulHeight (x • ![x⁻¹, 1]) = mulHeight ![x, 1]

Tactic:
H,

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
hx : x ≠ 0
H : x • ![x⁻¹, 1] = ![1, x]
⊢ mulHeight ![1, x] = mulHeight ![x, 1]
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
h_fin₂ : t₂.Finite
h_prod :
  ↑(absNorm (∏ᶠ (v : HeightOneSpectrum (𝓞 K)), v.maxPowDividing (span {x}))) =
    ∏ᶠ (v : HeightOneSpectrum (𝓞 K)), ↑(absNorm (v.maxPowDividing (span {x})))
⊢ (∏ᶠ (i : HeightOneSpectrum (𝓞 K)), ‖(embedding i) ↑x‖) *
      ∏ᶠ (v : HeightOneSpectrum (𝓞 K)), ↑(absNorm (v.maxPowDividing (span {x}))) =
    1

Tactic:
← finprod_mul_distrib h_fin₁ h_fin₂

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
h_fin₂ : t₂.Finite
h_prod :
  ↑(absNorm (∏ᶠ (v : HeightOneSpectrum (𝓞 K)), v.maxPowDividing (span {x}))) =
    ∏ᶠ (v : HeightOneSpectrum (𝓞 K)), ↑(absNorm (v.maxPowDividing (span {x})))
⊢ ∏ᶠ (i : HeightOneSpectrum (𝓞 K)), ‖(embedding i) ↑x‖ * ↑(absNorm (i.maxPowDividing (span {x}))) = 1
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
h_fin₂ : t₂.Finite
h_prod :
  ↑(absNorm (∏ᶠ (v : HeightOneSpectrum (𝓞 K)), v.maxPowDividing (span {x}))) =
    ∏ᶠ (v : HeightOneSpectrum (𝓞 K)), ↑(absNorm (v.maxPowDividing (span {x})))
⊢ (∏ᶠ (i : HeightOneSpectrum (𝓞 K)), ‖(embedding i) ↑x‖) *
      ↑(absNorm (∏ᶠ (v : HeightOneSpectrum (𝓞 K)), v.maxPowDividing (span {x}))) =
    1

Tactic:
rw [h_prod, ← finprod_mul_distrib h_fin₁ h_fin₂]

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
h_fin₂ : t₂.Finite
h_prod :
  ↑(absNorm (∏ᶠ (v : HeightOneSpectrum (𝓞 K)), v.maxPowDividing (span {x}))) =
    ∏ᶠ (v : HeightOneSpectrum (𝓞 K)), ↑(absNorm (v.maxPowDividing (span {x})))
⊢ ∏ᶠ (i : HeightOneSpectrum (𝓞 K)), ‖(embedding i) ↑x‖ * ↑(absNorm (i.maxPowDividing (span {x}))) = 1
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case c0
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
⊢ 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), max (↑v (∑ a ∈ s, x a)) 1

pp: case b0
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
⊢ 0 ≤ (Multiset.map (fun i ↦ ↑(#s) * ∏ a ∈ s, max (i (x a)) 1) archAbsVal).prod

pp: case h₁
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
⊢ (Multiset.map (fun v ↦ max (v (∑ a ∈ s, x a)) 1) archAbsVal).prod ≤
    (Multiset.map (fun i ↦ ↑(#s) * ∏ a ∈ s, max (i (x a)) 1) archAbsVal).prod

pp: case h₂
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
⊢ ∏ᶠ (v : ↑nonarchAbsVal), max (↑v (∑ a ∈ s, x a)) 1 ≤ ∏ᶠ (a : ↑nonarchAbsVal), ∏ b ∈ s, max (↑a (x b)) 1

Tactic:
· exact finprod_nonneg fun _ ↦ by positivity

Goal state after:
case b0
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
⊢ 0 ≤ (Multiset.map (fun i ↦ ↑(#s) * ∏ a ∈ s, max (i (x a)) 1) archAbsVal).prod

case h₁
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
⊢ (Multiset.map (fun v ↦ max (v (∑ a ∈ s, x a)) 1) archAbsVal).prod ≤
    (Multiset.map (fun i ↦ ↑(#s) * ∏ a ∈ s, max (i (x a)) 1) archAbsVal).prod

case h₂
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
⊢ ∏ᶠ (v : ↑nonarchAbsVal), max (↑v (∑ a ∈ s, x a)) 1 ≤ ∏ᶠ (a : ↑nonarchAbsVal), ∏ b ∈ s, max (↑a (x b)) 1
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
α : Type u_2
s : Finset α
x : α → K
hs : s.Nonempty
this✝ : ∀ a ∈ s, mulHeight₁ (x a) ≠ 0
this : ↑(#s) ^ totalWeight K ≠ 0
⊢ log (mulHeight₁ (∑ a ∈ s, x a)) ≤ log (↑(#s) ^ totalWeight K * ∏ i ∈ s, mulHeight₁ (x i))

Tactic:
exact (log_le_log <| by positivity) <| mulHeight₁_sum_le hs x

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

Goal state before:
pp: case refine_1
f : ℂ → ℂ := fun s ↦ riemannZeta s - 1 / (s - 1)
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] 1, DifferentiableAt ℂ f z

pp: case refine_2
f : ℂ → ℂ := fun s ↦ riemannZeta s - 1 / (s - 1)
⊢ (fun z ↦ f z - f 1) =o[𝓝[≠] 1] fun z ↦ (z - 1)⁻¹

Tactic:
· filter_upwards [self_mem_nhdsWithin] with s hs
    refine (differentiableAt_riemannZeta hs).sub ((differentiableAt_const _).div ?_ ?_)
    · fun_prop
    · rwa [mem_compl_singleton_iff, ← sub_ne_zero] at hs

Goal state after:
case refine_2
f : ℂ → ℂ := fun s ↦ riemannZeta s - 1 / (s - 1)
⊢ (fun z ↦ f z - f 1) =o[𝓝[≠] 1] fun z ↦ (z - 1)⁻¹
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
M : Type u_2
inst✝ : AddCommMonoid M
f : AbsoluteValue K ℝ → M
w : AbsoluteValue K ℝ
hw : w ∈ archAbsVal.toFinset
⊢ count w archAbsVal • f w = InfinitePlace.mult ⟨w, ⋯⟩ • f ↑⟨w, ⋯⟩

Tactic:
simp only [archAbsVal, mem_toFinset, mem_multisetInfinitePlace] at hw ⊢
      simp [count_multisetInfinitePlace_eq_mult ⟨w, hw⟩]

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

Goal state before:
pp: ⊢ (↑γ - log (4 * ↑π)) / 2 = ↑(γ - Real.log (4 * π)) / ↑2

Tactic:
ofReal_sub,

Goal state after:
⊢ (↑γ - log (4 * ↑π)) / 2 = (↑γ - ↑(Real.log (4 * π))) / ↑2
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case inr
K : Type u_6
inst✝³ : Field K
ι : Type u_7
ι' : Type u_8
inst✝² : Fintype ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h : ∀ (k : ι), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (M + N)
h✝ : Nonempty ι'
q' : ι × ι' → K := fun a ↦ (eval x) (q a)
H : mulHeight x ^ (M + N) ≤ ↑(Nat.card ι') ^ totalWeight K * mulHeight q' * mulHeight fun j ↦ (eval x) (p j)
⊢ mulHeight x ^ (M + N) ≤
    (↑(Nat.card ι') ^ totalWeight K * max (mulHeightBound q) 1 * mulHeight fun j ↦ (eval x) (p j)) * mulHeight x ^ M

Tactic:
H,

Goal state after:
case inr
K : Type u_6
inst✝³ : Field K
ι : Type u_7
ι' : Type u_8
inst✝² : Fintype ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h : ∀ (k : ι), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (M + N)
h✝ : Nonempty ι'
q' : ι × ι' → K := fun a ↦ (eval x) (q a)
H : mulHeight x ^ (M + N) ≤ ↑(Nat.card ι') ^ totalWeight K * mulHeight q' * mulHeight fun j ↦ (eval x) (p j)
⊢ (↑(Nat.card ι') ^ totalWeight K * mulHeight q' * mulHeight fun j ↦ (eval x) (p j)) ≤
    (↑(Nat.card ι') ^ totalWeight K * max (mulHeightBound q) 1 * mulHeight fun j ↦ (eval x) (p j)) * mulHeight x ^ M
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)
⊢ mulHeight₁ x ≤ B → ∃ x_1, IsIntegral ℤ ((↑↑x_1 + 1) * x)

Tactic:
refine fun h ↦ ⟨⟨n - 1, by grind [Nat.le_floor <| hn₁.trans h]⟩, ?_⟩

Goal state after:
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
⊢ IsIntegral ℤ ((↑↑⟨n - 1, ⋯⟩ + 1) * x)
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
x y : S
hxy : ∀ i < f.natDegree, h.coeff x i = h.coeff y i
i : Fin f.natDegree
⊢ h.basis.equivFun x i = h.basis.equivFun y i

Tactic:
Basis.equivFun_apply,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
x y : S
hxy : ∀ i < f.natDegree, h.coeff x i = h.coeff y i
i : Fin f.natDegree
⊢ (h.basis.repr x) i = h.basis.equivFun y i
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
x y : S
hxy : ∀ i < f.natDegree, h.coeff x i = h.coeff y i
i : Fin f.natDegree
⊢ h.coeff x ↑i = h.basis.equivFun y i

Tactic:
Basis.equivFun_apply,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
x y : S
hxy : ∀ i < f.natDegree, h.coeff x i = h.coeff y i
i : Fin f.natDegree
⊢ h.coeff x ↑i = (h.basis.repr y) i
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: case inr
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hs : 1 ≠ 1 ∨ ∑ j, Φ j = 0
⊢ DifferentiableAt ℂ (fun s ↦ ∑ j, Φ j * hurwitzZeta (toAddCircle j) s) 1

Tactic:
have := DifferentiableAt.fun_sum (u := univ) fun j _ ↦
      (differentiableAt_hurwitzZeta_sub_one_div (toAddCircle j)).const_mul (Φ j)

Goal state after:
case inr
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hs : 1 ≠ 1 ∨ ∑ j, Φ j = 0
this : DifferentiableAt ℂ (fun y ↦ ∑ i, Φ i * (hurwitzZeta (toAddCircle i) y - 1 / (y - 1) / y.Gammaℝ)) 1
⊢ DifferentiableAt ℂ (fun s ↦ ∑ j, Φ j * hurwitzZeta (toAddCircle j) s) 1
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: case inr
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hs : 1 ≠ 1 ∨ ∑ j, Φ j = 0
⊢ DifferentiableAt ℂ (fun s ↦ ∑ j, Φ j * hurwitzZeta (toAddCircle j) s) 1

Tactic:
· have := DifferentiableAt.fun_sum (u := univ) fun j _ ↦
      (differentiableAt_hurwitzZeta_sub_one_div (toAddCircle j)).const_mul (Φ j)
    simpa only [mul_sub, sum_sub_distrib, ← sum_mul, hs.neg_resolve_left rfl, zero_mul, sub_zero]

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
⊢ completedLFunction χ (1 - s) =
    (↑N ^ (s - 1) * χ (-1) / I ^ if χ.Even then 0 else 1) * ZMod.completedLFunction (𝓕 ⇑χ) s

Tactic:
split_ifs with h

Goal state after:
case pos
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
h : χ.Even
⊢ completedLFunction χ (1 - s) = ↑N ^ (s - 1) * χ (-1) / I ^ 0 * ZMod.completedLFunction (𝓕 ⇑χ) s

case neg
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
h : ¬χ.Even
⊢ completedLFunction χ (1 - s) = ↑N ^ (s - 1) * χ (-1) / I ^ 1 * ZMod.completedLFunction (𝓕 ⇑χ) s
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
s : ℂ
hs : s ≠ 1
H : deriv (LFunctionTrivChar₁ n) s = deriv (fun w ↦ (w - 1) * LFunctionTrivChar n w) s
⊢ deriv (LFunctionTrivChar₁ n) s = (s - 1) * deriv (LFunctionTrivChar n) s + LFunctionTrivChar n s

Tactic:
H,

Goal state after:
n : ℕ
inst✝ : NeZero n
s : ℂ
hs : s ≠ 1
H : deriv (LFunctionTrivChar₁ n) s = deriv (fun w ↦ (w - 1) * LFunctionTrivChar n w) s
⊢ deriv (fun w ↦ (w - 1) * LFunctionTrivChar n w) s = (s - 1) * deriv (LFunctionTrivChar n) s + LFunctionTrivChar n s
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
⊢ LFunction (fun k ↦ 𝕖 (j * k)) s = expZeta (toAddCircle j) s

Tactic:
let U := if j = 0 then {z : ℂ | z ≠ 1} else univ -- region of analyticity of both functions
  let V := {z : ℂ | 1 < re z} -- convergence region
  have hUo : IsOpen U := by
    by_cases h : j = 0
    · simpa only [h, ↓reduceIte, U] using! isOpen_compl_singleton
    · simp only [h, ↓reduceIte, isOpen_univ, U]
  let f := LFunction (fun k ↦ stdAddChar (j * k))
  let g := expZeta (toAddCircle j)
  have hU {u} : u ∈ U ↔ u ≠ 1 ∨ j ≠ 0 := by simp only [mem_ite_univ_right, U]; tauto
  -- hypotheses for uniqueness of analytic continuation
  have hf : AnalyticOnNhd ℂ f U := by
    refine DifferentiableOn.analyticOnNhd (fun u hu ↦ ?_) hUo
    refine (differentiableAt_LFunction _ _ ((hU.mp hu).imp_right fun h ↦ ?_)).differentiableWithinAt
    simp only [mul_comm j, AddChar.sum_mulShift _ (isPrimitive_stdAddChar _), h,
      ↓reduceIte, CharP.cast_eq_zero]
  have hg : AnalyticOnNhd ℂ g U := by
    refine DifferentiableOn.analyticOnNhd (fun u hu ↦ ?_) hUo
    refine (differentiableAt_expZeta _ _ ((hU.mp hu).imp_right fun h ↦ ?_)).differentiableWithinAt
    rwa [ne_eq, toAddCircle_eq_zero]
  have hUc : IsPreconnected U := by
    by_cases h : j = 0
    · simpa only [h, ↓reduceIte, U] using!
        (isConnected_compl_singleton_of_one_lt_rank (by simp) _).isPreconnected
    · simpa only [h, ↓reduceIte, U] using isPreconnected_univ
  have hV : V ∈ 𝓝 2 := (continuous_re.isOpen_preimage _ isOpen_Ioi).mem_nhds (by simp)
  have hUmem : 2 ∈ U := by simp [U]
  have hUmem' : s ∈ U := hU.mpr hjs.symm
  -- apply uniqueness result
  refine hf.eqOn_of_preconnected_of_eventuallyEq hg hUc hUmem ?_ hUmem'
  -- now remains to prove equality on `1 < re s`
  filter_upwards [hV] with z using LFunction_stdAddChar_eq_expZeta_of_one_lt_re _

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
⊢ (algebraMap ℚ ℝ) (bernoulli' k) = ↑(bernoulli k) + if k = 1 then 1 else 0

Tactic:
split_ifs with h

Goal state after:
case pos
k : ℕ
h : k = 1
⊢ (algebraMap ℚ ℝ) (bernoulli' k) = ↑(bernoulli k) + 1

case neg
k : ℕ
h : ¬k = 1
⊢ (algebraMap ℚ ℝ) (bernoulli' k) = ↑(bernoulli k) + 0
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)! = (-1) ^ (k + 1) / (2 * ↑k + 1) / (2 * ↑k + 1).Gammaℂ

Tactic:
simp_rw [this, Gammaℂ, cpow_neg, ← div_div, div_inv_eq_mul, div_mul_eq_mul_div, div_div]

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 * ↑π) ^ (2 * ↑k + 1) / ((2 * ↑k + 1) * 2 * Complex.Gamma (2 * ↑k + 1))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
n : ℕ
⊢ 2 * ↑k ≠ -↑n

Tactic:
← Int.cast_ofNat,

Goal state after:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
n : ℕ
⊢ ↑2 * ↑k ≠ -↑n
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
n : ℕ
⊢ 2 * ↑k + 1 ≠ -↑n

Tactic:
← Int.cast_ofNat,

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
n : ℕ
⊢ LFunction Φ (-(2 * (↑n + 1))) = 0

Tactic:
simp only [LFunction_def_even hΦ, hurwitzZetaEven_neg_two_mul_nat_add_one, mul_zero,
    sum_const_zero, ← neg_mul]

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

Goal state before:
pp: this : riemannZetaZerosᶜ ∈ Filter.codiscreteWithin {1}ᶜ
⊢ riemannZetaZerosᶜ ∈ Filter.codiscrete ℂ

Tactic:
simp only [mem_codiscreteWithin, Set.mem_compl_iff, Set.mem_singleton_iff, sdiff_compl,
    Set.inf_eq_inter, Filter.disjoint_principal_right, mem_codiscrete, compl_compl] at this ⊢

Goal state after:
this : ∀ (x : ℂ), ¬x = 1 → ({1}ᶜ ∩ riemannZetaZeros)ᶜ ∈ nhdsWithin x {x}ᶜ
⊢ ∀ (x : ℂ), riemannZetaZerosᶜ ∈ nhdsWithin x {x}ᶜ
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: n q : ℕ
a : ℤ
hq : q ≠ 0
h : IsCoprime a ↑q
this : NeZero q
⊢ IsUnit ↑a

Tactic:
ZMod.coe_int_isUnit_iff_isCoprime,

Goal state after:
n q : ℕ
a : ℤ
hq : q ≠ 0
h : IsCoprime a ↑q
this : NeZero q
⊢ IsCoprime (↑q) 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)
s : ℝ
hs : 1 < s
h₁ : LocallyIntegrableOn (fun t ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume
⊢ IntegrableOn (fun t ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume

Tactic:
have h₂ : (fun t : ℝ ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) =O[atTop] fun t ↦ t ^ (1 : ℝ) := by
    simp_rw [Real.rpow_one]
    refine IsBigO.trans_isEquivalent ?_ isEquivalent_nat_floor
    have : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ((n : ℝ) ^ (1 : ℝ) : ℝ)) atTop (𝓝 l) := by
      simpa using! hlim
    simpa using! (isBigO_atTop_natCast_rpow_of_tendsto_div_rpow this).comp_tendsto
        tendsto_nat_floor_atTop

Goal state after:
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
⊢ IntegrableOn (fun t ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume
Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient

Goal state before:
pp: 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) ⋯
this : I = (f ∘ₗ g).ker
e : (R ⧸ I) ≃ₗ[R] R ⧸ (f ∘ₗ g).ker := Submodule.quotEquivOfEq I (f ∘ₗ g).ker this
⊢ (R ⧸ I) ≃ₗ[R] ↥(I ^ n) ⧸ I • ⊤

Tactic:
refine e.trans ((f.comp g).quotKerEquivOfSurjective ?_)

Goal state after:
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) ⋯
this : I = (f ∘ₗ g).ker
e : (R ⧸ I) ≃ₗ[R] R ⧸ (f ∘ₗ g).ker := Submodule.quotEquivOfEq I (f ∘ₗ g).ker this
⊢ Function.Surjective ⇑(f ∘ₗ g)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inr
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ J(↑a | b) = J(↑(2 ^ e * a') | b % (4 * a))

Tactic:
nth_rw 1 [ha₂]

Goal state after:
case inr
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ J(↑(2 ^ e * a') | b) = J(↑(2 ^ e * a') | b % (4 * a))
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case ind.isFalse.isFalse.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
ha1 : ¬a = 1
h✝ : b % a = 0
⊢ 0 = if flip = true then -J(↑a | b) else J(↑a | b)

Tactic:
rename_i hba

Goal state after:
case ind.isFalse.isFalse.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
ha1 : ¬a = 1
hba : b % a = 0
⊢ 0 = if flip = true then -J(↑a | b) else J(↑a | b)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case ind.isFalse.isFalse.isFalse.isFalse
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
h✝ : ¬b % a = 0
⊢ fastJacobiSymAux (b % a) a (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) ⋯ = if flip = true then -J(↑a | b) else J(↑a | b)

Tactic:
rename_i hba

Goal state after:
case ind.isFalse.isFalse.isFalse.isFalse
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
⊢ fastJacobiSymAux (b % a) a (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) ⋯ = if flip = true then -J(↑a | b) else J(↑a | b)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case neg
a : ℤ
ha2 : ¬a % 2 = 0
b : ℕ
IH : ∀ m < 2 * b, J(a | m) = fastJacobiSym a m
hb0 : ¬2 * b = 0
hb2 : 2 * b % 2 = 0
⊢ J(1 | 2) * J(a | b) = J(a | b)

Tactic:
one_left,

Goal state after:
case neg
a : ℤ
ha2 : ¬a % 2 = 0
b : ℕ
IH : ∀ m < 2 * b, J(a | m) = fastJacobiSym a m
hb0 : ¬2 * b = 0
hb2 : 2 * b % 2 = 0
⊢ 1 * J(a | b) = J(a | b)
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 : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
h₃ : (↑s - 1) * ∫ (t : ℝ) in Set.Ioi 1, ↑t ^ (-↑s) = 1
Cs : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-s - 1)
h₄ : Cs ≤ C
⊢ (s - 1) * s * ∫ (t : ℝ) in Set.Ioi 1, ‖(S t - l * ↑t) * ↑t ^ (-↑s - 1)‖ =
    (s - 1) * s * ∫ (t : ℝ) in Set.Ioi 1, ‖S t - l * ↑t‖ * t ^ (-s - 1)

Tactic:
congr 1
      refine setIntegral_congr_fun measurableSet_Ioi fun t ht ↦ ?_
      replace ht : 0 ≤ t := zero_le_one.trans ht.le
      rw [norm_mul, show (-(s : ℂ) - 1) = (-s - 1 : ℝ) by simp, ← ofReal_cpow ht, norm_real,
        Real.norm_of_nonneg (Real.rpow_nonneg ht _)]

Goal state after: