mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: case neg
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
s : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
C : ℝ
h : IsFiniteMeasure (μ.variation.restrict s)
hC : ∀ᵐ (x : X) ∂μ.variation.restrict s, ‖f x‖ ≤ C
hs : ¬MeasurableSet s
h's : ¬μ.variation s = 0
this✝ : (ae (μ.variation.restrict s)).NeBot
x : X
hx : ‖f x‖ ≤ C
this : 0 ≤ C
⊢ 0 ≤ C * ‖B‖ * μ.variation.real s

Tactic:
positivity

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

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : SignedMeasure X
i j : Set X
him : MeasurableSet i
hi : 0 ≤[i] μ
hjm : MeasurableSet j
⊢ (μ.toMeasureOfZeroLE i him hi) j = ‖μ (i ∩ j)‖ₑ

Tactic:
by
  have : 0 ≤ μ (i ∩ j) :=
    μ.nonneg_of_zero_le_restrict (μ.zero_le_restrict_subset ‹_› Set.inter_subset_left ‹_›)
  rw [Real.enorm_of_nonneg this, μ.toMeasureOfZeroLE_apply hi him hjm, ENNReal.ofReal_eq_coe_nnreal]

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

Goal state before:
pp: case neg
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
s : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
C : ℝ
h : IsFiniteMeasure (μ.variation.restrict s)
hC : ∀ x ∈ s, ‖f x‖ ≤ C
x : X
hx : x ∈ s
hs : ¬MeasurableSet s
this : 0 ≤ C
⊢ 0 ≤ C * ‖B‖ * μ.variation.real s

Tactic:
positivity

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

Goal state before:
pp: case neg
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
s : ℕ → Set X
hm : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
hfi : μ.IntegrableOn f (⋃ i, s i)
hG : ¬CompleteSpace G
⊢ HasSum (fun n ↦ ∫ᵛ (x : X) in s n, f x ∂[B; μ]) ∫ᵛ (x : X) in ⋃ n, s n, f x ∂[B; μ]

pp: case pos
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
s : ℕ → Set X
hm : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
hfi : μ.IntegrableOn f (⋃ i, s i)
hG : CompleteSpace G
⊢ HasSum (fun n ↦ ∫ᵛ (x : X) in s n, f x ∂[B; μ]) ∫ᵛ (x : X) in ⋃ n, s n, f x ∂[B; μ]

Tactic:
· simp [integral_of_not_completeSpace hG]

Goal state after:
case pos
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
s : ℕ → Set X
hm : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
hfi : μ.IntegrableOn f (⋃ i, s i)
hG : CompleteSpace G
⊢ HasSum (fun n ↦ ∫ᵛ (x : X) in s n, f x ∂[B; μ]) ∫ᵛ (x : X) in ⋃ n, s n, f x ∂[B; μ]
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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
s : Set X
⊢ 0 ≤ ‖B‖ * ‖μ s‖

Tactic:
positivity

Goal state after:
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
s : ℕ → Set X
hm : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
hfi : μ.IntegrableOn f (⋃ i, s i)
hG : CompleteSpace G
I : ∑' (i : ℕ), ‖B‖ₑ * ∫⁻ (x : X) in s i, ‖f x‖ₑ ∂μ.variation < ∞
this : Summable fun n ↦ ∫ᵛ (x : X) in s n, f x ∂[B; μ]
⊢ (fun x ↦ 0) ≤ fun x ↦ ‖∫ᵛ (x : X) in ⋃ n, s n, f x ∂[B; μ] - ∑ i ∈ Finset.range x, ∫ᵛ (x : X) in s i, f x ∂[B; μ]‖ₑ

Tactic:
positivity

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

Goal state before:
pp: α : Type u_1
M : Type u_2
v : α → M
inst✝ : AddCommMonoidWithOne M
β : Type u_3
s : Finset β
f : β → presburger.Term α
| ∑ i ∈ s, Term.realize v (f i)

Tactic:
rw [← s.toList_toFinset, List.sum_toFinset _ s.nodup_toList]

Goal state after:
α : Type u_1
M : Type u_2
v : α → M
inst✝ : AddCommMonoidWithOne M
β : Type u_3
s : Finset β
f : β → presburger.Term α
| (List.map (fun i ↦ Term.realize v (f i)) s.toList).sum
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: case insert
M : Type u_1
inst✝ : AddCommMonoid 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:
simp_rw [mem_insert_iff, forall_eq_or_imp] at hS'
    simpa using hS'.1.union (ih hS'.2)

Goal state after:
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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
inst✝ : Nontrivial E
C : ℝ≥0
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = C * ‖x‖₊ * ‖y‖₊
hC : C ≠ 0
s : Set X
hs : MeasurableSet s
x : E
hx : x ≠ 0
this : C * ‖μ s‖₊ ≤ ‖B.flip (μ s)‖₊
⊢ 0 < C

Tactic:
positivity

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

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

Tactic:
simp_rw [mem_insert_iff, forall_eq_or_imp] at hS'
    simpa using hS'.1.union (ih hS'.2)

Goal state after:
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 < δ
hB : ‖B‖₊ ≠ 0
⊢ ‖B‖₊⁻¹ * δ > 0

Tactic:
positivity

Goal state after:
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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
f : X → E
c : ℝ
hG : CompleteSpace G
this : (c • μ).variation = ‖c‖₊ • μ.variation
⊢ DominatedFinMeasAdditive μ.variation (c • ⇑(μ.transpose B)) (‖c‖ * ‖B‖)

Tactic:
exact (dominatedFinMeasAdditive_cbmApplyMeasure μ B).smul c

Goal state after:
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 < δ
hB : ‖B‖₊ ≠ 0
⊢ 0 ≤ δ

Tactic:
positivity

Goal state after:
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})
⊢ ∑ i ∈ g.range, ‖i‖ₑ * (↑δ * (∑ i ∈ g.range, ‖i‖ₑ)⁻¹) ≤ ↑δ

Tactic:
← Finset.sum_mul,

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})
⊢ (∑ i ∈ g.range, ‖i‖ₑ) * (↑δ * (∑ i ∈ g.range, ‖i‖ₑ)⁻¹) ≤ ↑δ
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: case neg
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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
le_ae : ∀ᵐ (a : X) ∂μ.variation, 0 ≤ ‖f a‖
h : ¬AEStronglyMeasurable f μ.variation
⊢ 0 ≤ ‖B‖ * ∫ (a : X), ‖f a‖ ∂μ.variation

Tactic:
positivity

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

Goal state before:
pp: case refine_3
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✝
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F✝
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F✝ →L[ℝ] G
ι : Type u_7
f : X → E
hfi : AEStronglyMeasurable f μ.variation
F : ι → X → E
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, μ.Integrable (F i)
hF : Tendsto (fun i ↦ ∫⁻ (x : X), ‖F i x - f x‖ₑ ∂μ.variation) l (𝓝 0)
s : Set X
⊢ Tendsto (fun i ↦ ∫⁻ (x : X), ‖F i x - f x‖ₑ ∂(μ.restrict s).variation) l (𝓝 0)

Tactic:
simp_rw [← eLpNorm_one_eq_lintegral_enorm] at hF ⊢
    apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hF (fun _ ↦ zero_le)
      (fun i ↦ ?_)
    apply eLpNorm_mono_measure
    grw [variation_restrict_le]
    apply Measure.restrict_le_self

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: A : Set ℕ
hmul : A.Definable presburger {v | v 0 = v 1 * v 2}
k p : ℕ
hp : p > 0
h : ∃ x, x * x = max k p * max k p + p
⊢ False

Tactic:
rcases h with ⟨x, h₁⟩

Goal state after:
A : Set ℕ
hmul : A.Definable presburger {v | v 0 = v 1 * v 2}
k p : ℕ
hp : p > 0
x : ℕ
h₁ : x * x = max k p * max k p + p
⊢ False
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: case mp.inr
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
S : Set M
Scount : S.Countable
hS : (closure L).toFun S = N
h : (↑N).Nonempty
f : ℕ → M
h' : S ∪ {h.some} = range f
⊢ ↑N = ∅ ∨ ∃ s, (closure L).toFun (range s) = N

Tactic:
refine Or.intro_right _ ⟨f, ?_⟩

Goal state after:
case mp.inr
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
S : Set M
Scount : S.Countable
hS : (closure L).toFun S = N
h : (↑N).Nonempty
f : ℕ → M
h' : S ∪ {h.some} = range f
⊢ (closure L).toFun (range f) = N
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: L : Language
α : Type u'
n : ℕ
P : {m : ℕ} → L.BoundedFormula α m → Prop
φ✝ : L.BoundedFormula α n
hqf : ∀ {m : ℕ} {ψ : L.BoundedFormula α m}, ψ.IsQF → P ψ
hall : ∀ {m : ℕ} {ψ : L.BoundedFormula α (m + 1)}, P ψ → P (∀' ψ)
hex : ∀ {m : ℕ} {φ : L.BoundedFormula α (m + 1)}, P φ → P (∃' φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : L.BoundedFormula α m}, φ₁ ⇔[∅] φ₂ → (P φ₁ ↔ P φ₂)
m : ℕ
φ : L.BoundedFormula α m
hφ : φ.IsPrenex
⊢ P φ

Tactic:
induction hφ with
  | of_isQF hφ => exact hqf hφ
  | all _ hφ => exact hall hφ
  | ex _ hφ => exact hex hφ

Goal state after:
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: 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
hU : φ.IsUniversal
f : F
v : α → M
xs : Fin n → M
⊢ φ.Realize (⇑f ∘ v) (⇑f ∘ xs) → φ.Realize v xs

Tactic:
induction hU with
  | of_isQF hQF => simp [hQF.realize_embedding]
  | all _ ih =>
    simp only [realize_all, Nat.succ_eq_add_one]
    refine fun h a => ih ?_
    rw [Fin.comp_snoc]
    exact h (f a)

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

Goal state before:
pp: M : Type u_1
ι : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Finite ι
F : Type u_5
inst✝¹ : FunLike F (ι → ℕ) M
inst✝ : AddMonoidHomClass F (ι → ℕ) M
f : F
a : M
n : ℕ
g : (Fin n → ℕ) →+ M
⊢ IsSemilinearSet {x | f x ∈ a +ᵥ range ⇑g}

Tactic:
simp only [mem_vadd_set, mem_range, vadd_eq_add, exists_exists_eq_and]

Goal state after:
M : Type u_1
ι : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Finite ι
F : Type u_5
inst✝¹ : FunLike F (ι → ℕ) M
inst✝ : AddMonoidHomClass F (ι → ℕ) M
f : F
a : M
n : ℕ
g : (Fin n → ℕ) →+ M
⊢ IsSemilinearSet {x | ∃ a_1, a + g a_1 = f x}
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 : M ≃ₚ[L] N
h : f.dom = ⊤
⊢ (PartialEquiv.toEmbeddingOfEqTop h).toPartialEquiv = f

Tactic:
by
  rcases f with ⟨_, _, _⟩
  cases h
  apply PartialEquiv.ext
  · intro _ _
    rfl
  · rfl

Goal state after:
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case succ
L : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
inst✝¹ : IsEmpty L.Constants
inst✝ : IsEmpty (L.Relations 0)
n✝ : ℕ
r : L.Relations (n✝ + 1)
x : Fin (n✝ + 1) → ↥⊥
⊢ RelMap r ((fun a ↦ isEmptyElim a) ∘ x) ↔ RelMap r x

Tactic:
exact isEmptyElim (x 0)

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 : ι → ℕ
hx : x ∈ hs.fundamentalDomain
| toRatVec hs.base + ∑ i, Int.fract ((hs.basis.repr (toRatVec x - toRatVec hs.base)) i) • toRatVec ↑i

Tactic:
enter [2, 2, i]

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

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain
| toRatVec hs.base + ∑ i, Int.fract ((hs.basis.repr (toRatVec x - toRatVec hs.base)) i) • toRatVec ↑i

Tactic:
enter [2, 2, i]
    rw [Int.fract_eq_self.2 (hx i), ← hs.basis_apply]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain
i : ↑hs.basisSet
| (hs.basis.repr (toRatVec x - toRatVec hs.base)) i • hs.basis i
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
pp: case refine_1
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
φ : L[[α]].Sentence
x : φ ∈ (L.lhomWithConstants α).onTheory T
⊢ φ ∈ {φ | T.typesWith φ ∈ F}

Tactic:
exact F.mem_of_superset Filter.univ_mem (fun p _ ↦ p.subset x)

Goal state after:
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
⊢ 0 < 3

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : (↑↑p)⁻¹ ≤ 3⁻¹
⊢ 0 < 3

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : (↑↑p)⁻¹ ≤ 3⁻¹
hq : (↑↑q)⁻¹ ≤ 3⁻¹
⊢ 0 < 3

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: q r : ℕ+
hqr : q ≤ r
H : 4 ≤ q
h4r : 4 ≤ r
⊢ 0 < 4

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: q r : ℕ+
hqr : q ≤ r
H : 4 ≤ q
h4r : 4 ≤ r
hq : (↑↑q)⁻¹ ≤ 4⁻¹
⊢ 0 < 4

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: r : ℕ+
H : 6 ≤ r
⊢ 0 < 6

Tactic:
positivity

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

Goal state before:
pp: case pos
m n : ℕ
hm : ¬m = 0
hn : n = 0
⊢ liouville (m * n) = liouville m * liouville n

Tactic:
simp [hn]

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

Goal state before:
pp: case inl
n : ℕ
this : ∑ i ∈ n.divisors, ↑(μ i) * -Real.log ↑(n / i) = ∑ i ∈ n.divisors, (↑(μ i) * Real.log ↑i - ↑(μ i) * Real.log ↑n)
hn : n = 1
⊢ ↑(1 n) * Real.log ↑n = 0

Tactic:
simp [hn]

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

Goal state before:
pp: case inr
n : ℕ
this : ∑ i ∈ n.divisors, ↑(μ i) * -Real.log ↑(n / i) = ∑ i ∈ n.divisors, (↑(μ i) * Real.log ↑i - ↑(μ i) * Real.log ↑n)
hn : n ≠ 1
⊢ ↑(1 n) * Real.log ↑n = 0

Tactic:
simp [hn]

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

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

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

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

Goal state before:
pp: X : Type u_1
E : Type u_2
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure X
f : X → E
hf : Integrable f μ
hE : Nontrivial E
this : IsFiniteMeasure (μ.withDensity fun x ↦ ‖f x‖ₑ)
⊢ VectorMeasure.Integrable (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure fun x ↦ ‖f x‖⁻¹ • f x

Tactic:
simp only [VectorMeasure.Integrable, Measure.variation_toSignedMeasure]

Goal state after:
X : Type u_1
E : Type u_2
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure X
f : X → E
hf : Integrable f μ
hE : Nontrivial E
this : IsFiniteMeasure (μ.withDensity fun x ↦ ‖f x‖ₑ)
⊢ Integrable (fun x ↦ ‖f x‖⁻¹ • f x) (μ.withDensity fun x ↦ ‖f x‖ₑ)
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: ⊢ bernoulli 1 = X - C 2⁻¹

Tactic:
simp [bernoulli, ← smul_X_eq_monomial, sum_range_succ, ← C_1, -map_one, neg_div, sub_eq_add_neg]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (1 + X) = bernoulli m + m • X ^ (m - 1)
⊢ d + 2 ≠ 0

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

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

Tactic:
refine (locallyIntegrableOn_iff isLocallyClosed_Ici).mpr fun K hK₁ hK₂ ↦ ?_
  by_cases hK₃ : K.Nonempty
  · have h_inf : a ≤ sInf K := (hK₁ (hK₂.sInf_mem hK₃))
    refine IntegrableOn.mono_set ?_ (Bornology.IsBounded.subset_Icc_sInf_sSup hK₂.isBounded)
    refine integrableOn_mul_sum_Icc _ (ha.trans h_inf) ?_
    refine hg.integrableOn_compact_subset ?_ isCompact_Icc
    exact (Set.Icc_subset_Ici_iff (Real.sInf_le_sSup _ hK₂.bddBelow hK₂.bddAbove)).mpr h_inf
  · rw [Set.not_nonempty_iff_eq_empty.mp hK₃]
    exact integrableOn_empty

Goal state after:
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun x ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(2 * 18) = 6
⊢ 0 < 18 * (2 * 18) ^ √(2 * 18) / 4 ^ (18 / 3)

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun x ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(2 * 512) = 32
⊢ 0 < 4 ^ (512 / 3)

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: n : ℕ
n_large : 512 ≤ n
⊢ 0 < 2 * n

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ log ↑(primorial ⌊x⌋₊) ≤ log 4 * x

Tactic:
trans log (4 ^ ⌊x⌋₊)

Goal state after:
x : ℝ
hx : 0 ≤ x
⊢ log ↑(primorial ⌊x⌋₊) ≤ log (4 ^ ⌊x⌋₊)

x : ℝ
hx : 0 ≤ x
⊢ log (4 ^ ⌊x⌋₊) ≤ log 4 * x
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : EuclideanDomain R
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
bS : Basis ι R S
a : S
y : ℤ
hy : ∀ (k : ι), abv ((bS.repr a) k) ≤ y
⊢ abv (LinearMap.det ((Algebra.lmul R S) (∑ i, (bS.repr a) i • bS i))) ≤ normBound abv bS * y ^ Fintype.card ι

Tactic:
← LinearMap.det_toMatrix bS

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : EuclideanDomain R
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
bS : Basis ι R S
a : S
y : ℤ
hy : ∀ (k : ι), abv ((bS.repr a) k) ≤ y
⊢ abv ((LinearMap.toMatrix bS bS) ((Algebra.lmul R S) (∑ i, (bS.repr a) i • bS i))).det ≤
    normBound abv bS * y ^ Fintype.card ι
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_1
n p : ℕ
left✝¹ : (1 ≤ p ∧ p ≤ n) ∧ Nat.Prime p
k : ℕ
left✝ : 1 ≤ k
hk : k ≤ Nat.log p n
⊢ 1 ≤ p ^ k ∧ p ^ k ≤ n

Tactic:
exact ⟨by grind, pow_le_of_le_log (by linarith) hk⟩

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ (↑(filter Nat.Prime (Icc 1 n))).PairwiseDisjoint fun p ↦ image (fun x ↦ p ^ x) (Icc 1 (Nat.log p n))

Tactic:
by rw [pairwiseDisjoint_iff]; grind [Prime.pow_inj']

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
h : 1 ≤ x
⊢ 0 ≤ x

Tactic:
positivity

Goal state after: