mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝ : CompleteSpace G
hf : μ.Integrable f
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖B.flip y‖₊ * ‖x‖₊
s : Set X
hs : MeasurableSet s
ε : NNReal
εpos : 0 < ε
δ : NNReal := ε / 3
δpos : 0 < δ
g : X →ₛ E
hg : eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ
gmem : MemLp (⇑g) 1 μ.variation
I1 : ∫⁻ (a : X) in s, ‖f a‖ₑ ∂(μ.transpose B).variation ≤ ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation + ↑δ
I2 :
  ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation =
    ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i})
ρ : ℝ≥0∞
ρpos : ρ > 0
hρ : ∑ i ∈ g.range, ‖i‖ₑ * ρ ≤ ↑δ
P : E → Finset (Set X)
Pg : ∀ (i : E), ∀ t ∈ P i, t ⊆ ⇑g ⁻¹' {i}
Pdisj : ∀ (i : E), (↑(P i)).PairwiseDisjoint id
Pmeas : ∀ (i : E), ∀ t ∈ P i, MeasurableSet t
hP :
  ∀ (i : E),
    ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
      ‖i‖ₑ * (∑ p ∈ P i, ‖((μ.transpose B).restrict s) p‖ₑ + ρ)
I3 :
  ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
    ∑ i ∈ g.range.sigma P, ‖i.fst‖ₑ * ‖((μ.transpose B).restrict s) i.snd‖ₑ + ↑δ
⊢ ∑ i ∈ g.range.sigma P, ‖i.fst‖ₑ * ‖((μ.transpose B).restrict s) i.snd‖ₑ =
    ∑ i ∈ g.range.sigma P, ‖∫ᵛ (x : X) in i.snd, i.fst ∂[B; μ.restrict s]‖ₑ

Tactic:
congr! with ⟨i, p⟩ hi

Goal state after:
case a
X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝ : CompleteSpace G
hf : μ.Integrable f
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖B.flip y‖₊ * ‖x‖₊
s : Set X
hs : MeasurableSet s
ε : NNReal
εpos : 0 < ε
δ : NNReal := ε / 3
δpos : 0 < δ
g : X →ₛ E
hg : eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ
gmem : MemLp (⇑g) 1 μ.variation
I1 : ∫⁻ (a : X) in s, ‖f a‖ₑ ∂(μ.transpose B).variation ≤ ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation + ↑δ
I2 :
  ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation =
    ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i})
ρ : ℝ≥0∞
ρpos : ρ > 0
hρ : ∑ i ∈ g.range, ‖i‖ₑ * ρ ≤ ↑δ
P : E → Finset (Set X)
Pg : ∀ (i : E), ∀ t ∈ P i, t ⊆ ⇑g ⁻¹' {i}
Pdisj : ∀ (i : E), (↑(P i)).PairwiseDisjoint id
Pmeas : ∀ (i : E), ∀ t ∈ P i, MeasurableSet t
hP :
  ∀ (i : E),
    ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
      ‖i‖ₑ * (∑ p ∈ P i, ‖((μ.transpose B).restrict s) p‖ₑ + ρ)
I3 :
  ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
    ∑ i ∈ g.range.sigma P, ‖i.fst‖ₑ * ‖((μ.transpose B).restrict s) i.snd‖ₑ + ↑δ
i : E
p : Set X
hi : ⟨i, p⟩ ∈ g.range.sigma P
⊢ ‖⟨i, p⟩.fst‖ₑ * ‖((μ.transpose B).restrict s) ⟨i, p⟩.snd‖ₑ =
    ‖∫ᵛ (x : X) in ⟨i, p⟩.snd, ⟨i, p⟩.fst ∂[B; μ.restrict s]‖ₑ
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: L : Language
α : Type u'
β : Type v'
n m : ℕ
φ : L.BoundedFormula α m
h✝ : φ.IsPrenex
f : α → β ⊕ Fin n
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
x✝ : φ✝.IsPrenex
h : (BoundedFormula.relabel f φ✝).IsPrenex
⊢ (BoundedFormula.relabel f (∀' φ✝)).IsPrenex

Tactic:
simp [h.all]

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
s : Set M
hs : IsSemilinearSet s
⊢ ∃ P s', P.FG ∧ IsSemilinearSet s' ∧ s = Subtype.val '' s'

Tactic:
by
  rcases hs with ⟨S, hS, hS', rfl⟩
  choose! P t hP ht ht' using fun s hs => (hS' s hs).exists_fg_eq_subtypeVal
  have : Finite S := hS
  refine ⟨⨆ s : S, P s, ⋃ (s : S), AddSubmonoid.inclusion (le_iSup _ s) '' t s.1,
    .iSup _ fun s => hP s s.2, .iUnion fun s => (ht s s.2).isSemilinearSet.image _, ?_⟩
  simp_rw [sUnion_eq_iUnion, image_iUnion, image_image, AddSubmonoid.coe_inclusion,
    fun s : S => ht' s s.2]

Goal state after:
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
inst✝¹ : IsEmpty L.Constants
inst✝ : IsEmpty (L.Relations 0)
n : ℕ
r : L.Relations n
x : Fin n → ↥⊥
⊢ RelMap r ((fun a ↦ isEmptyElim a) ∘ x) ↔ RelMap r x

Tactic:
by
        cases n
        · exact isEmptyElim r
        · exact isEmptyElim (x 0)

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mpr
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ (hs.fract x = hs.base ∧ ∀ (i : ↑hs.basisSet), 0 ≤ hs.floor x i ∧ (↑i ∉ hs.periods → hs.floor x i = 0)) →
    ∃ y ∈ closure hs.periods, hs.base + y = x

Tactic:
intro ⟨hx₁, hx₂⟩
    refine ⟨∑ i : hs.basisSet with i.1 ∈ hs.periods, (hs.floor x i).toNat • i.1,
      sum_mem fun i hi => nsmul_mem (mem_closure_of_mem (Finset.mem_filter.1 hi).2) _, ?_⟩
    rw [Finset.sum_filter, ← hx₁]
    conv_rhs =>
      rw [← add_zero x, ← Finset.sum_const_zero (ι := hs.basisSet) (s := Finset.univ)]
    convert! (hs.add_floor_neg_toNat_sum_eq x).symm using 3 with i _ i
    · split_ifs with hi
      · simp
      · simp [(hx₂ i).2 hi]
    · simp [fun i => Int.toNat_eq_zero.2 (neg_nonpos.2 (hx₂ i).1)]

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective ⇑f
⊢ IsSemilinearSet (⇑f ⁻¹' s₁' \ ⇑f ⁻¹' s₂')

Tactic:
apply Nat.isSemilinearSet_sdiff <;> apply Nat.isSemilinearSet_preimage

Goal state after:
case hs₁
M : Type u_1
inst✝ : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective ⇑f
⊢ IsSemilinearSet s₁'

case hs₂
M : Type u_1
inst✝ : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective ⇑f
⊢ IsSemilinearSet s₂'
Module: Mathlib.NumberTheory.AlmostPrime

Goal state before:
pp: k l m n : ℕ
hm : k.IsAtMostAlmostPrime m
hn : l.IsAtMostAlmostPrime n
⊢ Ω (m * n) ≤ k + l

Tactic:
ArithmeticFunction.cardFactors_mul hm.1 hn.1

Goal state after:
k l m n : ℕ
hm : k.IsAtMostAlmostPrime m
hn : l.IsAtMostAlmostPrime n
⊢ Ω m + Ω n ≤ k + l
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : (↑↑p)⁻¹ ≤ 3⁻¹
⊢ 3 ≤ ↑↑q

Tactic:
by exact_mod_cast h3q

Goal state after:
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case «1».«1».«0»
H : 1 < sumInv {2, 3, 3}
⊢ Admissible {2, 3, 3}

pp: case «1».«1».«1»
H : 1 < sumInv {2, 3, 4}
⊢ Admissible {2, 3, 4}

pp: case «1».«1».«2»
H : 1 < sumInv {2, 3, 5}
⊢ Admissible {2, 3, 5}

Tactic:
· exact admissible_E6

Goal state after:
case «1».«1».«1»
H : 1 < sumInv {2, 3, 4}
⊢ Admissible {2, 3, 4}

case «1».«1».«2»
H : 1 < sumInv {2, 3, 5}
⊢ Admissible {2, 3, 5}
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = ↑p * u * v * b
⊢ 1 +
      ((u * x) ^ 1 * ↑(p.choose 1) +
        (∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * ↑(p.choose x_1) +
          (u * x) ^ p * ↑(p.choose p))) =
    1 +
      ↑p * u *
        (x +
          v *
            (a * x ^ 2 *
                ∑ i ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ (i - 2) * ↑(p.choose i / p) +
              b * x ^ p))

Tactic:
rw [mul_add]

Goal state after:
case h
R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = ↑p * u * v * b
⊢ 1 +
      ((u * x) ^ 1 * ↑(p.choose 1) +
        (∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * ↑(p.choose x_1) +
          (u * x) ^ p * ↑(p.choose p))) =
    1 +
      (↑p * u * x +
        ↑p * u *
          (v *
            (a * x ^ 2 *
                ∑ i ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ (i - 2) * ↑(p.choose i / p) +
              b * x ^ p)))
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : ℕ
u v : R
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
m✝ m : ℕ
⊢ ∃ y, (1 + u * x) ^ p ^ (m + 1) = 1 + ↑p ^ (m + 1) * u * (x + v * y)

Tactic:
rw [pow_succ', pow_mul]
    obtain ⟨y, hy⟩ := exists_one_add_mul_pow_prime_eq hp hvu hpuv x
    rw [hy]
    obtain ⟨z, hz⟩ :=
      exists_one_add_mul_pow_prime_pow_eq (u := p * u) (v := p * v) hp
      (mul_dvd_mul_left _ hvu)
      (by
        rw [mul_pow]
        simp only [← mul_assoc]
        rw [mul_assoc, mul_assoc, ← mul_assoc u, mul_comm u]
        apply mul_dvd_mul _ hpuv
        rw [← pow_two]
        exact pow_dvd_pow _ hp.two_le)
      (x + v * y) m
    use y + p * z
    rw [hz]
    ring

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

Goal state before:
pp: n : ℕ
hn : Odd n
⊢ IsCyclic (ZMod (2 * n))ˣ ↔ IsCyclic (ZMod n)ˣ

Tactic:
by
  simp [((Units.mapEquiv (chineseRemainder <| Nat.coprime_two_left.mpr hn).toMulEquiv).trans
    .prodUnits).isCyclic, Group.isCyclic_prod_iff, isCyclic_units_two]

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

Goal state before:
pp: case inr
m : ℕ
hm : Odd m
hm1 : m ≠ 1
x✝¹ : NeZero m
hn : Odd 2
hn1 : 2 ≠ 1
hmn : m.Coprime 2
x✝ : NeZero 2
e : (ZMod (m * 2))ˣ ≃* (ZMod m)ˣ × (ZMod 2)ˣ :=
  (Units.mapEquiv (chineseRemainder hmn).toMulEquiv).trans MulEquiv.prodUnits
⊢ False

Tactic:
· simp [← Nat.not_even_iff_odd] at hn

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Derivative

Goal state before:
pp: case e_a
R : Type u_1
inst✝ : CommRing R
f g : R⟦X⟧
hg : HasSubst g
n m : ℕ
hm : ∀ (b : ℕ), m ≤ b → ∀ n' ≤ n + 1, (coeff n') (g ^ b) = 0
this : (coeff (n + 1)) (subst g f) = (coeff (n + 1)) (subst g ↑((trunc (m + 1)) f))
x✝ : ℕ × ℕ
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal n
⊢ (coeff (i, j).1) (subst g ((d⁄dX R) ↑((trunc (m + 1)) f))) = (coeff (i, j).1) (subst g ((d⁄dX R) f))

Tactic:
simp only [coeff_subst' hg, coeff_derivative, coeff_coe, coeff_trunc]

Goal state after:
case e_a
R : Type u_1
inst✝ : CommRing R
f g : R⟦X⟧
hg : HasSubst g
n m : ℕ
hm : ∀ (b : ℕ), m ≤ b → ∀ n' ≤ n + 1, (coeff n') (g ^ b) = 0
this : (coeff (n + 1)) (subst g f) = (coeff (n + 1)) (subst g ↑((trunc (m + 1)) f))
x✝ : ℕ × ℕ
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal n
⊢ ∑ᶠ (d : ℕ), ((if d + 1 < m + 1 then (coeff (d + 1)) f else 0) * (↑d + 1)) • (coeff i) (g ^ d) =
    ∑ᶠ (d : ℕ), ((coeff (d + 1)) f * (↑d + 1)) • (coeff i) (g ^ d)
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

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

Tactic:
Measure.variation_toSignedMeasure,

Goal state after:
case inr
X : Type u_1
E : Type u_2
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure X
f : X → E
hf : Integrable f μ
hE : Nontrivial E
this✝ : IsFiniteMeasure (μ.withDensity fun x ↦ ‖f x‖ₑ)
I : VectorMeasure.Integrable (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure fun x ↦ ‖f x‖⁻¹ • f x
this :
  μ.withDensityᵥ f =
    withDensity (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure (fun x ↦ ‖f x‖⁻¹ • f x)
      (ContinuousLinearMap.lsmul ℝ ℝ).flip
⊢ ((μ.withDensity fun x ↦ ‖f x‖ₑ).withDensity fun x ↦ ‖‖f x‖⁻¹ • f x‖ₑ) = μ.withDensity fun x ↦ ‖f x‖ₑ
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
rw [bernoulli'_def]
  norm_num

Goal state after:
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:
norm_num [sum_range_succ, sum_range_succ, sum_range_zero, this]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
let B := mk fun n => bernoulli' n / (n ! : ℚ)
  suffices (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1) by
    rcases mul_eq_mul_right_iff.mp this with h | h <;>
      simp only [PowerSeries.ext_iff, evalNegHom, coeff_X] at h
    · apply eq_zero_of_neg_eq
      specialize h n
      split_ifs at h <;> simp_all [B, h_odd.neg_one_pow, factorial_ne_zero]
    · simpa +decide [Nat.factorial] using h 1
  have h : B * (exp ℚ - 1) = X * exp ℚ := by
    simpa [bernoulli'PowerSeries] using bernoulli'PowerSeries_mul_exp_sub_one ℚ
  rw [sub_mul, h, mul_sub X, sub_right_inj, ← neg_sub, mul_neg, neg_eq_iff_eq_neg]
  suffices evalNegHom (B * (exp ℚ - 1)) * exp ℚ = evalNegHom (X * exp ℚ) * exp ℚ by
    simpa [mul_assoc, sub_mul, mul_comm (evalNegHom (exp ℚ)), exp_mul_exp_neg_eq_one]
  congr

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:
rw [bernoulli, heven.neg_one_pow, one_mul]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
hn : n ≠ 1
x✝ : n < 1 ∨ 1 < n
⊢ bernoulli n = bernoulli' n

Tactic:
cases hn.lt_or_gt with

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:
convert! sum_mul_eq_sub_integral_mul₀ c hc m hf_diff hf_int
  all_goals rw [Nat.floor_natCast]

Goal state after:
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:
simp [field, h₃]

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
⊢ 1 = 2 - 1
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
have hne : ∀ m : ℕ, (m ! : ℚ) ≠ 0 := fun m => mod_cast factorial_ne_zero m
  -- compute the Cauchy product of two power series
  have h_cauchy :
    ((mk fun p => bernoulli p / p !) * mk fun q => coeff (q + 1) (exp ℚ ^ n)) =
      mk fun p => ∑ i ∈ range (p + 1),
          bernoulli i * (p + 1).choose i * (n : ℚ) ^ (p + 1 - i) / (p + 1)! := by
    ext q : 1
    let f a b := bernoulli a / a ! * coeff (b + 1) (exp ℚ ^ n)
    -- key step: use `PowerSeries.coeff_mul` and then rewrite sums
    simp only [f, coeff_mul, coeff_mk, sum_antidiagonal_eq_sum_range_succ f]
    apply sum_congr rfl
    intro m h
    simp only [exp_pow_eq_rescale_exp, rescale, RingHom.coe_mk]
    -- manipulate factorials and binomial coefficients
    have h : m < q + 1 := by simpa using h
    rw [choose_eq_factorial_div_factorial h.le, eq_comm, div_eq_iff (hne q.succ), succ_eq_add_one,
      mul_assoc _ _ (q.succ ! : ℚ), mul_comm _ (q.succ ! : ℚ), ← mul_assoc, div_mul_eq_mul_div]
    simp only [MonoidHom.coe_mk, OneHom.coe_mk, coeff_exp, Algebra.algebraMap_self, one_div,
      map_inv₀, map_natCast, coeff_mk]
    rw [mul_comm ((n : ℚ) ^ (q - m + 1)), ← mul_assoc _ _ ((n : ℚ) ^ (q - m + 1)), ← one_div,
      mul_one_div, div_div, tsub_add_eq_add_tsub (le_of_lt_succ h), cast_div, cast_mul]
    · ring
    · exact factorial_mul_factorial_dvd_factorial h.le
    · simp [factorial_ne_zero]
  -- same as our goal except we pull out `p!` for convenience
  have hps :
    (∑ k ∈ range n, (k : ℚ) ^ p) =
      (∑ i ∈ range (p + 1),
          bernoulli i * (p + 1).choose i * (n : ℚ) ^ (p + 1 - i) / (p + 1)!) * p ! := by
    suffices
      (mk fun p => ∑ k ∈ range n, (k : ℚ) ^ p * algebraMap ℚ ℚ p !⁻¹) =
        mk fun p =>
          ∑ i ∈ range (p + 1), bernoulli i * (p + 1).choose i * (n : ℚ) ^ (p + 1 - i) / (p + 1)! by
      rw [← div_eq_iff (hne p), div_eq_mul_inv, sum_mul]
      rw [PowerSeries.ext_iff] at this
      simpa using this p
    -- the power series `exp ℚ - 1` is non-zero, a fact we need in order to use `mul_right_inj'`
    have hexp : exp ℚ - 1 ≠ 0 := by
      simp only [exp, PowerSeries.ext_iff, Ne, not_forall]
      use 1
      simp
    have h_r : exp ℚ ^ n - 1 = X * mk fun p => coeff (p + 1) (exp ℚ ^ n) := by
      have h_const : C (constantCoeff (exp ℚ ^ n)) = 1 := by simp
      rw [← h_const, sub_const_eq_X_mul_shift]
    -- key step: a chain of equalities of power series
    rw [← mul_right_inj' hexp, mul_comm]
    rw [← exp_pow_sum, geom_sum_mul, h_r, ← bernoulliPowerSeries_mul_exp_sub_one,
      bernoulliPowerSeries, mul_right_comm]
    simp only [mul_comm, mul_eq_mul_left_iff, hexp, or_false]
    refine Eq.trans (mul_eq_mul_right_iff.mpr ?_) (Eq.trans h_cauchy ?_)
    · left
      congr
    · simp only [mul_comm, factorial]
  -- massage `hps` into our goal
  rw [hps, sum_mul]
  refine sum_congr rfl fun x _ => ?_
  simp [field, factorial]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ
n p : ℕ
f : ℕ → ℚ := fun i ↦ bernoulli i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
f' : ℕ → ℚ := fun i ↦ bernoulli' i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
hle : 1 ≤ n + 1
hne : ↑p + 1 + 1 ≠ 0
h1 : ∀ (r : ℚ), r * (↑p + 1 + 1) * ↑n ^ p.succ / (↑p + 1 + 1) = r * ↑n ^ p.succ
h2 : f 1 + ↑n ^ p.succ = 1 / 2 * ↑n ^ p.succ
⊢ ∑ k ∈ Ico 1 n.succ, ↑k ^ p.succ = ∑ i ∈ range p.succ.succ, f' i

Tactic:
have :
    (∑ i ∈ range p, bernoulli (i + 2) * (p + 2).choose (i + 2) * (n : ℚ) ^ (p - i) / ↑(p + 2)) =
      ∑ i ∈ range p, bernoulli' (i + 2) * (p + 2).choose (i + 2) * (n : ℚ) ^ (p - i) / ↑(p + 2) :=
    sum_congr rfl fun i _ => by rw [bernoulli_eq_bernoulli'_of_ne_one (succ_succ_ne_one i)]

Goal state after:
case succ
n p : ℕ
f : ℕ → ℚ := fun i ↦ bernoulli i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
f' : ℕ → ℚ := fun i ↦ bernoulli' i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
hle : 1 ≤ n + 1
hne : ↑p + 1 + 1 ≠ 0
h1 : ∀ (r : ℚ), r * (↑p + 1 + 1) * ↑n ^ p.succ / (↑p + 1 + 1) = r * ↑n ^ p.succ
h2 : f 1 + ↑n ^ p.succ = 1 / 2 * ↑n ^ p.succ
this :
  ∑ i ∈ range p, bernoulli (i + 2) * ↑((p + 2).choose (i + 2)) * ↑n ^ (p - i) / ↑(p + 2) =
    ∑ i ∈ range p, bernoulli' (i + 2) * ↑((p + 2).choose (i + 2)) * ↑n ^ (p - i) / ↑(p + 2)
⊢ ∑ k ∈ Ico 1 n.succ, ↑k ^ p.succ = ∑ i ∈ range p.succ.succ, f' i
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: n : ℕ
hn0 : n ≠ 0
⊢ ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n

Tactic:
by
  -- Split into cases whether `n` is large or small
  rcases lt_or_ge 511 n with h | h
  -- If `n` is large, apply the lemma derived from the inequalities on the central binomial
  -- coefficient.
  · exact exists_prime_lt_and_le_two_mul_eventually n h
  replace h : n < 521 := h.trans_lt (by norm_num1)
  revert h
  -- For small `n`, supply a list of primes to cover the initial cases.
  open Lean Elab Tactic in
  run_tac do
    for i in [317, 163, 83, 43, 23, 13, 7, 5, 3, 2] do
      let i : Term := quote i
      evalTactic <| ←
        `(tactic| refine exists_prime_lt_and_le_two_mul_succ $i (by norm_num1) (by norm_num1) ?_)
  exact fun h2 => ⟨2, prime_two, h2, Nat.mul_le_mul_left 2 (Nat.pos_of_ne_zero hn0)⟩

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_1
n q : ℕ
hq : q ∈ (filter Nat.Prime (Icc 1 n)).biUnion fun p ↦ image (fun x ↦ p ^ x) (Icc 1 (Nat.log p n))
⊢ q ∈ Icc 1 n

Tactic:
simp only [mem_biUnion, mem_filter, mem_Icc, mem_image] at hq ⊢

Goal state after:
case refine_1
n q : ℕ
hq : ∃ a, ((1 ≤ a ∧ a ≤ n) ∧ Nat.Prime a) ∧ ∃ a_1, (1 ≤ a_1 ∧ a_1 ≤ Nat.log a n) ∧ a ^ a_1 = q
⊢ 1 ≤ q ∧ q ≤ n
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_2
n x : ℕ
hx : x ∈ Icc 1 n
⊢ (∃ x_1 x_2, Nat.Prime x_1 ∧ 0 < x_2 ∧ x_1 ^ x_2 = x) →
    ∃ x_1, 1 ≤ x_1 ∧ x_1 ≤ n ∧ Nat.Prime x_1 ∧ ∃ x_2, 1 ≤ x_2 ∧ x_2 ≤ Nat.log x_1 n ∧ x_1 ^ x_2 = x

Tactic:
rintro ⟨p, k, hp, hk, rfl⟩

Goal state after:
case refine_2
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hx : p ^ k ∈ Icc 1 n
⊢ ∃ x, 1 ≤ x ∧ x ≤ n ∧ Nat.Prime x ∧ ∃ x_1, 1 ≤ x_1 ∧ x_1 ≤ Nat.log x n ∧ x ^ x_1 = p ^ k
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: case e'_4
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
a : S
y : ℤ
hy : ∀ (k : ι), abv ((bS.repr a) k) ≤ y
⊢ Fintype.card ι •
      ((Finset.image (fun ijk ↦ abv ((Algebra.leftMulMatrix bS) (bS ijk.1) ijk.2.1 ijk.2.2)) Finset.univ).max' ⋯ * y) =
    Finset.univ.card • y * ?convert_5

pp: case convert_5
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
a : S
y : ℤ
hy : ∀ (k : ι), abv ((bS.repr a) k) ≤ y
⊢ ℤ

pp: case convert_6
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
a : S
y : ℤ
hy : ∀ (k : ι), abv ((bS.repr a) k) ≤ y
⊢ ∀ (k i j : ι), abv ((LinearMap.toMatrix bS bS) ((Algebra.lmul R S) (bS k)) i j) ≤ ?convert_5

Tactic:
· rw [Finset.card_univ, smul_mul_assoc, mul_comm]

Goal state after:
case convert_6
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
a : S
y : ℤ
hy : ∀ (k : ι), abv ((bS.repr a) k) ≤ y
⊢ ∀ (k i j : ι),
    abv ((LinearMap.toMatrix bS bS) ((Algebra.lmul R S) (bS k)) i j) ≤
      (Finset.image (fun ijk ↦ abv ((Algebra.leftMulMatrix bS) (bS ijk.1) ijk.2.1 ijk.2.2)) Finset.univ).max' ⋯