mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, μ (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s | ∃ c ∈ C, ↑s = c}
C'C : ∀ s ∈ C', ↑s ∈ C
C'_dense : Dense C'
m₀ : ↑C' → E := fun x ↦ m ↑↑x
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ μ ↑s
s t : MeasuredSets μ
h : Disjoint ↑s ↑t
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : 8 * δ = ε
s' : Set α
s'C : s' ∈ C
hs' : μ (s' ∆ ↑s) < δ
⊢ ‖m₁ ⟨↑s ∪ ↑t, ⋯⟩ - m₁ s - m₁ t‖ₑ < ε

Tactic:
obtain ⟨t', t'C, ht'⟩ : ∃ t' ∈ C, μ (t' ∆ t) < δ := h'C _ _ t.2 δpos

Goal state after:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, μ (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s | ∃ c ∈ C, ↑s = c}
C'C : ∀ s ∈ C', ↑s ∈ C
C'_dense : Dense C'
m₀ : ↑C' → E := fun x ↦ m ↑↑x
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ μ ↑s
s t : MeasuredSets μ
h : Disjoint ↑s ↑t
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : 8 * δ = ε
s' : Set α
s'C : s' ∈ C
hs' : μ (s' ∆ ↑s) < δ
t' : Set α
t'C : t' ∈ C
ht' : μ (t' ∆ ↑t) < δ
⊢ ‖m₁ ⟨↑s ∪ ↑t, ⋯⟩ - m₁ s - m₁ t‖ₑ < ε
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
G : Type u_6
mX : MeasurableSpace X
mY : MeasurableSpace Y
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X E
ν : VectorMeasure Y F
B : E →L[ℝ] F →L[ℝ] G
inst✝ : μ.HasProd ν B
⊢ ∃ ρ, ∀ (s : Set Y) (t : Set X), MeasurableSet s → MeasurableSet t → ρ (s ×ˢ t) = (B.flip (ν s)) (μ t)

Tactic:
refine ⟨(μ.prod ν B).map Prod.swap, fun s t hs ht ↦ ?_⟩
    rw [map_apply _ (by fun_prop) (hs.prod ht)]
    simp

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

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : SignedMeasure X
r : Set X
hr : MeasurableSet r
⊢ μ.totalVariation r = (VectorMeasure.variation μ) r

Tactic:
apply le_antisymm

Goal state after:
case a
X : Type u_1
mX : MeasurableSpace X
μ : SignedMeasure X
r : Set X
hr : MeasurableSet r
⊢ μ.totalVariation r ≤ (VectorMeasure.variation μ) r

case a
X : Type u_1
mX : MeasurableSpace X
μ : SignedMeasure X
r : Set X
hr : MeasurableSet r
⊢ (VectorMeasure.variation μ) r ≤ μ.totalVariation r
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‖₊
⊢ (μ.transpose B).variation = C • μ.variation

Tactic:
apply le_antisymm

Goal state after:
case a
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‖₊
⊢ (μ.transpose B).variation ≤ C • μ.variation

case a
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‖₊
⊢ C • μ.variation ≤ (μ.transpose B).variation
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.toList.toFinset, Term.realize v (f i)

Tactic:
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 mp.add.inr.inr
M : Type u_1
inst✝ : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x✝ x : M
hx : x ∈ closure (insert a t)
hx✝ : a + x ∈ closure (a +ᵥ ↑(closure t))
y : M
hy : y ∈ closure (insert a t)
hy✝ : a + y ∈ closure (a +ᵥ ↑(closure t))
⊢ a + x + (a + y) = 0 ∨ ∃ y_1 ∈ closure (insert a t), a + y_1 = a + x + (a + y)

Tactic:
refine Or.inr ⟨_, add_mem (mem_closure_of_mem (mem_insert _ _)) (add_mem hx hy), ?_⟩
          simp_rw [← add_assoc, add_right_comm a a x]

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
s : Set M
hs : IsProperLinearSet s
⊢ IsLinearSet s

Tactic:
by
  rcases hs with ⟨a, t, ht, _, rfl⟩
  exact ⟨a, t, ht, rfl⟩

Goal state after:
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
inst✝ : NormedSpace ℝ F
f : X → E
μ : VectorMeasure X F
hμ : μ.Integrable f
c : ℝ
⊢ (c • μ).Integrable f

Tactic:
apply Integrable.mono_measure (Integrable.smul_measure_nnreal hμ (c := ‖c‖₊))

Goal state after:
X : Type u_2
E : Type u_4
F : Type u_5
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : X → E
μ : VectorMeasure X F
hμ : μ.Integrable f
c : ℝ
⊢ (c • μ).variation ≤ ‖c‖₊ • μ.variation
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 : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
⊢ ∫ᵛ (x : X), f x ∂[B; -μ] = -∫ᵛ (x : X), f x ∂[B; μ]

Tactic:
simp [integral, ← setToFun_neg', FunLike.coe_neg]

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
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
⊢ ∫ᵛ (x : X), f x ∂[-B; μ] = -∫ᵛ (x : X), f x ∂[B; μ]

Tactic:
simp [integral, ← setToFun_neg', FunLike.coe_neg]

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

Goal state before:
pp: case pos
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
⊢ ‖∫ᵛ (a : X), f a ∂[B; μ]‖ ≤ ‖B‖ * ∫ (a : X), ‖f a‖ ∂μ.variation

Tactic:
calc ‖∫ᵛ a, f a ∂[B; μ]‖
    _ ≤ ‖B‖ * ENNReal.toReal (∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ.variation) :=
      norm_integral_le_lintegral_norm
    _ = ‖B‖ * ∫ a, ‖f a‖ ∂μ.variation := by
      rw [integral_eq_lintegral_of_nonneg_ae le_ae <| h.norm]

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
ι : Type u_8
f : X → E
hfi : AEStronglyMeasurable f μ.variation
F : ι → X → E
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, μ.Integrable (F i)
hF : Tendsto (fun i ↦ eLpNorm (F i - f) 1 μ.variation) l (𝓝 0)
⊢ Tendsto (fun i ↦ ∫⁻ (x : X), ‖F i x - f x‖ₑ ∂μ.variation) l (𝓝 0)

Tactic:
simp_rw [eLpNorm_one_eq_lintegral_enorm, Pi.sub_apply] at hF

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
μ : VectorMeasure X F✝
B : E →L[ℝ] F✝ →L[ℝ] G
ι : Type u_8
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)
⊢ Tendsto (fun i ↦ ∫⁻ (x : X), ‖F i x - f x‖ₑ ∂μ.variation) l (𝓝 0)
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✝
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 ↦ eLpNorm (F i - f) 1 μ.variation) l (𝓝 0)
s : Set X
⊢ Tendsto (fun i ↦ ∫⁻ (x : X), ‖F i x - f x‖ₑ ∂μ.variation) l (𝓝 0)

Tactic:
simp_rw [eLpNorm_one_eq_lintegral_enorm, Pi.sub_apply] at hF

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✝
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)
s : Set X
hF : Tendsto (fun i ↦ ∫⁻ (x : X), ‖F i x - f x‖ₑ ∂μ.variation) l (𝓝 0)
⊢ Tendsto (fun i ↦ ∫⁻ (x : X), ‖F i x - f x‖ₑ ∂μ.variation) l (𝓝 0)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: case func.inl.zero
α : 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.zero) fun i ↦ Term.realize v (ts i)) = k + u ⬝ᵥ v

Tactic:
refine ⟨0, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp

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})
ρ : ℝ≥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‖ₑ + ρ)
⊢ ∑ i ∈ g.range, ∑ p ∈ P i, ‖i‖ₑ * ‖((μ.transpose B).restrict s) p‖ₑ + ↑δ =
    ∑ i ∈ g.range.sigma P, ‖i.fst‖ₑ * ‖((μ.transpose B).restrict s) i.snd‖ₑ + ↑δ

Tactic:
Finset.sum_sigma'

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.sigma P, ‖x.fst‖ₑ * ‖((μ.transpose B).restrict s) x.snd‖ₑ + ↑δ =
    ∑ i ∈ g.range.sigma P, ‖i.fst‖ₑ * ‖((μ.transpose B).restrict s) i.snd‖ₑ + ↑δ
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
β : Type u_9
inst✝ : MeasurableSpace β
φ : X → β
⊢ ((μ.map φ).transpose B).variation ≤ Measure.map φ (μ.transpose B).variation

Tactic:
by
  grw [transpose_map, variation_map_le]

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

Goal state before:
pp: α : Type u_1
A : Set ℕ
inst✝ : Finite α
n✝ : ℕ
this : Fintype α
n : ℕ
φ : presburger[[↑A]].BoundedFormula α (n + 1)
e : (α ⊕ Fin n) ⊕ Fin 1 ≃ α ⊕ Fin (n + 1) :=
  (Equiv.sumAssoc α (Fin n) (Fin 1)).trans ((_root_.Equiv.refl α).sumCongr finSumFinEquiv)
ih : IsSemilinearSet (⇑(LinearEquiv.funCongrLeft ℕ ℕ e) '' {v | φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)})
⊢ {v | ∀ (x : ℕ), φ.Realize (v ∘ Sum.inl) (Fin.snoc (v ∘ Sum.inr) x)} =
    {a | ¬∃ y, Sum.elim a y ∈ (⇑(LinearEquiv.funCongrLeft ℕ ℕ e) '' {v | φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)})ᶜ}

Tactic:
not_exists,

Goal state after:
α : Type u_1
A : Set ℕ
inst✝ : Finite α
n✝ : ℕ
this : Fintype α
n : ℕ
φ : presburger[[↑A]].BoundedFormula α (n + 1)
e : (α ⊕ Fin n) ⊕ Fin 1 ≃ α ⊕ Fin (n + 1) :=
  (Equiv.sumAssoc α (Fin n) (Fin 1)).trans ((_root_.Equiv.refl α).sumCongr finSumFinEquiv)
ih : IsSemilinearSet (⇑(LinearEquiv.funCongrLeft ℕ ℕ e) '' {v | φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)})
⊢ {v | ∀ (x : ℕ), φ.Realize (v ∘ Sum.inl) (Fin.snoc (v ∘ Sum.inr) x)} =
    {a |
      ∀ (x : Fin 1 → ℕ),
        Sum.elim a x ∉ (⇑(LinearEquiv.funCongrLeft ℕ ℕ e) '' {v | φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)})ᶜ}
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
s₁ s₂ : Set M
hs₁ : IsSemilinearSet s₁
hs₂ : IsSemilinearSet s₂
⊢ IsSemilinearSet (s₁ ∩ s₂)

Tactic:
by
  rcases hs₁.exists_fg_eq_subtypeVal₂ hs₂ with ⟨P, s₁', s₂', hP, hs₁', rfl, hs₂', rfl⟩
  rw [← image_inter Subtype.val_injective]
  apply image (f := P.subtype)
  rw [← AddMonoid.fg_iff_addSubmonoid_fg, AddMonoid.fg_def, fg_iff_exists_fin_addMonoidHom] at hP
  rcases hP with ⟨n, f, hf⟩
  rw [AddMonoidHom.mrange_eq_top] at hf
  rw [← image_preimage_eq (s₁' ∩ s₂') hf, preimage_inter]
  apply image
  apply Nat.isSemilinearSet_inter <;> apply Nat.isSemilinearSet_preimage <;> assumption

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

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : LinearIndepOn ℕ id s
⊢ LinearIndependent ℚ fun (x : ↑s) ↦ toRatVec ↑x

Tactic:
← LinearIndependent.iff_fractionRing ℤ ℚ,

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : LinearIndepOn ℕ id s
⊢ LinearIndependent ℤ fun (x : ↑s) ↦ toRatVec ↑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 g : M ≃ₚ[L] N
h : f ≤ g
x : ↥f.dom
⊢ g.toEquiv ((inclusion ⋯) x) = (inclusion ⋯) (f.toEquiv x)

Tactic:
apply (subtype _).injective
  change (subtype _).comp (g.toEquiv.toEmbedding.comp (inclusion _)) x = _
  rw [subtype_toEquiv_inclusion h]
  simp

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✝ : ι → ℚ
⊢ (∃ a, toRatVec ((Pi.basisFun ℕ ι) a) = x✝) ↔ ∃ y, (Pi.basisFun ℚ ι) y = x✝

Tactic:
congr!

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x✝¹ : ι → ℚ
x✝ : ι
⊢ toRatVec ((Pi.basisFun ℕ ι) x✝) = (Pi.basisFun ℚ ι) x✝
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case refl
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ { dom := g.1, cod := cod_f, toEquiv := equiv_f } = g

Tactic:
apply le_antisymm

Goal state after:
case refl.le_fg
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ { dom := g.1, cod := cod_f, toEquiv := equiv_f } ≤ g

case refl.le_gf
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ g ≤ { dom := g.1, cod := cod_f, toEquiv := equiv_f }
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
xy : Quotient.lift (fun x ↦ (g x.fst) x.snd) ⋯ ⟦Quotient.out x⟧ = Quotient.lift (fun x ↦ (g x.fst) x.snd) ⋯ y
⊢ x = y

Tactic:
← Quotient.out_eq y,

Goal state after:
L : Language
ι : Type v
inst✝⁵ : Preorder ι
G : ι → Type w
inst✝⁴ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝³ : IsDirectedOrder ι
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝¹ : Nonempty ι
P : Type u₁
inst✝ : L.Structure P
g : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
x y : DirectLimit G f
xy :
  Quotient.lift (fun x ↦ (g x.fst) x.snd) ⋯ ⟦Quotient.out x⟧ =
    Quotient.lift (fun x ↦ (g x.fst) x.snd) ⋯ ⟦Quotient.out y⟧
⊢ x = 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
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⟧ = y

Tactic:
← Quotient.out_eq y,

Goal state after:
L : Language
ι : Type v
inst✝⁵ : Preorder ι
G : ι → Type w
inst✝⁴ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝³ : IsDirectedOrder ι
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝¹ : Nonempty ι
P : Type u₁
inst✝ : L.Structure P
g : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
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.Fraisse

Goal state before:
pp: L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : (Quotient.mk' '' K).Countable
fg : ∀ M ∈ K, Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled L.Structure), (∃ x ∈ K, (Quotient.mk' x).out ≈ a) ↔ ∃ y, (F y).out ≈ a
hF' : ∀ (n : ℕ), (F n).out ∈ K
P : ↑K → ℕ → Bundled L.Structure
hPK : ∀ (N : ↑K) (n : ℕ), P N n ∈ K
hP : ∀ (N : ↑K) (n : ℕ), (fun M N ↦ Nonempty (↑M ↪[L] ↑N)) (↑N) (P N n)
hFP : ∀ (N : ↑K) (n : ℕ), (fun M N ↦ Nonempty (↑M ↪[L] ↑N)) (F (n + 1)).out (P N n)
G : ℕ → ↑K := Nat.rec ⟨(F 0).out, ⋯⟩ fun n N ↦ ⟨P N n, ⋯⟩
f : (i j : ℕ) → i ≤ j → ↑↑(G i) ↪[L] ↑↑(G j) := DirectedSystem.natLERec fun n ↦ Nonempty.some ⋯
⊢ ∃ M, Structure.CG L ↑M ∧ L.age ↑M = K

Tactic:
refine ⟨Bundled.of (@DirectLimit L _ _ (fun n ↦ (G n).val) _ f _ _), ?_, ?_⟩

Goal state after:
case refine_1
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : (Quotient.mk' '' K).Countable
fg : ∀ M ∈ K, Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled L.Structure), (∃ x ∈ K, (Quotient.mk' x).out ≈ a) ↔ ∃ y, (F y).out ≈ a
hF' : ∀ (n : ℕ), (F n).out ∈ K
P : ↑K → ℕ → Bundled L.Structure
hPK : ∀ (N : ↑K) (n : ℕ), P N n ∈ K
hP : ∀ (N : ↑K) (n : ℕ), (fun M N ↦ Nonempty (↑M ↪[L] ↑N)) (↑N) (P N n)
hFP : ∀ (N : ↑K) (n : ℕ), (fun M N ↦ Nonempty (↑M ↪[L] ↑N)) (F (n + 1)).out (P N n)
G : ℕ → ↑K := Nat.rec ⟨(F 0).out, ⋯⟩ fun n N ↦ ⟨P N n, ⋯⟩
f : (i j : ℕ) → i ≤ j → ↑↑(G i) ↪[L] ↑↑(G j) := DirectedSystem.natLERec fun n ↦ Nonempty.some ⋯
⊢ Structure.CG L ↑(Bundled.of (DirectLimit (fun n ↦ ↑↑(G n)) f))

case refine_2
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : (Quotient.mk' '' K).Countable
fg : ∀ M ∈ K, Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled L.Structure), (∃ x ∈ K, (Quotient.mk' x).out ≈ a) ↔ ∃ y, (F y).out ≈ a
hF' : ∀ (n : ℕ), (F n).out ∈ K
P : ↑K → ℕ → Bundled L.Structure
hPK : ∀ (N : ↑K) (n : ℕ), P N n ∈ K
hP : ∀ (N : ↑K) (n : ℕ), (fun M N ↦ Nonempty (↑M ↪[L] ↑N)) (↑N) (P N n)
hFP : ∀ (N : ↑K) (n : ℕ), (fun M N ↦ Nonempty (↑M ↪[L] ↑N)) (F (n + 1)).out (P N n)
G : ℕ → ↑K := Nat.rec ⟨(F 0).out, ⋯⟩ fun n N ↦ ⟨P N n, ⋯⟩
f : (i j : ℕ) → i ≤ j → ↑↑(G i) ↪[L] ↑↑(G j) := DirectedSystem.natLERec fun n ↦ Nonempty.some ⋯
⊢ L.age ↑(Bundled.of (DirectLimit (fun n ↦ ↑↑(G n)) f)) = K