mathlib-initiative/mathlib-tactics huggingface dataset:
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
this : UniformSpace B := IsTopologicalGroup.rightUniformSpace B
ε : ℝ
hε : ε > 0
U₀ : Set B
hU₀ : IsCompact U₀
K : Set B
hK : IsCompact K
hf₀ : ∀ x ∉ K, f x = 0
S : Set A := ⇑φ ⁻¹' (U₀⁻¹ * K)
hSc : IsCompact S
δ : ℝ
hδ0 : δ > 0
hδ : ENNReal.ofReal δ * μA S < ENNReal.ofReal ε
hS : ∀ {x : B}, x ∈ U₀ → ∀ {y : A}, y ∉ S → (H.pullback f x) y = 0
ha✝ : ∀ r ∈ uniformity E, ∀ᶠ (x : B × B) in uniformity B, (f x.1, f x.2) ∈ r
U : Set B
hU : U ∈ nhds 1
hf : (fun p ↦ p.2 * p.1⁻¹) ⁻¹' U ⊆ {x | (fun x ↦ (f x.1, f x.2) ∈ {p | dist p.1 p.2 < δ}) x}
t : B
ht : t ∈ U⁻¹
b : B
hb : U₀ ∈ nhds b
htb : (fun x1 x2 ↦ x1 * x2) t b ∈ U₀
a : A
ha : a ∈ S
⊢ ENNReal.ofReal (dist ((H.pullback f (t * b)) a) ((H.pullback f b) a)) ≤ ENNReal.ofReal δ

Tactic:
exact ENNReal.ofReal_le_ofReal (@hf ⟨t * b * φ a, b * φ a⟩ (by simpa)).le

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f✝ f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left✝ : StrictAnti εs
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (fun n ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto (fun x ↦ ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real (thickening (dist (μs x) ν + εs x) {a | t ≤ f a})) atTop
    (𝓝 (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real {a | t ≤ f a}))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
εs_pos : 0 < εs n
hn :
  ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real (thickening (dist (μs n) ν + εs n) {a | t ≤ f a}) <
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real {a | t ≤ f a}) + δ / 2
hn' : dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2
⊢ levyProkhorovEDist ↑(Ps n) ↑P = levyProkhorovEDist ↑(μs n).toMeasure ↑ν.toMeasure

Tactic:
rfl

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

Goal state before:
pp: case inr
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
h✝ : Nonempty Ω
xs : ℕ → Ω
xs_dense : DenseRange xs
⊢ ∃ As,
    (∀ (n : ℕ), MeasurableSet (As n)) ∧
      (∀ (n : ℕ), Bornology.IsBounded (As n)) ∧
        (∀ (n : ℕ), diam (As n) ≤ ε) ∧ ⋃ n, As n = univ ∧ Pairwise fun n m ↦ Disjoint (As n) (As m)

Tactic:
have half_ε_pos : 0 < ε / 2 := half_pos ε_pos

Goal state after:
case inr
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
h✝ : Nonempty Ω
xs : ℕ → Ω
xs_dense : DenseRange xs
half_ε_pos : 0 < ε / 2
⊢ ∃ As,
    (∀ (n : ℕ), MeasurableSet (As n)) ∧
      (∀ (n : ℕ), Bornology.IsBounded (As n)) ∧
        (∀ (n : ℕ), diam (As n) ≤ ε) ∧ ⋃ n, As n = univ ∧ Pairwise fun n m ↦ Disjoint (As n) (As m)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: case e'_2
E : Type u_1
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : BorelSpace E
inst✝² : T2Space E
inst✝¹ : ContinuousSMul ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
p✝ : ℝ
hp : 0 < p✝
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this✝³ : NormedAddCommGroup F := p.toNormedAddCommGroup
this✝² : NormedSpace ℝ F := { toModule := inst✝⁶, norm_smul_le := ⋯ }
this✝¹ : TopologicalSpace F := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
this✝ : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := (LinearEquiv.refl ℝ E).toContinuousLinearEquiv
ν : Measure F := map (⇑φ) μ
⊢ {x | g x < 1} = ⇑φ ⁻¹' {y | ‖y‖ < 1}

Tactic:
rfl

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: case e'_3
E : Type u_1
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : BorelSpace E
inst✝² : T2Space E
inst✝¹ : ContinuousSMul ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
p✝ : ℝ
hp : 0 < p✝
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this✝⁴ : NormedAddCommGroup F := p.toNormedAddCommGroup
this✝³ : NormedSpace ℝ F := { toModule := inst✝⁶, norm_smul_le := ⋯ }
this✝² : TopologicalSpace F := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
φ : E ≃L[ℝ] F := (LinearEquiv.refl ℝ E).toContinuousLinearEquiv
ν : Measure F := map (⇑φ) μ
ψ : E ≃ᵐ F := φ.toHomeomorph.toMeasurableEquiv
this : MeasurePreserving (⇑ψ) μ ν
⊢ ENNReal.ofReal ((∫ (x : E), Real.exp (-g x ^ p✝) ∂μ) / Real.Gamma (↑(finrank ℝ E) / p✝ + 1)) =
    ENNReal.ofReal ((∫ (x : E), Real.exp (-‖ψ x‖ ^ p✝) ∂μ) / Real.Gamma (↑(finrank ℝ F) / p✝ + 1))

Tactic:
rfl

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

Goal state before:
pp: case hbc
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
g : E →C_c ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
⊢ (↑μ).real univ ≤ ↑C

Tactic:
exact hμ

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: case e'_2
E : Type u_1
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
inst✝⁶ : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : BorelSpace E
inst✝³ : T2Space E
inst✝² : ContinuousSMul ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
inst✝ : Nontrivial E
r : ℝ
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this✝³ : NormedAddCommGroup F := p.toNormedAddCommGroup
this✝² : NormedSpace ℝ F := { toModule := inst✝⁷, norm_smul_le := ⋯ }
this✝¹ : TopologicalSpace F := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
this✝ : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := (LinearEquiv.refl ℝ E).toContinuousLinearEquiv
ν : Measure F := map (⇑φ) μ
⊢ {x | g x ≤ r} = ⇑φ ⁻¹' {y | ‖y‖ ≤ r}

Tactic:
rfl

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: case e'_3
E : Type u_1
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
inst✝⁶ : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : BorelSpace E
inst✝³ : T2Space E
inst✝² : ContinuousSMul ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
inst✝ : Nontrivial E
r : ℝ
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this✝³ : NormedAddCommGroup F := p.toNormedAddCommGroup
this✝² : NormedSpace ℝ F := { toModule := inst✝⁷, norm_smul_le := ⋯ }
this✝¹ : TopologicalSpace F := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
this✝ : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := (LinearEquiv.refl ℝ E).toContinuousLinearEquiv
ν : Measure F := map (⇑φ) μ
⊢ {x | g x < r} = ⇑φ ⁻¹' {y | ‖y‖ < r}

Tactic:
rfl

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst✝⁸ : (i : ι) → TopologicalSpace (X i)
inst✝⁷ : ∀ (i : ι), BorelSpace (X i)
inst✝⁶ : ∀ (i : ι), HasOuterApproxClosed (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst✝⁵ : (j : κ) → TopologicalSpace (Y j)
inst✝⁴ : ∀ (j : κ), BorelSpace (Y j)
inst✝³ : ∀ (j : κ), HasOuterApproxClosed (Y j)
inst✝² : Fintype ι
inst✝¹ : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst✝ : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i, (f i) (p.1 i)) * ↑(∏ j, (g j) (p.2 j)) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i, (f i) (p.1 i)) * ↑(∏ j, (g j) (p.2 j)) ∂ν
hμν : μ univ = ν univ
this : IsFiniteMeasure ν
π : Set (Set (((i : ι) → X i) × ((j : κ) → Y j))) :=
  image2 (fun s t ↦ s ×ˢ t) (univ.pi '' univ.pi fun x ↦ {s | IsClosed[inst✝⁸ x] s})
    (univ.pi '' univ.pi fun x ↦ {t | IsClosed[inst✝⁵ x] t})
⊢ μ = ν

Tactic:
have hπ1 : IsPiSystem π := by
    rintro - ⟨-, ⟨s₁, hs₁, rfl⟩, -, ⟨t₁, ht₁, rfl⟩, rfl⟩ -
      ⟨-, ⟨s₂, hs₂, rfl⟩, -, ⟨t₂, ht₂, rfl⟩, rfl⟩ -
    refine ⟨_, ⟨fun i ↦ s₁ i ∩ s₂ i, ?_, rfl⟩, _, ⟨fun j ↦ t₁ j ∩ t₂ j, ?_, rfl⟩, ?_⟩
    · simp only [Set.mem_pi, mem_univ, mem_ofPred_eq, forall_const] at hs₁ hs₂ ⊢
      exact fun i ↦ (hs₁ i).inter (hs₂ i)
    · simp only [Set.mem_pi, mem_univ, mem_ofPred_eq, forall_const] at ht₁ ht₂ ⊢
      exact fun j ↦ (ht₁ j).inter (ht₂ j)
    simp [Set.pi_inter_distrib, Set.prod_inter_prod]

Goal state after:
ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst✝⁸ : (i : ι) → TopologicalSpace (X i)
inst✝⁷ : ∀ (i : ι), BorelSpace (X i)
inst✝⁶ : ∀ (i : ι), HasOuterApproxClosed (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst✝⁵ : (j : κ) → TopologicalSpace (Y j)
inst✝⁴ : ∀ (j : κ), BorelSpace (Y j)
inst✝³ : ∀ (j : κ), HasOuterApproxClosed (Y j)
inst✝² : Fintype ι
inst✝¹ : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst✝ : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i, (f i) (p.1 i)) * ↑(∏ j, (g j) (p.2 j)) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i, (f i) (p.1 i)) * ↑(∏ j, (g j) (p.2 j)) ∂ν
hμν : μ univ = ν univ
this : IsFiniteMeasure ν
π : Set (Set (((i : ι) → X i) × ((j : κ) → Y j))) :=
  image2 (fun s t ↦ s ×ˢ t) (univ.pi '' univ.pi fun x ↦ {s | IsClosed[inst✝⁸ x] s})
    (univ.pi '' univ.pi fun x ↦ {t | IsClosed[inst✝⁵ x] t})
hπ1 : IsPiSystem π
⊢ μ = ν
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: case e'_5
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 Λ'
μlim_le : μlim univ ≤ ENNReal.ofReal ↑C
μlim' : FiniteMeasure E := ⟨μlim, ⋯⟩
g : E →ᵇ ℝ
g' : E →C_c ℝ := { toFun := ⇑g, continuous_toFun := ⋯, hasCompactSupport' := ⋯ }
⊢ Λ' g' = Λ g'

Tactic:
rfl

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
inst✝ : CompactSpace E
C : ℝ≥0
⊢ {μ | μ.mass = C} = {μ | μ.mass ≤ C} ∩ {μ | μ.mass = C}

Tactic:
grind

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

Goal state before:
pp: E : Type u_1
mE : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : ProperSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h : Tendsto (fun r ↦ limsup (fun n ↦ (μ n) {x | r < ‖x‖}) atTop) atTop (𝓝 0)
⊢ Tendsto (fun r ↦ ⨆ i, (μ i) {x | r < ‖x‖}) atTop (𝓝 0)

Tactic:
refine Nat.tendsto_iSup_of_tendsto_limsup (fun n ↦ ?_) h (fun n u v huv ↦ by gcongr)

Goal state after:
E : Type u_1
mE : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : ProperSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h : Tendsto (fun r ↦ limsup (fun n ↦ (μ n) {x | r < ‖x‖}) atTop) atTop (𝓝 0)
n : ℕ
⊢ Tendsto (fun r ↦ (μ n) {x | r < ‖x‖}) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Measure.TightNormed

Goal state before:
pp: case inr
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_2
ι : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype ι
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι 𝕜 E
h : ∀ (i : ι), Tendsto (fun r ↦ ⨆ μ ∈ S, μ {x | r < ‖⟪b i, x⟫_𝕜‖}) atTop (𝓝 0)
hE : Nontrivial E
h_rank : 0 < ↑(Fintype.card ι)
this✝ : Nonempty ι
this : ProperSpace E
h_le : (fun r ↦ ⨆ μ ∈ S, μ {x | r < ‖x‖}) ≤ fun r ↦ ∑ i, ⨆ μ ∈ S, μ {x | r / √↑(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖}
⊢ Tendsto (fun r ↦ ⨆ μ ∈ S, μ {x | r < ‖x‖}) atTop (𝓝 0)

Tactic:
refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds ?_ (fun _ ↦ zero_le) h_le

Goal state after:
case inr
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_2
ι : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype ι
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι 𝕜 E
h : ∀ (i : ι), Tendsto (fun r ↦ ⨆ μ ∈ S, μ {x | r < ‖⟪b i, x⟫_𝕜‖}) atTop (𝓝 0)
hE : Nontrivial E
h_rank : 0 < ↑(Fintype.card ι)
this✝ : Nonempty ι
this : ProperSpace E
h_le : (fun r ↦ ⨆ μ ∈ S, μ {x | r < ‖x‖}) ≤ fun r ↦ ∑ i, ⨆ μ ∈ S, μ {x | r / √↑(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖}
⊢ Tendsto (fun r ↦ ∑ i, ⨆ μ ∈ S, μ {x | r / √↑(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖}) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Measure.MeasuredSets

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
⊢ ∀ (x y : MeasuredSets μ), μ (↑x ∆ ↑y) = μ (↑y ∆ ↑x)

Tactic:
grind

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

Goal state before:
pp: case h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ D, D.Countable ∧ D ⊆ C ∧ μ (⋃₀ D)ᶜ = 0
h : mα = generateFrom C
s✝ : Set α
hs✝ : MeasurableSet s✝
ε✝ : ℝ≥0∞
hε : 0 < ε✝
s : Set α
hs : MeasurableSet s
h's : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ t ∈ C, μ (t ∆ s) < ε
ε : ℝ≥0∞
εpos : 0 < ε
t : Set α
tC : t ∈ C
ht : μ (t ∆ s) < ε / 2
t' : Set α
t'C : t' ∈ C
ht' : μ t'ᶜ < ε / 2
⊢ (t' \ t) ∆ sᶜ ⊆ t ∆ s ∪ t'ᶜ

Tactic:
grind

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

Goal state before:
pp: case h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ D, D.Countable ∧ D ⊆ C ∧ μ (⋃₀ D)ᶜ = 0
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε✝ : ℝ≥0∞
hε : 0 < ε✝
f : ℕ → Set α
f_disj : Pairwise (Function.onFun Disjoint f)
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ) (ε : ℝ≥0∞), 0 < ε → ∃ t ∈ C, μ (t ∆ f i) < ε
ε : ℝ≥0∞
εpos : 0 < ε
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε / 2
t : ℕ → Set α
tC : ∀ (i : ℕ), t i ∈ C
ht : ∀ (i : ℕ), μ (t i ∆ f i) < δ i
this : Tendsto (fun n ↦ μ (⋃ i ∈ Ici n, f i)) atTop (𝓝 0)
n : ℕ
hn : μ (⋃ i ∈ Ici n, f i) < ε / 2
x : α
hx : ((∃ i < n, x ∈ t i) ∧ ∀ (x_1 : ℕ), x ∉ f x_1) ∨ (∃ i, x ∈ f i) ∧ ∀ x_1 < n, x ∉ t x_1
⊢ (∃ i < n, x ∈ t i ∧ x ∉ f i ∨ x ∈ f i ∧ x ∉ t i) ∨ ∃ i, n ≤ i ∧ x ∈ f i

Tactic:
grind

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⁻¹
x : ℝ
hx : x ∈ Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)
⊢ |x| ≤ 2 * r⁻¹

Tactic:
grind

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
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
⊢ Finset.Ioc n m ⊆ Finset.range (m + 1)

Tactic:
grind

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : MeasurableSpace X
μ : Measure X
⊢ ∀ (x : X),
    (∀ (i : Set X), x ∈ i ∧ IsOpen[inst✝¹] i → ∃ x ∈ i, ∀ (i : Set X), x ∈ i ∧ IsOpen[inst✝¹] i → 0 < μ i) →
      ∀ (i : Set X), x ∈ i ∧ IsOpen[inst✝¹] i → 0 < μ i

Tactic:
grind

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

Goal state before:
pp: case refine_1
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : MeasurableSpace X
μ : Measure X
K : Set X
hK : IsCompact K
hKsub : K ⊆ μ.supportᶜ
⊢ ∀ ⦃s t : Set X⦄, s ⊆ t → μ t = 0 → μ s = 0

pp: case refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : MeasurableSpace X
μ : Measure X
K : Set X
hK : IsCompact K
hKsub : K ⊆ μ.supportᶜ
⊢ ∀ ⦃s t : Set X⦄, μ s = 0 → μ t = 0 → μ (s ∪ t) = 0

pp: case refine_3
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : MeasurableSpace X
μ : Measure X
K : Set X
hK : IsCompact K
hKsub : K ⊆ μ.supportᶜ
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, μ t = 0

Tactic:
· exact fun _ _ hst ht ↦ measure_mono_null hst ht

Goal state after:
case refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : MeasurableSpace X
μ : Measure X
K : Set X
hK : IsCompact K
hKsub : K ⊆ μ.supportᶜ
⊢ ∀ ⦃s t : Set X⦄, μ s = 0 → μ t = 0 → μ (s ∪ t) = 0

case refine_3
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : MeasurableSpace X
μ : Measure X
K : Set X
hK : IsCompact K
hKsub : K ⊆ μ.supportᶜ
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, μ t = 0
Module: Mathlib.MeasureTheory.Measure.ResolventTransform

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : NormedAlgebra 𝕜 A
m𝕜 : MeasurableSpace 𝕜
μ : Measure 𝕜
⊢ resolventTransform μ = fun a ↦ ∫ (x : 𝕜), resolvent a x ∂μ

Tactic:
rfl

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : NormedAlgebra 𝕜 A
m𝕜 : MeasurableSpace 𝕜
μ : Measure 𝕜
a : A
⊢ resolventTransform μ a = ∫ (x : 𝕜), resolvent a x ∂μ

Tactic:
rfl

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

Goal state before:
pp: case h
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : HereditarilyLindelofSpace 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : MeasurableSpace 𝕜
inst✝³ : BorelSpace 𝕜
inst✝² : RCLike A
inst✝¹ : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst✝ : IsFiniteMeasure μ
a : A
ha : a ∉ ⇑(algebraMap 𝕜 A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a (⇑(algebraMap 𝕜 A) '' μ.support)
s : Set A := ball a (infDist a (⇑(algebraMap 𝕜 A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
⊢ infDist a (⇑(algebraMap 𝕜 A) '' μ.support) / 2 ≤ infDist a (⇑(algebraMap 𝕜 A) '' μ.support)

Tactic:
grind

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : HereditarilyLindelofSpace 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : MeasurableSpace 𝕜
inst✝³ : BorelSpace 𝕜
inst✝² : RCLike A
inst✝¹ : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst✝ : IsFiniteMeasure μ
a : A
ha : a ∉ ⇑(algebraMap 𝕜 A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a (⇑(algebraMap 𝕜 A) '' μ.support)
s : Set A := ball a (infDist a (⇑(algebraMap 𝕜 A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ (⇑(algebraMap 𝕜 A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
x : 𝕜
hx : x ∈ μ.support
w : A
hw : w ∈ s
⊢ infDist a (⇑(algebraMap 𝕜 A) '' μ.support) / 2 ≤
    infDist a (⇑(algebraMap 𝕜 A) '' μ.support) - infDist a (⇑(algebraMap 𝕜 A) '' μ.support) / 2

Tactic:
grind

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : HereditarilyLindelofSpace 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : MeasurableSpace 𝕜
inst✝³ : BorelSpace 𝕜
inst✝² : RCLike A
inst✝¹ : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst✝ : IsFiniteMeasure μ
a : A
ha : a ∉ ⇑(algebraMap 𝕜 A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a (⇑(algebraMap 𝕜 A) '' μ.support)
s : Set A := ball a (infDist a (⇑(algebraMap 𝕜 A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ (⇑(algebraMap 𝕜 A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
x : 𝕜
hx : x ∈ μ.support
w : A
hw : w ∈ s
⊢ ‖(algebraMap 𝕜 A) x - a + (a - w)‖ ≤ ‖(algebraMap 𝕜 A) x - w‖

Tactic:
grind

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
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
x✝ : FiniteMeasure E
⊢ x✝ ∈ {μ | μ.mass = C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ↔
    x✝ ∈ {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∩ {μ | μ.mass = C}

Tactic:
grind

Goal state after: