mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case empty
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : AddMonoid.FG M
S : Set (Set M)
hS' : ∀ s ∈ ∅, IsSemilinearSet s
⊢ IsSemilinearSet (⋂₀ ∅)

Tactic:
| empty =>

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

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
⊢ ⊤ ≤ span ℚ (⇑toRatVec '' range ⇑(Pi.basisFun ℕ ι))

Tactic:
rw [top_le_iff]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
⊢ span ℚ (⇑toRatVec '' range ⇑(Pi.basisFun ℕ ι)) = ⊤
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝⁵ : Preorder ι
G : ι → Type w
inst✝⁴ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝³ : IsDirectedOrder ι
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝¹ : Nonempty ι
P : Type u₁
inst✝ : L.Structure P
g : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
n✝ : ℕ
R : L.Relations n✝
i : ι
y : Fin n✝ → G i
⊢ RelMap R (Quotient.lift (fun x ↦ (g x.fst) x.snd) ⋯ ∘ fun a ↦ ⟦Structure.Sigma.mk f i (y a)⟧) ↔
    RelMap R fun a ↦ ⟦Structure.Sigma.mk f i (y a)⟧

Tactic:
change RelMap R (Quotient.lift _ _ ∘ Quotient.mk _ ∘ Structure.Sigma.mk f i ∘ y) ↔ _

Goal state after:
L : Language
ι : Type v
inst✝⁵ : Preorder ι
G : ι → Type w
inst✝⁴ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝³ : IsDirectedOrder ι
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝¹ : Nonempty ι
P : Type u₁
inst✝ : L.Structure P
g : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
n✝ : ℕ
R : L.Relations n✝
i : ι
y : Fin n✝ → G i
⊢ RelMap R (Quotient.lift (fun x ↦ (g x.fst) x.snd) ⋯ ∘ Quotient.mk (setoid G f) ∘ Structure.Sigma.mk f i ∘ y) ↔
    RelMap R fun a ↦ ⟦Structure.Sigma.mk f i (y a)⟧
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : DenselyOrdered β
inst✝¹ : NoMinOrder β
inst✝ : NoMaxOrder β
nonem : Nonempty β
S : Finset α
f : ↥S ↪o β
b : β
x y : α
hxS : x ∉ S
Slt : Finset β := Finset.image (⇑f) ({x_1 ∈ S.attach | ↑x_1 < x})
Sgt : Finset β := Finset.image (⇑f) ({x_1 ∈ S.attach | x < ↑x_1})
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
hx : x ∈ insert x S
hy : y ∈ insert x S
hxy : ⟨x, hx⟩ < ⟨y, hy⟩
hyS : y ∉ S
⊢ (fun x_1 ↦ if hx : ↑x_1 ∈ S then f ⟨↑x_1, hx⟩ else b) ⟨x, hx⟩ <
    (fun x_1 ↦ if hx : ↑x_1 ∈ S then f ⟨↑x_1, hx⟩ else b) ⟨y, hy⟩

Tactic:
simp only [Finset.eq_of_mem_insert_of_notMem hy hyS, lt_self_iff_false] at hxy

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

Goal state before:
pp: case mpr.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
n : ℕ
heq : hs.floor (x + (n + 1) • ↑i) i = 0
⊢ hs.floor x i < 0

Tactic:
hs.floor_add_nsmul_self,

Goal state after:
case mpr.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
n : ℕ
heq : hs.floor x i + ↑(n + 1) = 0
⊢ hs.floor x i < 0
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mpr.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
n : ℕ
heq : hs.floor x i = hs.floor (hs.base + (n + 1) • ↑i) i
⊢ 0 < hs.floor x i

Tactic:
hs.floor_add_nsmul_self,

Goal state after:
case mpr.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
n : ℕ
heq : hs.floor x i = hs.floor hs.base i + ↑(n + 1)
⊢ 0 < hs.floor x i
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: case zero
a : (ZMod 0)ˣ
⊢ a ^ λ 0 = 1

Tactic:
rw [map_zero, pow_zero]

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

Goal state before:
pp: case pos
n : ℕ
hn : n ≠ 2
hn' : n ≤ 2
⊢ λ (2 ^ n) = 2 ^ (n - 2)

pp: case neg
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
⊢ λ (2 ^ n) = 2 ^ (n - 2)

Tactic:
· grind [carmichael_two_pow_of_le_two]

Goal state after:
case neg
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
⊢ λ (2 ^ n) = 2 ^ (n - 2)
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:

Tactic:
(u * x) ^ p * (p.choose p) = u ^ p * x ^ p := by simp [Nat.choose_self, mul_pow]
    _ = p * u * v * b * x ^ p := by rw [hb]
    _ = p * u * (v * (b * x ^ p)) := by ring_nf

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

Goal state before:
pp: case hP₂.inr
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‖ₑ + ↑δ
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) := Finset.image (fun p ↦ p.snd ∩ s) (g.range.sigma P)
p : Set X
i : X
hi : p ∈ P (g i)
q : Set X
j : X
hj : q ∈ P (g j)
htu : p ∩ s ≠ q ∩ s
hpq : p ≠ q
hij : g i ≠ g j
⊢ Disjoint p q

Tactic:
have : Disjoint (g ⁻¹' {g i}) (g ⁻¹' {g j}) := by grind
          exact this.mono (Pg (g i) p hi) (Pg (g j) q hj)

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
g : MvPowerSeries σ R
n : ℕ
⊢ ↑n * (g ^ (n - 1) * (pderiv R i) g) = ↑n * g ^ (n - 1) * (pderiv R i) g

Tactic:
mul_assoc

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
g : MvPowerSeries σ R
n : ℕ
⊢ ↑n * (g ^ (n - 1) * (pderiv R i) g) = ↑n * (g ^ (n - 1) * (pderiv R i) g)
Module: Mathlib.NumberTheory.BernoulliPolynomials

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

Tactic:
rw [mul_assoc, mul_assoc, ← Nat.cast_mul, ← Nat.cast_mul]

Goal state after:
k m : ℕ
x✝ : m ∈ range (k + 1)
⊢ (monomial (k - m)) (_root_.bernoulli m * ↑((k + 1).choose m * (k + 1 - m))) =
    (monomial (k - m)) (_root_.bernoulli m * ↑(k.choose m * (k + 1)))
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: m n : ℕ
⊢ ∏ x ∈ Ico 0 (m + n + 1) with Nat.Prime x, x =
    (∏ x ∈ Ico 0 (m + 1) with Nat.Prime x, x) * ∏ x ∈ Ico (m + 1) (m + n + 1) with Nat.Prime x, x

Tactic:
← prod_union,

Goal state after:
m n : ℕ
⊢ ∏ x ∈ Ico 0 (m + n + 1) with Nat.Prime x, x =
    ∏ x ∈ {p ∈ Ico 0 (m + 1) | Nat.Prime p} ∪ {p ∈ Ico (m + 1) (m + n + 1) | Nat.Prime p}, x

m n : ℕ
⊢ Disjoint ({p ∈ Ico 0 (m + 1) | Nat.Prime p}) ({p ∈ Ico (m + 1) (m + n + 1) | Nat.Prime p})
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: m : ℕ
ihn : ∀ m_1 < m + m + 1, m_1 ≠ 0 → m_1# < 4 ^ m_1
hn : m + m + 1 ≠ 0
hm : m > 0
⊢ (m + m + 1)# = (m + 1 + m)#

Tactic:
rw [add_right_comm]

Goal state after:
Module: Mathlib.NumberTheory.Bertrand

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

Tactic:
revert h

Goal state after:
case inr
n : ℕ
hn0 : n ≠ 0
⊢ n < 521 → ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n
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
⊢ Summable fun n ↦ f ↑n * c n

Tactic:
have h : ∀ n, ∑ k ∈ Icc 1 n, ‖c k‖ = ∑ k ∈ Icc 0 n, ‖(fun n ↦ if n = 0 then 0 else c n) k‖ := by
    intro n
    rw [Icc_eq_cons_Ioc n.zero_le, sum_cons, ← Icc_add_one_left_eq_Ioc, zero_add]
    simp_rw [if_pos, norm_zero, zero_add]
    exact Finset.sum_congr rfl fun _ h ↦ by rw [if_neg (zero_lt_one.trans_le (mem_Icc.mp h).1).ne']

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
h : ∀ (n : ℕ), ∑ k ∈ Icc 1 n, ‖c k‖ = ∑ k ∈ Icc 0 n, ‖(fun n ↦ if n = 0 then 0 else c n) k‖
⊢ Summable fun n ↦ f ↑n * c n
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case neg
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
hdvd : ¬p - 1 ∣ 2 * k
⊢ ∑ q ∈ vonStaudtPrimes k, 1 / ↑q = vonStaudtIndicator (2 * k) p / ↑p + ∑ q ∈ (vonStaudtPrimes k).erase p, 1 / ↑q

Tactic:
rw [Finset.erase_eq_of_notMem fun h ↦ hdvd (Finset.mem_filter.mp h).2.2]
    simp [vonStaudtIndicator, hdvd]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case neg
p d : ℕ
inst✝ : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
hp2 : 2 ≤ p
n : ℕ
hn : n ≥ 2
hne' : ¬(p = 2 ∧ n = 2)
⊢ n + 1 ≤ p ^ (n - 1)

Tactic:
induction hn with
    | refl => norm_num at hne' ⊢; lia
    | @step m hm IH =>
      by_cases hm2 : p = 2 ∧ m = 2
      · obtain ⟨rfl, rfl⟩ := hm2; norm_num
      · calc m + 1 + 1 ≤ p ^ (m - 1) + 1 := by linarith [IH hm2]
          _ ≤ p ^ (m - 1) * p := by nlinarith [Nat.one_le_pow (m - 1) p (by lia)]
          _ = p ^ m := by rw [show m = m - 1 + 1 by lia]; exact pow_succ ..

Goal state after:
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)
hp_ne : ↑p ≠ 0
P : ℚ := ↑p ^ (2 * k - 2 * m - 1)
hpow : ↑p ^ (2 * k - 2 * m) = P * ↑p
⊢ 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)

Tactic:
hpow

Goal state after:
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
⊢ bernoulli (2 * m) * ↑((2 * k + 1).choose (2 * m)) * (P * ↑p) / (2 * ↑k + 1) =
    (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p) * ↑((2 * k + 1).choose (2 * m)) * (P * ↑p) / (2 * ↑k + 1) -
      vonStaudtIndicator (2 * m) p * ↑((2 * k + 1).choose (2 * m)) * P / (2 * ↑k + 1)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ θ x = ∑ p ∈ Icc 0 ⌊x⌋₊ with Nat.Prime p, log ↑p

Tactic:
theta,

Goal state after:
x : ℝ
⊢ ∑ p ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime p, log ↑p = ∑ p ∈ Icc 0 ⌊x⌋₊ with Nat.Prime p, log ↑p
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)
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)
⊢ ↑((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))

Tactic:
hpow

Goal state after:
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)
⊢ ↑((2 * k).choose (2 * m)) * (P * ↑p) / (2 * ↑k - 2 * ↑m + 1) =
    ↑p * (↑((2 * k).choose (2 * m)) * P / (2 * ↑k - 2 * ↑m + 1))
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x y : ℝ
hxy : x ≤ y
⊢ ψ x ≤ ψ y

Tactic:
apply sum_le_sum_of_subset_of_nonneg

Goal state after:
case h
x y : ℝ
hxy : x ≤ y
⊢ Ioc 0 ⌊x⌋₊ ⊆ Ioc 0 ⌊y⌋₊

case hf
x y : ℝ
hxy : x ≤ y
⊢ ∀ i ∈ Ioc 0 ⌊y⌋₊, i ∉ Ioc 0 ⌊x⌋₊ → 0 ≤ Λ i
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x y : ℝ
hxy : x ≤ y
⊢ θ x ≤ θ y

Tactic:
apply sum_le_sum_of_subset_of_nonneg

Goal state after:
case h
x y : ℝ
hxy : x ≤ y
⊢ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p} ⊆ {p ∈ Ioc 0 ⌊y⌋₊ | Nat.Prime p}

case hf
x y : ℝ
hxy : x ≤ y
⊢ ∀ i ∈ {p ∈ Ioc 0 ⌊y⌋₊ | Nat.Prime p}, i ∉ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p} → 0 ≤ log ↑i
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ ∀ ⦃i : ℕ⦄,
    i ∈ ↑(filter Nat.Prime (Icc 1 n)) →
      ∀ ⦃j : ℕ⦄,
        j ∈ ↑(filter Nat.Prime (Icc 1 n)) →
          (image (fun x ↦ i ^ x) (Icc 1 (Nat.log i n)) ∩ image (fun x ↦ j ^ x) (Icc 1 (Nat.log j n))).Nonempty → i = j

Tactic:
grind [Prime.pow_inj']

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case h₂
x : ℝ
hx✝ : 0 ≤ x
hx : 1 ≤ x
⊢ 2 * x ^ (1 / 2) * x ^ (1 / 2) / (1 / 2) ≤ 4 * x

Tactic:
← mul_one_div

Goal state after:
case h₂
x : ℝ
hx✝ : 0 ≤ x
hx : 1 ≤ x
⊢ 2 * x ^ (1 / 2) * x ^ (1 / 2) * (1 / (1 / 2)) ≤ 4 * x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case h₂
x : ℝ
hx✝ : 0 ≤ x
hx : 1 ≤ x
⊢ 2 * x ^ (1 / 2) * x ^ (1 / 2) * (1 / (1 / 2)) ≤ 4 * x

Tactic:
mul_assoc

Goal state after:
case h₂
x : ℝ
hx✝ : 0 ≤ x
hx : 1 ≤ x
⊢ 2 * (x ^ (1 / 2) * x ^ (1 / 2)) * (1 / (1 / 2)) ≤ 4 * x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ ∑ n ∈ Ioc 0 ⌊x⌋₊, Λ n - θ x = ∑ n ∈ Ioc 0 ⌊x⌋₊ with ¬Nat.Prime n, Λ n

Tactic:
theta,

Goal state after:
x : ℝ
⊢ ∑ n ∈ Ioc 0 ⌊x⌋₊, Λ n - ∑ p ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime p, log ↑p = ∑ n ∈ Ioc 0 ⌊x⌋₊ with ¬Nat.Prime n, Λ n
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: C : ℝ
hC : ∀ (x : ℝ), ψ x - θ x ≤ C * √x
x : ℝ
x✝ : 0 ≤ x
this : θ x ≤ ψ x
⊢ ψ x - θ x ≤ C * √x

Tactic:
exact hC x

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x x✝ : ℝ
| θ x✝ / (x✝ * log x✝ ^ 2)

Tactic:
theta,

Goal state after:
x x✝ : ℝ
| (∑ p ∈ Ioc 0 ⌊x✝⌋₊ with Nat.Prime p, log ↑p) / (x✝ * log x✝ ^ 2)
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 ^ p ^ i) ^ aux g (p ^ k) = 1
⊢ ↑p ^ k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)

Tactic:
simp only [← zpow_natCast, ← zpow_mul, div_eq_mul_inv, ← zpow_sub] at H₂

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) - ↑(p ^ i) * aux g (p ^ k)) = 1
⊢ ↑p ^ k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
a✝ : 4 ≤ x
⊢ IntervalIntegrable (fun x ↦ log 4 * (1 / log x ^ 2)) volume 2 x

Tactic:
refine (intervalIntegrable_one_div_log_sq ?_ ?_).const_mul _ <;> linarith

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 1 < x
⊢ 1 ^ 2 < x

Tactic:
by simp [hx]

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r : R
n k : ℕ
hk : ∀ n_1 ≥ k, ‖limNthHom f_compat r - ↑(nthHom f r n_1)‖ < ↑p ^ (-↑n)
this : limNthHom f_compat r - ↑(nthHom f r (max n k)) ∈ Ideal.span {↑p ^ n}
⊢ (lift f_compat) r - ↑((f n) r).val ∈ Ideal.span {↑p ^ n}

Tactic:
dsimp [lift]

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r : R
n k : ℕ
hk : ∀ n_1 ≥ k, ‖limNthHom f_compat r - ↑(nthHom f r n_1)‖ < ↑p ^ (-↑n)
this : limNthHom f_compat r - ↑(nthHom f r (max n k)) ∈ Ideal.span {↑p ^ n}
⊢ limNthHom f_compat r - ↑((f n) r).val ∈ Ideal.span {↑p ^ n}
Module: Mathlib.NumberTheory.Cyclotomic.Gal

Goal state before:
pp: n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ✝ : IsPrimitiveRoot μ n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
h : Irreducible (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := zeta_spec n K L
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) n :=
  fun t ↦ IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)
f : L ≃ₐ[K] L
⊢ ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) ⋯)
      (IsPrimitiveRoot.powerBasis K hζ).gen =
    f (IsPrimitiveRoot.powerBasis K hζ).gen

Tactic:
rw [PowerBasis.equivOfMinpoly_gen]

Goal state after:
n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ✝ : IsPrimitiveRoot μ n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
h : Irreducible (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := zeta_spec n K L
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) n :=
  fun t ↦ IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)
f : L ≃ₐ[K] L
⊢ (IsPrimitiveRoot.powerBasis K ⋯).gen = f (IsPrimitiveRoot.powerBasis K hζ).gen
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: f : ℕ → ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
⊢ (toZModPow n) x = ↑(f n)

Tactic:
let s : PadicSeq p := ⟨(f ·), isCauSeq_padicNorm_of_pow_dvd_sub f p hi⟩

Goal state after:
f : ℕ → ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := ⟨fun x ↦ ↑(f x), ⋯⟩
⊢ (toZModPow n) x = ↑(f n)
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝³ x✝² x✝¹ : Poly α
x✝ : α → ℕ
⊢ x✝³ x✝ * x✝² x✝ * x✝¹ x✝ = x✝³ x✝ * (x✝² x✝ * x✝¹ x✝)

Tactic:
mul_assoc

Goal state after:
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: c d x y z w : ℕ
xy : SqLe x c y d
zw : SqLe z c w d
⊢ SqLe (x + z) c (y + w) d

Tactic:
by
  have xz := sqLe_add_mixed xy zw
  simp only [SqLe, mul_assoc] at xy zw
  simp [SqLe, mul_add, mul_comm, mul_left_comm, add_le_add, *]

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case e_a
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
H :
  (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) * ↑p ^ p ^ k = ↑p ^ (p ^ k * (k + 1) * (p - 1))
hnorm : (Algebra.norm K) (ζ ^ p ^ k - 1) = ↑p ^ p ^ k
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) = ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))

Tactic:
mul_assoc

Goal state after:
case e_a
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
H :
  (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) * ↑p ^ p ^ k =
    ↑p ^ (p ^ k * ((k + 1) * (p - 1)))
hnorm : (Algebra.norm K) (ζ ^ p ^ k - 1) = ↑p ^ p ^ k
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) = ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
⊢ xz a1 (m - n) = xz a1 m * xz a1 n - ↑(d a1) * yz a1 m * yz a1 n

Tactic:
rw [sub_eq_add_neg, ← mul_neg]

Goal state after:
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
⊢ xz a1 (m - n) = xz a1 m * xz a1 n + ↑(d a1) * yz a1 m * -yz a1 n
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case e_a.refine_2
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
hnorm : (Algebra.norm K) (ζ ^ p ^ k - 1) = ↑p ^ p ^ k
this : 0 < k.succ * (p - 1)
H : (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) = ↑p ^ (p ^ k * (k.succ * (p - 1)).pred)
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) = ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))

Tactic:
simp only [H, mul_comm _ (k + 1)]; norm_cast

Goal state after:
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case mp
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * z.im * z.im) = 0
⊢ z = 0

Tactic:
mul_assoc

Goal state after:
case mp
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
⊢ z = 0