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

Goal state before:
pp: case refine_2.inl
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝² : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜✝ : Set (Set X)
inst✝¹ : CountablyGenerated X
inst✝ : SFinite μ
this✝¹ : IsSeparable (μ.restrict μ.sigmaFiniteSet)
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : (μ.restrict μ.sigmaFiniteSet).MeasureDense 𝒜
ℬ : Set (Set X) := {x | ∃ s ∈ 𝒜, s ∩ μ.sigmaFiniteSet = x}
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
hs : (μ.restrict μ.sigmaFiniteSetᶜ) s = 0
this✝ : (μ.restrict μ.sigmaFiniteSet) s ≠ ∞
t : Set X
t_mem : t ∈ 𝒜
ht : (μ.restrict μ.sigmaFiniteSet) (s ∆ t) < ENNReal.ofReal ε
this : μ (s ∆ (t ∩ μ.sigmaFiniteSet) \ μ.sigmaFiniteSet) = 0
⊢ μ ((s ∩ μ.sigmaFiniteSet) ∆ (t ∩ (μ.sigmaFiniteSet ∩ μ.sigmaFiniteSet))) < ENNReal.ofReal ε

Tactic:
inter_self,

Goal state after:
case refine_2.inl
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝² : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜✝ : Set (Set X)
inst✝¹ : CountablyGenerated X
inst✝ : SFinite μ
this✝¹ : IsSeparable (μ.restrict μ.sigmaFiniteSet)
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : (μ.restrict μ.sigmaFiniteSet).MeasureDense 𝒜
ℬ : Set (Set X) := {x | ∃ s ∈ 𝒜, s ∩ μ.sigmaFiniteSet = x}
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
hs : (μ.restrict μ.sigmaFiniteSetᶜ) s = 0
this✝ : (μ.restrict μ.sigmaFiniteSet) s ≠ ∞
t : Set X
t_mem : t ∈ 𝒜
ht : (μ.restrict μ.sigmaFiniteSet) (s ∆ t) < ENNReal.ofReal ε
this : μ (s ∆ (t ∩ μ.sigmaFiniteSet) \ μ.sigmaFiniteSet) = 0
⊢ μ ((s ∩ μ.sigmaFiniteSet) ∆ (t ∩ μ.sigmaFiniteSet)) < ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝² : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜✝ : Set (Set X)
inst✝¹ : IsSeparable μ
inst✝ : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
𝒜₀ : Set (Set X) := {s | s ∈ 𝒜 ∧ μ s ≠ ∞}
h𝒜₀ : μ.MeasureDense 𝒜₀
count_𝒜₀ : 𝒜₀.Countable
p_ne_zero : p ≠ 0
u : Set E
countable_u : u.Countable
dense_u : Dense u
key : (n : ℕ) → (Fin n → ↑u) → (Fin n → ↑𝒜₀) → ↥(Lp E p μ) := fun n d s ↦ ∑ i, indicatorConstLp p ⋯ ⋯ ↑(d i)
D : Set ↥(Lp E p μ) := {s | ∃ n d t, s = key n d t}
f g : X → E
hf : MemLp f p μ
hg : MemLp g p μ
f_mem : ∀ (ε : ℝ), 0 < ε → ∃ b ∈ D, ‖MemLp.toLp f hf - b‖ < ε
g_mem : ∀ (ε : ℝ), 0 < ε → ∃ b ∈ D, ‖MemLp.toLp g hg - b‖ < ε
ε : ℝ
ε_pos : 0 < ε
bf : ↥(Lp E p μ)
hbf : ‖MemLp.toLp f hf - bf‖ < ε / 2
nf : ℕ
df : Fin nf → ↑u
sf : Fin nf → ↑𝒜₀
bf_eq : bf = key nf df sf
bg : ↥(Lp E p μ)
hbg : ‖MemLp.toLp g hg - bg‖ < ε / 2
ng : ℕ
dg : Fin ng → ↑u
sg : Fin ng → ↑𝒜₀
bg_eq : bg = key ng dg sg
d : Fin (nf + ng) → ↑u := fun i ↦ if h : ↑i < nf then df (i.castLT h) else dg (Fin.subNat nf (Fin.cast ⋯ i) ⋯)
s : Fin (nf + ng) → ↑𝒜₀ := fun i ↦ if h : ↑i < nf then sf (i.castLT h) else sg (Fin.subNat nf (Fin.cast ⋯ i) ⋯)
⊢ ‖MemLp.toLp f hf - bf‖ + ‖MemLp.toLp g hg - bg‖ < ε

Tactic:
linarith [hbf, hbg]

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

Goal state before:
pp: case neg
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
E : Set X
hE : MeasurableSet E
hE' : ¬⟨E, hE⟩ = ⊥
⊢ ‖μ E‖ₑ ≤ preVariationFun (fun x ↦ ‖μ x‖ₑ) E

Tactic:
calc
    ‖μ E‖ₑ = ∑ p ∈ (Finpartition.indiscrete hE').parts, ‖μ p‖ₑ := by simp
    _ ≤ preVariationFun (‖μ ·‖ₑ) E := by apply preVariation.sum_le

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: case inr.inr
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝³ : PseudoMetricSpace 𝓧
inst✝² : OpensMeasurableSpace 𝓧
inst✝¹ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
inst✝ : CompleteSpace 𝓧
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
hnonempty : Nonempty 𝓧
D : ℕ → 𝓧
hD : DenseRange D
u : ℕ → ℝ
hu_anti : StrictAnti u
hu_pos : ∀ (n : ℕ), 0 < u n
hu : Tendsto u atTop (𝓝 0)
hcov : ∀ (m : ℕ), ⋃ i, ball (D i) (u m) = univ
ε : ℝ≥0∞
εpos : 0 < ε
hεbound : ε ≤ 1
km : ℕ → ℕ
hbound : ∀ (m : ℕ), ∀ μ ∈ S, 1 - ε * 2 ^ (-↑m) < ↑(μ (⋃ i, ⋃ (_ : i ≤ km m), ball (D i) (u m)))
⊢ ∃ K, IsCompact K ∧ ∀ μ ∈ {x | ∃ μ ∈ S, ↑μ = x}, μ Kᶜ ≤ ε

Tactic:
let bigK := ⋂ m, ⋃ (i ≤ km (m + 1)), closure (ball (D i) (u m))

Goal state after:
case inr.inr
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝³ : PseudoMetricSpace 𝓧
inst✝² : OpensMeasurableSpace 𝓧
inst✝¹ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
inst✝ : CompleteSpace 𝓧
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
hnonempty : Nonempty 𝓧
D : ℕ → 𝓧
hD : DenseRange D
u : ℕ → ℝ
hu_anti : StrictAnti u
hu_pos : ∀ (n : ℕ), 0 < u n
hu : Tendsto u atTop (𝓝 0)
hcov : ∀ (m : ℕ), ⋃ i, ball (D i) (u m) = univ
ε : ℝ≥0∞
εpos : 0 < ε
hεbound : ε ≤ 1
km : ℕ → ℕ
hbound : ∀ (m : ℕ), ∀ μ ∈ S, 1 - ε * 2 ^ (-↑m) < ↑(μ (⋃ i, ⋃ (_ : i ≤ km m), ball (D i) (u m)))
bigK : Set 𝓧 :=
  ⋂ m, ⋃ i, ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m))
⊢ ∃ K, IsCompact K ∧ ∀ μ ∈ {x | ∃ μ ∈ S, ↑μ = x}, μ Kᶜ ≤ ε
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Goal state before:
pp: X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝³ : TopologicalSpace V
inst✝² : ENormedAddCommMonoid V
inst✝¹ : T2Space V
μ ν : VectorMeasure X V
inst✝ : ContinuousAdd V
E : Set X
x✝ : MeasurableSet E
⊢ ‖μ E‖ₑ + ‖ν E‖ₑ ≤ μ.variation E + ν.variation E

Tactic:
by
      gcongr <;> exact enorm_measure_le_variation _ E

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 α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ μ s
inst✝ : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
n : ℕ
⊢ m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)

Tactic:
induction n with
      | zero => simpa using h'm ∅ ∅ MeasurableSet.empty MeasurableSet.empty (by simp)
      | succ n ih =>
        simp only [Finset.range_add_one]
        rw [Finset.sum_insert (by simp)]
        simp only [Finset.mem_insert, Set.iUnion_iUnion_eq_or_left]
        rw [h'm _ _ (f_meas n), ih]
        · exact Finset.measurableSet_biUnion _ (fun i hi ↦ f_meas i)
        · simp only [Finset.mem_range, Set.disjoint_iUnion_right]
          intro i hi
          exact f_disj hi.ne'

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

Goal state before:
pp: 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 t : Set X
hs : MeasurableSet s
ht : MeasurableSet t
hf : μ.IntegrableOn f s
h'f : μ.IntegrableOn f t
⊢ (μ.restrict (s ∪ t)).variation ≤ (μ.restrict s).variation + (μ.restrict t).variation

Tactic:
grw [variation_restrict_le, Measure.restrict_union_le]

Goal state after:
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 t : Set X
hs : MeasurableSet s
ht : MeasurableSet t
hf : μ.IntegrableOn f s
h'f : μ.IntegrableOn f t
⊢ μ.variation.restrict s + μ.variation.restrict t ≤ (μ.restrict s).variation + (μ.restrict t).variation
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
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
hst : s =ᵐ[μ.variation] t
x : X
hx : s x = t x
⊢ x ∈ s ↔ x ∈ t

Tactic:
simpa using! hx

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
hts : s ⊆ t
h't : ∀ x ∈ t \ s, f x = 0
⊢ ∀ᵐ (x : X) ∂μ.variation, x ∈ t \ s → f x = 0

Tactic:
filter_upwards with x using h't x

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
s : Set X
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace ℝ F
inst✝² : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
inst✝¹ : CompleteSpace G
inst✝ : IsFiniteMeasure (μ.variation.restrict s)
c : E
⊢ ∫ᵛ (x : X) in s, c ∂[B; μ] = (B c) (μ s)

Tactic:
by
  by_cases hs : MeasurableSet s
  · have : IsFiniteMeasure (μ.restrict s).variation := by
      rwa [variation_restrict hs]
    rw [integral_const, restrict_apply _ hs MeasurableSet.univ, univ_inter]
  · simp [setIntegral_eq_zero_of_not_measurableSet hs, μ.not_measurable hs]

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

Goal state before:
pp: case h''m
α : 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 μ) := ⋯
C'C : ∀ s ∈ C', ↑s ∈ C
C'_dense : Dense C'
m₀ : ↑C' → E := ⋯
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := ⋯
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ μ ↑s
hAddit : ∀ (s t : MeasuredSets μ), Disjoint ↑s ↑t → m₁ ⟨↑s ∪ ↑t, ⋯⟩ = m₁ s + m₁ t
m' : Set α → E := ⋯
⊢ ∀ (s : Set α), ¬MeasurableSet s → m' s = 0

Tactic:
· intro s hs
      simp [m', hs]

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

Goal state before:
pp: X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
s : Set X
⊢ μ.semivariation s ≤ ↑μ.bound

Tactic:
apply (semivariation_mono (subset_univ _)).trans_eq
  simp only [VectorMeasure.bound]
  rw [ENNReal.coe_toNNReal semivariation_univ_lt_top.ne]

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
H : Type u_6
mX : MeasurableSpace X
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedAddCommGroup H
μ : VectorMeasure X F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace ℝ G
inst✝ : NormedSpace ℝ H
B : E →L[ℝ] F →L[ℝ] G
f : X → H
C : H →L[ℝ] E
hf : Integrable f μ.variation
⊢ ∫ᵛ (y : X), C (f y) ∂[B; μ] = ∫ᵛ (y : X), f y ∂[B ∘SL C; μ]

Tactic:
by_cases hG : CompleteSpace G; swap
  · simp [integral_of_not_completeSpace hG]
  apply hf.induction (P := fun f ↦ ∫ᵛ y, C (f y) ∂[B; μ] = ∫ᵛ y, f y ∂[B ∘L C; μ])
  · intro c s hs hc
    have : IsFiniteMeasure (μ.variation.restrict s) := ⟨by simpa⟩
    rw [integral_indicator_const _ hs]
    have : (fun y ↦ C (s.indicator (fun x ↦ c) y)) = s.indicator (fun x ↦ C c) := by
      ext; simp only [indicator]; grind
    simp_rw [this]
    rw [integral_indicator_const _ hs]
    rfl
  · intro f g _ f_int g_int hf hg
    simp only [Pi.add_apply, _root_.map_add]
    rw [integral_fun_add (C.integrable_comp f_int) (C.integrable_comp g_int), hf, hg,
      integral_fun_add f_int g_int]
  · apply isClosed_eq
    · have I (f : Lp H 1 μ.variation) : ∫ᵛ x, C (f x) ∂[B; μ] = ∫ᵛ x, (C.compLp f) x ∂[B; μ] :=
        (integral_congr_ae (coeFn_compLp _ _)).symm
      simp_rw [I]
      exact continuous_integral.comp (C.compLpL 1 μ.variation).continuous
    · exact continuous_integral
  · intro f g hfg _ hf
    have : ∀ᵐ x ∂μ.variation, C (f x) = C (g x) := by
      filter_upwards [hfg] with x hx using by simp [hx]
    rw [← integral_congr_ae hfg, ← integral_congr_ae this, hf]

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

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
inst✝⁶ : MeasurableSpace Y
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
φ : X → Y
⊢ (μ.map φ).transpose B = (μ.transpose B).map φ

Tactic:
by
  by_cases hφ : Measurable φ; swap
  · simp [map, hφ]
  ext s hs
  simp [transpose, map_apply, hs, hφ]

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

Goal state before:
pp: case mp.add
M : Type u_1
inst✝ : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x✝ x y : M
hx✝ : x ∈ closure (a +ᵥ ↑(closure t))
hy✝ : y ∈ closure (a +ᵥ ↑(closure t))
ih₁ : x = 0 ∨ ∃ y ∈ closure (insert a t), a + y = x
ih₂ : y = 0 ∨ ∃ y_1 ∈ closure (insert a t), a + y_1 = y
⊢ x + y = 0 ∨ ∃ y_1 ∈ closure (insert a t), a + y_1 = x + y

Tactic:
| add x y _ _ ih₁ ih₂ =>

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

Goal state before:
pp: case mp.refine_1
S : Finset (Set ℕ)
k p : Set ℕ → ℕ
hS : ∀ t ∈ S, p t > 0
hS' : ∀ t ∈ S, ∀ x ≥ k t, x ∈ t ↔ x + p t ∈ t
⊢ S.lcm p > 0

Tactic:
grind [Finset.lcm_eq_zero_iff]

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
f : M → AddSubmonoid M :=
  fun x ↦ if hx : x ∈ s then { carrier := {y | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
⊢ ∃ x ∈ s, IsSemilinearSet {y | y ∈ s ∧ x ≤ y}

Tactic:
have hf : ∀ x ∈ s, ∀ y, y ∈ f x ↔ x + y ∈ s := by simp_all [f]

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
f : M → AddSubmonoid M :=
  fun x ↦ if hx : x ∈ s then { carrier := {y | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
⊢ ∃ x ∈ s, IsSemilinearSet {y | y ∈ s ∧ 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)
n : ℕ
F : L.Functions n
x : Fin n → Σˣ f
i j : ι
hi : i ∈ upperBounds (range (Sigma.fst ∘ x))
hj : j ∈ upperBounds (range (Sigma.fst ∘ x))
⊢ Structure.Sigma.mk f i (funMap F (unify f x i hi)) ≈ Structure.Sigma.mk f j (funMap F (unify f x j hj))

Tactic:
by
  obtain ⟨k, ik, jk⟩ := directed_of (· ≤ ·) i j
  refine ⟨k, ik, jk, ?_⟩
  rw [(f i k ik).map_fun, (f j k jk).map_fun, comp_unify, comp_unify]

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

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

Tactic:
refine ⟨fun h => ?_, congr_arg toRatVec⟩
  ext i
  simpa [toRatVec] using congr_fun h i

Goal state after:
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case refl.refl
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
equiv_f : ↥g.1 ≃[L] ↥g.2
le_fg : { dom := g.1, cod := g.2, toEquiv := equiv_f } ≤ g
le_gf : g ≤ { dom := g.1, cod := g.2, toEquiv := equiv_f }
⊢ { dom := g.1, cod := g.2, toEquiv := equiv_f } = g

Tactic:
convert! rfl

Goal state after:
case e'_3.e'_8
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
equiv_f : ↥g.1 ≃[L] ↥g.2
le_fg : { dom := g.1, cod := g.2, toEquiv := equiv_f } ≤ g
le_gf : g ≤ { dom := g.1, cod := g.2, toEquiv := equiv_f }
e_6✝ : g.dom ≍ g.1
e_7✝ : g.cod ≍ g.2
⊢ g.toEquiv = equiv_f
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
this : Fintype ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain
i : ↑hs.basisSet
hi : i ∈ Finset.univ
⊢ (hs.basis.repr (toRatVec x - toRatVec hs.base)) i • hs.basis i ≤ toRatVec ↑i

Tactic:
← hs.basis_apply i

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
this : Fintype ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain
i : ↑hs.basisSet
hi : i ∈ Finset.univ
⊢ (hs.basis.repr (toRatVec x - toRatVec hs.base)) i • hs.basis i ≤ hs.basis i
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
X : Set M
X_count : X.Countable
X_gen : (closure L).toFun X = ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : (closure L).toFun Y = ⊤
x✝⁴ : Countable ↑X
x✝³ : Encodable ↑X
x✝² : Countable ↑Y
x✝¹ : Encodable ↑Y
D : ↑X ⊕ ↑Y → Order.Cofinal (L.FGEquiv M N) :=
  fun p ↦ Sum.recOn p (fun x ↦ ext_dom.definedAtLeft ↑x) fun y ↦ ext_cod.definedAtRight ↑y
S : ℕ →o M ≃ₚ[L] N := { toFun := Subtype.val ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
x✝ : X ⊆ ↑F.dom
⊢ Y ⊆ ↑F.cod

Tactic:
intro y

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
X : Set M
X_count : X.Countable
X_gen : (closure L).toFun X = ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : (closure L).toFun Y = ⊤
x✝⁴ : Countable ↑X
x✝³ : Encodable ↑X
x✝² : Countable ↑Y
x✝¹ : Encodable ↑Y
D : ↑X ⊕ ↑Y → Order.Cofinal (L.FGEquiv M N) :=
  fun p ↦ Sum.recOn p (fun x ↦ ext_dom.definedAtLeft ↑x) fun y ↦ ext_cod.definedAtRight ↑y
S : ℕ →o M ≃ₚ[L] N := { toFun := Subtype.val ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
x✝ : X ⊆ ↑F.dom
y : N
⊢ y ∈ Y → y ∈ ↑F.cod
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

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

Tactic:
rw [lintegral_biUnion_finset]
      · rintro ⟨i, p⟩ hi ⟨j, q⟩ hj hijpq
        simp only [Finset.coe_sigma, SimpleFunc.coe_range, mem_sigma_iff, mem_range,
          SetLike.mem_coe] at hi hj
        rcases eq_or_ne i j with rfl | hij
        · simp only [ne_eq, Sigma.mk.injEq, heq_eq_eq, true_and] at hijpq
          exact Pdisj i hi.2 hj.2 hijpq
        · have : Disjoint (g ⁻¹' {i}) (g ⁻¹' {j}) := by grind
          exact this.mono (Pg i p hi.2) (Pg j q hj.2)
      · rintro ⟨i, p⟩ hip
        simp only [Finset.mem_sigma, SimpleFunc.mem_range, mem_range] at hip
        exact Pmeas i p hip.2

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

Goal state before:
pp: case mpr.refine_1
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
y : ι → ℕ
hy : y ∈ closure {↑i}
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
heq : hs.fract (x + ↑i + y + z') = hs.fract (hs.base + z)
⊢ hs.fract x = hs.base

Tactic:
hs.fract_add_of_mem_closure (closure_mono sdiff_subset hz'),

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

Goal state before:
pp: case mpr.refine_1
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
y : ι → ℕ
hy : y ∈ closure {↑i}
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
heq : x + ↑i + y + z' = hs.base + z
⊢ hs.fract x = hs.base

Tactic:
apply congr_arg hs.fract at heq
        rwa [hs.fract_add_of_mem_closure (closure_mono sdiff_subset hz'),
          hs.fract_add_of_mem_closure (closure_mono (singleton_subset_iff.2 i.2) hy),
          hs.fract_add_of_mem_closure (mem_closure_of_mem i.2),
          hs.fract_add_of_mem_closure (closure_mono sdiff_subset hz), hs.fract_base] at heq

Goal state after: