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

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := ⋯
⊢ ∑ n ∈ Icc 0 ⌊x⌋₊, (log ↑n)⁻¹ * a n = θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)

Tactic:
sum_mul_eq_sub_integral_mul₁ a (f := fun n ↦ (log n)⁻¹) (by simp [a]) (by simp [a]),

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

case hf_diff
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
⊢ ∀ t ∈ Set.Icc 2 x, DifferentiableAt ℝ (fun n ↦ (log n)⁻¹) t

case hf_int
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
⊢ IntegrableOn (deriv fun n ↦ (log n)⁻¹) (Set.Icc 2 x) volume
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ n = 0 ∨ n = 1 ∨ 1 < n

Tactic:
lia

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

Goal state before:
pp: L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
g : L ≃+* L
inst✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
n : ℕ
⊢ (PadicInt.toZModPow n) (χ p g) = ↑((modularCyclotomicCharacter L ⋯) g)

Tactic:
toFun_apply

Goal state after:
L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
g : L ≃+* L
inst✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
n : ℕ
⊢ (PadicInt.toZModPow n) (PadicInt.ofIntSeq (fun n ↦ aux g (p ^ n)) ⋯) = ↑((modularCyclotomicCharacter L ⋯) g)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
ε : ℚ
hε : 0 < ε
j : ℕ
hj : j ≥ 1
⊢ j ≠ 0

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs

Goal state before:
pp: b : Basis (Fin 1) ℤ (𝓞 ℚ) := (Basis.singleton (Fin 1) ℤ).map ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm
⊢ (Algebra.trace ℤ (𝓞 ℚ)) ((↑ringOfIntegersEquiv).symm 1 * (↑ringOfIntegersEquiv).symm 1) = (Algebra.trace ℤ (𝓞 ℚ)) 1

Tactic:
show (AddEquiv.symm ↑ringOfIntegersEquiv) (1 : ℤ) = ringOfIntegersEquiv.symm 1 by rfl,

Goal state after:
b : Basis (Fin 1) ℤ (𝓞 ℚ) := (Basis.singleton (Fin 1) ℤ).map ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm
⊢ (Algebra.trace ℤ (𝓞 ℚ)) (ringOfIntegersEquiv.symm 1 * ringOfIntegersEquiv.symm 1) = (Algebra.trace ℤ (𝓞 ℚ)) 1
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
⊢ pellZd a1 (n + 1) = pellZd a1 n * { re := ↑a, im := 1 }

Tactic:
ext <;> simp

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

Goal state before:
pp: d : ℤ
a b : ℤ√d
⊢ star (a * b) = star b * star a

Tactic:
ext <;> simp

Goal state after:
case re
d : ℤ
a b : ℤ√d
⊢ a.re * b.re + d * a.im * b.im = b.re * a.re + d * b.im * a.im

case im
d : ℤ
a b : ℤ√d
⊢ -(a.im * b.re) + -(a.re * b.im) = -(b.re * a.im) + -(b.im * a.re)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d n : ℤ
⊢ ↑n = { re := n, im := 0 }

Tactic:
ext <;> simp

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

Goal state before:
pp: d : ℤ
n : ℕ
x y : ℤ
⊢ ↑n * { re := x, im := y } = { re := ↑n * x, im := ↑n * y }

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : Poly α
⊢ x✝ * 0 = 0

Tactic:
by ext; rw [mul_apply, zero_apply, mul_zero]

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

Goal state before:
pp: d n x y : ℤ
⊢ ↑n * { re := x, im := y } = { re := n * x, im := n * y }

Tactic:
ext <;> simp

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

Goal state before:
pp: d x y : ℤ
⊢ sqrtd * { re := x, im := y } = { re := d * y, im := x }

Tactic:
ext <;> simp

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

Goal state before:
pp: d : ℤ
⊢ sqrtd * sqrtd = ↑d

Tactic:
ext <;> simp

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

Goal state before:
pp: d n x y : ℤ
⊢ sqrtd * ↑n * { re := x, im := y } = { re := d * n * y, im := n * x }

Tactic:
ext <;> simp

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

Goal state before:
pp: d x y : ℤ
⊢ { re := x, im := y } = ↑x + sqrtd * ↑y

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case refine_2
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : γ → ℕ
ht : p ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) = 0
⊢ ∃ t, p (v ⊗ t) = 0

Tactic:
· have : v ⊗ t ∘ f = (v ⊗ t) ∘ (inl ⊗ inr ∘ f) := funext fun s => by rcases s with a | b <;> rfl
    exact ⟨t ∘ f, by rwa [this]⟩

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 + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
H :
  (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) * ↑p ^ p ^ k =
    ↑p ^ (p ^ k * (k.succ * (p - 1)).pred) * ↑p ^ p ^ k
hnorm : (Algebra.norm K) (ζ ^ p ^ k - 1) = ↑p ^ p ^ k
this✝ : 0 < k.succ * (p - 1)
h : ↑p ^ p ^ k = 0
this : ¬↑p ^ (k + 1) = 0
⊢ k + 1 ≠ 0

Tactic:
lia

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

Goal state before:
pp: d x y z w : ℕ
xy : { re := ↑x, im := -↑y }.Nonneg
zw : { re := -↑z, im := ↑w }.Nonneg
⊢ ({ re := ↑x, im := -↑y } + { re := -↑z, im := ↑w }).Nonneg

Tactic:
have : Nonneg ⟨Int.subNatNat x z, Int.subNatNat w y⟩ :=
    Int.subNatNat_elim x z
      (fun m n i => SqLe y d m 1 → SqLe n 1 w d → Nonneg ⟨i, Int.subNatNat w y⟩)
      (fun j k =>
        Int.subNatNat_elim w y
          (fun m n i => SqLe n d (k + j) 1 → SqLe k 1 m d → Nonneg ⟨Int.ofNat j, i⟩)
          (fun _ _ _ _ => trivial) fun m n xy zw => sqLe_cancel zw xy)
      (fun j k =>
        Int.subNatNat_elim w y
          (fun m n i => SqLe n d k 1 → SqLe (k + j + 1) 1 m d → Nonneg ⟨-[j+1], i⟩)
          (fun m n xy zw => sqLe_cancel xy zw) fun m n xy zw =>
          let t := Nat.le_trans zw (sqLe_of_le (Nat.le_add_right n (m + 1)) le_rfl xy)
          have : k + j + 1 ≤ k :=
            Nat.mul_self_le_mul_self_iff.1 (by simpa [one_mul] using t)
          absurd this (not_le_of_gt <| Nat.succ_le_succ <| Nat.le_add_right _ _))
      (nonnegg_pos_neg.1 xy) (nonnegg_neg_pos.1 zw)
  rw [add_def, neg_add_eq_sub]
  rwa [Int.subNatNat_eq_coe, Int.subNatNat_eq_coe] at this

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
⊢ ↑(yn a1 (n + 2) + yn a1 n) = ↑(2 * a * yn a1 (n + 1))

Tactic:
yn_succ_succ

Goal state after:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ ↑(2 * a * yn a1 (n + 1)) = ↑(2 * a * yn a1 (n + 1))
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
a : ℤ√↑d
n : ℕ
ha : a.Nonneg
x y : ℕ
x✝ : { re := ↑x, im := ↑y }.Nonneg
⊢ (↑↑n * { re := ↑x, im := ↑y }).Nonneg

Tactic:
rw [smul_val]; trivial

Goal state after:
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
⊢ 2 * n - k < n

Tactic:
lia

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

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
d : ℤ
f g : ℤ√d →+* R
h : f sqrtd = g sqrtd
⊢ f = g

Tactic:
ext ⟨re_x, im_x⟩

Goal state after:
R : Type u_1
inst✝ : NonAssocRing R
d : ℤ
f g : ℤ√d →+* R
h : f sqrtd = g sqrtd
re_x im_x : ℤ
⊢ f { re := re_x, im := im_x } = g { re := re_x, im := im_x }
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m ↦ ⌊fract (ξ * ↑m) * (↑n + 1)⌋
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)

Tactic:
have hn : 0 < (n : ℝ) + 1 := mod_cast Nat.succ_pos _

Goal state after:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m ↦ ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : j ≤ 2 * n
x✝¹ : a = 2
n1 : n = 1
x✝ : j = 0
i2 : i = 2
⊢ False

Tactic:
rw [n1, i2] at hin

Goal state after:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : 2 ≤ 1
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : j ≤ 2 * n
x✝¹ : a = 2
n1 : n = 1
x✝ : j = 0
i2 : i = 2
⊢ False
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : 2 * n < j
⊢ 4 * n - j ≤ 2 * n

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : 2 * n < j
j42n : 4 * n - j ≤ 2 * n
⊢ a = 2 → n = 1 → (i = 0 → 4 * n - j ≠ 2) ∧ (i = 2 → 4 * n - j ≠ 0)

Tactic:
lia

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

Goal state before:
pp: v : ℤ
hv : 0 < v
⊢ 0 < 2 * v - 1

Tactic:
lia

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

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

Tactic:
lia

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

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

Tactic:
lia

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

Goal state before:
pp: f : ℕ → ℂ
s : ℂ
hs : abscissaOfAbsConv f < ↑s.re
x : ℝ
hx₁ : abscissaOfAbsConv f < ↑x
hx₂ : ↑x < ↑s.re
⊢ x < s.re

Tactic:
simpa using hx₂

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
⊢ ↑a ≤ ↑a ^ 2 - (↑a - 1) ^ 2 - 1

Tactic:
lia

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

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

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

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n ↦ ‖f (p ^ n)‖
N : ℕ
⊢ (Summable fun m ↦ ‖f ↑m‖) ∧ HasSum (fun m ↦ f ↑m) (∏ p ∈ N.primesBelow, ∑' (n : ℕ), f (p ^ n))

Tactic:
rw [smoothNumbers_eq_factoredNumbers, primesBelow]

Goal state after:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n ↦ ‖f (p ^ n)‖
N : ℕ
⊢ (Summable fun m ↦ ‖f ↑m‖) ∧ HasSum (fun m ↦ f ↑m) (∏ p ∈ range N with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: n k : ℕ
hk : 0 < k
hn : 0 < n
w : ℕ := max n k
nw : n ≤ w
kw : k ≤ w
wpos : 0 < w
w1 : 1 < w + 1
a : ℕ := xn w1 w
a1 : 1 < a
na : n ≤ a
x : ℕ := xn a1 k
y : ℕ := yn a1 k
z : ℕ
ze : yn w1 w = w * z
t : ℕ
te : ↑t = 2 * ↑a * ↑n - ↑n * ↑n - 1
nt : ↑(n ^ k) < ↑t
tm : x ≡ y * (a - n) + n ^ k [MOD t]
⊢ 2 * ↑a * ↑n = ↑t + (↑n * ↑n + 1)

Tactic:
lia

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

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
N : ℕ
⊢ (Summable fun m ↦ ‖f ↑m‖) ∧ HasSum (fun m ↦ f ↑m) (∏ p ∈ N.primesBelow, (1 - f p)⁻¹)

Tactic:
rw [smoothNumbers_eq_factoredNumbers, primesBelow]

Goal state after:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
N : ℕ
⊢ (Summable fun m ↦ ‖f ↑m‖) ∧ HasSum (fun m ↦ f ↑m) (∏ p ∈ range N with Nat.Prime p, (1 - f p)⁻¹)
Module: Mathlib.NumberTheory.EulerProduct.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
hsum : Summable ⇑f
N : ℕ
⊢ ∏ p ∈ N.primesBelow, (1 - f p)⁻¹ = ∑' (m : ↑N.smoothNumbers), f ↑m

Tactic:
rw [smoothNumbers_eq_factoredNumbers, primesBelow]

Goal state after:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
hsum : Summable ⇑f
N : ℕ
⊢ ∏ p ∈ range N with Nat.Prime p, (1 - f p)⁻¹ = ∑' (m : ↑(factoredNumbers (range N))), f ↑m
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case e'_5.inl
ι : 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 : ι
hai : a i = 0
⊢ 0 * (Complex.Gamma s / ↑(p i) ^ s) = 0 * ∫ (a : ℝ) in Ioi 0, ↑a ^ (s - 1) * ↑(rexp (-p i * a)) ∂volume

Tactic:
zero_mul,

Goal state after:
case e'_5.inl
ι : 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 : ι
hai : a i = 0
⊢ 0 = 0 * ∫ (a : ℝ) in Ioi 0, ↑a ^ (s - 1) * ↑(rexp (-p i * a)) ∂volume
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) * (↑(rexp (-(p i * t))) * ↑(p i * t) ^ (s - 1)) = ↑t ^ (s - 1) * ↑(rexp (-p i * t))

Tactic:
mul_comm (↑(rexp _) : ℂ),

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

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

Tactic:
zero_mul,

Goal state after:
case e'_3
t : ℝ
ht : 0 < t
⊢ rexp 0 + ∑' (b : ℕ), f_nat 0 0 t (b + 1) - 1 = F_nat 0 1 t
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
⊢ mellin (fun x ↦ P.f_modif x - P.f x + P.f₀) s = (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀

Tactic:
have h_re1 : -1 < re (s - 1) := by simpa using P.hk.trans hs

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
h_re1 : -1 < (s - 1).re
⊢ mellin (fun x ↦ P.f_modif x - P.f x + P.f₀) s = (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a : ℝ
ha : a ≤ 1
t : ℝ
n : ℕ
⊢ f_int k a t (Int.negSucc n) = f_nat k (1 - a) t n

Tactic:
have : (Int.negSucc n) + a = -(n + (1 - a)) := by { push_cast; ring }

Goal state after:
k : ℕ
a : ℝ
ha : a ≤ 1
t : ℝ
n : ℕ
this : ↑(Int.negSucc n) + a = -(↑n + (1 - a))
⊢ f_int k a t (Int.negSucc n) = f_nat k (1 - a) t n
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

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

Tactic:
zero_mul,

Goal state after:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      cexp (2 * ↑π * I * ↑a * ↑↑(n + 1)) * ↑(rexp (-π * ↑↑(n + 1) ^ 2 * t)) +
        cexp (2 * ↑π * I * ↑a * ↑(-↑(n + 1))) * ↑(rexp (-π * ↑(-↑(n + 1)) ^ 2 * t)))
    (↑(cosKernel (↑a) t) + cexp 0 * ↑(rexp 0) - (cexp 0 * ↑(rexp 0) + cexp 0 * ↑(rexp 0)))
⊢ 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: a x : ℝ
hx : 0 < x
⊢ HasSum (fun n ↦ (↑n + a) * rexp (-π * (↑n + a) ^ 2 * x)) (oddKernel (↑a) x)

Tactic:
rw [← hasSum_ofReal, oddKernel_def' a x]
  have h1 := hasSum_jacobiTheta₂_term (a * I * x) (by rwa [I_mul_im, ofReal_re])
  have h2 := hasSum_jacobiTheta₂'_term (a * I * x) (by rwa [I_mul_im, ofReal_re])
  refine (((h2.div_const (2 * π * I)).add (h1.mul_left ↑a)).mul_left
    (cexp (-π * a ^ 2 * x))).congr_fun (fun n ↦ ?_)
  rw [jacobiTheta₂'_term, mul_assoc (2 * π * I), mul_div_cancel_left₀ _ two_pi_I_ne_zero, ← add_mul,
    mul_left_comm, jacobiTheta₂_term, ← Complex.exp_add]
  push_cast
  simp only [← mul_assoc, ← add_mul]
  congrm _ * cexp (?_ * x)
  simp only [mul_right_comm _ I, add_mul, mul_assoc _ I, I_mul_I]
  ring_nf

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

Goal state before:
pp: k : ℕ
hk : 2 ≤ k
hk2 : Even k
hkk : 1 < k
⊢ ¬k = 0

Tactic:
lia

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs' : s ≠ 1
this :
  DifferentiableAt ℂ
    (Function.update (fun s ↦ completedHurwitzZetaEven a s * s.Gammaℝ⁻¹) 0 (if a = 0 then -1 * 2⁻¹ else 0 * 2⁻¹)) s
⊢ DifferentiableAt ℂ (hurwitzZetaEven a) s

Tactic:
zero_mul,

Goal state after:
a : UnitAddCircle
s : ℂ
hs' : s ≠ 1
this :
  DifferentiableAt ℂ
    (Function.update (fun s ↦ completedHurwitzZetaEven a s * s.Gammaℝ⁻¹) 0 (if a = 0 then -1 * 2⁻¹ else 0)) s
⊢ DifferentiableAt ℂ (hurwitzZetaEven a) s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
this : DifferentiableAt ℂ (fun s ↦ completedHurwitzZetaEven a s / s.Gammaℝ - 1 / (s - 1) / s.Gammaℝ) 1
⊢ DifferentiableAt ℂ (fun s ↦ hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ) 1

Tactic:
apply this.congr_of_eventuallyEq
    filter_upwards [eventually_ne_nhds one_ne_zero] with x hx
    rw [hurwitzZetaEven, Function.update_of_ne hx]

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := ⋯
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n ↦ c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(sinKernel (↑a) t) / 2)
⊢ Summable fun i ↦ 1 / |↑i| ^ s.re

Tactic:
apply Summable.of_nat_of_neg <;>
    simpa

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

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

Tactic:
zero_mul,

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n ↦
      (s + 1).Gammaℝ * -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 +
        (s + 1).Gammaℝ * -I * ↑(-↑n).sign * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2)
    (completedSinZeta (↑a) s + 0 / ↑|0| ^ s / 2)
⊢ HasSum (fun n ↦ (s + 1).Gammaℝ * ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s) (completedSinZeta (↑a) s)
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: s : ℂ
hs : 1 < s.re
⊢ HasProd (fun p ↦ (1 - ↑↑p ^ (-s))⁻¹) (riemannZeta s)

Tactic:
← tsum_riemannZetaSummand hs

Goal state after:
s : ℂ
hs : 1 < s.re
⊢ HasProd (fun p ↦ (1 - ↑↑p ^ (-s))⁻¹) (∑' (n : ℕ), (riemannZetaSummandHom ⋯) n)
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:
← tsum_riemannZetaSummand hs

Goal state after:
s : ℂ
hs : 1 < s.re
⊢ Tendsto (fun n ↦ ∏ p ∈ n.primesBelow, (1 - ↑p ^ (-s))⁻¹) atTop (𝓝 (∑' (n : ℕ), (riemannZetaSummandHom ⋯) n))
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
inst✝ : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n
⊢ FermatLastTheoremWith R n

Tactic:
by
  intro a b c ha hb hc habc
  let s : Finset R := {a, b, c}; let d := s.gcd id
  obtain ⟨A, hA⟩ : d ∣ a := gcd_dvd (by simp [s])
  obtain ⟨B, hB⟩ : d ∣ b := gcd_dvd (by simp [s])
  obtain ⟨C, hC⟩ : d ∣ c := gcd_dvd (by simp [s])
  simp only [hA, hB, hC, mul_ne_zero_iff, mul_pow] at ha hb hc habc
  rw [← mul_add, mul_right_inj' (pow_ne_zero n ha.1)] at habc
  refine hn A B C ha.2 hb.2 hc.2 ?_ habc
  rw [← Finset.normalize_gcd, normalize_eq_one]
  refine isUnit_of_associated_mul ?_ ha.1
  grw [← Finset.gcd_mul_left', gcd_eq_gcd_image]
  refine .of_eq ?_; congr; simp [s, hA, hB, hC]

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

Goal state before:
pp: case pos
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this✝ : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
p : ℕ
h : Nat.Prime p
hp' : p ∣ N
this : ¬IsUnit ↑p
⊢ (1 - 0 * ↑p ^ (-s))⁻¹ = (1 - χ ↑p * ↑p ^ (-s))⁻¹ * (1 - χ ↑p * ↑p ^ (-s))

Tactic:
zero_mul,

Goal state after:
case pos
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this✝ : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
p : ℕ
h : Nat.Prime p
hp' : p ∣ N
this : ¬IsUnit ↑p
⊢ (1 - 0)⁻¹ = (1 - χ ↑p * ↑p ^ (-s))⁻¹ * (1 - χ ↑p * ↑p ^ (-s))
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
n : ℤ
h3 : a.gcd n = 1
hb20 : b ^ 2 ≠ 0
ht1 : a ^ 2 = 0 ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * 0 * n
ht3 : c = 0 ^ 2 + n ^ 2
ht4 : Int.gcd 0 n = 1
ht5 : 0 % 2 = 0 ∧ n % 2 = 1 ∨ 0 % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ 0
htt : PythagoreanTriple a n 0
⊢ False

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case h
x y z : ℤ
h : PythagoreanTriple x y z
m n : ℤ
H :
  (x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2) ∧
    m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
⊢ (x = 1 * (m ^ 2 - n ^ 2) ∧ y = 1 * (2 * m * n) ∨ x = 1 * (2 * m * n) ∧ y = 1 * (m ^ 2 - n ^ 2)) ∧ m.gcd n = 1

Tactic:
lia

Goal state after: