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

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

Tactic:
← mul_neg

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

Goal state before:
pp: case h₁
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD yn a1 n ^ 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]
L : xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD yn a1 n ^ 2]
⊢ xn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * yn a1 n [MOD yn a1 n ^ 2 * yn a1 n]

Tactic:
exact hx.mul_right' _

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

Goal state before:
pp: d : ℤ
hd : d ≤ 0
z : ℤ√d
⊢ z.norm = 1 ↔ IsUnit z

Tactic:
by
  rw [← norm_eq_one_iff, ← Int.natCast_inj, Int.natAbs_of_nonneg (norm_nonneg hd z), Int.ofNat_one]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i j✝ n : ℕ
ipos : 0 < i
hin : i ≤ n
h : xn a1 j✝ ≡ xn a1 i [MOD xn a1 n]
j' : ℕ := j✝ % (4 * n)
n4 : 0 < 4 * n
jl : j' < 4 * n
jj : j✝ ≡ j' [MOD 4 * n]
j q : ℕ
⊢ xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]

Tactic:
induction q with

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
p n : ℕ
hp : Prime p
hs : p ∉ s
hn : n ∈ factoredNumbers s
⊢ p ∉ n.primeFactorsList

Tactic:
exact fun H ↦ hs <| hn.2 p H

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph {v | (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1}
z x y : ℕ
e : x % y = z
⊢ (y = 0 ∨ z < y) ∧ ∃ c, z + y * c = x

Tactic:
rw [← e]

Goal state after:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph {v | (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1}
z x y : ℕ
e : x % y = z
⊢ (y = 0 ∨ x % y < y) ∧ ∃ c, x % y + y * c = x
Module: Mathlib.NumberTheory.LSeries.Convergence

Goal state before:
pp: f : ℕ → ℂ
x : ℝ
h : ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x + 1 - 1)
H : ↑x + 1 < abscissaOfAbsConv f
⊢ False

Tactic:
obtain ⟨y, hy₁, hy₂⟩ := EReal.exists_between_coe_real H

Goal state after:
f : ℕ → ℂ
x : ℝ
h : ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x + 1 - 1)
H : ↑x + 1 < abscissaOfAbsConv f
y : ℝ
hy₁ : ↑x + 1 < ↑y
hy₂ : ↑y < abscissaOfAbsConv f
⊢ False
Module: Mathlib.NumberTheory.LSeries.Convergence

Goal state before:
pp: f : ℕ → ℂ
x : ℝ
h : f =O[atTop] fun n ↦ ↑n ^ (x + 1 - 1)
H : ↑x + 1 < abscissaOfAbsConv f
⊢ False

Tactic:
obtain ⟨y, hy₁, hy₂⟩ := EReal.exists_between_coe_real H

Goal state after:
f : ℕ → ℂ
x : ℝ
h : f =O[atTop] fun n ↦ ↑n ^ (x + 1 - 1)
H : ↑x + 1 < abscissaOfAbsConv f
y : ℝ
hy₁ : ↑x + 1 < ↑y
hy₂ : ↑y < abscissaOfAbsConv f
⊢ False
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
⊢ |(fract ξ)⁻¹ - ↑v / ↑u'| < (↑u' * (2 * ↑u' - 1))⁻¹

Tactic:
obtain ⟨Hu, Hu'⟩ := aux₀ hu₀

Goal state after:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
⊢ |(fract ξ)⁻¹ - ↑v / ↑u'| < (↑u' * (2 * ↑u' - 1))⁻¹
Module: Mathlib.NumberTheory.EulerProduct.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ t ⊆ {n | N ≤ n}, ∑' (n : ↑t), f ↑n ∈ Metric.ball 0 ε
⊢ ∃ N, ∀ (s : Finset ℕ), N.primesBelow ⊆ s → ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε

Tactic:
simp_rw [mem_ball_zero_iff] at hN

Goal state after:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ t ⊆ {n | N ≤ n}, ‖∑' (n : ↑t), f ↑n‖ < ε
⊢ ∃ N, ∀ (s : Finset ℕ), N.primesBelow ⊆ s → ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε
Module: Mathlib.NumberTheory.LSeries.Deriv

Goal state before:
pp: case a
f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv (logMul f) < ↑s
⊢ LSeriesSummable f ↑s

Tactic:
refine (LSeriesSummable_of_abscissaOfAbsConv_lt_re <| by simp [hs])
      |>.norm.of_norm_bounded_eventually_nat (g := fun n ↦ ‖term (logMul f) s n‖) ?_

Goal state after:
case a
f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv (logMul f) < ↑s
⊢ ∀ᶠ (i : ℕ) in Filter.atTop, ‖term f (↑s) i‖ ≤ ‖term (logMul f) (↑s) i‖
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

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

Tactic:
← mul_neg

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

Goal state before:
pp: case e'_3.e_a.e_a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x ↦ P.g x - P.g₀) ∘ fun x ↦ x⁻¹) x‖ ≤ C * ‖((fun x ↦ x ^ (-(r + P.k))) ∘ fun x ↦ x⁻¹) x‖
x : ℝ
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0
hC' : ‖P.f x - (P.ε⁻¹ * ↑(x ^ P.k))⁻¹ • P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * ↑(x ^ P.k)‖
⊢ P.ε * ↑(x ^ (-P.k)) = (P.ε⁻¹ * ↑(x ^ P.k))⁻¹

Tactic:
rw [rpow_neg hx.le]

Goal state after:
case e'_3.e_a.e_a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x ↦ P.g x - P.g₀) ∘ fun x ↦ x⁻¹) x‖ ≤ C * ‖((fun x ↦ x ^ (-(r + P.k))) ∘ fun x ↦ x⁻¹) x‖
x : ℝ
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0
hC' : ‖P.f x - (P.ε⁻¹ * ↑(x ^ P.k))⁻¹ • P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * ↑(x ^ P.k)‖
⊢ P.ε * ↑(x ^ P.k)⁻¹ = (P.ε⁻¹ * ↑(x ^ P.k))⁻¹
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: a : ℝ
ha : 0 ≤ a
⊢ ∃ p, 0 < p ∧ (fun t ↦ F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-p * t)

Tactic:
split_ifs with h

Goal state after:
case pos
a : ℝ
ha : 0 ≤ a
h : a = 0
⊢ ∃ p, 0 < p ∧ (fun t ↦ F_nat 0 a t - 1) =O[atTop] fun t ↦ rexp (-p * t)

case neg
a : ℝ
ha : 0 ≤ a
h : ¬a = 0
⊢ ∃ p, 0 < p ∧ (fun t ↦ F_nat 0 a t - 0) =O[atTop] fun t ↦ rexp (-p * t)
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hP : IsStrongFEPair P
r : ℝ
⊢ P.f =O[𝓝[>] 0] fun x ↦ x ^ r

Tactic:
simpa using (hP.hg₀ ▸ P.hf_zero r :)

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
i : ι
⊢ a i = 0 ∨ 0 < π * q i

Tactic:
rcases hq i with h | h <;> simp [h, pi_pos]

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

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : x < 1
⊢ (Ioi 1).indicator (fun x ↦ P.f x - P.f₀) x + (Ioo 0 1).indicator (fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x -
        P.f x +
      P.f₀ =
    (Ioo 0 1).indicator (fun x ↦ P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x + {1}.indicator (fun x ↦ P.f₀ - P.f 1) x

Tactic:
simp_rw [indicator_of_notMem (notMem_Ioi.mpr hx'.le), indicator_of_mem (mem_Ioo.mpr ⟨hx, hx'⟩),
      indicator_of_notMem (mem_singleton_iff.not.mpr hx'.ne)]

Goal state after:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : x < 1
⊢ 0 + (P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) - P.f x + P.f₀ = P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀ + 0
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
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
i : ι
⊢ (if p i = 0 then 0 else a i) = 0 ∨ 0 < p i

Tactic:
split_ifs with h

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.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun n p ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun n p ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ := fun n ↦ 3 * π * ↑|n| ^ 2 * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n
⊢ Summable fun n ↦ 3 * π * (↑|n| ^ 2 * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|)))

Tactic:
exact (summable_pow_mul_jacobiTheta₂_term_bound S hT 2).mul_left _

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

Goal state before:
pp: ι : 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 : ℝ
⊢ 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))

Tactic:
split_ifs with h

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.LSeries.HurwitzZetaEven

Goal state before:
pp: a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
⊢ HasSum (fun n ↦ if ↑n + a = 0 then 0 else rexp (-π * (↑n + a) ^ 2 * t))
    (evenKernel (↑a) t - if ∃ n, ↑n = a then 1 else 0)

Tactic:
split_ifs with h

Goal state after:
case pos
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
h : ∃ n, ↑n = a
⊢ HasSum (fun n ↦ if ↑n + a = 0 then 0 else rexp (-π * (↑n + a) ^ 2 * t)) (evenKernel (↑a) t - 1)

case neg
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
h : ¬∃ n, ↑n = a
⊢ HasSum (fun n ↦ if ↑n + a = 0 then 0 else rexp (-π * (↑n + a) ^ 2 * t)) (evenKernel (↑a) t - 0)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
h : ∃ n, ↑n + a = 0
n : ℤ
hn : ↑n + a = 0
⊢ ↑(-n) = a

Tactic:
simpa [neg_eq_iff_add_eq_zero]

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

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

Tactic:
ofReal_sub,

Goal state after:
a t : ℝ
ht : 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
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ 1 / (-I * τ) ^ (3 / 2) *
      (-I * cexp (-↑π * I * z ^ 2 / τ) *
        (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))) =
    -2 * ↑π * (1 / (-I * τ) ^ (3 / 2)) * jacobiTheta₂'' z (-1 / τ)

Tactic:
mul_comm _ (1 / _),

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

Goal state before:
pp: case H
a : ℝ
⊢ ContinuousOn (fun x ↦ ↑(sinKernel (↑a) x)) (Ioi 0)

Tactic:
simp_rw [sinKernel_def]

Goal state after:
case H
a : ℝ
⊢ ContinuousOn (fun x ↦ jacobiTheta₂' (↑a) (I * ↑x) / (-2 * ↑π)) (Ioi 0)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : (fun x ↦ ‖evenKernel a x - if a = 0 then 1 else 0‖) =O[atTop] fun x ↦ rexp (-v * x)
x : ℝ
| ‖↑(evenKernel a x - if a = 0 then 1 else 0)‖

Tactic:
ofReal_sub,

Goal state after:
a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : (fun x ↦ ‖evenKernel a x - if a = 0 then 1 else 0‖) =O[atTop] fun x ↦ rexp (-v * x)
x : ℝ
| ‖↑(evenKernel a x) - ↑(if a = 0 then 1 else 0)‖
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaEven₀ a (1 - s) = completedCosZeta₀ a s

Tactic:
rw [completedHurwitzZetaEven₀, completedCosZeta₀, sub_div,
    (by simp : (1 / 2 : ℂ) = ↑(1 / 2 : ℝ)),
    (by rfl : (1 / 2 : ℝ) = (hurwitzEvenFEPair a).k),
    (hurwitzEvenFEPair a).functional_equation₀ (s / 2),
    (by rfl : (hurwitzEvenFEPair a).ε = 1),
    one_smul]

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

Goal state before:
pp: case e_f
s : ℂ
hs : 1 < s.re
this : completedRiemannZeta s = ∑' (b : ℕ), if b = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * 0 * ↑b)) / ↑b ^ s
n : ℕ
⊢ (if n = 0 then 0 else ↑π ^ (-s / 2) * Gamma (s / 2) / ↑n ^ s) = ↑π ^ (-s / 2) * Gamma (s / 2) / ↑n ^ s

Tactic:
split_ifs with h

Goal state after:
case pos
s : ℂ
hs : 1 < s.re
this : completedRiemannZeta s = ∑' (b : ℕ), if b = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * 0 * ↑b)) / ↑b ^ s
n : ℕ
h : n = 0
⊢ 0 = ↑π ^ (-s / 2) * Gamma (s / 2) / ↑n ^ s

case neg
s : ℂ
hs : 1 < s.re
this : completedRiemannZeta s = ∑' (b : ℕ), if b = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * 0 * ↑b)) / ↑b ^ s
n : ℕ
h : ¬n = 0
⊢ ↑π ^ (-s / 2) * Gamma (s / 2) / ↑n ^ s = ↑π ^ (-s / 2) * Gamma (s / 2) / ↑n ^ s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

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

Tactic:
have : -(if a = 0 then (1 : ℂ) else 0) = (if a = 0 then -1 else 0) := by { split_ifs <;> simp }

Goal state after:
a : UnitAddCircle
h1 : Tendsto (fun s ↦ s * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] 0) (𝓝 (-if a = 0 then 1 else 0))
this : (-if a = 0 then 1 else 0) = if a = 0 then -1 else 0
⊢ Tendsto (fun s ↦ s * completedHurwitzZetaEven a s) (𝓝[≠] 0) (𝓝 (if a = 0 then -1 else 0))
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: N : ℕ
R : Type u_1
inst✝ : CommMonoidWithZero R
χ : DirichletCharacter R N
n : ℕ
hn : n ≠ 0
⊢ χ ↑n = (toArithmeticFunction fun x ↦ χ ↑x) n

Tactic:
by
  simp [toArithmeticFunction, hn]

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

Goal state before:
pp: case inr.inr
χ : DirichletCharacter ℂ 0
n : ℕ
hn : n ≠ 0
hn' : n ≠ 1
this : ¬IsUnit ↑n
⊢ χ ↑n = δ n

Tactic:
simp_all [χ.map_nonunit this, delta]

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
aux : ↑|0| ^ s = 0
hint :
  HasSum
    (fun n ↦
      s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 +
        s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2)
    (completedCosZeta (↑a) s)
n : ℕ
⊢ (if n = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s) =
    s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 +
      s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2

Tactic:
split_ifs with h

Goal state after:
case pos
a : ℝ
s : ℂ
hs : 1 < s.re
aux : ↑|0| ^ s = 0
hint :
  HasSum
    (fun n ↦
      s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 +
        s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2)
    (completedCosZeta (↑a) s)
n : ℕ
h : n = 0
⊢ 0 =
    s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 +
      s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2

case neg
a : ℝ
s : ℂ
hs : 1 < s.re
aux : ↑|0| ^ s = 0
hint :
  HasSum
    (fun n ↦
      s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 +
        s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2)
    (completedCosZeta (↑a) s)
n : ℕ
h : ¬n = 0
⊢ s.Gammaℝ * ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s =
    s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 +
      s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: h : Summable ({p | Nat.Prime p}.indicator fun n ↦ 1 / ↑n)
k : ℕ
hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n ↦ 1 / ↑n) x < 1 / 2
h' : Summable (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n ↦ 1 / ↑n)
p : ℕ
hp : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow
hp₁ : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow.val
hp₂ : p ∉ k.primesBelow
hpp : Nat.Prime p
⊢ p ∈ {p | k ≤ p}

Tactic:
simpa [primesBelow, hpp] using hp₂

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Norm

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Free ℤ R
inst✝⁸ : Module.Finite ℤ R
K : Type u_2
inst✝⁷ : CommRing K
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝³ : Algebra ℚ K
inst✝² : IsDomain K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b
bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
i✝ j✝ : ι
⊢ (algebraMap ℤ ℚ) (b.toMatrix (Subtype.val ∘ ⇑(bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯)))) i✝ j✝) =
    b₀.toMatrix ((algebraMap R K) ↑I.den • Subtype.val ∘ ⇑bI) i✝ j✝

Tactic:
Basis.toMatrix_apply,

Goal state after:
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Free ℤ R
inst✝⁸ : Module.Finite ℤ R
K : Type u_2
inst✝⁷ : CommRing K
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝³ : Algebra ℚ K
inst✝² : IsDomain K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b
bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
i✝ j✝ : ι
⊢ (algebraMap ℤ ℚ) ((b.repr ((Subtype.val ∘ ⇑(bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯)))) j✝)) i✝) =
    (b₀.repr (((algebraMap R K) ↑I.den • Subtype.val ∘ ⇑bI) j✝)) i✝
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
x y : ↥φ.range
this : ‖φ (ι.symm (x - y))‖ = ‖ψ (ι.symm (x - y))‖
⊢ ‖↑((RingEquiv.ofLeftInverse hiφ) (ι.symm (x - y)))‖ = dist x y

Tactic:
RingEquiv.apply_symm_apply ι _,

Goal state after:
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
x y : ↥φ.range
this : ‖φ (ι.symm (x - y))‖ = ‖ψ (ι.symm (x - y))‖
⊢ ‖↑(x - y)‖ = dist x y
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ∑ w, w.mult = ∑ j, ∑ i with mk i = j, 1

Tactic:
exact Finset.sum_congr rfl
    (fun _ _ => by rw [Finset.sum_const, smul_eq_mul, mul_one, card_filter_mk_eq])

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.univ.erase w₁, f w ^ w.mult
⊢ S ≠ 0

Tactic:
Finset.prod_ne_zero_iff

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.univ.erase w₁, f w ^ w.mult
⊢ ∀ a ∈ Finset.univ.erase w₁, f a ^ a.mult ≠ 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
⊢ (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)

Tactic:
by
  refine Submodule.span_induction ?_ ?_ (fun _ _ _ _ hx hy => ?_) (fun a _ _ hx => ?_) hx
  · rintro _ ⟨x, rfl⟩
    rw [apply_at, apply_at, ComplexEmbedding.conjugate_coe_eq]
  · rw [Pi.zero_apply, Pi.zero_apply, map_zero]
  · rw [Pi.add_apply, Pi.add_apply, map_add, hx, hy]
  · rw [Pi.smul_apply, Complex.real_smul, map_mul, Complex.conj_ofReal]
    exact congrArg ((a : ℂ) * ·) hx

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
⊢ x ∈ ⇑(canonicalEmbedding K).toIntAlgHom.toLinearMap '' ↑(Submodule.span ℤ (Set.range ⇑(integralBasis K))) ↔
    x ∈ Subring.map (canonicalEmbedding K) (algebraMap (𝓞 K) K).range

Tactic:
Subring.mem_map,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
⊢ x ∈ ⇑(canonicalEmbedding K).toIntAlgHom.toLinearMap '' ↑(Submodule.span ℤ (Set.range ⇑(integralBasis K))) ↔
    ∃ x_1 ∈ (algebraMap (𝓞 K) K).range, (canonicalEmbedding K) x_1 = x
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsReal
⊢ NullSingletonClass volume

pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : ¬w.IsReal
⊢ NullSingletonClass volume

Tactic:
· have : NullSingletonClass (volume : Measure ({w : InfinitePlace K // IsReal w} → ℝ)) :=
      pi_nullSingletonClass ⟨w, hw⟩
    exact prod.instNullSingletonClass_fst

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : ¬w.IsReal
⊢ NullSingletonClass volume