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

Goal state before:
pp: case zero
a : ℕ
h : a ∣ 0
⊢ λ a ∣ λ 0

pp: case succ
a n✝ : ℕ
h : a ∣ n✝ + 1
⊢ λ a ∣ λ (n✝ + 1)

Tactic:
· simp

Goal state after:
case succ
a n✝ : ℕ
h : a ∣ n✝ + 1
⊢ λ a ∣ λ (n✝ + 1)
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
hcard : Nat.card (ZMod (2 ^ n))ˣ = 2 ^ (n - 1)
k : ℕ
hk : k ≤ n - 1
h : exponent (ZMod (2 ^ n))ˣ = 2 ^ k
this : ¬exponent (ZMod (2 ^ n))ˣ = Nat.card (ZMod (2 ^ n))ˣ
⊢ k ≤ n - 2

Tactic:
by grind

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: case refine_1
n : ℕ
⊢ ∑ i ∈ divisors 0, Λ i = Real.log ↑0

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

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

Tactic:
· simp

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

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

Goal state before:
pp: case refine_2
n p k : ℕ
hp : Nat.Prime p
⊢ ∑ x ∈ range (k + 1), Λ (p ^ x) = Real.log (↑p ^ k)

Tactic:
Real.log_pow,

Goal state after:
case refine_2
n p k : ℕ
hp : Nat.Prime p
⊢ ∑ x ∈ range (k + 1), Λ (p ^ x) = ↑k * Real.log ↑p
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

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

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

Goal state after:
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
n : ℕ
⊢ ↑p = ↑p * ↑1

pp: p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
n : ℕ
⊢ ¬↑p ∣ 1

Tactic:
· simp

Goal state after:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
n : ℕ
⊢ ¬↑p ∣ 1
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⌋₊
⊢ f ↑⌊b⌋₊ * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f ↑(⌊a⌋₊ + 1) * ∑ x ∈ Icc 0 ⌊a⌋₊, c x -
      ∑ x ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f ↑(x + 1) - f ↑x) * ∑ x ∈ Icc 0 x, c x =
    f b * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f a * ∑ x ∈ Icc 0 ⌊a⌋₊, c x - ∫ (x : ℝ) in a..b, deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x

Tactic:
have : ∑ 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 := by
    rw [← Ico_add_one_add_one_eq_Ioc, Nat.sub_add_cancel (by lia), Eq.comm]
    exact sum_congr rfl fun k hk ↦ (integralmulsum c hf_diff hf_int _ _ _ (mod_cast k.le_succ)
      le_rfl (mod_cast le_rfl) (ineqofmemIco' hk).1 <| mod_cast (ineqofmemIco' hk).2)

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
⊢ f ↑⌊b⌋₊ * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f ↑(⌊a⌋₊ + 1) * ∑ x ∈ Icc 0 ⌊a⌋₊, c x -
      ∑ x ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f ↑(x + 1) - f ↑x) * ∑ x ∈ Icc 0 x, c x =
    f b * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f a * ∑ x ∈ Icc 0 ⌊a⌋₊, c x - ∫ (x : ℝ) in a..b, deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

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

Tactic:
have h₁ : n < n + single i 1 := lt_def.mpr ⟨self_le_add_right _ _, i, by simp⟩

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h₁ : n < n + single i 1
⊢ (coeff n) (pderivFun i (f * g)) = (coeff n) (f • pderivFun i g + g • pderivFun i f)
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
⊢ f ↑⌊b⌋₊ * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f ↑(⌊a⌋₊ + 1) * ∑ x ∈ Icc 0 ⌊a⌋₊, c x -
      ∫ (x : ℝ) in ↑⌊a⌋₊.succ..↑⌊b⌋₊, deriv f x * ∑ n ∈ Icc 0 ⌊x⌋₊, c n =
    f b * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f a * ∑ x ∈ Icc 0 ⌊a⌋₊, c x - ∫ (x : ℝ) in a..b, deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x

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:
Nat.cast_add,

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
⊢ f ↑⌊b⌋₊ * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f (↑⌊a⌋₊ + ↑1) * ∑ x ∈ Icc 0 ⌊a⌋₊, c x -
      ∫ (x : ℝ) in ↑⌊a⌋₊ + ↑1..↑⌊b⌋₊, deriv f x * ∑ n ∈ Icc 0 ⌊x⌋₊, c n =
    f b * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f a * ∑ x ∈ Icc 0 ⌊a⌋₊, c x - ∫ (x : ℝ) in a..b, deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x

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.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case neg.inl
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : ¬n = 4
hn : Odd n
p m : ℕ
⊢ n = p ^ m ↔ 1 ≤ m ∧ n = p ^ m

Tactic:
and_iff_right_of_imp

Goal state after:
case neg.inl
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : ¬n = 4
hn : Odd n
p m : ℕ
⊢ n = p ^ m ↔ n = p ^ m

case neg.inl
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : ¬n = 4
hn : Odd n
p m : ℕ
⊢ n = p ^ m → 1 ≤ m
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case neg.inr.inl
n : ℕ
h0 : ¬2 * n = 0
h1 : ¬2 * n = 1
h2 : ¬2 * n = 2
h4 : ¬2 * n = 4
hn✝ : Even (2 * n)
hn : Odd n
p m : ℕ
⊢ n = p ^ m ↔ 1 ≤ m ∧ n = p ^ m

Tactic:
and_iff_right_of_imp

Goal state after:
case neg.inr.inl
n : ℕ
h0 : ¬2 * n = 0
h1 : ¬2 * n = 1
h2 : ¬2 * n = 2
h4 : ¬2 * n = 4
hn✝ : Even (2 * n)
hn : Odd n
p m : ℕ
⊢ n = p ^ m ↔ n = p ^ m

case neg.inr.inl
n : ℕ
h0 : ¬2 * n = 0
h1 : ¬2 * n = 1
h2 : ¬2 * n = 2
h4 : ¬2 * n = 4
hn✝ : Even (2 * n)
hn : Odd n
p m : ℕ
⊢ n = p ^ m → 1 ≤ m
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n i : ℕ
h : i ≤ n
⊢ n - i ∈ range (n + 1)

Tactic:
by grind

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

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

Tactic:
by grind

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: ⊢ eval (1 / 4) (∑ i ∈ range 0, (monomial (3 - i)) (_root_.bernoulli i * ↑(Nat.choose 3 i))) +
            _root_.bernoulli 0 * ↑(Nat.choose 3 0) * (1 / 4) ^ (3 - 0) +
          _root_.bernoulli 1 * ↑(Nat.choose 3 1) * (1 / 4) ^ (3 - 1) +
        _root_.bernoulli 2 * ↑(Nat.choose 3 2) * (1 / 4) ^ (3 - 2) +
      _root_.bernoulli 3 * ↑(Nat.choose 3 3) * (1 / 4) ^ (3 - 3) =
    3 / 64

Tactic:
rw [Finset.sum_range_zero, Polynomial.eval_zero, zero_add, _root_.bernoulli_one]

Goal state after:
⊢ _root_.bernoulli 0 * ↑(Nat.choose 3 0) * (1 / 4) ^ (3 - 0) + -1 / 2 * ↑(Nat.choose 3 1) * (1 / 4) ^ (3 - 1) +
        _root_.bernoulli 2 * ↑(Nat.choose 3 2) * (1 / 4) ^ (3 - 2) +
      _root_.bernoulli 3 * ↑(Nat.choose 3 3) * (1 / 4) ^ (3 - 3) =
    3 / 64
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 grind

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)
⊢ (bernoulli (d + 1)).comp (1 + X) = bernoulli (d + 1) + (d + 1) • X ^ (d + 1 - 1)

Tactic:
← smul_right_inj (show d + 2 ≠ 0 by positivity),

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 + 1) • X ^ (d + 1 - 1))
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 grind

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
| succ n =>

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
| succ n =>

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 grind

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
| succ n =>

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
| succ n =>

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 succ
n : ℕ
⊢ (bernoulli (n + 1)).comp (-X) = (-1) ^ (n + 1) • (bernoulli (n + 1) + (n + 1) • X ^ (n + 1 - 1))

Tactic:
| succ n =>

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

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

Tactic:
| succ n =>

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 = if n + 1 = 0 then 1 else 0

Tactic:
| succ n =>

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 grind

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
| succ n =>

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
| succ n =>

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 : ℕ
⊢ (PowerSeries.coeff (n + 1)) ((PowerSeries.mk fun n ↦ (aeval t) ((1 / ↑n !) • bernoulli n)) * (exp A - 1)) =
    (PowerSeries.coeff (n + 1)) (PowerSeries.X * (rescale t) (exp A))

Tactic:
| succ n =>

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 0, DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 0) volume
l : 𝕜
h_lim : Tendsto (fun n ↦ f ↑n * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → 𝕜
hg_dom : (fun t ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) =O[atTop] g
hg_int : IntegrableAtFilter g atTop volume
h_lim' :
  Tendsto (fun n ↦ ∫ (t : ℝ) in Set.Ioc 0 ↑n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) atTop
    (𝓝 (∫ (t : ℝ) in Set.Ioi 0, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))
x✝ : ℕ
⊢ IntegrableOn (deriv f) (Set.Icc 0 ↑x✝) volume

Tactic:
exact hf_int.integrableOn_compact_subset Set.Icc_subset_Ici_self isCompact_Icc

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 1) volume
l : 𝕜
h_lim : Tendsto (fun n ↦ f ↑n * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → ℝ
hg_dom : (fun t ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) =O[atTop] g
hg_int : IntegrableAtFilter g atTop volume
h :
  (fun n ↦ ∫ (x : ℝ) in 1..↑n, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k) =ᶠ[atTop] fun n ↦
    ∫ (t : ℝ) in Set.Ioc 1 ↑n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
h_lim' :
  Tendsto (fun n ↦ ∫ (t : ℝ) in Set.Ioc 1 ↑n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) atTop
    (𝓝 (∫ (t : ℝ) in Set.Ioi 1, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))
x✝ : ℕ
⊢ IntegrableOn (deriv f) (Set.Icc 1 ↑x✝) volume

Tactic:
exact hf_int.integrableOn_compact_subset Set.Icc_subset_Ici_self isCompact_Icc

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case succ
𝕜 : 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 : ℕ
⊢ ∑ i ∈ range (n + 1), ‖f ↑i * c i‖ ≤ max (C₁ + C₂) 1

Tactic:
| succ n =>

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

pp: case zero.refine_2
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
⊢ ∀ (k : Fin 0), ↑(abv (A 1 k % b - A 0 k % b)) < abv b • ε

Tactic:
· simp

Goal state after:
case zero.refine_2
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
⊢ ∀ (k : Fin 0), ↑(abv (A 1 k % b - A 0 k % b)) < abv b • ε
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
h₀ : ψ x = 0
contra : 2 ≤ x
⊢ 0 ≤ x

Tactic:
by grind

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
h₀ : θ x = 0
contra : 2 ≤ x
⊢ 0 ≤ x

Tactic:
by grind

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: x : ℝ
hx : 0 ≤ x
⊢ log (4 ^ ⌊x⌋₊) ≤ log 4 * x

Tactic:
Real.log_pow,

Goal state after:
x : ℝ
hx : 0 ≤ x
⊢ ↑⌊x⌋₊ * log 4 ≤ log 4 * x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n p : ℕ
hp : Prime p
x✝¹ : ℕ
x✝ : x✝¹ ∈ Icc 1 n
⊢ id x✝¹ ≠ 0

Tactic:
by grind

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n p : ℕ
hp : Prime p
this : 1 < p
m : ℕ
x✝ : 1 ≤ m
h : m ≤ n
⊢ 0 < m

Tactic:
by grind

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n p : ℕ
hp : Prime p
this✝ : 1 < p
h✝ : p ≤ n
this : p ^ log p n ≤ n
⊢ p ^ log p n ∈ Icc 1 n

Tactic:
by grind

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n p : ℕ
left✝¹ : (1 ≤ p ∧ p ≤ n) ∧ Nat.Prime p
k : ℕ
left✝ : 1 ≤ k
hk : k ≤ Nat.log p n
⊢ 1 ≤ p ^ k

Tactic:
by grind

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n p : ℕ
hp : p ∈ n.primesLE
k : ℕ
hk : k ∈ Icc 1 (Nat.log p n)
⊢ k ≠ 0

Tactic:
by grind

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

pp: case inr
n : ℕ
hn : n ≠ 0
⊢ ∑ p ∈ n.primesLE, ↑(Nat.log p n) * log ↑p ≤ ∑ _x ∈ n.primesLE, log ↑n

Tactic:
· simp

Goal state after:
case inr
n : ℕ
hn : n ≠ 0
⊢ ∑ p ∈ n.primesLE, ↑(Nat.log p n) * log ↑p ≤ ∑ _x ∈ n.primesLE, log ↑n
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n k : ℕ
hk : k ∈ range (n + 1)
⊢ k ≤ n

Tactic:
by grind

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.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 ι))
⊢ ∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))

Tactic:
have hε : 0 < ε := Real.rpow_pos_of_pos (Int.cast_pos.mpr (normBound_pos abv bS)) _

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 < ε
⊢ ∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))
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 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

pp: case inr
n : ℕ
hn : n > 0
⊢ ↑n * log 2 - log (↑n + 1) - 2 * √↑n * log ↑n ≤ θ ↑n

Tactic:
· simp

Goal state after:
case inr
n : ℕ
hn : n > 0
⊢ ↑n * log 2 - log (↑n + 1) - 2 * √↑n * log ↑n ≤ θ ↑n