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

Goal state before:
pp: ι : Type u_1
X : Type u_2
E : Type u_3
F : Type u_4
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : VectorMeasure X F
f : X → E
s : Set ι
hs : s.Finite
t : ι → Set X
ht : ∀ i ∈ s, MeasurableSet (t i)
h't : ∀ i ∈ s, μ.IntegrableOn f (t i)
⊢ μ.IntegrableOn f (⋃ i ∈ s, t i)

Tactic:
by
  induction s, hs using Set.Finite.induction_on with
  | empty => simp
  | insert _ h's hf =>
    simp only [mem_insert_iff, forall_eq_or_imp, iUnion_iUnion_eq_or_left] at ht h't ⊢
    exact IntegrableOn.union ht.1 (h's.measurableSet_biUnion ht.2)  h't.1 (hf ht.2 h't.2)

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
s t : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
hs : MeasurableSet s
ht : MeasurableSet t
hfs : μ.IntegrableOn f s
hts : t ⊆ s
⊢ ∫ᵛ (x : X) in s \ t, f x ∂[B; μ] = ∫ᵛ (x : X) in s, f x ∂[B; μ] - ∫ᵛ (x : X) in t, f x ∂[B; μ]

Tactic:
by
  rw [eq_sub_iff_add_eq, ← setIntegral_union (by grind) (hs.diff ht) ht (hfs.mono hs sdiff_subset)
    (hfs.mono hs hts), sdiff_union_of_subset hts]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : Set X
hs : IsHahnDecomposition μ ν s
hsc : IsHahnDecomposition ν μ sᶜ
h₁ :
  ((ν - μ).restrict s).toSignedMeasure =
    VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s
h₂ :
  ((μ - ν).restrict sᶜ).toSignedMeasure =
    VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ
h₁' : ((μ - ν).restrict s).toSignedMeasure = toSignedMeasure 0
h₂' : ((ν - μ).restrict sᶜ).toSignedMeasure = toSignedMeasure 0
partition₁ :
  ((μ - ν).restrict s).toSignedMeasure + VectorMeasure.restrict (μ - ν).toSignedMeasure sᶜ = (μ - ν).toSignedMeasure
partition₂ :
  ((ν - μ).restrict s).toSignedMeasure + VectorMeasure.restrict (ν - μ).toSignedMeasure sᶜ = (ν - μ).toSignedMeasure
⊢ μ.toSignedMeasure - ν.toSignedMeasure = (μ - ν).toSignedMeasure - (ν - μ).toSignedMeasure

Tactic:
toSignedMeasure_restrict_eq_restrict_toSignedMeasure _ _ hs.measurableSet.compl

Goal state after:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : Set X
hs : IsHahnDecomposition μ ν s
hsc : IsHahnDecomposition ν μ sᶜ
h₁ :
  ((ν - μ).restrict s).toSignedMeasure =
    VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s
h₂ :
  ((μ - ν).restrict sᶜ).toSignedMeasure =
    VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ
h₁' : ((μ - ν).restrict s).toSignedMeasure = toSignedMeasure 0
h₂' : ((ν - μ).restrict sᶜ).toSignedMeasure = toSignedMeasure 0
partition₁ : ((μ - ν).restrict s).toSignedMeasure + ((μ - ν).restrict sᶜ).toSignedMeasure = (μ - ν).toSignedMeasure
partition₂ : ((ν - μ).restrict s).toSignedMeasure + ((ν - μ).restrict sᶜ).toSignedMeasure = (ν - μ).toSignedMeasure
⊢ μ.toSignedMeasure - ν.toSignedMeasure = (μ - ν).toSignedMeasure - (ν - μ).toSignedMeasure
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 t : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
hs : MeasurableSet s
ht : MeasurableSet t
ht_eq : ∀ x ∈ t, f x = 0
⊢ ∀ᵐ (x : X) ∂μ.variation.restrict t, f x = 0

Tactic:
rw [ae_restrict_iff' ht]

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 t : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
hs : MeasurableSet s
ht : MeasurableSet t
ht_eq : ∀ x ∈ t, f x = 0
⊢ ∀ᵐ (x : X) ∂μ.variation, x ∈ t → f x = 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
f : X → E
s : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
hs : MeasurableSet s
h : ∀ᵐ (x : X) ∂μ.variation, x ∉ s → f x = 0
⊢ ∀ᵐ (x : X) ∂μ.variation.restrict (univ \ s), f x = 0

Tactic:
apply (ae_restrict_iff' (MeasurableSet.univ.diff hs)).2

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
hs : MeasurableSet s
h : ∀ᵐ (x : X) ∂μ.variation, x ∉ s → f x = 0
⊢ ∀ᵐ (x : X) ∂μ.variation, x ∈ univ \ s → f x = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation

Goal state before:
pp: case zero
X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
h : μ.semivariation univ = ∞
t : Set X → Set X
t_meas : ∀ (s : Set X), MeasurableSet s → μ.semivariation s = ∞ → MeasurableSet (t s)
t_subs : ∀ (s : Set X), MeasurableSet s → μ.semivariation s = ∞ → t s ⊆ s
t_var : ∀ (s : Set X), MeasurableSet s → μ.semivariation s = ∞ → μ.semivariation (t s) = ∞
ht : ∀ (s : Set X), MeasurableSet s → μ.semivariation s = ∞ → 1 ≤ ‖μ (s \ t s)‖ₑ
s : ℕ → Set X := fun n ↦ t^[n] univ
⊢ MeasurableSet (s 0) ∧ μ.semivariation (s 0) = ∞

Tactic:
| zero =>

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✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : hα = generateFrom C
M : ∀ s ∈ C, MeasurableSet s
D : Set (Set α)
DC : D ⊆ C
D_count : D.Countable
hD : ∀ s ∈ C, s ≤ᵐ[μ] ⋃₀ D
MD : MeasurableSet (⋃₀ D)
μ' : Measure α := μ.restrict (⋃₀ D)
s : Set α
hs : s ∈ C
⊢ μ s ≤ μ (s ∩ ⋃₀ D)

Tactic:
apply measure_mono_ae

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 : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : hα = generateFrom C
M : ∀ s ∈ C, MeasurableSet s
D : Set (Set α)
DC : D ⊆ C
D_count : D.Countable
hD : ∀ s ∈ C, s ≤ᵐ[μ] ⋃₀ D
MD : MeasurableSet (⋃₀ D)
μ' : Measure α := ⋯
s : Set α
hs : s ∈ C
⊢ s ≤ᵐ[μ] s ∩ ⋃₀ D
Module: Mathlib.MeasureTheory.VectorMeasure.Prod

Goal state before:
pp: 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)
hs : MeasurableSet s
⊢ StronglyMeasurable fun x ↦ ν (Prod.mk x ⁻¹' s)

Tactic:
induction s, hs
    using MeasurableSpace.induction_on_inter generateFrom_prod.symm isPiSystem_prod with

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', (∀ s ∈ C, m' s = m s) ∧ ∀ (s : Set α), ‖m' s‖ₑ ≤ μ s

Tactic:
have m'_le : m'.variation ≤ μ' := by
    exact variation_le_of_forall_enorm_le (fun s hs ↦ hm' _)

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 ≤ μ'
⊢ ∃ m', (∀ s ∈ C, m' s = m s) ∧ ∀ (s : Set α), ‖m' s‖ₑ ≤ μ s
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) (univ ×ˢ univ) = ρ (univ ×ˢ univ)

Tactic:
hρ _ _ MeasurableSet.univ MeasurableSet.univ,

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) = (B (μ univ)) (ν univ)
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.SignedMeasure

Goal state before:
pp: case pos
X : Type u_1
mX : MeasurableSpace X
s : SignedMeasure X
i : Set X
hi : MeasurableSet i
⊢ ‖s i‖ ≤ s.totalVariation.real i

Tactic:
rw [s.apply_eq_posPart_real_sub_negPart_real hi, totalVariation, measureReal_add_apply]

Goal state after:
case pos
X : Type u_1
mX : MeasurableSpace X
s : SignedMeasure X
i : Set X
hi : MeasurableSet i
⊢ ‖s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i‖ ≤
    s.toJordanDecomposition.posPart.real i + s.toJordanDecomposition.negPart.real i
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: case mp.zero
M : Type u_1
inst✝ : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x : M
⊢ 0 = 0 ∨ ∃ y ∈ closure (insert a t), a + y = 0

Tactic:
| zero =>

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
⊢ ‖∫ᵛ (a : X), f a ∂[B; μ]‖ₑ ≤ ‖B‖ₑ * ∫⁻ (a : X), ‖f a‖ₑ ∂μ.variation

Tactic:
by
  apply (enorm_setToFun_le _ (by simp)).trans
  gcongr
  simp [← coe_nnnorm]

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
hf : μ.Integrable f
⊢ ‖∫ᵛ (a : X), f a ∂[B; μ]‖ₑ ≤ ∫⁻ (a : X), ‖f a‖ₑ ∂(μ.transpose B).variation

Tactic:
rw [integral_eq_setToFun_transpose hf]

Goal state after:
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
hf : μ.Integrable f
⊢ ‖setToFun (μ.transpose B).variation ⇑(μ.transpose B) ⋯ f‖ₑ ≤ ∫⁻ (a : X), ‖f a‖ₑ ∂(μ.transpose B).variation
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: case inr.mpr.zero
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id ↑{b}
hb : 0 < b
x : ℕ
hx : x ≥ a
heq : a + 0 * b = x + b
⊢ ∃ a_1, a + a_1 * b = x

Tactic:
| zero =>

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

Goal state before:
pp: case inr.mpr
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id ↑{b}
hb : 0 < b
x : ℕ
hx : x ≥ a
y : ℕ
heq : a + y * b = x + b
⊢ ∃ a_1, a + a_1 * b = x

Tactic:
cases y with

Goal state after:
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

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 : M
⊢ ∀ {b : M}, a ∈ {y | x + y ∈ s} → b ∈ {y | x + y ∈ s} → a + b ∈ {y | x + y ∈ s}
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:
| zero =>

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

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

Tactic:
| zero =>

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

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℕ)
hs : IsSlice s
⊢ ∀ (a : ι → ℕ) (t : Finset ι), (∀ x ∈ s, ∀ i ∉ t, x i = a i) → IsSemilinearSet s

Tactic:
intro a

Goal state after:
ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℕ)
hs : IsSlice s
a : ι → ℕ
⊢ ∀ (t : Finset ι), (∀ x ∈ s, ∀ i ∉ t, x i = a i) → IsSemilinearSet s
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
⊢ ⊤.CG ↔ ∃ S, S.Countable ∧ (closure L).toFun S = ⊤

Tactic:
Substructure.cg_def

Goal state after:
L : Language
M : Type u_1
inst✝ : L.Structure M
⊢ (∃ S, S.Countable ∧ (closure L).toFun S = ⊤) ↔ ∃ S, S.Countable ∧ (closure L).toFun S = ⊤
Module: Mathlib.ModelTheory.DirectLimit

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

Tactic:
| zero =>

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

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

Tactic:
| zero =>

Goal state after:
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
⊢ L.IsExtensionPair M N ↔ ∀ (f : L.FGEquiv N M) (m : M), ∃ g, m ∈ (↑g).cod ∧ f ≤ g

Tactic:
by
  refine Iff.intro ?_ ?_ <;>
  · intro h f m
    obtain ⟨g, h1, h2⟩ := h f.symm m
    exact ⟨g.symm, h1, monotone_symm h2⟩

Goal state after:
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
G' : ι → Type w'
inst✝¹ : (i : ι) → L.Structure (G' i)
f' : (i j : ι) → i ≤ j → G' i ↪[L] G' j
g : (i : ι) → G i ≃[L] G' i
inst✝ : DirectedSystem G' fun i j h ↦ ⇑(f' i j h)
H_commuting : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (f' i j hij) ((g i) x)
U : (i : ι) → G i ↪[L] DirectLimit G' f' := fun i ↦ (of L ι G' f' i).comp (g i).toEmbedding
⊢ ∀ (i j : ι) (hij : i ≤ j) (x : G i), (U j) ((f i j hij) x) = (U i) x

Tactic:
intro _ _ _ _

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
G' : ι → Type w'
inst✝¹ : (i : ι) → L.Structure (G' i)
f' : (i j : ι) → i ≤ j → G' i ↪[L] G' j
g : (i : ι) → G i ≃[L] G' i
inst✝ : DirectedSystem G' fun i j h ↦ ⇑(f' i j h)
H_commuting : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (f' i j hij) ((g i) x)
U : (i : ι) → G i ↪[L] DirectLimit G' f' := fun i ↦ (of L ι G' f' i).comp (g i).toEmbedding
i✝ j✝ : ι
hij✝ : i✝ ≤ j✝
x✝ : G i✝
⊢ (U j✝) ((f i✝ j✝ hij✝) x✝) = (U i✝) x✝
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: case refine_2.refine_2
L : Language
ι : Type u_1
inst✝⁵ : Countable ι
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type w
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG L (G i)
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
S : L.Substructure (DirectLimit G f)
hS : ∀ (i : ι), Substructure.map (of L ι G f i).toHom ((Substructure.closure L).toFun (Classical.choose ⋯)) ≤ S
x : DirectLimit G f
a✝ : x ∈ ⊤
out : Quotient (setoid G f) → Σˣ f := Quotient.out
⊢ (of L ι G f (out x).fst).toHom (out x).snd = x

Tactic:
simp only [out, Embedding.coe_toHom, DirectLimit.of_apply, Sigma.eta, Quotient.out_eq]

Goal state after:
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)
⊢ (hs.fract x + ∑ a, if ↑a ∈ hs.periods then (hs.floor x a).toNat • ↑a else 0) = x + ∑ _x, 0

Tactic:
convert! (hs.add_floor_neg_toNat_sum_eq x).symm using 3 with i _ i

Goal state after:
case e'_2.a
ι : 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)
i : ↑hs.basisSet
a✝ : i ∈ Finset.univ
⊢ (if ↑i ∈ hs.periods then (hs.floor x i).toNat • ↑i else 0) = (hs.floor x i).toNat • ↑i

case e'_3.a
ι : 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)
i : ↑hs.basisSet
a✝ : i ∈ Finset.univ
⊢ 0 = (-hs.floor x i).toNat • ↑i
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
⊢ ∀ C ∈ Quotient.mk' '' L.age M, ∃ V, ⟦{ α := ↥↑V, str := inferInstance }⟧ = C

Tactic:
rintro _ ⟨N, ⟨N_fg, ⟨N_incl⟩⟩, N_eq⟩

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
C✝ : Quotient equivSetoid
N : Bundled L.Structure
N_eq : Quotient.mk' N = C✝
N_fg : Structure.FG L ↑N
N_incl : ↑N ↪[L] M
⊢ ∃ V, ⟦{ α := ↥↑V, str := inferInstance }⟧ = C✝
Module: Mathlib.ModelTheory.Graph

Goal state before:
pp: V : Type u
inst✝ : Language.graph.Structure V
⊢ V ⊨ Theory.simpleGraph ↔ (Std.Irrefl fun x y ↦ RelMap adj ![x, y]) ∧ Std.Symm fun x y ↦ RelMap adj ![x, y]

Tactic:
simp [Theory.simpleGraph]

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case mp
L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
M : Bundled L.Structure
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : (closure L).toFun ↑s = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst ∘ out) s, i_1 ≤ i
e' : ↥(DirectLimit.of L ι G f i).toHom.range ↪[L] G i
⊢ e.toHom.range ≤ (DirectLimit.of L ι G f i).toHom.range

Tactic:
← hs,

Goal state after:
case mp
L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
M : Bundled L.Structure
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : (closure L).toFun ↑s = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst ∘ out) s, i_1 ≤ i
e' : ↥(DirectLimit.of L ι G f i).toHom.range ↪[L] G i
⊢ (closure L).toFun ↑s ≤ (DirectLimit.of L ι G f i).toHom.range
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: case h.inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
this✝¹ : ∀ x ∈ Finset.image Prod.snd ({p ∈ ↑f | p.1 < a}), ∀ y ∈ Finset.image Prod.snd ({p ∈ ↑f | a < p.1}), x < y
b : β
hb : (∀ x ∈ Finset.image Prod.snd ({p ∈ ↑f | p.1 < a}), x < b) ∧ ∀ y ∈ Finset.image Prod.snd ({p ∈ ↑f | a < p.1}), b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
this✝ : p1 ≠ a
hl : p1 < a
this : cmp p1 a = Ordering.lt ∧ p2 < b
⊢ cmp (p1, p2).1 a = cmp (p1, p2).2 b

Tactic:
← cmp_eq_lt_iff

Goal state after:
case h.inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
this✝¹ : ∀ x ∈ Finset.image Prod.snd ({p ∈ ↑f | p.1 < a}), ∀ y ∈ Finset.image Prod.snd ({p ∈ ↑f | a < p.1}), x < y
b : β
hb : (∀ x ∈ Finset.image Prod.snd ({p ∈ ↑f | p.1 < a}), x < b) ∧ ∀ y ∈ Finset.image Prod.snd ({p ∈ ↑f | a < p.1}), b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
this✝ : p1 ≠ a
hl : p1 < a
this : cmp p1 a = Ordering.lt ∧ cmp p2 b = Ordering.lt
⊢ cmp (p1, p2).1 a = cmp (p1, p2).2 b
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hP : P.FG
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val '' s₂')
⊢ IsSemilinearSet (Subtype.val '' s₁' \ Subtype.val '' s₂')

Tactic:
rw [← image_sdiff Subtype.val_injective]

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hP : P.FG
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val '' s₂')
⊢ IsSemilinearSet (Subtype.val '' (s₁' \ s₂'))