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

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : Preorder M
inst✝ : L.OrderedStructure M
⊢ M ⊨ L.preorderTheory

Tactic:
by
  simp only [preorderTheory, Theory.model_insert_iff, Relations.realize_reflexive, relMap_leSymb,
    Theory.model_singleton_iff, Relations.realize_transitive, Matrix.cons_val_zero,
    Matrix.cons_val_one]
  exact ⟨inferInstance, inferInstance⟩

Goal state after:
Module: Mathlib.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
⊢ ((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable ↔ {p | S ⊆ ↑p}.Nonempty

Tactic:
Set.Nonempty

Goal state after:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
⊢ ((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable ↔ ∃ x, x ∈ {p | S ⊆ ↑p}
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: case hP₁
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 := ⋯
δ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‖ₑ + ↑δ
I4 :
  ∑ i ∈ g.range.sigma P, ‖i.fst‖ₑ * ‖((μ.transpose B).restrict s) i.snd‖ₑ ≤
    ∑ i ∈ g.range.sigma P, ‖∫ᵛ (x : X) in i.snd, f x ∂[B; μ.restrict s]‖ₑ + ↑δ
Q : Finset (Set X) := ⋯
⊢ ∀ t ∈ Q, t ⊆ s

Tactic:
intro t ht
        simp only [Finset.mem_image, Finset.mem_sigma, SimpleFunc.mem_range, mem_range,
          Sigma.exists, ↓existsAndEq, true_and, exists_and_right, Q] at ht
        rcases ht with ⟨p, -, rfl⟩
        exact inter_subset_right

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

Goal state before:
pp: n : ℕ
hn : n ≤ 2
⊢ exponent (ZMod (2 ^ n))ˣ = Fintype.card (ZMod (2 ^ n))ˣ

Tactic:
Fintype.card_eq_nat_card

Goal state after:
n : ℕ
hn : n ≤ 2
⊢ exponent (ZMod (2 ^ n))ˣ = Nat.card (ZMod (2 ^ n))ˣ
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: case neg.refine_1
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
⊢ exponent (ZMod (2 ^ n))ˣ ∣ 2 ^ (n - 2)

pp: case neg.refine_2
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
⊢ 2 ^ (n - 2) ∣ exponent (ZMod (2 ^ n))ˣ

Tactic:
· have hcard : Nat.card (ZMod (2 ^ n))ˣ = 2 ^ (n - 1) := by
      rw [card_eq_fintype_card, ZMod.card_units_eq_totient, totient_prime_pow prime_two <| by lia,
        Nat.add_one_sub_one, mul_one]
    have ⟨k, hk, h⟩ := dvd_prime_pow prime_two |>.mp <| hcard ▸ Group.exponent_dvd_nat_card
    have := IsCyclic.iff_exponent_eq_card.not.mp <| ZMod.isCyclic_units_two_pow_iff n |>.not.mpr hn'
    exact h ▸ Nat.pow_dvd_pow 2 (by grind)

Goal state after:
case neg.refine_2
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
⊢ 2 ^ (n - 2) ∣ exponent (ZMod (2 ^ n))ˣ
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: p n : ℕ
hp : Nat.Prime p
hp₂ : p ≠ 2
this : NeZero p
⊢ exponent (ZMod (p ^ n))ˣ = Fintype.card (ZMod (p ^ n))ˣ

Tactic:
Fintype.card_eq_nat_card

Goal state after:
p n : ℕ
hp : Nat.Prime p
hp₂ : p ≠ 2
this : NeZero p
⊢ exponent (ZMod (p ^ n))ˣ = Nat.card (ZMod (p ^ n))ˣ
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
⊢ IntegrableOn (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc a b) volume

Tactic:
obtain hb | hb := eq_or_lt_of_le (Nat.floor_le_floor hab)

Goal state after:
case inl.inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ = ⌊b⌋₊
⊢ IntegrableOn (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc a b) volume

case inl.inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
⊢ IntegrableOn (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc a b) volume
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: n : ℕ
⊢ 0 ≤ Λ n

Tactic:
vonMangoldt_apply

Goal state after:
n : ℕ
⊢ 0 ≤ if IsPrimePow n then Real.log ↑n.minFac else 0
Module: Mathlib.NumberTheory.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
h : ↑p ∣ a - b
k : ℕ
ih : ↑p ^ (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* R ⧸ span {↑p} := mk (span {↑p})
r : R
⊢ ↑p ∣ r ↔ f r = 0

Tactic:
by rw [eq_zero_iff_mem, mem_span_singleton]

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

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

Tactic:
obtain hb | hb := eq_or_lt_of_le (Nat.floor_le_floor hab)

Goal state after:
case inl
𝕜 : 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⌋₊
⊢ ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f ↑k * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊a⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k

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

Goal state before:
pp: case inl
⊢ IsCyclic (ZMod (4 * 0))ˣ ↔ 0 = 0 ∨ 0 = 1

Tactic:
simp [isCyclic_units_zero]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
⊢ (pderiv R i) (X i) = 1

Tactic:
by
  classical
  ext n
  simp only [coeff_pderiv, coeff_X, boole_mul, add_eq_right, coeff_one]
  split_ifs <;> simp_all

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:

Tactic:
∫⁻ (a : X) in s, ‖f a‖ₑ ∂(μ.transpose B).variation
  _ ≤ ∫⁻ a in s, ‖g a‖ₑ ∂(μ.transpose B).variation + δ := I1
  _ = ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (g ⁻¹' {i}) + δ := by rw [I2]
  _ ≤ (∑ i ∈ g.range.sigma P, ‖i.1‖ₑ * ‖(μ.transpose B).restrict s i.2‖ₑ + δ) + δ := by gcongr
  _ ≤ ((∑ i ∈ g.range.sigma P, ‖∫ᵛ x in i.2, f x ∂[B; μ.restrict s]‖ₑ + δ) + δ) + δ := by gcongr
  _ = (∑ i ∈ g.range.sigma P, ‖∫ᵛ x in i.2, f x ∂[B; μ.restrict s]‖ₑ) + 3 * δ := by ring
  _ ≤ (μ.withDensity f B).variation s + 3 * δ := by gcongr
  _ ≤ (μ.withDensity f B).variation s + ε := by
    simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, ENNReal.coe_div, ENNReal.coe_ofNat, δ]
    rw [ENNReal.mul_div_cancel (by simp) (by simp)]

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

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

Tactic:
simp [isCyclic_units_zero]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: case inl
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 : Subsingleton E
⊢ (μ.withDensityᵥ f).variation = μ.withDensity fun x ↦ ‖f x‖ₑ

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
⊢ (μ.withDensityᵥ f).variation = μ.withDensity fun x ↦ ‖f x‖ₑ

Tactic:
· simp [show f = 0 from Subsingleton.elim _ _]

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
⊢ (μ.withDensityᵥ f).variation = μ.withDensity fun x ↦ ‖f x‖ₑ
Module: Mathlib.RingTheory.PowerSeries.Exp

Goal state before:
pp: A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ k ∈ Finset.range n, exp A ^ k = mk fun p ↦ ∑ k ∈ Finset.range n, ↑k ^ p * (algebraMap ℚ A) (↑p !)⁻¹

Tactic:
simp only [exp_pow_eq_rescale_exp, rescale]
  ext
  simp only [one_div, coeff_mk, coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
    coeff_exp, map_sum]

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

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

Tactic:
← Icc_add_one_left_eq_Ioc,

Goal state after:
case inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 1 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 1 b) volume
hb : 1 ≤ b
this : 1 ≤ ⌊b⌋₊
⊢ f ↑0 * c 0 + ∑ x ∈ Icc (0 + 1) ⌊b⌋₊, f ↑x * c x =
    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: n : ℕ
⊢ n#.primeFactors = n.primesLE

Tactic:
primorial_eq_prod_primesLE

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

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

Tactic:
exact fun h ↦ h.even_sub_one <| mt succ.inj hn1

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: 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

Tactic:
mul_sum,

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
this : ∑ p ∈ antidiagonal n, bernoulli' p.1 / ↑p.1! * ((↑p.2 + 1) * ↑p.2!)⁻¹ = (↑n !)⁻¹
⊢ (coeff (n + 1, 0).1) (PowerSeries.mk fun n ↦ (algebraMap ℚ A) (bernoulli' n / ↑n !)) *
        (coeff (n + 1, 0).2) (exp A - 1) +
      ∑ p ∈ antidiagonal n,
        (coeff (p.1, p.2 + 1).1) (PowerSeries.mk fun n ↦ (algebraMap ℚ A) (bernoulli' n / ↑n !)) *
          (coeff (p.1, p.2 + 1).2) (exp A - 1) =
    (coeff (n + 1)) (exp A * X)

Tactic:
simpa [map_sum, Nat.factorial] using congr_arg (algebraMap ℚ A) this

Goal state after:
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:
· simp_rw [Nat.floor_eq_zero.mpr hb, Icc_self, sum_singleton, Nat.cast_zero, hc, mul_zero,
      Set.Ioc_eq_empty_of_le hb.le, Measure.restrict_empty, integral_zero_measure, sub_self]

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
⊢ Squarefree (n#)

Tactic:
primorial_eq_prod_primesLE

Goal state after:
n : ℕ
⊢ Squarefree (∏ p ∈ n.primesLE, p)
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
⊢ Squarefree (n#)

Tactic:
rw [primorial_eq_prod_primesLE]
  refine Finset.squarefree_prod_of_pairwise_isCoprime (fun _ hp _ hq hpq ↦ ?_)
    fun _ hp ↦ (prime_of_mem_primesLE hp).squarefree
  simp only [← coprime_iff_isRelPrime]
  exact (coprime_primes (prime_of_mem_primesLE hp) (prime_of_mem_primesLE hq)).mpr hpq

Goal state after:
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
⊢ n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)

Tactic:
have n_pos : 0 < n := (Nat.zero_le _).trans_lt n_large

Goal state after:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
⊢ n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (deriv fun t ↦ ‖f t‖) (Set.Ici 1) volume
h_bdd : (fun n ↦ ‖f ↑n‖ * ∑ k ∈ Icc 1 n, ‖c k‖) =O[atTop] fun x ↦ 1
g : ℝ → ℝ
hg₁ : (fun t ↦ deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 1 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
n : ℕ
⊢ ∑ k ∈ Icc 1 n, ‖c k‖ = ‖(fun n ↦ if n = 0 then 0 else c n) 0‖ + ∑ x ∈ Ioc 0 n, ‖(fun n ↦ if n = 0 then 0 else c n) x‖

Tactic:
← Icc_add_one_left_eq_Ioc,

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (deriv fun t ↦ ‖f t‖) (Set.Ici 1) volume
h_bdd : (fun n ↦ ‖f ↑n‖ * ∑ k ∈ Icc 1 n, ‖c k‖) =O[atTop] fun x ↦ 1
g : ℝ → ℝ
hg₁ : (fun t ↦ deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 1 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
n : ℕ
⊢ ∑ k ∈ Icc 1 n, ‖c k‖ =
    ‖(fun n ↦ if n = 0 then 0 else c n) 0‖ + ∑ x ∈ Icc (0 + 1) n, ‖(fun n ↦ if n = 0 then 0 else c n) x‖
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue

Goal state before:
pp: case succ.refine_2
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h✝ : abv.IsAdmissible
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (h✝.card ε ^ n).succ → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (h✝.card ε ^ (n + 1)).succ → Fin (n + 1) → R
M : ℕ := h✝.card ε
s : Fin (M ^ n).succ → Fin (M ^ n.succ).succ
s_inj : Function.Injective s
hs : ∀ (i₀ i₁ : Fin (M ^ n).succ), ↑(abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < abv b • ε
k₀ k₁ : Fin (h✝.card ε ^ n).succ
hk : k₀ ≠ k₁
h : ∀ (k : Fin n), ↑(abv (Fin.tail (A (s k₁)) k % b - Fin.tail (A (s k₀)) k % b)) < abv b • ε
i✝ : Fin (n + 1)
i : Fin n
⊢ ↑(abv (A (s k₁) i.succ % b - A (s k₀) i.succ % b)) < abv b • ε

Tactic:
· exact h i

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
norm_cast at ⊢ this

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

Goal state before:
pp: x : ℝ
⊢ θ x = θ ↑⌊x⌋₊

Tactic:
unfold theta
  rw [floor_natCast]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ Monotone ψ

Tactic:
intro x y hxy

Goal state after:
x y : ℝ
hxy : x ≤ y
⊢ ψ x ≤ ψ y
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ Monotone θ

Tactic:
intro x y hxy

Goal state after:
x y : ℝ
hxy : x ≤ y
⊢ θ x ≤ θ y
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k m p : ℕ
hm_lt : m < k
inst✝ : Fact (Nat.Prime p)
ih : pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p)
⊢ pIntegral p (bernoulli (2 * m) * ↑((2 * k + 1).choose (2 * m)) * ↑p ^ (2 * k - 2 * m) / (2 * ↑k + 1))

Tactic:
by
  have hp_ne : (p : ℚ) ≠ 0 := mod_cast (Nat.Prime.ne_zero Fact.out)
  set P := (p : ℚ) ^ (2 * k - 2 * m - 1)
  have hpow : (p : ℚ) ^ (2 * k - 2 * m) = P * p := by
    rw [show 2 * k - 2 * m = (2 * k - 2 * m - 1) + 1 by lia, pow_succ]
  have 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) := by rw [hpow]; field_simp [hp_ne]; ring
  rw [hdecomp]
  have hcmp := pIntegral_choose_mul_pow_div (p := p) hm_lt (by lia)
  have H x := choose_two_mul_succ_mul_div_eq x hm_lt
  apply (Rat.padicValuation p).map_sub_le
  · rw [mul_assoc, mul_div_assoc]
    apply pIntegral_mul ih
    have hpow_mul : ((2 * k).choose (2 * m) : ℚ) * (p : ℚ) ^ (2 * k - 2 * m) /
        (2 * k - 2 * m + 1) =
        (p : ℚ) * (((2 * k).choose (2 * m) : ℚ) * P / (2 * k - 2 * m + 1)) := by
      rw [hpow]; ring
    rw [H, hpow_mul]
    exact pIntegral_mul (Int.padicValuation_le_one p p) hcmp
  · unfold vonStaudtIndicator
    split_ifs
    · grind
    · simp

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k₁ p₁ : ℕ
⊢ k₁ ≠ 0 →
    k₁ ≤ N →
      p₁ ≠ 0 →
        ↑p₁ ≤ x →
          Nat.Prime p₁ →
            ↑p₁ ≤ x ^ (↑k₁)⁻¹ →
              ∀ (a b : ℕ),
                a ≠ 0 → a ≤ N → b ≠ 0 → ↑b ≤ x → Nat.Prime b → ↑b ≤ x ^ (↑a)⁻¹ → p₁ ^ k₁ = b ^ a → k₁ = a ∧ p₁ = b

Tactic:
hk₁

Goal state after:
case refine_2
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
⊢ k₁ ≤ N →
    p₁ ≠ 0 →
      ↑p₁ ≤ x →
        Nat.Prime p₁ →
          ↑p₁ ≤ x ^ (↑k₁)⁻¹ →
            ∀ (a b : ℕ),
              a ≠ 0 → a ≤ N → b ≠ 0 → ↑b ≤ x → Nat.Prime b → ↑b ≤ x ^ (↑a)⁻¹ → p₁ ^ k₁ = b ^ a → k₁ = a ∧ p₁ = b
Module: Mathlib.NumberTheory.FunctionField

Goal state before:
pp: F : Type u_3
K : Type u_4
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Algebra F⟮X⟯ K
inst✝² : FunctionField F K
inst✝¹ : Algebra F K
inst✝ : IsScalarTower F F⟮X⟯ K
y : K
hy : Transcendental F y
x : K := (algebraMap F⟮X⟯ K) X
Fyx : IntermediateField F K := restrictScalars F (↥F⟮y⟯)⟮x⟯
Fxy : IntermediateField F K := restrictScalars F (↥F⟮x⟯)⟮y⟯
this✝⁶ : Algebra ↥F⟮y⟯ ↥Fyx := (↥F⟮y⟯)⟮x⟯.algebra
this✝⁵ : Module ↥F⟮y⟯ ↥Fyx := Algebra.toModule
this✝⁴ : SMul ↥F⟮y⟯ ↥Fyx := this✝⁶.toSMul
this✝³ : Algebra ↥F⟮x⟯ ↥Fxy := (↥F⟮x⟯)⟮y⟯.algebra
this✝² : Module ↥F⟮x⟯ ↥Fxy := Algebra.toModule
this✝¹ : SMul ↥F⟮x⟯ ↥Fxy := this✝³.toSMul
this✝ : FiniteDimensional ↥F⟮y⟯ ↥Fyx
this : FiniteDimensional (↥F⟮(algebraMap F⟮X⟯ K) X⟯) K
⊢ FiniteDimensional (↥Fyx) K

Tactic:
unfold Fyx

Goal state after:
F : Type u_3
K : Type u_4
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Algebra F⟮X⟯ K
inst✝² : FunctionField F K
inst✝¹ : Algebra F K
inst✝ : IsScalarTower F F⟮X⟯ K
y : K
hy : Transcendental F y
x : K := (algebraMap F⟮X⟯ K) X
Fyx : IntermediateField F K := restrictScalars F (↥F⟮y⟯)⟮x⟯
Fxy : IntermediateField F K := restrictScalars F (↥F⟮x⟯)⟮y⟯
this✝⁶ : Algebra ↥F⟮y⟯ ↥Fyx := (↥F⟮y⟯)⟮x⟯.algebra
this✝⁵ : Module ↥F⟮y⟯ ↥Fyx := Algebra.toModule
this✝⁴ : SMul ↥F⟮y⟯ ↥Fyx := this✝⁶.toSMul
this✝³ : Algebra ↥F⟮x⟯ ↥Fxy := (↥F⟮x⟯)⟮y⟯.algebra
this✝² : Module ↥F⟮x⟯ ↥Fxy := Algebra.toModule
this✝¹ : SMul ↥F⟮x⟯ ↥Fxy := this✝³.toSMul
this✝ : FiniteDimensional ↥F⟮y⟯ ↥Fyx
this : FiniteDimensional (↥F⟮(algebraMap F⟮X⟯ K) X⟯) K
⊢ FiniteDimensional (↥(restrictScalars F (↥F⟮y⟯)⟮x⟯)) K
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
N₁ N₂ N₃ N₅ N₇ : ℕ
N : ℕ := N₁ + N₂ + N₃ + N₅ + N₇
h7 : ψ (x ^ (↑7)⁻¹) = ∑ k ∈ Icc 1 N, b x (7 * k)
h5 : ψ (x ^ (↑5)⁻¹) = ∑ k ∈ Icc 1 N, b x (5 * k)
h3 : ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 (2 * N), b x (3 * k)
h2 : ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 (3 * N), b x (2 * k)
h1 : ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 (1 + 6 * N), b x (1 * k)
⊢ ∑ n ∈ Icc 1 N, c x n ≤ ∑ n ∈ Icc 1 N, b x (5 * n)

Tactic:
apply sum_le_sum

Goal state after:
x : ℝ
hx : 0 ≤ x
N₁ N₂ N₃ N₅ N₇ : ℕ
N : ℕ := ⋯
h7 : ψ (x ^ (↑7)⁻¹) = ∑ k ∈ Icc 1 N, b x (7 * k)
h5 : ψ (x ^ (↑5)⁻¹) = ∑ k ∈ Icc 1 N, b x (5 * k)
h3 : ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 (2 * N), b x (3 * k)
h2 : ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 (3 * N), b x (2 * k)
h1 : ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 (1 + 6 * N), b x (1 * k)
⊢ ∀ i ∈ Icc 1 N, c x i ≤ b x (5 * i)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
⊢ modPart p r < ↑p

Tactic:
convert! Int.emod_lt_abs _ _
  · simp
  · exact mod_cast hp_prime.1.ne_zero

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
N₁ N₂ N₃ N₅ N₇ : ℕ
N : ℕ := N₁ + N₂ + N₃ + N₅ + N₇
h7 : ψ (x ^ (↑7)⁻¹) = ∑ k ∈ Icc 1 N, b x (7 * k)
h5 : ψ (x ^ (↑5)⁻¹) = ∑ k ∈ Icc 1 N, b x (5 * k)
h3 : ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 (2 * N), b x (3 * k)
h2 : ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 (3 * N), b x (2 * k)
h1 : ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 (1 + 6 * N), b x (1 * k)
this : ∑ n ∈ Icc 1 N, c x n ≤ ∑ n ∈ Icc 1 N, b x (5 * n)
⊢ ∑ n ∈ Icc 1 N, b x (7 * n) ≤ ∑ n ∈ Icc 1 N, c x n

Tactic:
apply sum_le_sum

Goal state after:
x : ℝ
hx : 0 ≤ x
N₁ N₂ N₃ N₅ N₇ : ℕ
N : ℕ := ⋯
h7 : ψ (x ^ (↑7)⁻¹) = ∑ k ∈ Icc 1 N, b x (7 * k)
h5 : ψ (x ^ (↑5)⁻¹) = ∑ k ∈ Icc 1 N, b x (5 * k)
h3 : ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 (2 * N), b x (3 * k)
h2 : ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 (3 * N), b x (2 * k)
h1 : ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 (1 + 6 * N), b x (1 * k)
this : ∑ n ∈ Icc 1 N, c x n ≤ ∑ n ∈ Icc 1 N, b x (5 * n)
⊢ ∀ i ∈ Icc 1 N, b x (7 * i) ≤ c x i
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : ↑p ^ n ∣ x - ↑a
hb : ↑p ^ n ∣ x - ↑b
⊢ ↑p ^ n ∣ a - b

Tactic:
rw [← dvd_neg, neg_sub] at ha

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : ↑p ^ n ∣ ↑a - x
hb : ↑p ^ n ∣ x - ↑b
⊢ ↑p ^ n ∣ a - b
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
g : L ≃+* L
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : g ζ = ↑(⋯.unit ^ aux g (p ^ (k + i)))
H₂ : (⋯.unit ^ aux g (p ^ (k + i))) ^ p ^ i = ⋯.unit ^ aux g (p ^ k)
⊢ ↑p ^ k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)

Tactic:
h_unit,

Goal state after:
L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
g : L ≃+* L
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : g ζ = ↑(⋯.unit ^ aux g (p ^ (k + i)))
H₂ : (⋯.unit ^ aux g (p ^ (k + i))) ^ p ^ i = (⋯.unit ^ p ^ i) ^ aux g (p ^ k)
⊢ ↑p ^ k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case hbc
x : ℝ
hx : 1 ≤ x
⊢ ↑(#({a ∈ ⌊x⌋₊.primesLE | ↑a ≤ √x})) ≤ √x

Tactic:
refine le_trans ?_ <| floor_le (sqrt_nonneg x)

Goal state after:
case hbc
x : ℝ
hx : 1 ≤ x
⊢ ↑(#({a ∈ ⌊x⌋₊.primesLE | ↑a ≤ √x})) ≤ ↑⌊√x⌋₊