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

Goal state before:
pp: case e_a
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ ↑n ! ≠ 0

Tactic:
·

Goal state after:
case e_a
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ ↑n ! ≠ 0
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case inr.hac
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
aux1 : ↑⌊a⌋₊ ≤ a
aux2 : b ≤ ↑⌊b⌋₊ + 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ ↑⌊a⌋₊ + 1
aux4 : ↑⌊a⌋₊ + 1 ≤ b
aux5 : ↑⌊b⌋₊ ≤ b
aux6 : a ≤ ↑⌊b⌋₊
this :
  ∑ k ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f ↑(k + 1) - f ↑k) * ∑ n ∈ Icc 0 k, c n =
    ∑ k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊, ∫ (t : ℝ) in ↑k..↑(k + 1), deriv f t * ∑ n ∈ Icc 0 ⌊t⌋₊, c n
⊢ IntervalIntegrable (fun x ↦ deriv f x * ∑ n ∈ Icc 0 ⌊x⌋₊, c n) volume a (↑⌊a⌋₊ + 1)

pp: case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
aux1 : ↑⌊a⌋₊ ≤ a
aux2 : b ≤ ↑⌊b⌋₊ + 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ ↑⌊a⌋₊ + 1
aux4 : ↑⌊a⌋₊ + 1 ≤ b
aux5 : ↑⌊b⌋₊ ≤ b
aux6 : a ≤ ↑⌊b⌋₊
this :
  ∑ k ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f ↑(k + 1) - f ↑k) * ∑ n ∈ Icc 0 k, c n =
    ∑ k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊, ∫ (t : ℝ) in ↑k..↑(k + 1), deriv f t * ∑ n ∈ Icc 0 ⌊t⌋₊, c n
⊢ ∀ k ∈ Set.Ico ⌊a⌋₊.succ ⌊b⌋₊, IntervalIntegrable (fun t ↦ deriv f t * ∑ n ∈ Icc 0 ⌊t⌋₊, c n) volume ↑k ↑(k + 1)

Tactic:
·

Goal state after:
case inr.hac
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
aux1 : ↑⌊a⌋₊ ≤ a
aux2 : b ≤ ↑⌊b⌋₊ + 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ ↑⌊a⌋₊ + 1
aux4 : ↑⌊a⌋₊ + 1 ≤ b
aux5 : ↑⌊b⌋₊ ≤ b
aux6 : a ≤ ↑⌊b⌋₊
this :
  ∑ k ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f ↑(k + 1) - f ↑k) * ∑ n ∈ Icc 0 k, c n =
    ∑ k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊, ∫ (t : ℝ) in ↑k..↑(k + 1), deriv f t * ∑ n ∈ Icc 0 ⌊t⌋₊, c n
⊢ IntervalIntegrable (fun x ↦ deriv f x * ∑ n ∈ Icc 0 ⌊x⌋₊, c n) volume a (↑⌊a⌋₊ + 1)
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case pos
n i : ℕ
h : i ≤ n
⊢ (∑ x ∈ range (n + 1), if n - x = i then _root_.bernoulli x * ↑(n.choose x) else 0) =
    _root_.bernoulli (n - i) * ↑(n.choose i)

pp: case neg
n i : ℕ
h : ¬i ≤ n
⊢ (∑ x ∈ range (n + 1), if n - x = i then _root_.bernoulli x * ↑(n.choose x) else 0) = 0

Tactic:
·

Goal state after:
case pos
n i : ℕ
h : i ≤ n
⊢ (∑ x ∈ range (n + 1), if n - x = i then _root_.bernoulli x * ↑(n.choose x) else 0) =
    _root_.bernoulli (n - i) * ↑(n.choose i)
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case neg
n i : ℕ
h : ¬i ≤ n
⊢ (∑ x ∈ range (n + 1), if n - x = i then _root_.bernoulli x * ↑(n.choose x) else 0) = 0

Tactic:
·

Goal state after:
case neg
n i : ℕ
h : ¬i ≤ n
⊢ (∑ x ∈ range (n + 1), if n - x = i then _root_.bernoulli x * ↑(n.choose x) else 0) = 0
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case pos
n : ℕ
h : n = 1
⊢ (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n

pp: case neg
n : ℕ
h : ¬n = 1
⊢ (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n

Tactic:
·

Goal state after:
case pos
n : ℕ
h : n = 1
⊢ (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case neg
n : ℕ
h : ¬n = 1
⊢ (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n

Tactic:
·

Goal state after:
case neg
n : ℕ
h : ¬n = 1
⊢ (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
aux1 : ↑⌊a⌋₊ ≤ a
aux2 : b ≤ ↑⌊b⌋₊ + 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ ↑⌊a⌋₊ + 1
aux4 : ↑⌊a⌋₊ + 1 ≤ b
aux5 : ↑⌊b⌋₊ ≤ b
aux6 : a ≤ ↑⌊b⌋₊
this :
  ∑ k ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f ↑(k + 1) - f ↑k) * ∑ n ∈ Icc 0 k, c n =
    ∑ k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊, ∫ (t : ℝ) in ↑k..↑(k + 1), deriv f t * ∑ n ∈ Icc 0 ⌊t⌋₊, c n
⊢ ∀ k ∈ Set.Ico ⌊a⌋₊.succ ⌊b⌋₊, IntervalIntegrable (fun t ↦ deriv f t * ∑ n ∈ Icc 0 ⌊t⌋₊, c n) volume ↑k ↑(k + 1)

Tactic:
·

Goal state after:
case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
aux1 : ↑⌊a⌋₊ ≤ a
aux2 : b ≤ ↑⌊b⌋₊ + 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ ↑⌊a⌋₊ + 1
aux4 : ↑⌊a⌋₊ + 1 ≤ b
aux5 : ↑⌊b⌋₊ ≤ b
aux6 : a ≤ ↑⌊b⌋₊
this :
  ∑ k ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f ↑(k + 1) - f ↑k) * ∑ n ∈ Icc 0 k, c n =
    ∑ k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊, ∫ (t : ℝ) in ↑k..↑(k + 1), deriv f t * ∑ n ∈ Icc 0 ⌊t⌋₊, c n
⊢ ∀ k ∈ Set.Ico ⌊a⌋₊.succ ⌊b⌋₊, IntervalIntegrable (fun t ↦ deriv f t * ∑ n ∈ Icc 0 ⌊t⌋₊, c n) volume ↑k ↑(k + 1)
Module: Mathlib.NumberTheory.BernoulliPolynomials

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

Tactic:
range_add_one,

Goal state after:
k : ℕ
⊢ ∑ x ∈ insert (k + 1) (range (k + 1)), (monomial (k - x)) (_root_.bernoulli x * ↑((k + 1).choose x) * ↑(k + 1 - x)) =
    (↑k + 1) * ∑ i ∈ range (k + 1), (monomial (k - i)) (_root_.bernoulli i * ↑(k.choose i))
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
⊢ ∑ 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

pp: case inr
𝕜 : 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 : b < 1
⊢ ∑ 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:
·

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
⊢ ∑ 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
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 lia

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

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

Tactic:
sum_range_succ_sub_sum,

Goal state after:
n : ℕ
⊢ (↑n + 1) • bernoulli n = ↑((n + 1).choose n) • bernoulli n
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
Module: Mathlib.NumberTheory.BernoulliPolynomials

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

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

Tactic:
·

Goal state after:
n p x : ℕ
hx : x ∈ range (p + 1)
⊢ _root_.bernoulli (p.succ - (p + 1 - x)) = _root_.bernoulli x
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 x)

Tactic:
·

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

Goal state before:
pp: n p : ℕ
⊢ ↑p + 1 ≠ 0

Tactic:
·

Goal state after:
n p : ℕ
⊢ ↑p + 1 ≠ 0
Module: Mathlib.NumberTheory.Primorial

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

Tactic:
range_add_one,

Goal state after:
n : ℕ
hn1 : n ≠ 1
hn : Odd n
⊢ {p ∈ insert (n + 1) (range (n + 1)) | Nat.Prime p} = {p ∈ range (n + 1) | Nat.Prime p}
Module: Mathlib.NumberTheory.Primorial

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

Tactic:
by lia

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 lia

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: case inl
n : ℕ
hn : n ≤ 2
⊢ n ≤ n#

pp: case inr
n : ℕ
hn : 2 < n
⊢ n ≤ n#

Tactic:
·

Goal state after:
case inl
n : ℕ
hn : n ≤ 2
⊢ n ≤ n#
Module: Mathlib.NumberTheory.Primorial

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

Tactic:
·

Goal state after:
case inr
n : ℕ
hn : 2 < n
⊢ n ≤ n#
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: case h.zero
ihn : ∀ m < 0, m ≠ 0 → m# < 4 ^ m
hn : 0 ≠ 0
⊢ 0# < 4 ^ 0

pp: case h.succ
n : ℕ
ihn : ∀ m < n + 1, m ≠ 0 → m# < 4 ^ m
hn : n + 1 ≠ 0
⊢ (n + 1)# < 4 ^ (n + 1)

Tactic:
·

Goal state after:
case h.zero
ihn : ∀ m < 0, m ≠ 0 → m# < 4 ^ m
hn : 0 ≠ 0
⊢ 0# < 4 ^ 0
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case inr
𝕜 : 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 : b < 1
⊢ ∑ 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:
·

Goal state after:
case inr
𝕜 : 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 : b < 1
⊢ ∑ 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
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: case h.succ.inl
m : ℕ
ihn : ∀ m_1 < m + m + 1, m_1 ≠ 0 → m_1# < 4 ^ m_1
hn : m + m + 1 ≠ 0
⊢ (m + m + 1)# < 4 ^ (m + m + 1)

pp: case h.succ.inr
n : ℕ
ihn : ∀ m < n + 1, m ≠ 0 → m# < 4 ^ m
hn : n + 1 ≠ 0
ho : Odd n
⊢ (n + 1)# < 4 ^ (n + 1)

Tactic:
·

Goal state after:
case h.succ.inl
m : ℕ
ihn : ∀ m_1 < m + m + 1, m_1 ≠ 0 → m_1# < 4 ^ m_1
hn : m + m + 1 ≠ 0
⊢ (m + m + 1)# < 4 ^ (m + m + 1)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case inl
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)
h : ∀ (n : ℕ), (coeff n) (B - (rescale (-1)) B) = if n = 1 then 1 else 0
⊢ bernoulli' n = 0

pp: case inr
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)
h : ∀ (n : ℕ), (coeff n) (exp ℚ - 1) = (coeff n) 0
⊢ bernoulli' n = 0

Tactic:
·

Goal state after:
case inl
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)
h : ∀ (n : ℕ), (coeff n) (B - (rescale (-1)) B) = if n = 1 then 1 else 0
⊢ bernoulli' n = 0
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: case h.succ.inl.inl
ihn : ∀ m < 0 + 0 + 1, m ≠ 0 → m# < 4 ^ m
hn : 0 + 0 + 1 ≠ 0
⊢ (0 + 0 + 1)# < 4 ^ (0 + 0 + 1)

pp: case h.succ.inl.inr
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)# < 4 ^ (m + m + 1)

Tactic:
·

Goal state after:
case h.succ.inl.inl
ihn : ∀ m < 0 + 0 + 1, m ≠ 0 → m# < 4 ^ m
hn : 0 + 0 + 1 ≠ 0
⊢ (0 + 0 + 1)# < 4 ^ (0 + 0 + 1)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case inr
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)
h : ∀ (n : ℕ), (coeff n) (exp ℚ - 1) = (coeff n) 0
⊢ bernoulli' n = 0

Tactic:
·

Goal state after:
case inr
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)
h : ∀ (n : ℕ), (coeff n) (exp ℚ - 1) = (coeff n) 0
⊢ bernoulli' n = 0
Module: Mathlib.NumberTheory.BernoulliPolynomials

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

pp: case neg
n i : ℕ
h : i ≤ n + 1
h' : ¬i = n + 1 - 1
⊢ _root_.bernoulli (n + 1 - i) * ↑((n + 1).choose i) * (-1) ^ i =
    (-1) ^ (n + 1) • (_root_.bernoulli (n + 1 - i) * ↑((n + 1).choose i) + (n + 1) • 0)

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

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:
·

Goal state after:
case pos
n i : ℕ
h : i ≤ n + 1
h' : i = n + 1 - 1
⊢ _root_.bernoulli (n + 1 - i) * ↑((n + 1).choose i) * (-1) ^ i =
    (-1) ^ (n + 1) • (_root_.bernoulli (n + 1 - i) * ↑((n + 1).choose i) + (n + 1) • 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

Tactic:
by lia

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 lia

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

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

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

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:
·

Goal state after:
case neg
n i : ℕ
h : i ≤ n + 1
h' : ¬i = n + 1 - 1
⊢ _root_.bernoulli (n + 1 - i) * ↑((n + 1).choose i) * (-1) ^ i =
    (-1) ^ (n + 1) • (_root_.bernoulli (n + 1 - i) * ↑((n + 1).choose i) + (n + 1) • 0)
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: case h.succ.inr
n : ℕ
ihn : ∀ m < n + 1, m ≠ 0 → m# < 4 ^ m
hn : n + 1 ≠ 0
ho : Odd n
⊢ (n + 1)# < 4 ^ (n + 1)

Tactic:
·

Goal state after:
case h.succ.inr
n : ℕ
ihn : ∀ m < n + 1, m ≠ 0 → m# < 4 ^ m
hn : n + 1 ≠ 0
ho : Odd n
⊢ (n + 1)# < 4 ^ (n + 1)
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: case h.succ.inr.inl
ihn : ∀ m < 1 + 1, m ≠ 0 → m# < 4 ^ m
hn : 1 + 1 ≠ 0
ho : Odd 1
⊢ (1 + 1)# < 4 ^ (1 + 1)

pp: case h.succ.inr.inr
n : ℕ
ihn : ∀ m < n + 1, m ≠ 0 → m# < 4 ^ m
hn✝ : n + 1 ≠ 0
ho : Odd n
hn : n ≠ 1
⊢ (n + 1)# < 4 ^ (n + 1)

Tactic:
·

Goal state after:
case h.succ.inr.inl
ihn : ∀ m < 1 + 1, m ≠ 0 → m# < 4 ^ m
hn : 1 + 1 ≠ 0
ho : Odd 1
⊢ (1 + 1)# < 4 ^ (1 + 1)
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: case h.succ.inr.inr
n : ℕ
ihn : ∀ m < n + 1, m ≠ 0 → m# < 4 ^ m
hn✝ : n + 1 ≠ 0
ho : Odd n
hn : n ≠ 1
⊢ (n + 1)# < 4 ^ (n + 1)

Tactic:
·

Goal state after:
case h.succ.inr.inr
n : ℕ
ihn : ∀ m < n + 1, m ≠ 0 → m# < 4 ^ m
hn✝ : n + 1 ≠ 0
ho : Odd n
hn : n ≠ 1
⊢ (n + 1)# < 4 ^ (n + 1)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ.succ.refine_1
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)
⊢ ∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2) =
    ∑ k ∈ range n, ↑(n.succ.succ.choose (k + 1 + 1)) * bernoulli' (k + 1 + 1)

pp: case succ.succ.refine_2
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)
⊢ ↑n + 1 + 1 - ↑(n.succ.succ.choose 0) * bernoulli' 0 - ↑(n.succ.succ.choose (0 + 1)) * bernoulli' (0 + 1) = ↑n / 2

Tactic:
·

Goal state after:
case succ.succ.refine_1
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)
⊢ ∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2) =
    ∑ k ∈ range n, ↑(n.succ.succ.choose (k + 1 + 1)) * bernoulli' (k + 1 + 1)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ.succ.refine_2
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)
⊢ ↑n + 1 + 1 - ↑(n.succ.succ.choose 0) * bernoulli' 0 - ↑(n.succ.succ.choose (0 + 1)) * bernoulli' (0 + 1) = ↑n / 2

Tactic:
·

Goal state after:
case succ.succ.refine_2
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)
⊢ ↑n + 1 + 1 - ↑(n.succ.succ.choose 0) * bernoulli' 0 - ↑(n.succ.succ.choose (0 + 1)) * bernoulli' (0 + 1) = ↑n / 2
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: case inl
⊢ 0# ≤ 4 ^ 0

pp: case inr
n : ℕ
hn : n ≠ 0
⊢ n# ≤ 4 ^ n

Tactic:
·

Goal state after:
case inl
⊢ 0# ≤ 4 ^ 0
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 0
⊢ n# ≤ 4 ^ n

Tactic:
·

Goal state after:
case inr
n : ℕ
hn : n ≠ 0
⊢ n# ≤ 4 ^ n
Module: Mathlib.NumberTheory.BernoulliPolynomials

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

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:
·

Goal state after:
case pos
n i : ℕ
h : ¬i ≤ n + 1
h✝ : i = n + 1 - 1
⊢ 0 * (-1) ^ i = (-1) ^ (n + 1) • (0 + (n + 1) • 1)
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:
·

Goal state after:
case neg
n i : ℕ
h : ¬i ≤ n + 1
h✝ : ¬i = n + 1 - 1
⊢ 0 * (-1) ^ i = (-1) ^ (n + 1) • (0 + (n + 1) • 0)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case e'_2
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 =
    ∑ x ∈ antidiagonal n.succ \ {(1, n)}, ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli' x.1

pp: case e'_3
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
⊢ 0 - ↑(((1, n).1 + (1, n).2).choose (1, n).2) / (↑(1, n).2 + 1) * bernoulli (1, n).1 =
    1 - ↑(((1, n).1 + (1, n).2).choose (1, n).2) / (↑(1, n).2 + 1) * bernoulli' (1, n).1

Tactic:
·

Goal state after:
case e'_2
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 =
    ∑ x ∈ antidiagonal n.succ \ {(1, n)}, ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli' x.1
Module: Mathlib.NumberTheory.AbelSummation

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

pp: case neg
𝕜 : 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
⊢ ∑ k ∈ Icc 0 ⌊b⌋₊, f ↑k * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (t : ℝ) in Set.Ioc 2 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
·

Goal state after:
case pos
𝕜 : 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
⊢ ∑ k ∈ Icc 0 ⌊b⌋₊, f ↑k * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (t : ℝ) in Set.Ioc 2 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
Module: Mathlib.NumberTheory.BernoulliPolynomials

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

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

Tactic:
·

Goal state after:
n : ℕ
⊢ (bernoulli (n + 1)).comp (1 - X) = ((bernoulli (n + 1)).comp (1 + X)).comp (-X)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case e'_3
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
⊢ 0 - ↑(((1, n).1 + (1, n).2).choose (1, n).2) / (↑(1, n).2 + 1) * bernoulli (1, n).1 =
    1 - ↑(((1, n).1 + (1, n).2).choose (1, n).2) / (↑(1, n).2 + 1) * bernoulli' (1, n).1

Tactic:
·

Goal state after:
case e'_3
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
⊢ 0 - ↑(((1, n).1 + (1, n).2).choose (1, n).2) / (↑(1, n).2 + 1) * bernoulli (1, n).1 =
    1 - ↑(((1, n).1 + (1, n).2).choose (1, n).2) / (↑(1, n).2 + 1) * bernoulli' (1, n).1
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: case 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
⊢ ConcaveOn ℝ (Set.Ioi 0.5) fun x ↦ log x + √(2 * x) * log (2 * x)

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:
·

Goal state after:
case 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
⊢ ConcaveOn ℝ (Set.Ioi 0.5) fun x ↦ log x + √(2 * x) * log (2 * x)