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

Goal state before:
pp: p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (cyclotomic (p ^ k) K)
heven : Even (φ (p ^ k) / 2)
⊢ 1 * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1)) = ↑↑1 * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (cyclotomic (p ^ k) K)
heven : ¬Even (φ (p ^ k) / 2)
⊢ -1 * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1)) = ↑↑(-1) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))

Tactic:
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 1) + ↑(im 1) * ↑r = 1

Tactic:
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:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
d : ℤ
f : ℤ√d →+* R
⊢ f ↑d = ↑d

Tactic:
map_intCast

Goal state after:
R : Type u_1
inst✝ : CommRing R
d : ℤ
f : ℤ√d →+* R
⊢ ↑d = ↑d
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:
simp

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

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

Tactic:
simp

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:
intro j

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]
j : ℕ
⊢ ∀ (q : ℕ), xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

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

Tactic:
hf

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

Goal state before:
pp: case inr
p n : ℕ
hp : p ≠ 0
e : ℕ
hn : n ∈ p.smoothNumbers
this : NoZeroDivisors ℕ
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
H : q ∈ n.primeFactorsList
⊢ q < p.succ

Tactic:
· exact (hn.2 q H).trans <| lt_succ_self p

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

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

Tactic:
simp

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

Goal state before:
pp: case bot
f : ℕ → ℂ
x : ℝ
h : ∀ (y : ℝ), x < y → LSeriesSummable f ↑y
y : EReal
hy : ∀ (a : ℝ), LSeriesSummable f ↑a → y ≤ ↑a
⊢ ↑x < ⊥ → y ≤ ⊥

Tactic:
simp

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

Goal state before:
pp: case top
f : ℕ → ℂ
x : ℝ
h : ∀ (y : ℝ), x < y → LSeriesSummable f ↑y
y : EReal
hy : ∀ (a : ℝ), LSeriesSummable f ↑a → y ≤ ↑a
⊢ ↑x < ⊤ → y ≤ ⊤

Tactic:
simp

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

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

Tactic:
hf

Goal state after:
case refine_1
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
hu₁ : u - ⌊ξ⌋ * v ≤ v
huv_cop : IsCoprime 0 v
hf : u - ⌊ξ⌋ * v = 0
⊢ False
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:
by
                rw [← two_mul]
                exact Nat.mul_lt_mul_of_pos_right (by decide) (strictMono_y a1 ipos)

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

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

Tactic:
hf

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

Goal state before:
pp: f : ℕ → ℝ
x : ℝ
h : (abscissaOfAbsConv fun x ↦ ↑(f x)) < ↑x
aux : term (fun x ↦ ↑(f x)) ↑x = fun n ↦ ↑(if n = 0 then 0 else f n / ↑n ^ x)
this : Summable fun x_1 ↦ if x_1 = 0 then 0 else f x_1 / ↑x_1 ^ x
⊢ Summable fun n ↦ f n / ↑n ^ x

Tactic:
refine this.congr_cofinite ?_

Goal state after:
f : ℕ → ℝ
x : ℝ
h : (abscissaOfAbsConv fun x ↦ ↑(f x)) < ↑x
aux : term (fun x ↦ ↑(f x)) ↑x = fun n ↦ ↑(if n = 0 then 0 else f n / ↑n ^ x)
this : Summable fun x_1 ↦ if x_1 = 0 then 0 else f x_1 / ↑x_1 ^ x
⊢ (fun x_1 ↦ if x_1 = 0 then 0 else f x_1 / ↑x_1 ^ x) =ᶠ[Filter.cofinite] fun n ↦ f n / ↑n ^ x
Module: Mathlib.NumberTheory.LSeries.Convolution

Goal state before:
pp: case inl
f g : ℕ → ℂ
s : ℂ
⊢ term (f ⍟ g) s 0 = ∑ p ∈ divisorsAntidiagonal 0, term f s p.1 * term g s p.2

Tactic:
simp

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

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
x✝ : ℕ × ℕ
⊢ x✝ ∈ (fun p ↦ p.1 * p.2) ⁻¹' {0} ↔ x✝ ∈ {0} ×ˢ univ ∪ univ ×ˢ {0}

Tactic:
simp

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

Tactic:
simp

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

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

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

Goal state before:
pp: f g : ℕ → ℂ
s a b : ℂ
hf : LSeriesHasSum f s a
hg : LSeriesHasSum g s b
⊢ LSeriesHasSum (f ⍟ g) s (a * b)

Tactic:
by
  have hsum := summable_mul_of_summable_norm hf.summable.norm hg.summable.norm
  -- NB: this `simpa` is quite slow if un-squeezed
  simpa only [LSeriesHasSum, term_convolution'] using (hf.mul hg hsum).tsum_fiberwise _

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

Goal state before:

Tactic:
|(fract ξ)⁻¹ - v / u'| = |(fract ξ - u' / v) * (v / u' / fract ξ)| := by
      rw [abs_sub_comm]; congr 1; field
    _ = |fract ξ - u' / v| * (v / u' / fract ξ) := by rw [abs_mul, abs_of_pos H₁]
    _ < ((v : ℝ) * (2 * v - 1))⁻¹ * (v / u' / fract ξ) := by gcongr
    _ = (u' * ((2 * v - 1) * fract ξ))⁻¹ := by field
    _ ≤ (u' * (2 * u' - 1) : ℝ)⁻¹ := by gcongr

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

Goal state before:
pp: case zero
f : ℕ → ℂ
⊢ abscissaOfAbsConv (logMul^[0] f) = abscissaOfAbsConv f

Tactic:
simp

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

Goal state before:
pp: case zero
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
⊢ iteratedDeriv 0 (LSeries f) s = (-1) ^ 0 * LSeries (logMul^[0] f) s

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case a
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ -a ≤ |a|

Tactic:
apply neg_le_abs

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

Goal state before:
pp: a : ℝ
ha : 0 ≤ a
this :
  ∃ p,
    0 < p ∧
      (fun t ↦
          rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 +
            a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop]
        fun t ↦ rexp (-p * t)
⊢ ∃ p, 0 < p ∧ F_nat 1 a =O[atTop] fun t ↦ rexp (-p * t)

Tactic:
let ⟨p, hp, hp'⟩ := this
    refine ⟨p, hp, (Eventually.isBigO ?_).trans hp'⟩
    filter_upwards [eventually_gt_atTop 0] with t ht
    exact F_nat_one_le ha ht

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

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

Tactic:
simp

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

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

Tactic:
refine (Integrable.smul_const ?_ _).smul _

Goal state after:
case hg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
⊢ Integrable (fun x ↦ ↑x ^ (s - ↑P.k - 1)) (volume.restrict (Ioc 0 1))
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:
simp

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

Goal state before:
pp: case H
x z✝ : ℝ
⊢ evenKernel (-↑z✝) x = evenKernel (↑z✝) x

Tactic:
simp [← QuotientAddGroup.mk_neg, ← ofReal_inj, evenKernel_def, jacobiTheta₂_neg_left]

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
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
hc1 : MellinConvergent (fun x ↦ P.f x - P.f₀) s
hc2 : MellinConvergent P.f_modif s
hc3 : mellin (fun x ↦ P.f_modif x - P.f x + P.f₀) s = (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀
⊢ mellin (fun x ↦ P.f x - P.f₀) s = P.Λ s

Tactic:
have := (hasMellin_sub hc2 hc1).2

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
hc1 : MellinConvergent (fun x ↦ P.f x - P.f₀) s
hc2 : MellinConvergent P.f_modif s
hc3 : mellin (fun x ↦ P.f_modif x - P.f x + P.f₀) s = (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀
this : mellin (fun t ↦ P.f_modif t - (P.f t - P.f₀)) s = mellin P.f_modif s - mellin (fun x ↦ P.f x - P.f₀) s
⊢ mellin (fun x ↦ P.f x - P.f₀) s = P.Λ s
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:
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:
simp

Goal state after:
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
⊢ Tendsto (fun s ↦ (s - ↑P.k) • P.Λ₀ s) (𝓝 ↑P.k) (𝓝 0)

Tactic:
rw [(by simp : 𝓝 0 = 𝓝 ((P.k - P.k : ℂ) • P.Λ₀ P.k))]
    apply ((continuous_sub_right _).smul P.differentiable_Λ₀.continuous).tendsto

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:
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
⊢ 𝓝 (-P.f₀) = 𝓝 (0 • P.Λ₀ 0 - P.f₀ - 0)

Tactic:
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:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: a t : ℝ
ht : 0 < t
⊢ HasSum (fun n ↦ if n = 0 then 0 else cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t)))
    (↑(cosKernel (↑a) t) - 1)

Tactic:
simpa using hasSum_ite_sub_hasSum (hasSum_int_cosKernel a ht) 0

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

Goal state before:
pp: case inl
z τ : ℂ
hτ : τ.im ≤ 0
this : (-1 / τ).im ≤ 0
⊢ 0 = 1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)

Tactic:
jacobiTheta₂_undef _ this,

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: k : ℕ
hk : 2 ≤ k
hk2 : Even k
hkk : 1 < k
⊢ (0 ^ k)⁻¹ = 0

Tactic:
simp

Goal state after:
k : ℕ
hk : 2 ≤ k
hk2 : Even k
hkk : 1 < k
⊢ ¬k = 0
Module: Mathlib.NumberTheory.LSeries.RiemannZeta

Goal state before:
pp: case refine_1
⊢ {s | 1 < s.re} ⊆ {1}ᶜ

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: k : ℕ
m : ℕ := 2 ^ k.primesBelow.card
N₀ : ℕ := 2 * m ^ 2
hN₀ : N₀ = 2 * m ^ 2
S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, 1 / ↑p
this : 1 / 2 ≤ S
⊢ 4 = 2 ^ 2

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp [completedHurwitzZetaEven, div_mul_eq_mul_div, mul_div_assoc]

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

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

Tactic:
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:
simp

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

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

Tactic:
exact_mod_cast hx

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

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case inl
a : UnitAddCircle
s : ℂ
h : a ≠ 0 ∨ s ≠ 0
h' : s ≠ 0
⊢ Function.update (fun s ↦ completedHurwitzZetaEven a s / s.Gammaℝ) 0 (if a = 0 then -1 / 2 else 0) s =
    completedHurwitzZetaEven a s / s.Gammaℝ

Tactic:
rw [Function.update_of_ne h']

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

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

Goal state before:
pp: case e_a.e_a
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ 1 / (↑n + ↑a) ^ s = 1 / ↑(↑n + a) ^ s

Tactic:
simp

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

Goal state before:
pp: case e_a.e_a
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ 1 / (↑n + 1 - ↑a) ^ s = 1 / ↑(↑n + 1 - a) ^ s

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: s : ℂ
hs : s ≠ 0
⊢ ↑1 ^ (-s) = 1

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: s : ℂ
n : ℕ
χ : DirichletCharacter ℂ n
hs : s ≠ 0
⊢ χ ↑1 * ↑1 ^ (-s) = 1

Tactic:
simp

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

Goal state before:
pp: case inl
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n ↦
      ((s + 1).Gammaℝ * -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) +
            (s + 1).Gammaℝ * -I * -↑(↑n).sign * cexp (2 * ↑π * I * ↑a * -↑n)) /
          ↑n ^ s /
        2)
    (completedSinZeta (↑a) s)
⊢ (s + 1).Gammaℝ * ↑(Real.sin (2 * π * a * ↑0)) / ↑0 ^ s =
    ((s + 1).Gammaℝ * -I * ↑(↑0).sign * cexp (2 * ↑π * I * ↑a * ↑0) +
          (s + 1).Gammaℝ * -I * -↑(↑0).sign * cexp (2 * ↑π * I * ↑a * -↑0)) /
        2 /
      ↑0 ^ s

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: s : ℂ
hs : 1 < s.re
⊢ Tendsto (fun n ↦ ∏ p ∈ n.primesBelow, (1 - ↑p ^ (-s))⁻¹) atTop (𝓝 (riemannZeta s))

Tactic:
by
  rw [← tsum_riemannZetaSummand hs]
  apply eulerProduct_completely_multiplicative <| summable_riemannZetaSummand hs

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

Goal state before:
pp: a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
this : ∀ (b : ℝ), 0 ≤ b → ↑(SignType.sign (↑n + b)) / ↑|↑n + b| ^ s = 1 / (↑n + ↑b) ^ s
⊢ (1 / (↑n + ↑a) ^ s - 1 / (↑n + 1 - ↑a) ^ s) / 2 =
    (↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s - ↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s) / 2

Tactic:
by
    simp only [add_sub_assoc, this a ha.1, this (1 - a) (sub_nonneg.mpr ha.2), push_cast]

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

Goal state before:
pp: a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
b : ℝ
hb : 0 ≤ b
⊢ ↑n + ↑b = ↑(↑n + b)

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case neg
z : ℤ
k : ℕ
x0 y0 : ℤ
left✝ : 0 < k
h2 : x0.gcd y0 = 1
h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) z
h0 : ¬(x0 * ↑k).gcd (y0 * ↑k) = 0
⊢ ↑k ^ 2 ∣ z ^ 2

Tactic:
sq z,

Goal state after:
case neg
z : ℤ
k : ℕ
x0 y0 : ℤ
left✝ : 0 < k
h2 : x0.gcd y0 = 1
h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) z
h0 : ¬(x0 * ↑k).gcd (y0 * ↑k) = 0
⊢ ↑k ^ 2 ∣ z * z
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
⊢ χ ↑0 * ↑(Λ 0) / ↑(Real.log ↑0) = 0

Tactic:
simp

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

Goal state before:
pp: a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (a ^ 2) (b ^ 2) c
h2 : (a ^ 2).gcd (b ^ 2) = 1
ha22 : a ^ 2 % 2 = 1
m n : ℤ
ht1 : a ^ 2 = m ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * m * n
ht3 : c = m ^ 2 + n ^ 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : b ^ 2 ≠ 0
h4 : 0 < m
r s : ℤ
left✝ : a = r ^ 2 - s ^ 2
htt2 : n = 2 * r * s
htt3 : m = r ^ 2 + s ^ 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : m.gcd (r * s) = 1
b' : ℤ
hb2' : b = 2 * b'
⊢ 4 ≠ 0

Tactic:
simp

Goal state after: