mathlib-initiative/mathlib-tactics huggingface dataset:
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
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ((μ.prod ν B).map Prod.swap) (s ×ˢ t) = (B.flip (ν s)) (μ t)

Tactic:
rw [map_apply _ (by fun_prop) (hs.prod ht)]

Goal state after:
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
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (μ.prod ν B) (Prod.swap ⁻¹' s ×ˢ t) = (B.flip (ν s)) (μ 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
h : ν.HasProd μ B.flip
⊢ μ.HasProd ν B

Tactic:
simpa using

Goal state after:
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
h : ν.HasProd μ B.flip
⊢ μ.HasProd ν B
Module: Mathlib.MeasureTheory.VectorMeasure.Prod

Goal state before:
pp: case basic
X : Type u_2
Y : Type u_3
F : Type u_5
mX : MeasurableSpace X
mY : MeasurableSpace Y
inst✝ : NormedAddCommGroup F
ν : VectorMeasure Y F
s✝ : Set (X × Y)
s : Set X
hs : s ∈ {s | MeasurableSet s}
t : Set Y
⊢ StronglyMeasurable fun x ↦ ν (Prod.mk x ⁻¹' (fun x1 x2 ↦ x1 ×ˢ x2) s t)

Tactic:
simpa using

Goal state after:
case basic
X : Type u_2
Y : Type u_3
F : Type u_5
mX : MeasurableSpace X
mY : MeasurableSpace Y
inst✝ : NormedAddCommGroup F
ν : VectorMeasure Y F
s✝ : Set (X × Y)
s : Set X
hs : s ∈ {s | MeasurableSet s}
t : Set Y
⊢ StronglyMeasurable fun x ↦ s.indicator (fun x ↦ ν t) x
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
ρ : VectorMeasure (X × Y) G
hρ : ∀ (s : Set X) (t : Set Y), MeasurableSet s → MeasurableSet t → ρ (s ×ˢ t) = (B (μ s)) (ν t)
this : μ.HasProd ν B
⊢ μ.prod ν B = ρ

Tactic:
apply ext_of_generateFrom _ _ generateFrom_prod.symm isPiSystem_prod

Goal state after:
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
ρ : VectorMeasure (X × Y) G
hρ : ∀ (s : Set X) (t : Set Y), MeasurableSet s → MeasurableSet t → ρ (s ×ˢ t) = (B (μ s)) (ν t)
this : μ.HasProd ν B
⊢ (μ.prod ν B) univ = ρ univ

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
ρ : VectorMeasure (X × Y) G
hρ : ∀ (s : Set X) (t : Set Y), MeasurableSet s → MeasurableSet t → ρ (s ×ˢ t) = (B (μ s)) (ν t)
this : μ.HasProd ν B
⊢ ∀ s ∈ image2 (fun x1 x2 ↦ x1 ×ˢ x2) {s | MeasurableSet s} {t | MeasurableSet t}, (μ.prod ν B) s = ρ s
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
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
⊢ (ae (μ.variation.restrict s)).NeBot

Tactic:
simpa using

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
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
⊢ ¬μ.variation s = 0
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
s : Set X
hs : MeasurableSet s
hpos : 0 ≤[s] μ
hneg : μ ≤[sᶜ] 0
hposPart : μ.toJordanDecomposition.posPart = μ.toMeasureOfZeroLE s hs hpos
hnegPart : μ.toJordanDecomposition.negPart = μ.toMeasureOfLEZero sᶜ ⋯ hneg
⊢ (VectorMeasure.variation μ) (s ∩ r ∪ sᶜ ∩ r) = (VectorMeasure.variation μ) r

Tactic:
by congr; grind

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✝, IsSemilinearSet s) → IsSemilinearSet (⋃₀ s✝)
hS' : IsSemilinearSet a✝¹ ∧ ∀ a ∈ s✝, IsSemilinearSet a
⊢ IsSemilinearSet (⋃₀ insert a✝¹ s✝)

Tactic:
simpa using

Goal state after:
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' : IsSemilinearSet a✝¹ ∧ ∀ a ∈ s✝, IsSemilinearSet a
⊢ IsSemilinearSet (a✝¹ ∪ ⋃₀ 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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
inst✝ : Nontrivial E
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖x‖₊ * ‖y‖₊
this : μ.variation = 1 • μ.variation
⊢ ∀ (x : E) (y : F), ‖(B x) y‖₊ = 1 * ‖x‖₊ * ‖y‖₊

Tactic:
simpa using

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
inst✝ : Nontrivial E
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖x‖₊ * ‖y‖₊
this : μ.variation = 1 • μ.variation
⊢ ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖x‖₊ * ‖y‖₊
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 : (∀ t ∈ s✝, IsLinearSet t) → IsSemilinearSet ↑(closure (⋃₀ s✝))
hS' : IsLinearSet a✝¹ ∧ ∀ a ∈ s✝, IsLinearSet a
⊢ IsSemilinearSet ↑(closure (⋃₀ insert a✝¹ s✝))

Tactic:
simpa using

Goal state after:
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 : (∀ t ∈ s✝, IsLinearSet t) → IsSemilinearSet ↑(closure (⋃₀ s✝))
hS' : IsLinearSet a✝¹ ∧ ∀ a ∈ s✝, IsLinearSet a
⊢ IsSemilinearSet (↑(closure a✝¹) + ↑(closure (⋃₀ s✝)))
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 : (∀ t ∈ s✝, IsLinearSet t) → IsSemilinearSet ↑(closure (⋃₀ s✝))
hS' : ∀ t ∈ insert a✝¹ s✝, IsLinearSet t
⊢ IsSemilinearSet ↑(closure (⋃₀ insert a✝¹ s✝))

Tactic:
simp_rw [mem_insert_iff, forall_eq_or_imp] at hS'
    simpa [closure_union, coe_sup] using hS'.1.closure.add (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 g : X → E
B : E →L[ℝ] F →L[ℝ] G
h : f =ᵐ[μ.variation] g
hf : ¬μ.Integrable f
⊢ ¬μ.Integrable g

Tactic:
simpa using

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 g : X → E
B : E →L[ℝ] F →L[ℝ] G
h : f =ᵐ[μ.variation] g
hf : ¬μ.Integrable f
⊢ ¬Integrable f μ.variation
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' : IsProperSemilinearSet a✝¹ ∧ ∀ a ∈ s✝, IsProperSemilinearSet a
⊢ IsProperSemilinearSet (⋃₀ insert a✝¹ s✝)

Tactic:
simpa using

Goal state after:
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' : IsProperSemilinearSet a✝¹ ∧ ∀ a ∈ s✝, IsProperSemilinearSet a
⊢ IsProperSemilinearSet (a✝¹ ∪ ⋃₀ s✝)
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: case pos
X : Type u_2
E : Type u_4
F : Type u_5
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → E
μ : VectorMeasure X F
hf : μ.Integrable f
s : Set X
hs : MeasurableSet s
⊢ (μ.restrict s).Integrable f

Tactic:
simpa using

Goal state after:
case pos
X : Type u_2
E : Type u_4
F : Type u_5
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → E
μ : VectorMeasure X F
hf : μ.Integrable f
s : Set X
hs : MeasurableSet s
⊢ Integrable f (μ.variation.restrict s)
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: case inr
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‖₊ * ‖B‖₊⁻¹ * δ ≤ δ

Tactic:
apply mul_le_of_le_one_left (by positivity) mul_inv_le_one

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 < δ
ρ : NNReal
ρpos : ρ > 0
hδ : ‖B‖₊ * ρ ≤ δ
⊢ ↑ρ ≠ 0

Tactic:
simpa using

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 < δ
ρ : NNReal
ρpos : ρ > 0
hδ : ‖B‖₊ * ρ ≤ δ
⊢ ¬ρ = 0
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: case a
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : IsCancelAdd M
a : M
t : Finset M
ih : ∀ m < t.card, ∀ (a : M) (t : Finset M), t.card = m → IsProperSemilinearSet (a +ᵥ ↑(closure ↑t))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : ∑ x ∈ t', f x • x = ∑ x ∈ t \ t', f x • x
g : M → ℕ
ih' :
  ∀ m < g i,
    ∀ (g : M → ℕ),
      g i = m → a +ᵥ ∑ a ∈ t, g a • a ∈ ⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ ↑(closure ↑(t.erase j))
hfg : ∀ j ∈ t', f j ≤ g j
j : M
hj : j ∈ t'
⊢ g j • j = (g j - f j + f j) • j

Tactic:
tsub_add_cancel_of_le (hfg j hj)

Goal state after:
case a
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : IsCancelAdd M
a : M
t : Finset M
ih : ∀ m < t.card, ∀ (a : M) (t : Finset M), t.card = m → IsProperSemilinearSet (a +ᵥ ↑(closure ↑t))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : ∑ x ∈ t', f x • x = ∑ x ∈ t \ t', f x • x
g : M → ℕ
ih' :
  ∀ m < g i,
    ∀ (g : M → ℕ),
      g i = m → a +ᵥ ∑ a ∈ t, g a • a ∈ ⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ ↑(closure ↑(t.erase j))
hfg : ∀ j ∈ t', f j ≤ g j
j : M
hj : j ∈ t'
⊢ g j • j = g j • j
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a : ℕ
t : Finset ℕ
ht : LinearIndepOn ℕ id ↑t
⊢ t.card ≤ 1

Tactic:
simpa using

Goal state after:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a : ℕ
t : Finset ℕ
ht : LinearIndepOn ℕ id ↑t
⊢ t.card ≤ 1
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id ↑{b}
⊢ b ≠ 0

Tactic:
simpa using

Goal state after:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id ↑{b}
⊢ ¬b = 0
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: case e'_8
α : 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)})
x✝ : α ⊕ Fin n → ℕ
a✝ : ℕ
i : Fin (n + 1)
⊢ Fin.snoc (x✝ ∘ Sum.inr) a✝ i = ((Sum.elim x✝ (Fin.cons a✝ finZeroElim) ∘ ⇑e.symm) ∘ Sum.inr) i

Tactic:
cases i using Fin.lastCases

Goal state after:
case e'_8.last
α : 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)})
x✝ : α ⊕ Fin n → ℕ
a✝ : ℕ
⊢ Fin.snoc (x✝ ∘ Sum.inr) a✝ (Fin.last n) = ((Sum.elim x✝ (Fin.cons a✝ finZeroElim) ∘ ⇑e.symm) ∘ Sum.inr) (Fin.last n)

case e'_8.cast
α : 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)})
x✝ : α ⊕ Fin n → ℕ
a✝ : ℕ
i✝ : Fin n
⊢ Fin.snoc (x✝ ∘ Sum.inr) a✝ i✝.castSucc = ((Sum.elim x✝ (Fin.cons a✝ finZeroElim) ∘ ⇑e.symm) ∘ Sum.inr) i✝.castSucc
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: A : Set ℕ
hmul : A.Definable presburger {v | v 0 = v 1 * v 2}
x✝ : Fin 1 → ℕ
⊢ x✝ ∈ {x | x 0 ∈ {x | ∃ x_1, x_1 * x_1 = x}} ↔
    x✝ ∈ (fun g ↦ g ∘ ![0]) '' (fun g ↦ g ∘ ![0, 1, 1]) ⁻¹' {v | v 0 = v 1 * v 2}

Tactic:
simpa using

Goal state after:
A : Set ℕ
hmul : A.Definable presburger {v | v 0 = v 1 * v 2}
x✝ : Fin 1 → ℕ
⊢ (∃ x, x * x = x✝ 0) ↔ ∃ a, x✝ 0 = a * a
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: A : Set ℕ
⊢ ¬A.Definable presburger {v | v 0 = v 1 * v 2}

Tactic:
by
  intro hmul
  have hsqr : A.Definable₁ presburger {x * x | x : ℕ} := by
    rw [Definable₁]
    convert! (hmul.preimage_comp (β := Fin 2) ![0, 1, 1]).image_comp ![0]
    ext
    simpa [funext_iff, Fin.exists_fin_succ_pi] using exists_congr fun _ => Eq.comm
  rw [definable₁_iff_ultimately_periodic] at hsqr
  rcases hsqr with ⟨k, p, hp, h⟩
  specialize h ((max k p) * (max k p)) ((Nat.le_mul_self _).trans' (le_max_left _ _))
  simp only [mem_ofPred_eq, exists_apply_eq_apply, true_iff] at h
  rcases h with ⟨x, h₁⟩
  by_cases h₂ : x ≤ max k p
  · apply Nat.mul_self_le_mul_self at h₂
    grind
  · simp only [not_le, Nat.lt_iff_add_one_le] at h₂
    apply Nat.mul_self_le_mul_self at h₂
    grind

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

Goal state before:
pp: case e_a
M : Type u_1
inst✝ : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x : M
⊢ x ∈ t ↔ x ∈ ⇑(closure (insert a t)).subtype '' ⇑(closure (insert a t)).subtype ⁻¹' t

Tactic:
simpa using

Goal state after:
case e_a
M : Type u_1
inst✝ : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x : M
⊢ x ∈ t → x ∈ closure (insert a t)
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: case succ
L : Language
G' : ℕ → Type w
inst✝ : (i : ℕ) → L.Structure (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
m : ℕ
x : G' m
k : ℕ
ih : ∀ (h : m ≤ m + k), (natLERec f' m (m + k) h) x = Nat.leRecOn h (fun k ↦ ⇑(f' k)) x
h : m ≤ m + (k + 1)
⊢ (natLERec f' m (m + (k + 1)) h) x = Nat.leRecOn h (fun k ↦ ⇑(f' k)) x

Tactic:
rw [Nat.leRecOn_succ le_self_add, natLERec, Nat.leRecOn_succ le_self_add, ← natLERec,
      Embedding.comp_apply, ih]

Goal state after:
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' : IsSemilinearSet a✝¹ ∧ ∀ a ∈ s✝, IsSemilinearSet a
⊢ IsSemilinearSet (⋂₀ insert a✝¹ s✝)

Tactic:
simpa using

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' : IsSemilinearSet a✝¹ ∧ ∀ a ∈ s✝, IsSemilinearSet a
⊢ IsSemilinearSet (a✝¹ ∩ ⋂₀ s✝)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
x y : ι → ℕ
h : toRatVec x = toRatVec y
i : ι
⊢ x i = y i

Tactic:
simpa using

Goal state after:
ι : Type u_3
x y : ι → ℕ
h : toRatVec x = toRatVec y
i : ι
⊢ x i = y i
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
t : Finset (ι → ℕ)
f : (ι → ℕ) → ℤ
ht : ↑t ⊆ s
hf : ∀ i ∉ t, f i = 0
heq : ∑ i ∈ t, f i • toRatVec i = 0
i : ι → ℕ
hs : (Int.toNat ∘ f) i = (Int.toNat ∘ (fun x ↦ -x) ∘ f) i
hi : i ∈ t
⊢ (f i).toNat = (-f i).toNat

Tactic:
simpa using

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
t : Finset (ι → ℕ)
f : (ι → ℕ) → ℤ
ht : ↑t ⊆ s
hf : ∀ i ∉ t, f i = 0
heq : ∑ i ∈ t, f i • toRatVec i = 0
i : ι → ℕ
hs : (Int.toNat ∘ f) i = (Int.toNat ∘ (fun x ↦ -x) ∘ f) i
hi : i ∈ t
⊢ (f i).toNat = (-f i).toNat
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mem
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x y✝ : ι → ℕ
i : ↑hs.basisSet
t : Set (ι → ℕ)
ht : t ⊆ hs.basisSet
hi : ↑i ∉ t
y : ι → ℕ
hy : y ∈ t
⊢ (hs.basis.repr (hs.basis ⟨y, ⋯⟩)) i = 0

Tactic:
simpa using

Goal state after:
case mem
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x y✝ : ι → ℕ
i : ↑hs.basisSet
t : Set (ι → ℕ)
ht : t ⊆ hs.basisSet
hi : ↑i ∉ t
y : ι → ℕ
hy : y ∈ t
⊢ ¬y = ↑i
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mp.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x = hs.base
i : ↑hs.basisSet
hi : hs.floor x i < 0
j : ↑hs.basisSet
hj : j ∈ Finset.univ.erase i
⊢ ↑j ∈ hs.basisSet \ {↑i}

Tactic:
simpa using

Goal state after:
case mp.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x = hs.base
i : ↑hs.basisSet
hi : hs.floor x i < 0
j : ↑hs.basisSet
hj : j ∈ Finset.univ.erase i
⊢ ¬j = i
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mp.refine_3
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x = hs.base
i : ↑hs.basisSet
hi : hs.floor x i < 0
j : ↑hs.basisSet
hj : j ∈ Finset.univ.erase i
⊢ ↑j ∈ hs.basisSet \ {↑i}

Tactic:
simpa using

Goal state after:
case mp.refine_3
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x = hs.base
i : ↑hs.basisSet
hi : hs.floor x i < 0
j : ↑hs.basisSet
hj : j ∈ Finset.univ.erase i
⊢ ¬j = i
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mpr.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
n : ℕ
heq : hs.floor x i = -↑(n + 1)
⊢ hs.floor x i < 0

Tactic:
simpa using

Goal state after:
case mpr.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
n : ℕ
heq : hs.floor x i = -↑(n + 1)
⊢ -1 < ↑n
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mp.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x = hs.base
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
hi' : 0 < hs.floor x i
j : ↑hs.basisSet
hj : j ∈ Finset.univ.erase i
⊢ ↑j ∈ hs.basisSet \ {↑i}

Tactic:
simpa using

Goal state after:
case mp.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x = hs.base
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
hi' : 0 < hs.floor x i
j : ↑hs.basisSet
hj : j ∈ Finset.univ.erase i
⊢ ¬j = i