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

Tactic:
Finset.sum_add_distrib,

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, ‖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‖ₑ + ↑δ
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: case falsum
α : Type u_1
A : Set ℕ
inst✝ : Finite α
n : ℕ
this : Fintype α
n✝ : ℕ
⊢ IsSemilinearSet {v | False}

Tactic:
exact .empty

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

Goal state before:
pp: case a.inl
ι : Type u_1
inst✝ : Finite ι
t : Finset ι
ih : ∀ t_1 ⊂ t, ∀ {s : Set (ι → ℕ)}, IsSlice s → ∀ (a : ι → ℕ), (∀ x ∈ s, ∀ i ∉ t_1, x i = a i) → IsSemilinearSet s
a : ι → ℕ
hs : IsSlice ∅
ht : ∀ x ∈ ∅, ∀ i ∉ t, x i = a i
⊢ IsSemilinearSet ∅

Tactic:
exact .empty

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable ((l : ℕ) × L.Functions l)
⊢ CG L M ↔ Countable M

Tactic:
rw [cg_def, Substructure.cg_iff_countable, topEquiv.toEquiv.countable_iff]

Goal state after:
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: case all
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst✝⁴ : L.Structure M
N : Type u_2
inst✝³ : L.Structure N
F : Type u_3
inst✝² : FunLike F M N
inst✝¹ : EmbeddingLike F M N
inst✝ : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsUniversal
ih : ∀ {xs : Fin (n✝ + 1) → M}, φ✝.Realize (⇑f ∘ v) (⇑f ∘ xs) → φ✝.Realize v xs
xs : Fin n✝ → M
⊢ (∀ (a : N), φ✝.Realize (⇑f ∘ v) (snoc (⇑f ∘ xs) a)) → ∀ (a : M), φ✝.Realize v (snoc xs a)

Tactic:
refine fun h a => ih ?_

Goal state after:
case all
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst✝⁴ : L.Structure M
N : Type u_2
inst✝³ : L.Structure N
F : Type u_3
inst✝² : FunLike F M N
inst✝¹ : EmbeddingLike F M N
inst✝ : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsUniversal
ih : ∀ {xs : Fin (n✝ + 1) → M}, φ✝.Realize (⇑f ∘ v) (⇑f ∘ xs) → φ✝.Realize v xs
xs : Fin n✝ → M
h : ∀ (a : N), φ✝.Realize (⇑f ∘ v) (snoc (⇑f ∘ xs) a)
a : M
⊢ φ✝.Realize (⇑f ∘ v) (⇑f ∘ snoc xs a)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case insert
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : AddMonoid.FG M
S : Set (Set M)
a✝¹ : Set M
s✝ : Set (Set M)
a✝ : a✝¹ ∉ s✝
hs✝ : s✝.Finite
ih : (∀ s ∈ s✝, IsSemilinearSet s) → IsSemilinearSet (⋂₀ s✝)
hS' : ∀ s ∈ insert a✝¹ s✝, IsSemilinearSet s
⊢ IsSemilinearSet (⋂₀ insert a✝¹ s✝)

Tactic:
mem_insert_iff,

Goal state after:
case insert
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : AddMonoid.FG M
S : Set (Set M)
a✝¹ : Set M
s✝ : Set (Set M)
a✝ : a✝¹ ∉ s✝
hs✝ : s✝.Finite
ih : (∀ s ∈ s✝, IsSemilinearSet s) → IsSemilinearSet (⋂₀ s✝)
hS' : ∀ (s : Set M), s = a✝¹ ∨ s ∈ s✝ → IsSemilinearSet s
⊢ IsSemilinearSet (⋂₀ insert a✝¹ s✝)
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: 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:
intro h
  rcases f with ⟨dom_f, cod_f, equiv_f⟩
  cases h_dom
  apply le_antisymm <;> (rw [le_def]; use le_rfl; ext ⟨x, hx⟩)
  · exact (h x hx).symm
  · exact h x hx

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

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
| ∑ x_1,
      (⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) x_1⌋.toNat • toRatVec ↑x_1 -
        (-⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) x_1⌋).toNat • toRatVec ↑x_1) ≤
    toRatVec x

Tactic:
enter [1, 2, _]
    rw [← Nat.cast_smul_eq_nsmul ℤ, ← Nat.cast_smul_eq_nsmul ℤ, ← sub_smul,
      Int.toNat_sub_toNat_neg, ← Int.cast_smul_eq_zsmul ℚ]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
x✝ : ↑hs.basisSet
| ↑⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) x✝⌋ • toRatVec ↑x✝
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
x✝ : ↑hs.basisSet
| (hs.floor x x✝).toNat • toRatVec ↑x✝ - (-hs.floor x x✝).toNat • toRatVec ↑x✝

Tactic:
rw [← Nat.cast_smul_eq_nsmul ℤ, ← Nat.cast_smul_eq_nsmul ℤ, ← sub_smul,
      Int.toNat_sub_toNat_neg]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
x✝ : ↑hs.basisSet
| hs.floor x x✝ • toRatVec ↑x✝
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
⊢ Substructure.map (lift L ι G f g Hg).toHom (⨆ i, (of L ι G f i).toHom.range) = ⨆ i, Substructure.map (g i).toHom ⊤

Tactic:
Substructure.map_iSup

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
⊢ ⨆ i, Substructure.map (lift L ι G f g Hg).toHom (of L ι G f i).toHom.range = ⨆ i, Substructure.map (g i).toHom ⊤
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mpr.refine_1
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
y : ι → ℕ
hy : y ∈ closure {↑i}
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
heq : hs.fract (x + ↑i + y) = hs.fract (hs.base + z)
⊢ hs.fract x = hs.base

Tactic:
hs.fract_add_of_mem_closure (closure_mono (singleton_subset_iff.2 i.2) hy),

Goal state after:
case mpr.refine_1
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
y : ι → ℕ
hy : y ∈ closure {↑i}
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
heq : hs.fract (x + ↑i) = hs.fract (hs.base + z)
⊢ hs.fract x = hs.base
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
⊢ ∃ y ∈ {f | ∃ b, (a, b) ∈ ↑f}, f ≤ y

Tactic:
obtain ⟨b, a_b⟩ := exists_across f a

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
b : β
a_b : ∀ p ∈ ↑f, cmp p.1 a = cmp p.2 b
⊢ ∃ y ∈ {f | ∃ b, (a, b) ∈ ↑f}, f ≤ y
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mpr.refine_1
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
y : ι → ℕ
hy : y ∈ closure {↑i}
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
heq : hs.fract x = hs.fract (hs.base + ↑i + y)
⊢ hs.fract x = hs.base

Tactic:
hs.fract_add_of_mem_closure (closure_mono (singleton_subset_iff.2 i.2) hy),

Goal state after:
case mpr.refine_1
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
y : ι → ℕ
hy : y ∈ closure {↑i}
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
heq : hs.fract x = hs.fract (hs.base + ↑i)
⊢ hs.fract x = hs.base
Module: Mathlib.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
φ ψ : L[[α]].Sentence
⊢ T.typesWith (φ ⊓ ψ) = T.typesWith φ ∩ T.typesWith ψ

Tactic:
ext p

Goal state after:
L : Language
T : L.Theory
α : Type w
φ ψ : L[[α]].Sentence
p : T.CompleteType α
⊢ p ∈ T.typesWith (φ ⊓ ψ) ↔ p ∈ T.typesWith φ ∩ T.typesWith ψ
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case inl
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 1 < sumInv (A' p' q')

Tactic:
A',

Goal state after:
case inl
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 1 < sumInv {1, p', q'}
Module: Mathlib.NumberTheory.AlmostPrime

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

Tactic:
rw [ArithmeticFunction.cardFactors_mul hm.1 hn.1]

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

Goal state before:
pp: p q r : ℕ+
H : 1 < sumInv {p, q, r}
S : List ℕ+ := {p, q, r}.sort fun a b ↦ a ≤ b
⊢ (∃ q_1 r_1, A' q_1 r_1 = {p, q, r}) ∨
    (∃ r_1, D' r_1 = {p, q, r}) ∨ E' 3 = {p, q, r} ∨ E' 4 = {p, q, r} ∨ E' 5 = {p, q, r}

Tactic:
have hS : S.SortedLE := (pairwise_sort _ _).sortedLE

Goal state after:
p q r : ℕ+
H : 1 < sumInv {p, q, r}
S : List ℕ+ := {p, q, r}.sort fun a b ↦ a ≤ b
hS : S.SortedLE
⊢ (∃ q_1 r_1, A' q_1 r_1 = {p, q, r}) ∨
    (∃ r_1, D' r_1 = {p, q, r}) ∨ E' 3 = {p, q, r} ∨ E' 4 = {p, q, r} ∨ E' 5 = {p, q, r}
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: n : ℕ
⊢ ∀ i ∈ (n + 1).divisors, 0 ≤ Λ i

Tactic:
exact fun _ _ => vonMangoldt_nonneg

Goal state after:
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 <;> simp (disch := grind [Finset.mem_antidiagonal]) [hm]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: k : ℕ
⊢ derivative (bernoulli (k + 1)) = (↑k + 1) * bernoulli k

Tactic:
simp_rw [bernoulli, derivative_sum, derivative_monomial, Nat.sub_sub, Nat.add_sub_add_right]
  -- LHS sum has an extra term, but the coefficient is zero:
  rw [range_add_one, sum_insert notMem_range_self, tsub_self, cast_zero, mul_zero,
    map_zero, zero_add, mul_sum]
  -- the rest of the sum is termwise equal:
  refine sum_congr rfl fun m _ => ?_
  conv_rhs => rw [← Nat.cast_one, ← Nat.cast_add, ← C_eq_natCast, C_mul_monomial, mul_comm]
  rw [mul_assoc, mul_assoc, ← Nat.cast_mul, ← Nat.cast_mul]
  congr 3
  rw [(choose_mul_succ_eq k m).symm]

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ n.primesBelow = filter Prime (Ico 0 n)

Tactic:
ext p

Goal state after:
n p : ℕ
⊢ p ∈ n.primesBelow ↔ p ∈ filter Prime (Ico 0 n)
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ n.primesLE = filter Prime (Icc 0 n)

Tactic:
ext p

Goal state after:
n p : ℕ
⊢ p ∈ n.primesLE ↔ p ∈ filter Prime (Icc 0 n)
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ n.primesBelow = filter Prime (Ioo 0 n)

Tactic:
ext p

Goal state after:
n p : ℕ
⊢ p ∈ n.primesBelow ↔ p ∈ filter Prime (Ioo 0 n)
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ n.primesLE = filter Prime (Ioc 0 n)

Tactic:
ext p

Goal state after:
n p : ℕ
⊢ p ∈ n.primesLE ↔ p ∈ filter Prime (Ioc 0 n)
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ n.primesBelow = filter Prime (Ico 1 n)

Tactic:
ext p

Goal state after:
n p : ℕ
⊢ p ∈ n.primesBelow ↔ p ∈ filter Prime (Ico 1 n)
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ n.primesLE = filter Prime (Icc 1 n)

Tactic:
ext p

Goal state after:
n p : ℕ
⊢ p ∈ n.primesLE ↔ p ∈ filter Prime (Icc 1 n)
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ n.primesBelow = filter Prime (Ioo 1 n)

Tactic:
ext p

Goal state after:
n p : ℕ
⊢ p ∈ n.primesBelow ↔ p ∈ filter Prime (Ioo 1 n)
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ n.primesLE = filter Prime (Ioc 1 n)

Tactic:
ext p

Goal state after:
n p : ℕ
⊢ p ∈ n.primesLE ↔ p ∈ filter Prime (Ioc 1 n)
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ n.primesBelow = filter Prime (Ico 2 n)

Tactic:
ext p

Goal state after:
n p : ℕ
⊢ p ∈ n.primesBelow ↔ p ∈ filter Prime (Ico 2 n)
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ n.primesLE = filter Prime (Icc 2 n)

Tactic:
ext p

Goal state after:
n p : ℕ
⊢ p ∈ n.primesLE ↔ p ∈ filter Prime (Icc 2 n)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ (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:
have hfact : ∀ m, (m ! : ℚ) ≠ 0 := fun m => mod_cast factorial_ne_zero m

Goal state after:
case succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 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
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)
⊢ ↑p ^ (2 * k - 2 * m) = P * ↑p

Tactic:
rw [show 2 * k - 2 * m = (2 * k - 2 * m - 1) + 1 by lia, pow_succ]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ n.lcmUpto.primeFactors = n.primesLE

Tactic:
ext p

Goal state after:
n p : ℕ
⊢ p ∈ n.lcmUpto.primeFactors ↔ p ∈ n.primesLE
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case e_s
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k : ℕ
x✝ : k ∈ Icc 1 N
⊢ {x_1 ∈ filter Nat.Prime (Ioc 0 ⌊x⌋₊) | x_1 ≤ ⌊x ^ (↑k)⁻¹⌋₊} = {p ∈ Ioc 0 ⌊x ^ (1 / ↑k)⌋₊ | Nat.Prime p}

Tactic:
ext p

Goal state after:
case e_s
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k : ℕ
x✝ : k ∈ Icc 1 N
p : ℕ
⊢ p ∈ {x_1 ∈ filter Nat.Prime (Ioc 0 ⌊x⌋₊) | x_1 ≤ ⌊x ^ (↑k)⁻¹⌋₊} ↔ p ∈ {p ∈ Ioc 0 ⌊x ^ (1 / ↑k)⌋₊ | Nat.Prime p}
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ ψ x = θ x + ∑ n ∈ Icc 2 N, θ (x ^ (1 / ↑n))

Tactic:
by
  rw [psi_eq_sum_theta' (by linarith) hN, ← add_sum_Ioc_eq_sum_Icc]
  · congr
    simp
  · apply le_trans _ hN
    rw [le_floor_iff' one_ne_zero, le_div_iff₀ (by positivity), cast_one, one_mul]
    gcongr

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ log (2 ^ n) ≤ log ((↑n + 1) * ↑n.lcmUpto)

Tactic:
exact log_le_log (by positivity) <| mod_cast two_pow_le_mul_lcmUpto n

Goal state after:
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)
⊢ ↑p ^ k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)

Tactic:
have h_unit : (h.isUnit NeZero.out).unit =
      (hζ.isUnit NeZero.out).unit ^ (p ^ i) := by ext; rfl

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

Goal state before:
pp: ⊢ (fun x ↦ ∫ (t : ℝ) in 2..x, 1 / log t ^ 2) =O[atTop] fun x ↦ 4 * x / log x ^ 2 + √x / log 2 ^ 2

Tactic:
apply IsBigO.of_bound'
    filter_upwards [eventually_ge_atTop 4] with x hx
    apply le_trans <| intervalIntegral.abs_integral_le_integral_abs (by linarith)
    rw [intervalIntegral.integral_congr (g := (fun t ↦ 1 / log t ^ 2))]
    · grw [integral_one_div_log_sq_le_explicit hx, norm_of_nonneg]
      positivity
    intro t ht
    simp

Goal state after:
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₂ : ↑(p ^ i) * ↑(p ^ k) ∣ ↑(p ^ i) * (aux g (p ^ (k + i)) - aux g (p ^ k))
⊢ ↑(p ^ i) ≠ 0

Tactic:
by simp [NeZero.ne p]

Goal state after:
Module: Mathlib.RingTheory.Localization.NormTrace

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Nontrivial R
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
this : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
⊢ (norm Rₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((norm R) a)

Tactic:
rw [Algebra.norm_eq_matrix_det (b.localizationLocalization Rₘ M Sₘ),
    Algebra.norm_eq_matrix_det b, RingHom.map_det, ← Algebra.map_leftMulMatrix_localization]

Goal state after:
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 ⋯
s : PadicSeq p := ⟨fun x ↦ ↑(f x), ⋯⟩
hs : ↑x = mk s
⊢ (toZModPow n) x = ↑(f n)

Tactic:
obtain ⟨e, he⟩ := Ideal.mem_span_singleton.mp (PadicInt.appr_spec n x)

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), ⋯⟩
hs : ↑x = mk s
e : ℤ_[p]
he : x - ↑(x.appr n) = ↑p ^ n * e
⊢ (toZModPow n) x = ↑(f n)
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: 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 }
bm : { re := x, im := y } * { re := { re := x, im := y }.re, im := -{ re := x, im := y }.im } = 1
y0l : 0 < { re := x - x, im := y - -y }
hn : { re := x, im := -y } ≤ { re := ↑a, im := -1 }
t :
  { re := x, im := y } * { re := x, im := -y } * { re := ↑a, im := 1 } ≤
    { re := x, im := y } * { re := ↑a, im := -1 } * { re := ↑a, im := 1 }
⊢ False

Tactic:
rw [bm, one_mul, mul_assoc, Eq.trans (mul_comm _ _) a1m, mul_one] at t

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 }
bm : { re := x, im := y } * { re := { re := x, im := y }.re, im := -{ re := x, im := y }.im } = 1
y0l : 0 < { re := x - x, im := y - -y }
hn : { re := x, im := -y } ≤ { re := ↑a, im := -1 }
t : { re := ↑a, im := 1 } ≤ { re := x, im := y }
⊢ False