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

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝⁷ : EuclideanDomain R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := bS.repr a
s_eq : ∀ (i : ι), s i = (bS.repr a) i
qs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i / b
rs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i % b
r_eq✝ : ∀ (j : Fin (cardM bS adm).succ) (i : ι), rs j i = μ j * s i % b
μ_eq : ∀ (i : ι) (j : Fin (cardM bS adm).succ), μ j * s i = b * qs j i + rs j i
μ_mul_a_eq : ∀ (j : Fin (cardM bS adm).succ), μ j • a = b • ∑ i, qs j i • bS i + ∑ i, rs j i • bS i
j k : Fin (adm.card ε ^ Fintype.card ι).succ
j_ne_k : j ≠ k
hjk : ∀ (k_1 : ι), ↑(abv (μ k * s k_1 % b - μ j * s k_1 % b)) < abv b • ε
hjk' : ∀ (i : ι), ↑(abv (rs k i - rs j i)) < abv b • ε
q : S := ∑ i, (qs k i - qs j i) • bS i
r : R := μ k - μ j
r_eq : r = μ k - μ j
this : r • a - b • q = ∑ x, (rs k x • bS x - rs j x • bS x)
⊢ abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))

Tactic:
rw [this, Algebra.norm_algebraMap_of_basis bS, abv.map_pow]

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝⁷ : EuclideanDomain R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := bS.repr a
s_eq : ∀ (i : ι), s i = (bS.repr a) i
qs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i / b
rs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i % b
r_eq✝ : ∀ (j : Fin (cardM bS adm).succ) (i : ι), rs j i = μ j * s i % b
μ_eq : ∀ (i : ι) (j : Fin (cardM bS adm).succ), μ j * s i = b * qs j i + rs j i
μ_mul_a_eq : ∀ (j : Fin (cardM bS adm).succ), μ j • a = b • ∑ i, qs j i • bS i + ∑ i, rs j i • bS i
j k : Fin (adm.card ε ^ Fintype.card ι).succ
j_ne_k : j ≠ k
hjk : ∀ (k_1 : ι), ↑(abv (μ k * s k_1 % b - μ j * s k_1 % b)) < abv b • ε
hjk' : ∀ (i : ι), ↑(abv (rs k i - rs j i)) < abv b • ε
q : S := ∑ i, (qs k i - qs j i) • bS i
r : R := μ k - μ j
r_eq : r = μ k - μ j
this : r • a - b • q = ∑ x, (rs k x • bS x - rs j x • bS x)
⊢ abv ((Algebra.norm R) (∑ x, (rs k x • bS x - rs j x • bS x))) < abv b ^ Fintype.card ι
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ ∃ c, ∀ᶠ (x : ℝ) in atTop, ‖ψ x - θ x‖ ≤ c * ‖√x‖

Tactic:
norm_eq_abs,

Goal state after:
⊢ ∃ c, ∀ᶠ (x : ℝ) in atTop, |ψ x - θ x| ≤ c * |√x|
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Fintype ι
b : ι → B
f : B ≃ₐ[A] C
⊢ discr A b = discr A (⇑f ∘ b)

Tactic:
discr_def

Goal state after:
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Fintype ι
b : ι → B
f : B ≃ₐ[A] C
⊢ (traceMatrix A b).det = discr A (⇑f ∘ b)
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: A : Type u
B : Type v
ι : Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype ι
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i, g i • b i = 0
i : ι
hi : g i ≠ 0
this : traceMatrix A b *ᵥ g = 0
h : ¬discr A b = 0
⊢ False

Tactic:
discr_def

Goal state after:
A : Type u
B : Type v
ι : Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype ι
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i, g i • b i = 0
i : ι
hi : g i ≠ 0
this : traceMatrix A b *ᵥ g = 0
h : ¬(traceMatrix A b).det = 0
⊢ False
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : Fintype ι
K : Type u
L : Type v
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Module.Finite K L
R : Type z
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
b : ι → L
h : ∀ (i : ι), IsIntegral R (b i)
⊢ IsIntegral R (discr K b)

Tactic:
discr_def

Goal state after:
ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : Fintype ι
K : Type u
L : Type v
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Module.Finite K L
R : Type z
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
b : ι → L
h : ∀ (i : ι), IsIntegral R (b i)
⊢ IsIntegral R (traceMatrix K b).det
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ yn a1 n
hp : n % m > 0
⊢ False

Tactic:
have co : Nat.Coprime (yn a1 m) (xn a1 (m * (n / m))) :=
          Nat.Coprime.symm <| (xy_coprime a1 _).coprime_dvd_right (y_mul_dvd a1 m (n / m))

Goal state after:
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ yn a1 n
hp : n % m > 0
co : (yn a1 m).Coprime (xn a1 (m * (n / m)))
⊢ False
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
hd : d ≤ 0
n : ℤ√d
⊢ 0 ≤ -(d * n.im * n.im)

Tactic:
rw [mul_assoc, neg_mul_eq_neg_mul]

Goal state after:
d : ℤ
hd : d ≤ 0
n : ℤ√d
⊢ 0 ≤ -d * (n.im * n.im)
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
this : { re := subNatNat x z, im := subNatNat w y }.Nonneg
⊢ { re := ↑x + -↑z, im := -↑y + ↑w }.Nonneg

Tactic:
neg_add_eq_sub

Goal state after:
d x y z w : ℕ
xy : { re := ↑x, im := -↑y }.Nonneg
zw : { re := -↑z, im := ↑w }.Nonneg
this : { re := subNatNat x z, im := subNatNat w y }.Nonneg
⊢ { re := ↑x + -↑z, im := ↑w - ↑y }.Nonneg
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case refl
a : ℕ
a1 : 1 < a
h : 2 = a
⊢ a = 2 ∧ 0 = 0

Tactic:
exact ⟨h.symm, rfl⟩

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 ^ k) / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1)) = ↑↑1 * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))

Tactic:
by rw [heven.neg_one_pow]; simp

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Duality

Goal state before:
pp: M : Type u_1
R : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommRing R
a : Mˣ
⊢ (∃ χ, χ ↑a ≠ 1) ↔ ∃ φ, φ a ≠ 1

Tactic:
refine ⟨fun ⟨χ, hχ⟩ ↦ ⟨χ.toUnitHom, ?_⟩, fun ⟨φ, hφ⟩ ↦ ⟨ofUnitHom φ, ?_⟩⟩

Goal state after:
case refine_1
M : Type u_1
R : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommRing R
a : Mˣ
x✝ : ∃ χ, χ ↑a ≠ 1
χ : MulChar M R
hχ : χ ↑a ≠ 1
⊢ χ.toUnitHom a ≠ 1

case refine_2
M : Type u_1
R : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommRing R
a : Mˣ
x✝ : ∃ φ, φ a ≠ 1
φ : Mˣ →* Rˣ
hφ : φ a ≠ 1
⊢ (ofUnitHom φ) ↑a ≠ 1
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
v : Fin2 n → ℕ
x : ℕ
⊢ ((x ::ₒ v) ∘ none :: some) ∈ S ↔ (x :: v) ∈ S

Tactic:
rw [show Option.elim' x v ∘ cons none some = x :: v from
          funext fun s => by rcases s with a | b <;> rfl]

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
hpm : ¬p ∣ m
| m

Tactic:
← prod_primeFactorsList hm₀

Goal state after:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
hpm : ¬p ∣ m
| m.primeFactorsList.prod
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
m : ℕ
hm₀ : m ≠ 0
hm : ∀ p_1 ∈ m.primeFactorsList, p_1 ∈ insert p s
| m

Tactic:
← prod_primeFactorsList hm₀

Goal state after:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
m : ℕ
hm₀ : m ≠ 0
hm : ∀ p_1 ∈ m.primeFactorsList, p_1 ∈ insert p s
| m.primeFactorsList.prod
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
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
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v

Tactic:
refine ⟨lt_of_le_of_ne' hu₀ fun hf => ?_, lt_of_le_of_ne hu₁ fun 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 (u - ⌊ξ⌋ * v) v
hf : u - ⌊ξ⌋ * v = 0
⊢ False

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
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 ∈ range N with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))

Tactic:
exact summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum hf₁ hmul hsum _

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

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ 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
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h : 2 * ↑u' - (1 + ↑u') / ↑v < (2 * ↑v - 1) * fract ξ
this : (2 * ↑v - 1) * (-(↑v * (2 * ↑v - 1))⁻¹ + ↑u' / ↑v) = 2 * ↑u' - (1 + ↑u') / ↑v
⊢ 2 * ↑u' - 1 ≤ 2 * ↑u' - (1 + ↑u') / ↑v

Tactic:
sub_le_sub_iff_left,

Goal state after:
ξ : ℝ
u v : ℤ
hv : 2 ≤ 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
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h : 2 * ↑u' - (1 + ↑u') / ↑v < (2 * ↑v - 1) * fract ξ
this : (2 * ↑v - 1) * (-(↑v * (2 * ↑v - 1))⁻¹ + ↑u' / ↑v) = 2 * ↑u' - (1 + ↑u') / ↑v
⊢ (1 + ↑u') / ↑v ≤ 1
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case e'_3
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.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ = ‖P.f x - (P.ε⁻¹ * ↑(x ^ P.k))⁻¹ • P.g₀‖

Tactic:
congr 3

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: k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ ‖↑n‖ ^ k * ‖rexp (-π * ((↑n + a) ^ 2 * t))‖ ≤
    |↑n| ^ k * rexp (-π * (t * ↑n ^ 2 - 2 * (|a| * (t * |↑n|))) + -π * (a ^ 2 * t))

Tactic:
norm_eq_abs,

Goal state after:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ |↑n| ^ k * |rexp (-π * ((↑n + a) ^ 2 * t))| ≤
    |↑n| ^ k * rexp (-π * (t * ↑n ^ 2 - 2 * (|a| * (t * |↑n|))) + -π * (a ^ 2 * t))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a t : ℝ
ht : 0 < t
this : Summable fun n ↦ ↑n ^ k * rexp (-π * (↑n + a) ^ 2 * t)
⊢ ∀ᶠ (i : ℕ) in atTop, ‖(↑i + a) ^ k‖ * ‖rexp (-π * (↑i + a) ^ 2 * t)‖ ≤ 2 ^ k * ↑i ^ k * rexp (-π * (↑i + a) ^ 2 * t)

Tactic:
norm_eq_abs,

Goal state after:
k : ℕ
a t : ℝ
ht : 0 < t
this : Summable fun n ↦ ↑n ^ k * rexp (-π * (↑n + a) ^ 2 * t)
⊢ ∀ᶠ (i : ℕ) in atTop, |(↑i + a) ^ k| * |rexp (-π * (↑i + a) ^ 2 * t)| ≤ 2 ^ k * ↑i ^ k * rexp (-π * (↑i + a) ^ 2 * 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
⊢ P.f (1 / x) - P.f₀ + 0 = (P.ε * ↑(x ^ P.k)) • (0 + (P.g x - (P.ε⁻¹ * ↑(x ^ (-P.k))) • P.f₀))

Tactic:
P.h_feq _ hx

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.ε * ↑(x ^ P.k)) • P.g x - P.f₀ + 0 = (P.ε * ↑(x ^ P.k)) • (0 + (P.g x - (P.ε⁻¹ * ↑(x ^ (-P.k))) • P.f₀))
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

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

Tactic:
indicator_of_mem (by grind),

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

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

Tactic:
indicator_of_mem (by grind),

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

Goal state before:
pp: z τ : ℂ
⊢ (starRingEnd ℂ) (jacobiTheta₂' z τ) = jacobiTheta₂' ((starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)

Tactic:
rw [← neg_inj, ← jacobiTheta₂'_neg_left, jacobiTheta₂', jacobiTheta₂', conj_tsum, ← tsum_neg]

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

Goal state before:
pp: case H
x a : ℝ
⊢ oddKernel (-↑a) x = -oddKernel (↑a) x

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

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

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

Tactic:
congr 3

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

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

Goal state before:
pp: a : UnitAddCircle
⊢ ∃ p, 0 < p ∧ (fun x ↦ cosKernel a x - 1) =O[atTop] fun x ↦ rexp (-p * x)

Tactic:
by
  induction a using QuotientAddGroup.induction_on with | H a =>
  obtain ⟨p, hp, hp'⟩ := HurwitzKernelBounds.isBigO_atTop_F_nat_zero_sub zero_le_one
  refine ⟨p, hp, (Eventually.isBigO ?_).trans (hp'.const_mul_left 2)⟩
  filter_upwards [eventually_gt_atTop 0] with t ht
  simp only [eq_false_intro one_ne_zero, if_false, sub_zero,
    ← (hasSum_nat_cosKernel₀ a ht).tsum_eq, HurwitzKernelBounds.F_nat]
  apply tsum_of_norm_bounded ((HurwitzKernelBounds.summable_f_nat 0 1 ht).hasSum.mul_left 2)
  intro n
  rw [norm_mul, norm_mul, norm_two, mul_assoc, mul_le_mul_iff_of_pos_left two_pos,
    norm_of_nonneg (exp_pos _).le, HurwitzKernelBounds.f_nat, pow_zero, one_mul, Real.norm_eq_abs]
  exact mul_le_of_le_one_left (exp_pos _).le (abs_cos_le_one _)

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

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
⊢ 1 / (-I * τ) ^ (1 / 2) * cexp (↑π * I * (-1 / τ) * z ^ 2) *
      ∑' (n : ℤ), cexp (2 * ↑π * I * ↑n * (z / τ) + ↑π * I * ↑n ^ 2 * (-1 / τ)) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) *
      ∑' (n : ℤ), cexp (2 * ↑π * I * ↑n * (z / τ) + ↑π * I * ↑n ^ 2 * (-1 / τ))

Tactic:
congr 3

Goal state after:
case e_a.e_a
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
⊢ ↑π * I * (-1 / τ) * z ^ 2 = -↑π * I * z ^ 2 / τ
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case refine_2
a : UnitAddCircle
s : ℂ
hs : s ≠ 0 ∨ a ≠ 0
hs' : s ≠ 1
⊢ s / 2 ≠ 1 / 2

Tactic:
exact hs' ∘ (div_left_inj' two_ne_zero).mp

Goal state after:
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))
⊢ (-if a = 0 then 1 else 0) = if a = 0 then -1 else 0

Tactic:
by { split_ifs <;> simp }

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
hF :
  ∀ (t : ℝ),
    0 < t →
      HasSum (fun n ↦ if ↑n + a = 0 then 0 else 1 / 2 * ↑(rexp (-π * (↑n + a) ^ 2 * t)))
        ((↑(evenKernel (↑a) t) - ↑(if ↑a = 0 then 1 else 0)) / 2)
⊢ completedHurwitzZetaEven (↑a) s = mellin (fun t ↦ ↑(evenKernel (↑a) t) - ↑(if ↑a = 0 then 1 else 0)) (s / 2) / 2

Tactic:
apply_ite ofReal,

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
hF :
  ∀ (t : ℝ),
    0 < t →
      HasSum (fun n ↦ if ↑n + a = 0 then 0 else 1 / 2 * ↑(rexp (-π * (↑n + a) ^ 2 * t)))
        ((↑(evenKernel (↑a) t) - ↑(if ↑a = 0 then 1 else 0)) / 2)
⊢ completedHurwitzZetaEven (↑a) s = mellin (fun t ↦ ↑(evenKernel (↑a) t) - if ↑a = 0 then ↑1 else ↑0) (s / 2) / 2
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)) - I * ↑n * cexp (2 * ↑π * ↑a * ↑n * I) =
    I * ↑n * cexp (-(2 * ↑π * I * ↑a * ↑n)) - I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n)

Tactic:
congr 3

Goal state after:
case e_a.e_a.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 : ℕ
⊢ -(2 * ↑π * ↑a * ↑n * I) = -(2 * ↑π * I * ↑a * ↑n)

case e_a.e_a.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 : ℕ
⊢ 2 * ↑π * ↑a * ↑n * I = 2 * ↑π * I * ↑a * ↑n
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ℝ

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

Tactic:
· rw [Function.update_of_ne h']

Goal state after:
case inr
a : UnitAddCircle
h : a ≠ 0 ∨ 0 ≠ 0
⊢ Function.update (fun s ↦ completedHurwitzZetaEven a s / s.Gammaℝ) 0 (if a = 0 then -1 / 2 else 0) 0 =
    completedHurwitzZetaEven a 0 / Gammaℝ 0
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaOdd a (1 - s) = completedSinZeta a s

Tactic:
completedHurwitzZetaOdd,

Goal state after:
a : UnitAddCircle
s : ℂ
⊢ (hurwitzOddFEPair a).Λ ((1 - s + 1) / 2) / 2 = completedSinZeta a s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case inr
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)
n : ℕ
h : n ≠ 0
⊢ (s + 1).Gammaℝ * ((cexp (-(2 * ↑π * ↑a * ↑n) * I) - cexp (2 * ↑π * ↑a * ↑n * I)) * I) / 2 / ↑n ^ s =
    (s + 1).Gammaℝ * (-I * 1 * cexp (2 * ↑π * I * ↑a * ↑n) + -I * -1 * cexp (2 * ↑π * I * ↑a * -↑n)) / 2 / ↑n ^ s

Tactic:
congr 3

Goal state after:
case inr.e_a.e_a.e_a
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)
n : ℕ
h : n ≠ 0
⊢ (cexp (-(2 * ↑π * ↑a * ↑n) * I) - cexp (2 * ↑π * ↑a * ↑n * I)) * I =
    -I * 1 * cexp (2 * ↑π * I * ↑a * ↑n) + -I * -1 * cexp (2 * ↑π * I * ↑a * -↑n)