mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsZeroOneMeasure μ
inst✝¹ : StandardBorelSpace α
inst✝ : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep : ∀ x ∈ univ, ∀ y ∈ univ, (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : ℕ → Set α := fun n ↦ if h : μ (A n) = 1 then A n else (A n)ᶜ
mBn : MeasurableSet (⋂ n, B n)
hBn : μ (⋂ n, B n) = 1
neBn : (⋂ n, B n).Nonempty
y : α
hy : y ∈ ⋂ n, B n
⊢ y ∈ univ

Tactic:
by trivial

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsZeroOneMeasure μ
inst✝¹ : StandardBorelSpace α
inst✝ : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep : ∀ x ∈ univ, ∀ y ∈ univ, (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : ℕ → Set α := fun n ↦ if h : μ (A n) = 1 then A n else (A n)ᶜ
mBn : MeasurableSet (⋂ n, B n)
hBn : μ (⋂ n, B n) = 1
neBn : (⋂ n, B n).Nonempty
y : α
hy : y ∈ ⋂ n, B n
⊢ neBn.some ∈ univ

Tactic:
by trivial

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_sigma_subadd : m.IsSigmaSubadditive
m_top : ∀ s ∉ C, m s = ∞
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hs_subset : s ⊆ ⋃ i, f i
⊢ m s = m (s ∩ ⋃ i, f i)

Tactic:
by rw [inter_eq_self_of_subset_left hs_subset]

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_sigma_subadd : m.IsSigmaSubadditive
m_top : ∀ s ∉ C, m s = ∞
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hs_subset : s ⊆ ⋃ i, f i
⊢ m (s ∩ ⋃ i, f i) = m (⋃ i, s ∩ f i)

Tactic:
rw [inter_iUnion]

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_top : ∀ s ∉ C, m s = ∞
hs : s ∈ C
t : Set α
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_subset : t ⊆ ⋃ i, f i
A : ℕ → Finset (Set α) := fun i ↦ hC.disjointOfDiff ⋯ ⋯
h_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃₀ ↑(A i)
h_m_eq : ∀ (i : ℕ), m (f i) = m (f i ∩ s) + ∑ u ∈ A i, m u
⊢ (OuterMeasure.ofFunction ⇑m ⋯) (t ∩ s) + (OuterMeasure.ofFunction ⇑m ⋯) (t \ s) ≤ ∑' (i : ℕ), m (f i)

Tactic:
h_m_eq

Goal state after:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_top : ∀ s ∉ C, m s = ∞
hs : s ∈ C
t : Set α
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_subset : t ⊆ ⋃ i, f i
A : ℕ → Finset (Set α) := fun i ↦ hC.disjointOfDiff ⋯ ⋯
h_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃₀ ↑(A i)
h_m_eq : ∀ (i : ℕ), m (f i) = m (f i ∩ s) + ∑ u ∈ A i, m u
⊢ (OuterMeasure.ofFunction ⇑m ⋯) (t ∩ s) + (OuterMeasure.ofFunction ⇑m ⋯) (t \ s) ≤
    ∑' (i : ℕ), (m (f i ∩ s) + ∑ u ∈ A i, m u)
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝³ : PseudoMetricSpace 𝓧
inst✝² : OpensMeasurableSpace 𝓧
inst✝¹ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
inst✝ : CompleteSpace 𝓧
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
hnonempty : Nonempty 𝓧
D : ℕ → 𝓧
hD : ∀ (x : 𝓧), ∀ r > 0, ∃ y, dist x (D y) < r
u : ℕ → ℝ
hu_anti : StrictAnti u
hu_pos : ∀ (n : ℕ), 0 < u n
hu : Tendsto u atTop (𝓝 0)
m : ℕ
p : 𝓧
⊢ p ∈ ⋃ i, ball (D i) (u m) ↔ p ∈ univ

Tactic:
exact ⟨fun a ↦ trivial, fun _ ↦ mem_iUnion.mpr <| hD p (u m) (hu_pos m)⟩

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

Goal state before:
pp: case inl
α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
h'α : IsEmpty α
⊢ ∃ m,
    (∀ (u v : α), u ≤ v → m (Ioc u v) = Function.rightLim f v - Function.rightLim f u) ∧
      m botSet = 0 ∧ ∀ (s : Set α), ‖m s‖ₑ ≤ hf.measureAux s

Tactic:
exact ⟨0, by simp⟩

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

Goal state before:
pp: α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
a : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
x : α
hx : ∀ (i : ℕ), u i < x ∧ x ≤ a
this : a ≤ x
⊢ x ∈ {a}

Tactic:
simp [le_antisymm this (hx 0).2]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation

Goal state before:
pp: X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
s : Set X
⊢ μ.semivariation univ = ↑(μ.semivariation univ).toNNReal

Tactic:
rw [ENNReal.coe_toNNReal semivariation_univ_lt_top.ne]

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

Goal state before:
pp: X : Type u_2
Y : Type u_3
E : Type u_4
F : Type u_5
mX : MeasurableSpace X
mY : MeasurableSpace Y
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
μ : VectorMeasure X E
ν : VectorMeasure Y F
inst✝ : IsFiniteMeasure μ.variation
s : Set (X × Y)
hs : MeasurableSet s
⊢ μ.Integrable fun x ↦ ν (Prod.mk x ⁻¹' s)

Tactic:
refine Integrable.of_bound (μ := μ.variation) ?_ ν.bound ?_
  · exact (stronglyMeasurable_vectorMeasure_prodMk_left hs).aestronglyMeasurable
  · exact Eventually.of_forall (fun x ↦ norm_apply_le_bound)

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

Goal state before:
pp: α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ s ∈ C, MeasurableSet s
M : MeasurableSpace α := generateFrom C
Mle : M ≤ hα
μ' : Measure α := μ.trim Mle
hμ' : μ' = μ.trim Mle
m' : VectorMeasure α E
m'C : ∀ s ∈ C, m' s = m s
hm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ μ' s
m'_le : m'.variation ≤ μ'
this✝ : MeasurableSpace α := hα
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : Pairwise (Function.onFun Disjoint f)
this :
  ∫ᵛ (x : α), μ[fun x ↦ ∑' (d : ℕ), (f d).indicator 1 x | M] x ∂•m' =
    ∫ᵛ (x : α), ∑' (d : ℕ), μ[(f d).indicator 1 | M] x ∂•m'
⊢ HasSum (fun i ↦ ∫ᵛ (x : α), μ[(f i).indicator 1 | M] x ∂•m') (∫ᵛ (x : α), ∑' (d : ℕ), μ[(f d).indicator 1 | M] x ∂•m')

Tactic:
have I : ∑' (i : ℕ), ∫⁻ (a : α), ‖μ[(f i).indicator (1 : α → ℝ) | M] a‖ₑ ∂μ < ∞ := by
        have A i : ∫⁻ a, ‖μ[(f i).indicator (1 : α → ℝ) | M] a‖ₑ ∂μ = μ (f i) :=
          lintegral_enorm_condExp_indicator Mle (f_meas i)
        simp_rw [A, ← measure_iUnion hf f_meas]
        exact measure_lt_top _ _

Goal state after:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ s ∈ C, MeasurableSet s
M : MeasurableSpace α := generateFrom C
Mle : M ≤ hα
μ' : Measure α := μ.trim Mle
hμ' : μ' = μ.trim Mle
m' : VectorMeasure α E
m'C : ∀ s ∈ C, m' s = m s
hm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ μ' s
m'_le : m'.variation ≤ μ'
this✝ : MeasurableSpace α := hα
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : Pairwise (Function.onFun Disjoint f)
this :
  ∫ᵛ (x : α), μ[fun x ↦ ∑' (d : ℕ), (f d).indicator 1 x | M] x ∂•m' =
    ∫ᵛ (x : α), ∑' (d : ℕ), μ[(f d).indicator 1 | M] x ∂•m'
I : ∑' (i : ℕ), ∫⁻ (a : α), ‖μ[(f i).indicator 1 | M] a‖ₑ ∂μ < ∞
⊢ HasSum (fun i ↦ ∫ᵛ (x : α), μ[(f i).indicator 1 | M] x ∂•m') (∫ᵛ (x : α), ∑' (d : ℕ), μ[(f d).indicator 1 | M] x ∂•m')
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: case insert
ι : Type u_1
X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f : X → E
B : E →L[ℝ] F →L[ℝ] G
μ : ι → VectorMeasure X F
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, (μ i).Integrable f) → ∫ᵛ (x : X), f x ∂[B; ∑ i ∈ s, μ i] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]
hf : (μ a).Integrable f ∧ ∀ a ∈ s, (μ a).Integrable f
⊢ ∫ᵛ (x : X), f x ∂[B; μ a] + ∫ᵛ (x : X), f x ∂[B; ∑ i ∈ s, μ i] =
    ∫ᵛ (x : X), f x ∂[B; μ a] + ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]

Tactic:
ih hf.2

Goal state after:
case insert
ι : Type u_1
X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f : X → E
B : E →L[ℝ] F →L[ℝ] G
μ : ι → VectorMeasure X F
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, (μ i).Integrable f) → ∫ᵛ (x : X), f x ∂[B; ∑ i ∈ s, μ i] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]
hf : (μ a).Integrable f ∧ ∀ a ∈ s, (μ a).Integrable f
⊢ ∫ᵛ (x : X), f x ∂[B; μ a] + ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i] =
    ∫ᵛ (x : X), f x ∂[B; μ a] + ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: case mp
s : Set ℕ
⊢ IsSemilinearSet s → ∃ k, ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s

Tactic:
intro hs

Goal state after:
case mp
s : Set ℕ
hs : IsSemilinearSet s
⊢ ∃ k, ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hf : μ.Integrable f
hg : μ.Integrable g
⊢ edist ∫ᵛ (a : X), f a ∂[B; μ] ∫ᵛ (a : X), g a ∂[B; μ] ≤ ‖B‖ₑ * ∫⁻ (a : X), edist (f a) (g a) ∂μ.variation

Tactic:
rw [edist_dist]

Goal state after:
X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hf : μ.Integrable f
hg : μ.Integrable g
⊢ ENNReal.ofReal (dist ∫ᵛ (a : X), f a ∂[B; μ] ∫ᵛ (a : X), g a ∂[B; μ]) ≤
    ‖B‖ₑ * ∫⁻ (a : X), edist (f a) (g a) ∂μ.variation
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
ι : Type u_7
hf : μ.Integrable f
l : Filter ι
s : ι → Set X
hs : Tendsto (⇑μ.variation ∘ s) l (𝓝 0)
⊢ Tendsto (fun x ↦ ‖∫ᵛ (x : X) in s x, f x ∂[B; μ]‖) l (𝓝 0)

Tactic:
simp_rw [← coe_nnnorm, ← NNReal.coe_zero, NNReal.tendsto_coe, ← ENNReal.tendsto_coe,
    ENNReal.coe_zero]

Goal state after:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
ι : Type u_7
hf : μ.Integrable f
l : Filter ι
s : ι → Set X
hs : Tendsto (⇑μ.variation ∘ s) l (𝓝 0)
⊢ Tendsto (fun a ↦ ↑‖∫ᵛ (x : X) in s a, f x ∂[B; μ]‖₊) l (𝓝 0)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: case neg
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : {x | x ∈ s ∧ x < k}.Finite
h₂ : {x | x ∈ s ∧ k ≤ x ∧ x < k + p}.Finite
x : ℕ
hx : x ∈ s
hx' : ¬x < k
⊢ x ∈ s ∧ x < k ∨ ∃ x_1, ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ a, x_1 + a * p = x

Tactic:
rw [not_lt] at hx'

Goal state after:
case neg
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : {x | x ∈ s ∧ x < k}.Finite
h₂ : {x | x ∈ s ∧ k ≤ x ∧ x < k + p}.Finite
x : ℕ
hx : x ∈ s
hx' : k ≤ x
⊢ x ∈ s ∧ x < k ∨ ∃ x_1, ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ a, x_1 + a * p = x
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: 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
x : M
hx : x ∈ s
⊢ ∀ {a b : M}, a ∈ {y | x + y ∈ s} → b ∈ {y | x + y ∈ s} → a + b ∈ {y | x + y ∈ s}

Tactic:
intro a b ha hb

Goal state after:
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
x : M
hx : x ∈ s
a b : M
ha : a ∈ {y | x + y ∈ s}
hb : b ∈ {y | x + y ∈ s}
⊢ a + b ∈ {y | x + y ∈ s}
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: case func.inl.one
α : Type u_1
A : Set ℕ
inst✝ : Fintype α
ts : Fin 0 → presburger[[↑A]].Term α
k : Fin 0 → ℕ
u : Fin 0 → α → ℕ
ih : ∀ (a : Fin 0) (v : α → ℕ), Term.realize v (ts a) = k a + u a ⬝ᵥ v
⊢ ∃ k u, ∀ (v : α → ℕ), (Structure.funMap (Sum.inl presburgerFunc.one) fun i ↦ Term.realize v (ts i)) = k + u ⬝ᵥ v

Tactic:
refine ⟨1, 0, fun v => ?_⟩

Goal state after:
case func.inl.one
α : Type u_1
A : Set ℕ
inst✝ : Fintype α
ts : Fin 0 → presburger[[↑A]].Term α
k : Fin 0 → ℕ
u : Fin 0 → α → ℕ
ih : ∀ (a : Fin 0) (v : α → ℕ), Term.realize v (ts a) = k a + u a ⬝ᵥ v
v : α → ℕ
⊢ (Structure.funMap (Sum.inl presburgerFunc.one) fun i ↦ Term.realize v (ts i)) = 1 + 0 ⬝ᵥ v
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: case func.inr
α : Type u_1
A : Set ℕ
inst✝ : Fintype α
l : ℕ
ts : Fin l → presburger[[↑A]].Term α
ih : ∀ (a : Fin l), ∃ k u, ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v
f : (constantsOn ↑A).Functions l
⊢ ∃ k u, ∀ (v : α → ℕ), (Structure.funMap (Sum.inr f) fun i ↦ Term.realize v (ts i)) = k + u ⬝ᵥ v

Tactic:
| inr f =>

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
hs : (Substructure.map f.toHom s).CG
⊢ s.CG

Tactic:
rcases hs with ⟨t, h1, h2⟩
  rw [cg_def]
  refine ⟨f ⁻¹' t, h1.preimage f.injective, ?_⟩
  have hf : Function.Injective f.toHom := f.injective
  refine map_injective_of_injective hf ?_
  rw [← h2, map_closure, Embedding.coe_toHom, image_preimage_eq_of_subset]
  intro x hx
  have h' := subset_closure (L := L) hx
  rw [h2] at h'
  exact Hom.map_le_range h'

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

Goal state before:
pp: case a.inr
ι : 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
s : Set (ι → ℕ)
hs : IsSlice s
a : ι → ℕ
ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i
hs' : s.Nonempty
x : ι → ℕ
hx : x ∈ s
hx' : IsSemilinearSet {y | y ∈ s ∧ x ≤ y}
i : ι
hi : i ∈ t
j : ℕ
hj : j ∈ Finset.range (x i)
⊢ IsSemilinearSet {y | y ∈ s ∧ y i = j}

Tactic:
simp only [Finset.mem_range] at hj

Goal state after:
case a.inr
ι : 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
s : Set (ι → ℕ)
hs : IsSlice s
a : ι → ℕ
ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i
hs' : s.Nonempty
x : ι → ℕ
hx : x ∈ s
hx' : IsSemilinearSet {y | y ∈ s ∧ x ≤ y}
i : ι
hi : i ∈ t
j : ℕ
hj : j < x i
⊢ IsSemilinearSet {y | y ∈ s ∧ y i = j}
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 : f ≤ g
x : ↥f.dom
⊢ g.toEquiv ((inclusion ⋯) x) = (inclusion ⋯) (f.toEquiv x)

Tactic:
apply (subtype _).injective

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h : f ≤ g
x : ↥f.dom
⊢ g.cod.subtype (g.toEquiv ((inclusion ⋯) x)) = g.cod.subtype ((inclusion ⋯) (f.toEquiv x))
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mpr
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx₁ : hs.fract x = hs.base
hx₂ : ∀ (i : ↑hs.basisSet), 0 ≤ hs.floor x i ∧ (↑i ∉ hs.periods → hs.floor x i = 0)
⊢ ∃ y ∈ closure hs.periods, hs.base + y = x

Tactic:
refine ⟨∑ i : hs.basisSet with i.1 ∈ hs.periods, (hs.floor x i).toNat • i.1,
      sum_mem fun i hi => nsmul_mem (mem_closure_of_mem (Finset.mem_filter.1 hi).2) _, ?_⟩

Goal state after:
case mpr
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx₁ : hs.fract x = hs.base
hx₂ : ∀ (i : ↑hs.basisSet), 0 ≤ hs.floor x i ∧ (↑i ∉ hs.periods → hs.floor x i = 0)
⊢ hs.base + ∑ i with ↑i ∈ hs.periods, (hs.floor x i).toNat • ↑i = x
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mp
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ hs.fract x ≠ hs.base →
    ∃ i ∈ hs.fundamentalDomain \ {hs.base}, ∃ y ∈ closure hs.basisSet, ∃ y' ∈ closure hs.basisSet, x + y' = i + y

Tactic:
intro hx
      refine ⟨hs.fract x, ⟨hs.fract_mem_fundamentalDomain x, hx⟩, ∑ i, (hs.floor x i).toNat • i.1,
        ?_, ∑ i, (-hs.floor x i).toNat • i.1, ?_, ?_⟩
      · exact sum_mem fun i _ => nsmul_mem (mem_closure_of_mem i.2) _
      · exact sum_mem fun i _ => nsmul_mem (mem_closure_of_mem i.2) _
      · exact hs.add_floor_neg_toNat_sum_eq x

Goal state after:
Module: Mathlib.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
M : ModelType ↑p
φ : L[[α]].Sentence
⊢ (φ ∈ T.typeOf fun a ↦ ↑(L.con a)) ↔ φ ∈ p

Tactic:
simp only [CompleteType.mem_typeOf]

Goal state after:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
M : ModelType ↑p
φ : L[[α]].Sentence
⊢ ((Formula.equivSentence.symm φ).Realize fun a ↦ ↑(L.con a)) ↔ φ ∈ p
Module: Mathlib.NumberTheory.AlmostPrime

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

Tactic:
by
  refine ⟨mul_ne_zero hm.1 hn.1, ?_⟩
  rw [ArithmeticFunction.cardFactors_mul hm.1 hn.1]
  exact add_le_add hm.2 hn.2

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

Goal state before:
pp: case refine_3
n a b : ℕ
ha' : 1 < a
hb' : 1 < b
hab : a.Coprime b
ha : ∑ a ∈ a.divisors with IsPrimePow a, Real.log ↑a.minFac = Real.log ↑a
hb : ∑ a ∈ b.divisors with IsPrimePow a, Real.log ↑a.minFac = Real.log ↑b
⊢ ∑ x ∈ a.divisors with IsPrimePow x, Real.log ↑x.minFac + ∑ x ∈ b.divisors with IsPrimePow x, Real.log ↑x.minFac =
    Real.log ↑(a * b)

Tactic:
ha,

Goal state after:
case refine_3
n a b : ℕ
ha' : 1 < a
hb' : 1 < b
hab : a.Coprime b
ha : ∑ a ∈ a.divisors with IsPrimePow a, Real.log ↑a.minFac = Real.log ↑a
hb : ∑ a ∈ b.divisors with IsPrimePow a, Real.log ↑a.minFac = Real.log ↑b
⊢ Real.log ↑a + ∑ x ∈ b.divisors with IsPrimePow x, Real.log ↑x.minFac = Real.log ↑(a * b)
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝ : CompleteSpace G
hf : μ.Integrable f
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖B.flip y‖₊ * ‖x‖₊
s : Set X
hs : MeasurableSet s
ε : NNReal
εpos : 0 < ε
δ : NNReal := ε / 3
δpos : 0 < δ
g : X →ₛ E
hg : eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ
gmem : MemLp (⇑g) 1 μ.variation
I1 : ∫⁻ (a : X) in s, ‖f a‖ₑ ∂(μ.transpose B).variation ≤ ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation + ↑δ
I2 :
  ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation =
    ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i})
ρ : ℝ≥0∞
ρpos : ρ > 0
hρ : ∑ i ∈ g.range, ‖i‖ₑ * ρ ≤ ↑δ
P : E → Finset (Set X)
Pg : ∀ (i : E), ∀ t ∈ P i, t ⊆ ⇑g ⁻¹' {i}
Pdisj : ∀ (i : E), (↑(P i)).PairwiseDisjoint id
Pmeas : ∀ (i : E), ∀ t ∈ P i, MeasurableSet t
hP :
  ∀ (i : E),
    ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
      ‖i‖ₑ * (∑ p ∈ P i, ‖((μ.transpose B).restrict s) p‖ₑ + ρ)
I3 :
  ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
    ∑ i ∈ g.range.sigma P, ‖i.fst‖ₑ * ‖((μ.transpose B).restrict s) i.snd‖ₑ + ↑δ
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]‖ₑ + ↑δ
I5 : ∑ i ∈ g.range.sigma P, ‖∫ᵛ (x : X) in i.snd, f x ∂[B; μ.restrict s]‖ₑ ≤ (μ.withDensity f B).variation s
⊢ (μ.withDensity f B).variation s + 3 * ↑δ ≤ (μ.withDensity f B).variation s + ↑ε

Tactic:
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 neg.inr.inl
n : ℕ
h0 : ¬2 * n = 0
h1 : ¬2 * n = 1
h2 : ¬2 * n = 2
h4 : ¬2 * n = 4
hn✝ : Even (2 * n)
hn : Odd n
⊢ (∃ p m, Nat.Prime p ∧ Odd p ∧ n = p ^ m) ↔ ∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * n = 2 * x ^ x_1

pp: case neg.inr.inl
n : ℕ
h0 : ¬2 * n = 0
h1 : ¬2 * n = 1
h2 : ¬2 * n = 2
h4 : ¬2 * n = 4
hn✝ : Even (2 * n)
hn : Odd n
⊢ ¬∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * n = x ^ x_1

Tactic:
· congr! with p m
      rw [Nat.mul_left_cancel_iff zero_lt_two, and_iff_right_of_imp]
      rintro rfl
      contrapose! h2
      cases Nat.lt_one_iff.mp h2
      rw [pow_zero, mul_one]

Goal state after:
case neg.inr.inl
n : ℕ
h0 : ¬2 * n = 0
h1 : ¬2 * n = 1
h2 : ¬2 * n = 2
h4 : ¬2 * n = 4
hn✝ : Even (2 * n)
hn : Odd n
⊢ ¬∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * n = x ^ x_1
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n p : ℕ
f : ℕ → ℚ := fun i ↦ bernoulli i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
f' : ℕ → ℚ := fun i ↦ bernoulli' i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
hle : 1 ≤ n + 1
hne : ↑p + 1 + 1 ≠ 0
h1 : ∀ (r : ℚ), r * (↑p + 1 + 1) * ↑n ^ p.succ / (↑p + 1 + 1) = r * ↑n ^ p.succ
h2 : f 1 + ↑n ^ p.succ = 1 / 2 * ↑n ^ p.succ
this :
  ∑ i ∈ range p, bernoulli (i + 2) * ↑((p + 2).choose (i + 2)) * ↑n ^ (p - i) / ↑(p + 2) =
    ∑ i ∈ range p, bernoulli' (i + 2) * ↑((p + 2).choose (i + 2)) * ↑n ^ (p - i) / ↑(p + 2)
⊢ ∑ i ∈ range p.succ.succ, f i + ↑n ^ p.succ = ∑ i ∈ range p, f i.succ.succ + f 1 + f 0 + ↑n ^ p.succ

Tactic:
by
      simp_rw [sum_range_succ']

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_1
n q : ℕ
hq : q ∈ (filter Nat.Prime (Icc 1 n)).biUnion fun p ↦ image (fun x ↦ p ^ x) (Icc 1 (Nat.log p n))
⊢ q ∈ Icc 1 n

pp: case refine_2
n x : ℕ
hx : x ∈ Icc 1 n
⊢ (x ∉ (filter Nat.Prime (Icc 1 n)).biUnion fun p ↦ image (fun x ↦ p ^ x) (Icc 1 (Nat.log p n))) → Λ x = 0

Tactic:
· simp only [mem_biUnion, mem_filter, mem_Icc, mem_image] at hq ⊢
      obtain ⟨p, _, k, ⟨_, hk⟩, rfl⟩ := hq
      exact ⟨by grind, pow_le_of_le_log (by linarith) hk⟩

Goal state after:
case refine_2
n x : ℕ
hx : x ∈ Icc 1 n
⊢ (x ∉ (filter Nat.Prime (Icc 1 n)).biUnion fun p ↦ image (fun x ↦ p ^ x) (Icc 1 (Nat.log p n))) → Λ x = 0
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n p : ℕ
hp : p ∈ n.primesLE
k : ℕ
hk : k ∈ Icc 1 (Nat.log p n)
⊢ Λ (p ^ k) = log ↑p

Tactic:
vonMangoldt_apply_pow (by grind),

Goal state after:
n p : ℕ
hp : p ∈ n.primesLE
k : ℕ
hk : k ∈ Icc 1 (Nat.log p n)
⊢ Λ p = log ↑p