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

Goal state before:
pp: x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun x ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
⊢ ∃ x1 x2, 0.5 < x1 ∧ x1 < x2 ∧ x2 ≤ x ∧ 0 ≤ f x1 ∧ f x2 ≤ 0

Tactic:
refine ⟨18, 512, by norm_num1, by norm_num1, x_large, ?_, ?_⟩

Goal state after:
case refine_1
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun x ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
⊢ 0 ≤ f 18

case refine_2
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun x ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
⊢ f 512 ≤ 0
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: case hf.inr
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
x : ℕ
hx : x ≤ 2 * n
h2x : 2 * n < 3 * x
h : x ≤ n
⊢ x ^ n.centralBinom.factorization x = 1

Tactic:
· rw [factorization_centralBinom_of_two_mul_self_lt_three_mul n_large h h2x, Nat.pow_zero]

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

Tactic:
cases p with

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: p l : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ (∑ v ∈ Ico 1 p, ↑v ^ l + if p - 1 ∣ l then 1 else 0) = 0

Tactic:
by
  have hbij : (∑ v ∈ Ico 1 p, (v : ZMod p) ^ l) = ∑ u : (ZMod p)ˣ, (u : ZMod p) ^ l :=
    Finset.sum_bij'
      (fun v hv ↦ Units.mk0 (v : ZMod p) (mt (ZMod.natCast_eq_zero_iff v p).mp (by
        grind [not_dvd_of_pos_of_lt])))
      (fun u _ ↦ (u : ZMod p).val)
      (fun _ _ ↦ Finset.mem_univ _)
      (fun u _ ↦ by grind [u.ne_zero, ZMod.val_ne_zero, ZMod.val_lt])
      (fun v hv ↦ by simp [ZMod.val_cast_of_lt (Finset.mem_Ico.mp hv).2])
      (fun u _ ↦ Units.ext (ZMod.natCast_zmod_val _))
      (fun _ _ ↦ rfl)
  rw [hbij, FiniteField.sum_pow_units, ZMod.card]
  grind

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: p M N : ℕ
inst✝ : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := M.factorization p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : ↑p ≠ 0
hdecomp : p ^ e * M' = M
hM_eq : ↑M = ↑(p ^ e) * ↑M'
hrw : ↑p ^ N / ↑M = ↑p ^ (N - e) / ↑M'
hM'_eq : ↑p ^ (N - e) / ↑M' = Rat.divInt (↑p ^ (N - e)) ↑M'
⊢ (Rat.divInt (↑p ^ (N - e)) ↑M').den ∣ M'

Tactic:
exact Int.natCast_dvd_natCast.mp (Rat.den_dvd _ _)

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case 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 < 2 * k
⊢ (Rat.padicValuation p) (↑p ^ (2 * k) / (2 * ↑k + 1)) ≤ 1

Tactic:
exact_mod_cast pIntegral_pow_div (by lia)
      (factorization_succ_le_sub_one (by lia) |>.trans tsub_le_self)

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

Goal state before:
pp: case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : cardPowDegree (x - y) < a
hyz : cardPowDegree (y - z) < a
ha : 0 < a
hxy' : x - y ≠ 0
hyz' : y - z ≠ 0
hxz' : x - z ≠ 0
this : 1 ≤ ↑(Fintype.card Fq)
⊢ (x - z).natDegree ≤ (x - y).natDegree ∨ (x - z).natDegree ≤ (y - z).natDegree

Tactic:
rw [natDegree_le_iff_degree_le, natDegree_le_iff_degree_le, ← le_max_iff, ←
    degree_eq_natDegree hxy', ← degree_eq_natDegree hyz']

Goal state after:
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : cardPowDegree (x - y) < a
hyz : cardPowDegree (y - z) < a
ha : 0 < a
hxy' : x - y ≠ 0
hyz' : y - z ≠ 0
hxz' : x - z ≠ 0
this : 1 ≤ ↑(Fintype.card Fq)
⊢ (x - z).degree ≤ max (x - y).degree (y - z).degree
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case pos
x : ℝ
h : x < 2
⊢ θ x ≤ ψ x

Tactic:
theta_eq_zero_of_lt_two h,

Goal state after:
case pos
x : ℝ
h : x < 2
⊢ 0 ≤ ψ x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ ↑n.lcmUpto ≠ 0

Tactic:
by simp [lcmUpto_ne_zero]

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
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
j : Fin (cardM bS adm).succ
i : ι
x✝ : i ∈ Finset.univ
⊢ ((distinctElems bS adm) j * s i) • bS i =
    b • ((distinctElems bS adm) j * s i / b) • bS i + ((distinctElems bS adm) j * s i % b) • bS i

Tactic:
μ_eq,

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
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
j : Fin (cardM bS adm).succ
i : ι
x✝ : i ∈ Finset.univ
⊢ (b * qs j i + rs j i) • bS i = b • ((b * qs j i + rs j i) / b) • bS i + ((b * qs j i + rs j i) % b) • bS i
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case succ
x : ℝ
N : ℕ
ih :
  ∑ n ∈ Icc 1 (1 + 6 * N), b x n =
    b x 1 + ∑ n ∈ Icc 1 (3 * N), b x (2 * n) + ∑ n ∈ Icc 1 (2 * N), b x (3 * n) + ∑ n ∈ Icc 1 N, c x n
⊢ ∑ n ∈ Icc 1 (1 + 6 * (N + 1)), b x n =
    b x 1 + ∑ n ∈ Icc 1 (3 * (N + 1)), b x (2 * n) + ∑ n ∈ Icc 1 (2 * (N + 1)), b x (3 * n) + ∑ n ∈ Icc 1 (N + 1), c x n

Tactic:
| succ N ih =>

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Polynomial.Bivariate

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B : Type u_3
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : A
y : B
hx : Transcendental R x
hy : Transcendental R y
h : IsAlgebraic (↥R[x]) y
⊢ IsAlgebraic (↥R[y]) ((algebraMap A B) x)

Tactic:
obtain ⟨f, hnezero, halg⟩ := h
  refine ⟨hy.algEquivAdjoin (swap (hx.algEquivAdjoin.symm f)),
    by simpa only [map_ne_zero_iff _ (AlgEquiv.injective _)], ?_⟩
  simpa [Transcendental.algEquivAdjoin_swap_eq_aeval hy, aeval_aeval_eq_aeval_algEquivAdjoin y hx]

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : x - ↑a ∈ Ideal.span {↑p ^ n}
hb : x - ↑b ∈ Ideal.span {↑p ^ n}
⊢ ↑a = ↑b

Tactic:
rw [Ideal.mem_span_singleton] at ha hb
  rw [← sub_eq_zero, ← Int.cast_sub, ZMod.intCast_zmod_eq_zero_iff_dvd, Int.natCast_pow]
  rw [← dvd_neg, neg_sub] at ha
  have := dvd_add ha hb
  rwa [sub_eq_add_neg, sub_eq_add_neg, add_assoc, neg_add_cancel_left, ← sub_eq_add_neg, ←
    Int.cast_sub, pow_p_dvd_int_iff] at this

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
hn : OfNat.ofNat n < p
⊢ (OfNat.ofNat n).zmodRepr = OfNat.ofNat n

Tactic:
by
  convert! zmodRepr_natCast_of_lt hn
  rcases n with _ | _ | n <;> simp

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

Goal state before:
pp: case refine_3
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✝¹ : IsDedekindDomain S
inst✝ : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ∏ m ∈ finsetApprox bS adm, m
hM : (algebraMap R S) M ≠ 0
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
b_min : ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0
J : Ideal S
hJ : Ideal.span {(algebraMap R S) M} * ↑I = Ideal.span {b} * J
⊢ (algebraMap R S) M ∈ ↑⟨J, ⋯⟩

Tactic:
rw [← SetLike.mem_coe, ← Set.singleton_subset_iff, ← Ideal.span_le, ← Ideal.dvd_iff_le]

Goal state after:
case refine_3
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✝¹ : IsDedekindDomain S
inst✝ : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ∏ m ∈ finsetApprox bS adm, m
hM : (algebraMap R S) M ≠ 0
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
b_min : ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0
J : Ideal S
hJ : Ideal.span {(algebraMap R S) M} * ↑I = Ideal.span {b} * J
⊢ ↑⟨J, ⋯⟩ ∣ Ideal.span {(algebraMap R S) M}
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
x y : ℤ_[p]
I : Ideal ℤ_[p] := Ideal.span {↑v}
⊢ x * y - ↑(f x * f y) = x * (y - ↑(f y)) + (x - ↑(f x)) * ↑(f y)

Tactic:
rw [cast_mul]

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
x y : ℤ_[p]
I : Ideal ℤ_[p] := Ideal.span {↑v}
⊢ x * y - ↑(f x) * ↑(f y) = x * (y - ↑(f y)) + (x - ↑(f x)) * ↑(f y)
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
this : ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim
hn : n = pb.dim
h₂ : 2 ∣ pb.dim * (pb.dim - 1)
hne : ↑2 ≠ 0
⊢ n ≠ 0

Tactic:
← zero_lt_iff,

Goal state after:
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
this : ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim
hn : n = pb.dim
h₂ : 2 ∣ pb.dim * (pb.dim - 1)
hne : ↑2 ≠ 0
⊢ 0 < n
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : ((minpoly K pb.gen).aroots E).Nodup
hroots : ∀ (σ : L →ₐ[K] E), σ pb.gen ∈ (minpoly K pb.gen).aroots E
⊢ (algebraMap K E) (discr K ⇑pb.basis) =
    (algebraMap K E) (-1) ^ (n * (n - 1) / 2) *
      (algebraMap K E) ((norm K) ((aeval pb.gen) (derivative (minpoly K pb.gen))))

Tactic:
map_neg,

Goal state after:
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : ((minpoly K pb.gen).aroots E).Nodup
hroots : ∀ (σ : L →ₐ[K] E), σ pb.gen ∈ (minpoly K pb.gen).aroots E
⊢ (algebraMap K E) (discr K ⇑pb.basis) =
    (-(algebraMap K E) 1) ^ (n * (n - 1) / 2) *
      (algebraMap K E) ((norm K) ((aeval pb.gen) (derivative (minpoly K pb.gen))))
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : yn a1 m ≤ yn a1 n
⊢ yn a1 m ≤ yn a1 n * a

Tactic:
rw [← mul_one (yn a1 m)]

Goal state after:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : yn a1 m ≤ yn a1 n
⊢ yn a1 m * 1 ≤ yn a1 n * a
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n := ⋯
xle : xn a1 (2 * n - k) ≤ xn a1 n
⊢ xn a1 k + xn a1 (2 * n - k) ≡ xn a1 n - xn a1 (2 * n - k) + xn a1 (2 * n - k) [MOD xn a1 n]

Tactic:
rw [tsub_add_cancel_of_le xle]

Goal state after:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n := eq_of_xn_modEq_lem3._proof_1_5 npos k kn
xle : xn a1 (2 * n - k) ≤ xn a1 n
⊢ xn a1 k + xn a1 (2 * n - k) ≡ xn a1 n [MOD xn a1 n]
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
h : a = 0
⊢ a.norm = 0

Tactic:
rw [h, norm_zero]

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

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

Tactic:
let f : ℤ → ℤ := fun m => ⌊fract (ξ * m) * (n + 1)⌋

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

Goal state before:
pp: s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
⊢ Function.RightInverse
    (fun x ↦
      match x with
      | ⟨m, property⟩ => (m.factorization p, ⟨(List.filter (fun x ↦ decide (x ∈ s)) m.primeFactorsList).prod, ⋯⟩))
    fun x ↦
    match x with
    | (e, n) => ⟨p ^ e * ↑n, ⋯⟩

Tactic:
rintro ⟨m, hm₀, 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
⊢ (fun x ↦
        match x with
        | (e, n) => ⟨p ^ e * ↑n, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨m, property⟩ => (m.factorization p, ⟨(List.filter (fun x ↦ decide (x ∈ s)) m.primeFactorsList).prod, ⋯⟩))
        ⟨m, ⋯⟩) =
    ⟨m, ⋯⟩
Module: Mathlib.NumberTheory.LSeries.Convolution

Goal state before:
pp: f g : ℕ → ℂ
s a b : ℂ
hf : LSeriesHasSum f s a
hg : LSeriesHasSum g s b
⊢ LSeriesHasSum (f ⍟ g) s (a * b)

Tactic:
have hsum := summable_mul_of_summable_norm hf.summable.norm hg.summable.norm
  -- NB: this `simpa` is quite slow if un-squeezed
  simpa only [LSeriesHasSum, term_convolution'] using (hf.mul hg hsum).tsum_fiberwise _

Goal state after:
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
⊢ ∃ n, ↑u / ↑v = ξ.convergent n

Tactic:
have Hv : (v : ℚ) ≠ 0 := (Nat.cast_pos.mpr (zero_lt_one.trans ht)).ne'

Goal state after:
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
⊢ ∃ n, ↑u / ↑v = ξ.convergent n
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
⊢ ‖f_nat k a t n‖ ≤ g_nat k a t n

Tactic:
rw [f_nat, norm_of_nonneg (by positivity), g_nat]
  simp only [neg_mul, add_sq]
  gcongr
  have H₁ : (n : ℝ) ≤ n ^ 2 := mod_cast Nat.le_self_pow two_ne_zero n
  have H₂ : 0 ≤ 2 * n * a := by positivity
  linear_combination H₁ + H₂

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : x < 1
⊢ 1 < 1 / x

Tactic:
rwa [lt_one_div one_pos hx, div_one]

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

Goal state before:
pp: case mp
z τ : ℂ
h : Summable fun x ↦ jacobiTheta₂_term_fderiv x z τ
this : Summable fun x ↦ ‖jacobiTheta₂_term_fderiv x z τ‖
⊢ ∀ᶠ (i : ℤ) in cofinite, ‖jacobiTheta₂_term i z τ‖ ≤ ‖jacobiTheta₂_term_fderiv i z τ‖

Tactic:
have : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0 :=
      Int.cofinite_eq ▸ (mem_sup.mpr ⟨eventually_ne_atBot 0, eventually_ne_atTop 0⟩)

Goal state after:
case mp
z τ : ℂ
h : Summable fun x ↦ jacobiTheta₂_term_fderiv x z τ
this✝ : Summable fun x ↦ ‖jacobiTheta₂_term_fderiv x z τ‖
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
⊢ ∀ᶠ (i : ℤ) in cofinite, ‖jacobiTheta₂_term i z τ‖ ≤ ‖jacobiTheta₂_term_fderiv i z τ‖
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case mp
z τ : ℂ
h : Summable fun x ↦ jacobiTheta₂'_term x z τ
⊢ ∀ᶠ (i : ℤ) in cofinite, ‖jacobiTheta₂_term i z τ‖ ≤ (2 * π)⁻¹ * ‖jacobiTheta₂'_term i z τ‖

Tactic:
have : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0 :=
      Int.cofinite_eq ▸ (mem_sup.mpr ⟨eventually_ne_atBot 0, eventually_ne_atTop 0⟩)

Goal state after:
case mp
z τ : ℂ
h : Summable fun x ↦ jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
⊢ ∀ᶠ (i : ℤ) in cofinite, ‖jacobiTheta₂_term i z τ‖ ≤ (2 * π)⁻¹ * ‖jacobiTheta₂'_term i z τ‖
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a t : ℝ
ht : 0 < t
n : ℤ
⊢ cexp (↑π * I * ↑a * ↑n * 2 - ↑π * ↑n ^ 2 * ↑t) = cexp (↑π * I * ↑a * ↑n * 2 + ↑π * I ^ 2 * ↑n ^ 2 * ↑t)

Tactic:
simp [sub_eq_add_neg]

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
⊢ LSeriesSummable ((fun n ↦ χ ↑n) * f) s

Tactic:
by
  refine .of_norm <| h.norm.of_nonneg_of_le (fun _ ↦ norm_nonneg _) fun n ↦ norm_term_le s ?_
  simpa using mul_le_of_le_one_left (norm_nonneg <| f n) <| χ.norm_le_one n

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ ∑' (p : Primes), -Complex.log (1 - χ ↑↑p * ↑↑p ^ (-s)) = L (fun n ↦ χ ↑n * ↑(Λ n) / ↑(Real.log ↑n)) s

Tactic:
have hpow_le (p : Primes) : ‖χ p * (p : ℂ) ^ (-s)‖ < 1 := by
    grw [norm_mul, norm_le_one, norm_natCast_cpow_of_pos (mod_cast p.prop.pos), neg_re, one_mul]
    apply rpow_lt_one_of_one_lt_of_neg (mod_cast p.prop.one_lt) (by linarith)
  rw [tsum_congr (fun p ↦ (hasSum_taylorSeries_neg_log' (hpow_le p)).tsum_eq.symm),
    LSeries_def₀ (by simp)]
  let f : ℕ → ℂ := fun n ↦ χ n * Λ n / Real.log n * ((n : ℂ) ^ (-s))
  calc
    _ = ∑' (p : Primes) (k : ℕ), (χ (p ^ (k + 1)) * ((p ^ (k + 1) : ℕ) : ℂ) ^ (-s)) *
          Λ (p ^ (k + 1)) / Real.log (p ^ (k + 1)) := by
      refine tsum_congr fun p ↦ tsum_congr fun k ↦ ?_
      have : Complex.log p ≠ 0 := mod_cast p.prop.log_ne_zero
      simp [mul_pow, ← cpow_nat_mul, ← natCast_cpow_natCast_mul, vonMangoldt_apply_pow,
        vonMangoldt_apply_prime p.2, field]
    _ = ∑' n : {n : ℕ // IsPrimePow n}, f n := by
      rw [← tsum_primes_pow_eq]
      · exact tsum_congr fun p ↦ tsum_congr fun k ↦ (by unfold f; simp; ring)
      · apply comp_injective _ Subtype.coe_injective (f := f)
        apply of_norm_bounded_eventually_nat (g := (↑· ^ (-s.re)))
        · simp [hs]
        · filter_upwards [eventually_gt_atTop 1] with n hn
          simp only [f, norm_mul, norm_div, norm_real, norm_eq_abs]
          grw [norm_le_one, vonMangoldt_le_log]
          have := log_pos (x := n) (mod_cast hn)
          field_simp
          rw [← ofReal_natCast n, norm_cpow_eq_rpow_re_of_nonneg (by simp) (by simp; grind)]
          simp
    _ = _ := by
      simp only [div_eq_mul_inv _ (_ ^ _), ← cpow_neg]
      suffices (Function.support f) ⊆ {n | IsPrimePow n} from
        tsum_subtype_eq_of_support_subset this
      intro n hn
      contrapose! hn
      simp [f, vonMangoldt_eq_zero_iff.mpr hn]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Radical

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
⊢ p ^ (i + 1) ∣ normalize p * derivative (p ^ (i + 1))

Tactic:
derivative_pow_succ,

Goal state after:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
⊢ p ^ (i + 1) ∣ normalize p * (C (↑i + 1) * p ^ i * derivative p)
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
⊢ radical a ∣ radical b ↔ primeFactors a ⊆ primeFactors b

Tactic:
radical_dvd_radical_iff_normalizedFactors_subset_normalizedFactors,

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
⊢ normalizedFactors a ⊆ normalizedFactors b ↔ primeFactors a ⊆ primeFactors b
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case inr.refine_2
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
hb : b ≠ 0
h : radical a ∣ b
⊢ a ∣ b ^ (normalizedFactors a).card

Tactic:
· classical
    rwa [dvd_iff_normalizedFactors_le_normalizedFactors ha <| pow_ne_zero _ hb,
      normalizedFactors_pow, Multiset.le_card_smul_iff_subset, ← Multiset.toFinset_subset,
      toFinset_normalizedFactors, toFinset_normalizedFactors,
      ← radical_dvd_iff_primeFactors_subset hb]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.FractionalIdeal

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : ↥ℤ⁰
⊢ ↑↑x ≠ 0

Tactic:
Int.cast_ne_zero

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : ↥ℤ⁰
⊢ ↑x ≠ 0
Module: Mathlib.NumberTheory.NumberField.FractionalIdeal

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ Free.ChooseBasisIndex ℤ ↥↑↑I
⊢ |(integralBasis K).det ⇑((basisOfFractionalIdeal K I).reindex e.symm)| = FractionalIdeal.absNorm ↑I

Tactic:
rw [← FractionalIdeal.abs_det_basis_change (RingOfIntegers.basis K) I.1
    ((fractionalIdealBasis K I.1).reindex e.symm)]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ Free.ChooseBasisIndex ℤ ↥↑↑I
⊢ |(integralBasis K).det ⇑((basisOfFractionalIdeal K I).reindex e.symm)| =
    |(Basis.localizationLocalization ℚ ℤ⁰ K (RingOfIntegers.basis K)).det
        (Subtype.val ∘ ⇑((fractionalIdealBasis K ↑I).reindex e.symm))|