mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case e'_3
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m ↦ ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
H : ∀ m ∈ D, f m ≠ ↑n
hD : #(Ico 0 ↑n) < #D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ m ∈ D, f m ∈ Ico 0 ↑n
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_lt_y : x < y
hxy : f x = f y
⊢ (ξ * ↑(y - x) - ↑(⌊ξ * ↑y⌋ - ⌊ξ * ↑x⌋)) * (↑n + 1) = fract (ξ * ↑y) * (↑n + 1) - fract (ξ * ↑x) * (↑n + 1)

Tactic:
push_cast

Goal state after:
case e'_3
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m ↦ ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
H : ∀ m ∈ D, f m ≠ ↑n
hD : #(Ico 0 ↑n) < #D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ m ∈ D, f m ∈ Ico 0 ↑n
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_lt_y : x < y
hxy : f x = f y
⊢ (ξ * (↑y - ↑x) - (↑⌊ξ * ↑y⌋ - ↑⌊ξ * ↑x⌋)) * (↑n + 1) = fract (ξ * ↑y) * (↑n + 1) - fract (ξ * ↑x) * (↑n + 1)
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
a b : ℤ
x✝ : b ≠ 0
h : ξ = ↑a / ↑b
q : ℚ
⊢ 1 / ↑q.den ^ 2 = ↑(1 / ↑q.den ^ 2)

Tactic:
push_cast

Goal state after:
ξ : ℝ
a b : ℤ
x✝ : b ≠ 0
h : ξ = ↑a / ↑b
q : ℚ
⊢ 1 / ↑q.den ^ 2 = 1 / ↑q.den ^ 2
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: ⊢ factoredNumbers ∅ = {1}

Tactic:
ext m

Goal state after:
m : ℕ
⊢ m ∈ factoredNumbers ∅ ↔ m ∈ {1}
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
N : ℕ
hN : ¬Prime N
⊢ factoredNumbers (insert N s) = factoredNumbers s

Tactic:
ext m

Goal state after:
s : Finset ℕ
N : ℕ
hN : ¬Prime N
m : ℕ
⊢ m ∈ factoredNumbers (insert N s) ↔ m ∈ factoredNumbers s
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
⊢ p ^ e * n ∈ factoredNumbers (insert p s)

Tactic:
have hp' := pow_ne_zero e hp.ne_zero
  refine ⟨mul_ne_zero hp' hn.1, fun q hq ↦ ?_⟩
  rcases (mem_primeFactorsList_mul hp' hn.1).mp hq with H | H
  · rw [mem_primeFactorsList hp'] at H
    rw [(prime_dvd_prime_iff_eq H.1 hp).mp <| H.1.dvd_of_dvd_pow H.2]
    exact Finset.mem_insert_self p s
  · exact Finset.mem_insert_of_mem <| hn.2 _ H

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: case left
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
hpm : ¬p ∣ m
⊢ (p ^ e * m).factorization p = e

Tactic:
factorization_mul (pow_ne_zero e hp.ne_zero) hm₀,

Goal state after:
case left
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
hpm : ¬p ∣ m
⊢ ((p ^ e).factorization + m.factorization) p = e
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |↑⌊ξ⌋ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
hf : ξ = ↑⌊ξ⌋
h' : ↑⌊ξ⌋ - ↑u / ↑v = (↑⌊ξ⌋ * ↑v - ↑u) / ↑v
⊢ ⌊ξ⌋ * v ≠ u

Tactic:
rintro rfl

Goal state after:
ξ : ℝ
v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
hf : ξ = ↑⌊ξ⌋
hcop : IsCoprime (⌊ξ⌋ * v) v
left✝ : v = 1 → -(1 / 2) < ξ - ↑(⌊ξ⌋ * v)
h : |↑⌊ξ⌋ - ↑(⌊ξ⌋ * v) / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h' : ↑⌊ξ⌋ - ↑(⌊ξ⌋ * v) / ↑v = (↑⌊ξ⌋ * ↑v - ↑(⌊ξ⌋ * v)) / ↑v
⊢ False
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: n : ℕ
⊢ n.smoothNumbers = factoredNumbers (Finset.range n)

Tactic:
by
  simp only [smoothNumbers, ne_eq, mem_primeFactorsList', and_imp, factoredNumbers,
    Finset.mem_range]

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: N k : ℕ
⊢ N.smoothNumbersUpTo k ⊆
    Finset.image
      (fun x ↦
        match x with
        | (s, m) => m ^ 2 * s.prod id)
      (k.primesBelow.powerset ×ˢ (Finset.range (N.sqrt + 1)).erase 0)

Tactic:
by
  intro n hn
  obtain ⟨hn₁, hn₂⟩ := mem_smoothNumbersUpTo.mp hn
  obtain ⟨s, hs, m, hm⟩ := eq_prod_primes_mul_sq_of_mem_smoothNumbers hn₂
  simp only [id_eq, Finset.mem_range, Finset.mem_image,
    Finset.mem_product, Finset.mem_powerset, Finset.mem_erase, Prod.exists]
  refine ⟨s, m, ⟨Finset.mem_powerset.mp hs, ?_, ?_⟩, hm.symm⟩
  · have := hm ▸ ne_zero_of_mem_smoothNumbers hn₂
    simp only [ne_eq, _root_.mul_eq_zero, sq_eq_zero_iff, not_or] at this
    exact this.1
  · rw [Nat.lt_succ_iff, le_sqrt']
    refine LE.le.trans ?_ (hm ▸ hn₁)
    nth_rw 1 [← mul_one (m ^ 2)]
    gcongr
    exact Finset.one_le_prod' fun p hp ↦
      (prime_of_mem_primesBelow <| Finset.mem_powerset.mp hs hp).one_le

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: N k : ℕ
⊢ N.roughNumbersUpTo k =
    ((N + 1).primesBelow \ k.primesBelow).biUnion fun p ↦ {m ∈ Finset.range (N + 1) | m ≠ 0 ∧ p ∣ m}

Tactic:
ext m

Goal state after:
N k m : ℕ
⊢ m ∈ N.roughNumbersUpTo k ↔
    m ∈ ((N + 1).primesBelow \ k.primesBelow).biUnion fun p ↦ {m ∈ Finset.range (N + 1) | m ≠ 0 ∧ p ∣ m}
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case mp
m n k : ℕ
⊢ n ^ k = m →
    k = 0 ∧ m = 1 ∨
      0 < k ∧
        (n = 0 ∧ m = 0 ∨
          0 < n ∧
            ∃ w a t z,
              ∃ (a1 : 1 < a),
                xn a1 k ≡ yn a1 k * (a - n) + m [MOD t] ∧
                  2 * a * n = t + (n * n + 1) ∧
                    m < t ∧ n ≤ w ∧ k ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1)

Tactic:
rintro rfl

Goal state after:
case mp
n k : ℕ
⊢ k = 0 ∧ n ^ k = 1 ∨
    0 < k ∧
      (n = 0 ∧ n ^ k = 0 ∨
        0 < n ∧
          ∃ w a t z,
            ∃ (a1 : 1 < a),
              xn a1 k ≡ yn a1 k * (a - n) + n ^ k [MOD t] ∧
                2 * a * n = t + (n * n + 1) ∧
                  n ^ k < t ∧ n ≤ w ∧ k ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1)
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
⊢ j ≠ 0

Tactic:
rintro rfl

Goal state after:
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
yj : w * z = yn hw1 0
a1 : 1 < xn hw1 0
tm : xn a1 k ≡ yn a1 k * (xn hw1 0 - n) + m [MOD t]
ta : 2 * xn hw1 0 * n = t + (n * n + 1)
zp : xn hw1 0 * xn hw1 0 - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
⊢ False
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: n : ℤ
z τ : ℂ
⊢ 2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ = ↑(π * (2 * ↑n)) * z * I + ↑(π * ↑n ^ 2) * τ * I

Tactic:
push_cast

Goal state after:
n : ℤ
z τ : ℂ
⊢ 2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ = ↑π * (2 * ↑n) * z * I + ↑π * ↑n ^ 2 * τ * I
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
⊢ (↑n + a) ^ k * rexp (-π * (↑n + a) ^ 2 * t) ≤ (↑n + a) ^ k * rexp (-π * (↑n + a ^ 2) * t)

Tactic:
simp only [neg_mul, add_sq]

Goal state after:
k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
⊢ (↑n + a) ^ k * rexp (-(π * (↑n ^ 2 + 2 * ↑n * a + a ^ 2) * t)) ≤ (↑n + a) ^ k * rexp (-(π * (↑n + a ^ 2) * t))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a : ℝ
ha : a ≤ 1
t : ℝ
n : ℕ
⊢ ↑(Int.negSucc n) + a = -(↑n + (1 - a))

Tactic:
push_cast

Goal state after:
k : ℕ
a : ℝ
ha : a ≤ 1
t : ℝ
n : ℕ
⊢ -(↑n + 1) + a = -(↑n + (1 - a))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a t : ℝ
ht : 0 < t
m : ℕ
⊢ -↑(m + 1) + a = -(↑m + (1 - a))

Tactic:
push_cast

Goal state after:
k : ℕ
a t : ℝ
ht : 0 < t
m : ℕ
⊢ -(↑m + 1) + a = -(↑m + (1 - a))
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
⊢ (∫ (x : ℝ) in Ioc 0 1, ↑x ^ (s - 1)) • P.f₀ - P.ε • ∫ (a : ℝ) in Ioc 0 1, ↑a ^ (s - ↑P.k - 1) • P.g₀ =
    (∫ (x : ℝ) in Ioc 0 1, ↑x ^ (s - 1)) • P.f₀ - P.ε • (∫ (x : ℝ) in Ioc 0 1, ↑x ^ (s - ↑P.k - 1)) • P.g₀

pp: case hf
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
⊢ Integrable (fun x ↦ ↑x ^ (s - 1) • P.f₀) (volume.restrict (Ioc 0 1))

pp: case hg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
⊢ Integrable (fun x ↦ P.ε • ↑x ^ (s - ↑P.k - 1) • P.g₀) (volume.restrict (Ioc 0 1))

Tactic:
integral_smul_const

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
⊢ (∫ (x : ℝ) in Ioc 0 1, ↑x ^ (s - 1)) • P.f₀ - P.ε • (∫ (x : ℝ) in Ioc 0 1, ↑x ^ (s - ↑P.k - 1)) • P.g₀ =
    (∫ (x : ℝ) in Ioc 0 1, ↑x ^ (s - 1)) • P.f₀ - P.ε • (∫ (x : ℝ) in Ioc 0 1, ↑x ^ (s - ↑P.k - 1)) • P.g₀

case hf
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
⊢ Integrable (fun x ↦ ↑x ^ (s - 1) • P.f₀) (volume.restrict (Ioc 0 1))

case hg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
⊢ Integrable (fun x ↦ P.ε • ↑x ^ (s - ↑P.k - 1) • P.g₀) (volume.restrict (Ioc 0 1))
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
⊢ HasSum (fun i ↦ ↑π ^ (-s) * Complex.Gamma s * a i / ↑(p i) ^ s) (mellin F s)

Tactic:
by
  have hs' : s ≠ 0 := fun h ↦ lt_irrefl _ (zero_re ▸ h ▸ hs)
  let a' i := if p i = 0 then 0 else a i
  have hp' i : a' i = 0 ∨ 0 < p i := by
    simp only [a']
    split_ifs with h <;> try tauto
    exact Or.inr (lt_of_le_of_ne (hp i) (Ne.symm h))
  have (i t : _) : (if p i = 0 then 0 else a i * rexp (-π * p i * t)) =
      a' i * rexp (-π * p i * t) := by
    simp [a']
  simp_rw [this] at hF
  convert! hasSum_mellin_pi_mul hp' hs hF ?_ using 2 with i
  · rcases eq_or_ne (p i) 0 with h | h <;>
    simp [a', h, ofReal_zero, zero_cpow hs', div_zero]
  · refine h_sum.of_norm_bounded (fun i ↦ ?_)
    simp only [a']
    split_ifs
    · simp only [norm_zero, zero_div]
      positivity
    · have := hp i
      rw [norm_of_nonneg (by positivity)]

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

Goal state before:
pp: x : ℝ
hx : 0 < x
a : ℝ
⊢ I * ↑(1 / x) = -1 / (I * ↑x)

Tactic:
push_cast

Goal state after:
x : ℝ
hx : 0 < x
a : ℝ
⊢ I * (1 / ↑x) = -1 / (I * ↑x)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
n : ℤ
⊢ ↑π * I * ↑n ^ 2 * 2 = ↑(n ^ 2) * (2 * ↑π * I)

Tactic:
push_cast

Goal state after:
z τ : ℂ
n : ℤ
⊢ ↑π * I * ↑n ^ 2 * 2 = ↑n ^ 2 * (2 * ↑π * I)
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ ↑P.k - 0 ≠ 0

Tactic:
simpa using P.hk.ne'

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case e_f
z τ : ℂ
n : ℤ
⊢ 2 * ↑π * I * ↑(-n) * cexp (2 * ↑π * I * ↑(-n) * -z + ↑π * I * ↑(-n) ^ 2 * τ) =
    -(2 * ↑π * I * ↑n) * cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)

Tactic:
push_cast

Goal state after:
case e_f
z τ : ℂ
n : ℤ
⊢ 2 * ↑π * I * -↑n * cexp (2 * ↑π * I * -↑n * -z + ↑π * I * (-↑n) ^ 2 * τ) =
    -(2 * ↑π * I * ↑n) * cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: 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 * Real.cos (2 * π * a * (↑n + 1)) * rexp (-π * (↑n + 1) ^ 2 * t)) =
    (cexp (2 * ↑π * I * ↑a * ↑(n + 1)) + cexp (-(2 * ↑π * I * ↑a * ↑(n + 1)))) * ↑(rexp (-π * ↑(n + 1) ^ 2 * t))

Tactic:
push_cast

Goal state after:
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 * Complex.cos (2 * ↑π * ↑a * (↑n + 1)) * cexp (-↑π * (↑n + 1) ^ 2 * ↑t) =
    (cexp (2 * ↑π * I * ↑a * (↑n + 1)) + cexp (-(2 * ↑π * I * ↑a * (↑n + 1)))) * cexp (-↑π * (↑n + 1) ^ 2 * ↑t)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

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

Tactic:
exact div_nonneg (neg_nonneg.mpr hτ) (normSq_nonneg τ)

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

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

Tactic:
exact div_nonneg (neg_nonneg.mpr hτ) (normSq_nonneg τ)

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

Goal state before:
pp: case e_a
a : UnitAddCircle
s : ℂ
⊢ (1 / (↑(1 / 2) - s / 2)) • 1 / 2 = 1 / (1 - s)

Tactic:
push_cast

Goal state after:
case e_a
a : UnitAddCircle
s : ℂ
⊢ (1 / (1 / 2 - s / 2)) • 1 / 2 = 1 / (1 - s)
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
⊢ (cexp (-↑π * I * z ^ 2 * τ⁻¹) * (-↑π * I * deriv (fun z ↦ z ^ 2) z * τ⁻¹) * jacobiTheta₂ (z * τ⁻¹) (-1 * τ⁻¹) +
        cexp (-↑π * I * z ^ 2 * τ⁻¹) * (1 * τ⁻¹ * jacobiTheta₂' (z * τ⁻¹) (-1 * τ⁻¹))) *
      (1 / (-I * τ) ^ (1 / 2)) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 * τ⁻¹) * τ⁻¹ *
      (jacobiTheta₂' (z * τ⁻¹) (-1 * τ⁻¹) - 2 * ↑π * I * z * jacobiTheta₂ (z * τ⁻¹) (-1 * τ⁻¹))

Tactic:
deriv_pow_field

Goal state after:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun w ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ (cexp (-↑π * I * z ^ 2 * τ⁻¹) * (-↑π * I * (↑2 * z ^ (2 - 1)) * τ⁻¹) * jacobiTheta₂ (z * τ⁻¹) (-1 * τ⁻¹) +
        cexp (-↑π * I * z ^ 2 * τ⁻¹) * (1 * τ⁻¹ * jacobiTheta₂' (z * τ⁻¹) (-1 * τ⁻¹))) *
      (1 / (-I * τ) ^ (1 / 2)) =
    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 x : ℝ
hx : 0 < x
h1 : HasSum (fun n ↦ jacobiTheta₂_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
h2 : HasSum (fun n ↦ jacobiTheta₂'_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x))
n : ℤ
⊢ ↑((↑n + a) * rexp (-π * (↑n + a) ^ 2 * x)) =
    (↑n + ↑a) * cexp (-↑π * ↑a ^ 2 * ↑x + (2 * ↑π * I * ↑n * (↑a * I * ↑x) + ↑π * I * ↑n ^ 2 * (I * ↑x)))

Tactic:
push_cast

Goal state after:
a x : ℝ
hx : 0 < x
h1 : HasSum (fun n ↦ jacobiTheta₂_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
h2 : HasSum (fun n ↦ jacobiTheta₂'_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x))
n : ℤ
⊢ (↑n + ↑a) * cexp (-↑π * (↑n + ↑a) ^ 2 * ↑x) =
    (↑n + ↑a) * cexp (-↑π * ↑a ^ 2 * ↑x + (2 * ↑π * I * ↑n * (↑a * I * ↑x) + ↑π * I * ↑n ^ 2 * (I * ↑x)))
Module: Mathlib.NumberTheory.LSeries.HurwitzZeta

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
n : ℕ
⊢ -↑n = 1 - ↑(n + 1)

Tactic:
push_cast

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
n : ℕ
⊢ -↑n = 1 - (↑n + 1)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case refine_2
a : UnitAddCircle
s : ℂ
hs : s ≠ 0 ∨ a ≠ 0
hs' : s ≠ 1
⊢ s / 2 ≠ ↑(hurwitzEvenFEPair a).k

Tactic:
change s / 2 ≠ ↑(1 / 2 : ℝ)
    rw [ofReal_div, ofReal_one, ofReal_ofNat]
    exact hs' ∘ (div_left_inj' two_ne_zero).mp

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ cexp (2 * ↑π * I * ↑a * ↑n) / 2
hF :
  ∀ (t : ℝ),
    0 < t → HasSum (fun n ↦ if ↑n = 0 then 0 else c n * ↑(rexp (-π * ↑n ^ 2 * t))) ((↑(cosKernel (↑a) t) - 1) / 2)
i : ℤ
⊢ 2 * ↑π * I * ↑a * ↑i = ↑(2 * π * a * ↑i) * I

Tactic:
push_cast

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ cexp (2 * ↑π * I * ↑a * ↑n) / 2
hF :
  ∀ (t : ℝ),
    0 < t → HasSum (fun n ↦ if ↑n = 0 then 0 else c n * ↑(rexp (-π * ↑n ^ 2 * t))) ((↑(cosKernel (↑a) t) - 1) / 2)
i : ℤ
⊢ 2 * ↑π * I * ↑a * ↑i = 2 * ↑π * ↑a * ↑i * I
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: 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 * ↑n * ((cexp (-↑(2 * π * a * ↑n) * I) - cexp (↑(2 * π * a * ↑n) * I)) * I / 2) * ↑(rexp (-π * ↑n ^ 2 * t)) =
    (-I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n) + -(-I * ↑n) * cexp (-(2 * ↑π * I * ↑a * ↑n))) * ↑(rexp (-π * ↑n ^ 2 * t))

Tactic:
push_cast

Goal state after:
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 * ↑n * ((cexp (-(2 * ↑π * ↑a * ↑n) * I) - cexp (2 * ↑π * ↑a * ↑n * I)) * I / 2) * cexp (-↑π * ↑n ^ 2 * ↑t) =
    (-I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n) + -(-I * ↑n) * cexp (-(2 * ↑π * I * ↑a * ↑n))) * cexp (-↑π * ↑n ^ 2 * ↑t)
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: case neg
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun n ↦ χ ↑n) 1
n : ℕ
h₁ : ↑n = 1
h₂ : ¬n = 0
⊢ 1 / ↑n ≤ ‖χ ↑n‖ / ↑n ^ re 1

pp: case pos
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun n ↦ χ ↑n) 1
n : ℕ
h₁ : ¬↑n = 1
h✝ : n = 0
⊢ 0 ≤ 0

pp: case neg
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun n ↦ χ ↑n) 1
n : ℕ
h₁ : ¬↑n = 1
h✝ : ¬n = 0
⊢ 0 ≤ ‖χ ↑n‖ / ↑n ^ re 1

Tactic:
· simp [h₁, χ.map_one]

Goal state after:
case pos
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun n ↦ χ ↑n) 1
n : ℕ
h₁ : ¬↑n = 1
h✝ : n = 0
⊢ 0 ≤ 0

case neg
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun n ↦ χ ↑n) 1
n : ℕ
h₁ : ¬↑n = 1
h✝ : ¬n = 0
⊢ 0 ≤ ‖χ ↑n‖ / ↑n ^ re 1
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: ⊢ ((fun n ↦ ↑(Λ n)) ⍟ fun n ↦ ↑(ζ n)) = fun n ↦ Complex.log ↑n

Tactic:
by
  ext n
  simpa [apply_ite, LSeries.convolution_def, -vonMangoldt_mul_zeta]
    using congr_arg (ofReal <| · n) vonMangoldt_mul_zeta

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

Goal state before:
pp: case 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 : Even n
⊢ ↑(a.natAbs ^ n + b.natAbs ^ n) = ↑(c.natAbs ^ n)

Tactic:
push_cast

Goal state after:
case 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 : Even n
⊢ |a| ^ n + |b| ^ n = |c| ^ n
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case inr.inl.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
hc : c < 0
⊢ ↑(a.natAbs ^ n + b.natAbs ^ n) = ↑(c.natAbs ^ n)

Tactic:
push_cast

Goal state after:
case inr.inl.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
hc : c < 0
⊢ |a| ^ n + |b| ^ n = |c| ^ n
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case inr.inl.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
hb : 0 < b
hc : c < 0
⊢ ↑(b.natAbs ^ n + c.natAbs ^ n) = ↑(a.natAbs ^ n)

Tactic:
push_cast

Goal state after:
case inr.inl.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
hb : 0 < b
hc : c < 0
⊢ |b| ^ n + |c| ^ n = |a| ^ n
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case inr.inl.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 : a < 0
hb : 0 < b
hc : 0 < c
⊢ ↑(a.natAbs ^ n + c.natAbs ^ n) = ↑(b.natAbs ^ n)

Tactic:
push_cast

Goal state after:
case inr.inl.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 : a < 0
hb : 0 < b
hc : 0 < c
⊢ |a| ^ n + |c| ^ n = |b| ^ n
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case inr.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 : 0 < a
hb : b < 0
hc : c < 0
⊢ ↑(c.natAbs ^ n + a.natAbs ^ n) = ↑(b.natAbs ^ n)

Tactic:
push_cast

Goal state after:
case inr.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 : 0 < a
hb : b < 0
hc : c < 0
⊢ |c| ^ n + |a| ^ n = |b| ^ n
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case inr.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 : 0 < a
hb : b < 0
hc : 0 < c
⊢ ↑(c.natAbs ^ n + b.natAbs ^ n) = ↑(a.natAbs ^ n)

Tactic:
push_cast

Goal state after:
case inr.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 : 0 < a
hb : b < 0
hc : 0 < c
⊢ |c| ^ n + |b| ^ n = |a| ^ n
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ (1 - s + 1) / 2 = ↑(3 / 2) - (s + 1) / 2

Tactic:
push_cast

Goal state after:
a : UnitAddCircle
s : ℂ
⊢ (1 - s + 1) / 2 = 3 / 2 - (s + 1) / 2
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case inr.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
hc : 0 < c
⊢ ↑(a.natAbs ^ n + b.natAbs ^ n) = ↑(c.natAbs ^ n)

Tactic:
push_cast

Goal state after:
case inr.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
hc : 0 < c
⊢ |a| ^ n + |b| ^ n = |c| ^ n
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
tfae_1_to_2 : FermatLastTheoremWith ℕ n → FermatLastTheoremWith ℤ n
h : FermatLastTheoremWith ℤ n
a b c : ℚ
ha : a.num ≠ 0
hb : b.num ≠ 0
hc : c.num ≠ 0
habc : a ^ n + b ^ n = c ^ n
this : (↑a.den * ↑b.den * ↑c.den) ^ n ≠ 0
⊢ ↑((a.num * ↑b.den * ↑c.den) ^ n + (↑a.den * b.num * ↑c.den) ^ n) / (↑a.den * ↑b.den * ↑c.den) ^ n =
    ↑((↑a.den * ↑b.den * c.num) ^ n) / (↑a.den * ↑b.den * ↑c.den) ^ n

Tactic:
push_cast

Goal state after:
n : ℕ
tfae_1_to_2 : FermatLastTheoremWith ℕ n → FermatLastTheoremWith ℤ n
h : FermatLastTheoremWith ℤ n
a b c : ℚ
ha : a.num ≠ 0
hb : b.num ≠ 0
hc : c.num ≠ 0
habc : a ^ n + b ^ n = c ^ n
this : (↑a.den * ↑b.den * ↑c.den) ^ n ≠ 0
⊢ ((↑a.num * ↑b.den * ↑c.den) ^ n + (↑a.den * ↑b.num * ↑c.den) ^ n) / (↑a.den * ↑b.den * ↑c.den) ^ n =
    (↑a.den * ↑b.den * ↑c.num) ^ n / (↑a.den * ↑b.den * ↑c.den) ^ n