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

Goal state before:
pp: n : ℕ
⊢ ∑ k ∈ range n, ↑(n.choose k) * bernoulli' k = ↑n

Tactic:
by
  cases n with | zero => simp | succ n =>
  suffices
    ((n + 1 : ℚ) * ∑ k ∈ range n, ↑(n.choose k) / (n - k + 1) * bernoulli' k) =
      ∑ x ∈ range n, ↑(n.succ.choose x) * bernoulli' x by
    rw_mod_cast [sum_range_succ, bernoulli'_def, ← this, choose_succ_self_right]
    ring
  simp_rw [mul_sum, ← mul_assoc]
  refine sum_congr rfl fun k hk => ?_
  congr
  have : ((n - k : ℕ) : ℚ) + 1 ≠ 0 := by norm_cast
  simp only [← cast_sub (mem_range.1 hk).le, succ_eq_add_one, field, mul_comm]
  rw_mod_cast [tsub_add_eq_add_tsub (mem_range.1 hk).le, choose_mul_succ_eq]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n p : ℕ
⊢ ∑ k ∈ Ico 1 (n + 1), ↑k ^ p = ∑ i ∈ range (p + 1), bernoulli' i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1)

Tactic:
← Nat.cast_succ

Goal state after:
n p : ℕ
⊢ ∑ k ∈ Ico 1 (n + 1), ↑k ^ p = ∑ i ∈ range (p + 1), bernoulli' i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑p.succ
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n p : ℕ
f : ℕ → ℚ := fun i ↦ bernoulli i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
f' : ℕ → ℚ := fun i ↦ bernoulli' i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
hle : 1 ≤ n + 1
hne : ↑p + 1 + 1 ≠ 0
h1 : ∀ (r : ℚ), r * (↑p + 1 + 1) * ↑n ^ p.succ / (↑p + 1 + 1) = r * ↑n ^ p.succ
⊢ f 1 + ↑n ^ p.succ = 1 / 2 * ↑n ^ p.succ

Tactic:
simp_rw [f, bernoulli_one, choose_one_right, succ_sub_succ_eq_sub, cast_succ, tsub_zero, h1]

Goal state after:
n p : ℕ
f : ℕ → ℚ := fun i ↦ bernoulli i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
f' : ℕ → ℚ := fun i ↦ bernoulli' i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
hle : 1 ≤ n + 1
hne : ↑p + 1 + 1 ≠ 0
h1 : ∀ (r : ℚ), r * (↑p + 1 + 1) * ↑n ^ p.succ / (↑p + 1 + 1) = r * ↑n ^ p.succ
⊢ -1 / 2 * ↑n ^ p.succ + ↑n ^ p.succ = 1 / 2 * ↑n ^ p.succ
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: case inr
n : ℕ
hn0 : n ≠ 0
⊢ n < 2 → ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n

Tactic:
exact fun h2 => ⟨2, prime_two, h2, Nat.mul_le_mul_left 2 (Nat.pos_of_ne_zero hn0)⟩

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (deriv fun t ↦ ‖f t‖) (Set.Ici 1) volume
h_bdd : (fun n ↦ ‖f ↑n‖ * ∑ k ∈ Icc 1 n, ‖c k‖) =O[atTop] fun x ↦ 1
g : ℝ → ℝ
hg₁ : (fun t ↦ deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 1 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
n : ℕ
⊢ ∑ k ∈ Icc 1 n, ‖c k‖ = ∑ x ∈ Icc 1 n, ‖if x = 0 then 0 else c x‖

Tactic:
exact Finset.sum_congr rfl fun _ h ↦ by rw [if_neg (zero_lt_one.trans_le (mem_Icc.mp h).1).ne']

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_1
n p : ℕ
hp : Prime p
this : 1 < p
⊢ ∀ (b : ℕ), 1 ≤ b → b ≤ n → (id b).factorization p ≤ log p n

Tactic:
exact fun m _ h ↦ le_log_of_pow_le this (le_of_dvd (by grind) (ordProj_dvd m p) |>.trans h)

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n p : ℕ
⊢ p ∈ n.lcmUpto.primeFactors ↔ p ∈ n.primesLE

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
n p : ℕ
h : p ∈ n.lcmUpto.primeFactors
⊢ p ∈ n.primesLE

case refine_2
n p : ℕ
h : p ∈ n.primesLE
⊢ p ∈ n.lcmUpto.primeFactors
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_1
n p : ℕ
h : p ∈ n.lcmUpto.primeFactors
this : Prime p
⊢ p ∈ n.primesLE

Tactic:
← support_factorization,

Goal state after:
case refine_1
n p : ℕ
h : p ∈ n.lcmUpto.factorization.support
this : Prime p
⊢ p ∈ n.primesLE
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ ∑ p ∈ Icc 1 n with Nat.Prime p, ∑ q ∈ image (fun k ↦ p ^ k) (Icc 1 (Nat.log p n)), Λ q =
    ∑ p ∈ n.primesLE, ∑ k ∈ Icc 1 (Nat.log p n), Λ (p ^ k)

Tactic:
refine sum_congr (primesLE_eq_filter_Icc_one n).symm fun p hp ↦ ?_

Goal state after:
n p : ℕ
hp : p ∈ n.primesLE
⊢ ∑ q ∈ image (fun k ↦ p ^ k) (Icc 1 (Nat.log p n)), Λ q = ∑ k ∈ Icc 1 (Nat.log p n), Λ (p ^ k)
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]
hbε : 0 < cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : A i₁ % b = A i₀ % b
⊢ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε

Tactic:
rwa [h, sub_self, map_zero, Int.cast_zero]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n k : ℕ
hkn : k ≤ n
⊢ ∀ (p : ℕ), Nat.Prime p → (n.choose k).factorization p ≤ n.lcmUpto.factorization p

Tactic:
intro p

Goal state after:
n k : ℕ
hkn : k ≤ n
p : ℕ
⊢ Nat.Prime p → (n.choose k).factorization p ≤ n.lcmUpto.factorization p
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ.succ.inr
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)
i : ℕ
hi : i + 1 + 1 < 2 * k
hodd : Odd (i + 2)
⊢ (Rat.padicValuation p)
      (bernoulli (i + 1 + 1) * ↑((2 * k + 1).choose (i + 1 + 1)) * ↑p ^ (2 * k - (i + 1 + 1)) / (2 * ↑k + 1)) ≤
    1

Tactic:
simp [bernoulli_eq_zero_of_odd hodd (by lia)]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ ↑⌊log x / log 2⌋₊ ≤ log x / log 2

Tactic:
· exact floor_le (by bound)

Goal state after:
Module: Mathlib.NumberTheory.FunctionField

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F[X] K
inst✝¹ : Algebra F⟮X⟯ K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
hinj : Function.Injective ⇑(algebraMap F[X] K)
⊢ ∀ (a : F[X]), (algebraMap F[X] ↥(ringOfIntegers F K)) a = 0 → a = 0

Tactic:
intro p

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F[X] K
inst✝¹ : Algebra F⟮X⟯ K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
hinj : Function.Injective ⇑(algebraMap F[X] K)
p : F[X]
⊢ (algebraMap F[X] ↥(ringOfIntegers F K)) p = 0 → p = 0
Module: Mathlib.NumberTheory.FunctionField

Goal state before:
pp: F : Type u_3
K : Type u_4
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Algebra F⟮X⟯ K
inst✝² : FunctionField F K
inst✝¹ : Algebra F K
inst✝ : IsScalarTower F F⟮X⟯ K
y : K
hy : Transcendental F y
x : K := (algebraMap F⟮X⟯ K) X
Fyx : IntermediateField F K := restrictScalars F (↥F⟮y⟯)⟮x⟯
Fxy : IntermediateField F K := restrictScalars F (↥F⟮x⟯)⟮y⟯
this✝⁵ : Algebra ↥F⟮y⟯ ↥Fyx := (↥F⟮y⟯)⟮x⟯.algebra
this✝⁴ : Module ↥F⟮y⟯ ↥Fyx := Algebra.toModule
this✝³ : SMul ↥F⟮y⟯ ↥Fyx := this✝⁵.toSMul
this✝² : Algebra ↥F⟮x⟯ ↥Fxy := (↥F⟮x⟯)⟮y⟯.algebra
this✝¹ : Module ↥F⟮x⟯ ↥Fxy := Algebra.toModule
this✝ : SMul ↥F⟮x⟯ ↥Fxy := this✝².toSMul
this : FiniteDimensional ↥F⟮y⟯ ↥Fyx
⊢ FiniteDimensional (↥Fyx) K

Tactic:
have := FiniteDimensional.adjoin_algebraMap_X (F := F) (K := K)

Goal state after:
F : Type u_3
K : Type u_4
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Algebra F⟮X⟯ K
inst✝² : FunctionField F K
inst✝¹ : Algebra F K
inst✝ : IsScalarTower F F⟮X⟯ K
y : K
hy : Transcendental F y
x : K := (algebraMap F⟮X⟯ K) X
Fyx : IntermediateField F K := restrictScalars F (↥F⟮y⟯)⟮x⟯
Fxy : IntermediateField F K := restrictScalars F (↥F⟮x⟯)⟮y⟯
this✝⁶ : Algebra ↥F⟮y⟯ ↥Fyx := (↥F⟮y⟯)⟮x⟯.algebra
this✝⁵ : Module ↥F⟮y⟯ ↥Fyx := Algebra.toModule
this✝⁴ : SMul ↥F⟮y⟯ ↥Fyx := this✝⁶.toSMul
this✝³ : Algebra ↥F⟮x⟯ ↥Fxy := (↥F⟮x⟯)⟮y⟯.algebra
this✝² : Module ↥F⟮x⟯ ↥Fxy := Algebra.toModule
this✝¹ : SMul ↥F⟮x⟯ ↥Fxy := this✝³.toSMul
this✝ : FiniteDimensional ↥F⟮y⟯ ↥Fyx
this : FiniteDimensional (↥F⟮(algebraMap F⟮X⟯ K) X⟯) K
⊢ FiniteDimensional (↥Fyx) K
Module: Mathlib.NumberTheory.FunctionField

Goal state before:
pp: F : Type u_3
K : Type u_4
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Algebra F⟮X⟯ K
inst✝² : FunctionField F K
inst✝¹ : Algebra F K
inst✝ : IsScalarTower F F⟮X⟯ K
y : K
hy : Transcendental F y
x : K := (algebraMap F⟮X⟯ K) X
Fyx : IntermediateField F K := restrictScalars F (↥F⟮y⟯)⟮x⟯
Fxy : IntermediateField F K := restrictScalars F (↥F⟮x⟯)⟮y⟯
this✝⁶ : Algebra ↥F⟮y⟯ ↥Fyx := (↥F⟮y⟯)⟮x⟯.algebra
this✝⁵ : Module ↥F⟮y⟯ ↥Fyx := Algebra.toModule
this✝⁴ : SMul ↥F⟮y⟯ ↥Fyx := this✝⁶.toSMul
this✝³ : Algebra ↥F⟮x⟯ ↥Fxy := (↥F⟮x⟯)⟮y⟯.algebra
this✝² : Module ↥F⟮x⟯ ↥Fxy := Algebra.toModule
this✝¹ : SMul ↥F⟮x⟯ ↥Fxy := this✝³.toSMul
this✝ : FiniteDimensional ↥F⟮y⟯ ↥Fyx
this : FiniteDimensional (↥F⟮(algebraMap F⟮X⟯ K) X⟯) K
⊢ FiniteDimensional (↥(restrictScalars F (↥F⟮y⟯)⟮x⟯)) K

Tactic:
rw [adjoin_simple_comm]

Goal state after:
F : Type u_3
K : Type u_4
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Algebra F⟮X⟯ K
inst✝² : FunctionField F K
inst✝¹ : Algebra F K
inst✝ : IsScalarTower F F⟮X⟯ K
y : K
hy : Transcendental F y
x : K := (algebraMap F⟮X⟯ K) X
Fyx : IntermediateField F K := restrictScalars F (↥F⟮y⟯)⟮x⟯
Fxy : IntermediateField F K := restrictScalars F (↥F⟮x⟯)⟮y⟯
this✝⁶ : Algebra ↥F⟮y⟯ ↥Fyx := (↥F⟮y⟯)⟮x⟯.algebra
this✝⁵ : Module ↥F⟮y⟯ ↥Fyx := Algebra.toModule
this✝⁴ : SMul ↥F⟮y⟯ ↥Fyx := this✝⁶.toSMul
this✝³ : Algebra ↥F⟮x⟯ ↥Fxy := (↥F⟮x⟯)⟮y⟯.algebra
this✝² : Module ↥F⟮x⟯ ↥Fxy := Algebra.toModule
this✝¹ : SMul ↥F⟮x⟯ ↥Fxy := this✝³.toSMul
this✝ : FiniteDimensional ↥F⟮y⟯ ↥Fyx
this : FiniteDimensional (↥F⟮(algebraMap F⟮X⟯ K) X⟯) K
⊢ FiniteDimensional (↥(restrictScalars F (↥F⟮x⟯)⟮y⟯)) K
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ ψ x - θ x ≤ ψ (x ^ 2⁻¹) + ψ (x ^ 3⁻¹) + ψ (x ^ 5⁻¹) ∧ ψ (x ^ 2⁻¹) + ψ (x ^ 3⁻¹) + ψ (x ^ 7⁻¹) ≤ ψ x - θ x

Tactic:
by
  obtain ⟨N₁, h1⟩ := psi_pow_eq_sum_b x 1 hx
  obtain ⟨N₂, h2⟩ := psi_pow_eq_sum_b x 2 hx
  obtain ⟨N₃, h3⟩ := psi_pow_eq_sum_b x 3 hx
  obtain ⟨N₅, h5⟩ := psi_pow_eq_sum_b x 5 hx
  obtain ⟨N₇, h7⟩ := psi_pow_eq_sum_b x 7 hx
  let N := N₁ + N₂ + N₃ + N₅ + N₇
  specialize h1 (1 + 6 * N) (by lia)
  specialize h2 (3 * N) (by lia)
  specialize h3 (2 * N) (by lia)
  specialize h5 N (by lia)
  specialize h7 N (by lia)
  have : ∑ n ∈ Icc 1 N, c x n ≤ ∑ n ∈ Icc 1 N, b x (5 * n) := by
    apply sum_le_sum
    intro n hn
    unfold c
    linarith [(b_antitone x hx (by grind) (by grind) (by lia) : b x (6 * n + 1) ≤ b x (6 * n)),
      (b_antitone x hx (by grind) (by grind) (by lia) : b x (6 * n - 1) ≤ b x (5 * n))]
  have : ∑ n ∈ Icc 1 N, b x (7 * n) ≤ ∑ n ∈ Icc 1 N, c x n := by
    apply sum_le_sum; intro n hn; simp only [mem_Icc, c] at hn ⊢
    linarith [(b_antitone x hx (by grind) (by grind) (by lia) : b x (6 * n) ≤ b x (6 * n - 1)),
      (b_antitone x hx (by grind) (by grind) (by lia) : b x (7 * n) ≤ b x (6 * n + 1))]
  have : b x 1 = θ x := by simp [b]
  simp only [cast_one, one_mul, sum_b_eq_b_add_sum_add_sum_add_sum, inv_one, rpow_one] at h1
  grind

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ↑p ∣ x
⊢ x.zmodRepr = 0

Tactic:
apply zmodRepr_unique _ _ (Nat.Prime.pos Fact.out)
  simp [maximalIdeal_eq_span_p, Ideal.mem_span_singleton, hx]

Goal state after:
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
inst✝ : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
q : S
r : R
hr : r ∈ finsetApprox bS adm
hqr : abv ((Algebra.norm R) (r • a' - b' • q)) < abv ((Algebra.norm R) ((algebraMap R S) b'))
⊢ abv ((Algebra.norm R) ((algebraMap R S) b')) * abv ((Algebra.norm R) (r • a - q * b)) =
    abv ((Algebra.norm R) (r • a' - b' • q)) * abv ((Algebra.norm R) b)

Tactic:
← abv.map_mul,

Goal state after:
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
inst✝ : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
q : S
r : R
hr : r ∈ finsetApprox bS adm
hqr : abv ((Algebra.norm R) (r • a' - b' • q)) < abv ((Algebra.norm R) ((algebraMap R S) b'))
⊢ abv ((Algebra.norm R) ((algebraMap R S) b') * (Algebra.norm R) (r • a - q * b)) =
    abv ((Algebra.norm R) (r • a' - b' • q)) * abv ((Algebra.norm R) b)
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
inst✝ : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
q : S
r : R
hr : r ∈ finsetApprox bS adm
hqr : abv ((Algebra.norm R) (r • a' - b' • q)) < abv ((Algebra.norm R) ((algebraMap R S) b'))
⊢ abv ((Algebra.norm R) ((algebraMap R S) b' * (r • a - q * b))) =
    abv ((Algebra.norm R) (r • a' - b' • q)) * abv ((Algebra.norm R) b)

Tactic:
← abv.map_mul,

Goal state after:
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
inst✝ : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
q : S
r : R
hr : r ∈ finsetApprox bS adm
hqr : abv ((Algebra.norm R) (r • a' - b' • q)) < abv ((Algebra.norm R) ((algebraMap R S) b'))
⊢ abv ((Algebra.norm R) ((algebraMap R S) b' * (r • a - q * b))) =
    abv ((Algebra.norm R) (r • a' - b' • q) * (Algebra.norm R) b)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ θ x ≤ ψ x

Tactic:
theta_le_psi

Goal state after:
x : ℝ
⊢ ψ x ≤ ψ x
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝² x✝¹ x✝ : Poly α
⊢ x✝² * (x✝¹ + x✝) = x✝² * x✝¹ + x✝² * x✝

Tactic:
by ext; simp_rw [add_apply, mul_apply]; apply mul_add

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

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

Tactic:
have : (⟨x, y⟩ * a : ℤ√d) = (x : ℤ√d) * a + sqrtd * ((y : ℤ√d) * a) := by
    rw [decompose, right_distrib, mul_assoc, Int.cast_natCast, Int.cast_natCast]

Goal state after:
d x y : ℕ
a : ℤ√↑d
ha : a.Nonneg
this : { re := ↑x, im := ↑y } * a = ↑x * a + sqrtd * (↑y * a)
⊢ ({ re := ↑x, im := ↑y } * a).Nonneg
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case e'_2
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (cyclotomic (2 ^ (0 + 1)) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
⊢ discr K ((fun i ↦ (algebraMap K L) (-1) ^ ↑i) ∘ ⇑e.symm) = discr K fun i ↦ (algebraMap K L) (-1) ^ ↑i

pp: case pos.convert_2
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (cyclotomic (2 ^ (0 + 1)) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
⊢ (discr K fun i ↦ (algebraMap K L) (-1) ^ ↑i) = 1

Tactic:
· congr 1
        ext i
        simp only [map_neg, map_one, Function.comp_apply, Fin.val_eq_zero, _root_.pow_zero]
        suffices (e.symm i : ℕ) = 0 by simp [this]
        rw [← Nat.lt_one_iff]
        convert! (e.symm i).2
        rw [this]

Goal state after:
case pos.convert_2
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (cyclotomic (2 ^ (0 + 1)) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
⊢ (discr K fun i ↦ (algebraMap K L) (-1) ^ ↑i) = 1
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ xn a1 (2 * n + 2 * n - j) + xn a1 (2 * n - j) ≡ 0 [MOD xn a1 n]

Tactic:
add_tsub_assoc_of_le h'

Goal state after:
a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ xn a1 (2 * n + (2 * n - j)) + xn a1 (2 * n - j) ≡ 0 [MOD xn a1 n]
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
this : 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 this

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

Goal state before:
pp: ξ : ℚ
f : ℚ → ℤ × ℕ := fun q ↦ (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
hinj : Function.Injective f
xy : ℤ × ℕ
q : ℚ
hq₁ : q ∈ s
hq₂ : f q = xy
hd : q.den ≤ ξ.den
hn : ⌈ξ * ↑q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑q.den⌋ + 1
⊢ xy ∈ Icc (⌈ξ * ↑q.den⌉ - 1) (⌊ξ * ↑q.den⌋ + 1) ×ˢ {q.den}

Tactic:
simp only [prod_singleton, mem_image, mem_Icc]

Goal state after:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q ↦ (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
hinj : Function.Injective f
xy : ℤ × ℕ
q : ℚ
hq₁ : q ∈ s
hq₂ : f q = xy
hd : q.den ≤ ξ.den
hn : ⌈ξ * ↑q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑q.den⌋ + 1
⊢ ∃ x, (⌈ξ * ↑q.den⌉ - 1 ≤ x ∧ x ≤ ⌊ξ * ↑q.den⌋ + 1) ∧ (x, q.den) = xy
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: case right
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
hpm : ¬p ∣ m
⊢ (List.filter (fun x ↦ decide (x ∈ s)) (p ^ e * m).primeFactorsList).prod = m

Tactic:
conv_rhs => rw [← prod_primeFactorsList hm₀]

Goal state after:
case right
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
hpm : ¬p ∣ m
⊢ (List.filter (fun x ↦ decide (x ∈ s)) (p ^ e * m).primeFactorsList).prod = 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
⊢ (replicate (List.count p m.primeFactorsList) p ++ List.filter (fun x ↦ decide (x ∈ s)) m.primeFactorsList).prod = m

Tactic:
conv_rhs => rw [← 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
⊢ (replicate (List.count p m.primeFactorsList) p ++ List.filter (fun x ↦ decide (x ∈ s)) m.primeFactorsList).prod =
    m.primeFactorsList.prod
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
s : Finset ℕ
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
H₁ : ∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n) = ∏ p ∈ s with Nat.Prime p, (1 - f p)⁻¹
⊢ ∀ {p : ℕ}, Nat.Prime p → Summable fun n ↦ ‖f (p ^ n)‖

Tactic:
intro p

Goal state after:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
s : Finset ℕ
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
H₁ : ∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n) = ∏ p ∈ s with Nat.Prime p, (1 - f p)⁻¹
p : ℕ
⊢ Nat.Prime p → Summable fun n ↦ ‖f (p ^ n)‖
Module: Mathlib.NumberTheory.LSeries.Positivity

Goal state before:
pp: case isFalse.succ
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
k : ℕ
h✝ : ¬k = 0
n : ℕ
IH : 0 ≤ logMul^[n] a k
⊢ 0 ≤ logMul^[n + 1] a k

Tactic:
Function.iterate_succ_apply'

Goal state after:
case isFalse.succ
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
k : ℕ
h✝ : ¬k = 0
n : ℕ
IH : 0 ≤ logMul^[n] a k
⊢ 0 ≤ logMul (logMul^[n] a) k
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
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)

Tactic:
rw [convergent_succ, ← hn,
      (mod_cast toNat_of_nonneg huv₀.le : ((u - ⌊ξ⌋ * v).toNat : ℚ) = u - ⌊ξ⌋ * v),
      cast_natCast, inv_div, sub_div, mul_div_cancel_right₀ _ Hv, add_sub_cancel]

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

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.LSeries.AbstractFuncEq

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

Tactic:
apply Integrable.smul_const
      rw [← IntegrableOn, ← intervalIntegrable_iff_integrableOn_Ioc_of_le zero_le_one]
      exact intervalIntegral.intervalIntegrable_cpow' h_re1

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

Goal state before:
pp: x : ℝ
⊢ oddKernel 0 x = 0

Tactic:
by
  simpa using oddKernel_neg 0 x

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

Goal state before:
pp: case inr.H
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * ↑(1 / x)) = I * ↑x
h2 : -I * (I * ↑(1 / x)) = 1 / ↑x
h3 : ↑x ^ (3 / 2) ≠ 0
h4 : (↑x).arg ≠ π
J : ℂ
⊢ J * (-2 * ↑π) = (↑x ^ (3 / 2))⁻¹ * (-2 * ↑π * ↑x ^ (3 / 2) * J)

Tactic:
← div_eq_inv_mul,

Goal state after:
case inr.H
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * ↑(1 / x)) = I * ↑x
h2 : -I * (I * ↑(1 / x)) = 1 / ↑x
h3 : ↑x ^ (3 / 2) ≠ 0
h4 : (↑x).arg ≠ π
J : ℂ
⊢ J * (-2 * ↑π) = -2 * ↑π * ↑x ^ (3 / 2) * J / ↑x ^ (3 / 2)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ completedCosZeta₀ a (1 - s) = completedHurwitzZetaEven₀ a s

Tactic:
by
  rw [← completedHurwitzZetaEven₀_one_sub, sub_sub_cancel]

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n ↦ if n = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s) (completedCosZeta (↑a) s)

Tactic:
have aux : ((|0| : ℤ) : ℂ) ^ s = 0 := by
    rw [abs_zero, Int.cast_zero, zero_cpow (ne_zero_of_one_lt_re hs)]

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
aux : ↑|0| ^ s = 0
⊢ HasSum (fun n ↦ if n = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s) (completedCosZeta (↑a) s)
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
⊢ ¬LSeriesSummable (fun n ↦ χ ↑n) 1

Tactic:
by
  refine fun h ↦ (Real.not_summable_indicator_one_div_natCast hN 1) ?_
  refine h.norm.of_nonneg_of_le (fun m ↦ Set.indicator_apply_nonneg (fun _ ↦ by positivity))
    (fun n ↦ ?_)
  simp only [norm_term_eq, Set.indicator, Set.mem_ofPred_eq]
  split_ifs with h₁ h₂
  · simp [h₂]
  · simp [h₁, χ.map_one]
  all_goals positivity

Goal state after: