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

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

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
b : ℝ
hb : 0 ≤ b
hf_diff : ∀ t ∈ Set.Icc 0 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 0 b) volume
⊢ f 0 * c 0 + (f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f 0 * c 0 - ∫ (t : ℝ) in Set.Ioc 0 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (t : ℝ) in Set.Ioc 0 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case zero
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ n ≤ 2 ↔ n ≤ 2

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case e'_2.h
𝕜 : 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
⊢ m = m

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case e'_3.h
𝕜 : 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
⊢ m = m

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ (if Prime n then insert n ({p ∈ range n | Prime p}) else {p ∈ range n | Prime p}) =
    if Prime n then insert n ({p ∈ range n | Prime p}) else {p ∈ range n | Prime p}

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

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

Tactic:
]

Goal state after:
a k : ℕ
h0 : a ≠ 0
h1 : a < k
n : ℕ
⊢ #({x ∈ Ico 0 k | Prime x} ∪ {x ∈ Ico k (k + n) | Prime x}) ≤
    #({p ∈ Ico 0 k | Prime p}) + #({p ∈ Ico k (k + n) | Prime p})
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}) ≤
    #({x ∈ range k | Prime x}) + #({p ∈ Ico k (k + n) | Prime p})

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: case h
a k : ℕ
h0 : a ≠ 0
h1 : a < k
n p : ℕ
hp : p ∈ Ico k (k + n)
⊢ Prime p → p.Coprime a

Tactic:
]

Goal state after:
case h
a k : ℕ
h0 : a ≠ 0
h1 : a < k
n p : ℕ
hp : p ∈ Ico k (k + n)
⊢ Prime p → p.Coprime a
Module: Mathlib.NumberTheory.PrimeCounting

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

Tactic:
]

Goal state after:
a k : ℕ
h0 : a ≠ 0
h1 : a < k
n : ℕ
⊢ #({b ∈ Ico k (k + n) | a.Coprime b}) ≤ φ a * (n / a + 1)
Module: Mathlib.NumberTheory.PrimeCounting

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

Tactic:
]

Goal state after:
a k : ℕ
h0 : a ≠ 0
h1 : a ≤ k
n : ℕ
⊢ π' (k + n + 1) ≤ π k + φ a * (n / a + 1)
Module: Mathlib.NumberTheory.BernoulliPolynomials

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

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

pp: n p : ℕ
⊢ ↑p + 1 ≠ 0

Tactic:
]

Goal state after:
n p : ℕ
⊢ ∑ i ∈ range (p + 1), _root_.bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) =
    ∑ i ∈ range (p.succ + 1), eval (↑n) ((monomial i) (_root_.bernoulli (p.succ - i) * ↑(p.succ.choose i))) -
      _root_.bernoulli p.succ

n p : ℕ
⊢ ↑p + 1 ≠ 0
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
]

Goal state after:
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 (p.succ - (p + 1 - (p + 1))) * ↑(p.succ.choose (p + 1 - (p + 1))) * ↑n ^ (p + 1 - (p + 1)) -
      _root_.bernoulli p.succ =
    ∑ i ∈ range (p + 1), _root_.bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i)

Tactic:
]

Goal state after:
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 (p.succ - (p + 1 - (p + 1))) * ↑(p.succ.choose (p + 1 - (p + 1))) * ↑n ^ (p + 1 - (p + 1)) -
      _root_.bernoulli p.succ =
    ∑ i ∈ range (p + 1), _root_.bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i)
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
⊢ (∏ p ∈ n.primesLE, p).primeFactors = n.primesLE

Tactic:
]

Goal state after:
n : ℕ
⊢ (∏ p ∈ n.primesLE, p).primeFactors = n.primesLE
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n p x : ℕ
hx : x ∈ range (p + 1)
⊢ _root_.bernoulli x = _root_.bernoulli x

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
neg_eq_zero

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

Goal state before:
pp: n p x : ℕ
hx : x ∈ range (p + 1)
⊢ ↑(p.succ.choose (p + 1 - x)) = ↑((p + 1).choose (p + 1 - x))

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
]

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

Goal state before:
pp: n x : ℕ
hx : x ∈ range n
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n p : ℕ
⊢ eval (↑n) (bernoulli p.succ) - _root_.bernoulli p.succ = eval (↑n) (bernoulli p.succ) - _root_.bernoulli p.succ

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

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

Tactic:
]

Goal state after:
case succ
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (1 + X) = bernoulli m + m • X ^ (m - 1)
⊢ ((d + 2) • bernoulli (d + 1)).comp (1 + X) = (d + 2) • bernoulli (d + 1) + (d + 2) • (d + 1) • X ^ (d + 1 - 1)
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
]

Goal state after:
⊢ 1 - ∑ k ∈ range 0, ↑(Nat.choose 0 k) / (↑0 - ↑k + 1) * bernoulli' k = 1
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
]

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

Goal state before:
pp: n : ℕ
hn1 : n ≠ 1
hn : Odd n
⊢ {p ∈ range (n + 1) | Nat.Prime p} = {p ∈ range (n + 1) | Nat.Prime p}

pp: n : ℕ
hn1 : n ≠ 1
hn : Odd n
⊢ Nat.Prime (n + 1) → Even n

Tactic:
]

Goal state after:
n : ℕ
hn1 : n ≠ 1
hn : Odd n
⊢ Nat.Prime (n + 1) → Even n
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
]

Goal state after:
⊢ 1 - ∑ k ∈ range 2, ↑(Nat.choose 2 k) / (↑2 - ↑k + 1) * bernoulli' k = 1 / 6
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
]

Goal state after:
⊢ 1 - ∑ k ∈ range 3, ↑(Nat.choose 3 k) / (↑3 - ↑k + 1) * bernoulli' k = 0
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
]

Goal state after:
this : Nat.choose 4 2 = 6
⊢ 1 - ∑ k ∈ range 4, ↑(Nat.choose 4 k) / (↑4 - ↑k + 1) * bernoulli' k = -1 / 30
Module: Mathlib.NumberTheory.Primorial

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

pp: case hab
m n : ℕ
⊢ 0 ≤ m + 1

pp: case hbc
m n : ℕ
⊢ m + 1 ≤ m + n + 1

pp: m n : ℕ
⊢ Disjoint ({p ∈ Ico 0 (m + 1) | Nat.Prime p}) ({p ∈ Ico (m + 1) (m + n + 1) | Nat.Prime p})

Tactic:
]

Goal state after:
case hab
m n : ℕ
⊢ 0 ≤ m + 1

case hbc
m n : ℕ
⊢ m + 1 ≤ m + n + 1

m n : ℕ
⊢ Disjoint ({p ∈ Ico 0 (m + 1) | Nat.Prime p}) ({p ∈ Ico (m + 1) (m + n + 1) | Nat.Prime p})
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: m n : ℕ
h : n ≤ m
p : ℕ
hp : (m + 1 ≤ p ∧ p < m + n + 1) ∧ Nat.Prime p
⊢ p ∣ (m + n).choose m

Tactic:
]

Goal state after:
m n : ℕ
h : n ≤ m
p : ℕ
hp : (m + 1 ≤ p ∧ p < m + n + 1) ∧ Nat.Prime p
⊢ p ∣ (m + n).choose m
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case succ.e_a
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) =
    ∑ x ∈ range (d + 1), (d + 2).choose x • x • X ^ (x - 1) + ((d + 2) * (d + 1)) • X ^ (d + 1 - 1)

Tactic:
]

Goal state after:
case succ.e_a
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) =
    ∑ x ∈ range (d + 1), (d + 2).choose x • x • X ^ (x - 1) + ((d + 2) * (d + 1)) • X ^ (d + 1 - 1)
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 = (d + 2) • ∑ i ∈ range (d + 1), (d + 1).choose i • X ^ i

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
hn : Squarefree n
this : n ∣ ∏ p ∈ range (n + 1) with Nat.Prime p, p
⊢ n ∣ n#

Tactic:
]

Goal state after:
n : ℕ
hn : Squarefree n
this : n ∣ ∏ p ∈ range (n + 1) with Nat.Prime p, p
⊢ n ∣ n#
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
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:
]

Goal state after:
case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
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)
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case inl
𝕜 : 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⌋₊
⊢ f 1 * c 1 +
      (f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f 1 * (0 + c 1) - ∫ (t : ℝ) in Set.Ioc 1 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, 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:
]

Goal state after:
case inl
𝕜 : 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⌋₊
⊢ f 1 * c 1 +
      (f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f 1 * (0 + c 1) - ∫ (t : ℝ) in Set.Ioc 1 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, 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
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 =
    ∑ x ∈ range (d + 1 + 1), ((d + 2).choose x * x) • X ^ (x - 1)

Tactic:
]

Goal state after:
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 =
    ∑ x ∈ range (d + 1 + 1), ((d + 2).choose x * x) • X ^ (x - 1)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ i ∈ antidiagonal n, bernoulli' i.1 / ↑i.1! * ((↑i.2 + 1) * ↑i.2!)⁻¹ * ↑n ! = 1

Tactic:
]

Goal state after:
case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ i ∈ antidiagonal n, bernoulli' i.1 / ↑i.1! * ((↑i.2 + 1) * ↑i.2!)⁻¹ * ↑n ! = 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
⊢ (m + 1 + m)# = (m + 1 + m)#

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case succ
n i : ℕ
⊢ (if i ≤ n + 1 then _root_.bernoulli (n + 1 - i) * ↑((n + 1).choose i) else 0) * (-1) ^ i =
    (-1) ^ (n + 1) •
      ((if i ≤ n + 1 then _root_.bernoulli (n + 1 - i) * ↑((n + 1).choose i) else 0) +
        (n + 1) • if i = n + 1 - 1 then 1 else 0)

Tactic:
]

Goal state after:
case succ
n i : ℕ
⊢ (if i ≤ n + 1 then _root_.bernoulli (n + 1 - i) * ↑((n + 1).choose i) else 0) * (-1) ^ i =
    (-1) ^ (n + 1) •
      ((if i ≤ n + 1 then _root_.bernoulli (n + 1 - i) * ↑((n + 1).choose i) else 0) +
        (n + 1) • if i = n + 1 - 1 then 1 else 0)
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).choose m = (m + 1)# * (m + m + 1).choose m

Tactic:
]

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 ℚ
⊢ evalNegHom B * (1 - exp ℚ) = -(X * 1)

Tactic:
]

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.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 + m + 1) ≤ 4 ^ (m + m + 1)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case inr.inl
n : ℕ
hn : n ≠ 1
hgt : 1 < n
heven : Even n
⊢ bernoulli' n = bernoulli' n

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case inr.inr
n : ℕ
hn : n ≠ 1
hgt : 1 < n
hodd : Odd n
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

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

pp: case neg.inr.h_odd
n i : ℕ
h✝ : i ≤ n + 1
h' : ¬i = n + 1 - 1
h : Odd (n + 1 - i)
⊢ Odd (n + 1 - i)

pp: case neg.inr.hlt
n i : ℕ
h✝ : i ≤ n + 1
h' : ¬i = n + 1 - 1
h : Odd (n + 1 - i)
⊢ 1 < n + 1 - i

Tactic:
]

Goal state after:
case neg.inr
n i : ℕ
h✝ : i ≤ n + 1
h' : ¬i = n + 1 - 1
h : Odd (n + 1 - i)
⊢ 0 * ↑((n + 1).choose i) * (-1) ^ i = (-1) ^ (n + 1) • (0 * ↑((n + 1).choose i) + (n + 1) • 0)

case neg.inr.h_odd
n i : ℕ
h✝ : i ≤ n + 1
h' : ¬i = n + 1 - 1
h : Odd (n + 1 - i)
⊢ Odd (n + 1 - i)

case neg.inr.hlt
n i : ℕ
h✝ : i ≤ n + 1
h' : ¬i = n + 1 - 1
h : Odd (n + 1 - i)
⊢ 1 < n + 1 - i
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ.succ.refine_1.e_f
n : ℕ
f :
  ∑ k ∈ range n, ↑(n.succ.succ.choose (k + 1 + 1)) * bernoulli' (k + 1 + 1) =
    ↑n + 1 + 1 - ↑(n.succ.succ.choose 0) * bernoulli' 0 - ↑(n.succ.succ.choose (0 + 1)) * bernoulli' (0 + 1)
x : ℕ
⊢ ↑((n + 2).choose (x + 2)) * bernoulli' x.succ.succ = ↑(n.succ.succ.choose (x + 1 + 1)) * bernoulli' (x + 1 + 1)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case e'_2.h
𝕜 : 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
⊢ m = m

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case e'_3.h
𝕜 : 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
⊢ m = m

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
]

Goal state after:
case succ
n : ℕ
⊢ ∑ k ∈ antidiagonal (n + 1), ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli k.1 = 0
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
⊢ Squarefree (∏ p ∈ n.primesLE, p)

Tactic:
]

Goal state after:
n : ℕ
⊢ Squarefree (∏ p ∈ n.primesLE, p)
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:
]

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
⊢ ↑(((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
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)}
h : p ∈ antidiagonal n.succ ∧ ¬p = (1, n)
⊢ p ∈ ?m.256 ∧ p ≠ ?m.258

Tactic:
]

Goal state after:
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)}
h : p ∈ antidiagonal n.succ ∧ ¬p = (1, n)
⊢ p ∈ ?m.256 ∧ p ≠ ?m.258
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
⊢ ∑ x ∈ range (n + 1),
        (PowerSeries.coeff (x, n + 1 - x).1) (PowerSeries.mk fun n ↦ (aeval t) ((1 / ↑n !) • bernoulli n)) *
          (PowerSeries.coeff (x, n + 1 - x).2) (exp A - 1) +
      (PowerSeries.coeff (n + 1, n + 1 - (n + 1)).1) (PowerSeries.mk fun n ↦ (aeval t) ((1 / ↑n !) • bernoulli n)) *
        (PowerSeries.coeff (n + 1, n + 1 - (n + 1)).2) (exp A - 1) =
    t ^ n * (algebraMap ℚ A) (1 / ↑n !)

Tactic:
]

Goal state after:
case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
⊢ ∑ x ∈ range (n + 1),
        (PowerSeries.coeff (x, n + 1 - x).1) (PowerSeries.mk fun n ↦ (aeval t) ((1 / ↑n !) • bernoulli n)) *
          (PowerSeries.coeff (x, n + 1 - x).2) (exp A - 1) +
      (PowerSeries.coeff (n + 1, n + 1 - (n + 1)).1) (PowerSeries.mk fun n ↦ (aeval t) ((1 / ↑n !) • bernoulli n)) *
        (PowerSeries.coeff (n + 1, n + 1 - (n + 1)).2) (exp A - 1) =
    t ^ n * (algebraMap ℚ A) (1 / ↑n !)
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 ∈ {0, 1} ∪ Icc 2 ⌊b⌋₊, f ↑k * c k = ∑ x ∈ Icc 2 ⌊b⌋₊, f ↑x * c x

Tactic:
]

Goal state after:
𝕜 : 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 ∈ {0, 1} ∪ Icc 2 ⌊b⌋₊, f ↑k * c k = ∑ x ∈ Icc 2 ⌊b⌋₊, f ↑x * c 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)
x : ℝ
h5 : 0 < x
h6 : 0 < 2 * x
h7 : 0 < (2 * x) ^ √(2 * x)
⊢ f x = log x + √(2 * x) * log (2 * x) - log 4 / 3 * x

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
⊢ (algebraMap ℚ A) ↑(n + 1)! *
      ∑ x ∈ range (n + 1),
        (PowerSeries.coeff x) (PowerSeries.mk fun n ↦ (aeval t) ((1 / ↑n !) • bernoulli n)) *
          ((PowerSeries.coeff (n + 1 - x)) (exp A) - (PowerSeries.coeff (n + 1 - x)) 1) =
    (algebraMap ℚ A) ↑(n + 1)! * (t ^ n * (algebraMap ℚ A) (1 / ↑n !))

Tactic:
]

Goal state after:
case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
⊢ (algebraMap ℚ A) ↑(n + 1)! *
      ∑ x ∈ range (n + 1),
        (PowerSeries.coeff x) (PowerSeries.mk fun n ↦ (aeval t) ((1 / ↑n !) • bernoulli n)) *
          ((PowerSeries.coeff (n + 1 - x)) (exp A) - (PowerSeries.coeff (n + 1 - x)) 1) =
    (algebraMap ℚ A) ↑(n + 1)! * (t ^ n * (algebraMap ℚ A) (1 / ↑n !))