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

Goal state before:
pp: 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 • ε
⊢ ∀ (i : ι), ↑(abv (rs k i - rs j i)) < abv b • ε

Tactic:
simpa only [r_eq] using hjk

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_2
⊢ (fun x ↦ 1 / log 2 ^ 2 * √x) =O[atTop] fun x ↦ x / log x ^ 2

Tactic:
apply IsBigO.const_mul_left sqrt_isLittleO.isBigO

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case ha
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ log √x

Tactic:
exact log_nonneg (one_le_sqrt.mpr hx)

Goal state after:
Module: Mathlib.RingTheory.Localization.NormTrace

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
M : Submonoid R
inst✝⁹ : IsLocalization M Rₘ
Sₘ : Type u_5
inst✝⁸ : CommRing Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
⊢ discr Rₘ ⇑(Basis.localizationLocalization Rₘ M Sₘ b) = (algebraMap R Rₘ) (discr R ⇑b)

Tactic:
by
  rw [Algebra.discr_def, Algebra.discr_def, RingHom.map_det,
    Algebra.traceMatrix_localizationLocalization]

Goal state after:
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
r : R
⊢ ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ n ≥ N, ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε

Tactic:
intro ε hε
  obtain ⟨ε', hε'0, hε'⟩ : ∃ v : ℚ, (0 : ℝ) < v ∧ ↑v < ε := exists_rat_btwn hε
  norm_cast at hε'0
  obtain ⟨N, hN⟩ := padicNormE.defn (nthHomSeq f_compat r) hε'0
  use N
  intro n hn
  apply _root_.lt_trans _ hε'
  change (padicNormE _ : ℝ) < _
  norm_cast
  exact hN _ hn

Goal state after:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: A : Type u
ι : Type w
inst✝² : DecidableEq ι
inst✝¹ : CommRing A
inst✝ : Fintype ι
b b' : Basis ι ℤ A
this : IsUnit (b'.toMatrix ⇑b).det
⊢ discr ℤ ⇑b' = (b'.toMatrix ⇑b).det ^ 2 * discr ℤ ⇑b'

Tactic:
by
      rw [Int.isUnit_iff, ← sq_eq_one_iff] at this
      rw [this, one_mul]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
x y : ℤ
h1 : 1 ≤ { re := x, im := y }
hp : IsPell { re := x, im := y }
h : { re := x, im := y } ≤ pellZd a1 (n + 1)
ha : ¬{ re := ↑a, im := 1 } ≤ { re := x, im := y }
h1l : 1 < { re := x, im := y }
bm : { re := x, im := y } * { re := { re := x, im := y }.re, im := -{ re := x, im := y }.im } = 1
y0l : 0 < { re := x - x, im := y - -y }
hn : { re := x, im := -y } ≤ { re := ↑a, im := -1 }
⊢ False

Tactic:
have t := mul_le_mul_of_nonneg_right
                      (mul_le_mul_of_nonneg_left hn (le_trans zero_le_one h1)) a1p
              rw [bm, one_mul, mul_assoc, Eq.trans (mul_comm _ _) a1m, mul_one] at t
              exact ha t

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

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

Tactic:
simpa [SqLe, mul_comm, mul_left_comm] using Nat.mul_le_mul_left d (nonnegg_pos_neg.1 ha)

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
⊢ xn a1 i % xn a1 n < xn a1 (j + 1) % xn a1 n

Tactic:
suffices xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n from
      (lt_or_eq_of_le (Nat.le_of_succ_le_succ ij)).elim
        (fun h => lt_trans (eq_of_xn_modEq_lem1 h (le_of_lt jn)) this) fun h => by
        rw [h]; exact this
    rw [Nat.mod_eq_of_lt (strictMono_x _ (Nat.lt_of_succ_lt jn)),
        Nat.mod_eq_of_lt (strictMono_x _ jn)]
    exact strictMono_x _ (Nat.lt_succ_self _)

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

Goal state before:
pp: case e'_3.e'_6
p : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (cyclotomic p K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
hζ' : IsPrimitiveRoot ζ (p ^ (0 + 1))
⊢ ↑p ^ (p - 2) = ↑p ^ (p - 1 - 1)

Tactic:
Nat.sub_sub

Goal state after:
case e'_3.e'_6
p : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (cyclotomic p K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
hζ' : IsPrimitiveRoot ζ (p ^ (0 + 1))
⊢ ↑p ^ (p - 2) = ↑p ^ (p - (1 + 1))
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case pos
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m ↦ ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
m : ℤ
hm : m ∈ D
hf : f m = ↑n
hf' : ↑↑n ≤ fract (ξ * ↑m) * (↑n + 1)
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |(ξ * ↑k - ↑j) * (↑n + 1)| ≤ 1

Tactic:
have hm₀ : 0 < m := by
      have hf₀ : f 0 = 0 := by
        simp only [f, cast_zero, mul_zero, fract_zero, zero_mul, floor_zero]
      refine Ne.lt_of_le (fun h => n_pos.ne ?_) (mem_Icc.mp hm).1
      exact mod_cast hf₀.symm.trans (h.symm ▸ hf : f 0 = n)

Goal state after:
case pos
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m ↦ ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
m : ℤ
hm : m ∈ D
hf : f m = ↑n
hf' : ↑↑n ≤ fract (ξ * ↑m) * (↑n + 1)
hm₀ : 0 < m
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |(ξ * ↑k - ↑j) * (↑n + 1)| ≤ 1
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case neg
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m ↦ ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
H : ∀ m ∈ D, f m ≠ ↑n
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |(ξ * ↑k - ↑j) * (↑n + 1)| ≤ 1

Tactic:
· have hD : #(Ico (0 : ℤ) n) < #D := by rw [card_Icc, card_Ico]; exact lt_add_one n
    have hfu' : ∀ m, f m ≤ n := fun m => lt_add_one_iff.mp (floor_lt.mpr (mod_cast hfu m))
    have hwd : ∀ m : ℤ, m ∈ D → f m ∈ Ico (0 : ℤ) n := fun x hx =>
      mem_Ico.mpr
        ⟨floor_nonneg.mpr (mul_nonneg (fract_nonneg (ξ * x)) hn.le), Ne.lt_of_le (H x hx) (hfu' x)⟩
    obtain ⟨x, hx, y, hy, x_lt_y, hxy⟩ : ∃ x ∈ D, ∃ y ∈ D, x < y ∧ f x = f y := by
      obtain ⟨x, hx, y, hy, x_ne_y, hxy⟩ := exists_ne_map_eq_of_card_lt_of_maps_to hD hwd
      rcases lt_trichotomy x y with (h | h | h)
      exacts [⟨x, hx, y, hy, h, hxy⟩, False.elim (x_ne_y h), ⟨y, hy, x, hx, h, hxy.symm⟩]
    refine
      ⟨⌊ξ * y⌋ - ⌊ξ * x⌋, y - x, sub_pos_of_lt x_lt_y,
        sub_le_iff_le_add.mpr <| le_add_of_le_of_nonneg (mem_Icc.mp hy).2 (mem_Icc.mp hx).1, ?_⟩
    convert_to! |fract (ξ * y) * (n + 1) - fract (ξ * x) * (n + 1)| ≤ 1
    · congr; push_cast; simp only [fract]; ring
    exact (abs_sub_lt_one_of_floor_eq_floor hxy.symm).le

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

Goal state before:
pp: ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < ↑k.toNat
hk₁ : ↑k.toNat ≤ ↑n
h : |↑↑k.toNat * ξ - ↑j| ≤ 1 / (↑n + 1)
hk : ↑k.toNat = k
⊢ ∃ k, 0 < k ∧ k ≤ n ∧ |↑k * ξ - ↑(round (↑k * ξ))| ≤ 1 / (↑n + 1)

Tactic:
exact ⟨k.toNat, natCast_pos.mp hk₀, Nat.cast_le.mp hk₁, (round_le (↑k.toNat * ξ) j).trans h⟩

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

Goal state before:
pp: ξ : ℝ
n : ℕ
n_pos : 0 < n
⊢ ∃ k, 0 < k ∧ k ≤ n ∧ |↑k * ξ - ↑(round (↑k * ξ))| ≤ 1 / (↑n + 1)

Tactic:
by
  obtain ⟨j, k, hk₀, hk₁, h⟩ := exists_int_int_abs_mul_sub_le ξ n_pos
  have hk := toNat_of_nonneg hk₀.le
  rw [← hk] at hk₀ hk₁ h
  exact ⟨k.toNat, natCast_pos.mp hk₀, Nat.cast_le.mp hk₁, (round_le (↑k.toNat * ξ) j).trans h⟩

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)
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
o : j = n ∨ n < j
jn✝ : j > n
jn : j ≠ n
s : xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
h : i = j
⊢ xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n

Tactic:
exact s

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

Goal state before:
pp: case left
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den
⊢ q.den ≤ ξ.den

Tactic:
rcases eq_or_ne ξ q with (rfl | H)
    · exact le_rfl
    · have hξ₀ : (0 : ℚ) < ξ.den := Nat.cast_pos.mpr ξ.pos
      rw [← Rat.num_div_den ξ, div_mul_eq_mul_div, div_sub' hξ₀.ne', abs_div, abs_of_pos hξ₀,
        div_lt_iff₀ hξ₀, div_mul_comm, mul_one] at h
      refine Nat.cast_le.mp ((one_lt_div hq₀).mp <| lt_of_le_of_lt ?_ h).le
      norm_cast
      rw [mul_comm _ q.num]
      exact Int.one_le_abs (sub_ne_zero_of_ne <| mt Rat.eq_iff_mul_eq_mul.mpr H)

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

Goal state before:
pp: case inr
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
hp₁ : p.1 ≠ 0
hp₂ : p.2 ≠ 0
⊢ f p.1 * g p.2 / ↑n ^ s = f p.1 * g p.2 / ↑(p.1 * p.2) ^ s

Tactic:
(mem_divisorsAntidiagonal.mp hp).1

Goal state after:
case inr
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
hp₁ : p.1 ≠ 0
hp₂ : p.2 ≠ 0
⊢ f p.1 * g p.2 / ↑n ^ s = f p.1 * g p.2 / ↑n ^ s
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

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

Tactic:
simp_rw [← ofReal_mul, ← ofReal_neg, ← ofReal_exp, ← neg_mul (p i)] at this

Goal state after:
case e'_5.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 : ∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) * ↑(rexp (-p i * t)) = (1 / ↑(p i)) ^ s * Complex.Gamma s
⊢ a i * (Complex.Gamma s / ↑(p i) ^ s) = a i * ∫ (a : ℝ) in Ioi 0, ↑a ^ (s - 1) * ↑(rexp (-p i * a)) ∂volume
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

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

Tactic:
mul_le_mul_iff_right₀ two_pos,

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

Goal state before:
pp: S T : ℝ
hT : 0 < T
k : ℕ
⊢ (fun n ↦ ↑n ^ k * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑n))) =O[atTop] fun n ↦ ↑n ^ k * rexp (-1 * ↑n)

Tactic:
apply IsBigO.mul (isBigO_refl _ _)

Goal state after:
S T : ℝ
hT : 0 < T
k : ℕ
⊢ (fun x ↦ rexp (-π * (T * ↑x ^ 2 - 2 * S * ↑x))) =O[atTop] fun x ↦ rexp (-1 * ↑x)
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
⊢ P.f_modif (1 / x) = (P.ε * ↑(x ^ P.k)) • P.g_modif x

Tactic:
have : 1 < 1 / x := by rwa [lt_one_div one_pos hx, div_one]
    rw [f_modif, Pi.add_apply, indicator_of_mem (mem_Ioi.mpr this),
      indicator_of_notMem (notMem_Ioo_of_ge this.le), g_modif, Pi.add_apply,
      indicator_of_notMem (notMem_Ioi.mpr hx'.le),
      indicator_of_mem (mem_Ioo.mpr ⟨hx, hx'⟩), P.h_feq _ hx]
    simp_rw [rpow_neg hx.le]
    match_scalars <;> field [(rpow_pos_of_pos hx P.k).ne', P.hε]

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

Goal state before:
pp: case mpr
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ 2 * π * 1 * ‖↑n‖ = 2 * π * ↑|n|

Tactic:
norm_intCast,

Goal state after:
case mpr
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ 2 * π * 1 * |↑n| = 2 * π * ↑|n|
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
⊢ Tendsto (fun s ↦ (s - ↑P.k) • (1 / s) • P.f₀) (𝓝 ↑P.k) (𝓝 0)

Tactic:
(by simp : 𝓝 0 = 𝓝 ((P.k - P.k : ℂ) • (1 / P.k : ℂ) • P.f₀))

Goal state after:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun s ↦ (s - ↑P.k) • (1 / s) • P.f₀) (𝓝 ↑P.k) (𝓝 ((↑P.k - ↑P.k) • (1 / ↑P.k) • P.f₀))
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
h3 : 1 / (-I * (I * ↑x)) ^ (1 / 2) = 1 / ↑(x ^ (1 / 2))
⊢ -↑π * I * (↑a * I * ↑x) ^ 2 / (I * ↑x) = -(-↑π * ↑a ^ 2 * ↑x)

Tactic:
rw [mul_pow, mul_pow, I_sq, div_eq_iff hx']

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
h3 : 1 / (-I * (I * ↑x)) ^ (1 / 2) = 1 / ↑(x ^ (1 / 2))
⊢ -↑π * I * (↑a ^ 2 * -1 * ↑x ^ 2) = -(-↑π * ↑a ^ 2 * ↑x) * (I * ↑x)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
n : ℤ
⊢ cexp (↑π * I * ↑n ^ 2 * 2) = 1

Tactic:
rw [(by push_cast; ring : (π * I * n ^ 2 * 2 : ℂ) = (n ^ 2 :) * (2 * π * I)), exp_int_mul,
    exp_two_pi_mul_I, one_zpow]

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)) * jacobiTheta₂ (↑a) (-1 / (I * ↑x)) = ↑1 / ↑(x ^ (1 / 2)) * jacobiTheta₂ (↑a) (-1 / (I * ↑x))

Tactic:
ofReal_one

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)) * jacobiTheta₂ (↑a) (-1 / (I * ↑x)) = 1 / ↑(x ^ (1 / 2)) * jacobiTheta₂ (↑a) (-1 / (I * ↑x))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
⊢ (starRingEnd ℂ) (∑' (n : ℤ), jacobiTheta₂_term n (-z) τ) = jacobiTheta₂ ((starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)

Tactic:
conj_tsum

Goal state after:
z τ : ℂ
⊢ ∑' (a : ℤ), (starRingEnd ℂ) (jacobiTheta₂_term a (-z) τ) = jacobiTheta₂ ((starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
⊢ ∑' (a : ℤ), (starRingEnd ℂ) (jacobiTheta₂_term a (-z) τ) = jacobiTheta₂ ((starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)

Tactic:
congr 2 with n

Goal state after:
case e_f
z τ : ℂ
n : ℤ
⊢ (starRingEnd ℂ) (jacobiTheta₂_term n (-z) τ) = jacobiTheta₂_term n ((starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

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

Tactic:
ofReal_one

Goal state after:
a t : ℝ
ht : 0 < t
⊢ HasSum (fun x ↦ ↑(2 * Real.cos (2 * π * a * (↑x + 1)) * rexp (-π * (↑x + 1) ^ 2 * t))) (↑(cosKernel (↑a) t) - 1)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
⊢ -∑' (a : ℤ), (starRingEnd ℂ) (jacobiTheta₂'_term a z τ) =
    ∑' (n : ℤ), jacobiTheta₂'_term n (-(starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)

Tactic:
← 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: x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * ↑(1 / x)) = I * ↑x
⊢ ↑1 / ↑x = 1 / ↑x

Tactic:
ofReal_one

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

Goal state before:
pp: s : ℂ
⊢ completedCosZeta₀ 0 s = completedRiemannZeta₀ s

Tactic:
completedRiemannZeta₀,

Goal state after:
s : ℂ
⊢ completedCosZeta₀ 0 s = completedHurwitzZetaEven₀ 0 s
Module: Mathlib.NumberTheory.LSeries.RiemannZeta

Goal state before:
pp: s : ℂ
⊢ completedHurwitzZetaEven 0 s = completedRiemannZeta₀ s - 1 / s - 1 / (1 - s)

Tactic:
completedRiemannZeta₀,

Goal state after:
s : ℂ
⊢ completedHurwitzZetaEven 0 s = completedHurwitzZetaEven₀ 0 s - 1 / s - 1 / (1 - s)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ (hurwitzEvenFEPair a).Λ (1 / 2 - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2

Tactic:
(by simp : (1 / 2 : ℂ) = ↑(1 / 2 : ℝ)),

Goal state after:
a : UnitAddCircle
s : ℂ
⊢ (hurwitzEvenFEPair a).Λ (↑(1 / 2) - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ (s / 2) / 2
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ (hurwitzEvenFEPair a).Λ₀ (1 / 2 - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2

Tactic:
(by simp : (1 / 2 : ℂ) = ↑(1 / 2 : ℝ)),

Goal state after:
a : UnitAddCircle
s : ℂ
⊢ (hurwitzEvenFEPair a).Λ₀ (↑(1 / 2) - s / 2) / 2 = (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
Module: Mathlib.NumberTheory.LSeries.RiemannZeta

Goal state before:
pp: ⊢ Tendsto (fun x ↦ ↑((x - 1) * ∑' (n : ℕ), 1 / ↑n ^ x)) (𝓝[>] 1) (𝓝 ↑1)

Tactic:
ofReal_one

Goal state after:
⊢ Tendsto (fun x ↦ ↑((x - 1) * ∑' (n : ℕ), 1 / ↑n ^ x)) (𝓝[>] 1) (𝓝 1)
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
f : ℕ → M
⊢ ∏' (p : Primes), f ↑p = tprod ({n | Prime n}.mulIndicator f)

Tactic:
exact tprod_subtype {n | n.Prime} f

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

Goal state before:
pp: case pos
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun n ↦ χ ↑n) 1
n : ℕ
h₁ : ↑n = 1
h₂ : n = 0
⊢ 1 / ↑n ≤ 0

pp: case neg
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun n ↦ χ ↑n) 1
n : ℕ
h₁ : ↑n = 1
h₂ : ¬n = 0
⊢ 1 / ↑n ≤ ‖χ ↑n‖ / ↑n ^ re 1

pp: case pos
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun n ↦ χ ↑n) 1
n : ℕ
h₁ : ¬↑n = 1
h✝ : n = 0
⊢ 0 ≤ 0

pp: case neg
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun n ↦ χ ↑n) 1
n : ℕ
h₁ : ¬↑n = 1
h✝ : ¬n = 0
⊢ 0 ≤ ‖χ ↑n‖ / ↑n ^ re 1

Tactic:
· simp [h₂]

Goal state after:
case neg
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun n ↦ χ ↑n) 1
n : ℕ
h₁ : ↑n = 1
h₂ : ¬n = 0
⊢ 1 / ↑n ≤ ‖χ ↑n‖ / ↑n ^ re 1

case pos
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun n ↦ χ ↑n) 1
n : ℕ
h₁ : ¬↑n = 1
h✝ : n = 0
⊢ 0 ≤ 0

case neg
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun n ↦ χ ↑n) 1
n : ℕ
h₁ : ¬↑n = 1
h✝ : ¬n = 0
⊢ 0 ≤ ‖χ ↑n‖ / ↑n ^ re 1
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case refine_1
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)
⊢ Summable fun i ↦ ‖1 / 2‖ / |↑i + a| ^ s.re

Tactic:
simp_rw [← mul_one_div ‖_‖]

Goal state after:
case refine_1
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)
⊢ Summable fun i ↦ ‖1 / 2‖ * (1 / |↑i + a| ^ s.re)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs' : s ≠ 1
⊢ DifferentiableAt ℂ (hurwitzZetaEven a) s

Tactic:
by
  have := differentiableAt_update_of_residue
    (fun t ht ht' ↦ differentiableAt_completedHurwitzZetaEven a (Or.inl ht) ht')
    (completedHurwitzZetaEven_residue_zero a) s hs'
  simp_rw [div_eq_mul_inv, ite_mul, zero_mul, ← div_eq_mul_inv] at this
  exact this

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
⊢ hurwitzZetaEven a (1 - s) = completedHurwitzZetaEven a (1 - s) * (1 - s).Gammaℝ⁻¹

Tactic:
hurwitzZetaEven_def_of_ne_or_ne,

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
⊢ completedHurwitzZetaEven a (1 - s) / (1 - s).Gammaℝ = completedHurwitzZetaEven a (1 - s) * (1 - s).Gammaℝ⁻¹

a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
⊢ a ≠ 0 ∨ 1 - s ≠ 0
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
⊢ ↑2 ∣ b ^ 2

Tactic:
rw [ht2, mul_assoc]

Goal state after:
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
⊢ ↑2 ∣ 2 * (m * n)
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
hc : IsRelPrime a b
⊢ Disjoint (primeFactors a) (primeFactors b)

Tactic:
by
  classical
  exact Multiset.disjoint_toFinset.mpr (disjoint_normalizedFactors hc)

Goal state after: