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

Goal state before:
pp: case hf
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n) μ
x : Fin n → E
h : innerₗ E = ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ)
hint' : ∀ (k : ℕ), ↑k ≤ ↑n → Integrable (fun x ↦ ‖x‖ ^ k * ‖1 x‖) μ
⊢ ContDiff ℝ (↑n) (fourierIntegral Real.fourierChar μ (innerₗ E) 1)

Tactic:
rw [h]
    exact contDiff_fourierIntegral _ hint'

Goal state after:
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
hX : #X < 𝔠
⊢ IsTopologicalBasis {s | IsClopen s}

Tactic:
refine isTopologicalBasis_of_isOpen_of_nhds (fun x s ↦ IsClopen.isOpen s) (fun x s hxs hs ↦ ?_)

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst✝¹] s
⊢ ∃ v ∈ {s | IsClopen s}, x ∈ v ∧ v ⊆ s
Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝⁶ : Group G
inst✝⁵ : AddCommGroup A
inst✝⁴ : DistribMulAction G A
inst✝³ : TopologicalSpace A
inst✝² : IsTopologicalAddGroup A
inst✝¹ : LocallyCompactSpace A
inst✝ : ContinuousConstSMul G A
g✝ : G
this✝ : MeasurableSpace A := borel A
this : BorelSpace A
g g' : G
⊢ (DomMulAct.mk (g * g') • addHaar).addHaarScalarFactor addHaar =
    (DomMulAct.mk g • addHaar).addHaarScalarFactor addHaar * (DomMulAct.mk g' • addHaar).addHaarScalarFactor addHaar

Tactic:
by
      simp_rw [DomMulAct.mk_mul]
      rw [addHaarScalarFactor_eq_mul _ (DomMulAct.mk g' • addHaar (G := A))]
      congr 1
      simp_rw [mul_smul]
      rw [addHaarScalarFactor_domSMul]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝¹⁰ : Group G
inst✝⁹ : AddCommGroup A
inst✝⁸ : DistribMulAction G A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : IsTopologicalAddGroup A
inst✝⁵ : LocallyCompactSpace A
inst✝⁴ : ContinuousConstSMul G A
inst✝³ : MeasurableSpace A
inst✝² : BorelSpace A
μ : Measure A
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : μ.Regular
s : Set A
hs₀ : μ s ≠ 0
hs : μ s ≠ ∞
g : G
⊢ ↑((distribHaarChar A) g) = μ (g • s) / μ s

Tactic:
by
  rw [← distribHaarChar_mul, ENNReal.mul_div_cancel_right] <;> simp [*]

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

Goal state before:
pp: Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
P : ProbabilityMeasure Ω
ε : ℝ
ε_pos : ε > 0
third_ε_pos : 0 < ε / 3
third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)
Es : ℕ → Set Ω
Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)
Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)
Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3
Es_cover : ⋃ n, Es n = univ
Es_disjoint : Pairwise fun n m ↦ Disjoint (Es n) (Es m)
N : ℕ
hN : ↑P (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)
Js_finite : {J | J ⊆ Iio N}.Finite
Gs : Set (Set Ω) := (fun J ↦ thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J | J ⊆ Iio N}
Gs_open :
  ∀ (J : Set ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening (ε / 3) (⋃ j ∈ J, Es j))
mem_nhds_P :
  ∀ (G : Set Ω),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G → {Q | ↑P G < ↑Q G + ENNReal.ofReal (ε / 3)} ∈ 𝓝 P
Q : ProbabilityMeasure Ω
hQ :
  ∀ i ⊆ Iio N,
    ↑P (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) < ↑Q (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) + ENNReal.ofReal (ε / 3)
δ : ℝ
B : Set Ω
δ_gt : 2 * (ε / 3) < δ
x✝ : MeasurableSet B
JB : Set ℕ := {i | (B ∩ Es i).Nonempty ∧ i ∈ Iio N}
this : B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ ⋃ j ∈ Ici N, Es j
ω : Ω
i : ℕ
i_large : N ≤ i
ω_in_Esi : ω ∈ Es i
j : ℕ
j_small : j < N
ω_in_Esj : ω ∈ Es j
⊢ False

Tactic:
exact disjoint_left.mp (Es_disjoint (show j ≠ i by lia)) ω_in_Esj ω_in_Esi

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

Goal state before:
pp: case refine_2.inl
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K) n)
A : ∀ (n : ℕ), IsCompact ((partialSups K) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∈ f
ν : ℕ → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n)).InnerRegular
νK : ∀ (n : ℕ), (ν n) ((partialSups K) n)ᶜ = 0
hν : ∀ (n : ℕ), Tendsto (fun ρ ↦ ρ.restrict (disjointed K n)) (↑f) (𝓝 (ν n))
B : (Measure.sum fun n ↦ ↑(ν n)) univ ≤ ↑C
μ : FiniteMeasure E := ⟨Measure.sum fun n ↦ ↑(ν n), ⋯⟩
L : Tendsto id (↑f) (𝓝 μ)
n : ℕ
h : NormalSpace E
this : (↑μ).InnerRegular
⊢ ∀ (i : E → ℝ), Continuous[inst✝², _] i → EqOn i 0 (K n) → 0 ≤ i → i ≤ 1 → ∫ (x : E), i x ∂↑μ ≤ ↑(u n)

Tactic:
intro g

Goal state after:
case refine_2.inl
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K) n)
A : ∀ (n : ℕ), IsCompact ((partialSups K) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∈ f
ν : ℕ → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n)).InnerRegular
νK : ∀ (n : ℕ), (ν n) ((partialSups K) n)ᶜ = 0
hν : ∀ (n : ℕ), Tendsto (fun ρ ↦ ρ.restrict (disjointed K n)) (↑f) (𝓝 (ν n))
B : (Measure.sum fun n ↦ ↑(ν n)) univ ≤ ↑C
μ : FiniteMeasure E := ⟨Measure.sum fun n ↦ ↑(ν n), ⋯⟩
L : Tendsto id (↑f) (𝓝 μ)
n : ℕ
h : NormalSpace E
this : (↑μ).InnerRegular
g : E → ℝ
⊢ Continuous[inst✝², _] g → EqOn g 0 (K n) → 0 ≤ g → g ≤ 1 → ∫ (x : E), g x ∂↑μ ≤ ↑(u n)
Module: Mathlib.MeasureTheory.Measure.PreVariation

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
P : Finpartition s
hs : MeasurableSet s
hP : ∀ p ∈ P.parts, MeasurableSet p
⊢ ∀ ⦃s t : Set X⦄, MeasurableSet s → MeasurableSet t → MeasurableSet (s ⊔ t)

Tactic:
by measurability

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

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
P : Finpartition s
hs : MeasurableSet s
hP : ∀ p ∈ P.parts, MeasurableSet p
⊢ ∀ ⦃s t : Set X⦄, MeasurableSet s → MeasurableSet t → MeasurableSet (s ⊓ t)

Tactic:
by measurability

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

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
P : Finpartition s
hs : MeasurableSet s
hP : ∀ p ∈ P.parts, MeasurableSet p
⊢ MeasurableSet ⊥

Tactic:
by measurability

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

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
P : Finpartition s
hP : ∀ p ∈ P.parts, MeasurableSet p
⊢ ∀ ⦃s t : Set X⦄, MeasurableSet s → MeasurableSet t → MeasurableSet (s ⊔ t)

Tactic:
by measurability

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

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
P : Finpartition s
hP : ∀ p ∈ P.parts, MeasurableSet p
⊢ ∀ ⦃s t : Set X⦄, MeasurableSet s → MeasurableSet t → MeasurableSet (s ⊓ t)

Tactic:
by measurability

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

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
P : Finpartition s
hP : ∀ p ∈ P.parts, MeasurableSet p
⊢ MeasurableSet ⊥

Tactic:
by measurability

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

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
P : (i : ℕ) → Finpartition ⟨s i, ⋯⟩
n : ℕ
s' : ℕ → Subtype MeasurableSet := fun i ↦ ⟨s i, ⋯⟩
hs_disj : (↑(Finset.range n)).PairwiseDisjoint s'
Q : Finpartition ((Finset.range n).sup fun i ↦ ⟨s i, ⋯⟩) := Finpartition.combine P ⋯
⊢ ∀ ⦃x y : Set X⦄, MeasurableSet x → MeasurableSet y → MeasurableSet (x ⊔ y)

Tactic:
by measurability

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 : ∀ (n : ℕ) (r : ℝ), 0 < r → 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖ ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ),
    0 < r → (μ n).real {x | r < |⟪z, x⟫|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖
h_limsup_le :
  ∀ (r : ℝ),
    0 < r →
      limsup (fun n ↦ (μ n).real {x | r < |⟪z, x⟫|}) atTop ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z)‖
ε : ℝ
hε : ε > 0
hf0 : f 0 = 1
hf_tendsto : ∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε
δ : ℝ
hδ : 0 < δ
hδ_lt : ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε / 4
r : ℝ
hrδ : 4 * δ⁻¹ ≤ r
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
h_le_Ioc : ∀ x ∈ Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹), ‖1 - f (x • z)‖ ≤ ε / 4
⊢ ε / 2 < ε

Tactic:
simp [hε]

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

Goal state before:

Tactic:
μ (s ∆ (t ∩ T N))
          ≤ μ (s \ (s ∩ T N)) + μ ((s ∆ t) ∩ T N) := by
              rw [← symmDiff_of_le (inter_subset_left ..), symmDiff_comm _ s,
                inter_symmDiff_distrib_right]
              exact measure_symmDiff_le _ _ _
        _ < ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2) := by
              apply ENNReal.add_lt_add
              · rw [measure_sdiff
                    (inter_subset_left ..)
                    (ms.inter (hgen ▸ measurableSet_generateFrom (T_mem N))).nullMeasurableSet
                    (ne_top_of_le_ne_top hμs (measure_mono (inter_subset_left ..))),
                  lt_ofReal_iff_toReal_lt (sub_ne_top hμs),
                  toReal_sub_of_le (measure_mono (inter_subset_left ..)) hμs]
                apply lt_of_le_of_lt (sub_le_dist ..)
                nth_rw 1 [← univ_inter s]
                rw [inter_comm s, dist_comm, ← T_spanning, iUnion_inter _ T]
                apply hN N (le_refl _)
              · rwa [← μ.restrict_apply' (hgen ▸ measurableSet_generateFrom (T_mem N))]
        _ = ENNReal.ofReal ε := by
              rw [← ofReal_add (by linarith [ε_pos]) (by linarith [ε_pos]), add_halves]

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_sigma_subadd : m.IsSigmaSubadditive
m_top : ∀ s ∉ C, m s = ∞
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hs_subset : s ⊆ ⋃ i, f i
⊢ m s = m (s ∩ ⋃ i, f i)

Tactic:
rw [inter_eq_self_of_subset_left hs_subset]

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
⊢ (inducedOuterMeasure (fun x x_1 ↦ m x) ⋯ ⋯) s = m s

Tactic:
by
  suffices inducedOuterMeasure (fun x _ ↦ m x) hC.empty_mem addContent_empty s = m.extend hC s by
    rwa [m.extend_eq hC hs] at this
  refine Eq.trans ?_ ((m.extend hC).ofFunction_eq hC ?_ ?_ hs)
  · congr
  · intro f hf hf_mem
    rw [m.extend_eq hC hf_mem]
    refine (m_sigma_subadd hf hf_mem).trans_eq ?_
    congr with i
    rw [m.extend_eq hC (hf i)]
  · exact fun _ ↦ m.extend_eq_top _

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent

Goal state before:
pp: case hs
α : Type u_1
C : Set (Set α)
s : Set α
mα : MeasurableSpace α
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
hC_gen : mα = MeasurableSpace.generateFrom C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
⊢ MeasurableSet s

Tactic:
· rw [hC_gen]
    apply MeasurableSpace.measurableSet_generateFrom hs

Goal state after:
Module: Mathlib.MeasureTheory.SpecificCodomains.Pi

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p : ℝ≥0∞
ι : Type u_2
inst✝¹ : Fintype ι
E : ι → Type u_3
inst✝ : (i : ι) → NormedAddCommGroup (E i)
f : X → (i : ι) → E i
hf : ∀ (i : ι), MemLp (fun x ↦ f x i) p μ
⊢ MemLp f p μ

Tactic:
have : f = ∑ i, (Pi.single i) ∘ (f · i) := by ext; simp
    rw [this]
    refine memLp_finsetSum' _ fun i _ ↦ ?_
    exact (Isometry.single i).lipschitz.comp_memLp (by simp) (hf i)

Goal state after:
Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
q : ℝ≥0∞
inst✝⁴ : Fact (1 ≤ q)
ι : Type u_2
inst✝³ : Fintype ι
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
f : X → PiLp q E
inst✝¹ : (i : ι) → NormedSpace ℝ (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
hf : ∀ (i : ι), Integrable (fun x ↦ (f x).ofLp i) μ
i : ι
⊢ (∫ (x : X), f x ∂μ).ofLp i = ∫ (x : X), (f x).ofLp i ∂μ

Tactic:
rw [← PiLp.proj_apply (𝕜 := ℝ) q E i (∫ x, f x ∂μ), ← ContinuousLinearMap.integral_comp_comm]
  · simp
  exact Integrable.of_eval_piLp hf

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

Goal state before:
pp: 𝓧 : 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))
μ : ProbabilityMeasure 𝓧
hs : μ ∈ S
m : ℕ
⊢ MeasurableSet
    (⋃ i, ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m)))

Tactic:
by measurability

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

Goal state before:
pp: case refine_1
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
s : Set X
hs : MeasurableSet s
h : μ.variation s = 0
t : Set X
hts : t ⊆ s
ht : MeasurableSet t
⊢ ‖μ t‖ₑ ≤ μ.variation s

Tactic:
apply (enorm_measure_le_variation _ _).trans (measure_mono hts)

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)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
B : ∀ (n : ℕ), m (⋃ i, f i) = m (⋃ i ∈ Finset.range n, f i) + m (⋃ i ∈ Set.Ici n, f i)
C : ∀ (n : ℕ), m (⋃ i, f i) - ∑ i ∈ Finset.range n, m (f i) = m (⋃ i ∈ Set.Ici n, f i)
⊢ Filter.Tendsto (fun e ↦ ‖m (⋃ i, f i) - ∑ i ∈ Finset.range e, m (f i)‖ₑ) Filter.atTop (nhds 0)

Tactic:
simp only [C]

Goal state after:
α : 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)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
B : ∀ (n : ℕ), m (⋃ i, f i) = m (⋃ i ∈ Finset.range n, f i) + m (⋃ i ∈ Set.Ici n, f i)
C : ∀ (n : ℕ), m (⋃ i, f i) - ∑ i ∈ Finset.range n, m (f i) = m (⋃ i ∈ Set.Ici n, f i)
⊢ Filter.Tendsto (fun e ↦ ‖m (⋃ i ∈ Set.Ici e, f i)‖ₑ) Filter.atTop (nhds 0)
Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation

Goal state before:
pp: case inr.refine_1.a
α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
h'α : Nonempty α
m : AddContent E {s | ∃ u v, u ≤ v ∧ s = Ioc u v} := AddContent.onIoc (Function.rightLim f)
A : ∀ s ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}, ‖m s‖ₑ ≤ hf.measureAux s
B : hα = generateFrom {s | ∃ u v, u ≤ v ∧ s = Ioc u v}
m' : VectorMeasure α E
hm' : ∀ s ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}, m' s = m s
h'm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ hf.measureAux s
u v : α
huv : u ≤ v
⊢ Ioc u v ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}

Tactic:
· exact ⟨u, v, huv, rfl⟩

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

Tactic:
| insert _ _ ih =>

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

Goal state before:
pp: case pos
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
⊢ (fun s ↦ ∫ᵛ (x : X) in s, f x ∂[B; μ]) = fun s ↦ ∫ᵛ (x : X) in s, g x ∂[B; μ]

Tactic:
ext s

Goal state after:
case pos
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
s : Set X
⊢ ∫ᵛ (x : X) in s, f x ∂[B; μ] = ∫ᵛ (x : X) in s, g x ∂[B; μ]
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:
| insert _ _ ih =>

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

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

Tactic:
| insert _ _ ih =>

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

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

Tactic:
by
  classical
  rw [isLinearSet_iff] at hs
  rcases hs with ⟨a, t, rfl⟩
  induction hn : t.card using Nat.strong_induction_on generalizing a t with | _ n ih
  subst hn
  by_cases hindep : LinearIndepOn ℕ id (t : Set M)
  · exact IsProperLinearSet.isProperSemilinearSet ⟨a, t, by simpa⟩
  rw [not_linearIndepOn_finset_iffₒₛ] at hindep
  rcases hindep with ⟨t', ht', f, heq, i, hi, hfi⟩
  simp only [Function.id_def] at heq
  convert_to IsProperSemilinearSet (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j),
    (a + k • j) +ᵥ (closure (t.erase j : Set M) : Set M))
  · ext x
    simp only [mem_vadd_set, SetLike.mem_coe]
    constructor
    · rintro ⟨y, hy, rfl⟩
      rw [mem_closure_finset] at hy
      rcases hy with ⟨g, -, rfl⟩
      induction hn : g i using Nat.strong_induction_on generalizing g with | _ n ih'
      subst hn
      by_cases! hfg : ∀ j ∈ t', f j ≤ g j
      · convert!
        ih' (g i - f i) (Nat.sub_lt_self hfi (hfg i hi))
          (fun j => if j ∈ t' then g j - f j else g j + f j) (by simp [hi]) using 1
        conv_lhs => rw [← Finset.union_sdiff_of_subset ht']
        simp_rw [vadd_eq_add, add_left_cancel_iff, Finset.sum_union Finset.sdiff_disjoint.symm,
          ite_smul, Finset.sum_ite, Finset.filter_mem_eq_inter, Finset.inter_eq_right.2 ht',
          Finset.filter_notMem_eq_sdiff, add_smul, Finset.sum_add_distrib, ← heq, ← add_assoc,
          add_right_comm, ← Finset.sum_add_distrib]
        congr! 2 with j hj
        rw [← add_smul, tsub_add_cancel_of_le (hfg j hj)]
      · rcases hfg with ⟨j, hj, hgj⟩
        simp only [mem_iUnion, Finset.mem_range, mem_vadd_set, SetLike.mem_coe, vadd_eq_add]
        refine ⟨j, hj, g j, hgj, ∑ k ∈ t.erase j, g k • k,
          sum_mem fun x hx => (nsmul_mem (mem_closure_of_mem hx) _), ?_⟩
        rw [← Finset.sum_erase_add _ _ (ht' hj), ← add_assoc, add_right_comm]
    · simp only [mem_iUnion, Finset.mem_range, mem_vadd_set, SetLike.mem_coe, vadd_eq_add]
      rintro ⟨j, hj, k, hk, y, hy, rfl⟩
      refine ⟨k • j + y,
        add_mem (nsmul_mem (mem_closure_of_mem (ht' hj)) _)
          ((closure_mono (t.erase_subset j)) hy), ?_⟩
      rw [add_assoc]
  · exact .biUnion_finset fun j hj => .biUnion_finset fun k hk =>
      ih _ (Finset.card_lt_card (Finset.erase_ssubset (ht' hj))) _ _ rfl

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

Goal state before:
pp: case inr
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id ↑{b}
hb : 0 < b
x : ℕ
hx : x ≥ a
⊢ x ∈ a +ᵥ ↑(closure ↑{b}) ↔ x + b ∈ a +ᵥ ↑(closure ↑{b})

Tactic:
simp only [Finset.coe_singleton, mem_vadd_set, SetLike.mem_coe,
          AddSubmonoid.mem_closure_singleton, smul_eq_mul, vadd_eq_add, exists_exists_eq_and]

Goal state after:
case inr
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id ↑{b}
hb : 0 < b
x : ℕ
hx : x ≥ a
⊢ (∃ a_1, a + a_1 * b = x) ↔ ∃ a_1, a + a_1 * b = x + b
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: α : Type u_1
A : Set ℕ
inst✝ : Finite α
v : α → ℕ
t : Finset (α → ℕ)
x : α → ℕ
⊢ (∃ a, v + ∑ i ∈ t.attach, ↑(a i) * ↑i = x) ↔ ∃ i, ∀ (b : α), x b = v b + ∑ i_1 ∈ t.attach, ↑i_1 b * i i_1

Tactic:
congr! with a

Goal state after:
α : Type u_1
A : Set ℕ
inst✝ : Finite α
v : α → ℕ
t : Finset (α → ℕ)
x : α → ℕ
a : ↥t → ℕ
⊢ v + ∑ i ∈ t.attach, ↑(a i) * ↑i = x ↔ ∀ (b : α), x b = v b + ∑ i ∈ t.attach, ↑i b * a i
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
v : α → ℕ
⊢ (Structure.funMap (Sum.inl presburgerFunc.zero) fun i ↦ Term.realize v (ts i)) = 0 + 0 ⬝ᵥ v

Tactic:
rw [withConstants_funMap_sumInl]

Goal state after:
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
v : α → ℕ
⊢ (Structure.funMap presburgerFunc.zero fun i ↦ Term.realize v (ts i)) = 0 + 0 ⬝ᵥ v