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

Goal state before:
pp: case e_f
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : BorelSpace E
r : E
L : StrongDual ℝ E
a : E
⊢ ↑(L (a + r)) * I = ↑(L a) * I + ↑(L r) * I

Tactic:
simp only [map_add, ofReal_add]

Goal state after:
case e_f
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : BorelSpace E
r : E
L : StrongDual ℝ E
a : E
⊢ (↑(L a) + ↑(L r)) * I = ↑(L a) * I + ↑(L r) * I
Module: Mathlib.MeasureTheory.Measure.DiracProba

Goal state before:
pp: X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : OpensMeasurableSpace X
⊢ Continuous[inst✝¹, ProbabilityMeasure.instTopologicalSpace] fun x ↦ diracProba x

Tactic:
rw [continuous_iff_continuousAt]

Goal state after:
X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : OpensMeasurableSpace X
⊢ ∀ (x : X), ContinuousAt (fun x ↦ diracProba x) x
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: X : Type u_1
inst✝⁷ : TopologicalSpace X
inst✝⁶ : T2Space X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
μ ν : Measure X
inst✝³ : LocallyCompactSpace X
inst✝² : ν.OuterRegular
inst✝¹ : IsFiniteMeasureOnCompacts ν
inst✝ : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), ∫ (x : X), f x ∂μ ≤ ∫ (x : X), f x ∂ν
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : ν K < ∞
hνK : ν K ≠ ∞
hμK : μ K ≠ ∞
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst✝⁷] V
pV3 : ν V ≤ ν K + ↑ε
⊢ μ K ≤ ν K + ↑ε

Tactic:
suffices μ.real K ≤ ν.real K + ε by
    rwa [← ENNReal.toReal_le_toReal, ENNReal.toReal_add, ENNReal.coe_toReal]
    all_goals finiteness

Goal state after:
X : Type u_1
inst✝⁷ : TopologicalSpace X
inst✝⁶ : T2Space X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
μ ν : Measure X
inst✝³ : LocallyCompactSpace X
inst✝² : ν.OuterRegular
inst✝¹ : IsFiniteMeasureOnCompacts ν
inst✝ : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), ∫ (x : X), f x ∂μ ≤ ∫ (x : X), f x ∂ν
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : ν K < ∞
hνK : ν K ≠ ∞
hμK : μ K ≠ ∞
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst✝⁷] V
pV3 : ν V ≤ ν K + ↑ε
⊢ μ.real K ≤ ν.real K + ↑ε
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: case pos
Ω : Type u_1
inst✝² : PseudoMetricSpace Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G
ε : ℝ≥0∞
ε_pos : 0 < ε
easy : ε ≤ ↑P G
ε_top : ε = ∞
⊢ {Q | ↑P G < ↑Q G + ε} ∈ 𝓝 P

pp: case neg
Ω : Type u_1
inst✝² : PseudoMetricSpace Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G
ε : ℝ≥0∞
ε_pos : 0 < ε
easy : ε ≤ ↑P G
ε_top : ¬ε = ∞
⊢ {Q | ↑P G < ↑Q G + ε} ∈ 𝓝 P

Tactic:
· simp [ε_top, measure_lt_top]

Goal state after:
case neg
Ω : Type u_1
inst✝² : PseudoMetricSpace Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G
ε : ℝ≥0∞
ε_pos : 0 < ε
easy : ε ≤ ↑P G
ε_top : ¬ε = ∞
⊢ {Q | ↑P G < ↑Q G + ε} ∈ 𝓝 P
Module: Mathlib.MeasureTheory.Measure.Haar.Extension

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹³ : Group A
inst✝¹² : Group B
inst✝¹¹ : Group C
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : TopologicalSpace B
inst✝⁸ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝⁷ : IsTopologicalGroup A
inst✝⁶ : IsTopologicalGroup B
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace A
inst✝³ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝² : NormedSpace ℝ E
inst✝¹ : IsTopologicalGroup C
inst✝ : LocallyCompactSpace B
f : CompactlySupportedContinuousMap B E
⊢ HasCompactSupport fun c ↦ ∫ (a : A), (H.pullback f (Function.invFun (⇑ψ) c)) a ∂μA

Tactic:
obtain ⟨K, hK, hf⟩ := exists_compact_iff_hasCompactSupport.mpr f.hasCompactSupport
      refine exists_compact_iff_hasCompactSupport.mp
        ⟨ψ '' K, hK.image H.isOpenQuotientMap.continuous, fun x hx ↦ ?_⟩
      suffices ∀ a : A, f (Function.invFun ψ x * φ a) = 0 by simp [this, pullback_def]
      refine fun a ↦ hf _ (mt (Set.mem_image_of_mem ψ) ?_)
      rwa [map_mul, Function.rightInverse_invFun H.isOpenQuotientMap.surjective,
        H.mulExact.apply_apply_eq_one, mul_one]

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

Goal state before:
pp: Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
⊢ Continuous[ProbabilityMeasure.instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ofMeasure

Tactic:
rw [continuous_iff_continuousAt]

Goal state after:
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
⊢ ∀ (x : ProbabilityMeasure Ω), ContinuousAt ofMeasure x
Module: Mathlib.MeasureTheory.Measure.Haar.Extension

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝¹⁷ : Group A
inst✝¹⁶ : Group B
inst✝¹⁵ : Group C
inst✝¹⁴ : TopologicalSpace A
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝¹¹ : IsTopologicalGroup A
inst✝¹⁰ : IsTopologicalGroup B
inst✝⁹ : MeasurableSpace A
inst✝⁸ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝⁷ : IsTopologicalGroup C
inst✝⁶ : LocallyCompactSpace B
inst✝⁵ : MeasurableSpace C
inst✝⁴ : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst✝³ : T2Space B
inst✝² : MeasurableSpace B
inst✝¹ : BorelSpace B
U : Set B
hU : IsOpen U
inst✝ : DiscreteTopology A
h✝ : μC Set.univ * μA {1} < (H.inducedMeasure μA μC) U
ho : 0 < μA {1}
ht : μA {1} < ⊤
K : Set B
hKU : K ⊆ U
hK : IsCompact K
f : C(B, ℝ)
hf1 : Set.EqOn (⇑f) 1 K
hf2 : IsCompact (tsupport ⇑f)
hf3 : tsupport ⇑f ⊆ U
hf4 : ∀ (x : B), f x ∈ Set.Icc 0 1
h :
  μC Set.univ * μA {1} <
    ENNReal.ofReal (∫ (c : C), ((H.pushforward μA) { toContinuousMap := f, hasCompactSupport' := hf2 }) c ∂μC)
c : C
hc : (μA {1}).toReal < ((H.pushforward μA) { toContinuousMap := f, hasCompactSupport' := hf2 }) c
⊢ ¬Set.InjOn (⇑ψ) U

Tactic:
contrapose! hc

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝¹⁷ : Group A
inst✝¹⁶ : Group B
inst✝¹⁵ : Group C
inst✝¹⁴ : TopologicalSpace A
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝¹¹ : IsTopologicalGroup A
inst✝¹⁰ : IsTopologicalGroup B
inst✝⁹ : MeasurableSpace A
inst✝⁸ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝⁷ : IsTopologicalGroup C
inst✝⁶ : LocallyCompactSpace B
inst✝⁵ : MeasurableSpace C
inst✝⁴ : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst✝³ : T2Space B
inst✝² : MeasurableSpace B
inst✝¹ : BorelSpace B
U : Set B
hU : IsOpen U
inst✝ : DiscreteTopology A
h✝ : μC Set.univ * μA {1} < (H.inducedMeasure μA μC) U
ho : 0 < μA {1}
ht : μA {1} < ⊤
K : Set B
hKU : K ⊆ U
hK : IsCompact K
f : C(B, ℝ)
hf1 : Set.EqOn (⇑f) 1 K
hf2 : IsCompact (tsupport ⇑f)
hf3 : tsupport ⇑f ⊆ U
hf4 : ∀ (x : B), f x ∈ Set.Icc 0 1
h :
  μC Set.univ * μA {1} <
    ENNReal.ofReal (∫ (c : C), ((H.pushforward μA) { toContinuousMap := f, hasCompactSupport' := hf2 }) c ∂μC)
c : C
hc : Set.InjOn (⇑ψ) U
⊢ ((H.pushforward μA) { toContinuousMap := f, hasCompactSupport' := hf2 }) c ≤ (μA {1}).toReal
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this✝ : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℝ), 0 ≤ ∑ i, |x i| ^ p
eq_norm : ∀ (x : ι → ℝ), ‖toLp (ENNReal.ofReal p) x‖ = (∑ i, |x i| ^ p) ^ (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
⊢ volume {x | ∑ i, |x i| ^ p < 1} = ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))

Tactic:
have nm_zero : ‖toLp (.ofReal p) (0 : ι → ℝ)‖ = 0 := norm_zero

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this✝ : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℝ), 0 ≤ ∑ i, |x i| ^ p
eq_norm : ∀ (x : ι → ℝ), ‖toLp (ENNReal.ofReal p) x‖ = (∑ i, |x i| ^ p) ^ (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
nm_zero : ‖toLp (ENNReal.ofReal p) 0‖ = 0
⊢ volume {x | ∑ i, |x i| ^ p < 1} = ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
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
inst✝ : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C} ∈ f
Λ : (E →C_c ℝ) → ℝ
h₀Λ : ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-↑C * ‖g.toBoundedContinuousFunction‖) (↑C * ‖g.toBoundedContinuousFunction‖)
hΛ : ∀ (g : E →C_c ℝ), Tendsto (fun μ ↦ ∫ (x : E), g x ∂↑μ) (↑f) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
o : E →C_c ℝ := { toFun := 1, continuous_toFun := ⋯, hasCompactSupport' := ⋯ }
this : μlim univ ≤ ENNReal.ofReal (Λ' o)
⊢ μlim univ ≤ ENNReal.ofReal ↑C

Tactic:
apply this.trans

Goal state after:
E : Type u_1
inst✝⁴ : MeasurableSpace E
inst✝³ : TopologicalSpace E
inst✝² : T2Space E
inst✝¹ : BorelSpace E
inst✝ : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C} ∈ f
Λ : (E →C_c ℝ) → ℝ
h₀Λ : ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-↑C * ‖g.toBoundedContinuousFunction‖) (↑C * ‖g.toBoundedContinuousFunction‖)
hΛ : ∀ (g : E →C_c ℝ), Tendsto (fun μ ↦ ∫ (x : E), g x ∂↑μ) (↑f) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := ⋯
μlim : Measure E := ⋯
o : E →C_c ℝ := ⋯
this : μlim univ ≤ ENNReal.ofReal (Λ' o)
⊢ ENNReal.ofReal (Λ' o) ≤ ENNReal.ofReal ↑C
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i, |x i| ^ p
h₂ : ∀ (x : ι → ℝ), 0 ≤ (∑ i, |x i| ^ p) ^ (1 / p)
hr : r ≤ 0
x : ι → ℝ
⊢ x ∈ {x | (∑ i, |x i| ^ p) ^ (1 / p) < r} ↔ x ∈ ∅

Tactic:
refine ⟨fun hx => ?_, fun hx => hx.elim⟩

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i, |x i| ^ p
h₂ : ∀ (x : ι → ℝ), 0 ≤ (∑ i, |x i| ^ p) ^ (1 / p)
hr : r ≤ 0
x : ι → ℝ
hx : x ∈ {x | (∑ i, |x i| ^ p) ^ (1 / p) < r}
⊢ x ∈ ∅
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
inst✝ : CompactSpace E
C : ℝ≥0
⊢ IsCompact {μ | μ.mass = C}

Tactic:
have : {μ : FiniteMeasure E | μ.mass = C} = {μ | μ.mass ≤ C} ∩ {μ | μ.mass = C} := by grind

Goal state after:
E : Type u_1
inst✝⁴ : MeasurableSpace E
inst✝³ : TopologicalSpace E
inst✝² : T2Space E
inst✝¹ : BorelSpace E
inst✝ : CompactSpace E
C : ℝ≥0
this : {μ | μ.mass = C} = {μ | μ.mass ≤ C} ∩ {μ | μ.mass = C}
⊢ IsCompact {μ | μ.mass = C}
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : 0 < p
this✝ : (ENNReal.ofReal p).toReal = p
eq_norm : ∀ (x : ι → ℝ), ‖toLp (ENNReal.ofReal p) x‖ = (∑ i, |x i| ^ p) ^ (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
⊢ volume {x | (∑ i, |x i| ^ p) ^ (1 / p) ≤ r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))

Tactic:
have nm_zero : ‖toLp (.ofReal p) (0 : ι → ℝ)‖ = 0 := norm_zero

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : 0 < p
this✝ : (ENNReal.ofReal p).toReal = p
eq_norm : ∀ (x : ι → ℝ), ‖toLp (ENNReal.ofReal p) x‖ = (∑ i, |x i| ^ p) ^ (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
nm_zero : ‖toLp (ENNReal.ofReal p) 0‖ = 0
⊢ volume {x | (∑ i, |x i| ^ p) ^ (1 / p) ≤ r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℂ), 0 ≤ ∑ i, ‖x i‖ ^ p
h₂ : ∀ (x : ι → ℂ), 0 ≤ (∑ i, ‖x i‖ ^ p) ^ (1 / p)
hr : r ≤ 0
x : ι → ℂ
⊢ x ∈ {x | (∑ i, ‖x i‖ ^ p) ^ (1 / p) < r} ↔ x ∈ ∅

Tactic:
refine ⟨fun hx => ?_, fun hx => hx.elim⟩

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℂ), 0 ≤ ∑ i, ‖x i‖ ^ p
h₂ : ∀ (x : ι → ℂ), 0 ≤ (∑ i, ‖x i‖ ^ p) ^ (1 / p)
hr : r ≤ 0
x : ι → ℂ
hx : x ∈ {x | (∑ i, ‖x i‖ ^ p) ^ (1 / p) < r}
⊢ x ∈ ∅
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
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
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), ⋯⟩
g : E →ᵇ ℝ
ε : ℝ
εpos : ε > 0
this : Tendsto (fun n ↦ ∫ (x : E), g x ∂∑ i ∈ Finset.range n, ↑(ν i)) atTop (𝓝 (∫ (x : E), g x ∂↑μ))
⊢ ∀ᶠ (n : ℕ) in atTop, dist (∫ (x : E), g x ∂∑ i ∈ Finset.range (n + 1), ↑(ν i)) (∫ (x : E), g x ∂↑μ) < ε / 3

Tactic:
exact Metric.tendsto_nhds.1 (this.comp (tendsto_add_atTop_nat 1)) _ (by positivity)

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : OpensMeasurableSpace X
s : Set X
x : X
hxs : x ∈ interior s
hxμ : ∀ (i : Set X), x ∈ i ∧ IsOpen[inst✝²] i → 0 < μ i
⊢ ∀ (i : Set X), x ∈ i ∧ IsOpen[inst✝²] i → 0 < μ (i ∩ s)

Tactic:
rintro u ⟨hxu, hu⟩

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : OpensMeasurableSpace X
s : Set X
x : X
hxs : x ∈ interior s
hxμ : ∀ (i : Set X), x ∈ i ∧ IsOpen[inst✝²] i → 0 < μ i
u : Set X
hxu : x ∈ u
hu : IsOpen[inst✝²] u
⊢ 0 < μ (u ∩ s)
Module: Mathlib.MeasureTheory.Measure.ResolventTransform

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : MeasurableSpace 𝕜
inst✝² : CompleteSpace 𝕜
inst✝¹ : NormedDivisionRing A
inst✝ : NormedAlgebra 𝕜 A
μ : Measure 𝕜
a : A
hz : a ∉ ⇑(algebraMap 𝕜 A) '' μ.support
x : 𝕜
hx : x ∈ μ.support
this✝ : 0 < infDist a (⇑(algebraMap 𝕜 A) '' μ.support)
this : infDist a (⇑(algebraMap 𝕜 A) '' μ.support) ≤ ‖(algebraMap 𝕜 A) x - a‖
⊢ ‖Ring.inverse ((algebraMap 𝕜 A) x - a)‖ ≤ (infDist a (⇑(algebraMap 𝕜 A) '' μ.support))⁻¹

Tactic:
Ring.inverse_eq_inv',

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : MeasurableSpace 𝕜
inst✝² : CompleteSpace 𝕜
inst✝¹ : NormedDivisionRing A
inst✝ : NormedAlgebra 𝕜 A
μ : Measure 𝕜
a : A
hz : a ∉ ⇑(algebraMap 𝕜 A) '' μ.support
x : 𝕜
hx : x ∈ μ.support
this✝ : 0 < infDist a (⇑(algebraMap 𝕜 A) '' μ.support)
this : infDist a (⇑(algebraMap 𝕜 A) '' μ.support) ≤ ‖(algebraMap 𝕜 A) x - a‖
⊢ ‖((algebraMap 𝕜 A) x - a)⁻¹‖ ≤ (infDist a (⇑(algebraMap 𝕜 A) '' μ.support))⁻¹
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: case inr
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)
⊢ dist (indicatorConstLp p ms hμs c) (indicatorConstLp p ⋯ hμt c) < ε

Tactic:
dist_indicatorConstLp_eq_norm,

Goal state after:
case inr
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)
⊢ ‖indicatorConstLp p ⋯ ⋯ c‖ < ε
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
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 : Monotone K
this✝ : Tendsto (fun m ↦ ∑ i ∈ Finset.range (m + 1), ↑(ν i) (K n)ᶜ) atTop (𝓝 (∑' (i : ℕ), ↑(ν i) (K n)ᶜ))
m : ℕ
hm : n ≤ m
this : ∑ i ∈ Finset.range (m + 1), ↑(ν i) (K n)ᶜ = ∑ i ∈ Finset.Ioc n m, ↑(ν i) (K n)ᶜ
⊢ (∑ i ∈ Finset.Ioc n m, ν i).mass ≤ u n

Tactic:
have : Tendsto (fun (μ : FiniteMeasure E) ↦
        (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)).mass) f
        (𝓝 ((∑ i ∈ Finset.Ioc n m, ν i).mass)) := by
      apply Tendsto.mass
      exact tendsto_finsetSum _ (fun i hi ↦ hν i)

Goal state after:
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 : Monotone K
this✝¹ : Tendsto (fun m ↦ ∑ i ∈ Finset.range (m + 1), ↑(ν i) (K n)ᶜ) atTop (𝓝 (∑' (i : ℕ), ↑(ν i) (K n)ᶜ))
m : ℕ
hm : n ≤ m
this✝ : ∑ i ∈ Finset.range (m + 1), ↑(ν i) (K n)ᶜ = ∑ i ∈ Finset.Ioc n m, ↑(ν i) (K n)ᶜ
this :
  Tendsto (fun μ ↦ (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)).mass) (↑f) (𝓝 (∑ i ∈ Finset.Ioc n m, ν i).mass)
⊢ (∑ i ∈ Finset.Ioc n m, ν i).mass ≤ u n
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s = 1
hμt : μ t = 1
h✝ : μ (s ∩ t) = 0
⊢ μ (s ∩ t)ᶜ = μ (sᶜ ∪ tᶜ)

Tactic:
by simp [compl_inter]

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 ↦ T n ∩ s) Filter.atTop (nhds (μ (⋃ n, T n ∩ s)))
⊢ ∃ t ∈ 𝒜, μ (s ∆ t) < ENNReal.ofReal ε

Tactic:
rw [← tendsto_toReal_iff] at this

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)
⊢ ∃ t ∈ 𝒜, μ (s ∆ t) < ENNReal.ofReal ε

case hf
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 ↦ T n ∩ s) Filter.atTop (nhds (μ (⋃ n, T n ∩ s)))
⊢ ∀ (i : ℕ), (⇑μ ∘ fun n ↦ T n ∩ s) i ≠ ∞

case hx
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 ↦ T n ∩ s) Filter.atTop (nhds (μ (⋃ n, T n ∩ s)))
⊢ μ (⋃ n, T n ∩ 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_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
⊢ (AddContent.extend hC m).IsSigmaSubadditive

pp: case refine_3
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
⊢ ∀ s ∉ C, (AddContent.extend hC m) s = ∞

Tactic:
· 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)]

Goal state after:
case refine_3
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
⊢ ∀ s ∉ C, (AddContent.extend hC m) s = ∞
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}
a : E
s : Set X
ms : MeasurableSet s
hμs✝ : μ s < ∞
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
μs_pow_nonneg : 0 ≤ μ.real s ^ (1 / p.toReal)
approx_a_pos : 0 < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
b : E
b_mem : b ∈ u
hb : ‖a - b‖ < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
t : Set X
ht : t ∈ 𝒜₀
hμt : μ t ≠ ∞
hst : ‖indicatorConstLp p ms hμs b - indicatorConstLp p ⋯ hμt b‖ < ε / 3
mt : MeasurableSet t
⊢ indicatorConstLp p mt hμt b = key 1 (fun x ↦ ⟨b, b_mem⟩) fun x ↦ ⟨t, ht⟩

Tactic:
by simp [key]

Goal state after: