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

Goal state before:
pp: a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
⊢ ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))

Tactic:
by
      let k2nl : 2 * n - k < n := by lia
      have xle : xn a1 (2 * n - k) ≤ xn a1 n := le_of_lt <| strictMono_x a1 k2nl
      suffices xn a1 k % xn a1 n = xn a1 n - xn a1 (2 * n - k) by rw [this, Int.ofNat_sub xle]
      rw [← Nat.mod_eq_of_lt (Nat.sub_lt (x_pos a1 n) (x_pos a1 (2 * n - k)))]
      apply ModEq.add_right_cancel' (xn a1 (2 * n - k))
      rw [tsub_add_cancel_of_le xle]
      have t := xn_modEq_x2n_sub_lem a1 k2nl.le
      rw [tsub_tsub_cancel_of_le k2n] at t
      exact t.trans dvd_rfl.zero_modEq_nat

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
d : ℤ
r : { r // r * r = ↑d }
⊢ ↑(re 1) + ↑(im 1) * ↑r = 1

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
d : ℤ
r : { r // r * r = ↑d }
⊢ ↑(re 0) + ↑(im 0) * ↑r = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
d : ℤ
r : { r // r * r = ↑d }
⊢ (fun f ↦ ⟨f sqrtd, ⋯⟩)
      ((fun r ↦ { toFun := fun a ↦ ↑a.re + ↑a.im * ↑r, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })
        r) =
    r

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : (n - 1).succ = n
il : i ≤ n - 1
ile : i = n - 1
e : 2 * xn a1 (n - 1) = xn a1 n
⊢ a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2

Tactic:
let ⟨a2, s1⟩ :=
                    @eq_of_xn_modEq_lem2 _ a1 (n - 1)
                      (by rwa [tsub_add_cancel_of_le (succ_le_of_lt npos)])

Goal state after:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : (n - 1).succ = n
il : i ≤ n - 1
ile : i = n - 1
e : 2 * xn a1 (n - 1) = xn a1 n
a2 : a = 2
s1 : n - 1 = 0
⊢ a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2
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]
this : ∀ (j q : ℕ), xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]
⊢ xn a1 j ≡ xn a1 j' [MOD xn a1 n]

Tactic:
rw [← Nat.mod_add_div j (4 * n)]

Goal state after:
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]
this : ∀ (j q : ℕ), xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]
⊢ xn a1 (j % (4 * n) + 4 * n * (j / (4 * n))) ≡ xn a1 j' [MOD xn a1 n]
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
⊢ xn a1 0 ≡ xn b1 0 [MOD c] ∧ yn a1 0 ≡ yn b1 0 [MOD c]

Tactic:
simp [Nat.ModEq.refl]

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: case right
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
hpm : ¬p ∣ m
⊢ List.filter (fun x ↦ decide (x ∈ s)) (replicate e p) ++ List.filter (fun x ↦ decide (x ∈ s)) m.primeFactorsList ~
    m.primeFactorsList

Tactic:
filter_eq_nil_iff.mpr <| by grind,

Goal state after:
case right
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
hpm : ¬p ∣ m
⊢ [] ++ List.filter (fun x ↦ decide (x ∈ s)) m.primeFactorsList ~ m.primeFactorsList
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:
by
                rw [← e]
                exact ⟨or_iff_not_imp_left.2 fun h => mod_lt _ (Nat.pos_of_ne_zero h), x / y,
                  mod_add_div _ _⟩

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

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
h : (↑u - ξ * ↑v) * (2 * ↑v - 1) + ↑v * (2 * ↑v - 1) < ↑v * (2 * ↑v - 1) + 1
this : (↑u - ↑⌊ξ⌋ * ↑v) * (2 * ↑v - 1) < (↑u - ξ * ↑v + ↑v) * (2 * ↑v - 1)
⊢ (u - ⌊ξ⌋ * v) * (2 * v - 1) < v * (2 * v - 1) + 1

Tactic:
add_mul

Goal state after:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
h : (↑u - ξ * ↑v) * (2 * ↑v - 1) + ↑v * (2 * ↑v - 1) < ↑v * (2 * ↑v - 1) + 1
this : (↑u - ↑⌊ξ⌋ * ↑v) * (2 * ↑v - 1) < (↑u - ξ * ↑v) * (2 * ↑v - 1) + ↑v * (2 * ↑v - 1)
⊢ (u - ⌊ξ⌋ * v) * (2 * v - 1) < v * (2 * v - 1) + 1
Module: Mathlib.NumberTheory.LSeries.Convergence

Goal state before:
pp: f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
⊢ s.re ≤ (↑s.re).re

Tactic:
by simp

Goal state after:
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
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]
ky : k ≤ 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])
ipos : i > 0
iln : i ≤ n
yd : 4 * yn a1 i ∣ 4 * n
jk : j ≡ k [MOD 4 * yn a1 i]
⊢ yn a1 i + yn a1 i < 4 * yn a1 i

Tactic:
rw [← two_mul]
                exact Nat.mul_lt_mul_of_pos_right (by decide) (strictMono_y a1 ipos)

Goal state after:
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 ^ 2 * τ.im + -(2 * π * ↑n * z.im) ≤ -π * (T * ↑n ^ 2 + -(2 * S * ↑|n|))

Tactic:
neg_mul,

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

Goal state before:
pp: ⊢ 1 - 0 ≠ 0

Tactic:
by simp

Goal state after:
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:
neg_mul,

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

Goal state before:
pp: case convert_3.inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this : IntegrableOn (fun x ↦ ↑(rexp (-(p i * x))) * ↑(p i * x) ^ (s - 1)) (Ioi 0) volume
t : ℝ
ht : 0 < t
⊢ 1 / ↑(p i) ^ (s - 1) * ↑(p i * t) ^ (s - 1) * ↑(rexp (-(p i * t))) = ↑t ^ (s - 1) * ↑(rexp (-p i * t))

Tactic:
neg_mul,

Goal state after:
case convert_3.inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this : IntegrableOn (fun x ↦ ↑(rexp (-(p i * x))) * ↑(p i * x) ^ (s - 1)) (Ioi 0) volume
t : ℝ
ht : 0 < t
⊢ 1 / ↑(p i) ^ (s - 1) * ↑(p i * t) ^ (s - 1) * ↑(rexp (-(p i * t))) = ↑t ^ (s - 1) * ↑(rexp (-(p i * t)))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case refine_2.inr.inr.inr
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im = 0
hz : 0 < z.im
this : Function.Injective fun x ↦ -↑x
h : Tendsto (fun x ↦ rexp (-(-(2 * π * ↑x) * z.im))) atTop (𝓝 0)
⊢ False

Tactic:
neg_mul,

Goal state after:
case refine_2.inr.inr.inr
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im = 0
hz : 0 < z.im
this : Function.Injective fun x ↦ -↑x
h : Tendsto (fun x ↦ rexp (- -(2 * π * ↑x * z.im))) atTop (𝓝 0)
⊢ False
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)‖ *
      ‖(2 * ↑π * I * ↑n) • ContinuousLinearMap.fst ℂ ℂ ℂ + (↑π * I * ↑n ^ 2) • ContinuousLinearMap.snd ℂ ℂ ℂ‖ ≤
    ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)‖ * ((2 * π + 1 * π) * ↑|n| ^ 2)

Tactic:
add_mul

Goal state after:
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)‖ *
      ‖(2 * ↑π * I * ↑n) • ContinuousLinearMap.fst ℂ ℂ ℂ + (↑π * I * ↑n ^ 2) • ContinuousLinearMap.snd ℂ ℂ ℂ‖ ≤
    ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)‖ * (2 * π * ↑|n| ^ 2 + 1 * π * ↑|n| ^ 2)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ HasSum (fun n ↦ (↑n + a) * rexp (-π * (↑n + a ^ 2) * t))
    (rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 + a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t)))

Tactic:
add_mul

Goal state after:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ HasSum (fun n ↦ ↑n * rexp (-π * (↑n + a ^ 2) * t) + a * rexp (-π * (↑n + a ^ 2) * t))
    (rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 + a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t)))
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

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

Tactic:
indicator_of_mem (mem_Ioi.mpr this),

Goal state after:
case inr.inr
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.f (1 / x) - P.f₀ + (Ioo 0 1).indicator (fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) (1 / x) =
    (P.ε * ↑(x ^ P.k)) • P.g_modif x
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: a : ℝ
ha : 0 ≤ a
aux' : (fun t ↦ ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x ↦ 1
ha' : 0 < a
| fun t ↦ rexp (-(π * a ^ 2) * t)

Tactic:
t

Goal state after:
a : ℝ
ha : 0 ≤ a
aux' : (fun t ↦ ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x ↦ 1
ha' : 0 < a
t : ℝ
| rexp (-(π * a ^ 2) * t)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ 0 < 3

Tactic:
by simp

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

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
⊢ ∀ (m : ℂ) (x : ℂ × ℂ →L[ℂ] ℂ), (m • x) (1, 0) = (RingHom.id ℂ) m • x (1, 0)

Tactic:
by simp

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

Goal state before:
pp: x : ℝ
hx : 0 < x
a : ℝ
h1 : I * ↑(1 / x) = -1 / (I * ↑x)
hx' : I * ↑x ≠ 0
h2 : ↑a * I * ↑x / (I * ↑x) = ↑a
⊢ 1 / (-I * (I * ↑x)) ^ (1 / 2) = 1 / ↑(x ^ (1 / 2))

Tactic:
neg_mul,

Goal state after:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * ↑(1 / x) = -1 / (I * ↑x)
hx' : I * ↑x ≠ 0
h2 : ↑a * I * ↑x / (I * ↑x) = ↑a
⊢ 1 / (-(I * (I * ↑x))) ^ (1 / 2) = 1 / ↑(x ^ (1 / 2))
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ 𝓝 (P.ε • P.g₀) = 𝓝 (0 - 0 - -P.ε • P.g₀)

Tactic:
by simp

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ 𝓝 0 = 𝓝 ((↑P.k - ↑P.k) • P.Λ₀ ↑P.k)

Tactic:
by simp

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ 𝓝 0 = 𝓝 ((↑P.k - ↑P.k) • (1 / ↑P.k) • P.f₀)

Tactic:
by simp

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

Goal state before:
pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ ContinuousAt (HDiv.hDiv 1) ↑P.k

Tactic:
have := ofReal_ne_zero.mpr P.hk.ne'

Goal state after:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
this : ↑P.k ≠ 0
⊢ ContinuousAt (HDiv.hDiv 1) ↑P.k
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ 𝓝 (-P.f₀) = 𝓝 (0 • P.Λ₀ 0 - P.f₀ - 0)

Tactic:
by simp

Goal state after:
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
s : ℂ
⊢ {1}.Subsingleton

Tactic:
by simp

Goal state after:
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:
mul_assoc _ (cexp _) (cexp _),

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)) * cexp (-↑π * ↑a ^ 2 * ↑x)) * jacobiTheta₂ (↑a) (-1 / (I * ↑x)) =
    ↑(1 / x ^ (1 / 2)) * jacobiTheta₂ (↑a) (-1 / (I * ↑x))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: z : ℂ
⊢ im 0 ≤ 0

Tactic:
by simp

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

Goal state before:
pp: z : ℂ
⊢ 3 / 2 ≠ 0

Tactic:
by simp

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

Goal state before:
pp: z τ : ℂ
hτ : τ ≠ 0
⊢ -2 * ↑π = 2 * ↑π * -1

Tactic:
neg_mul,

Goal state after:
z τ : ℂ
hτ : τ ≠ 0
⊢ -(2 * ↑π) = 2 * ↑π * -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:
neg_mul,

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) / τ) *
        (-jacobiTheta₂' (z / τ) (-(1 / τ)) + z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * ↑π * I)))

Tactic:
neg_mul,

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) / τ) *
        (-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) / τ) *
        (-jacobiTheta₂' (z / τ) (-(1 / τ)) + z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * ↑π * I)))

Tactic:
neg_mul,

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) / τ) *
        (-jacobiTheta₂' (z / τ) (-(1 / τ)) + z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * ↑π * I)))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

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

Tactic:
neg_mul,

Goal state after:
x : ℝ
hx : 0 < x
a : ℝ
⊢ - -(↑x * I) = I * ↑x
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

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

Tactic:
neg_mul,

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

Goal state before:
pp: a : UnitAddCircle
⊢ 𝓝 1 = 𝓝 (1 + (1 - 1) * hurwitzZetaOdd a 1)

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: ⊢ (abscissaOfAbsConv fun n ↦ ↑(μ n)) = 1

Tactic:
by
  simpa [abscissaOfAbsConv, LSeriesSummable_moebius_iff, Set.Ioi_def, EReal.image_coe_Ioi]
    using csInf_Ioo <| EReal.coe_lt_top 1

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

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

Tactic:
neg_mul,

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

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

Tactic:
neg_mul,

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

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

Tactic:
neg_mul,

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

Goal state before:
pp: x : ℝ
hx : 1 < x
hx' : 1 < (↑x).re
x✝ : ℕ
⊢ 0 x✝ ≤ 1 x✝

Tactic:
by simp

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

Goal state before:
pp: x : ℝ
hx : 1 < x
hx' : 1 < (↑x).re
⊢ 0 < 1 1

Tactic:
by simp

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

Goal state before:
pp: s : ℂ
hs : 1 < s.re
hf : Summable fun x ↦ ‖term (logMul 1) s x‖
n : ℕ
hΛ : ‖(fun n ↦ ↑(Λ n)) n‖ ≤ ‖Complex.log ↑n‖
⊢ ‖Complex.log ↑n‖ ≤ ‖logMul 1 n‖

Tactic:
by simp

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

Goal state before:
pp: x✝⁵ x✝⁴ x✝³ : ℕ
x✝² : x✝⁵ ≠ 0
x✝¹ : x✝⁴ ≠ 0
x✝ : x✝³ ≠ 0
⊢ x✝⁵ ^ 0 + x✝⁴ ^ 0 ≠ x✝³ ^ 0

Tactic:
by simp

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

Goal state before:
pp: h : FermatLastTheoremFor 1
⊢ 1 ≠ 0

Tactic:
by simp

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

Goal state before:
pp: h : FermatLastTheoremFor 1
⊢ 2 ≠ 0

Tactic:
by simp

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

Goal state before:
pp: h : FermatLastTheoremFor 1
⊢ 1 ^ 1 + 1 ^ 1 = 2 ^ 1

Tactic:
by simp

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

Goal state before:
pp: h : FermatLastTheoremFor 2
⊢ 3 ≠ 0

Tactic:
by simp

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

Goal state before:
pp: h : FermatLastTheoremFor 2
⊢ 4 ≠ 0

Tactic:
by simp

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

Goal state before:
pp: h : FermatLastTheoremFor 2
⊢ 5 ≠ 0

Tactic:
by simp

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

Goal state before:
pp: h : FermatLastTheoremFor 2
⊢ 3 ^ 2 + 4 ^ 2 = 5 ^ 2

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
neg_mul,

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

Goal state before:
pp: a : UnitAddCircle
hs' : 1 ≠ 1 ∨ a ≠ 0
x : ℂ
hx : x ∈ {0}ᶜ
⊢ Function.update (fun s ↦ completedCosZeta a s / s.Gammaℝ) 0 (-1 / 2) x = completedCosZeta a x * x.Gammaℝ⁻¹

Tactic:
Function.update_of_ne hx,

Goal state after:
a : UnitAddCircle
hs' : 1 ≠ 1 ∨ a ≠ 0
x : ℂ
hx : x ∈ {0}ᶜ
⊢ completedCosZeta a x / x.Gammaℝ = completedCosZeta a x * x.Gammaℝ⁻¹