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

Goal state before:
pp: case ha
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
this : y ≤ a
⊢ 0 ≤ a - y

pp: case h
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
this : y ≤ a
⊢ 1 ≤ y

Tactic:
<;>

Goal state after:
case ha
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
this : y ≤ a
⊢ 0 ≤ a - y

case h
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
this : y ≤ a
⊢ 1 ≤ y
Module: Mathlib.NumberTheory.LSeries.Convolution

Goal state before:
pp: case inl
f g : ℕ → ℂ
s : ℂ
hS : (fun p ↦ p.1 * p.2) ⁻¹' {0} = {0} ×ˢ univ ∪ univ ×ˢ {0}
snd✝ : ℕ
hp : (0, snd✝) ∈ (fun p ↦ p.1 * p.2) ⁻¹' {0}
⊢ term f s (↑⟨(0, snd✝), hp⟩).1 * term g s (↑⟨(0, snd✝), hp⟩).2 = 0

pp: case inr
f g : ℕ → ℂ
s : ℂ
hS : (fun p ↦ p.1 * p.2) ⁻¹' {0} = {0} ×ˢ univ ∪ univ ×ˢ {0}
fst✝ : ℕ
hp : (fst✝, 0) ∈ (fun p ↦ p.1 * p.2) ⁻¹' {0}
⊢ term f s (↑⟨(fst✝, 0), hp⟩).1 * term g s (↑⟨(fst✝, 0), hp⟩).2 = 0

Tactic:
<;>

Goal state after:
case inl
f g : ℕ → ℂ
s : ℂ
hS : (fun p ↦ p.1 * p.2) ⁻¹' {0} = {0} ×ˢ univ ∪ univ ×ˢ {0}
snd✝ : ℕ
hp : (0, snd✝) ∈ (fun p ↦ p.1 * p.2) ⁻¹' {0}
⊢ term f s (↑⟨(0, snd✝), hp⟩).1 * term g s (↑⟨(0, snd✝), hp⟩).2 = 0

case inr
f g : ℕ → ℂ
s : ℂ
hS : (fun p ↦ p.1 * p.2) ⁻¹' {0} = {0} ×ˢ univ ∪ univ ×ˢ {0}
fst✝ : ℕ
hp : (fst✝, 0) ∈ (fun p ↦ p.1 * p.2) ⁻¹' {0}
⊢ term f s (↑⟨(fst✝, 0), hp⟩).1 * term g s (↑⟨(fst✝, 0), hp⟩).2 = 0
Module: Mathlib.NumberTheory.LSeries.Deriv

Goal state before:
pp: f : ℕ → ℂ
n : ℕ
s : ℂ
hn : n ≠ 0
⊢ HasDerivAt (fun z ↦ ↑n ^ (-z)) (-log ↑n * ↑n ^ (-s)) s

Tactic:
simpa only [mul_comm, ← mul_neg_one (log n), ← mul_assoc]
    using (hasDerivAt_neg' s).const_cpow (Or.inl <| Nat.cast_ne_zero.mpr hn)

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

Goal state before:
pp: case e'_5
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₁ : ↑1 = 1 → -(1 / 2) < ξ - ↑u
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ↑u ≤ ξ
⊢ ↑u = ↑u / ↑↑1

pp: case e'_6
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₁ : ↑1 = 1 → -(1 / 2) < ξ - ↑u
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ↑u ≤ ξ
⊢ 1 = (↑↑1 * (2 * ↑↑1 - 1))⁻¹

Tactic:
<;>

Goal state after:
case e'_5
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₁ : ↑1 = 1 → -(1 / 2) < ξ - ↑u
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ↑u ≤ ξ
⊢ ↑u = ↑u / ↑↑1

case e'_6
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₁ : ↑1 = 1 → -(1 / 2) < ξ - ↑u
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ↑u ≤ ξ
⊢ 1 = (↑↑1 * (2 * ↑↑1 - 1))⁻¹
Module: Mathlib.NumberTheory.LSeries.Deriv

Goal state before:
pp: case a
f : ℕ → ℂ
⊢ abscissaOfAbsConv (logMul f) ≤ abscissaOfAbsConv f

pp: case a
f : ℕ → ℂ
⊢ abscissaOfAbsConv f ≤ abscissaOfAbsConv (logMul f)

Tactic:
<;>

Goal state after:
case a
f : ℕ → ℂ
⊢ abscissaOfAbsConv (logMul f) ≤ abscissaOfAbsConv f

case a
f : ℕ → ℂ
⊢ abscissaOfAbsConv f ≤ abscissaOfAbsConv (logMul f)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case hf₁
S T : ℝ
hT : 0 < T
k : ℕ
this : Summable fun n ↦ ↑n ^ k * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑n))
⊢ Summable fun n ↦ ↑|↑n| ^ k * rexp (-π * (T * ↑↑n ^ 2 - 2 * S * ↑|↑n|))

pp: case hf₂
S T : ℝ
hT : 0 < T
k : ℕ
this : Summable fun n ↦ ↑n ^ k * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑n))
⊢ Summable fun n ↦ ↑|(-↑n)| ^ k * rexp (-π * (T * ↑(-↑n) ^ 2 - 2 * S * ↑|(-↑n)|))

Tactic:
<;>

Goal state after:
case hf₁
S T : ℝ
hT : 0 < T
k : ℕ
this : Summable fun n ↦ ↑n ^ k * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑n))
⊢ Summable fun n ↦ ↑|↑n| ^ k * rexp (-π * (T * ↑↑n ^ 2 - 2 * S * ↑|↑n|))

case hf₂
S T : ℝ
hT : 0 < T
k : ℕ
this : Summable fun n ↦ ↑n ^ k * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑n))
⊢ Summable fun n ↦ ↑|(-↑n)| ^ k * rexp (-π * (T * ↑(-↑n) ^ 2 - 2 * S * ↑|(-↑n)|))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: n : ℤ
z τ : ℂ
this : ‖(jacobiTheta₂_term_fderiv n z τ) (0, 1)‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ π * ↑|n| ^ 2 * ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)‖ ≤
    ‖(cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ) •
          ((2 * ↑π * I * ↑n) • ContinuousLinearMap.fst ℂ ℂ ℂ + (↑π * I * ↑n ^ 2) • ContinuousLinearMap.snd ℂ ℂ ℂ))
        (0, 1)‖

Tactic:
FunLike.coe_smul,

Goal state after:
n : ℤ
z τ : ℂ
this : ‖(jacobiTheta₂_term_fderiv n z τ) (0, 1)‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ π * ↑|n| ^ 2 * ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)‖ ≤
    ‖(cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ) •
          ⇑((2 * ↑π * I * ↑n) • ContinuousLinearMap.fst ℂ ℂ ℂ + (↑π * I * ↑n ^ 2) • ContinuousLinearMap.snd ℂ ℂ ℂ))
        (0, 1)‖
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: n : ℤ
z τ : ℂ
this : ‖(jacobiTheta₂_term_fderiv n z τ) (0, 1)‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ π * ↑|n| ^ 2 * ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)‖ ≤
    ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ) •
        (((2 * ↑π * I * ↑n) • ContinuousLinearMap.fst ℂ ℂ ℂ) (0, 1) +
          ((↑π * I * ↑n ^ 2) • ContinuousLinearMap.snd ℂ ℂ ℂ) (0, 1))‖

Tactic:
FunLike.coe_smul,

Goal state after:
n : ℤ
z τ : ℂ
this : ‖(jacobiTheta₂_term_fderiv n z τ) (0, 1)‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ π * ↑|n| ^ 2 * ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)‖ ≤
    ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ) •
        (((2 * ↑π * I * ↑n) • ⇑(ContinuousLinearMap.fst ℂ ℂ ℂ)) (0, 1) +
          ((↑π * I * ↑n ^ 2) • ⇑(ContinuousLinearMap.snd ℂ ℂ ℂ)) (0, 1))‖
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: 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

pp: 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

Tactic:
<;>

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.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : x < 1
this : 1 < 1 / x
⊢ P.ε * ↑(x ^ P.k) * 1 = P.ε * ↑(x ^ P.k) * 1

pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : x < 1
this : 1 < 1 / x
⊢ -1 = P.ε * ↑(x ^ P.k) * -(P.ε⁻¹ * (↑(x ^ P.k))⁻¹ * 1)

Tactic:
<;>

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : x < 1
this : 1 < 1 / x
⊢ P.ε * ↑(x ^ P.k) * 1 = P.ε * ↑(x ^ P.k) * 1

E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : x < 1
this : 1 < 1 / x
⊢ -1 = P.ε * ↑(x ^ P.k) * -(P.ε⁻¹ * (↑(x ^ P.k))⁻¹ * 1)
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case pos
ι : 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
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
i : ι
h : p i = 0
⊢ 0 = 0 ∨ 0 < p i

pp: case neg
ι : 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
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
i : ι
h : ¬p i = 0
⊢ a i = 0 ∨ 0 < p i

Tactic:
<;>

Goal state after:
case pos
ι : 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
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
i : ι
h : p i = 0
⊢ 0 = 0 ∨ 0 < p i

case neg
ι : 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
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
i : ι
h : ¬p i = 0
⊢ a i = 0 ∨ 0 < p i
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

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

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

Tactic:
<;>

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

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

Goal state before:
pp: case refine_1
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)
this :
  (fun t ↦ F_int 0 (↑a) t - if a = 0 then 1 else 0) =ᶠ[atTop] fun t ↦
    (F_nat 0 a t - if a = 0 then 1 else 0) + F_nat 0 (1 - a) t
⊢ (fun t ↦ rexp (-p * t)) =O[atTop] fun t ↦ rexp (-min p q * t)

pp: case refine_2
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)
this :
  (fun t ↦ F_int 0 (↑a) t - if a = 0 then 1 else 0) =ᶠ[atTop] fun t ↦
    (F_nat 0 a t - if a = 0 then 1 else 0) + F_nat 0 (1 - a) t
⊢ (fun t ↦ rexp (-q * t)) =O[atTop] fun t ↦ rexp (-min p q * t)

Tactic:
<;>

Goal state after:
case refine_1
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)
this :
  (fun t ↦ F_int 0 (↑a) t - if a = 0 then 1 else 0) =ᶠ[atTop] fun t ↦
    (F_nat 0 a t - if a = 0 then 1 else 0) + F_nat 0 (1 - a) t
⊢ (fun t ↦ rexp (-p * t)) =O[atTop] fun t ↦ rexp (-min p q * t)

case refine_2
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)
this :
  (fun t ↦ F_int 0 (↑a) t - if a = 0 then 1 else 0) =ᶠ[atTop] fun t ↦
    (F_nat 0 a t - if a = 0 then 1 else 0) + F_nat 0 (1 - a) t
⊢ (fun t ↦ rexp (-q * t)) =O[atTop] fun t ↦ rexp (-min p q * t)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: case refine_1
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)
this : F_int 1 ↑a =ᶠ[atTop] fun t ↦ F_nat 1 a t + F_nat 1 (1 - a) t
⊢ (fun t ↦ rexp (-p * t)) =O[atTop] fun t ↦ rexp (-min p q * t)

pp: case refine_2
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)
this : F_int 1 ↑a =ᶠ[atTop] fun t ↦ F_nat 1 a t + F_nat 1 (1 - a) t
⊢ (fun t ↦ rexp (-q * t)) =O[atTop] fun t ↦ rexp (-min p q * t)

Tactic:
<;>

Goal state after:
case refine_1
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)
this : F_int 1 ↑a =ᶠ[atTop] fun t ↦ F_nat 1 a t + F_nat 1 (1 - a) t
⊢ (fun t ↦ rexp (-p * t)) =O[atTop] fun t ↦ rexp (-min p q * t)

case refine_2
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)
this : F_int 1 ↑a =ᶠ[atTop] fun t ↦ F_nat 1 a t + F_nat 1 (1 - a) t
⊢ (fun t ↦ rexp (-q * t)) =O[atTop] fun t ↦ rexp (-min p q * t)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
x : ℝ
⊢ evenKernel (-a) x = evenKernel a x

Tactic:
induction a using QuotientAddGroup.induction_on with
  | H => simp [← QuotientAddGroup.mk_neg, ← ofReal_inj, evenKernel_def, jacobiTheta₂_neg_left]

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

Goal state before:
pp: case pos
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
i : ι
t : ℝ
h : r i = 0
⊢ a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = 0

pp: case neg
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
i : ι
t : ℝ
h : ¬r i = 0
⊢ a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
i : ι
t : ℝ
h : r i = 0
⊢ a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = 0

case neg
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
i : ι
t : ℝ
h : ¬r i = 0
⊢ a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

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

Tactic:
← Complex.exp_add,

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

Goal state before:
pp: case inr.H
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * ↑(1 / x) = -1 / (I * ↑x)
hx' : I * ↑x ≠ 0
h2 : ↑a * I * ↑x / (I * ↑x) = ↑a
h3 : 1 / (-I * (I * ↑x)) ^ (1 / 2) = 1 / ↑(x ^ (1 / 2))
h4 : -↑π * I * (↑a * I * ↑x) ^ 2 / (I * ↑x) = -(-↑π * ↑a ^ 2 * ↑x)
⊢ 1 / ↑(x ^ (1 / 2)) * (cexp (-(-↑π * ↑a ^ 2 * ↑x)) * cexp (-↑π * ↑a ^ 2 * ↑x)) * jacobiTheta₂ (↑a) (-1 / (I * ↑x)) =
    ↑(1 / x ^ (1 / 2)) * jacobiTheta₂ (↑a) (-1 / (I * ↑x))

Tactic:
← Complex.exp_add,

Goal state after:
case inr.H
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * ↑(1 / x) = -1 / (I * ↑x)
hx' : I * ↑x ≠ 0
h2 : ↑a * I * ↑x / (I * ↑x) = ↑a
h3 : 1 / (-I * (I * ↑x)) ^ (1 / 2) = 1 / ↑(x ^ (1 / 2))
h4 : -↑π * I * (↑a * I * ↑x) ^ 2 / (I * ↑x) = -(-↑π * ↑a ^ 2 * ↑x)
⊢ 1 / ↑(x ^ (1 / 2)) * cexp (-(-↑π * ↑a ^ 2 * ↑x) + -↑π * ↑a ^ 2 * ↑x) * jacobiTheta₂ (↑a) (-1 / (I * ↑x)) =
    ↑(1 / x ^ (1 / 2)) * jacobiTheta₂ (↑a) (-1 / (I * ↑x))
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hP : IsStrongFEPair P
s : ℂ
t : ℝ
ht₁ : t ≠ 1
ht₀ : 0 < t
ht : t < 1
⊢ ↑t ^ (s - 1) • (((Ioo 0 1).indicator fun x ↦ P.f x) + (Ioi 1).indicator fun x ↦ P.f x) t = ↑t ^ (s - 1) • P.f t

pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hP : IsStrongFEPair P
s : ℂ
t : ℝ
ht₁ : t ≠ 1
ht₀ : 0 < t
ht : ¬t < 1
⊢ ↑t ^ (s - 1) • (((Ioi 1).indicator fun x ↦ P.f x) + (Ioo 0 1).indicator fun x ↦ P.f x) t = ↑t ^ (s - 1) • P.f t

Tactic:
<;>

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hP : IsStrongFEPair P
s : ℂ
t : ℝ
ht₁ : t ≠ 1
ht₀ : 0 < t
ht : t < 1
⊢ ↑t ^ (s - 1) • (((Ioo 0 1).indicator fun x ↦ P.f x) + (Ioi 1).indicator fun x ↦ P.f x) t = ↑t ^ (s - 1) • P.f t

case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hP : IsStrongFEPair P
s : ℂ
t : ℝ
ht₁ : t ≠ 1
ht₀ : 0 < t
ht : ¬t < 1
⊢ ↑t ^ (s - 1) • (((Ioi 1).indicator fun x ↦ P.f x) + (Ioo 0 1).indicator fun x ↦ P.f x) t = ↑t ^ (s - 1) • P.f t
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case refine_1
z τ J J' : ℂ
⊢ ↑π * I * (z + 1) ^ 2 * τ + -↑π * I * (τ + 2 * (z * τ)) = ↑π * I * z ^ 2 * τ

pp: case refine_2
z τ J J' : ℂ
⊢ J' - 2 * ↑π * I * J + (z * J + J) * (2 * ↑π * I) = J' + z * J * (2 * ↑π * I)

Tactic:
<;>

Goal state after:
case refine_1
z τ J J' : ℂ
⊢ ↑π * I * (z + 1) ^ 2 * τ + -↑π * I * (τ + 2 * (z * τ)) = ↑π * I * z ^ 2 * τ

case refine_2
z τ J J' : ℂ
⊢ J' - 2 * ↑π * I * J + (z * J + J) * (2 * ↑π * I) = J' + z * J * (2 * ↑π * I)
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 * τ) * cexp (-↑π * I * (τ + 2 * z)))

Tactic:
← Complex.exp_add,

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

Goal state before:
pp: case inl
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
i : ι
h : r i = 0
⊢ 0 = (s + 1).Gammaℝ * (a i * 0) / 0

Tactic:
div_zero

Goal state after:
case inl
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
i : ι
h : r i = 0
⊢ 0 = 0
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
⊢ ∑' (n : ℤ), jacobiTheta₂'_term n (-z) τ = -∑' (n : ℤ), jacobiTheta₂'_term n z τ

Tactic:
← tsum_neg,

Goal state after:
z τ : ℂ
⊢ ∑' (n : ℤ), jacobiTheta₂'_term n (-z) τ = ∑' (b : ℤ), -jacobiTheta₂'_term b z τ
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
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:
<;>

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

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

Goal state before:
pp: case inl
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
i : ι
h : r i = 0
⊢ 0 = ‖a i‖ / 0

Tactic:
div_zero

Goal state after:
case inl
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
i : ι
h : r i = 0
⊢ 0 = 0