mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.Equivalence

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h₁ : φ ⟹[T] ψ
h₂ : φ ⟹[T] θ
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (φ ⟹ ψ ⊓ θ).Realize v xs

Tactic:
simp only [BoundedFormula.realize_imp, BoundedFormula.realize_inf]

Goal state after:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h₁ : φ ⟹[T] ψ
h₂ : φ ⟹[T] θ
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ φ.Realize v xs → ψ.Realize v xs ∧ θ.Realize v xs
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 (s₁' ∩ s₂')

Tactic:
rw [← image_preimage_eq (s₁' ∩ s₂') hf, preimage_inter]

Goal state after:
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 '' (⇑f ⁻¹' s₁' ∩ ⇑f ⁻¹' s₂'))
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case mpr
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
⊢ (∃ (h_dom : f.dom = g.dom),
      ∀ (x : M) (h : x ∈ f.dom), f.cod.subtype (f.toEquiv ⟨x, h⟩) = g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)) →
    f = g

Tactic:
rintro ⟨h, H⟩; exact ext h H

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
⊢ Function.Injective fun f ↦ f.toPartialEquiv

Tactic:
intro _ _ h

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
a₁✝ a₂✝ : M ↪[L] N
h : (fun f ↦ f.toPartialEquiv) a₁✝ = (fun f ↦ f.toPartialEquiv) a₂✝
⊢ a₁✝ = a₂✝
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mp.refine_3
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x ≠ hs.base
⊢ x + ∑ i, (-hs.floor x i).toNat • ↑i = hs.fract x + ∑ i, (hs.floor x i).toNat • ↑i

Tactic:
exact hs.add_floor_neg_toNat_sum_eq x

Goal state after:
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, ∫⁻ (x : X) in i.snd, ‖g x - f x‖ₑ ∂(μ.transpose B).variation +
      ∑ i ∈ g.range.sigma P, ‖∫ᵛ (x : X) in i.snd, f x ∂[B; μ.restrict s]‖ₑ =
    ∫⁻ (x : X) in ⋃ i ∈ g.range.sigma P, i.snd, ‖g x - f x‖ₑ ∂(μ.transpose B).variation +
      ∑ i ∈ g.range.sigma P, ‖∫ᵛ (x : X) in i.snd, f x ∂[B; μ.restrict s]‖ₑ

Tactic:
by
      rw [lintegral_biUnion_finset]
      · rintro ⟨i, p⟩ hi ⟨j, q⟩ hj hijpq
        simp only [Finset.coe_sigma, SimpleFunc.coe_range, mem_sigma_iff, mem_range,
          SetLike.mem_coe] at hi hj
        rcases eq_or_ne i j with rfl | hij
        · simp only [ne_eq, Sigma.mk.injEq, heq_eq_eq, true_and] at hijpq
          exact Pdisj i hi.2 hj.2 hijpq
        · have : Disjoint (g ⁻¹' {i}) (g ⁻¹' {j}) := by grind
          exact this.mono (Pg i p hi.2) (Pg j q hj.2)
      · rintro ⟨i, p⟩ hip
        simp only [Finset.mem_sigma, SimpleFunc.mem_range, mem_range] at hip
        exact Pmeas i p hip.2

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

Goal state before:
pp: case mp.refine_4
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x = hs.base
i : ↑hs.basisSet
hi : hs.floor x i < 0
⊢ x + ∑ x_1, (-hs.floor x x_1).toNat • ↑x_1 = hs.fract x + ∑ x_1, (hs.floor x x_1).toNat • ↑x_1

Tactic:
exact hs.add_floor_neg_toNat_sum_eq x

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

Goal state before:
pp: case mp.refine_4
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x = hs.base
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
hi' : 0 < hs.floor x i
⊢ x + ∑ x_1, (-hs.floor x x_1).toNat • ↑x_1 = hs.fract x + ∑ x_1, (hs.floor x x_1).toNat • ↑x_1

Tactic:
exact hs.add_floor_neg_toNat_sum_eq x

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

Goal state before:
pp: case refine_2
α : Type u_2
s✝ : Finset α
f : α → ℕ
a : α
s : Finset α
ha : a ∉ s
ih : λ (s.lcm f) = s.lcm (⇑λ ∘ f)
⊢ λ (GCDMonoid.lcm (f a) (s.lcm f)) = GCDMonoid.lcm ((⇑λ ∘ f) a) (s.lcm (⇑λ ∘ f))

Tactic:
← ih

Goal state after:
case refine_2
α : Type u_2
s✝ : Finset α
f : α → ℕ
a : α
s : Finset α
ha : a ∉ s
ih : λ (s.lcm f) = s.lcm (⇑λ ∘ f)
⊢ λ (GCDMonoid.lcm (f a) (s.lcm f)) = GCDMonoid.lcm ((⇑λ ∘ f) a) (λ (s.lcm f))
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: n : ℕ
⊢ 0 ≤ if IsPrimePow n then Real.log ↑n.minFac else 0

Tactic:
split_ifs

Goal state after:
case pos
n : ℕ
h✝ : IsPrimePow n
⊢ 0 ≤ Real.log ↑n.minFac

case neg
n : ℕ
h✝ : ¬IsPrimePow n
⊢ 0 ≤ 0
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 : R
hy : (1 + u * x) ^ p = 1 + ↑p * u * (x + v * y)
⊢ ↑p ^ 2 ∣ ↑p ^ p

Tactic:
exact pow_dvd_pow _ hp.two_le

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

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this : Fact (Nat.Prime p)
n : ℕ
a : ZMod (p ^ (n + 1)) := 1 + ↑p
ha_def : a = 1 + ↑p
⊢ IsUnit a

Tactic:
ha_def,

Goal state after:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this : Fact (Nat.Prime p)
n : ℕ
a : ZMod (p ^ (n + 1)) := 1 + ↑p
ha_def : a = 1 + ↑p
⊢ IsUnit (1 + ↑p)
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
n : σ →₀ ℕ
⊢ (if n = 0 then ↑(n i) + 1 else 0) = if n = 0 then 1 else 0

Tactic:
split_ifs

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
n : σ →₀ ℕ
h✝ : n = 0
⊢ ↑(n i) + 1 = 1

case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
n : σ →₀ ℕ
h✝ : ¬n = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsAddTorsionFree R
f g : MvPowerSeries σ R
hD : ∀ (i : σ), (pderiv R i) f = (pderiv R i) g
hc : constantCoeff f = constantCoeff g
n : σ →₀ ℕ
h : ¬n = 0
i : σ
hi : n i ≠ 0
this : single i 1 ≤ n
e :
  (coeff (n - single i 1 + single i 1)) f * (↑((n - single i 1) i) + 1) =
    (coeff (n - single i 1 + single i 1)) g * (↑((n - single i 1) i) + 1)
⊢ (coeff n) f = (coeff n) g

Tactic:
tsub_add_cancel_of_le this,

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsAddTorsionFree R
f g : MvPowerSeries σ R
hD : ∀ (i : σ), (pderiv R i) f = (pderiv R i) g
hc : constantCoeff f = constantCoeff g
n : σ →₀ ℕ
h : ¬n = 0
i : σ
hi : n i ≠ 0
this : single i 1 ≤ n
e : (coeff n) f * (↑((n - single i 1) i) + 1) = (coeff n) g * (↑((n - single i 1) i) + 1)
⊢ (coeff n) f = (coeff n) g
Module: Mathlib.RingTheory.PowerSeries.Derivative

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : ¬d < n
⊢ 0 = (Polynomial.derivative ((trunc (n + 1)) f)).coeff d

Tactic:
have : ¬d + 1 < n + 1 := by rwa [succ_lt_succ_iff]

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : ¬d < n
this : ¬d + 1 < n + 1
⊢ 0 = (Polynomial.derivative ((trunc (n + 1)) f)).coeff d
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case pos
n : ℕ
h0 : ¬n = 0
h1 : n = 1
⊢ IsCyclic (ZMod n)ˣ ↔ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)

Tactic:
h1

Goal state after:
case pos
n : ℕ
h0 : ¬n = 0
h1 : n = 1
⊢ IsCyclic (ZMod 1)ˣ ↔ 1 = 0 ∨ 1 = 1 ∨ 1 = 2 ∨ 1 = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (1 = p ^ m ∨ 1 = 2 * p ^ m)
Module: Mathlib.RingTheory.PowerSeries.Derivative

Goal state before:
pp: 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) =
    ((coeff (d + 1)) f * (↑d + 1)) • (coeff i) (g ^ d)

Tactic:
split_ifs

Goal state after:
case pos
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 : ℕ
h✝ : d + 1 < m + 1
⊢ ((coeff (d + 1)) f * (↑d + 1)) • (coeff i) (g ^ d) = ((coeff (d + 1)) f * (↑d + 1)) • (coeff i) (g ^ d)

case neg
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 : ℕ
h✝ : ¬d + 1 < m + 1
⊢ (0 * (↑d + 1)) • (coeff i) (g ^ d) = ((coeff (d + 1)) f * (↑d + 1)) • (coeff i) (g ^ d)
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
suffices
    ((n + 1 : ℚ) * ∑ k ∈ range n, ↑(n.choose k) / (n - k + 1) * bernoulli' k) =
      ∑ x ∈ range n, ↑(n.succ.choose x) * bernoulli' x by
    rw_mod_cast [sum_range_succ, bernoulli'_def, ← this, choose_succ_self_right]
    ring

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

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

Tactic:
refine ⟨?_, fun h ↦ dvd_prod_of_mem _ (by grind)⟩

Goal state after:
p n : ℕ
hp : Prime p
⊢ p ∣ n# → p ≤ n
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)!
⊢ ∑ 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) =
    t ^ n * (algebraMap ℚ A) (1 / ↑n !)

Tactic:
rw [← (hnp1.map (algebraMap ℚ A)).mul_right_inj]

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 !))
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if n.succ = 0 then 1 else 0) = 0
⊢ (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!)⁻¹) =
    0

Tactic:
simp only [CharP.cast_eq_zero, zero_add, inv_one, map_one, sub_self, mul_zero]

Goal state after:
case succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if n.succ = 0 then 1 else 0) = 0
⊢ (algebraMap ℚ A) (∑ x ∈ antidiagonal (n + 1), bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹) = 0
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: 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
this : ∑ k ∈ Ico 1 n.succ, ↑k ^ p.succ = ∑ i ∈ range p.succ.succ, f' i
⊢ ∑ k ∈ Ico 1 (n + 1), ↑k ^ (p + 1) =
    ∑ i ∈ range (p + 1 + 1), bernoulli' i * ↑((p + 1 + 1).choose i) * ↑n ^ (p + 1 + 1 - i) / ↑(p + 1).succ

Tactic:
convert!
    this

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: 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
⊢ -1 / 2 * (↑p + 1 + 1) * ↑n ^ (p + 1) / (↑p + 1 + 1) + ↑n ^ p.succ = 1 / 2 * ↑n ^ p.succ

Tactic:
h1

Goal state after:
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
⊢ -1 / 2 * ↑n ^ p.succ + ↑n ^ p.succ = 1 / 2 * ↑n ^ p.succ
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
by
  rw [← Nat.cast_succ]
  -- dispose of the trivial case
  cases p with | zero => simp | succ p =>
  let f i := bernoulli i * p.succ.succ.choose i * (n : ℚ) ^ (p.succ.succ - i) / p.succ.succ
  let f' i := bernoulli' i * p.succ.succ.choose i * (n : ℚ) ^ (p.succ.succ - i) / p.succ.succ
  suffices (∑ k ∈ Ico 1 n.succ, (k : ℚ) ^ p.succ) = ∑ i ∈ range p.succ.succ, f' i by convert!
    this
  -- prove some algebraic facts that will make things easier for us later on
  have hle := Nat.le_add_left 1 n
  have hne : (p + 1 + 1 : ℚ) ≠ 0 := by norm_cast
  have h1 : ∀ r : ℚ, r * (p + 1 + 1) * (n : ℚ) ^ p.succ / (p + 1 + 1 : ℚ) = r * (n : ℚ) ^ p.succ :=
      fun r => by rw [mul_div_right_comm, mul_div_cancel_right₀ _ hne]
  have h2 : f 1 + (n : ℚ) ^ p.succ = 1 / 2 * (n : ℚ) ^ p.succ := by
    simp_rw [f, bernoulli_one, choose_one_right, succ_sub_succ_eq_sub, cast_succ, tsub_zero, h1]
    ring
  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)]
  calc
    (-- replace sum over `Ico` with sum over `range` and simplify
        ∑ k ∈ Ico 1 n.succ, (k : ℚ) ^ p.succ)
    _ = ∑ k ∈ range n.succ, (k : ℚ) ^ p.succ := by simp [sum_Ico_eq_sub _ hle]
    -- extract the last term of the sum
    _ = (∑ k ∈ range n, (k : ℚ) ^ p.succ) + (n : ℚ) ^ p.succ := by rw [sum_range_succ]
    -- apply the key lemma, `sum_range_pow`
    _ = (∑ i ∈ range p.succ.succ, f i) + (n : ℚ) ^ p.succ := by simp [f, sum_range_pow]
    -- extract the first two terms of the sum
    _ = (∑ i ∈ range p, f i.succ.succ) + f 1 + f 0 + (n : ℚ) ^ p.succ := by
      simp_rw [sum_range_succ']
    _ = (∑ i ∈ range p, f i.succ.succ) + (f 1 + (n : ℚ) ^ p.succ) + f 0 := by ring
    _ = (∑ i ∈ range p, f i.succ.succ) + 1 / 2 * (n : ℚ) ^ p.succ + f 0 := by rw [h2]
    -- convert from `bernoulli` to `bernoulli'`
    _ = (∑ i ∈ range p, f' i.succ.succ) + f' 1 + f' 0 := by
      simpa [f, f', h1, fun i => show i + 2 = i + 1 + 1 from rfl]
    -- rejoin the first two terms of the sum
    _ = ∑ i ∈ range p.succ.succ, f' i := by simp_rw [sum_range_succ']

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
hdvd : p - 1 ∣ 2 * k
⊢ p < 2 * k + 2

Tactic:
have := Nat.le_of_dvd (by lia) hdvd

Goal state after:
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
hdvd : p - 1 ∣ 2 * k
this : p - 1 ≤ 2 * k
⊢ p < 2 * k + 2
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : x < 2
n : ℕ
hn : (0 < n ∧ n ≤ ⌊x⌋₊) ∧ Nat.Prime n
⊢ ↑n = 1

Tactic:
have := lt_of_le_of_lt (le_floor_iff' hn.1.1.ne' |>.mp hn.1.2) hx

Goal state after:
x : ℝ
hx : x < 2
n : ℕ
hn : (0 < n ∧ n ≤ ⌊x⌋₊) ∧ Nat.Prime n
this : ↑n < 2
⊢ ↑n = 1
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case hy
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)
⊢ (Rat.padicValuation p) ((if p - 1 ∣ 2 * m then 1 else 0) * ↑((2 * k + 1).choose (2 * m)) * P / (2 * ↑k + 1)) ≤ 1

Tactic:
split_ifs

Goal state after:
case pos
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) (1 * ↑((2 * k + 1).choose (2 * m)) * P / (2 * ↑k + 1)) ≤ 1

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
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ (∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k + 1 - i) / (2 * ↑k + 1)) / ↑p =
    ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1)

Tactic:
have hp_ne : (p : ℚ) ≠ 0 := mod_cast (Fact.out : p.Prime).ne_zero
  rw [Finset.sum_div]
  refine Finset.sum_congr rfl fun i hi ↦ ?_
  have := Finset.mem_range.mp hi
  rw [show 2 * k + 1 - i = (2 * k - i) + 1 by lia, pow_succ]
  field_simp [hp_ne]

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 ι))
hε : 0 < ε
ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := bS.repr a
s_eq : ∀ (i : ι), s i = (bS.repr a) i
qs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i / b
rs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i % b
r_eq : ∀ (j : Fin (cardM bS adm).succ) (i : ι), rs j i = μ j * s i % b
μ_eq : ∀ (i : ι) (j : Fin (cardM bS adm).succ), μ j * s i = b * qs j i + rs j i
j : Fin (cardM bS adm).succ
⊢ ∑ x, (distinctElems bS adm) j • (bS.repr a) x • bS x =
    ∑ x, (b • ((distinctElems bS adm) j * s x / b) • bS x + ((distinctElems bS adm) j * s x % b) • bS x)

Tactic:
refine Finset.sum_congr rfl fun i _ => ?_

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 < ε
ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := bS.repr a
s_eq : ∀ (i : ι), s i = (bS.repr a) i
qs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i / b
rs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i % b
r_eq : ∀ (j : Fin (cardM bS adm).succ) (i : ι), rs j i = μ j * s i % b
μ_eq : ∀ (i : ι) (j : Fin (cardM bS adm).succ), μ j * s i = b * qs j i + rs j i
j : Fin (cardM bS adm).succ
i : ι
x✝ : i ∈ Finset.univ
⊢ (distinctElems bS adm) j • (bS.repr a) i • bS i =
    b • ((distinctElems bS adm) j * s i / b) • bS i + ((distinctElems bS adm) j * s i % b) • bS i
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case h
x : ℝ
n : ℕ
hx : 0 ≤ x
this : 0 ≤ x ^ (↑n)⁻¹
⊢ ∀ N ≥ ⌊log (x ^ (↑n)⁻¹) / log 2⌋₊, ψ (x ^ (↑n)⁻¹) = ∑ k ∈ Icc 1 N, b x (n * k)

Tactic:
intro N hN

Goal state after:
case h
x : ℝ
n : ℕ
hx : 0 ≤ x
this : 0 ≤ x ^ (↑n)⁻¹
N : ℕ
hN : N ≥ ⌊log (x ^ (↑n)⁻¹) / log 2⌋₊
⊢ ψ (x ^ (↑n)⁻¹) = ∑ k ∈ Icc 1 N, b x (n * k)