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

Goal state before:
pp: ι : Type u_1
T : Type u_4
X : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
inst✝⁸ : (i : ι) → TopologicalSpace (X i)
inst✝⁷ : ∀ (i : ι), BorelSpace (X i)
inst✝⁶ : ∀ (i : ι), HasOuterApproxClosed (X i)
mT : MeasurableSpace T
inst✝⁵ : TopologicalSpace T
inst✝⁴ : BorelSpace T
inst✝³ : HasOuterApproxClosed T
inst✝² : Fintype ι
μ ν : Measure (((i : ι) → X i) × T)
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ) (g : T →ᵇ ℝ),
    ∫ (p : ((i : ι) → X i) × T), (∏ i, (f i) (p.1 i)) * g p.2 ∂μ =
      ∫ (p : ((i : ι) → X i) × T), (∏ i, (f i) (p.1 i)) * g p.2 ∂ν
⊢ μ = ν

Tactic:
let e : ((Π i, X i) × T) ≃ᵐ ((Π i, X i) × (Unit → T)) :=
    { toFun p := ⟨fun i ↦ p.1 i, fun _ ↦ p.2⟩
      invFun p := ⟨fun i ↦ p.1 i, p.2 ()⟩
      left_inv p := by simp
      right_inv p := by simp }

Goal state after:
ι : Type u_1
T : Type u_4
X : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
inst✝⁸ : (i : ι) → TopologicalSpace (X i)
inst✝⁷ : ∀ (i : ι), BorelSpace (X i)
inst✝⁶ : ∀ (i : ι), HasOuterApproxClosed (X i)
mT : MeasurableSpace T
inst✝⁵ : TopologicalSpace T
inst✝⁴ : BorelSpace T
inst✝³ : HasOuterApproxClosed T
inst✝² : Fintype ι
μ ν : Measure (((i : ι) → X i) × T)
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ) (g : T →ᵇ ℝ),
    ∫ (p : ((i : ι) → X i) × T), (∏ i, (f i) (p.1 i)) * g p.2 ∂μ =
      ∫ (p : ((i : ι) → X i) × T), (∏ i, (f i) (p.1 i)) * g p.2 ∂ν
e : ((i : ι) → X i) × T ≃ᵐ ((i : ι) → X i) × (Unit → T) :=
  { toFun := fun p ↦ (fun i ↦ p.1 i, fun x ↦ p.2), invFun := fun p ↦ (fun i ↦ p.1 i, p.2 ()), left_inv := ⋯,
    right_inv := ⋯, measurable_toFun := ⋯, measurable_invFun := ⋯ }
⊢ μ = ν
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)
h𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : μ t ≠ ∞
hμst : μ (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
⊢ ‖c‖ * ((ε / ‖c‖) ^ p.toReal) ^ (1 / p.toReal) = ε

Tactic:
one_div,

Goal state after:
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)
h𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : μ t ≠ ∞
hμst : μ (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
⊢ ‖c‖ * ((ε / ‖c‖) ^ p.toReal) ^ p.toReal⁻¹ = ε
Module: Mathlib.MeasureTheory.Measure.LevyConvergence

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
ι : Type u_2
𝓕 : Filter ι
μ₀ : ProbabilityMeasure E
μ : ι → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun n ↦ charFun (↑(μ n)) t) 𝓕 (𝓝 (charFun (↑μ₀) t))
g : E →ᵇ ℂ
hg : g ∈ charPoly continuous_probChar ⋯
⊢ Tendsto (fun n ↦ ∫ (x : E), g x ∂↑(μ n)) 𝓕 (𝓝 (∫ (x : E), g x ∂↑μ₀))

Tactic:
by
  rw [mem_charPoly] at hg
  obtain ⟨w, hw⟩ := hg
  have h_eq (μ : Measure E) (hμ : IsProbabilityMeasure μ) :
      ∫ x, g x ∂μ = w.coeff.sum (fun a z ↦ z * ∫ x, (probChar (innerₗ E x a) : ℂ) ∂μ) := by
    simp_rw [hw, Finsupp.sum]
    rw [integral_finsetSum]
    · congr with y
      rw [integral_const_mul]
    · refine fun i hi ↦ Integrable.const_mul ?_ _
      change Integrable (innerProbChar i) μ
      exact BoundedContinuousFunction.integrable μ _
  simp_rw [h_eq (μ _), h_eq μ₀]
  refine tendsto_finsetSum _ fun y hy ↦ Tendsto.const_mul _ ?_
  simpa [← charFun_eq_integral_probChar] using h y

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
⊢ IsFiniteMeasure μ.toFiniteAux

Tactic:
rw [Measure.toFiniteAux]
  split_ifs
  · assumption
  · exact (exists_isFiniteMeasure_absolutelyContinuous μ).choose_spec.1

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

Goal state before:
pp: E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet {x | ∃ μ ∈ S, ↑μ = x}
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
n : ℕ
K : Set E
K_comp : IsCompact K
hK : ∀ μ ∈ {x | ∃ μ ∈ S, ↑μ = x}, μ Kᶜ ≤ ↑(u n)
μ : ProbabilityMeasure E
hμ : μ ∈ S
⊢ μ Kᶜ ≤ u n

Tactic:
have : (μ : Measure E) Kᶜ ≤ u n := hK _ ⟨μ, hμ, rfl⟩

Goal state after:
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet {x | ∃ μ ∈ S, ↑μ = x}
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
n : ℕ
K : Set E
K_comp : IsCompact K
hK : ∀ μ ∈ {x | ∃ μ ∈ S, ↑μ = x}, μ Kᶜ ≤ ↑(u n)
μ : ProbabilityMeasure E
hμ : μ ∈ S
this : ↑μ Kᶜ ≤ ↑(u n)
⊢ μ Kᶜ ≤ u n
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: case neg.inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsZeroOneMeasure μ
inst✝¹ : StandardBorelSpace α
inst✝ : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep : ∀ x ∈ univ, ∀ y ∈ univ, (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : ℕ → Set α := fun n ↦ if h : μ (A n) = 1 then A n else (A n)ᶜ
mBn : MeasurableSet (⋂ n, B n)
n : ℕ
h : ¬μ (A n) = 1
h₀ : μ (A n) = 0
⊢ μ (A n) = 0

Tactic:
exact h₀

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

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : IsSetAlgebra 𝒜
S : μ.FiniteSpanningSetsIn 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
T : ℕ → Set X := accumulate S.set
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), μ (T n) < ∞
T_spanning : ⋃ n, T n = univ
mono : Monotone fun n ↦ T n ∩ s
this✝ : Filter.Tendsto (fun n ↦ ((⇑μ ∘ fun n ↦ T n ∩ s) n).toReal) Filter.atTop (nhds (μ (⋃ n, T n ∩ s)).toReal)
N : ℕ
hN : ∀ n ≥ N, dist ((⇑μ ∘ fun n ↦ T n ∩ s) n).toReal (μ (⋃ n, T n ∩ s)).toReal < ε / 2
this : Fact (μ (T N) < ∞)
t : Set X
t_mem : t ∈ 𝒜
ht : (μ.restrict (T N)) (s ∆ t) < ENNReal.ofReal (ε / 2)
⊢ ∃ t ∈ 𝒜, μ (s ∆ t) < ENNReal.ofReal ε

Tactic:
refine ⟨t ∩ T N, h𝒜.inter_mem t_mem (T_mem N), ?_⟩

Goal state after:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : IsSetAlgebra 𝒜
S : μ.FiniteSpanningSetsIn 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
T : ℕ → Set X := accumulate S.set
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), μ (T n) < ∞
T_spanning : ⋃ n, T n = univ
mono : Monotone fun n ↦ T n ∩ s
this✝ : Filter.Tendsto (fun n ↦ ((⇑μ ∘ fun n ↦ T n ∩ s) n).toReal) Filter.atTop (nhds (μ (⋃ n, T n ∩ s)).toReal)
N : ℕ
hN : ∀ n ≥ N, dist ((⇑μ ∘ fun n ↦ T n ∩ s) n).toReal (μ (⋃ n, T n ∩ s)).toReal < ε / 2
this : Fact (μ (T N) < ∞)
t : Set X
t_mem : t ∈ 𝒜
ht : (μ.restrict (T N)) (s ∆ t) < ENNReal.ofReal (ε / 2)
⊢ μ (s ∆ (t ∩ T N)) < ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.Order.UpperLower

Goal state before:
pp: case h
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ
H : Tendsto (fun r ↦ volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
⊢ closedBall (f (ε n) ⋯) (ε n / 4) ⊆ (closure s)ᶜ

Tactic:
← interior_compl

Goal state after:
case h
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ
H : Tendsto (fun r ↦ volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
⊢ closedBall (f (ε n) ⋯) (ε n / 4) ⊆ interior sᶜ
Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent

Goal state before:
pp: case refine_2
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_top : ∀ s ∉ C, m s = ∞
hs : s ∈ C
t : Set α
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_subset : t ⊆ ⋃ i, f i
A : ℕ → Finset (Set α) := fun i ↦ hC.disjointOfDiff ⋯ ⋯
h_m_eq : ∀ (i : ℕ), m (f i) = m (f i ∩ s) + ∑ u ∈ A i, m u
i : ℕ
h_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃ i_1 ∈ ↑(A i), i_1
⊢ (OuterMeasure.ofFunction ⇑m ⋯) (⋃ i_1 ∈ ↑(A i), i_1) ≤ ∑ u ∈ hC.disjointOfDiff ⋯ ⋯, m u

Tactic:
obtain h6 := MeasureTheory.measure_biUnion_finset_le
      (μ := OuterMeasure.ofFunction m addContent_empty) (A i) id

Goal state after:
case refine_2
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_top : ∀ s ∉ C, m s = ∞
hs : s ∈ C
t : Set α
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_subset : t ⊆ ⋃ i, f i
A : ℕ → Finset (Set α) := fun i ↦ hC.disjointOfDiff ⋯ ⋯
h_m_eq : ∀ (i : ℕ), m (f i) = m (f i ∩ s) + ∑ u ∈ A i, m u
i : ℕ
h_diff_eq_sUnion : ∀ (i : ℕ), f i \ s = ⋃ i_1 ∈ ↑(A i), i_1
h6 : (OuterMeasure.ofFunction ⇑m ⋯) (⋃ i_1 ∈ A i, id i_1) ≤ ∑ i ∈ A i, (OuterMeasure.ofFunction ⇑m ⋯) (id i)
⊢ (OuterMeasure.ofFunction ⇑m ⋯) (⋃ i_1 ∈ ↑(A i), i_1) ≤ ∑ u ∈ hC.disjointOfDiff ⋯ ⋯, m u
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✝¹ : CountablyGenerated X
inst✝ : SFinite μ
⊢ ∃ 𝒜, 𝒜.Countable ∧ μ.MeasureDense 𝒜

Tactic:
have := isSeparable_of_sigmaFinite (μ.restrict μ.sigmaFiniteSet)
    rcases exists_countable_measureDense (μ.restrict μ.sigmaFiniteSet) with ⟨𝒜, count_𝒜, h𝒜⟩
    let ℬ := {s ∩ μ.sigmaFiniteSet | s ∈ 𝒜}
    refine ⟨ℬ, count_𝒜.image (fun s ↦ s ∩ μ.sigmaFiniteSet), ?_, ?_⟩
    · rintro - ⟨s, s_mem, rfl⟩
      exact (h𝒜.measurable s s_mem).inter measurableSet_sigmaFiniteSet
    · intro s ms hμs ε ε_pos
      rcases restrict_compl_sigmaFiniteSet_eq_zero_or_top μ s with hs | hs
      · have : (μ.restrict μ.sigmaFiniteSet) s ≠ ∞ :=
          ne_top_of_le_ne_top hμs <| μ.restrict_le_self _
        rcases h𝒜.approx s ms this ε ε_pos with ⟨t, t_mem, ht⟩
        refine ⟨t ∩ μ.sigmaFiniteSet, ⟨t, t_mem, rfl⟩, ?_⟩
        have : μ (s ∆ (t ∩ μ.sigmaFiniteSet) \ μ.sigmaFiniteSet) = 0 := by
          rw [sdiff_eq_compl_inter, inter_symmDiff_distrib_left, ← ENNReal.bot_eq_zero, eq_bot_iff]
          calc
            μ ((μ.sigmaFiniteSetᶜ ∩ s) ∆ (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet)))
              ≤ μ ((μ.sigmaFiniteSetᶜ ∩ s) ∪ (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet))) :=
                measure_mono symmDiff_subset_union
            _ ≤ μ (μ.sigmaFiniteSetᶜ ∩ s) + μ (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet)) :=
                measure_union_le _ _
            _ = 0 := by
                rw [inter_comm, ← μ.restrict_apply ms, hs, ← inter_assoc, inter_comm,
                  ← inter_assoc, inter_compl_self, empty_inter, measure_empty, zero_add]
        rwa [← measure_inter_add_sdiff _ measurableSet_sigmaFiniteSet, this, add_zero,
          inter_symmDiff_distrib_right, inter_assoc, inter_self, ← inter_symmDiff_distrib_right,
          ← μ.restrict_apply' measurableSet_sigmaFiniteSet]
      · refine False.elim <| hμs ?_
        rw [eq_top_iff, ← hs]
        exact μ.restrict_le_self _

Goal state after:
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 + MemLp.toLp g hg - (bf + bg)‖ = ‖MemLp.toLp f hf - bf + (MemLp.toLp g hg - bg)‖

Tactic:
by congr; abel

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

Goal state before:
pp: case inr.inl
𝓧 : 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 < ε
μ : Measure 𝓧
hμ : μ ∈ {x | ∃ μ ∈ S, ↑μ = x}
⊢ μ ∅ᶜ ≤ ε

Tactic:
simp only [mem_ofPred_eq] at hμ

Goal state after:
case inr.inl
𝓧 : 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 < ε
μ : Measure 𝓧
hμ : ∃ μ_1 ∈ S, ↑μ_1 = μ
⊢ μ ∅ᶜ ≤ ε
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 g : X → E
s : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
h : ∀ᵐ (x : X) ∂μ.variation, x ∈ s → f x = g x
⊢ ∫ᵛ (x : X) in s, f x ∂[B; μ] = ∫ᵛ (x : X) in s, g x ∂[B; μ]

Tactic:
by
  by_cases hs : MeasurableSet s; swap
  · simp [setIntegral_eq_zero_of_not_measurableSet hs]
  apply integral_congr_ae
  rw [variation_restrict hs]
  exact (ae_restrict_iff' hs).2 h

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

Goal state before:
pp: case e'_5
α : 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
a : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : {a} = ⋂ n, Ioc (u n) a
L1 : Tendsto (fun n ↦ hf.vectorMeasure (Ioc (u n) a)) atTop (𝓝 (hf.vectorMeasure {a}))
this : Tendsto u atTop (𝓝[<] a)
⊢ Function.leftLim f a = Function.leftLim (Function.rightLim f) a

Tactic:
have : (𝓝[<] a).NeBot := by
      rw [← mem_closure_iff_nhdsWithin_neBot, closure_Iio' ⟨b, hb⟩]
      exact self_mem_Iic

Goal state after:
case e'_5
α : 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
a : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : {a} = ⋂ n, Ioc (u n) a
L1 : Tendsto (fun n ↦ hf.vectorMeasure (Ioc (u n) a)) atTop (𝓝 (hf.vectorMeasure {a}))
this✝ : Tendsto u atTop (𝓝[<] a)
this : (𝓝[<] a).NeBot
⊢ Function.leftLim f a = Function.leftLim (Function.rightLim f) a
Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation

Goal state before:
pp: case inr
α : 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
a b : α
hf : BoundedVariationOn f univ
h : a ≤ b
h' : a < b
⊢ hf.vectorMeasure (Icc a a) + hf.vectorMeasure (Ioo a b) = Function.leftLim f b - Function.leftLim f a

Tactic:
hf.vectorMeasure_Icc le_rfl,

Goal state after:
case inr
α : 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
a b : α
hf : BoundedVariationOn f univ
h : a ≤ b
h' : a < b
⊢ Function.rightLim f a - Function.leftLim f a + hf.vectorMeasure (Ioo a b) =
    Function.leftLim f b - Function.leftLim f a
Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation

Goal state before:
pp: α : 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
a : α
this : Nonempty α
hlim : Tendsto f atBot (𝓝 (atBot.limUnder f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
A : Tendsto (fun n ↦ hf.vectorMeasure (Icc (u n) a)) atTop (𝓝 (hf.vectorMeasure (Iic a)))
⊢ hf.vectorMeasure (Iic a) = Function.rightLim f a - atBot.limUnder f

Tactic:
have B : Tendsto (fun n ↦ hf.vectorMeasure (Icc (u n) a)) atTop
      (𝓝 (f.rightLim a - limUnder atBot f)) := by
    have : (fun n ↦ f.rightLim a - f.leftLim (u n)) =ᶠ[atTop]
        (fun n ↦ hf.vectorMeasure (Icc (u n) a)) := by
      have : ∀ᶠ n in atTop, u n ≤ a := by
        simp only [tendsto_atBot, eventually_atTop] at hu
        simp [hu]
      filter_upwards [this] with n hn using by rw [hf.vectorMeasure_Icc hn]
    apply Tendsto.congr' this
    apply Tendsto.sub tendsto_const_nhds
    exact (tendsto_leftLim_atBot_of_tendsto hf.tendsto_atBot_limUnder).comp hu

Goal state after:
α : 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
a : α
this : Nonempty α
hlim : Tendsto f atBot (𝓝 (atBot.limUnder f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
A : Tendsto (fun n ↦ hf.vectorMeasure (Icc (u n) a)) atTop (𝓝 (hf.vectorMeasure (Iic a)))
B : Tendsto (fun n ↦ hf.vectorMeasure (Icc (u n) a)) atTop (𝓝 (Function.rightLim f a - atBot.limUnder f))
⊢ hf.vectorMeasure (Iic a) = Function.rightLim f a - atBot.limUnder f
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'_le : m'.variation ≤ μ'
this : MeasurableSpace α := hα
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : Pairwise (Function.onFun Disjoint f)
⊢ HasSum (fun i ↦ if MeasurableSet (f i) then ∫ᵛ (x : α), μ[(f i).indicator 1 | M] x ∂•m' else 0)
    (if MeasurableSet (⋃ i, f i) then ∫ᵛ (x : α), μ[(⋃ i, f i).indicator 1 | M] x ∂•m' else 0)

Tactic:
have : ∫ᵛ (x : α), μ[fun x ↦ ∑' (d : ℕ), (f d).indicator 1 x | M] x ∂•m'
          = ∫ᵛ (x : α), ∑' d, μ[(f d).indicator 1 | M] x ∂•m' := by
        apply VectorMeasure.integral_congr_ae
        apply ae_mono m'_le
        apply ae_eq_trim_of_measurable _ (by fun_prop) (by fun_prop)
        apply condExp_tsum (fun i ↦ ?_)
        · simp only [enorm_indicator_eq_indicator_enorm, Pi.one_apply, enorm_one, f_meas,
            lintegral_indicator, lintegral_const, MeasurableSet.univ, Measure.restrict_apply,
            Set.univ_inter, one_mul, ne_eq, ← measure_iUnion hf f_meas, measure_ne_top,
            not_false_eq_true]
        · exact AEStronglyMeasurable.indicator (by fun_prop) (f_meas i)
      simp only [f_meas, ↓reduceIte, implies_true, MeasurableSet.iUnion,
        indicator_iUnion_of_pairwise_disjoint _ hf, this]
      have I : ∑' (i : ℕ), ∫⁻ (a : α), ‖μ[(f i).indicator (1 : α → ℝ) | M] a‖ₑ ∂μ < ∞ := by
        have A i : ∫⁻ a, ‖μ[(f i).indicator (1 : α → ℝ) | M] a‖ₑ ∂μ = μ (f i) :=
          lintegral_enorm_condExp_indicator Mle (f_meas i)
        simp_rw [A, ← measure_iUnion hf f_meas]
        exact measure_lt_top _ _
      rw [integral_tsum (by fun_prop)]; swap
      · apply ne_of_lt
        grw [m'_le, hμ']
        have A i : Measurable[M] (fun x ↦ ‖μ[(f i).indicator (1 : α → ℝ) | M] x‖ₑ) := by fun_prop
        simp_rw [lintegral_trim Mle (A _)]
        exact I
      refine Summable.hasSum (Summable.of_enorm ?_)
      apply ne_of_lt (lt_of_le_of_lt ?_ I)
      gcongr with i
      grw [enorm_integral_le_lintegral_enorm, ContinuousLinearMap.opENorm_lsmul_le, one_mul,
        lintegral_mono' m'_le le_rfl, hμ', lintegral_trim _ (by fun_prop)]

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

Goal state before:
pp: case neg
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))
j : M
hj : j ∈ t'
hgj : g j < f j
⊢ ∃ i, ∃ (_ : i ∈ t'), ∃ i_1, ∃ (_ : i_1 < f i), ∃ y ∈ closure ↑(t.erase i), a + i_1 • i + y = a + ∑ a ∈ t, g a • a

Tactic:
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) _), ?_⟩

Goal state after:
case neg
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))
j : M
hj : j ∈ t'
hgj : g j < f j
⊢ a + g j • j + ∑ k ∈ t.erase j, g k • k = a + ∑ a ∈ t, g a • a