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

Goal state before:
pp: case refine_2
n : ℕ
⊢ ∀ (p n : ℕ), Nat.Prime p → ∑ i ∈ (p ^ n).divisors, Λ i = Real.log ↑(p ^ n)

pp: case refine_3
n : ℕ
⊢ ∀ (a b : ℕ),
    1 < a →
      1 < b →
        a.Coprime b →
          ∑ i ∈ a.divisors, Λ i = Real.log ↑a →
            ∑ i ∈ b.divisors, Λ i = Real.log ↑b → ∑ i ∈ (a * b).divisors, Λ i = Real.log ↑(a * b)

Tactic:
· intro p k hp
    rw [sum_divisors_prime_pow hp, cast_pow, Real.log_pow, Finset.sum_range_succ', Nat.pow_zero,
      vonMangoldt_apply_one]
    simp [vonMangoldt_apply_pow (Nat.succ_ne_zero _), vonMangoldt_apply_prime hp]

Goal state after:
case refine_3
n : ℕ
⊢ ∀ (a b : ℕ),
    1 < a →
      1 < b →
        a.Coprime b →
          ∑ i ∈ a.divisors, Λ i = Real.log ↑a →
            ∑ i ∈ b.divisors, Λ i = Real.log ↑b → ∑ i ∈ (a * b).divisors, Λ i = Real.log ↑(a * b)
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h₁ : n < n + single i 1
h₂ : n + single i 1 < n + single i 1 + single i 1
h₃ : n < n + single i 1 + single i 1
⊢ MvPolynomial.coeff (n + single i 1)
        ((trunc R (n + single i 1 + single i 1)) f * (trunc R (n + single i 1 + single i 1)) g) *
      (↑(n i) + 1) =
    (coeff n) (f * pderivFun i g) +
      MvPolynomial.coeff n ((trunc R (n + single i 1 + single i 1)) g * (trunc R (n + single i 1)) (pderivFun i f))

Tactic:
← coeff_trunc_mul_trunc_eq_coeff_mul₂ _ _ f (g.pderivFun i) h₃ h₁,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h₁ : n < n + single i 1
h₂ : n + single i 1 < n + single i 1 + single i 1
h₃ : n < n + single i 1 + single i 1
⊢ MvPolynomial.coeff (n + single i 1)
        ((trunc R (n + single i 1 + single i 1)) f * (trunc R (n + single i 1 + single i 1)) g) *
      (↑(n i) + 1) =
    MvPolynomial.coeff n ((trunc R (n + single i 1 + single i 1)) f * (trunc R (n + single i 1)) (pderivFun i g)) +
      MvPolynomial.coeff n ((trunc R (n + single i 1 + single i 1)) g * (trunc R (n + single i 1)) (pderivFun i f))
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPowerSeries σ R
⊢ pderivFun i (f * g) = f • pderivFun i g + g • pderivFun i f

Tactic:
ext n
  have h₁ : n < n + single i 1 := lt_def.mpr ⟨self_le_add_right _ _, i, by simp⟩
  have h₂ : n + single i 1 < n + single i 1 + single i 1 :=
    lt_def.mpr ⟨self_le_add_right _ _, i, by simp⟩
  have h₃ : n < n + single i 1 + single i 1 := lt_trans h₁ h₂
  rw [coeff_pderivFun, map_add, ← coeff_trunc_mul_trunc_eq_coeff_mul _ _ _ h₂, smul_eq_mul,
    smul_eq_mul, ← coeff_trunc_mul_trunc_eq_coeff_mul₂ _ _ g (f.pderivFun i) h₃ h₁,
    ← coeff_trunc_mul_trunc_eq_coeff_mul₂ _ _ f (g.pderivFun i) h₃ h₁, trunc_pderivFun,
    trunc_pderivFun, ← coeff_coe, ← coeff_coe, ← coeff_coe, ← map_add, coe_mul, coe_mul, coe_mul,
    ← pderivFun_coe_mul_coe, coeff_pderivFun]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

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

Tactic:
intro x

Goal state after:
n x : ℕ
⊢ x ∈ range n →
    (∑ i ∈ range (n + 1 - x), ↑((n + 1 - x).choose i) * _root_.bernoulli i) • (monomial x) ↑((n + 1).choose x) = 0
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n p : ℕ
⊢ ∀ x ∈ range (p + 1),
    _root_.bernoulli (p.succ - (p + 1 - x)) * ↑(p.succ.choose (p + 1 - x)) * ↑n ^ (p + 1 - x) =
      _root_.bernoulli x * ↑((p + 1).choose x) * ↑n ^ (p + 1 - x)

Tactic:
intro x

Goal state after:
n p x : ℕ
⊢ x ∈ range (p + 1) →
    _root_.bernoulli (p.succ - (p + 1 - x)) * ↑(p.succ.choose (p + 1 - x)) * ↑n ^ (p + 1 - x) =
      _root_.bernoulli x * ↑((p + 1).choose x) * ↑n ^ (p + 1 - x)
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case a.a
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (1 + X) = bernoulli m + m • X ^ (m - 1)
x✝ : ℕ
a✝ : x✝ ∈ range (d + 1)
| (d + 2).choose x✝ • (bernoulli x✝).comp (1 + X)

Tactic:
hd _ (mem_range.1 (by assumption))

Goal state after:
case a.a
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (1 + X) = bernoulli m + m • X ^ (m - 1)
x✝ : ℕ
a✝ : x✝ ∈ range (d + 1)
| (d + 2).choose x✝ • (bernoulli x✝ + x✝ • X ^ (x✝ - 1))
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n ↦ bernoulli' n / ↑n !
h : B * (exp ℚ - 1) = X * exp ℚ
⊢ evalNegHom B * (exp ℚ - 1) = X * 1

Tactic:
← neg_sub,

Goal state after:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n ↦ bernoulli' n / ↑n !
h : B * (exp ℚ - 1) = X * exp ℚ
⊢ evalNegHom B * -(1 - exp ℚ) = X * 1
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)
⊢ ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))

Tactic:
intro x

Goal state after:
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)
x : ℝ
⊢ 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: case hf
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
⊢ ∀ x ∈ Finset.range (2 * n + 1), x ∉ Finset.range (2 * n / 3 + 1) → x ^ n.centralBinom.factorization x = 1

Tactic:
intro x

Goal state after:
case hf
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
x : ℕ
⊢ x ∈ Finset.range (2 * n + 1) → x ∉ Finset.range (2 * n / 3 + 1) → x ^ n.centralBinom.factorization x = 1
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ Monotone ψ

Tactic:
intro x

Goal state after:
x : ℝ
⊢ ∀ ⦃b : ℝ⦄, x ≤ b → ψ x ≤ ψ b
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ Monotone θ

Tactic:
intro x

Goal state after:
x : ℝ
⊢ ∀ ⦃b : ℝ⦄, x ≤ b → θ x ≤ θ b
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: case convert_6
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
a : S
y : ℤ
hy : ∀ (k : ι), abv ((bS.repr a) k) ≤ y
i j k : ι
⊢ abv ((LinearMap.toMatrix bS bS) ((Algebra.lmul R S) (bS i)) j k) ≤
    (Finset.image (fun ijk ↦ abv ((Algebra.leftMulMatrix bS) (bS ijk.1) ijk.2.1 ijk.2.2)) Finset.univ).max' ⋯

Tactic:
apply Finset.le_max'

Goal state after:
case convert_6
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
a : S
y : ℤ
hy : ∀ (k : ι), abv ((bS.repr a) k) ≤ y
i j k : ι
⊢ abv ((LinearMap.toMatrix bS bS) ((Algebra.lmul R S) (bS i)) j k) ∈
    Finset.image (fun ijk ↦ abv ((Algebra.leftMulMatrix bS) (bS ijk.1) ijk.2.1 ijk.2.2)) Finset.univ
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case e_s
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k : ℕ
x✝ : k ∈ Icc 1 N
p : ℕ
⊢ ((0 < p ∧ p ≤ ⌊x⌋₊) ∧ Nat.Prime p) ∧ p ≤ ⌊x ^ (↑k)⁻¹⌋₊ ↔ (0 < p ∧ p ≤ ⌊x ^ (1 / ↑k)⌋₊) ∧ Nat.Prime p

Tactic:
refine ⟨fun _ ↦ (by simp_all), fun h ↦ ?_⟩

Goal state after:
case e_s
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k : ℕ
x✝ : k ∈ Icc 1 N
p : ℕ
h : (0 < p ∧ p ≤ ⌊x ^ (1 / ↑k)⌋₊) ∧ Nat.Prime p
⊢ ((0 < p ∧ p ≤ ⌊x⌋₊) ∧ Nat.Prime p) ∧ p ≤ ⌊x ^ (↑k)⁻¹⌋₊
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
⊢ ¬p ∣ (bernoulli (2 * k) + ∑ q ∈ vonStaudtPrimes k, 1 / ↑q).den

Tactic:
rw [sum_one_div_prime_eq_indicator_div_add (p := p) hk, ← add_assoc]

Goal state after:
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
⊢ ¬p ∣ (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / ↑p + ∑ q ∈ vonStaudtPrimes k with q ≠ p, 1 / ↑q).den
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
grind [theta_eq_zero_iff, psi_eq_zero_iff, psi_nonneg]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case h
⊢ ∀ (x : ℝ), ψ x - θ x ≤ (log 4 + 4) * 3 * √x

Tactic:
intro x

Goal state after:
case h
x : ℝ
⊢ ψ x - θ x ≤ (log 4 + 4) * 3 * √x
Module: Mathlib.NumberTheory.Padics.RingHoms

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

Tactic:
norm_natCast_zmodRepr_eq_one_iff,

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ‖x‖ = 1 ↔ x.zmodRepr ≠ 0
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: case refine_1
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 S)⁰

Tactic:
rw [mem_nonZeroDivisors_iff_ne_zero]

Goal state after:
case refine_1
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 ≠ 0
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]), ↑(f (x * y)) = ↑(f x) * ↑(f y)

Tactic:
intro x

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 : ℤ_[p]
⊢ ∀ (y : ℤ_[p]), ↑(f (x * y)) = ↑(f x) * ↑(f y)
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]), ↑(f (x + y)) = ↑(f x) + ↑(f y)

Tactic:
intro x

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 : ℤ_[p]
⊢ ∀ (y : ℤ_[p]), ↑(f (x + y)) = ↑(f x) + ↑(f y)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
⊢ θ x = ↑(π ⌊x⌋₊) * log x - ∫ (t : ℝ) in 2..x, ↑(π ⌊t⌋₊) / t

Tactic:
by
  -- Rewrite in a form to which Abel summation can be applied
  rw [theta_eq_sum_Icc, sum_filter]
  let a : ℕ → ℝ := Set.indicator (Set.ofPred Nat.Prime) (fun n ↦ 1)
  trans ∑ n ∈ Icc 0 ⌊x⌋₊, log n * a n
  · refine sum_congr rfl fun n _ ↦ ?_
    split_ifs with h <;> simp [a, h]
  rw [sum_mul_eq_sub_integral_mul₁ a (by simp [a, not_prime_zero])
    (by simp [a, not_prime_one]) _ (fun z ⟨hz, _⟩ ↦ (by fun_prop (disch := linarith))) ?hint,
    ← intervalIntegral.integral_of_le hx]
  case hint =>
    rw [deriv_log']
    refine ContinuousOn.integrableOn_Icc ?_
    fun_prop (disch := grind)
  -- Rewrite the derivative inside the integral
  simp only [primeCounting, primeCounting', count_eq_card_filter_range]
  have int_deriv (f : ℝ → ℝ) :
      ∫ u in 2..x, deriv (fun x ↦ log x) u * f u =
      ∫ u in 2..x, f u / u :=
    intervalIntegral.integral_congr fun u _ ↦ by rw [deriv_log, mul_comm, div_eq_mul_inv]
  rw [int_deriv]
  simp [a, Set.indicator_apply, range_succ_eq_Icc_zero, mul_comm]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 4 ≤ x
⊢ 2 ^ 2 ≤ x

Tactic:
by norm_num [hx]

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

Goal state before:
pp: case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)
⊢ ∀ (x : ℤ_[p]), ↑p ^ (n + 1) ∣ x - ↑(x.appr (n + 1))

Tactic:
intro x

Goal state after:
case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)
x : ℤ_[p]
⊢ ↑p ^ (n + 1) ∣ x - ↑(x.appr (n + 1))
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ (∫ (x : ℝ) in 2..√x, 1 / log x ^ 2) + ∫ (x : ℝ) in √x..x, 1 / log x ^ 2 ≤ 4 * x / log x ^ 2 + √x / log 2 ^ 2

Tactic:
grw [integral_1_div_log_sq_le two_le_sqrt (by linarith),
      integral_1_div_log_sq_le sqrt_le_x (by linarith)]

Goal state after:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ (√x - 2) / log 2 ^ 2 + (x - √x) / log √x ^ 2 ≤ 4 * x / log x ^ 2 + √x / log 2 ^ 2
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: A : Type u
B : Type v
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
ι' : Type u_1
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι'
b : Basis ι A B
f : ι ≃ ι'
⊢ discr A (⇑b ∘ ⇑f.symm) = discr A ⇑b

Tactic:
← Basis.coe_reindex,

Goal state after:
A : Type u
B : Type v
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
ι' : Type u_1
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι'
b : Basis ι A B
f : ι ≃ ι'
⊢ discr A ⇑(b.reindex f) = discr A ⇑b
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ ∀ᶠ (x : ℝ) in atTop, ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖ ≤ log 4 * ‖∫ (t : ℝ) in 2..x, 1 / log t ^ 2‖

Tactic:
filter_upwards [eventually_ge_atTop 4] with x _

Goal state after:
x : ℝ
a✝ : 4 ≤ x
⊢ ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖ ≤ log 4 * ‖∫ (t : ℝ) in 2..x, 1 / log t ^ 2‖
Module: Mathlib.NumberTheory.Padics.RingHoms

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

Tactic:
intro x

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
⊢ ∀ (a b : ℕ), x - ↑a ∈ Ideal.span {↑(p ^ n)} → x - ↑b ∈ Ideal.span {↑(p ^ n)} → ↑a = ↑b
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
⊢ DenseRange Nat.cast

Tactic:
intro x

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ x ∈ closure (Set.range Nat.cast)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ∀ ε > 0, ∃ k, dist x ↑k < ε

Tactic:
intro ε hε

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
ε : ℝ
hε : ε > 0
⊢ ∃ k, dist x ↑k < ε
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
⊢ DenseRange Int.cast

Tactic:
intro x

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ x ∈ closure (Set.range Int.cast)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ θ x ≤ ↑(π ⌊x⌋₊) * log x

Tactic:
grw [← psi_le_primeCounting_mul_log', theta_le_psi]

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

Goal state before:
pp: case pos
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)
⊢ ∀ (ib : ℝ),
    0 < ib →
      ∃ ia ∈ galGroupBasis K L,
        ∀ x ∈ id ia,
          ((Units.coeHom ℤ_[p]).comp ((cyclotomicCharacter L p).comp (MulSemiringAction.toRingAut Gal(L/K) L))) x ∈
            Metric.ball 1 ib

Tactic:
intro ε hε

Goal state after:
case pos
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 < ε
⊢ ∃ ia ∈ galGroupBasis K L,
    ∀ x ∈ id ia,
      ((Units.coeHom ℤ_[p]).comp ((cyclotomicCharacter L p).comp (MulSemiringAction.toRingAut Gal(L/K) L))) x ∈
        Metric.ball 1 ε
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
⊢ IsCauSeq (padicNorm p) fun n ↦ ↑(nthHom f r n)

Tactic:
intro ε hε

Goal state after:
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
ε : ℚ
hε : ε > 0
⊢ ∃ i, ∀ j ≥ i, padicNorm p ((fun n ↦ ↑(nthHom f r n)) j - (fun n ↦ ↑(nthHom f r n)) i) < ε
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
⊢ nthHomSeq f_compat 1 ≈ 1

Tactic:
intro ε hε

Goal state after:
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
ε : ℚ
hε : ε > 0
⊢ ∃ i, ∀ j ≥ i, padicNorm p (↑(nthHomSeq f_compat 1 - 1) j) < ε
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
⊢ ((MulSemiringAction.toRingAut Gal(L/K) L) σ) ↑(⋯.unit ^ i) = ↑(⋯.unit ^ i)

Tactic:
exact hσ ⟨ζ k ^ i, pow_mem (mem_adjoin_simple_self K (ζ k)) _⟩

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 s : R
⊢ nthHomSeq f_compat (r + s) ≈ nthHomSeq f_compat r + nthHomSeq f_compat s

Tactic:
intro ε hε

Goal state after:
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 s : R
ε : ℚ
hε : ε > 0
⊢ ∃ i, ∀ j ≥ i, padicNorm p (↑(nthHomSeq f_compat (r + s) - (nthHomSeq f_compat r + nthHomSeq f_compat s)) j) < ε
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 s : R
⊢ nthHomSeq f_compat (r * s) ≈ nthHomSeq f_compat r * nthHomSeq f_compat s

Tactic:
intro ε hε

Goal state after:
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 s : R
ε : ℚ
hε : ε > 0
⊢ ∃ i, ∀ j ≥ i, padicNorm p (↑(nthHomSeq f_compat (r * s) - nthHomSeq f_compat r * nthHomSeq f_compat s) j) < ε
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ε

Goal state after:
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
ε : ℝ
hε : 0 < ε
⊢ ∃ N, ∀ n ≥ N, ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε
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
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), (toZModPow n).comp g = f n
r : R
⊢ ∀ ε > 0, dist ((lift f_compat) r) (g r) ≤ ε

Tactic:
intro ε hε

Goal state after:
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
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), (toZModPow n).comp g = f n
r : R
ε : ℝ
hε : ε > 0
⊢ dist ((lift f_compat) r) (g r) ≤ ε
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: f : ℕ → ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i
⊢ IsCauSeq (padicNorm p) fun x ↦ ↑(f x)

Tactic:
intro ε hε

Goal state after:
f : ℕ → ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i
ε : ℚ
hε : ε > 0
⊢ ∃ i, ∀ j ≥ i, padicNorm p ((fun x ↦ ↑(f x)) j - (fun x ↦ ↑(f x)) i) < ε
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
h : d a1 = n * n
⊢ n * n + 1 = a * a

Tactic:
by rw [← h]; exact Nat.succ_pred_eq_of_pos (asq_pos a1)

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : 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 : (α → ℕ) → ℤ
pf : IsPoly f
⊢ C ⟨f, pf⟩

Tactic:
induction pf with

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ yn a1 n
hp : n % m > 0
co : (yn a1 m).Coprime (xn a1 (m * (n / m)))
e : m = 0
⊢ False

Tactic:
by
            rw [e, Nat.mod_zero] at hp;rw [e] at h
            exact _root_.ne_of_lt (strictMono_y a1 hp) (eq_zero_of_zero_dvd h).symm

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

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

Tactic:
exact Int.ofNat_le.1 (le_of_neg_le_neg (Int.le.intro y (by simp [add_comm, *])))

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

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

Tactic:
have : Nonneg ⟨_, _⟩ :=
      nonnegg_pos_neg.2 (sqLe_add (nonnegg_pos_neg.1 ha) (nonnegg_pos_neg.1 hb))

Goal state after:
case inr.inl.inr.inl
d x y : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
z w : ℕ
hb : { re := ↑z, im := -↑w }.Nonneg
this : { re := ↑(x + z), im := -↑(y + w) }.Nonneg
⊢ ({ re := ↑x, im := -↑y } + { re := ↑z, im := -↑w }).Nonneg