awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) (1 - s) =
      Φ j *
        ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
          (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s +
            cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) j) s))
simp :
  HPow.hPow (α := ℂ) (↑N : ℂ) (-(1 - s)) *
      ∑ x : ZMod N,
        Φ x *
          ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
            (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
              cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s)) =
    HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * ((2 * (↑π : ℂ)) ^ (-s) * Gamma s) *
      (cexp ((↑π : ℂ) * I * s / 2) * LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ) s +
        cexp (-(↑π : ℂ) * I * s / 2) *
          LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) fun (x : ZMod N) ↦ Φ (-x)) s)
⊢ HPow.hPow (α := ℂ) (↑N : ℂ) (-(1 - s)) *
      ∑ j : ZMod N, Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) (1 - s) =
    HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * (2 * (↑π : ℂ)) ^ (-s) * Gamma s *
      (cexp ((↑π : ℂ) * I * s / 2) * LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ) s +
        cexp (-(↑π : ℂ) * I * s / 2) *
          LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) fun (x : ZMod N) ↦ Φ (-x)) s)

Tactic:
simp only [this, mul_assoc _ _ (Gamma s)]

Premises used: mul_assoc, Complex.Gamma
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) (1 - s) =
      Φ j *
        ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
          (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s +
            cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) j) s))
generalize :
  ∀ (C : ℂ),
    HPow.hPow (α := ℂ) (↑N : ℂ) (-(1 - s)) *
        ∑ x : ZMod N,
          Φ x *
            (C *
              (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
                cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s)) =
      HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * C *
        (cexp ((↑π : ℂ) * I * s / 2) * LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ) s +
          cexp (-(↑π : ℂ) * I * s / 2) *
            LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) fun (x : ZMod N) ↦ Φ (-x)) s)
⊢ HPow.hPow (α := ℂ) (↑N : ℂ) (-(1 - s)) *
      ∑ x : ZMod N,
        Φ x *
          ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
            (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
              cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s)) =
    HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * ((2 * (↑π : ℂ)) ^ (-s) * Gamma s) *
      (cexp ((↑π : ℂ) * I * s / 2) * LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ) s +
        cexp (-(↑π : ℂ) * I * s / 2) *
          LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) fun (x : ZMod N) ↦ Φ (-x)) s)

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

Premises used: Real.pi, HMul.hMul, Complex.Gamma, OfNat.ofNat, Neg.neg
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) (1 - s) =
      Φ j *
        ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
          (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s +
            cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) j) s))
C : ℂ
simp_rw :
  C *
      (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) *
        ∑ x : ZMod N,
          Φ x *
            (cexp (-(↑π : ℂ) * (I * s) / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
              cexp ((↑π : ℂ) * (I * s) / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s)) =
    C *
      (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) *
        (cexp ((↑π : ℂ) * (I * s) / 2) * LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ) s +
          cexp (-(↑π : ℂ) * (I * s) / 2) *
            LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) fun (x : ZMod N) ↦ Φ (-x)) s))
⊢ HPow.hPow (α := ℂ) (↑N : ℂ) (-(1 - s)) *
      ∑ x : ZMod N,
        Φ x *
          (C *
            (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
              cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s)) =
    HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * C *
      (cexp ((↑π : ℂ) * I * s / 2) * LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ) s +
        cexp (-(↑π : ℂ) * I * s / 2) *
          LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) fun (x : ZMod N) ↦ Φ (-x)) s)

Tactic:
simp_rw [← mul_assoc, mul_comm _ C, mul_assoc, ← mul_sum, ← mul_assoc, mul_comm _ C, mul_assoc,
    neg_sub]

Premises used: Finset.mul_sum, neg_sub, mul_assoc, mul_comm
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) (1 - s) =
      Φ j *
        ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
          (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s +
            cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) j) s))
C : ℂ
e_a :
  ∑ x : ZMod N,
      Φ x *
        (cexp (-(↑π : ℂ) * (I * s) / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
          cexp ((↑π : ℂ) * (I * s) / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s) =
    cexp ((↑π : ℂ) * (I * s) / 2) * LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ) s +
      cexp (-(↑π : ℂ) * (I * s) / 2) *
        LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) fun (x : ZMod N) ↦ Φ (-x)) s
⊢ C *
      (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) *
        ∑ x : ZMod N,
          Φ x *
            (cexp (-(↑π : ℂ) * (I * s) / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
              cexp ((↑π : ℂ) * (I * s) / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s)) =
    C *
      (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) *
        (cexp ((↑π : ℂ) * (I * s) / 2) * LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ) s +
          cexp (-(↑π : ℂ) * (I * s) / 2) *
            LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) fun (x : ZMod N) ↦ Φ (-x)) s))

Tactic:
congr 2
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) (1 - s) =
      Φ j *
        ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
          (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s +
            cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) j) s))
C : ℂ
⊢ Φ 0 = 0 → Φ (-0) = 0

Tactic:
simp only [neg_zero, imp_self]

Premises used: imp_self, neg_zero
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) (1 - s) =
      Φ j *
        ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
          (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s +
            cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) j) s))
C : ℂ
e_a :
  ∑ x : ZMod N,
      Φ x *
        (cexp (-(↑π : ℂ) * (I * s) / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
          cexp ((↑π : ℂ) * (I * s) / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s) =
    cexp ((↑π : ℂ) * (I * s) / 2) * ∑ j : ZMod N, Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s +
      cexp (-(↑π : ℂ) * (I * s) / 2) *
        ∑ j : ZMod N, Φ (-j) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s
⊢ ∑ x : ZMod N,
      Φ x *
        (cexp (-(↑π : ℂ) * (I * s) / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
          cexp ((↑π : ℂ) * (I * s) / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s) =
    cexp ((↑π : ℂ) * (I * s) / 2) * LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) Φ) s +
      cexp (-(↑π : ℂ) * (I * s) / 2) *
        LFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) fun (x : ZMod N) ↦ Φ (-x)) s

Tactic:
rw [LFunction_dft _ hs', LFunction_dft _ (hs'.imp_left <| by simp only [neg_zero, imp_self])]

Premises used: Or.imp_left, ZMod.LFunction_dft
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) (1 - s) =
      Φ j *
        ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
          (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s +
            cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) j) s))
C : ℂ
enter : ∑ j : ZMod N, Φ (-j) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s
| cexp ((↑π : ℂ) * (I * s) / 2) * ∑ j : ZMod N, Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s +
    cexp (-(↑π : ℂ) * (I * s) / 2) *
      ∑ j : ZMod N, Φ (-j) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s

Tactic:
enter [2, 2]
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) (1 - s) =
      Φ j *
        ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
          (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s +
            cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) j) s))
C : ℂ
⊢ {a : ZMod N | (Equiv.neg (ZMod N) : (a : ZMod N) → ZMod N) a ≠ a} ⊆ (↑Finset.univ : Set (ZMod N))

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) (1 - s) =
      Φ j *
        ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
          (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s +
            cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) j) s))
C : ℂ
rw : ∑ x : ZMod N, Φ (- -x) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (- -x)) s
| ∑ j : ZMod N, Φ (-j) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s

Tactic:
rw [← (Equiv.neg _).sum_comp _ _ (by simp), Equiv.neg_apply]

Premises used: Equiv.neg, Equiv.neg_apply, Equiv.Perm.sum_comp
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) (1 - s) =
      Φ j *
        ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
          (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s +
            cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) j) s))
C : ℂ
enter : ∑ x : ZMod N, Φ (- -x) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (- -x)) s
| cexp ((↑π : ℂ) * (I * s) / 2) * ∑ j : ZMod N, Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s +
    cexp (-(↑π : ℂ) * (I * s) / 2) *
      ∑ j : ZMod N, Φ (-j) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s

Tactic:
enter [2, 2]; rw [← (Equiv.neg _).sum_comp _ _ (by simp), Equiv.neg_apply]

Premises used: Equiv.neg, Equiv.neg_apply, Equiv.Perm.sum_comp
-- Module: Mathlib.NumberTheory.LSeries.ZMod
Goal:
N : ℕ
inst : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) (1 - s) =
      Φ j *
        ((2 * (↑π : ℂ)) ^ (-s) * Gamma s *
          (cexp (-(↑π : ℂ) * I * s / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) j) s +
            cexp ((↑π : ℂ) * I * s / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) j) s))
C : ℂ
e_a :
  ∑ x : ZMod N,
      Φ x *
        (cexp (-(↑π : ℂ) * (I * s) / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
          cexp ((↑π : ℂ) * (I * s) / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s) =
    cexp ((↑π : ℂ) * (I * s) / 2) * ∑ j : ZMod N, Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s +
      cexp (-(↑π : ℂ) * (I * s) / 2) *
        ∑ x : ZMod N, Φ (- -x) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (- -x)) s
⊢ ∑ x : ZMod N,
      Φ x *
        (cexp (-(↑π : ℂ) * (I * s) / 2) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) x) s +
          cexp ((↑π : ℂ) * (I * s) / 2) * expZeta (-(toAddCircle : (a : ZMod N) → UnitAddCircle) x) s) =
    cexp ((↑π : ℂ) * (I * s) / 2) * ∑ j : ZMod N, Φ j * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s +
      cexp (-(↑π : ℂ) * (I * s) / 2) *
        ∑ j : ZMod N, Φ (-j) * expZeta ((toAddCircle : (a : ZMod N) → UnitAddCircle) (-j)) s

Tactic:
conv_rhs => enter [2, 2]; rw [← (Equiv.neg _).sum_comp _ _ (by simp), Equiv.neg_apply]

Premises used: Equiv.neg, Equiv.neg_apply, Equiv.Perm.sum_comp
-- Module: Mathlib.NumberTheory.LSeries.ZetaZeros
Goal:
z : ℂ
⊢ z ∈ riemannZetaZeros ↔ riemannZeta z = 0

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, Set.singleton, riemannZetaZeros
-- Module: Mathlib.NumberTheory.LSeries.ZetaZeros
Goal:
⊢ Membership.mem (γ := Set ℂ) {1}ᶜ 2

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.ZetaZeros
Goal:
refine_1 : riemannZeta 2 ≠ 0
refine_2 : IsConnected (α := ℂ) {1}ᶜ
⊢ Membership.mem (γ := Filter ℂ) (Filter.codiscreteWithin {1}ᶜ) riemannZetaZerosᶜ

Tactic:
refine analyticOn_riemannZeta.preimage_zero_mem_codiscreteWithin (x := 2) ?_ (by simp) ?_

Premises used: analyticOn_riemannZeta, AnalyticOnNhd.preimage_zero_mem_codiscreteWithin
-- Module: Mathlib.NumberTheory.LSeries.ZetaZeros
Goal:
⊢ riemannZeta 2 ≠ 0

Tactic:
riemannZeta_ne_zero_of_one_le_re Nat.one_le_ofNat

Premises used: Nat.one_le_ofNat, riemannZeta_ne_zero_of_one_le_re
-- Module: Mathlib.NumberTheory.LSeries.ZetaZeros
Goal:
⊢ riemannZeta 2 ≠ 0

Tactic:
exact riemannZeta_ne_zero_of_one_le_re Nat.one_le_ofNat

Premises used: riemannZeta_ne_zero_of_one_le_re
-- Module: Mathlib.NumberTheory.LSeries.ZetaZeros
Goal:
⊢ 1 < Module.rank ℝ ℂ

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.ZetaZeros
Goal:
⊢ IsConnected (α := ℂ) {1}ᶜ

Tactic:
exact isConnected_compl_singleton_of_one_lt_rank (by simp) 1

Premises used: isConnected_compl_singleton_of_one_lt_rank, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.ZetaZeros
Goal:
⊢ Membership.mem (γ := Filter ℂ) (Filter.codiscreteWithin {1}ᶜ) riemannZetaZerosᶜ

Tactic:
have := riemannZetaZeros_codiscreteWithin_compl_one
-- Module: Mathlib.NumberTheory.LSeries.ZetaZeros
Goal:
this : Membership.mem (γ := Filter ℂ) (Filter.codiscreteWithin {1}ᶜ) riemannZetaZerosᶜ
simp :
  ∀ (this : ∀ (x : ℂ), ¬x = 1 → ({1}ᶜ ∩ riemannZetaZeros)ᶜ ∈ nhdsWithin x {x}ᶜ) (x : ℂ),
    riemannZetaZerosᶜ ∈ nhdsWithin x {x}ᶜ
⊢ 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 ⊢

Premises used: compl_compl, mem_codiscrete, Set.mem_singleton_iff, mem_codiscreteWithin, sdiff_compl, Set.inf_eq_inter, Set.mem_compl_iff, Filter.disjoint_principal_right
-- Module: Mathlib.NumberTheory.LSeries.ZetaZeros
Goal:
this : ∀ (x : ℂ), ¬x = 1 → ({1}ᶜ ∩ riemannZetaZeros)ᶜ ∈ nhdsWithin x {x}ᶜ
x : ℂ
inl : Membership.mem (γ := Filter ℂ) (nhdsWithin 1 {1}ᶜ) riemannZetaZerosᶜ
inr : ∀ (hx : x ≠ 1), riemannZetaZerosᶜ ∈ nhdsWithin x {x}ᶜ
⊢ riemannZetaZerosᶜ ∈ nhdsWithin x {x}ᶜ

Tactic:
rcases eq_or_ne x 1 with rfl | hx

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.LSeries.ZetaZeros
Goal:
this : ∀ (x : ℂ), ¬x = 1 → ({1}ᶜ ∩ riemannZetaZeros)ᶜ ∈ nhdsWithin x {x}ᶜ
⊢ Membership.mem (γ := Filter ℂ) (nhdsWithin 1 {1}ᶜ) riemannZetaZerosᶜ

Tactic:
riemannZeta_eventually_ne_zero_nhds_one.filter_mono nhdsWithin_le_nhds

Premises used: Filter.Eventually.filter_mono, Set.Mem, Filter.Eventually, setOf, nhdsWithin_le_nhds, Set.preimage, Set.singleton, riemannZeta_eventually_ne_zero_nhds_one, riemannZetaZeros
-- Module: Mathlib.NumberTheory.LSeries.ZetaZeros
Goal:
this : ∀ (x : ℂ), ¬x = 1 → ({1}ᶜ ∩ riemannZetaZeros)ᶜ ∈ nhdsWithin x {x}ᶜ
⊢ Membership.mem (γ := Filter ℂ) (nhdsWithin 1 {1}ᶜ) riemannZetaZerosᶜ

Tactic:
exact riemannZeta_eventually_ne_zero_nhds_one.filter_mono nhdsWithin_le_nhds

Premises used: Filter.Eventually.filter_mono, nhdsWithin_le_nhds, riemannZeta_eventually_ne_zero_nhds_one
-- Module: Mathlib.NumberTheory.LSeries.ZetaZeros
Goal:
this : ∀ (x : ℂ), ¬x = 1 → ({1}ᶜ ∩ riemannZetaZeros)ᶜ ∈ nhdsWithin x {x}ᶜ
x : ℂ
hx : x ≠ 1
⊢ ({1}ᶜ ∩ riemannZetaZeros)ᶜ ⊆ riemannZetaZerosᶜ

Tactic:
grind [riemannZeta_one_ne_zero, mem_riemannZetaZeros]

Premises used: riemannZeta_one_ne_zero, mem_riemannZetaZeros
-- Module: Mathlib.NumberTheory.LSeries.ZetaZeros
Goal:
this : ∀ (x : ℂ), ¬x = 1 → ({1}ᶜ ∩ riemannZetaZeros)ᶜ ∈ nhdsWithin x {x}ᶜ
x : ℂ
hx : x ≠ 1
⊢ riemannZetaZerosᶜ ∈ nhdsWithin x {x}ᶜ

Tactic:
exact Filter.mem_of_superset (this x hx)
      (by grind [riemannZeta_one_ne_zero, mem_riemannZetaZeros])

Premises used: Filter.mem_of_superset
-- Module: Mathlib.NumberTheory.LSeries.ZetaZeros
Goal:
⊢ IsClosed riemannZetaZeros

Tactic:
simpa using (mem_codiscrete'.mp compl_riemannZetaZeros_mem_codiscrete).1

Premises used: mem_codiscrete', _private.0.compl_riemannZetaZeros_mem_codiscrete, And.left, Iff.mp
-- Module: Mathlib.NumberTheory.LSeries.ZetaZeros
Goal:
⊢ IsDiscrete riemannZetaZeros

Tactic:
simpa using (mem_codiscrete'.mp compl_riemannZetaZeros_mem_codiscrete).2

Premises used: mem_codiscrete', _private.0.compl_riemannZetaZeros_mem_codiscrete, And.right, Iff.mp
-- Module: Mathlib.NumberTheory.LSeries.ZetaZeros
Goal:
S : Set ℂ
hS : IsCompact S
apply : IsDiscrete (S ∩ riemannZetaZeros)
⊢ (S ∩ riemannZetaZeros).Finite

Tactic:
apply (hS.inter_right isClosed_riemannZetaZeros).finite

Premises used: isClosed_riemannZetaZeros, IsCompact.inter_right, IsCompact.finite
-- Module: Mathlib.NumberTheory.LSeries.ZetaZeros
Goal:
S : Set ℂ
hS : IsCompact S
⊢ IsDiscrete (S ∩ riemannZetaZeros)

Tactic:
isDiscrete_riemannZetaZeros.mono Set.inter_subset_right

Premises used: IsDiscrete.mono, isDiscrete_riemannZetaZeros, Set.inter_subset_right
-- Module: Mathlib.NumberTheory.LSeries.ZetaZeros
Goal:
S : Set ℂ
hS : IsCompact S
⊢ IsDiscrete (S ∩ riemannZetaZeros)

Tactic:
exact isDiscrete_riemannZetaZeros.mono Set.inter_subset_right

Premises used: IsDiscrete.mono, isDiscrete_riemannZetaZeros, Set.inter_subset_right
-- Module: Mathlib.NumberTheory.LSeries.ZetaZeros
Goal:
⊢ Tendsto (α := { x : ℂ // x ∈ riemannZetaZeros }) (Subtype.val (p := fun (x : ℂ) ↦ x ∈ riemannZetaZeros)) cofinite
    (cocompact ℂ)

Tactic:
isClosed_riemannZetaZeros.tendsto_coe_cofinite_of_isDiscrete isDiscrete_riemannZetaZeros

Premises used: IsClosed.tendsto_coe_cofinite_of_isDiscrete, isClosed_riemannZetaZeros, isDiscrete_riemannZetaZeros
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
R : Type u
inst : CommRing R
R' : Type v
inst_1 : CommMonoid R'
φ : AddChar R R'
a : R
h : 0 < ringChar R
⊢ Membership.mem (γ := Subgroup R'ˣ) (rootsOfUnity (↑(ringChar R).toPNat' : ℕ) R')
    (IsUnit.unit (a := (φ : (a : R) → R') a) ⋯)

Tactic:
simp only [mem_rootsOfUnity', IsUnit.unit_spec, Nat.toPNat'_coe, h, ↓reduceIte,
    ← map_nsmul_eq_pow, nsmul_eq_mul, CharP.cast_eq_zero, zero_mul, map_zero_eq_one]

Premises used: CharP.cast_eq_zero, AddChar.map_nsmul_eq_pow, Nat.toPNat'_coe, MulZeroClass.zero_mul, AddChar.map_zero_eq_one, nsmul_eq_mul, reduceIte, mem_rootsOfUnity', IsUnit.unit_spec
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
R : Type u
inst : CommRing R
R' : Type v
inst_1 : CommMonoid R'
R'' : Type u_1
inst_2 : CommMonoid R''
φ : AddChar R R'
f : R' →* R''
hφ : φ.IsPrimitive
hf : Function.Injective.{v + 1, u_1 + 1} (α := R') (β := R'') (⇑f : (a : R') → R'')
a : R
ha : a ≠ 0
⊢ (f.compAddChar φ).mulShift a ≠ 1

Tactic:
simpa [DFunLike.ext_iff] using (MonoidHom.compAddChar_injective_right f hf).ne (hφ ha)

Premises used: Function.Injective.ne, DFunLike.ext_iff, MonoidHom.compAddChar_injective_right
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
R : Type u
inst : CommRing R
R' : Type v
inst_1 : CommMonoid R'
ψ : AddChar R R'
hψ : ψ.IsPrimitive
a b : R
h : ψ.mulShift a = ψ.mulShift b
⊢ ψ.mulShift a * ψ.mulShift (-b) = ψ.mulShift b * ψ.mulShift (-b)

Tactic:
apply_fun fun x => x * mulShift ψ (-b) at h

Premises used: HMul.hMul, Neg.neg, AddChar.mulShift
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
R : Type u
inst : CommRing R
R' : Type v
inst_1 : CommMonoid R'
ψ : AddChar R R'
hψ : ψ.IsPrimitive
a b : R
h : ψ.mulShift a * ψ.mulShift (-b) = ψ.mulShift b * ψ.mulShift (-b)
⊢ ψ.mulShift (a + -b) = 1

Tactic:
simp only [mulShift_mul, mulShift_zero, add_neg_cancel] at h

Premises used: add_neg_cancel, AddChar.mulShift_mul, AddChar.mulShift_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
R : Type u
inst : CommRing R
R' : Type v
inst_1 : CommMonoid R'
ψ : AddChar R R'
hψ : ψ.IsPrimitive
a b : R
h : ψ.mulShift (a + -b) = 1
⊢ a = b

Tactic:
simpa [← sub_eq_add_neg, sub_eq_zero] using (hψ · h)

Premises used: sub_eq_zero, sub_eq_add_neg
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
R' : Type v
inst : CommMonoid R'
F : Type u
inst_1 : Field F
ψ : AddChar F R'
hψ : ψ ≠ 1
a : F
ha : a ≠ 0
h : ψ.mulShift a = 1
⊢ ψ = 1

Tactic:
simpa [mulShift_mulShift, ha] using congr_arg (mulShift · a⁻¹) h

Premises used: congr_arg, Inv.inv, AddChar.mulShift_mulShift, AddChar.mulShift
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
R : Type u
inst : CommRing R
R' : Type v
inst_1 : CommMonoid R'
inst_2 : Finite R
e : AddChar R R'
r : R
hr : ¬IsUnit r
simp : ∃ (x : R) (_ : x ≠ 0), ¬(e.mulShift r).mulShift x ≠ 1
⊢ ¬(e.mulShift r).IsPrimitive

Tactic:
simp only [IsPrimitive, not_forall]

Premises used: AddChar.IsPrimitive, Classical.not_forall
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
R : Type u
inst : CommRing R
R' : Type v
inst_1 : CommMonoid R'
inst_2 : Finite R
e : AddChar R R'
r : R
hr : ¬IsUnit r
⊢ ∃ (x : R) (_ : x * r = 0), ¬x = 0

Tactic:
simp only [isUnit_iff_mem_nonZeroDivisors_of_finite,
    mem_nonZeroDivisors_iff_right, not_forall] at hr

Premises used: mem_nonZeroDivisors_iff_right, isUnit_iff_mem_nonZeroDivisors_of_finite, Classical.not_forall
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
R : Type u
inst : CommRing R
R' : Type v
inst_1 : CommMonoid R'
inst_2 : Finite R
e : AddChar R R'
r : R
hr : ∃ (x : R) (_ : x * r = 0), ¬x = 0
rcases : ∀ (x : R) (h : x * r = 0) (h' : ¬x = 0), ∃ (x : R) (_ : x ≠ 0), ¬(e.mulShift r).mulShift x ≠ 1
⊢ ∃ (x : R) (_ : x ≠ 0), ¬(e.mulShift r).mulShift x ≠ 1

Tactic:
rcases hr with ⟨x, h, h'⟩