mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case e_a.e_a
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      (cexp (2 * ↑π * I * ↑a * ↑(n + 1)) + cexp (-(2 * ↑π * I * ↑a * ↑(n + 1)))) * ↑(rexp (-π * ↑(n + 1) ^ 2 * t)))
    (↑(cosKernel (↑a) t) - 1)
n : ℕ
⊢ 2 * ↑π * ↑a * (↑n + 1) * I = 2 * ↑π * I * ↑a * (↑n + 1)

pp: case e_a.e_a
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      (cexp (2 * ↑π * I * ↑a * ↑(n + 1)) + cexp (-(2 * ↑π * I * ↑a * ↑(n + 1)))) * ↑(rexp (-π * ↑(n + 1) ^ 2 * t)))
    (↑(cosKernel (↑a) t) - 1)
n : ℕ
⊢ -(2 * ↑π * ↑a * (↑n + 1)) * I = -(2 * ↑π * I * ↑a * (↑n + 1))

Tactic:
<;>

Goal state after:
case e_a.e_a
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      (cexp (2 * ↑π * I * ↑a * ↑(n + 1)) + cexp (-(2 * ↑π * I * ↑a * ↑(n + 1)))) * ↑(rexp (-π * ↑(n + 1) ^ 2 * t)))
    (↑(cosKernel (↑a) t) - 1)
n : ℕ
⊢ 2 * ↑π * ↑a * (↑n + 1) * I = 2 * ↑π * I * ↑a * (↑n + 1)

case e_a.e_a
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      (cexp (2 * ↑π * I * ↑a * ↑(n + 1)) + cexp (-(2 * ↑π * I * ↑a * ↑(n + 1)))) * ↑(rexp (-π * ↑(n + 1) ^ 2 * t)))
    (↑(cosKernel (↑a) t) - 1)
n : ℕ
⊢ -(2 * ↑π * ↑a * (↑n + 1)) * I = -(2 * ↑π * I * ↑a * (↑n + 1))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : τ.im ≤ 0
⊢ (-1 / τ).im ≤ 0

Tactic:
rw [neg_div, neg_im, one_div, inv_im, neg_nonpos]

Goal state after:
z τ : ℂ
hτ : τ.im ≤ 0
⊢ 0 ≤ -τ.im / normSq τ
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case inl.hτ
z τ : ℂ
hτ : τ.im ≤ 0
⊢ (-1 / τ).im ≤ 0

pp: case inl.hτ
z τ : ℂ
hτ : τ.im ≤ 0
⊢ (-1 / τ).im ≤ 0

Tactic:
<;>

Goal state after:
case inl.hτ
z τ : ℂ
hτ : τ.im ≤ 0
⊢ (-1 / τ).im ≤ 0

case inl.hτ
z τ : ℂ
hτ : τ.im ≤ 0
⊢ (-1 / τ).im ≤ 0
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case inl.hτ
z τ : ℂ
hτ : τ.im ≤ 0
⊢ (-1 / τ).im ≤ 0

Tactic:
rw [neg_div, neg_im, one_div, inv_im, neg_nonpos]

Goal state after:
case inl.hτ
z τ : ℂ
hτ : τ.im ≤ 0
⊢ 0 ≤ -τ.im / normSq τ
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case inl.hτ
z τ : ℂ
hτ : τ.im ≤ 0
⊢ 0 ≤ -τ.im / normSq τ

pp: case inl.hτ
z τ : ℂ
hτ : τ.im ≤ 0
⊢ 0 ≤ -τ.im / normSq τ

Tactic:
<;>

Goal state after:
case inl.hτ
z τ : ℂ
hτ : τ.im ≤ 0
⊢ 0 ≤ -τ.im / normSq τ

case inl.hτ
z τ : ℂ
hτ : τ.im ≤ 0
⊢ 0 ≤ -τ.im / normSq τ
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case e_f
⊢ { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 0 then 1 else 0, g₀ := 1,
        hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯,
        hf_top := ⋯, hg_top := ⋯ }.g =
    ofReal ∘ evenKernel 0

pp: case e_g
⊢ { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 0 then 1 else 0, g₀ := 1,
        hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯,
        hf_top := ⋯, hg_top := ⋯ }.f =
    ofReal ∘ cosKernel 0

pp: case e_ε
⊢ { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 0 then 1 else 0, g₀ := 1,
          hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯,
          hf_top := ⋯, hg_top := ⋯ }.ε⁻¹ =
    1

pp: case e_f₀
⊢ { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 0 then 1 else 0, g₀ := 1,
        hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯,
        hf_top := ⋯, hg_top := ⋯ }.g₀ =
    if 0 = 0 then 1 else 0

pp: case e_g₀
⊢ { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 0 then 1 else 0, g₀ := 1,
        hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯,
        hf_top := ⋯, hg_top := ⋯ }.f₀ =
    1

Tactic:
<;>

Goal state after:
case e_f
⊢ { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 0 then 1 else 0, g₀ := 1,
        hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯,
        hf_top := ⋯, hg_top := ⋯ }.g =
    ofReal ∘ evenKernel 0

case e_g
⊢ { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 0 then 1 else 0, g₀ := 1,
        hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯,
        hf_top := ⋯, hg_top := ⋯ }.f =
    ofReal ∘ cosKernel 0

case e_ε
⊢ { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 0 then 1 else 0, g₀ := 1,
          hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯,
          hf_top := ⋯, hg_top := ⋯ }.ε⁻¹ =
    1

case e_f₀
⊢ { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 0 then 1 else 0, g₀ := 1,
        hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯,
        hf_top := ⋯, hg_top := ⋯ }.g₀ =
    if 0 = 0 then 1 else 0

case e_g₀
⊢ { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 0 then 1 else 0, g₀ := 1,
        hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯,
        hf_top := ⋯, hg_top := ⋯ }.f₀ =
    1
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case e_f
a : UnitAddCircle
⊢ ofReal ∘ evenKernel (-a) = ofReal ∘ evenKernel a

pp: case e_g
a : UnitAddCircle
⊢ ofReal ∘ cosKernel (-a) = ofReal ∘ cosKernel a

pp: case e_f₀
a : UnitAddCircle
⊢ (if -a = 0 then 1 else 0) = if a = 0 then 1 else 0

Tactic:
<;>

Goal state after:
case e_f
a : UnitAddCircle
⊢ ofReal ∘ evenKernel (-a) = ofReal ∘ evenKernel a

case e_g
a : UnitAddCircle
⊢ ofReal ∘ cosKernel (-a) = ofReal ∘ cosKernel a

case e_f₀
a : UnitAddCircle
⊢ (if -a = 0 then 1 else 0) = if a = 0 then 1 else 0
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun w ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ 1 / (-I * τ) ^ (1 / 2) *
      (deriv (fun z ↦ cexp (-↑π * I * z ^ 2 * τ⁻¹)) z * jacobiTheta₂ (z * τ⁻¹) (-1 * τ⁻¹) +
        cexp (-↑π * I * z ^ 2 * τ⁻¹) * (1 * τ⁻¹ * jacobiTheta₂' (z * τ⁻¹) (-1 * τ⁻¹))) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 * τ⁻¹) * τ⁻¹ *
      (jacobiTheta₂' (z * τ⁻¹) (-1 * τ⁻¹) - 2 * ↑π * I * z * jacobiTheta₂ (z * τ⁻¹) (-1 * τ⁻¹))

Tactic:
deriv_cexp (((differentiableAt_pow _).const_mul _).mul_const _),

Goal state after:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun w ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ 1 / (-I * τ) ^ (1 / 2) *
      (cexp (-↑π * I * z ^ 2 * τ⁻¹) * deriv (fun z ↦ -↑π * I * z ^ 2 * τ⁻¹) z * jacobiTheta₂ (z * τ⁻¹) (-1 * τ⁻¹) +
        cexp (-↑π * I * z ^ 2 * τ⁻¹) * (1 * τ⁻¹ * jacobiTheta₂' (z * τ⁻¹) (-1 * τ⁻¹))) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 * τ⁻¹) * τ⁻¹ *
      (jacobiTheta₂' (z * τ⁻¹) (-1 * τ⁻¹) - 2 * ↑π * I * z * jacobiTheta₂ (z * τ⁻¹) (-1 * τ⁻¹))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a t : ℝ
ht : 0 < t
h : -2 * ↑π ≠ 0
n : ℤ
⊢ -I * ↑n * (cexp (2 * ↑π * I * ↑a * ↑n) * cexp ↑(-π * ↑n ^ 2 * t)) =
    2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * ↑a + ↑π * I * ↑n ^ 2 * (I * ↑t)) / (-2 * ↑π)

Tactic:
← Complex.exp_add,

Goal state after:
a t : ℝ
ht : 0 < t
h : -2 * ↑π ≠ 0
n : ℤ
⊢ -I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n + ↑(-π * ↑n ^ 2 * t)) =
    2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * ↑a + ↑π * I * ↑n ^ 2 * (I * ↑t)) / (-2 * ↑π)
Module: Mathlib.NumberTheory.LSeries.RiemannZeta

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : s ≠ 1
⊢ hurwitzZetaEven 0 (1 - s) = 2 * (2 * ↑π) ^ (-s) * Gamma s * cos (↑π * s / 2) * hurwitzZetaEven 0 s

Tactic:
hurwitzZetaEven_one_sub 0 hs (Or.inr hs'),

Goal state after:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : s ≠ 1
⊢ 2 * (2 * ↑π) ^ (-s) * Gamma s * cos (↑π * s / 2) * cosZeta 0 s =
    2 * (2 * ↑π) ^ (-s) * Gamma s * cos (↑π * s / 2) * hurwitzZetaEven 0 s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case refine_1.inl
a : UnitAddCircle
s : ℂ
hs' : s ≠ 1
h : s ≠ 0
⊢ s / 2 ≠ 0 ∨ (hurwitzEvenFEPair a).f₀ = 0

pp: case refine_1.inr
a : UnitAddCircle
s : ℂ
hs' : s ≠ 1
h : a ≠ 0
⊢ s / 2 ≠ 0 ∨ (hurwitzEvenFEPair a).f₀ = 0

Tactic:
<;>

Goal state after:
case refine_1.inl
a : UnitAddCircle
s : ℂ
hs' : s ≠ 1
h : s ≠ 0
⊢ s / 2 ≠ 0 ∨ (hurwitzEvenFEPair a).f₀ = 0

case refine_1.inr
a : UnitAddCircle
s : ℂ
hs' : s ≠ 1
h : a ≠ 0
⊢ s / 2 ≠ 0 ∨ (hurwitzEvenFEPair a).f₀ = 0
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case hf
a b : UnitAddCircle
this :
  ∀ (s : ℂ),
    completedHurwitzZetaEven a s - completedHurwitzZetaEven b s =
      completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s -
        ((if a = 0 then 1 else 0) - if b = 0 then 1 else 0) / s
⊢ DifferentiableAt ℂ (completedHurwitzZetaEven₀ a) 1

pp: case hg
a b : UnitAddCircle
this :
  ∀ (s : ℂ),
    completedHurwitzZetaEven a s - completedHurwitzZetaEven b s =
      completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s -
        ((if a = 0 then 1 else 0) - if b = 0 then 1 else 0) / s
⊢ DifferentiableAt ℂ (completedHurwitzZetaEven₀ b) 1

Tactic:
<;>

Goal state after:
case hf
a b : UnitAddCircle
this :
  ∀ (s : ℂ),
    completedHurwitzZetaEven a s - completedHurwitzZetaEven b s =
      completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s -
        ((if a = 0 then 1 else 0) - if b = 0 then 1 else 0) / s
⊢ DifferentiableAt ℂ (completedHurwitzZetaEven₀ a) 1

case hg
a b : UnitAddCircle
this :
  ∀ (s : ℂ),
    completedHurwitzZetaEven a s - completedHurwitzZetaEven b s =
      completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s -
        ((if a = 0 then 1 else 0) - if b = 0 then 1 else 0) / s
⊢ DifferentiableAt ℂ (completedHurwitzZetaEven₀ b) 1
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case pos
a : UnitAddCircle
h1 : Tendsto (fun s ↦ s * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] 0) (𝓝 (-if a = 0 then 1 else 0))
h✝ : a = 0
⊢ -1 = -1

pp: case neg
a : UnitAddCircle
h1 : Tendsto (fun s ↦ s * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] 0) (𝓝 (-if a = 0 then 1 else 0))
h✝ : ¬a = 0
⊢ -0 = 0

Tactic:
<;>

Goal state after:
case pos
a : UnitAddCircle
h1 : Tendsto (fun s ↦ s * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] 0) (𝓝 (-if a = 0 then 1 else 0))
h✝ : a = 0
⊢ -1 = -1

case neg
a : UnitAddCircle
h1 : Tendsto (fun s ↦ s * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] 0) (𝓝 (-if a = 0 then 1 else 0))
h✝ : ¬a = 0
⊢ -0 = 0
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case pos
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ cexp (2 * ↑π * I * ↑a * ↑n) / 2
t : ℝ
ht : 0 < t
n : ℤ
h✝ : n = 0
⊢ 0 = 0 / 2

pp: case neg
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ cexp (2 * ↑π * I * ↑a * ↑n) / 2
t : ℝ
ht : 0 < t
n : ℤ
h✝ : ¬n = 0
⊢ c n * ↑(rexp (-π * ↑n ^ 2 * t)) = cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t)) / 2

Tactic:
<;>

Goal state after:
case pos
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ cexp (2 * ↑π * I * ↑a * ↑n) / 2
t : ℝ
ht : 0 < t
n : ℤ
h✝ : n = 0
⊢ 0 = 0 / 2

case neg
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ cexp (2 * ↑π * I * ↑a * ↑n) / 2
t : ℝ
ht : 0 < t
n : ℤ
h✝ : ¬n = 0
⊢ c n * ↑(rexp (-π * ↑n ^ 2 * t)) = cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t)) / 2
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: case inl
s : ℂ
hs : 1 < s.re
n : ℕ
hn : n = 0
⊢ term (fun n ↦ if n = 0 then 0 else 1) s n = 1 / ↑n ^ s

pp: case inr
s : ℂ
hs : 1 < s.re
n : ℕ
hn : n ≠ 0
⊢ term (fun n ↦ if n = 0 then 0 else 1) s n = 1 / ↑n ^ s

Tactic:
<;>

Goal state after:
case inl
s : ℂ
hs : 1 < s.re
n : ℕ
hn : n = 0
⊢ term (fun n ↦ if n = 0 then 0 else 1) s n = 1 / ↑n ^ s

case inr
s : ℂ
hs : 1 < s.re
n : ℕ
hn : n ≠ 0
⊢ term (fun n ↦ if n = 0 then 0 else 1) s n = 1 / ↑n ^ s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case e_a.e_a.e_a
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) +
        -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t)))
    ↑(sinKernel (↑a) t)
n : ℕ
⊢ -(2 * ↑π * ↑a * ↑n * I) = -(2 * ↑π * I * ↑a * ↑n)

pp: case e_a.e_a.e_a
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) +
        -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t)))
    ↑(sinKernel (↑a) t)
n : ℕ
⊢ 2 * ↑π * ↑a * ↑n * I = 2 * ↑π * I * ↑a * ↑n

Tactic:
<;>

Goal state after:
case e_a.e_a.e_a
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) +
        -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t)))
    ↑(sinKernel (↑a) t)
n : ℕ
⊢ -(2 * ↑π * ↑a * ↑n * I) = -(2 * ↑π * I * ↑a * ↑n)

case e_a.e_a.e_a
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) +
        -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t)))
    ↑(sinKernel (↑a) t)
n : ℕ
⊢ 2 * ↑π * ↑a * ↑n * I = 2 * ↑π * I * ↑a * ↑n
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
m : ℕ
hm : FermatLastTheoremWith R m
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
k : ℕ
⊢ a ^ k ≠ 0

pp: case refine_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
m : ℕ
hm : FermatLastTheoremWith R m
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
k : ℕ
⊢ b ^ k ≠ 0

pp: case refine_3
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
m : ℕ
hm : FermatLastTheoremWith R m
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
k : ℕ
⊢ c ^ k ≠ 0

Tactic:
<;>

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
m : ℕ
hm : FermatLastTheoremWith R m
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
k : ℕ
⊢ a ^ k ≠ 0

case refine_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
m : ℕ
hm : FermatLastTheoremWith R m
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
k : ℕ
⊢ b ^ k ≠ 0

case refine_3
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
m : ℕ
hm : FermatLastTheoremWith R m
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
k : ℕ
⊢ c ^ k ≠ 0
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case inr.inl
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
⊢ False

pp: case inr.inr
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
⊢ False

Tactic:
<;>

Goal state after:
case inr.inl
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
⊢ False

case inr.inr
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
⊢ False
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case inr.inl.inl
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : b < 0
⊢ False

pp: case inr.inl.inr
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : 0 < b
⊢ False

pp: case inr.inr.inl
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : b < 0
⊢ False

pp: case inr.inr.inr
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : 0 < b
⊢ False

Tactic:
<;>

Goal state after:
case inr.inl.inl
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : b < 0
⊢ False

case inr.inl.inr
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : 0 < b
⊢ False

case inr.inr.inl
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : b < 0
⊢ False

case inr.inr.inr
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : 0 < b
⊢ False
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
n : ℕ
this : -2 * (↑n + 1) ≠ 0
⊢ completedHurwitzZetaEven a (-2 * (↑n + 1)) / 0 = 0

Tactic:
div_zero

Goal state after:
a : UnitAddCircle
n : ℕ
this : -2 * (↑n + 1) ≠ 0
⊢ 0 = 0
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case a
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
h : FermatLastTheoremWith R n
a b c : R
x✝³ : a ≠ 0
x✝² : b ≠ 0
x✝¹ : c ≠ 0
x✝ : a ^ n + b ^ n = c ^ n
⊢ a ≠ 0

pp: case a
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
h : FermatLastTheoremWith R n
a b c : R
x✝³ : a ≠ 0
x✝² : b ≠ 0
x✝¹ : c ≠ 0
x✝ : a ^ n + b ^ n = c ^ n
⊢ b ≠ 0

pp: case a
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
h : FermatLastTheoremWith R n
a b c : R
x✝³ : a ≠ 0
x✝² : b ≠ 0
x✝¹ : c ≠ 0
x✝ : a ^ n + b ^ n = c ^ n
⊢ c ≠ 0

pp: case a
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
h : FermatLastTheoremWith R n
a b c : R
x✝³ : a ≠ 0
x✝² : b ≠ 0
x✝¹ : c ≠ 0
x✝ : a ^ n + b ^ n = c ^ n
⊢ a ^ n + b ^ n = c ^ n

Tactic:
<;>

Goal state after:
case a
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
h : FermatLastTheoremWith R n
a b c : R
x✝³ : a ≠ 0
x✝² : b ≠ 0
x✝¹ : c ≠ 0
x✝ : a ^ n + b ^ n = c ^ n
⊢ a ≠ 0

case a
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
h : FermatLastTheoremWith R n
a b c : R
x✝³ : a ≠ 0
x✝² : b ≠ 0
x✝¹ : c ≠ 0
x✝ : a ^ n + b ^ n = c ^ n
⊢ b ≠ 0

case a
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
h : FermatLastTheoremWith R n
a b c : R
x✝³ : a ≠ 0
x✝² : b ≠ 0
x✝¹ : c ≠ 0
x✝ : a ^ n + b ^ n = c ^ n
⊢ c ≠ 0

case a
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
h : FermatLastTheoremWith R n
a b c : R
x✝³ : a ≠ 0
x✝² : b ≠ 0
x✝¹ : c ≠ 0
x✝ : a ^ n + b ^ n = c ^ n
⊢ a ^ n + b ^ n = c ^ n
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n ↦ (1 / ↑|↑n + a| ^ s + 1 / ↑|↑n + 1 - a| ^ s) / 2) (hurwitzZetaEven (↑a) s)

Tactic:
refine (hasSum_int_hurwitzZetaEven a hs).nat_add_neg_add_one.congr_fun fun n ↦ ?_

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ (1 / ↑|↑n + a| ^ s + 1 / ↑|↑n + 1 - a| ^ s) / 2 = 1 / ↑|↑↑n + a| ^ s / 2 + 1 / ↑|↑(-(↑n + 1)) + a| ^ s / 2
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case e_a.e_a
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ 1 / (↑n + ↑a) ^ s = 1 / ↑|↑n + a| ^ s

pp: case e_a.e_a
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ 1 / (↑n + 1 - ↑a) ^ s = 1 / ↑|↑n + 1 - a| ^ s

Tactic:
<;>

Goal state after:
case e_a.e_a
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ 1 / (↑n + ↑a) ^ s = 1 / ↑|↑n + a| ^ s

case e_a.e_a
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ 1 / (↑n + 1 - ↑a) ^ s = 1 / ↑|↑n + 1 - a| ^ s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case e_a.e_a
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ 1 / (↑n + ↑a) ^ s = 1 / ↑(↑n + a) ^ s

pp: case e_a.e_a
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ 1 / (↑n + 1 - ↑a) ^ s = 1 / ↑(↑n + 1 - a) ^ s

Tactic:
<;>

Goal state after:
case e_a.e_a
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ 1 / (↑n + ↑a) ^ s = 1 / ↑(↑n + a) ^ s

case e_a.e_a
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ 1 / (↑n + 1 - ↑a) ^ s = 1 / ↑(↑n + 1 - a) ^ s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
n : ℕ
this : -2 * (↑n + 1) ≠ 0
⊢ completedCosZeta a (-2 * (↑n + 1)) / 0 = 0

Tactic:
div_zero

Goal state after:
a : UnitAddCircle
n : ℕ
this : -2 * (↑n + 1) ≠ 0
⊢ 0 = 0
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case hf₁
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := ⋯
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n ↦ c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(sinKernel (↑a) t) / 2)
⊢ Summable fun n ↦ 1 / |↑↑n| ^ s.re

pp: case hf₂
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := ⋯
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n ↦ c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(sinKernel (↑a) t) / 2)
⊢ Summable fun n ↦ 1 / |↑(-↑n)| ^ s.re

Tactic:
<;>

Goal state after:
case hf₁
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := ⋯
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n ↦ c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(sinKernel (↑a) t) / 2)
⊢ Summable fun n ↦ 1 / |↑↑n| ^ s.re

case hf₂
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := ⋯
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n ↦ c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(sinKernel (↑a) t) / 2)
⊢ Summable fun n ↦ 1 / |↑(-↑n)| ^ s.re
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case neg.inl
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hb : b ^ n = 1 ∨ b ^ n = -1
hc : c ^ n = 1 ∨ c ^ n = -1
hn : ¬n = 0
ha : a ^ n = 1
⊢ a ^ n + b ^ n ≠ c ^ n

pp: case neg.inr
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hb : b ^ n = 1 ∨ b ^ n = -1
hc : c ^ n = 1 ∨ c ^ n = -1
hn : ¬n = 0
ha : a ^ n = -1
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
<;>

Goal state after:
case neg.inl
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hb : b ^ n = 1 ∨ b ^ n = -1
hc : c ^ n = 1 ∨ c ^ n = -1
hn : ¬n = 0
ha : a ^ n = 1
⊢ a ^ n + b ^ n ≠ c ^ n

case neg.inr
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hb : b ^ n = 1 ∨ b ^ n = -1
hc : c ^ n = 1 ∨ c ^ n = -1
hn : ¬n = 0
ha : a ^ n = -1
⊢ a ^ n + b ^ n ≠ c ^ n
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case neg.inl.inl
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hc : c ^ n = 1 ∨ c ^ n = -1
hn : ¬n = 0
ha : a ^ n = 1
hb : b ^ n = 1
⊢ a ^ n + b ^ n ≠ c ^ n

pp: case neg.inl.inr
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hc : c ^ n = 1 ∨ c ^ n = -1
hn : ¬n = 0
ha : a ^ n = 1
hb : b ^ n = -1
⊢ a ^ n + b ^ n ≠ c ^ n

pp: case neg.inr.inl
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hc : c ^ n = 1 ∨ c ^ n = -1
hn : ¬n = 0
ha : a ^ n = -1
hb : b ^ n = 1
⊢ a ^ n + b ^ n ≠ c ^ n

pp: case neg.inr.inr
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hc : c ^ n = 1 ∨ c ^ n = -1
hn : ¬n = 0
ha : a ^ n = -1
hb : b ^ n = -1
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
<;>

Goal state after:
case neg.inl.inl
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hc : c ^ n = 1 ∨ c ^ n = -1
hn : ¬n = 0
ha : a ^ n = 1
hb : b ^ n = 1
⊢ a ^ n + b ^ n ≠ c ^ n

case neg.inl.inr
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hc : c ^ n = 1 ∨ c ^ n = -1
hn : ¬n = 0
ha : a ^ n = 1
hb : b ^ n = -1
⊢ a ^ n + b ^ n ≠ c ^ n

case neg.inr.inl
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hc : c ^ n = 1 ∨ c ^ n = -1
hn : ¬n = 0
ha : a ^ n = -1
hb : b ^ n = 1
⊢ a ^ n + b ^ n ≠ c ^ n

case neg.inr.inr
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hc : c ^ n = 1 ∨ c ^ n = -1
hn : ¬n = 0
ha : a ^ n = -1
hb : b ^ n = -1
⊢ a ^ n + b ^ n ≠ c ^ n