mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : EuclideanDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
T : Type u_6
inst✝² : Ring T
inst✝¹ : LinearOrder T
inst✝ : IsStrictOrderedRing T
a : S
y : T
hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y
i : ι
him : (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).Nonempty
y' : ℤ := ⋯
y'_def : y' = (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).max' him
hy' : ∀ (k : ι), abv ((bS.repr a) k) ≤ y'
⊢ ∀ y_1 ∈ Finset.image (fun x ↦ ↑x) (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ), y_1 < y

Tactic:
simp only [Finset.mem_image]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : EuclideanDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
T : Type u_6
inst✝² : Ring T
inst✝¹ : LinearOrder T
inst✝ : IsStrictOrderedRing T
a : S
y : T
hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y
i : ι
him : (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).Nonempty
y' : ℤ := (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).max' him
y'_def : y' = (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).max' him
hy' : ∀ (k : ι), abv ((bS.repr a) k) ≤ y'
⊢ ∀ (y_1 : T), (∃ a_1, (∃ a_2 ∈ Finset.univ, abv ((bS.repr a) a_2) = a_1) ∧ ↑a_1 = y_1) → y_1 < y
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : EuclideanDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝² : Infinite R
inst✝¹ : DecidableEq R
inst✝ : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
q : S
r : R
hr : r ∈ finsetApprox bS adm
hqr : abv ((Algebra.norm R) (r • a' - b' • q)) < abv ((Algebra.norm R) ((algebraMap R S) b'))
⊢ ∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - q * b)) < abv ((Algebra.norm R) b)

Tactic:
refine ⟨q, r, hr, ?_⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : EuclideanDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝² : Infinite R
inst✝¹ : DecidableEq R
inst✝ : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
q : S
r : R
hr : r ∈ finsetApprox bS adm
hqr : abv ((Algebra.norm R) (r • a' - b' • q)) < abv ((Algebra.norm R) ((algebraMap R S) b'))
⊢ abv ((Algebra.norm R) (r • a - q * b)) < abv ((Algebra.norm R) b)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
int_deriv :
  ∀ (f : ℝ → ℝ), ∫ (u : ℝ) in 2..x, deriv (fun x ↦ (log x)⁻¹) u * f u = ∫ (u : ℝ) in 2..x, f u * -(u * log u ^ 2)⁻¹
⊢ (log x)⁻¹ * ∑ k ∈ Icc 0 ⌊x⌋₊, a k - ∫ (u : ℝ) in 2..x, (∑ k ∈ Icc 0 ⌊u⌋₊, a k) * -(u * log u ^ 2)⁻¹ =
    θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)

Tactic:
simp [a, Set.indicator_apply, sum_filter, theta_eq_sum_Icc]

Goal state after:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
int_deriv :
  ∀ (f : ℝ → ℝ), ∫ (u : ℝ) in 2..x, deriv (fun x ↦ (log x)⁻¹) u * f u = ∫ (u : ℝ) in 2..x, f u * -(u * log u ^ 2)⁻¹
⊢ ((log x)⁻¹ * ∑ x ∈ Icc 0 ⌊x⌋₊, if Nat.Prime x then log ↑x else 0) +
      ∫ (x : ℝ) in 2..x, (∑ x ∈ Icc 0 ⌊x⌋₊, if Nat.Prime x then log ↑x else 0) * ((log x ^ 2)⁻¹ * x⁻¹) =
    (∑ a ∈ Icc 0 ⌊x⌋₊, if Nat.Prime a then log ↑a else 0) / log x +
      ∫ (t : ℝ) in 2..x, (∑ a ∈ Icc 0 ⌊t⌋₊, if Nat.Prime a then log ↑a else 0) / (t * log t ^ 2)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
⊢ x.appr n ≤ x.appr (n + 1)

Tactic:
dsimp [appr]

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
⊢ x.appr n ≤
    if hy : x - ↑(x.appr n) = 0 then x.appr n
    else x.appr n + p ^ n * (toZMod (↑(unitCoeff hy) * ↑p ^ (↑(x - ↑(x.appr n)).valuation - ↑n).natAbs)).val
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ x.appr (m + k) - x.appr m
⊢ p ^ m ∣ x.appr (m + k + 1) - x.appr m

Tactic:
dsimp [appr]

Goal state after:
case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ x.appr (m + k) - x.appr m
⊢ p ^ m ∣
    (if hy : x - ↑(x.appr (m + k)) = 0 then x.appr (m + k)
      else
        x.appr (m + k) +
          p ^ (m + k) * (toZMod (↑(unitCoeff hy) * ↑p ^ (↑(x - ↑(x.appr (m + k))).valuation - (↑m + ↑k)).natAbs)).val) -
      x.appr m
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
⊢ yz a1 (m - n) = xz a1 n * yz a1 m + -(xz a1 m * yz a1 n)

Tactic:
← mul_neg,

Goal state after:
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
⊢ yz a1 (m - n) = xz a1 n * yz a1 m + xz a1 m * -yz a1 n
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a k x y : ℕ
a1 : 1 < a
ky✝ : k ≤ y
u v s t b : ℕ
b1 : 1 < b
rem : b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y]
i n j : ℕ
bm1 : b ≡ 1 [MOD 4 * yn a1 i]
ba : b ≡ a [MOD xn a1 n]
vp : 0 < yn a1 n
yv : yn a1 i * yn a1 i ∣ yn a1 n
sx : xn b1 j ≡ xn a1 i [MOD xn a1 n]
tk : yn b1 j ≡ k [MOD 4 * yn a1 i]
x✝ :
  1 < a ∧
    k ≤ yn a1 i ∧
      (xn a1 i = 1 ∧ yn a1 i = 0 ∨
        ∃ u v s t b,
          xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧
                  b ≡ 1 [MOD 4 * yn a1 i] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i])
o :
  xn a1 i = 1 ∧ yn a1 i = 0 ∨
    ∃ u v s t b,
      xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1 ∧
        u * u - (a * a - 1) * v * v = 1 ∧
          s * s - (b * b - 1) * t * t = 1 ∧
            1 < b ∧
              b ≡ 1 [MOD 4 * yn a1 i] ∧
                b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i]
xy : xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1
uv : xn a1 n * xn a1 n - (a * a - 1) * yn a1 n * yn a1 n = 1
st : xn b1 j * xn b1 j - (b * b - 1) * yn b1 j * yn b1 j = 1
i0 : i = 0
ky : k = 0
⊢ xn a1 k = xn a1 i ∧ yn a1 k = yn a1 i

Tactic:
i0,

Goal state after:
a k x y : ℕ
a1 : 1 < a
ky✝ : k ≤ y
u v s t b : ℕ
b1 : 1 < b
rem : b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y]
i n j : ℕ
bm1 : b ≡ 1 [MOD 4 * yn a1 i]
ba : b ≡ a [MOD xn a1 n]
vp : 0 < yn a1 n
yv : yn a1 i * yn a1 i ∣ yn a1 n
sx : xn b1 j ≡ xn a1 i [MOD xn a1 n]
tk : yn b1 j ≡ k [MOD 4 * yn a1 i]
x✝ :
  1 < a ∧
    k ≤ yn a1 i ∧
      (xn a1 i = 1 ∧ yn a1 i = 0 ∨
        ∃ u v s t b,
          xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧
                  b ≡ 1 [MOD 4 * yn a1 i] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i])
o :
  xn a1 i = 1 ∧ yn a1 i = 0 ∨
    ∃ u v s t b,
      xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1 ∧
        u * u - (a * a - 1) * v * v = 1 ∧
          s * s - (b * b - 1) * t * t = 1 ∧
            1 < b ∧
              b ≡ 1 [MOD 4 * yn a1 i] ∧
                b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i]
xy : xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1
uv : xn a1 n * xn a1 n - (a * a - 1) * yn a1 n * yn a1 n = 1
st : xn b1 j * xn b1 j - (b * b - 1) * yn b1 j * yn b1 j = 1
i0 : i = 0
ky : k = 0
⊢ xn a1 k = xn a1 0 ∧ yn a1 k = yn a1 0
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).factorization + m.factorization) p = e

Tactic:
Finsupp.add_apply,

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 p + m.factorization p = e
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : ↑u + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ ↑⌊ξ⌋
⊢ 2⁻¹ < fract ξ

Tactic:
rw [fract, hξ₁, cast_sub, cast_one, lt_sub_iff_add_lt', sub_add]

Goal state after:
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : ↑u + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ ↑⌊ξ⌋
⊢ ↑u - (1 - 2⁻¹) < ξ
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ -(2 * S * ↑|n|) ≤ 2 * ↑n * z.im

Tactic:
← mul_neg,

Goal state after:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ 2 * S * -↑|n| ≤ 2 * ↑n * z.im
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a t : ℝ
ht : 0 < t
this : Summable fun n ↦ ↑n ^ k * rexp (-π * (↑n + a) ^ 2 * t)
⊢ ∀ᶠ (i : ℕ) in atTop, ‖f_nat k a t i‖ ≤ 2 ^ k * (↑i ^ k * rexp (-π * (↑i + a) ^ 2 * t))

Tactic:
simp_rw [← mul_assoc, f_nat, norm_mul, norm_eq_abs, abs_exp,
    mul_le_mul_iff_of_pos_right (exp_pos _), ← mul_pow, abs_pow, two_mul]

Goal state after:
k : ℕ
a t : ℝ
ht : 0 < t
this : Summable fun n ↦ ↑n ^ k * rexp (-π * (↑n + a) ^ 2 * t)
⊢ ∀ᶠ (i : ℕ) in atTop, |↑i + a| ^ k ≤ (↑i + ↑i) ^ k
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ (fun x ↦ (P.ε * ↑(x ^ (-P.k))) • P.g₀) =O[𝓝[>] 0] fun x ↦ x ^ (-P.k)

Tactic:
rw [← isBigO_norm_norm]

Goal state after:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ (fun x ↦ ‖(P.ε * ↑(x ^ (-P.k))) • P.g₀‖) =O[𝓝[>] 0] fun x ↦ ‖x ^ (-P.k)‖
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: case e'_3
t : ℝ
ht : 0 < t
⊢ rexp (-π * (0 * 0) * t) + ∑' (b : ℕ), f_nat 0 0 t (b + 1) - 1 = F_nat 0 1 t

Tactic:
mul_zero,

Goal state after:
case e'_3
t : ℝ
ht : 0 < t
⊢ rexp (-π * 0 * t) + ∑' (b : ℕ), f_nat 0 0 t (b + 1) - 1 = F_nat 0 1 t
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: case e'_3
t : ℝ
ht : 0 < t
⊢ rexp (-π * 0 * t) + ∑' (b : ℕ), f_nat 0 0 t (b + 1) - 1 = F_nat 0 1 t

Tactic:
mul_zero,

Goal state after:
case e'_3
t : ℝ
ht : 0 < t
⊢ rexp (0 * t) + ∑' (b : ℕ), f_nat 0 0 t (b + 1) - 1 = F_nat 0 1 t
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case refine_2.inr
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im = 0
h : Summable fun x ↦ rexp (-π * ↑x ^ 2 * 0 - 2 * π * ↑x * z.im)
⊢ False

Tactic:
mul_zero,

Goal state after:
case refine_2.inr
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im = 0
h : Summable fun x ↦ rexp (0 - 2 * π * ↑x * z.im)
⊢ False
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: case e'_6
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
⊢ rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 =
    rexp (-π * a ^ 2 * t) * (rexp (-π * t) / (1 - rexp (-π * t)) ^ 2)

Tactic:
mul_add,

Goal state after:
case e'_6
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
⊢ rexp ((-π * a ^ 2 + -π * 1) * t) / (1 - rexp (-π * t)) ^ 2 =
    rexp (-π * a ^ 2 * t) * (rexp (-π * t) / (1 - rexp (-π * t)) ^ 2)
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / q i ^ s.re
i : ι
⊢ a i = 0 ∨ 0 < π * q i

Tactic:
rcases hq i with h | h

Goal state after:
case inl
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / q i ^ s.re
i : ι
h : a i = 0
⊢ a i = 0 ∨ 0 < π * q i

case inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / q i ^ s.re
i : ι
h : 0 < q i
⊢ a i = 0 ∨ 0 < π * q i
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

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

Tactic:
rcases hq i with h | h

Goal state after:
case inl
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
h : a i = 0
⊢ a i / ↑(π * q i) ^ s = ↑π ^ (-s) * a i / ↑(q i) ^ s

case inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
h : 0 < q i
⊢ a i / ↑(π * q i) ^ s = ↑π ^ (-s) * a i / ↑(q i) ^ s
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: n : ℤ
z τ : ℂ
⊢ π * ↑|n| ^ 2 * ‖jacobiTheta₂_term n z τ‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖

Tactic:
by
  have : ‖(jacobiTheta₂_term_fderiv n z τ) (0, 1)‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖ := by
    refine (ContinuousLinearMap.le_opNorm _ _).trans ?_
    simp_rw [Prod.norm_def, norm_one, norm_zero, max_eq_right zero_le_one, mul_one, le_refl]
  refine le_trans ?_ this
  simp_rw [jacobiTheta₂_term_fderiv, jacobiTheta₂_term, FunLike.coe_smul, Pi.smul_apply, add_apply,
    FunLike.coe_smul, ContinuousLinearMap.coe_fst', ContinuousLinearMap.coe_snd', Pi.smul_apply,
    smul_zero, zero_add, smul_eq_mul, mul_one, mul_comm _ ‖cexp _‖, norm_mul]
  refine mul_le_mul_of_nonneg_left (le_of_eq ?_) (norm_nonneg _)
  simp_rw [norm_real, norm_of_nonneg pi_pos.le, norm_I, mul_one,
    Int.cast_abs, ← norm_intCast, norm_pow]

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

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

Tactic:
rcases hq i with h | h

Goal state after:
case inl
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
h : a i = 0
⊢ ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re

case inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
h : 0 < q i
⊢ ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: case negSucc
k : ℕ
a : ℝ
ha : a ∈ Icc 0 1
t : ℝ
ht : 0 < t
a✝ : ℕ
⊢ f_int k a t (Int.negSucc a✝) = Int.rec (f_nat k a t) (f_nat k (1 - a) t) (Int.negSucc a✝)

Tactic:
· rw [f_int_negSucc _ ha.2]

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

Goal state before:
pp: a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : (fun t ↦ F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : (fun t ↦ F_nat 0 (1 - a) t) =O[atTop] fun t ↦ rexp (-q * t)
⊢ ∃ p, 0 < p ∧ (fun t ↦ F_int 0 (↑a) t - if a = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-p * t)

Tactic:
refine ⟨_, lt_min hp hq, ?_⟩

Goal state after:
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : (fun t ↦ F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : (fun t ↦ F_nat 0 (1 - a) t) =O[atTop] fun t ↦ rexp (-q * t)
⊢ (fun t ↦ F_int 0 (↑a) t - if a = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-min p q * t)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : F_nat 1 a =O[atTop] fun t ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : F_nat 1 (1 - a) =O[atTop] fun t ↦ rexp (-q * t)
⊢ ∃ p, 0 < p ∧ F_int 1 ↑a =O[atTop] fun t ↦ rexp (-p * t)

Tactic:
refine ⟨_, lt_min hp hq, ?_⟩

Goal state after:
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : F_nat 1 a =O[atTop] fun t ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : F_nat 1 (1 - a) =O[atTop] fun t ↦ rexp (-q * t)
⊢ F_int 1 ↑a =O[atTop] fun t ↦ rexp (-min p q * t)
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case refine_2.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ ↑P.k
⊢ DifferentiableAt ℂ (fun s ↦ (P.ε / (↑P.k - s)) • P.g₀) s

pp: case refine_2.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : P.g₀ = 0
⊢ DifferentiableAt ℂ (fun s ↦ (P.ε / (↑P.k - s)) • P.g₀) s

Tactic:
· fun_prop (disch := grind)

Goal state after:
case refine_2.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : P.g₀ = 0
⊢ DifferentiableAt ℂ (fun s ↦ (P.ε / (↑P.k - s)) • P.g₀) s
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

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

Tactic:
mul_add,

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

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

Tactic:
mul_add,

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

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

Tactic:
mul_add,

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

Goal state before:
pp: case inl
z τ : ℂ
hτ : τ.im ≤ 0
⊢ 0 = cexp (-↑π * I * (τ + 2 * z)) * (0 - 2 * ↑π * I * 0)

Tactic:
mul_zero,

Goal state after:
case inl
z τ : ℂ
hτ : τ.im ≤ 0
⊢ 0 = cexp (-↑π * I * (τ + 2 * z)) * (0 - 0)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case inl
z : ℂ
⊢ 0 = -2 * ↑π / (-I * 0) ^ (3 / 2) * jacobiTheta₂'' z (-1 / 0)

Tactic:
mul_zero,

Goal state after:
case inl
z : ℂ
⊢ 0 = -2 * ↑π / 0 ^ (3 / 2) * jacobiTheta₂'' z (-1 / 0)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
n : ℤ
| (2 * ↑π * I * (↑n + 1) - 2 * ↑π * I) *
    cexp (2 * ↑π * I * (↑n + 1) * z + ↑π * I * (↑n + 1) ^ 2 * τ + -↑π * I * (τ + 2 * z))

Tactic:
mul_add,

Goal state after:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
| (2 * ↑π * I * ↑n + 2 * ↑π * I * 1 - 2 * ↑π * I) *
    cexp ((2 * ↑π * I * ↑n + 2 * ↑π * I * 1) * z + ↑π * I * (↑n + 1) ^ 2 * τ + -↑π * I * (τ + 2 * z))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

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

Tactic:
mul_zero,

Goal state after:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      cexp (2 * ↑π * I * ↑a * ↑↑(n + 1)) * ↑(rexp (-π * ↑↑(n + 1) ^ 2 * t)) +
        cexp (2 * ↑π * I * ↑a * ↑(-↑(n + 1))) * ↑(rexp (-π * ↑(-↑(n + 1)) ^ 2 * t)))
    (↑(cosKernel (↑a) t) + cexp 0 * ↑(rexp (0 * t)) - (cexp 0 * ↑(rexp (0 * t)) + cexp 0 * ↑(rexp (0 * t))))
⊢ HasSum (fun x ↦ ↑(2 * Real.cos (2 * π * a * (↑x + 1)) * rexp (-π * (↑x + 1) ^ 2 * t))) (↑(cosKernel (↑a) t) - 1)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case inr.e_a
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ -(I *
        (cexp (-↑π * I * z ^ 2 / τ) *
          (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ)))) =
    I *
      (cexp (↑π * I * z ^ 2 * (-1 / τ)) *
        (-jacobiTheta₂' (z / τ) (-1 / τ) + z * jacobiTheta₂ (z / τ) (-1 / τ) * (2 * ↑π * I)))

Tactic:
← mul_neg,

Goal state after:
case inr.e_a
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ I *
      -(cexp (-↑π * I * z ^ 2 / τ) *
          (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))) =
    I *
      (cexp (↑π * I * z ^ 2 * (-1 / τ)) *
        (-jacobiTheta₂' (z / τ) (-1 / τ) + z * jacobiTheta₂ (z / τ) (-1 / τ) * (2 * ↑π * I)))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case inr.e_a
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ I *
      -(cexp (-↑π * I * z ^ 2 / τ) *
          (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))) =
    I *
      (cexp (↑π * I * z ^ 2 * (-1 / τ)) *
        (-jacobiTheta₂' (z / τ) (-1 / τ) + z * jacobiTheta₂ (z / τ) (-1 / τ) * (2 * ↑π * I)))

Tactic:
← mul_neg,

Goal state after:
case inr.e_a
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ I *
      (cexp (-↑π * I * z ^ 2 / τ) *
        -(jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))) =
    I *
      (cexp (↑π * I * z ^ 2 * (-1 / τ)) *
        (-jacobiTheta₂' (z / τ) (-1 / τ) + z * jacobiTheta₂ (z / τ) (-1 / τ) * (2 * ↑π * I)))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case H
x : ℝ
hx : x ≤ 0
a' : ℝ
⊢ cexp (-↑π * ↑a' ^ 2 * ↑x) * (↑a' * 0) = 0

pp: case H.hτ
x : ℝ
hx : x ≤ 0
a' : ℝ
⊢ (I * ↑x).im ≤ 0

pp: case H.hτ
x : ℝ
hx : x ≤ 0
a' : ℝ
⊢ (I * ↑x).im ≤ 0

Tactic:
mul_zero,

Goal state after:
case H
x : ℝ
hx : x ≤ 0
a' : ℝ
⊢ cexp (-↑π * ↑a' ^ 2 * ↑x) * 0 = 0

case H.hτ
x : ℝ
hx : x ≤ 0
a' : ℝ
⊢ (I * ↑x).im ≤ 0

case H.hτ
x : ℝ
hx : x ≤ 0
a' : ℝ
⊢ (I * ↑x).im ≤ 0