mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
inst✝ : NormedSpace ℝ E
C : ℝ
h : ∀ z ∈ [a -[ℝ] b], ‖ω z‖ ≤ C
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
⊢ ‖∫ᶜ (x : E) in Path.segment a b, ω x‖ ≤ C * ‖b - a‖ * |1 - 0|

Tactic:
rw [curveIntegral_segment]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
inst✝ : NormedSpace ℝ E
C : ℝ
h : ∀ z ∈ [a -[ℝ] b], ‖ω z‖ ≤ C
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
⊢ ‖∫ (t : ℝ) in 0..1, (ω ((lineMap a b) t)) (b - a)‖ ≤ C * ‖b - a‖ * |1 - 0|
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
hfc : ContinuousOn f (segment ℝ a b)
hfd : ∀ t ∈ Ioo 0 1, LineDifferentiableAt ℝ f ((lineMap a b) t) (b - a)
hf' : ∀ᵐ (t : ℝ), t ∈ Ioo 0 1 → ‖lineDeriv ℝ f ((lineMap a b) t) (b - a)‖ ≤ C
g : ℝ → F := fun t ↦ f ((lineMap a b) t)
⊢ ‖f b - f a‖ ≤ C * volume.real {t | t ∈ Ioo 0 1 ∧ lineDeriv ℝ f ((lineMap a b) t) (b - a) ≠ 0}

Tactic:
have hgc : ContinuousOn g (Icc 0 1) := by
    refine hfc.comp ?_ ?_
    · exact AffineMap.lineMap_continuous.continuousOn
    · simp [segment_eq_image_lineMap, mapsTo_image]

Goal state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
hfc : ContinuousOn f (segment ℝ a b)
hfd : ∀ t ∈ Ioo 0 1, LineDifferentiableAt ℝ f ((lineMap a b) t) (b - a)
hf' : ∀ᵐ (t : ℝ), t ∈ Ioo 0 1 → ‖lineDeriv ℝ f ((lineMap a b) t) (b - a)‖ ≤ C
g : ℝ → F := fun t ↦ f ((lineMap a b) t)
hgc : ContinuousOn g (Icc 0 1)
⊢ ‖f b - f a‖ ≤ C * volume.real {t | t ∈ Ioo 0 1 ∧ lineDeriv ℝ f ((lineMap a b) t) (b - a) ≠ 0}
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DiffContOnCl ℝ f s
hab : openSegment ℝ a b ⊆ s
hC : ∀ x ∈ s, ‖fderiv ℝ f x‖ ≤ C
hmem_s : ∀ t ∈ Ioo 0 1, (lineMap a b) t ∈ s
hC₀ : 0 ≤ C
hfc : ContinuousOn f (segment ℝ a b)
⊢ ‖f b - f a‖ ≤ C * ‖b - a‖ * volume.real {t | t ∈ Ioo 0 1 ∧ fderiv ℝ f ((lineMap a b) t) ≠ 0}

Tactic:
have hfd : ∀ t ∈ Ioo (0 : ℝ) 1, LineDifferentiableAt ℝ f (lineMap a b t) (b - a) := fun t ht ↦
    (hf.differentiableAt hs <| hmem_s t ht).lineDifferentiableAt

Goal state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DiffContOnCl ℝ f s
hab : openSegment ℝ a b ⊆ s
hC : ∀ x ∈ s, ‖fderiv ℝ f x‖ ≤ C
hmem_s : ∀ t ∈ Ioo 0 1, (lineMap a b) t ∈ s
hC₀ : 0 ≤ C
hfc : ContinuousOn f (segment ℝ a b)
hfd : ∀ t ∈ Ioo 0 1, LineDifferentiableAt ℝ f ((lineMap a b) t) (b - a)
⊢ ‖f b - f a‖ ≤ C * ‖b - a‖ * volume.real {t | t ∈ Ioo 0 1 ∧ fderiv ℝ f ((lineMap a b) t) ≠ 0}
Module: Mathlib.MeasureTheory.MeasurableSpace.Card

Goal state before:
pp: case refine_3
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
u : Set α
j : Ordinal.{v}
hj : j < ω_ 1
hj' : u ∈ generateMeasurableRec s j
⊢ ∃ i, ∃ (_ : i < ω_ 1), uᶜ ∈ generateMeasurableRec s i

Tactic:
exact ⟨_, (isSuccLimit_omega 1).succ_lt hj,
      compl_mem_generateMeasurableRec (Order.lt_succ j) hj'⟩

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

Goal state before:
pp: E : Type u_1
𝕜 : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA : (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A).SeparatesPoints
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
A_toReal : Subalgebra ℝ (E →ᵇ ℝ) :=
  Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm ⋯) (Subalgebra.restrictScalars ℝ A.toSubalgebra)
hA_toReal : (Subalgebra.map (toContinuousMapₐ ℝ) A_toReal).SeparatesPoints
heq' : ∀ g ∈ A_toReal, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
f : E →ᵇ ℝ
h0 : Tendsto (fun ε ↦ 6 * √ε) (𝓝[>] 0) (𝓝 0)
lim1 : Tendsto (fun ε ↦ |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (f x) ∂P'|) (𝓝[>] 0) (𝓝 0)
⊢ ∫ (x : E), f x ∂P = ∫ (x : E), f x ∂P'

Tactic:
have lim2 : Tendsto (fun ε => |∫ x, mulExpNegMulSq ε (f x) ∂P
      - ∫ x, mulExpNegMulSq ε (f x) ∂P'|) (𝓝[>] 0)
      (𝓝 |∫ x, f x ∂↑P - ∫ x, f x ∂↑P'|) :=
    Tendsto.abs (Tendsto.sub (tendsto_integral_mulExpNegMulSq_comp f)
      (tendsto_integral_mulExpNegMulSq_comp f))

Goal state after:
E : Type u_1
𝕜 : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA : (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A).SeparatesPoints
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
A_toReal : Subalgebra ℝ (E →ᵇ ℝ) :=
  Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm ⋯) (Subalgebra.restrictScalars ℝ A.toSubalgebra)
hA_toReal : (Subalgebra.map (toContinuousMapₐ ℝ) A_toReal).SeparatesPoints
heq' : ∀ g ∈ A_toReal, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
f : E →ᵇ ℝ
h0 : Tendsto (fun ε ↦ 6 * √ε) (𝓝[>] 0) (𝓝 0)
lim1 : Tendsto (fun ε ↦ |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (f x) ∂P'|) (𝓝[>] 0) (𝓝 0)
lim2 :
  Tendsto (fun ε ↦ |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (f x) ∂P'|) (𝓝[>] 0)
    (𝓝 |∫ (x : E), f x ∂P - ∫ (x : E), f x ∂P'|)
⊢ ∫ (x : E), f x ∂P = ∫ (x : E), f x ∂P'
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
Λ✝ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : CompactSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
⊢ IsFiniteMeasure (rieszMeasure Λ)

Tactic:
constructor
  let o : C_c(X, ℝ) := ⟨1, HasCompactSupport.of_compactSpace 1⟩
  calc rieszMeasure Λ univ
  _ ≤ ENNReal.ofReal (Λ o) :=
    rieszMeasure_le_of_eq_one _ (fun x ↦ zero_le_one) isCompact_univ (fun x hx ↦ rfl)
  _ < ⊤ := by simp

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

Goal state before:
pp: μ : Measure ℝ
r : ℝ
inst✝ : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (fun x ↦ sinc (r * x)) μ
⊢ 2⁻¹ * r * ‖2 * (↑r)⁻¹ + 2 * ↑r⁻¹ - 2 * (2 * ↑r⁻¹) * ↑(∫ (x : ℝ), sinc (2 * r⁻¹ * x) ∂μ)‖ =
    2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun μ t‖

Tactic:
intervalIntegral.integral_sub intervalIntegrable_const intervalIntegrable_charFun,

Goal state after:
μ : Measure ℝ
r : ℝ
inst✝ : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (fun x ↦ sinc (r * x)) μ
⊢ 2⁻¹ * r * ‖2 * (↑r)⁻¹ + 2 * ↑r⁻¹ - 2 * (2 * ↑r⁻¹) * ↑(∫ (x : ℝ), sinc (2 * r⁻¹ * x) ∂μ)‖ =
    2⁻¹ * r * ‖(∫ (x : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1) - ∫ (x : ℝ) in -2 * r⁻¹..2 * r⁻¹, charFun μ 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
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C} ∈ f
g : E →C_c ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
⊢ ∫ (x : E), -‖g.toBoundedContinuousFunction‖ ∂↑μ ≤ ∫ (x : E), g x ∂↑μ

Tactic:
by
        gcongr
        · simp
        · exact g.continuous.integrable_of_hasCompactSupport g.hasCompactSupport
        · intro x
          apply neg_le_of_abs_le
          exact g.toBoundedContinuousFunction.norm_coe_le_norm x

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

Goal state before:
pp: α : 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
⊢ Dense (SetLike.coe ⁻¹' C)

Tactic:
by
  rw [EMetric.dense_iff]
  rintro s ε εpos
  rcases exists_measure_symmDiff_lt_of_generateFrom_isSetRing hC h'C h s.2 εpos with ⟨t, tC, ht⟩
  have t_meas : MeasurableSet t := by rw [h]; exact measurableSet_generateFrom tC
  refine ⟨⟨t, t_meas⟩, ?_, tC⟩
  simpa [MeasuredSets.edist_def] using! ht

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : MeasurableSpace 𝕜
a : A
inst✝⁵ : OpensMeasurableSpace 𝕜
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : CompleteSpace A
inst✝¹ : MeasurableSpace A
inst✝ : BorelSpace A
h1 : ContinuousOn (resolvent a) (resolventSet 𝕜 a)
⊢ ContinuousOn (resolvent a) (resolventSet 𝕜 a)ᶜ

Tactic:
continuousOn_iff_continuous_domRestrict

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : MeasurableSpace 𝕜
a : A
inst✝⁵ : OpensMeasurableSpace 𝕜
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : CompleteSpace A
inst✝¹ : MeasurableSpace A
inst✝ : BorelSpace A
h1 : ContinuousOn (resolvent a) (resolventSet 𝕜 a)
⊢ Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ((resolventSet 𝕜 a)ᶜ.domRestrict (resolvent a))
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
⊢ interior s ∩ μ.support ⊆ (μ.restrict s).support

Tactic:
rintro x ⟨hxs, hxμ⟩
  rw [mem_support_restrict, (nhdsWithin_basis_open x s).frequently_smallSets pos_mono]
  rw [(nhds_basis_opens x).mem_measureSupport] at hxμ
  rintro u ⟨hxu, hu⟩
  apply hxμ (u ∩ interior s) ⟨⟨hxu, hxs⟩, hu.inter isOpen_interior⟩ |>.trans_le
  gcongr
  exact interior_subset

Goal state after:
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 ≠ ∞
⊢ indicatorConstLp p ms hμs c ∈ closure {x | ∃ s, ∃ (hs : s ∈ 𝒜) (hμs : μ s ≠ ∞), indicatorConstLp p ⋯ hμs c = x}

Tactic:
refine Metric.mem_closure_iff.2 fun ε hε ↦ ?_

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
⊢ ∃ b ∈ {x | ∃ s, ∃ (hs : s ∈ 𝒜) (hμs : μ s ≠ ∞), indicatorConstLp p ⋯ hμs c = x},
    dist (indicatorConstLp p ms hμs c) b < ε
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 ∈ s, ‖resolvent w x ^ 2‖ ≤ (infDist a (⇑(algebraMap 𝕜 A) '' μ.support) / 2)⁻¹ ^ 2

Tactic:
w

Goal state after:
𝕜 : 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
⊢ w ∈ s → ‖resolvent w x ^ 2‖ ≤ (infDist a (⇑(algebraMap 𝕜 A) '' μ.support) / 2)⁻¹ ^ 2
Module: Mathlib.MeasureTheory.Measure.LevyConvergence

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
E : Type u_3
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : PolishSpace E
inst✝ : BorelSpace E
ι : Type u_4
𝓕 : Filter ι
μ : ι → ProbabilityMeasure E
h_tight : IsTightMeasureSet {x | ∃ n, ↑(μ n) = x}
μ₀ : ProbabilityMeasure E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA : (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A).SeparatesPoints
hμ : ∀ g ∈ A, Tendsto (fun n ↦ ∫ (x : E), g x ∂↑(μ n)) 𝓕 (𝓝 (∫ (x : E), g x ∂↑μ₀))
this : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace E := TopologicalSpace.upgradeIsCompletelyMetrizable E
h✝ : 𝓕.NeBot
U : Ultrafilter ι
hU : ↑U ≤ 𝓕
⊢ IsTightMeasureSet {x | ∃ μ_1 ∈ {x | ∃ n, μ n = x}, ↑μ_1 = x}

Tactic:
by simpa using h_tight

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) μ
resolvent'_bound : ∀ᵐ (x : 𝕜) ∂μ, ∀ w ∈ s, ‖resolvent w x ^ 2‖ ≤ (infDist a (⇑(algebraMap 𝕜 A) '' μ.support) / 2)⁻¹ ^ 2
x : 𝕜
hx : x ∈ μ.support
⊢ ∀ w ∈ s, HasDerivAt (fun w ↦ resolvent w x) (resolvent w x ^ 2) w

Tactic:
w

Goal state after:
𝕜 : 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) μ
resolvent'_bound : ∀ᵐ (x : 𝕜) ∂μ, ∀ w ∈ s, ‖resolvent w x ^ 2‖ ≤ (infDist a (⇑(algebraMap 𝕜 A) '' μ.support) / 2)⁻¹ ^ 2
x : 𝕜
hx : x ∈ μ.support
w : A
⊢ w ∈ s → HasDerivAt (fun w ↦ resolvent w x) (resolvent w x ^ 2) w
Module: Mathlib.MeasureTheory.Measure.LevyConvergence

Goal state before:
pp: case inr
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
E : Type u_3
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : PolishSpace E
inst✝ : BorelSpace E
ι : Type u_4
𝓕 : Filter ι
μ : ι → ProbabilityMeasure E
h_tight : IsTightMeasureSet {x | ∃ n, ↑(μ n) = x}
μ₀ : ProbabilityMeasure E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA : (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A).SeparatesPoints
hμ : ∀ g ∈ A, Tendsto (fun n ↦ ∫ (x : E), g x ∂↑(μ n)) 𝓕 (𝓝 (∫ (x : E), g x ∂↑μ₀))
this : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace E := TopologicalSpace.upgradeIsCompletelyMetrizable E
h✝ : 𝓕.NeBot
U : Ultrafilter ι
hU : ↑U ≤ 𝓕
h_compact : IsCompact (closure[instTopologicalSpace] {x | ∃ n, μ n = x})
μ' : ProbabilityMeasure E
hμ' : ∀ (f : E →ᵇ 𝕜), Tendsto (fun i ↦ ∫ (ω : E), f ω ∂↑(μ i)) (↑U) (𝓝 (∫ (ω : E), f ω ∂↑μ'))
g : E →ᵇ 𝕜
hg : g ∈ A
⊢ Tendsto ((fun n ↦ ∫ (x : E), g x ∂↑(μ n)) ∘ fun x ↦ x) U.1 (𝓝 (∫ (x : E), g x ∂↑μ'))

Tactic:
exact hμ' g

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_top : ∀ s ∉ C, m s = ∞
hs : s ∈ C
⊢ (OuterMeasure.ofFunction ⇑m ⋯).IsCaratheodory s

Tactic:
OuterMeasure.isCaratheodory_iff_le'

Goal state after:
α : 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 α),
    (OuterMeasure.ofFunction ⇑m ⋯) (t ∩ s) + (OuterMeasure.ofFunction ⇑m ⋯) (t \ s) ≤ (OuterMeasure.ofFunction ⇑m ⋯) t
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)
⊢ IsTightMeasureSet {x | ∃ μ ∈ S, ↑μ = x}

Tactic:
isTightMeasureSet_iff_exists_isCompact_measure_compl_le

Goal state after:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝³ : PseudoMetricSpace 𝓧
inst✝² : OpensMeasurableSpace 𝓧
inst✝¹ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
inst✝ : CompleteSpace 𝓧
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
⊢ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ ∈ {x | ∃ μ ∈ S, ↑μ = x}, μ Kᶜ ≤ ε
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
s t : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
hs : MeasurableSet s
ht : MeasurableSet t
hfs : μ.IntegrableOn f s
hts : t ⊆ s
⊢ ∫ᵛ (x : X) in s \ t ∪ t, f x ∂[B; μ] = ∫ᵛ (x : X) in s, f x ∂[B; μ]

Tactic:
sdiff_union_of_subset hts

Goal state after:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
s t : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
hs : MeasurableSet s
ht : MeasurableSet t
hfs : μ.IntegrableOn f s
hts : t ⊆ s
⊢ ∫ᵛ (x : X) in s, f x ∂[B; μ] = ∫ᵛ (x : X) in s, f x ∂[B; μ]
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: case a
α : 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)
n : ℕ
this : ⋃ i, f i = (⋃ i ∈ Finset.range n, f i) ∪ ⋃ i ∈ Set.Ici n, f i
⊢ MeasurableSet (⋃ i ∈ Set.Ici n, f i)

pp: case a
α : 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)
n : ℕ
this : ⋃ i, f i = (⋃ i ∈ Finset.range n, f i) ∪ ⋃ i ∈ Set.Ici n, f i
⊢ Disjoint (⋃ i ∈ Finset.range n, f i) (⋃ i ∈ Set.Ici n, f i)

Tactic:
· exact MeasurableSet.biUnion (Set.to_countable _) (fun i hi ↦ f_meas i)

Goal state after:
case a
α : 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)
n : ℕ
this : ⋃ i, f i = (⋃ i ∈ Finset.range n, f i) ∪ ⋃ i ∈ Set.Ici n, f i
⊢ Disjoint (⋃ i ∈ Finset.range n, f i) (⋃ i ∈ Set.Ici n, f i)
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✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, μ (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s | ∃ c ∈ C, ↑s = c}
C'C : ∀ s ∈ C', ↑s ∈ C
C'_dense : Dense C'
m₀ : ↑C' → E := fun x ↦ m ↑↑x
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ μ ↑s
s t : MeasuredSets μ
h : Disjoint ↑s ↑t
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : 8 * δ = ε
s' : Set α
s'C : s' ∈ C
hs' : μ (s' ∆ ↑s) < δ
t' : Set α
t'C : t' ∈ C
ht' : μ (t' ∆ ↑t) < δ
It : ‖m t' - m₁ t‖ₑ < δ
hμ' : μ (s' ∩ t') < 2 * δ
s'' : Set α := s' \ t'
s''C : s'' ∈ C
⊢ ‖m₁ ⟨↑s ∪ ↑t, ⋯⟩ - m₁ s - m₁ t‖ₑ < ε

Tactic:
have hs'' : μ (s'' ∆ s) < 3 * δ := calc
      μ (s'' ∆ s)
      _ ≤ μ (s'' ∆ s') + μ (s' ∆ s) := measure_symmDiff_le _ _ _
      _ < 2 * δ + δ := by gcongr; simp [s'', symmDiff, hμ']
      _ = 3 * δ := by ring

Goal state after:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, μ (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s | ∃ c ∈ C, ↑s = c}
C'C : ∀ s ∈ C', ↑s ∈ C
C'_dense : Dense C'
m₀ : ↑C' → E := fun x ↦ m ↑↑x
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ μ ↑s
s t : MeasuredSets μ
h : Disjoint ↑s ↑t
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : 8 * δ = ε
s' : Set α
s'C : s' ∈ C
hs' : μ (s' ∆ ↑s) < δ
t' : Set α
t'C : t' ∈ C
ht' : μ (t' ∆ ↑t) < δ
It : ‖m t' - m₁ t‖ₑ < δ
hμ' : μ (s' ∩ t') < 2 * δ
s'' : Set α := s' \ t'
s''C : s'' ∈ C
hs'' : μ (s'' ∆ ↑s) < 3 * δ
⊢ ‖m₁ ⟨↑s ∪ ↑t, ⋯⟩ - m₁ s - m₁ t‖ₑ < ε