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

Goal state before:
pp: n : ℕ
⊢ bernoulli n = ∑ i ∈ range (n + 1), (monomial i) (_root_.bernoulli (n - i) * ↑(n.choose i))

Tactic:
by
  rw [← sum_range_reflect, add_succ_sub_one, add_zero, bernoulli]
  apply sum_congr rfl
  rintro x hx
  rw [mem_range_succ_iff] at hx
  rw [choose_symm hx, tsub_tsub_cancel_of_le hx]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
⊢ (↑n + 1) • bernoulli n = ↑((n + 1).choose n) • bernoulli n

Tactic:
choose_succ_self_right,

Goal state after:
n : ℕ
⊢ (↑n + 1) • bernoulli n = ↑(n + 1) • bernoulli n
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (1 + X) = bernoulli m + m • X ^ (m - 1)
⊢ (d + 2) • ∑ i ∈ range (d + 1), (d + 1).choose i • X ^ i =
    ∑ i ∈ range (d + 1), ((d + 2).choose (i + 1) * (i + 1)) • X ^ i

Tactic:
by
      simp_rw [smul_sum, smul_smul, ← add_one_mul_choose_eq (d + 1)]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
i : ℕ
hi : i ∈ range (n + 1)
⊢ (algebraMap ℚ A) (↑(n + 1)! * (1 / ↑i !) * (1 / ↑(n + 1 - i)!)) * (aeval t) (bernoulli i) =
    (algebraMap ℚ A) (↑(n + 1)! / (↑i ! * ↑(n + 1 - i)!)) * (aeval t) (bernoulli i)

Tactic:
field_simp

Goal state after:
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbs

Goal state before:
pp: n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
⊢ 0 < |b| • ε

Tactic:
rw [Algebra.smul_def]

Goal state after:
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
⊢ 0 < (algebraMap ℤ ℝ) |b| * ε
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ Monotone ψ

Tactic:
by
  intro x y hxy
  apply sum_le_sum_of_subset_of_nonneg
  · exact Ioc_subset_Ioc (by rfl) (by gcongr)
  · simp

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ.zero
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
ih : ∀ (m : ℕ), 0 < m → m < k → pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p)
hi : 0 + 1 < 2 * k
⊢ (Rat.padicValuation p) (-1 / 2 * (2 * ↑k + 1) * ↑p ^ (2 * k - 1) / (2 * ↑k + 1)) ≤ 1

Tactic:
field_simp

Goal state after:
case succ.zero
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
ih : ∀ (m : ℕ), 0 < m → m < k → pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p)
hi : 0 + 1 < 2 * k
⊢ (Rat.padicValuation p) (-(↑p ^ (2 * k - 1) / 2)) ≤ 1
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k p : ℕ
hk : 0 < k
hfilter : ∑ v ∈ Ico 1 p, ↑v ^ (2 * k) = ∑ v ∈ range p, ↑v ^ (2 * k)
⊢ ∑ x ∈ range (2 * k), bernoulli x * ↑((2 * k + 1).choose x) * ↑p ^ (2 * k + 1 - x) / (2 * ↑k + 1) +
      bernoulli (2 * k) * (2 * ↑k + 1) * ↑p ^ 1 / (2 * ↑k + 1) =
    ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k + 1 - i) / (2 * ↑k + 1) +
      ↑p * bernoulli (2 * k)

Tactic:
field_simp

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ (∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k + 1 - i) / (2 * ↑k + 1)) / ↑p =
    ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1)

Tactic:
have hp_ne : (p : ℚ) ≠ 0 := mod_cast (Fact.out : p.Prime).ne_zero

Goal state after:
k p : ℕ
inst✝ : Fact (Nat.Prime p)
hp_ne : ↑p ≠ 0
⊢ (∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k + 1 - i) / (2 * ↑k + 1)) / ↑p =
    ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ (∑ x ∈ Icc 1 N ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) with
      match x with
      | (k, p) => p ≤ ⌊x ^ (↑k)⁻¹⌋₊,
      match x with
      | (k, p) => f (p ^ k)) =
    ∑ k ∈ Icc 1 N, ∑ p ∈ Ioc 0 ⌊x ^ (1 / ↑k)⌋₊ with Nat.Prime p, f (p ^ k)

Tactic:
rw [sum_filter, sum_product]

Goal state after:
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ (∑ x_1 ∈ Icc 1 N,
      ∑ y ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime y,
        if
            match (x_1, y) with
            | (k, p) => p ≤ ⌊x ^ (↑k)⁻¹⌋₊ then
          match (x_1, y) with
          | (k, p) => f (p ^ k)
        else 0) =
    ∑ k ∈ Icc 1 N, ∑ p ∈ Ioc 0 ⌊x ^ (1 / ↑k)⌋₊ with Nat.Prime p, f (p ^ k)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
n m : ℕ
hnm : n ≤ m
hn : 1 ≤ n
hm : 1 ≤ m
h : 1 < x
⊢ (↑m)⁻¹ ≤ (↑n)⁻¹

Tactic:
field_simp

Goal state after:
x : ℝ
hx : 0 ≤ x
n m : ℕ
hnm : n ≤ m
hn : 1 ≤ n
hm : 1 ≤ m
h : 1 < x
⊢ ↑n ≤ ↑m
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
k : ℕ
ih : ∀ m < k, m > 0 → ¬p ∣ (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p).den
hk : k > 0
T : ℤ
hT :
  bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / ↑p =
    ↑T - ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1)
⊢ ¬p ∣ (↑T - ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1)).den

Tactic:
have hT_int : pIntegral p T := Int.padicValuation_le_one p T

Goal state after:
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
k : ℕ
ih : ∀ m < k, m > 0 → ¬p ∣ (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p).den
hk : k > 0
T : ℤ
hT :
  bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / ↑p =
    ↑T - ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1)
hT_int : pIntegral p ↑T
⊢ ¬p ∣ (↑T - ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1)).den
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ (fun x ↦ ↑(π ⌊x⌋₊) - θ x / log x) =O[atTop] fun x ↦ x / log x ^ 2

Tactic:
apply integral_theta_div_log_sq_isBigO.congr' _ (by rfl)
  filter_upwards [eventually_ge_atTop 2] with x hx
  rw [primeCounting_eq_theta_div_log_add_integral hx]
  simp

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 1 < x
this : 0 < log √x
⊢ ↑(π ⌊x⌋₊) ≤ log 4 * x / log √x + √x

Tactic:
field_simp

Goal state after:
x : ℝ
hx : 1 < x
this : 0 < log √x
⊢ ↑(π ⌊x⌋₊) * log √x ≤ log 4 * x + log √x * √x
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: case pos.refine_1
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk' : k ≠ 0
hk : ↑p ^ (-↑k) < ε
⊢ IsIntegral K (ζ k)

Tactic:
exact ((hζ k).isIntegral (Nat.pos_of_neZero _)).tower_top

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

Goal state before:
pp: case pos.refine_2
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk' : k ≠ 0
hk : ↑p ^ (-↑k) < ε
σ : Gal(L/K)
hσ : σ ∈ id ((fun g ↦ g.carrier) K⟮ζ k⟯.fixingSubgroup)
i : ℕ
hi : i < p ^ k
ht : ⋯.unit ^ i ∈ rootsOfUnity (p ^ k) L
⊢ p ^ k ≠ 1

Tactic:
· exact (one_lt_pow₀ ‹Fact p.Prime›.1.one_lt hk').ne'

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: d x y : ℤ
⊢ IsPell { re := x, im := y } ↔
    star { re := x, im := y } * { re := x, im := y } = 1 ∧ { re := x, im := y } * star { re := x, im := y } = 1

Tactic:
isPell_norm,

Goal state after:
d x y : ℤ
⊢ { re := x, im := y } * star { re := x, im := y } = 1 ↔
    star { re := x, im := y } * { re := x, im := y } = 1 ∧ { re := x, im := y } * star { re := x, im := y } = 1
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
b : ℤ√↑(d a1)
h1 : 1 ≤ b
hp : IsPell b
h : b ≤ pellZd a1 (n + 1)
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
ha : { re := ↑a, im := 1 } ≤ b
⊢ 1 ≤ b * { re := ↑a, im := -1 }

Tactic:
by rw [← a1m]; exact mul_le_mul_of_nonneg_right ha am1p

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case sub
α : Type u_1
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f f✝ g✝ : (α → ℕ) → ℤ
a✝¹ : IsPoly f✝
a✝ : IsPoly g✝
ihf : C ⟨f✝, a✝¹⟩
ihg : C ⟨g✝, a✝⟩
⊢ C ⟨fun x ↦ f✝ x - g✝ x, ⋯⟩

Tactic:
apply H3 _ _ ihf ihg

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

Goal state before:
pp: case inr.inl.inl.refine_2
d x y : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
z w : ℕ
hb : { re := ↑z, im := ↑w }.Nonneg
i : ℕ
h : { re := ↑x, im := -↑y }.im + { re := ↑z, im := ↑w }.im = -↑i
⊢ x ≤ x + z

Tactic:
· apply Nat.le_add_right

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

Goal state before:
pp: case inr.inr.inl.refine_2
d x y : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
z w : ℕ
hb : { re := ↑z, im := ↑w }.Nonneg
i : ℕ
h : { re := -↑x, im := ↑y }.re + { re := ↑z, im := ↑w }.re = -↑i
⊢ y ≤ y + w

Tactic:
· apply Nat.le_add_right

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
simp [_root_.pow_succ, mul_comm, mul_left_comm]
        ring

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

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

Tactic:
contrapose hφ
    simpa only [ofUnitHom_eq, equivToUnitHom_symm_coe, Units.val_eq_one] using hφ

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
ile,

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

Goal state before:
pp: α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, (Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0
t : Option β → ℕ
ht : p ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) = 0
⊢ p (t none ::ₒ v ⊗ t ∘ some) = 0

Tactic:
show (v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some) = t none ::ₒ v ⊗ t ∘ some from
                funext fun s => by rcases s with a | b <;> try { cases a <;> rfl }; rfl

Goal state after:
α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, (Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0
t : Option β → ℕ
ht : p (t none ::ₒ v ⊗ t ∘ some) = 0
⊢ p (t none ::ₒ v ⊗ t ∘ some) = 0
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a k x✝¹ y✝ : ℕ
x✝ : ∃ (a1 : 1 < a), xn a1 k = x✝¹ ∧ yn a1 k = y✝
a1 : 1 < a
hx : xn a1 k = x✝¹
hy : yn a1 k = y✝
kpos : k > 0
x : ℕ := xn a1 k
y : ℕ := yn a1 k
m : ℕ := 2 * (k * y)
u : ℕ := xn a1 m
v : ℕ := yn a1 m
ky : k ≤ y
yv : y * y ∣ v
uco : u.Coprime (4 * y)
b : ℕ
ba : b % u = a
bm1 : b ≡ 1 [MOD 4 * y]
m1 : 1 < m
vp : 0 < v
this✝ : xn a1 1 < u
this : a < u
⊢ b % u ≤ b

Tactic:
apply Nat.mod_le

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

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

Tactic:
cases a with

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case mpr
m n k : ℕ
⊢ k = 0 ∧ m = 1 ∨
      0 < k ∧
        (n = 0 ∧ m = 0 ∨
          0 < n ∧
            ∃ w a t z,
              ∃ (a1 : 1 < a),
                xn a1 k ≡ yn a1 k * (a - n) + m [MOD t] ∧
                  2 * a * n = t + (n * n + 1) ∧
                    m < t ∧ n ≤ w ∧ k ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1) →
    n ^ k = m

Tactic:
rintro (⟨rfl, rfl⟩ | ⟨hk0, ⟨rfl, rfl⟩ | ⟨hn0, w, a, t, z, a1, tm, ta, mt, nw, kw, zp⟩⟩)
    · exact _root_.pow_zero n
    · exact zero_pow hk0.ne'
    have hw0 : 0 < w := hn0.trans_le nw
    have hw1 : 1 < w + 1 := Nat.succ_lt_succ hw0
    rcases eq_pell hw1 zp with ⟨j, rfl, yj⟩
    have hj0 : 0 < j := by
      apply Nat.pos_of_ne_zero
      rintro rfl
      exact lt_irrefl 1 a1
    have wj : w ≤ j :=
      Nat.le_of_dvd hj0
        (modEq_zero_iff_dvd.1 <|
          (yn_modEq_a_sub_one hw1 j).symm.trans <| modEq_zero_iff_dvd.2 ⟨z, yj.symm⟩)
    have hnka : n ^ k < xn hw1 j := calc
      n ^ k ≤ n ^ j := Nat.pow_le_pow_right hn0 (le_trans kw wj)
      _ < (w + 1) ^ j := Nat.pow_lt_pow_left (Nat.lt_succ_of_le nw) hj0.ne'
      _ ≤ xn hw1 j := xn_ge_a_pow hw1 j
    have nt : (↑(n ^ k) : ℤ) < 2 * xn hw1 j * n - n * n - 1 :=
      eq_pow_of_pell_lem hn0.ne' hk0.ne' hnka
    have na : n ≤ xn hw1 j := (Nat.le_self_pow hk0.ne' _).trans hnka.le
    have te : (t : ℤ) = 2 * xn hw1 j * n - n * n - 1 := by
      rw [sub_sub, eq_sub_iff_add_eq]
      exact mod_cast ta.symm
    have : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + n ^ k [MOD t] := by
      apply modEq_of_dvd
      rw [te, Nat.cast_add, Nat.cast_mul, Int.ofNat_sub na]
      exact x_sub_y_dvd_pow a1 n k
    have : n ^ k % t = m % t := (this.symm.trans tm).add_left_cancel' _
    rw [← te] at nt
    rwa [Nat.mod_eq_of_lt (Nat.cast_lt.1 nt), Nat.mod_eq_of_lt mt] at this

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

Goal state before:
pp: case h
v : ℕ
ih : ∀ m < v, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u ↑v
⊢ ∃ n, ↑u / ↑v = ξ.convergent n

Tactic:
| h v ih =>

Goal state after:
case h
v : ℕ
ih : ∀ m < v, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u ↑v
⊢ ∃ n, ↑u / ↑v = ξ.convergent n
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case h.inr.inr
v : ℕ
ih : ∀ m < v, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u ↑v
ht : 1 < v
huv₀ : 0 < u - ⌊ξ⌋ * ↑v
huv₁ : u - ⌊ξ⌋ * ↑v < ↑v
Hv : ↑v ≠ 0
huv₁' : (u - ⌊ξ⌋ * ↑v).toNat < v
inv : ContfracLegendre.Ass (fract ξ)⁻¹ ↑v ↑(u - ⌊ξ⌋ * ↑v).toNat
n : ℕ
hn : ↑↑v / ↑(u - ⌊ξ⌋ * ↑v).toNat = (fract ξ)⁻¹.convergent n
⊢ ∃ n, ↑u / ↑v = ξ.convergent n

Tactic:
use n + 1

Goal state after:
case h
v : ℕ
ih : ∀ m < v, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u ↑v
ht : 1 < v
huv₀ : 0 < u - ⌊ξ⌋ * ↑v
huv₁ : u - ⌊ξ⌋ * ↑v < ↑v
Hv : ↑v ≠ 0
huv₁' : (u - ⌊ξ⌋ * ↑v).toNat < v
inv : ContfracLegendre.Ass (fract ξ)⁻¹ ↑v ↑(u - ⌊ξ⌋ * ↑v).toNat
n : ℕ
hn : ↑↑v / ↑(u - ⌊ξ⌋ * ↑v).toNat = (fract ξ)⁻¹.convergent n
⊢ ↑u / ↑v = ξ.convergent (n + 1)
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 (-x)) * ↑x ^ (s - 1)) (Ioi 0) volume
⊢ Integrable (fun t ↦ a i * (↑t ^ (s - 1) * ↑(rexp (-p i * t)))) (volume.restrict (Ioi 0))

Tactic:
← mul_zero (p i),

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 (-x)) * ↑x ^ (s - 1)) (Ioi (p i * 0)) volume
⊢ Integrable (fun t ↦ a i * (↑t ^ (s - 1) * ↑(rexp (-p i * t)))) (volume.restrict (Ioi 0))
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

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

Tactic:
indicator_of_mem (mem_Ioi.mpr hx'),

Goal state after:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : 1 < x
this : 1 / x < 1
⊢ P.f (1 / x) - (P.ε * ↑((1 / x) ^ (-P.k))) • P.g₀ =
    (P.ε * ↑(x ^ P.k)) • (P.g x - P.g₀ + (Ioo 0 1).indicator (fun x ↦ P.g x - (P.ε⁻¹ * ↑(x ^ (-P.k))) • P.f₀) x)
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hx : 0 < 1
⊢ P.f_modif (1 / 1) = (P.ε * ↑(1 ^ P.k)) • P.g_modif 1

Tactic:
simp [f_modif, g_modif]

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

Goal state before:
pp: case mp
z τ : ℂ
⊢ (Summable fun x ↦ jacobiTheta₂'_term x z τ) → Summable fun x ↦ jacobiTheta₂_term x z τ

Tactic:
refine fun h ↦ (h.norm.mul_left (2 * π)⁻¹).of_norm_bounded_eventually ?_

Goal state after:
case mp
z τ : ℂ
h : Summable fun x ↦ jacobiTheta₂'_term x z τ
⊢ ∀ᶠ (i : ℤ) in cofinite, ‖jacobiTheta₂_term i z τ‖ ≤ (2 * π)⁻¹ * ‖jacobiTheta₂'_term i z τ‖
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' : 1 < x
⊢ (Ioi 1).indicator (fun x ↦ P.f x - P.f₀) x + (Ioo 0 1).indicator (fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x -
        P.f x +
      P.f₀ =
    (Ioo 0 1).indicator (fun x ↦ P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x + {1}.indicator (fun x ↦ P.f₀ - P.f 1) x

Tactic:
indicator_of_mem (mem_Ioi.mpr 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' : 1 < x
⊢ P.f x - P.f₀ + (Ioo 0 1).indicator (fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x - P.f x + P.f₀ =
    (Ioo 0 1).indicator (fun x ↦ P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x + {1}.indicator (fun x ↦ P.f₀ - P.f 1) x
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))
⊢ HasSum (fun i ↦ ↑π ^ (-s) * Complex.Gamma s * a i / ↑(p i) ^ s) (mellin F s)

Tactic:
simp_rw [this] at hF

Goal state after:
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a' i * ↑(rexp (-π * p i * t))) (F t)
⊢ HasSum (fun i ↦ ↑π ^ (-s) * Complex.Gamma s * a i / ↑(p i) ^ s) (mellin F s)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
⊢ HasFDerivAt (fun p ↦ jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)

Tactic:
let f : ℤ → ℂ × ℂ → ℂ := fun n p ↦ jacobiTheta₂_term n p.1 p.2

Goal state after:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun n p ↦ jacobiTheta₂_term n p.1 p.2
⊢ HasFDerivAt (fun p ↦ jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : (fun t ↦ F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : (fun t ↦ F_nat 0 (1 - a) t) =O[atTop] fun t ↦ rexp (-q * t)
t : ℝ
ht : 0 < t
⊢ (F_int 0 (↑a) t - if a = 0 then 1 else 0) = (F_nat 0 a t - if a = 0 then 1 else 0) + F_nat 0 (1 - a) t

Tactic:
rw [F_int_eq_of_mem_Icc 0 (Ico_subset_Icc_self ha) ht]

Goal state after:
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : (fun t ↦ F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : (fun t ↦ F_nat 0 (1 - a) t) =O[atTop] fun t ↦ rexp (-q * t)
t : ℝ
ht : 0 < t
⊢ (F_nat 0 a t + F_nat 0 (1 - a) t - if a = 0 then 1 else 0) =
    (F_nat 0 a t - if a = 0 then 1 else 0) + F_nat 0 (1 - a) t
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case e'_6
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ ↑|r i| ^ s = ↑(r i ^ 2) ^ (s / 2)

Tactic:
rw [← sq_abs, ofReal_pow, ← cpow_nat_mul']

Goal state after:
case e'_6
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ ↑|r i| ^ s = ↑|r i| ^ (↑2 * (s / 2))

case e'_6.hlt
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ -π < ↑2 * (↑|r i|).arg

case e'_6.hle
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ ↑2 * (↑|r i|).arg ≤ π
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

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

Tactic:
field_simp

Goal state after:
case e_a.e_f
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
n : ℤ
⊢ (↑n + I ^ 2 * z) ^ 2 / τ = I ^ 2 * (-z ^ 2 + ↑n * (z * 2 + -↑n)) / τ
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: N k : ℕ
⊢ ↑(N.roughNumbersUpTo k).card ≤ ↑N * ∑ p ∈ N.succ.primesBelow \ k.primesBelow, 1 / ↑p

Tactic:
simp_rw [Finset.mul_sum, mul_one_div]

Goal state after:
N k : ℕ
⊢ ↑(N.roughNumbersUpTo k).card ≤ ∑ x ∈ N.succ.primesBelow \ k.primesBelow, ↑N / ↑x