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

Goal state before:
pp: case e'_3.refine_3.«0»
q : ℚ
this : Finset.univ.gcd ![q.num, ↑q.den] = 1
⊢ |![q.num, ↑q.den] ((fun i ↦ i) ⟨0, ⋯⟩)| ≤ max |q.num| ↑q.den

pp: case e'_3.refine_3.«1»
q : ℚ
this : Finset.univ.gcd ![q.num, ↑q.den] = 1
⊢ |![q.num, ↑q.den] ((fun i ↦ i) ⟨1, ⋯⟩)| ≤ max |q.num| ↑q.den

Tactic:
<;>

Goal state after:
case e'_3.refine_3.«0»
q : ℚ
this : Finset.univ.gcd ![q.num, ↑q.den] = 1
⊢ |![q.num, ↑q.den] ((fun i ↦ i) ⟨0, ⋯⟩)| ≤ max |q.num| ↑q.den

case e'_3.refine_3.«1»
q : ℚ
this : Finset.univ.gcd ![q.num, ↑q.den] = 1
⊢ |![q.num, ↑q.den] ((fun i ↦ i) ⟨1, ⋯⟩)| ≤ max |q.num| ↑q.den
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
z : S
i : ℕ
⊢ h.coeff z i = if hi : i < f.natDegree then (h.basis.repr z) ⟨i, hi⟩ else 0

Tactic:
by
  split_ifs with hi
  · exact h.coeff_apply_lt z i hi
  · exact h.coeff_apply_le z i (le_of_not_gt hi)

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

Goal state before:
pp: K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
⊢ ∃ C,
    ∀ {a b c d : K},
      ![a, b] ≠ 0 → ![c, d] ≠ 0 → C + logHeight ![a, b] + logHeight ![c, d] ≤ logHeight ![a * c, a * d + b * c, b * d]

Tactic:
by
  obtain ⟨C', hC₀, hC⟩ := mulHeight_sym2_ge K
  refine ⟨log C', fun hab hcd ↦ ?_⟩
  simp only [logHeight_eq_log_mulHeight]
  pull (disch := positivity) log
  exact log_le_log (by positivity) (hC hab hcd)

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

Goal state before:
pp: case ha
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : ↑j.val / ↑N ∈ Set.Icc 0 1
m : ℕ
⊢ 0 ≤ ↑N

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

Tactic:
<;>

Goal state after:
case ha
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : ↑j.val / ↑N ∈ Set.Icc 0 1
m : ℕ
⊢ 0 ≤ ↑N

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

Goal state before:
pp: case inl
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
h : s ≠ 0 ∨ N ≠ 1
hχ : χ.Even
⊢ LFunction χ s = completedLFunction χ s / χ.gammaFactor s

pp: case inr
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
h : s ≠ 0 ∨ N ≠ 1
hχ : χ.Odd
⊢ LFunction χ s = completedLFunction χ s / χ.gammaFactor s

Tactic:
<;>

Goal state after:
case inl
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
h : s ≠ 0 ∨ N ≠ 1
hχ : χ.Even
⊢ LFunction χ s = completedLFunction χ s / χ.gammaFactor s

case inr
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
h : s ≠ 0 ∨ N ≠ 1
hχ : χ.Odd
⊢ LFunction χ s = completedLFunction χ s / χ.gammaFactor s
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))
⊢ ↑N ^ (-(1 - s)) *
      ∑ x,
        Φ x *
          ((2 * ↑π) ^ (-s) * Gamma s *
            (cexp (-↑π * I * s / 2) * expZeta (toAddCircle x) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle x) s)) =
    ↑N ^ (s - 1) * ((2 * ↑π) ^ (-s) * Gamma s) *
      (cexp (↑π * I * s / 2) * LFunction (𝓕 Φ) s + cexp (-↑π * I * s / 2) * LFunction (𝓕 fun x ↦ Φ (-x)) s)

Tactic:
generalize (2 * π) ^ (-s) * Gamma s = C

Goal state after:
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 : ℂ
⊢ ↑N ^ (-(1 - s)) *
      ∑ x,
        Φ x *
          (C *
            (cexp (-↑π * I * s / 2) * expZeta (toAddCircle x) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle x) s)) =
    ↑N ^ (s - 1) * C *
      (cexp (↑π * I * s / 2) * LFunction (𝓕 Φ) s + cexp (-↑π * I * s / 2) * LFunction (𝓕 fun x ↦ Φ (-x)) s)
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case neg
k : ℕ
k1 : ¬k = 1
⊢ bernoulliFun k 2⁻¹ = (2 / 2 ^ k - 1) * ↑(bernoulli k)

Tactic:
have m := bernoulliFun_mul k two_ne_zero 2⁻¹

Goal state after:
case neg
k : ℕ
k1 : ¬k = 1
m : bernoulliFun k (↑2 * 2⁻¹) = ↑2 ^ k / ↑2 * ∑ i ∈ Finset.range 2, bernoulliFun k (2⁻¹ + ↑i / ↑2)
⊢ bernoulliFun k 2⁻¹ = (2 / 2 ^ k - 1) * ↑(bernoulli k)
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: case e_a.e_f
N : ℕ
inst✝ : NeZero N
a : ℂ
Φ : ZMod N → ℂ
s : ℂ
i : ZMod N
⊢ ↑N ^ (-s) * (a * Φ i * completedHurwitzZetaEven (toAddCircle i) s) =
    a * (↑N ^ (-s) * (Φ i * completedHurwitzZetaEven (toAddCircle i) s))

pp: case e_a.e_f
N : ℕ
inst✝ : NeZero N
a : ℂ
Φ : ZMod N → ℂ
s : ℂ
i : ZMod N
⊢ ↑N ^ (-s) * (a * Φ i * completedHurwitzZetaOdd (toAddCircle i) s) =
    a * (↑N ^ (-s) * (Φ i * completedHurwitzZetaOdd (toAddCircle i) s))

Tactic:
<;>

Goal state after:
case e_a.e_f
N : ℕ
inst✝ : NeZero N
a : ℂ
Φ : ZMod N → ℂ
s : ℂ
i : ZMod N
⊢ ↑N ^ (-s) * (a * Φ i * completedHurwitzZetaEven (toAddCircle i) s) =
    a * (↑N ^ (-s) * (Φ i * completedHurwitzZetaEven (toAddCircle i) s))

case e_a.e_f
N : ℕ
inst✝ : NeZero N
a : ℂ
Φ : ZMod N → ℂ
s : ℂ
i : ZMod N
⊢ ↑N ^ (-s) * (a * Φ i * completedHurwitzZetaOdd (toAddCircle i) s) =
    a * (↑N ^ (-s) * (Φ i * completedHurwitzZetaOdd (toAddCircle i) s))
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case pos
k : ℕ
n : ℤ
hn : n ≠ 0
h✝ : k = 1
⊢ ↑1 = 1

pp: case neg
k : ℕ
n : ℤ
hn : n ≠ 0
h✝ : ¬k = 1
⊢ ↑0 = 0

Tactic:
<;>

Goal state after:
case pos
k : ℕ
n : ℤ
hn : n ≠ 0
h✝ : k = 1
⊢ ↑1 = 1

case neg
k : ℕ
n : ℤ
hn : n ≠ 0
h✝ : ¬k = 1
⊢ ↑0 = 0
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case inl
k : ℕ
hk : k ≠ 0
⊢ 0 = -↑k ! / 0

Tactic:
div_zero

Goal state after:
case inl
k : ℕ
hk : k ≠ 0
⊢ 0 = 0
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: case refine_1
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
⊢ Differentiable ℂ fun s ↦ ↑N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaEven₀ (toAddCircle j) s

pp: case refine_2
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
⊢ Differentiable ℂ fun s ↦ ↑N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaOdd (toAddCircle j) s

Tactic:
<;>

Goal state after:
case refine_1
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
⊢ Differentiable ℂ fun s ↦ ↑N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaEven₀ (toAddCircle j) s

case refine_2
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
⊢ Differentiable ℂ fun s ↦ ↑N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaOdd (toAddCircle j) s
Module: Mathlib.NumberTheory.LSeries.Linearity

Goal state before:
pp: case zero
f g : ℕ → ℂ
s : ℂ
⊢ term (f + g) s 0 = (term f s + term g s) 0

pp: case succ
f g : ℕ → ℂ
s : ℂ
n✝ : ℕ
⊢ term (f + g) s (n✝ + 1) = (term f s + term g s) (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
f g : ℕ → ℂ
s : ℂ
⊢ term (f + g) s 0 = (term f s + term g s) 0

case succ
f g : ℕ → ℂ
s : ℂ
n✝ : ℕ
⊢ term (f + g) s (n✝ + 1) = (term f s + term g s) (n✝ + 1)
Module: Mathlib.NumberTheory.LSeries.Linearity

Goal state before:
pp: case zero
f : ℕ → ℂ
s : ℂ
⊢ term (-f) s 0 = (-term f s) 0

pp: case succ
f : ℕ → ℂ
s : ℂ
n✝ : ℕ
⊢ term (-f) s (n✝ + 1) = (-term f s) (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
f : ℕ → ℂ
s : ℂ
⊢ term (-f) s 0 = (-term f s) 0

case succ
f : ℕ → ℂ
s : ℂ
n✝ : ℕ
⊢ term (-f) s (n✝ + 1) = (-term f s) (n✝ + 1)
Module: Mathlib.NumberTheory.LSeries.Linearity

Goal state before:
pp: case zero
f : ℕ → ℂ
c s : ℂ
⊢ term (c • f) s 0 = (c • term f s) 0

pp: case succ
f : ℕ → ℂ
c s : ℂ
n✝ : ℕ
⊢ term (c • f) s (n✝ + 1) = (c • term f s) (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
f : ℕ → ℂ
c s : ℂ
⊢ term (c • f) s 0 = (c • term f s) 0

case succ
f : ℕ → ℂ
c s : ℂ
n✝ : ℕ
⊢ term (c • f) s (n✝ + 1) = (c • term f s) (n✝ + 1)
Module: Mathlib.NumberTheory.LSeries.Linearity

Goal state before:
pp: case zero
f : ℕ → ℂ
c s : ℂ
⊢ term (c • f) s 0 = (c • term f s) 0

Tactic:
simp [mul_div_assoc]

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

Goal state before:
pp: case succ
f : ℕ → ℂ
c s : ℂ
n✝ : ℕ
⊢ term (c • f) s (n✝ + 1) = (c • term f s) (n✝ + 1)

Tactic:
simp [mul_div_assoc]

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

Goal state before:
pp: case inl
ι : Type u_1
f : ι → ℕ → ℂ
S : Finset ι
s : ℂ
n : ℕ
hn : n = 0
⊢ term (∑ i ∈ S, f i) s n = ∑ i ∈ S, term (f i) s n

pp: case inr
ι : Type u_1
f : ι → ℕ → ℂ
S : Finset ι
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ term (∑ i ∈ S, f i) s n = ∑ i ∈ S, term (f i) s n

Tactic:
<;>

Goal state after:
case inl
ι : Type u_1
f : ι → ℕ → ℂ
S : Finset ι
s : ℂ
n : ℕ
hn : n = 0
⊢ term (∑ i ∈ S, f i) s n = ∑ i ∈ S, term (f i) s n

case inr
ι : Type u_1
f : ι → ℕ → ℂ
S : Finset ι
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ term (∑ i ∈ S, f i) s n = ∑ i ∈ S, term (f i) s n
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: case hs
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := ⋯
G : ℂ → ℂ := ⋯
U : Set ℂ := ⋯
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
Uc : Set ℂ := ⋯
⊢ (if ∑ j, Φ j = 0 then ∅ else {0}).Countable

pp: case ht
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := ⋯
G : ℂ → ℂ := ⋯
U : Set ℂ := ⋯
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
Uc : Set ℂ := ⋯
⊢ (if Φ 0 = 0 then ∅ else {1}).Countable

Tactic:
<;>

Goal state after:
case hs
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := ⋯
G : ℂ → ℂ := ⋯
U : Set ℂ := ⋯
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
Uc : Set ℂ := ⋯
⊢ (if ∑ j, Φ j = 0 then ∅ else {0}).Countable

case ht
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := ⋯
G : ℂ → ℂ := ⋯
U : Set ℂ := ⋯
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
Uc : Set ℂ := ⋯
⊢ (if Φ 0 = 0 then ∅ else {1}).Countable
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:
have hac₀ : ‖(a : ℂ)‖ < 1 := by
    simp only [Complex.norm_of_nonneg ha₀, ha₁]

Goal state after:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
⊢ 0 ≤ 3 * (-log (1 - ↑a)).re + 4 * (-log (1 - ↑a * z)).re + (-log (1 - ↑a * z ^ 2)).re
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: case pos
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
Uc : Set ℂ := (if ∑ j, Φ j = 0 then ∅ else {0}) ∪ if Φ 0 = 0 then ∅ else {1}
this : Uc.Countable
x : ℂ
h : Φ 0 = 0
⊢ x ∈ U ↔ x ∈ Ucᶜ

pp: case neg
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
Uc : Set ℂ := (if ∑ j, Φ j = 0 then ∅ else {0}) ∪ if Φ 0 = 0 then ∅ else {1}
this : Uc.Countable
x : ℂ
h : ¬Φ 0 = 0
⊢ x ∈ U ↔ x ∈ Ucᶜ

Tactic:
<;>

Goal state after:
case pos
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
Uc : Set ℂ := (if ∑ j, Φ j = 0 then ∅ else {0}) ∪ if Φ 0 = 0 then ∅ else {1}
this : Uc.Countable
x : ℂ
h : Φ 0 = 0
⊢ x ∈ U ↔ x ∈ Ucᶜ

case neg
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
Uc : Set ℂ := (if ∑ j, Φ j = 0 then ∅ else {0}) ∪ if Φ 0 = 0 then ∅ else {1}
this : Uc.Countable
x : ℂ
h : ¬Φ 0 = 0
⊢ x ∈ U ↔ x ∈ Ucᶜ
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
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * completedLFunction (𝓕 Φ) s

Tactic:
have hUp : IsPreconnected U := by
    -- need to write `U` as the complement of an obviously countable set
    let Uc : Set ℂ := (if ∑ j, Φ j = 0 then ∅ else {0}) ∪ (if Φ 0 = 0 then ∅ else {1})
    have : Uc.Countable := by
      apply Countable.union <;>
      split_ifs <;>
      simp only [countable_singleton, countable_empty]
    convert! (this.isConnected_compl_of_one_lt_rank ?_).isPreconnected using 1
    · ext x
      by_cases h : Φ 0 = 0 <;>
      by_cases h' : ∑ j, Φ j = 0 <;>
      simp [U, Uc, h, h', and_comm]
    · simp only [rank_real_complex, Nat.one_lt_ofNat]

Goal state after:
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
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * completedLFunction (𝓕 Φ) s
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

Goal state after:
case pos
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn✝ : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit ↑n
hn : ↑n ^ (-x) < 1
⊢ 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
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
pk : Nat.Primes × ℕ
| (↑↑pk.1)⁻¹ ^ ↑pk.2 * (↑↑pk.1)⁻¹ ^ (3 / 2)

Tactic:
Real.rpow_natCast

Goal state after:
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
pk : Nat.Primes × ℕ
| (↑↑pk.1)⁻¹ ^ pk.2 * (↑↑pk.1)⁻¹ ^ (3 / 2)
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
⊢ Summable fun pk ↦ (↑↑pk.1)⁻¹ ^ (↑pk.2 + 3 / 2)

Tactic:
conv => enter [1, pk]; rw [Real.rpow_add <| hp₀ pk.1, Real.rpow_natCast]

Goal state after:
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
⊢ Summable fun pk ↦ (↑↑pk.1)⁻¹ ^ pk.2 * (↑↑pk.1)⁻¹ ^ (3 / 2)
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ ∑' (a_1 : ℕ), ↑(residueClass a a_1) / ↑a_1 ^ ↑x = ↑(LFunctionResidueClassAux a ↑x).re + (↑q.totient)⁻¹ / (↑x - 1)

Tactic:
simp_rw [← LFunctionResidueClassAux_real ha hx,
      eqOn_LFunctionResidueClassAux ha <| Set.mem_ofPred.mpr (ofReal_re x ▸ hx), sub_add_cancel,
      LSeries, term]

Goal state after:
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ ∑' (a_1 : ℕ), ↑(residueClass a a_1) / ↑a_1 ^ ↑x = ∑' (n : ℕ), if n = 0 then 0 else ↑(residueClass a n) / ↑n ^ ↑x
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

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

pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
x✝¹ : ℕ
x✝ : x✝¹ ∈ Ico 1 (p / 2).succ
h✝ : ¬(↑a * ↑x✝¹).val ≤ p / 2
⊢ ↑(↑a * ↑x✝¹).val = -1 * -(↑a * ↑x✝¹)

Tactic:
<;>

Goal state after:
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
x✝¹ : ℕ
x✝ : x✝¹ ∈ Ico 1 (p / 2).succ
h✝ : (↑a * ↑x✝¹).val ≤ p / 2
⊢ ↑(↑a * ↑x✝¹).val = 1 * (↑a * ↑x✝¹)

case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
x✝¹ : ℕ
x✝ : x✝¹ ∈ Ico 1 (p / 2).succ
h✝ : ¬(↑a * ↑x✝¹).val ≤ p / 2
⊢ ↑(↑a * ↑x✝¹).val = -1 * -(↑a * ↑x✝¹)
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: case inl
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : ↑a ≠ 0
hp : Odd p
this : ↑(legendreSym p a) = ↑((-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val}))
h✝ : legendreSym p a = 1
⊢ legendreSym p a = (-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val})

pp: case inr
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : ↑a ≠ 0
hp : Odd p
this : ↑(legendreSym p a) = ↑((-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val}))
h✝ : legendreSym p a = -1
⊢ legendreSym p a = (-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val})

Tactic:
<;>

Goal state after:
case inl
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : ↑a ≠ 0
hp : Odd p
this : ↑(legendreSym p a) = ↑((-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val}))
h✝ : legendreSym p a = 1
⊢ legendreSym p a = (-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val})

case inr
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : ↑a ≠ 0
hp : Odd p
this : ↑(legendreSym p a) = ↑((-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val}))
h✝ : legendreSym p a = -1
⊢ legendreSym p a = (-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val})
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: case inl.inl
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : ↑a ≠ 0
hp : Odd p
this : ↑(legendreSym p a) = ↑((-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val}))
h✝¹ : legendreSym p a = 1
h✝ : (-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val}) = 1
⊢ legendreSym p a = (-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val})

pp: case inl.inr
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : ↑a ≠ 0
hp : Odd p
this : ↑(legendreSym p a) = ↑((-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val}))
h✝¹ : legendreSym p a = 1
h✝ : (-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val}) = -1
⊢ legendreSym p a = (-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val})

pp: case inr.inl
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : ↑a ≠ 0
hp : Odd p
this : ↑(legendreSym p a) = ↑((-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val}))
h✝¹ : legendreSym p a = -1
h✝ : (-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val}) = 1
⊢ legendreSym p a = (-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val})

pp: case inr.inr
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : ↑a ≠ 0
hp : Odd p
this : ↑(legendreSym p a) = ↑((-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val}))
h✝¹ : legendreSym p a = -1
h✝ : (-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val}) = -1
⊢ legendreSym p a = (-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val})

Tactic:
<;>

Goal state after:
case inl.inl
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : ↑a ≠ 0
hp : Odd p
this : ↑(legendreSym p a) = ↑((-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val}))
h✝¹ : legendreSym p a = 1
h✝ : (-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val}) = 1
⊢ legendreSym p a = (-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val})

case inl.inr
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : ↑a ≠ 0
hp : Odd p
this : ↑(legendreSym p a) = ↑((-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val}))
h✝¹ : legendreSym p a = 1
h✝ : (-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val}) = -1
⊢ legendreSym p a = (-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val})

case inr.inl
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : ↑a ≠ 0
hp : Odd p
this : ↑(legendreSym p a) = ↑((-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val}))
h✝¹ : legendreSym p a = -1
h✝ : (-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val}) = 1
⊢ legendreSym p a = (-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val})

case inr.inr
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : ↑a ≠ 0
hp : Odd p
this : ↑(legendreSym p a) = ↑((-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val}))
h✝¹ : legendreSym p a = -1
h✝ : (-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val}) = -1
⊢ legendreSym p a = (-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val})
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable (fun n ↦ if n = 0 then 0 else f n) s
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
this : ∀ (n : ℕ), (∑ k ∈ Icc 1 n, if k = 0 then 0 else f k) = ∑ k ∈ Icc 1 n, f k
⊢ s * ∫ (t : ℝ) in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, if k = 0 then 0 else f k) * ↑t ^ (-(s + 1)) =
    s * ∫ (t : ℝ) in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-(s + 1))

pp: f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable (fun n ↦ if n = 0 then 0 else f n) s
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
this : ∀ (n : ℕ), (∑ k ∈ Icc 1 n, if k = 0 then 0 else f k) = ∑ k ∈ Icc 1 n, f k
⊢ (fun n ↦ ∑ k ∈ Icc 1 n, if k = 0 then 0 else f k) =O[atTop] fun n ↦ ↑n ^ r

pp: f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable (fun n ↦ if n = 0 then 0 else f n) s
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
this : ∀ (n : ℕ), (∑ k ∈ Icc 1 n, if k = 0 then 0 else f k) = ∑ k ∈ Icc 1 n, f k
⊢ ∀ {n : ℕ}, n ≠ 0 → ¬n = 0

Tactic:
<;>

Goal state after:
f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable (fun n ↦ if n = 0 then 0 else f n) s
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
this : ∀ (n : ℕ), (∑ k ∈ Icc 1 n, if k = 0 then 0 else f k) = ∑ k ∈ Icc 1 n, f k
⊢ s * ∫ (t : ℝ) in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, if k = 0 then 0 else f k) * ↑t ^ (-(s + 1)) =
    s * ∫ (t : ℝ) in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-(s + 1))

f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable (fun n ↦ if n = 0 then 0 else f n) s
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
this : ∀ (n : ℕ), (∑ k ∈ Icc 1 n, if k = 0 then 0 else f k) = ∑ k ∈ Icc 1 n, f k
⊢ (fun n ↦ ∑ k ∈ Icc 1 n, if k = 0 then 0 else f k) =O[atTop] fun n ↦ ↑n ^ r

f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable (fun n ↦ if n = 0 then 0 else f n) s
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
this : ∀ (n : ℕ), (∑ k ∈ Icc 1 n, if k = 0 then 0 else f k) = ∑ k ∈ Icc 1 n, f k
⊢ ∀ {n : ℕ}, n ≠ 0 → ¬n = 0
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p q : ℕ
hp0 : ¬p = 0
⊢ ∑ a ∈ Ico 1 (p / 2).succ, #({x ∈ Ico 1 (q / 2).succ | x * p ≤ a * q}) =
    #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q})

Tactic:
simp only [card_eq_sum_ones, sum_filter, sum_product]

Goal state after: