mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.PowerSeries.Exp

Goal state before:
pp: case e'_3
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ 1 = (rescale (1 + -1)) (exp A)

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: X : Type u_1
E : Type u_2
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure X
f : X → E
hf : Integrable f μ
hE : Nontrivial E
this✝ : IsFiniteMeasure (μ.withDensity fun x ↦ ‖f x‖ₑ)
I : VectorMeasure.Integrable (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure fun x ↦ ‖f x‖⁻¹ • f x
this :
  μ.withDensityᵥ f =
    withDensity (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure (fun x ↦ ‖f x‖⁻¹ • f x)
      (ContinuousLinearMap.lsmul ℝ ℝ).flip
x : X
hx : f x ≠ 0
h'x : ‖f x‖ ≠ 0
⊢ ‖f x‖ₑ ≠ ∞

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
⊢ (if 0 ≤ n then _root_.bernoulli (n - 0) * ↑(n.choose 0) else 0) = _root_.bernoulli n

Tactic:
if_pos (Nat.zero_le n),

Goal state after:
n : ℕ
⊢ _root_.bernoulli (n - 0) * ↑(n.choose 0) = _root_.bernoulli n
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case zero
n : ℕ
hd : ∀ m < 0, (bernoulli m).comp (1 + X) = bernoulli m + m • X ^ (m - 1)
⊢ (bernoulli 0).comp (1 + X) = bernoulli 0 + 0 • X ^ (0 - 1)

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: ⊢ 1 - ∑ k ∈ range 0, ↑(Nat.choose 0 k) / (↑0 - ↑k + 1) * bernoulli' k = 1

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case zero
⊢ ∑ k ∈ range 0, ↑(Nat.choose 0 k) * bernoulli' k = ↑0

Tactic:
simp

Goal state after:
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) • X ^ (d + 1)).comp (1 + X) - ∑ i ∈ range (d + 1), ((d + 2).choose i • bernoulli i).comp (1 + X)

Tactic:
congr
    · skip
    · apply_congr
      · skip
      · rw [smul_comp, hd _ (mem_range.1 (by assumption))]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case zero
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ (coeff 0) (bernoulli'PowerSeries A * (exp A - 1)) = (coeff 0) (X * exp A)

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case zero
⊢ (bernoulli 0).comp (-X) = (-1) ^ 0 • (bernoulli 0 + 0 • X ^ (0 - 1))

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case pos
i : ℕ
h : i ≤ i + 1
⊢ _root_.bernoulli (i + 1 - i) * ↑((i + 1).choose i) * (-1) ^ i =
    (-1) ^ (i + 1) • (_root_.bernoulli (i + 1 - i) * ↑((i + 1).choose i) + (i + 1) • 1)

Tactic:
simp

Goal state after:
case pos
i : ℕ
h : i ≤ i + 1
⊢ -1 / 2 * (↑i + 1) * (-1) ^ i = (-1) ^ (i + 1) * (-1 / 2 * (↑i + 1)) + ((-1) ^ (i + 1) * ↑i + (-1) ^ (i + 1))
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: m : ℕ
ihn : ∀ m_1 < m + m + 1, m_1 ≠ 0 → m_1# < 4 ^ m_1
hn : m + m + 1 ≠ 0
hm : m > 0
⊢ 0 < 4 ^ m

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case zero
⊢ ∑ k ∈ range 0, ↑(Nat.choose 0 k) * bernoulli k = if 0 = 1 then 1 else 0

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ.zero
⊢ ∑ k ∈ range (0 + 1), ↑((0 + 1).choose k) * bernoulli k = if 0 + 1 = 1 then 1 else 0

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case zero
⊢ ∑ k ∈ antidiagonal 0, ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli k.1 = if 0 = 0 then 1 else 0

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case neg
n i : ℕ
h : ¬i ≤ n + 1
h✝ : ¬i = n + 1 - 1
⊢ 0 * (-1) ^ i = (-1) ^ (n + 1) • (0 + (n + 1) • 0)

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case zero
⊢ (bernoulli 0).comp (1 - X) = (-1) ^ 0 * bernoulli 0

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case zero
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
⊢ (PowerSeries.coeff 0) ((PowerSeries.mk fun n ↦ (aeval t) ((1 / ↑n !) • bernoulli n)) * (exp A - 1)) =
    (PowerSeries.coeff 0) (PowerSeries.X * (rescale t) (exp A))

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case zero
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ (coeff 0) (bernoulliPowerSeries A * (exp A - 1)) = (coeff 0) X

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ.zero
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ (algebraMap ℚ A) (bernoulli (0 + 1) / ((↑0 + 1) * ↑0!)) * ((algebraMap ℚ A) (↑0 + 1)⁻¹ - 1) +
      (algebraMap ℚ A) (∑ x ∈ antidiagonal 0, bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹) =
    if 0 + 1 = 1 then 1 else 0

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hc1 : c 1 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 2 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 2 b) volume
hb : 2 ≤ b
this : 2 ≤ ⌊b⌋₊
H : ∑ k ∈ Icc 0 ⌊b⌋₊, f ↑k * c k = f ↑2 * c 2 + ∑ k ∈ Ioc 2 ⌊b⌋₊, f ↑k * c k
⊢ 2 = ⌊2⌋₊

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case h
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p ↦ bernoulli p / ↑p !) * PowerSeries.mk fun q ↦ (coeff (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
⊢ ¬(coeff 1) ((PowerSeries.mk fun n ↦ (algebraMap ℚ ℚ) (1 / ↑n !)) - 1) = (coeff 1) 0

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p ↦ bernoulli p / ↑p !) * PowerSeries.mk fun q ↦ (coeff (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
⊢ C (constantCoeff (exp ℚ ^ n)) = 1

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case succ.calc_3
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
h_bdd : (fun n ↦ ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖) =O[atTop] fun x ↦ 1
hf_int : LocallyIntegrableOn (deriv fun t ↦ ‖f t‖) (Set.Ici ↑m) volume
hf :
  ∀ (n : ℕ),
    ∑ k ∈ Icc 0 n, ‖f ↑k‖ * ‖c k‖ =
      ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖ - ∫ (t : ℝ) in Set.Ioc ↑m ↑n, deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖
g : ℝ → ℝ
hg₁ : (fun t ↦ deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
C₁ : ℝ
hC₁ : ∀ (n : ℕ), ‖‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖‖ ≤ C₁
C₂ : ℝ := ∫ (t : ℝ) in Set.Ioi ↑m, ‖deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖‖
n : ℕ
⊢ C₁ + ∫ (a : ℝ) in Set.Ioc ↑m ↑n, |deriv (fun t ↦ ‖f t‖) a * ∑ k ∈ Icc 0 ⌊a⌋₊, ‖c k‖| ≤
    C₁ + ∫ (t : ℝ) in Set.Ioc ↑m ↑n, ‖deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖‖

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Finite ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : ι → R
h✝ : abv.IsAdmissible
n : ℕ
e : ι ≃ Fin n
t : Fin n → Fin (h✝.card ε)
ht : ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(abv ((A ∘ ⇑e.symm) i₁ % b - (A ∘ ⇑e.symm) i₀ % b)) < abv b • ε
i₀ i₁ : ι
h : (t ∘ ⇑e) i₀ = (t ∘ ⇑e) i₁
⊢ ↑(abv (A i₁ % b - A i₀ % b)) < abv b • ε

Tactic:
convert! (config := { transparency := .default }) ht (e i₀) (e i₁) h <;>
    simp only [e.symm_apply_apply]

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

Goal state before:
pp: case zero.refine_1
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : abv.IsAdmissible
this : DecidableEq R
ε : ℝ
_hε : 0 < ε
b : R
_hb : b ≠ 0
A : Fin (h.card ε ^ 0).succ → Fin 0 → R
⊢ 0 ≠ 1

Tactic:
simp

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
⊢ ↑(p ^ e * M') = ↑(p ^ e) * ↑M'

Tactic:
simp

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'
⊢ ↑(p ^ (N - e)) / ↑M' = ↑(NNRat.divNat (p ^ (N - e)) M')

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
x✝¹ : ℕ
x✝ : x✝¹ ∈ Ioc 0 ⌊x⌋₊
⊢ 0 ≤ Λ x✝¹

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ ∑ n ∈ Ioc 0 ⌊x⌋₊, Λ n = Λ 0 + ∑ x ∈ Ioc 0 ⌊x⌋₊, Λ x

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ 0 ≤ ⌊x⌋₊

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ (∑ a ∈ Ioc 0 ⌊x⌋₊, if Nat.Prime a then log ↑a else 0) =
    (if Nat.Prime 0 then log ↑0 else 0) + ∑ x ∈ Ioc 0 ⌊x⌋₊, if Nat.Prime x then log ↑x else 0

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case hf
x y : ℝ
hxy : x ≤ y
⊢ ∀ i ∈ Ioc 0 ⌊y⌋₊, i ∉ Ioc 0 ⌊x⌋₊ → 0 ≤ Λ i

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ ∑ p ∈ n.primesLE, ∑ k ∈ Icc 1 (Nat.log p n), log ↑p = ∑ p ∈ n.primesLE, ↑(Nat.log p n) * log ↑p

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case inl
⊢ ∑ p ∈ primesLE 0, ↑(Nat.log p 0) * log ↑p ≤ ∑ _x ∈ primesLE 0, log ↑0

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ ∑ k ∈ range (n + 1), n.lcmUpto = (n + 1) * n.lcmUpto

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case neg
k m p : ℕ
hm_lt : m < k
inst✝ : Fact (Nat.Prime p)
ih : pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p)
hp_ne : ↑p ≠ 0
P : ℚ := ↑p ^ (2 * k - 2 * m - 1)
hpow : ↑p ^ (2 * k - 2 * m) = P * ↑p
hdecomp :
  bernoulli (2 * m) * ↑((2 * k + 1).choose (2 * m)) * ↑p ^ (2 * k - 2 * m) / (2 * ↑k + 1) =
    (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p) * ↑((2 * k + 1).choose (2 * m)) * ↑p ^ (2 * k - 2 * m) /
        (2 * ↑k + 1) -
      vonStaudtIndicator (2 * m) p * ↑((2 * k + 1).choose (2 * m)) * P / (2 * ↑k + 1)
hcmp : pIntegral p (↑((2 * k).choose (2 * m)) * ↑p ^ (2 * k - 2 * m - 1) / (2 * ↑k - 2 * ↑m + 1))
H : ∀ (x : ℚ), ↑((2 * k + 1).choose (2 * m)) * x / (2 * ↑k + 1) = ↑((2 * k).choose (2 * m)) * x / (2 * ↑k - 2 * ↑m + 1)
h✝ : ¬p - 1 ∣ 2 * m
⊢ (Rat.padicValuation p) (0 * ↑((2 * k + 1).choose (2 * m)) * P / (2 * ↑k + 1)) ≤ 1

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case e_a
x : ℝ
hx : 2 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ x ^ (1 / ↑1) = x

Tactic:
simp

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), μ j • a = b • ∑ i, qs j i • bS i + ∑ i, rs j i • bS i

Tactic:
intro j

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
⊢ μ j • a = b • ∑ i, qs j i • bS i + ∑ i, rs j i • bS i
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case neg
x : ℝ
n : ℕ
hn : n ∈ Ioc 0 ⌊x⌋₊
h : ¬Nat.Prime n
⊢ Λ n - 0 = Λ n

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case inl
⊢ ↑0 * log 2 - log (↑0 + 1) - 2 * √↑0 * log ↑0 ≤ θ ↑0

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
simp

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

Goal state before:
pp: case e'_4
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
⊢ ↑p = |↑p|

Tactic:
simp

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
rdcp : r.den.Coprime p
⊢ ↑r.num - ↑r.num * ↑(r.den.gcd p) = 0

Tactic:
by
    rw [rdcp.gcd_eq_one]
    simp only [mul_one, cast_one, sub_self]

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

Goal state before:
pp: case e'_4
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
n : ℤ := modPart p r
this : ↑p ∣ r.num - n * ↑r.den
⊢ ↑(r * ↑r.den) = ↑r.num

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
rcases le_total x 1 with h | h

Goal state after:
case h.inl
x : ℝ
h : x ≤ 1
⊢ ψ x - θ x ≤ (log 4 + 4) * 3 * √x

case h.inr
x : ℝ
h : 1 ≤ x
⊢ ψ x - θ x ≤ (log 4 + 4) * 3 * √x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ ∃ C, ∀ (x : ℝ), ψ x - θ x ≤ C * √x

Tactic:
by
  use (log 4 + 4) * 3
  intro x
  rcases le_total x 1 with h | h
  · rw [theta_eq_zero_of_le_one h, psi_eq_zero_of_le_one h, sub_self]; positivity
  have (n : ℕ) (hn : 2 ≤ n) : ψ (x ^ (1 / (n : ℝ))) ≤ (log 4 + 4) * x.sqrt := by
    grw [psi_le_const_mul_self (by positivity), sqrt_eq_rpow x]; gcongr; norm_cast
  linarith [psi_sub_theta_le_psi_add_psi_add_psi x, this 2 (le_refl _), this 3 (by norm_num),
    this 5 (by norm_num)]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x✝ x : ℝ
hx : x ∈ Set.Icc 2 x✝
this : x ≠ 0
⊢ log x ^ 2 ≠ 0

Tactic:
simp

Goal state after:
x✝ x : ℝ
hx : x ∈ Set.Icc 2 x✝
this : x ≠ 0
⊢ ¬x = 0 ∧ ¬x = 1 ∧ ¬x = -1
Module: Mathlib.NumberTheory.Padics.RingHoms

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

Tactic:
simp

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ↑x.zmodRepr - ↑x.zmodRepr ∈ maximalIdeal ℤ_[p]

Tactic:
simp

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

Goal state before:
pp: case zero
p : ℕ
hp_prime : Fact (Nat.Prime p)
hn : OfNat.ofNat 0 < p
⊢ OfNat.ofNat 0 = ↑(OfNat.ofNat 0)

Tactic:
simp

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

Goal state before:
pp: case succ.zero
p : ℕ
hp_prime : Fact (Nat.Prime p)
hn : OfNat.ofNat (0 + 1) < p
⊢ OfNat.ofNat (0 + 1) = ↑(OfNat.ofNat (0 + 1))

Tactic:
simp

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

Goal state before:
pp: case succ.succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
hn : OfNat.ofNat (n + 1 + 1) < p
⊢ OfNat.ofNat (n + 1 + 1) = ↑(OfNat.ofNat (n + 1 + 1))

Tactic:
simp

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

Goal state before:
pp: p' : ℕ
hp_prime : Fact (Nat.Prime (0 + p' + 1))
x : ℤ_[0 + p' + 1]
⊢ x.zmodRepr < (0 + p').succ

Tactic:
simpa only [zero_add] using zmodRepr_lt_p x

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: a b : ℝ
hab : a ≤ b
one_lt : 1 < a
⊢ IntervalIntegrable (fun x ↦ 1 / log a ^ 2) volume a b

Tactic:
simp

Goal state after:
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
inst✝¹ : Fintype ι
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i, g i • b i = 0
i✝ : ι
hi : g i✝ ≠ 0
i : ι
⊢ ∀ (j : ι), (trace A B) (b i * b j) * g j = (trace A B) (g j • b j * b i)

Tactic:
intro j

Goal state after:
A : Type u
B : Type v
ι : Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype ι
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i, g i • b i = 0
i✝ : ι
hi : g i✝ ≠ 0
i j : ι
⊢ (trace A B) (b i * b j) * g j = (trace A B) (g j • b j * b i)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 4 ≤ x
t : ℝ
ht : t ∈ Set.uIcc 2 x
⊢ (fun x ↦ |1 / log x ^ 2|) t = (fun t ↦ 1 / log t ^ 2) t

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ ∀ᶠ (x : ℝ) in atTop, x / log x = 0 → x / log x ^ 2 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
⊢ ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2) = (θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)) - θ x / log x

Tactic:
simp

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

Goal state before:
pp: case inr
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
this✝ : 1 ≤ Nat.card ↥(rootsOfUnity n L)
h : 1 = Nat.card ↥(rootsOfUnity n L)
this : Subsingleton ↥(rootsOfUnity n L)
⊢ (RingEquiv.refl L) ↑↑1 = ↑(↑1 ^ ZMod.val 1)

Tactic:
simp

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ((toZModPow n) x).cast = ((ZMod.castHom ⋯ (ZMod (p ^ m))).comp (toZModPow n)) x

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case inl
⊢ (↑0 * log 2 - log (↑0 + 1)) / log ↑0 ≤ ↑(π 0)

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case inr.inl
⊢ (↑1 * log 2 - log (↑1 + 1)) / log ↑1 ≤ ↑(π 1)

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ ↑(π ⌊x⌋₊) * log √x = ∑ p ∈ ⌊x⌋₊.primesLE, log √x

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ ⌊√x⌋₊ = #(Icc 1 ⌊√x⌋₊)

Tactic:
simp

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

Goal state before:
pp: 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 : ↑p ^ (-↑k) < ε
⊢ k + 1 ≠ 0

Tactic:
simp

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

Goal state before:
pp: case h
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
k : ℕ
hk : ↑p ^ (-↑k) < ε
⊢ ∀ j ≥ k, padicNorm p ((fun n ↦ ↑(nthHom f r n)) j - (fun n ↦ ↑(nthHom f r n)) k) < ε

Tactic:
intro j

Goal state after:
case h
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
k : ℕ
hk : ↑p ^ (-↑k) < ε
j : ℕ
⊢ j ≥ k → padicNorm p ((fun n ↦ ↑(nthHom f r n)) j - (fun n ↦ ↑(nthHom f r n)) k) < ε
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)
⊢ ↑2 ≠ 0

Tactic:
simp

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

Goal state before:
pp: case h
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 < ε
⊢ ∀ j ≥ 1, padicNorm p (↑(nthHomSeq f_compat 1 - 1) j) < ε

Tactic:
intro j

Goal state after:
case h
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 < ε
j : ℕ
⊢ j ≥ 1 → padicNorm p (↑(nthHomSeq f_compat 1 - 1) j) < ε
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case h
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
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ ∀ j ≥ n, padicNorm p (↑(nthHomSeq f_compat (r + s) - (nthHomSeq f_compat r + nthHomSeq f_compat s)) j) < ε

Tactic:
intro j

Goal state after:
case h
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
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
⊢ j ≥ n → padicNorm p (↑(nthHomSeq f_compat (r + s) - (nthHomSeq f_compat r + nthHomSeq f_compat s)) j) < ε
Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
L : Type u_2
inst✝¹ : Field L
inst✝ : NumberField L
f : K ≃+* L
x✝ : ℚ
⊢ f ((algebraMap ℚ K) x✝) = (algebraMap ℚ L) x✝

Tactic:
simp

Goal state after: