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‖ₑ + ρ)
⊢ ∑ x ∈ g.range, ‖x‖ₑ * ∑ p ∈ P x, ‖((μ.transpose B).restrict s) p‖ₑ + ∑ x ∈ g.range, ‖x‖ₑ * ρ ≤
    ∑ i ∈ g.range, ∑ p ∈ P i, ‖i‖ₑ * ‖((μ.transpose B).restrict s) p‖ₑ + ↑δ

Tactic:
Finset.mul_sum

Goal state after:
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‖ₑ + ρ)
⊢ ∑ x ∈ g.range, ∑ i ∈ P x, ‖x‖ₑ * ‖((μ.transpose B).restrict s) i‖ₑ + ∑ x ∈ g.range, ‖x‖ₑ * ρ ≤
    ∑ i ∈ g.range, ∑ p ∈ P i, ‖i‖ₑ * ‖((μ.transpose B).restrict s) p‖ₑ + ↑δ
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: X : Type u_2
E : Type u_4
F : Type u_5
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
μ : VectorMeasure X F
β : Type u_9
inst✝ : MeasurableSpace β
φ : X → β
hφ : MeasurableEmbedding φ
f : β → E
⊢ Integrable f (μ.map φ).variation ↔ Integrable (f ∘ φ) μ.variation

Tactic:
← hφ.integrable_map_iff,

Goal state after:
X : Type u_2
E : Type u_4
F : Type u_5
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
μ : VectorMeasure X F
β : Type u_9
inst✝ : MeasurableSpace β
φ : X → β
hφ : MeasurableEmbedding φ
f : β → E
⊢ Integrable f (μ.map φ).variation ↔ Integrable f (Measure.map φ μ.variation)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case neg.hu₁
M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : M → AddSubmonoid M := ⋯
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : M → AddSemigroupIdeal M := ⋯
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun x ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
u : M
hu₁ : u ∈ f a
hu₂ : u ≠ 0
hxu : a + x + u ∈ s
w' u' : M
hu'₁ : u' ∈ f a
hu'₂ : u' ≠ 0
ih : ∀ y < w' + u', ∀ u ∈ f a, u ≠ 0 → a + x + (y + u) ∈ s → y + u ∈ f a
hxy : a + x + (w' + u' + u) ∈ s
hw₁ : ¬w' + u' = 0
⊢ u' + u ∈ f a

Tactic:
exact add_mem hu'₁ hu₁

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

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
⊢ (∃ a n f, s = a +ᵥ range ⇑f) ↔ ∃ v n A, s = {x | ∃ x_1, v + A *ᵥ x_1 = x}

Tactic:
refine exists₂_congr fun v n => ⟨fun ⟨f, hf⟩ => ⟨f.toNatLinearMap.toMatrix', ?_⟩, fun ⟨A, hA⟩ =>
    ⟨A.mulVecLin, ?_⟩⟩ <;> ext

Goal state after:
case refine_1
ι : Type u_3
s : Set (ι → ℕ)
v : ι → ℕ
n : ℕ
x✝¹ : ∃ f, s = v +ᵥ range ⇑f
f : (Fin n → ℕ) →+ ι → ℕ
hf : s = v +ᵥ range ⇑f
x✝ : ι → ℕ
⊢ x✝ ∈ s ↔ x✝ ∈ {x | ∃ x_1, v + LinearMap.toMatrix' f.toNatLinearMap *ᵥ x_1 = x}

case refine_2
ι : Type u_3
s : Set (ι → ℕ)
v : ι → ℕ
n : ℕ
x✝¹ : ∃ A, s = {x | ∃ x_1, v + A *ᵥ x_1 = x}
A : Matrix ι (Fin n) ℕ
hA : s = {x | ∃ x_1, v + A *ᵥ x_1 = x}
x✝ : ι → ℕ
⊢ x✝ ∈ s ↔ x✝ ∈ v +ᵥ range ⇑↑A.mulVecLin
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
x y : DirectLimit G f
i : ι
hx : (Quotient.out x).fst ≤ i
hy : (Quotient.out y).fst ≤ i
xy :
  (g i) ((f (Quotient.out x).fst i hx) (Quotient.out x).snd) =
    (g i) ((f (Quotient.out y).fst i hy) (Quotient.out y).snd)
⊢ ⟦Quotient.out x⟧ = ⟦Quotient.out y⟧

Tactic:
Quotient.eq_iff_equiv,

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
x y : DirectLimit G f
i : ι
hx : (Quotient.out x).fst ≤ i
hy : (Quotient.out y).fst ≤ i
xy :
  (g i) ((f (Quotient.out x).fst i hx) (Quotient.out x).snd) =
    (g i) ((f (Quotient.out y).fst i hy) (Quotient.out y).snd)
⊢ Quotient.out x ≈ Quotient.out y
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
i : ι
x : G i
⊢ (lift L ι G f g Hg).toFun ⟦Structure.Sigma.mk f i x⟧ = (g i) x

Tactic:
simp only [lift, Quotient.lift_mk]

Goal state after:
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: case refine_2
L : Language
ι : Type u_1
inst✝⁵ : Countable ι
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type w
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG L (G i)
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
⊢ (Substructure.closure L).toFun (⋃ i, ⇑(of L ι G f i) '' Classical.choose ⋯) = ⊤

Tactic:
rw [eq_top_iff, Substructure.closure_iUnion]

Goal state after:
case refine_2
L : Language
ι : Type u_1
inst✝⁵ : Countable ι
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type w
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG L (G i)
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
⊢ ⊤ ≤ ⨆ i, (Substructure.closure L).toFun (⇑(of L ι G f i) '' Classical.choose ⋯)
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 ι
y : ι → ℕ
hy : y ∈ closure hs.periods
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
⊢ hs.floor (hs.base + y) i = 0

Tactic:
hs.floor_add_of_mem_closure hs.periods_subset_basisSet hi hy,

Goal state after:
case mp.refine_3
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
y : ι → ℕ
hy : y ∈ closure hs.periods
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
⊢ hs.floor hs.base i = 0
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case mp
L : Language
M : Type w
inst✝ : L.Structure M
M_CG : Structure.CG L M
⊢ L.IsUltrahomogeneous M → L.IsExtensionPair M M

Tactic:
intro M_homog ⟨f, f_FG⟩ m

Goal state after:
case mp
L : Language
M : Type w
inst✝ : L.Structure M
M_CG : Structure.CG L M
M_homog : L.IsUltrahomogeneous M
f : M ≃ₚ[L] M
f_FG : f.dom.FG
m : M
⊢ ∃ g, m ∈ (↑g).dom ∧ ⟨f, f_FG⟩ ≤ g
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case inr.inr.inr
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
h2n : ¬2 ∣ n
this✝¹ : Nat.Coprime 4 n
h : (Nat.card (ZMod 4)ˣ).Coprime (Nat.card (ZMod n)ˣ)
this✝ : NeZero n
this : Odd (φ n)
⊢ False

Tactic:
rw [Nat.odd_totient_iff] at this

Goal state after:
case inr.inr.inr
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
h2n : ¬2 ∣ n
this✝¹ : Nat.Coprime 4 n
h : (Nat.card (ZMod 4)ˣ).Coprime (Nat.card (ZMod n)ˣ)
this✝ : NeZero n
this : n = 1 ∨ n = 2
⊢ False
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
⊢ _root_.bernoulli (n - 0) * ↑(n.choose 0) = _root_.bernoulli n

Tactic:
Nat.sub_zero,

Goal state after:
n : ℕ
⊢ _root_.bernoulli n * ↑(n.choose 0) = _root_.bernoulli n
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
← Finset.add_sum_erase _ _ hp_mem

Goal state after:
case pos
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
hdvd : p - 1 ∣ 2 * k
hp_mem : p ∈ vonStaudtPrimes k
⊢ 1 / ↑p + ∑ x ∈ (vonStaudtPrimes k).erase p, 1 / ↑x =
    vonStaudtIndicator (2 * k) p / ↑p + ∑ q ∈ (vonStaudtPrimes k).erase p, 1 / ↑q
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k m p : ℕ
hm_lt : m < k
inst✝ : Fact (Nat.Prime p)
d : ℕ := 2 * k - 2 * m
hd : d ≥ 2
hd_def : d = 2 * k - 2 * m
⊢ pIntegral p (↑((2 * k).choose (2 * m)) * ↑p ^ (d - 1) / (2 * ↑k - 2 * ↑m + 1))

Tactic:
have ⟨hd_plus_one_ne_zero, h_exp, hkm⟩ :
      d + 1 ≠ 0 ∧ 2 * k - 2 * m - 1 = d - 1 ∧ 2 * m ≤ 2 * k := by lia

Goal state after:
k m p : ℕ
hm_lt : m < k
inst✝ : Fact (Nat.Prime p)
d : ℕ := 2 * k - 2 * m
hd : d ≥ 2
hd_def : d = 2 * k - 2 * m
hd_plus_one_ne_zero : d + 1 ≠ 0
h_exp : 2 * k - 2 * m - 1 = d - 1
hkm : 2 * m ≤ 2 * k
⊢ pIntegral p (↑((2 * k).choose (2 * m)) * ↑p ^ (d - 1) / (2 * ↑k - 2 * ↑m + 1))
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : x < 2
n : ℕ
hn : 0 < n ∧ n ≤ ⌊x⌋₊
⊢ n = 1

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

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

Goal state before:
pp: case h₂
x : ℝ
hx : 1 ≤ x
⊢ θ x ≤ log 4 * x

Tactic:
exact theta_le_log4_mul_x (by linarith)

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Polynomial.Bivariate

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
hx : Transcendental R x
p : R[X][Y]
⊢ (algEquivAdjoin hx) (swap p) = (aeval (C ⟨x, ⋯⟩)) p

Tactic:
by
  simp [algEquivAdjoin, Bivariate.aveal_eq_map_swap]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
intro n hn

Goal state after:
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 : ℕ
hn : n ∈ Icc 1 N
⊢ c x n ≤ b x (5 * n)
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
intro n hn

Goal state after:
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 : ℕ
hn : n ∈ Icc 1 N
⊢ b x (7 * n) ≤ c x n
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ (ψ - θ) =O[atTop] Real.sqrt

Tactic:
isBigO_iff,

Goal state after:
⊢ ∃ c, ∀ᶠ (x : ℝ) in atTop, ‖(ψ - θ) x‖ ≤ c * ‖√x‖
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ x - (toZMod x).cast ∈ maximalIdeal ℤ_[p]

Tactic:
convert! sub_zmodRepr_mem x using 2

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ (toZMod x).cast = ↑x.zmodRepr
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 4 ≤ x
⊢ ∫ (x : ℝ) in 2..x, |1 / log x ^ 2| ≤ ‖4 * x / log x ^ 2 + √x / log 2 ^ 2‖

Tactic:
rw [intervalIntegral.integral_congr (g := (fun t ↦ 1 / log t ^ 2))]

Goal state after:
x : ℝ
hx : 4 ≤ x
⊢ ∫ (x : ℝ) in 2..x, 1 / log x ^ 2 ≤ ‖4 * x / log x ^ 2 + √x / log 2 ^ 2‖

x : ℝ
hx : 4 ≤ x
⊢ Set.EqOn (fun x ↦ |1 / log x ^ 2|) (fun t ↦ 1 / log t ^ 2) (Set.uIcc 2 x)
Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs

Goal state before:
pp: b : Basis (Fin 1) ℤ (𝓞 ℚ) := (Basis.singleton (Fin 1) ℤ).map ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm
⊢ (Algebra.traceMatrix ℤ ⇑b).det = (Algebra.trace ℤ (𝓞 ℚ)) (b default * b default)

Tactic:
Matrix.det_unique,

Goal state after:
b : Basis (Fin 1) ℤ (𝓞 ℚ) := (Basis.singleton (Fin 1) ℤ).map ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm
⊢ Algebra.traceMatrix ℤ (⇑b) default default = (Algebra.trace ℤ (𝓞 ℚ)) (b default * b default)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case h
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
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
N : ℕ
hN : ∀ i ≥ N, padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'
⊢ ∀ n ≥ N, ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε

Tactic:
intro n hn

Goal state after:
case h
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
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
N : ℕ
hN : ∀ i ≥ N, padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'
n : ℕ
hn : n ≥ N
⊢ ‖limNthHom f_compat r - ↑(nthHom f r 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
f g : L ≃ₐ[K] L
hfg : (autToPow K hμ) f = (autToPow K hμ) g
⊢ f μ = g μ

Tactic:
← autToPow_spec K hμ g,

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
f g : L ≃ₐ[K] L
hfg : (autToPow K hμ) f = (autToPow K hμ) g
⊢ f μ = μ ^ (↑((autToPow K hμ) g)).val
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: case e'_3
A : Type u
ι : Type w
inst✝² : DecidableEq ι
inst✝¹ : CommRing A
inst✝ : Fintype ι
b b' : Basis ι ℤ A
⊢ IsUnit (b'.toMatrix ⇑b).det

Tactic:
rw [← LinearMap.toMatrix_id_eq_basis_toMatrix b b']

Goal state after:
case e'_3
A : Type u
ι : Type w
inst✝² : DecidableEq ι
inst✝¹ : CommRing A
inst✝ : Fintype ι
b b' : Basis ι ℤ A
⊢ IsUnit ((LinearMap.toMatrix b b') LinearMap.id).det
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case e_a.inr
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
hp2 : p ≠ 2
hpo : Odd p
a : ℕ
ha : p - 1 = 2 * a
⊢ ((-1) ^ (p ^ k * (2 * (p ^ k * a) - 1))) ^ a = (-1) ^ (p ^ k * a)

Tactic:
(hpo.pow.mul _).neg_one_pow,

Goal state after:
case e_a.inr
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
hp2 : p ≠ 2
hpo : Odd p
a : ℕ
ha : p - 1 = 2 * a
⊢ (-1) ^ a = (-1) ^ (p ^ k * 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
hp2 : p ≠ 2
hpo : Odd p
a : ℕ
ha : p - 1 = 2 * a
⊢ Odd (2 * (p ^ k * a) - 1)
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝² x✝¹ x✝ : Poly α
⊢ x✝² + x✝¹ + x✝ = x✝² + (x✝¹ + x✝)

Tactic:
ext; simp_rw [add_apply, ← add_assoc]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
b : ℤ√↑(d a1)
h1 : 1 ≤ b
hp : IsPell b
h : b ≤ pellZd a1 (n + 1)
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
ha : ¬{ re := ↑a, im := 1 } ≤ b
h1l : 1 < b
⊢ False

Tactic:
obtain ⟨x, y⟩ := b

Goal state after:
a : ℕ
a1 : 1 < a
n : ℕ
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
x y : ℤ
h1 : 1 ≤ { re := x, im := y }
hp : IsPell { re := x, im := y }
h : { re := x, im := y } ≤ pellZd a1 (n + 1)
ha : ¬{ re := ↑a, im := 1 } ≤ { re := x, im := y }
h1l : 1 < { re := x, im := y }
⊢ False
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n t : ℕ
h : yn a1 n * yn a1 n ∣ yn a1 t
nt : n ∣ t
n0l : 0 < n
k : ℕ
ke : t = n * k
xm : yn a1 t ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]
⊢ k * xn a1 n ^ (k - 1) * yn a1 n ≡ 0 [MOD yn a1 n * yn a1 n]

Tactic:
exact (xm.of_dvd <| by simp [_root_.pow_succ]).symm.trans h.modEq_zero_nat

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

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
a b : ℤ√↑d
ab : a ≤ b
ba : b ≤ a
⊢ (-(a - b)).Nonneg

Tactic:
by rwa [neg_sub]

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

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
x✝¹ x✝ : ℤ√↑d
ab : x✝¹ ≤ x✝
ba : x✝ ≤ x✝¹
⊢ (-(x✝¹ - x✝)).Nonneg

Tactic:
by rwa [neg_sub]

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

Goal state before:
pp: case neg
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : d < 0
⊢ a.re = re 0 ∧ a.im = im 0

Tactic:
suffices a.re * a.re = 0 by
      rw [eq_zero_of_mul_self_eq_zero this] at ha ⊢
      simpa only [true_and, or_self_right, re_zero, im_zero, eq_self_iff_true, zero_eq_mul,
        mul_zero, mul_eq_zero, h.ne, false_or, or_self_iff] using ha

Goal state after:
case neg
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : d < 0
⊢ a.re * a.re = 0
Module: Mathlib.NumberTheory.DirichletCharacter.Bounds

Goal state before:
pp: F : Type u_1
inst✝ : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : (ZMod n)ˣ
⊢ ‖χ ↑a‖ = 1

Tactic:
by
  refine (pow_eq_one_iff_of_nonneg (norm_nonneg _) (Nat.card_pos (α := (ZMod n)ˣ)).ne').mp ?_
  rw [← norm_pow, ← map_pow, ← Units.val_pow_eq_pow_val, pow_card_eq_one', Units.val_one, map_one,
    norm_one]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a k x y : ℕ
x✝ : ∃ (a1 : 1 < a), xn a1 k = x ∧ yn a1 k = y
a1 : 1 < a
hx : xn a1 k = x
hy : yn a1 k = y
k0 : k = 0
⊢ 0 ≤ yn a1 0 ∧
    (xn a1 0 = 1 ∧ yn a1 0 = 0 ∨
      ∃ u v s t b,
        xn a1 0 * xn a1 0 - (a * a - 1) * yn a1 0 * yn a1 0 = 1 ∧
          u * u - (a * a - 1) * v * v = 1 ∧
            s * s - (b * b - 1) * t * t = 1 ∧
              1 < b ∧
                b ≡ 1 [MOD 4 * yn a1 0] ∧
                  b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 0 * yn a1 0 ∣ v ∧ s ≡ xn a1 0 [MOD u] ∧ t ≡ 0 [MOD 4 * yn a1 0])

Tactic:
exact ⟨le_rfl, Or.inl ⟨rfl, rfl⟩⟩

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
x✝ : v ∈ {v | ∃ (h : v ∈ f.Dom), f.fn v h ::ₒ v ∈ S}
x : v ∈ f.Dom
hS : f.fn v x ::ₒ v ∈ S
⊢ ∃ (h : (f (v, (f.fn v x ::ₒ v) none).1).Dom), (f (v, (f.fn v x ::ₒ v) none).1).get h = (v, (f.fn v x ::ₒ v) none).2

Tactic:
exact ⟨x, rfl⟩

Goal state after:
Module: Mathlib.NumberTheory.DirichletCharacter.Orthogonality

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
n : ℕ
inst✝² : NeZero n
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsDomain R
a : ZMod n
⊢ ∑ χ, χ a = if a = 1 then ↑n.totient else 0

Tactic:
split_ifs with ha
  · simpa only [ha, map_one, Finset.sum_const, Finset.card_univ, nsmul_eq_mul, mul_one,
      ← Nat.card_eq_fintype_card]
      using congrArg Nat.cast <| card_eq_totient_of_hasEnoughRootsOfUnity R n
  · exact sum_characters_eq_zero R ha

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

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |↑⌊ξ⌋ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
hf : ξ = ↑⌊ξ⌋
⊢ 2 * ↑v - 1 < 1

Tactic:
refine (mul_lt_iff_lt_one_right hv₀).1 ((inv_lt_inv₀ hv₀ (mul_pos hv₁ hv₂)).1 (h.trans_le' ?_))

Goal state after:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |↑⌊ξ⌋ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
hf : ξ = ↑⌊ξ⌋
⊢ (↑v)⁻¹ ≤ |↑⌊ξ⌋ - ↑u / ↑v|
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: ⊢ factoredNumbers ∅ = {1}

Tactic:
ext m
  simp only [mem_factoredNumbers, Finset.notMem_empty, ← List.eq_nil_iff_forall_not_mem,
    primeFactorsList_eq_nil, and_or_left, not_and_self_iff, ne_and_eq_iff_right zero_ne_one,
    false_or, Set.mem_singleton_iff]

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: N : ℕ
s : Finset ℕ
h : N.primesBelow ⊆ s
⊢ (factoredNumbers s)ᶜ \ {0} ⊆ {n | N ≤ n}

Tactic:
intro n hn

Goal state after:
N : ℕ
s : Finset ℕ
h : N.primesBelow ⊆ s
n : ℕ
hn : n ∈ (factoredNumbers s)ᶜ \ {0}
⊢ n ∈ {n | N ≤ n}