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

Goal state before:
pp: n : ℕ
⊢ n.primesBelow = filter Prime (Ioo 1 n)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ n.primesLE = filter Prime (Ioc 1 n)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ n.primesBelow = filter Prime (Ico 2 n)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ n.primesLE = filter Prime (Icc 2 n)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: ⊢ Monotone primesBelow

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: ⊢ Monotone primesLE

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ (n + 1).primesBelow = if Prime n then insert n n.primesBelow else n.primesBelow

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ #n.primesBelow = π' n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ #n.primesLE = π n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
hf_diff : ∀ t ∈ Set.Icc 0 ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 0 ↑m) volume
⊢ ∑ k ∈ Icc 0 m, f ↑k * c k = f ↑m * ∑ k ∈ Icc 0 m, c k - ∫ (t : ℝ) in Set.Ioc 0 ↑m, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: a k : ℕ
h0 : a ≠ 0
h1 : a < k
n : ℕ
⊢ π' (k + n) ≤ #({p ∈ range k | Prime p}) + #({p ∈ Ico k (k + n) | Prime p})

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: a k : ℕ
h0 : a ≠ 0
h1 : a < k
n : ℕ
⊢ #({p ∈ range k | Prime p}) + #({p ∈ Ico k (k + n) | Prime p}) ≤ π' k + #({p ∈ Ico k (k + n) | Prime p})

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: a k : ℕ
h0 : a ≠ 0
h1 : a < k
n : ℕ
⊢ π' k + #({p ∈ Ico k (k + n) | Prime p}) ≤ π' k + #({b ∈ Ico k (k + n) | a.Coprime b})

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: a k : ℕ
h0 : a ≠ 0
h1 : a < k
n : ℕ
⊢ π' k + #({b ∈ Ico k (k + n) | a.Coprime b}) ≤ π' k + φ a * (n / a + 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: a k : ℕ
h0 : a ≠ 0
h1 : a ≤ k
n : ℕ
⊢ π (k + n) ≤ π k + φ a * (n / a + 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n x : ℕ
hx : x ∈ range n
⊢ n + 1 - x ≠ 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
⊢ ∑ k ∈ range (n + 1), ↑((n + 1).choose k) • bernoulli k = (monomial n) (↑n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
⊢ (n + 1) • bernoulli n = (n + 1) • X ^ n - ∑ k ∈ range n, (n + 1).choose k • bernoulli k

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
← sum_sub_distrib,

Goal state after:
n : ℕ
⊢ 1 -
      ∑ x ∈ range n,
        (↑(n.choose x) / (↑n - ↑x + 1) * bernoulli' x - ↑(n.choose (n - x)) / (↑n - ↑x + 1) * bernoulli' x) =
    1
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
⊢ n#.primeFactors = n.primesLE

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: ⊢ 0# = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: ⊢ 1# = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: ⊢ 2# = 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: m n : ℕ
h : m ≤ n
⊢ {p ∈ range (m + 1) | Nat.Prime p} ⊆ {p ∈ range (n + 1) | Nat.Prime p}

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n p : ℕ
⊢ eval (↑n) (bernoulli p.succ) = _root_.bernoulli p.succ + (↑p + 1) * ∑ k ∈ range n, ↑k ^ p

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n x : ℕ
hx : x ∈ range n
⊢ ↑(n.choose x) / (↑n - ↑x + 1) * bernoulli' x - ↑(n.choose (n - x)) / (↑n - ↑x + 1) * bernoulli' x = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: m n : ℕ
h : m ≤ n
⊢ ∀ i ∈ {p ∈ range (n + 1) | Nat.Prime p}, i ∉ {p ∈ range (m + 1) | Nat.Prime p} → 1 ≤ i

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
⊢ ∑ k ∈ antidiagonal n, ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli' k.1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: ⊢ bernoulli' 0 = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: ⊢ bernoulli' 1 = 1 / 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
hn1 : n ≠ 1
hn : Odd n
⊢ (n + 1)# = n#

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: ⊢ bernoulli' 2 = 1 / 6

Tactic:
by

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)
x✝ : ℕ
a✝ : x✝ ∈ range (d + 1)
⊢ x✝ ∈ range (d + 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: ⊢ bernoulli' 3 = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: ⊢ Nat.choose 4 2 = 6

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: ⊢ bernoulli' 4 = -1 / 30

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: m n : ℕ
⊢ m + 1 ≤ m + n + 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
this :
  (↑n + 1) * ∑ k ∈ range n, ↑(n.choose k) / (↑n - ↑k + 1) * bernoulli' k =
    ∑ x ∈ range n, ↑(n.succ.choose x) * bernoulli' x
⊢ ∑ k ∈ range (n + 1), ↑((n + 1).choose k) * bernoulli' k = ↑(n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: m n : ℕ
⊢ (m + n)# = m# * ∏ p ∈ Ico (m + 1) (m + n + 1) with Nat.Prime p, p

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n k : ℕ
hk : k ∈ range n
⊢ ↑(n - k) + 1 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: m n : ℕ
h : n ≤ m
p : ℕ
hp : p ∈ {p ∈ Ico (m + 1) (m + n + 1) | Nat.Prime p}
⊢ p ∣ (m + n).choose m

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: p n : ℕ
hp : Prime p
h : p ≤ n
⊢ p ∈ {p ∈ range (n + 1) | Prime p}

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: p n : ℕ
hp : Prime p
⊢ p ∣ n# ↔ p ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
hn : Squarefree n
⊢ n.primeFactors ⊆ {p ∈ range (n + 1) | Nat.Prime p}

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
hn : Squarefree n
⊢ n ∣ n#

Tactic:
by

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) - (d + 2) • X ^ (d + 1) = (d + 2) • ∑ i ∈ range (d + 1), (d + 1).choose i • X ^ i

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
hn : 2 < n
⊢ ∀ i ∈ {p ∈ range (n + 1) | Nat.Prime p}, 1 ≤ id i

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
hn : 2 < n
⊢ 3 ∈ {p ∈ range (n + 1) | Nat.Prime p}

Tactic:
by

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) • ∑ i ∈ range (d + 1), (d + 1).choose i • X ^ i =
    ∑ i ∈ range (d + 1), ((d + 2).choose (i + 1) * (i + 1)) • X ^ i

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
hn : 2 < n
this : 3 ≤ n#
q : ℕ := (n# - 1).minFac
h1 : q ≤ n
⊢ n# - 1 ≠ 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
hn : 2 < n
this : 3 ≤ n#
q : ℕ := (n# - 1).minFac
⊢ n < q

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
this : ∑ p ∈ antidiagonal n, bernoulli' p.1 / ↑p.1! * ((↑p.2 + 1) * ↑p.2!)⁻¹ = (↑n !)⁻¹
⊢ (coeff (n + 1, 0).1) (PowerSeries.mk fun n ↦ (algebraMap ℚ A) (bernoulli' n / ↑n !)) *
        (coeff (n + 1, 0).2) (exp A - 1) +
      ∑ p ∈ antidiagonal n,
        (coeff (p.1, p.2 + 1).1) (PowerSeries.mk fun n ↦ (algebraMap ℚ A) (bernoulli' n / ↑n !)) *
          (coeff (p.1, p.2 + 1).2) (exp A - 1) =
    (coeff (n + 1)) (exp A * X)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
hn : 2 < n
⊢ n < n#

Tactic:
by

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)
⊢ ∑ i ∈ range (d + 1), ((d + 2).choose (i + 1) * (i + 1)) • X ^ i =
    ∑ i ∈ range (d + 1), ((d + 2).choose i * i) • X ^ (i - 1) + ((d + 2).choose (d + 1) * (d + 1)) • X ^ (d + 1 - 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
⊢ n ≤ n#

Tactic:
by

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)
⊢ ∑ i ∈ range (d + 1), ((d + 2).choose i * i) • X ^ (i - 1) + ((d + 2).choose (d + 1) * (d + 1)) • X ^ (d + 1 - 1) =
    ∑ i ∈ range (d + 1), (d + 2).choose i • i • X ^ (i - 1) + ((d + 2) * (d + 1)) • X ^ (d + 1 - 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
⊢ (bernoulli n).comp (1 + X) = bernoulli n + n • X ^ (n - 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
x : ℚ
⊢ eval (1 + x) (bernoulli n) = eval x (bernoulli n) + ↑n * x ^ (n - 1)

Tactic:
by

Goal state after:
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
⊢ (m + m + 1)# = (m + 1 + m)#

Tactic:
by

Goal state after:
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 !
this : (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
⊢ bernoulli' n = 0

Tactic:
by

Goal state after:
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 !
⊢ B * (exp ℚ - 1) = X * exp ℚ

Tactic:
by

Goal state after:
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
⊢ (m + 1)# * (m + 1 + m).choose (m + 1) = (m + 1)# * (2 * m + 1).choose m

Tactic:
by

Goal state after:
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
⊢ m + 1 < m + m + 1

Tactic:
by

Goal state after:
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
⊢ m + 1 ≠ 0

Tactic:
by

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

Goal state after:
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 ℚ
this : evalNegHom (B * (exp ℚ - 1)) * exp ℚ = evalNegHom (X * exp ℚ) * exp ℚ
⊢ evalNegHom B * (1 - exp ℚ) = -(X * 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
h_odd : Odd n
hlt : 1 < n
⊢ bernoulli' n = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
⊢ bernoulli' n = (-1) ^ n * bernoulli n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: ⊢ bernoulli 0 = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: ⊢ bernoulli 1 = -1 / 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: ⊢ bernoulli 2 = 6⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
h_odd : Odd n
hlt : 1 < n
⊢ bernoulli n = 0

Tactic:
by

Goal state after:
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
⊢ 4 ^ (m + 1) * 4 ^ m ≤ 4 ^ (m + m + 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
hn : n ≠ 1
⊢ bernoulli n = bernoulli' n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
this : ∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2) = ↑n / 2
⊢ ∑ k ∈ range (n + 1 + 1), ↑((n + 1 + 1).choose k) * bernoulli k = if n + 1 + 1 = 1 then 1 else 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
ihn : ∀ m < n + 1, m ≠ 0 → m# < 4 ^ m
hn✝ : n + 1 ≠ 0
ho : Odd n
hn : n ≠ 1
⊢ n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n# < 4 ^ n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
⊢ (1, n) ∈ antidiagonal n.succ

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
h₁ : (1, n) ∈ antidiagonal n.succ
⊢ (1 + n).choose n = n + 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
⊢ n# ≤ 4 ^ n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
⊢ Squarefree (n#)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
m : ℕ
hf_diff : ∀ t ∈ Set.Icc 1 ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 1 ↑m) volume
⊢ ∑ k ∈ Icc 0 m, f ↑k * c k = f ↑m * ∑ k ∈ Icc 0 m, c k - ∫ (t : ℝ) in Set.Ioc 1 ↑m, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ
n : ℕ
h₁ : (1, n) ∈ antidiagonal n.succ
h₃ : (1 + n).choose n = n + 1
H :
  ↑(((1, n).1 + (1, n).2).choose (1, n).2) / (↑(1, n).2 + 1) * bernoulli' (1, n).1 +
      ∑ x ∈ antidiagonal n.succ \ {(1, n)}, ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli' x.1 =
    1
⊢ ↑(((1, n).1 + (1, n).2).choose (1, n).2) / (↑(1, n).2 + 1) * bernoulli (1, n).1 +
      ∑ x ∈ antidiagonal n.succ \ {(1, n)}, ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli x.1 =
    0

Tactic:
apply add_eq_of_eq_sub'

Goal state after:
case succ
n : ℕ
h₁ : (1, n) ∈ antidiagonal n.succ
h₃ : (1 + n).choose n = n + 1
H :
  ↑(((1, n).1 + (1, n).2).choose (1, n).2) / (↑(1, n).2 + 1) * bernoulli' (1, n).1 +
      ∑ x ∈ antidiagonal n.succ \ {(1, n)}, ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli' x.1 =
    1
⊢ ∑ x ∈ antidiagonal n.succ \ {(1, n)}, ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli x.1 =
    0 - ↑(((1, n).1 + (1, n).2).choose (1, n).2) / (↑(1, n).2 + 1) * bernoulli (1, n).1
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
⊢ (bernoulli n).comp (-X) = (-1) ^ n • (bernoulli n + n • X ^ (n - 1))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
x : ℚ
⊢ eval (-x) (bernoulli n) = (-1) ^ n * (eval x (bernoulli n) + ↑n * x ^ (n - 1))

Tactic:
by

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 : b < 2
⊢ ∀ n ∈ Icc 0 ⌊b⌋₊, c n = 0

Tactic:
by

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 : b < 2
H₁ : ∀ n ∈ Icc 0 ⌊b⌋₊, c n = 0
⊢ ∀ n ∈ Icc 0 ⌊b⌋₊, f ↑n * c n = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
h₁ : (1, n) ∈ antidiagonal n.succ
h₃ : (1 + n).choose n = n + 1
H :
  ↑(((1, n).1 + (1, n).2).choose (1, n).2) / (↑(1, n).2 + 1) * bernoulli' (1, n).1 +
      ∑ x ∈ antidiagonal n.succ \ {(1, n)}, ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli' x.1 =
    1
p : ℕ × ℕ
h : p ∈ antidiagonal n.succ \ {(1, n)}
⊢ p ∈ ?m.256 ∧ p ≠ ?m.258

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
⊢ (bernoulli n).comp (1 - X) = (-1) ^ n * bernoulli n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
x : ℚ
⊢ eval (1 - x) (bernoulli n) = (-1) ^ n * eval x (bernoulli n)

Tactic:
by

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

Goal state after:
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))
⊢ 0 < 512

Tactic:
by

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⌋₊
k : ℕ
hk : k ∈ {0, 1}
hk' : k ∉ Icc 2 ⌊b⌋₊
⊢ f ↑k * c k = 0

Tactic:
by

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⌋₊
⊢ ∑ k ∈ Icc 0 ⌊b⌋₊, f ↑k * c k = f ↑2 * c 2 + ∑ k ∈ Ioc 2 ⌊b⌋₊, f ↑k * c k

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
by

Goal state after:
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
⊢ 1 - 2 / 3 = 1 / 3

Tactic:
by

Goal state after:
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
⊢ 0 ≤ 0.5

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: case hg
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := ⋯
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
⊢ ConvexOn ℝ (Set.Ioi 0.5) (HMul.hMul (log 4 / 3))

Tactic:
apply ConvexOn.smul

Goal state after:
case hg.hc
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := ⋯
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
⊢ 0 ≤ log 4 / 3

case hg.hf
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := ⋯
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
⊢ ConvexOn ℝ (Set.Ioi 0.5) fun x ↦ x
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
⊢ 1 ≤ 4

Tactic:
by

Goal state after:
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
⊢ 0 ≤ 3

Tactic:
by

Goal state after: