mathlib-initiative/mathlib-tactics huggingface dataset:
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
g : E →ᵇ ℝ
hgA_toReal : g ∈ A_toReal
⊢ ∫ (x : E), ↑(g x) ∂P = ↑(∫ (x : E), g x ∂P')

Tactic:
← integral_ofReal

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
g : E →ᵇ ℝ
hgA_toReal : g ∈ A_toReal
⊢ ∫ (x : E), ↑(g x) ∂P = ∫ (x : E), ↑(g x) ∂P'
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_3
inst✝⁶ : MeasurableSpace E
μ ν : Measure E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
t : E
⊢ Integrable (fun x ↦ cexp (↑⟪x, t⟫ * I)) (μ ∗ ν)

Tactic:
· exact (integrable_const (1 : ℝ)).mono (by fun_prop) (by simp)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
p : ℝ≥0∞
inst✝² : Fact (1 ≤ p)
inst✝¹ : SFinite μ
inst✝ : SFinite ν
L : StrongDual ℝ (WithLp p (E × F))
⊢ charFunDual (Measure.map (toLp p) (μ.prod ν)) L =
    charFunDual μ (L ∘SL ↑(prodContinuousLinearEquiv p ℝ E F).symm ∘SL ContinuousLinearMap.inl ℝ E F) *
      charFunDual ν (L ∘SL ↑(prodContinuousLinearEquiv p ℝ E F).symm ∘SL ContinuousLinearMap.inr ℝ E F)

Tactic:
simp_rw [charFunDual_apply, ← integral_prod_mul, ← Complex.exp_add, ← add_mul, ← ofReal_add,
    L.comp_apply, ← map_add, ContinuousLinearMap.comp_inl_add_comp_inr]
  rw [← MeasurableEquiv.coe_toLp, integral_map_equiv]
  simp

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: p : ℝ≥0∞
inst✝⁵ : Fact (1 ≤ p)
ι : Type u_4
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
E : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
L : StrongDual ℝ (PiLp p E)
⊢ ∫ (v : WithLp p ((i : ι) → E i)), cexp (↑(L v) * I) ∂Measure.map (toLp p) (Measure.pi μ) =
    ∫ (x : (i : ι) → E i),
      ∏ i,
        cexp
          (↑((L ∘SL ↑(PiLp.continuousLinearEquiv p ℝ E).symm ∘SL ContinuousLinearMap.single ℝ E i) (x i)) *
            I) ∂Measure.pi μ

Tactic:
← Complex.exp_sum,

Goal state after:
p : ℝ≥0∞
inst✝⁵ : Fact (1 ≤ p)
ι : Type u_4
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
E : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
L : StrongDual ℝ (PiLp p E)
⊢ ∫ (v : WithLp p ((i : ι) → E i)), cexp (↑(L v) * I) ∂Measure.map (toLp p) (Measure.pi μ) =
    ∫ (x : (i : ι) → E i),
      cexp
        (∑ x_1,
          ↑((L ∘SL ↑(PiLp.continuousLinearEquiv p ℝ E).symm ∘SL ContinuousLinearMap.single ℝ E x_1) (x x_1)) *
            I) ∂Measure.pi μ
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
μ ν : Measure E
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
L : StrongDual ℝ E
⊢ Integrable (fun v ↦ cexp (↑(L v) * I)) (μ ∗ ν)

Tactic:
· exact (integrable_const (1 : ℝ)).mono (by fun_prop) (by simp)

Goal state after:
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✝ : IsFiniteMeasure μ
K : Set X
hK : IsCompact K
h : μ Kᶜ = 0
⊢ ∃ ν, ν.InnerRegular ∧ IsFiniteMeasure ν ∧ ν Kᶜ = 0 ∧ ∀ (g : X →ᵇ ℝ), ∫ (x : X), g x ∂μ = ∫ (x : X), g x ∂ν

Tactic:
let μ' : Measure K := μ.comap Subtype.val

Goal state after:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
K : Set X
hK : IsCompact K
h : μ Kᶜ = 0
μ' : Measure ↑K := Measure.comap Subtype.val μ
⊢ ∃ ν, ν.InnerRegular ∧ IsFiniteMeasure ν ∧ ν Kᶜ = 0 ∧ ∀ (g : X →ᵇ ℝ), ∫ (x : X), g x ∂μ = ∫ (x : X), g x ∂ν
Module: Mathlib.MeasureTheory.Measure.IntegralCharFun

Goal state before:
pp: μ : Measure ℝ
r : ℝ
inst✝ : IsFiniteMeasure μ
hr : 0 < r
h_int : Integrable (Function.uncurry fun x y ↦ cexp (↑x * ↑y * I)) ((volume.restrict (Set.uIoc (-r) r)).prod μ)
y : ℝ
hry : ¬r * y = 0
hy : y = 0
⊢ r * y = 0

Tactic:
simp [hy]

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 * ‖∫ (x : ℝ), 1 - sinc (2 * r⁻¹ * x) ∂μ‖ =
    2⁻¹ * r * ‖2 * (2 * r⁻¹) - 2 * (2 * r⁻¹) * ∫ (x : ℝ), sinc (2 * r⁻¹ * x) ∂μ‖

Tactic:
mul_assoc 2,

Goal state after:
μ : Measure ℝ
r : ℝ
inst✝ : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (fun x ↦ sinc (r * x)) μ
⊢ 2 * ‖∫ (x : ℝ), 1 - sinc (2 * r⁻¹ * x) ∂μ‖ =
    2⁻¹ * r * ‖2 * (2 * r⁻¹) - 2 * (2 * r⁻¹ * ∫ (x : ℝ), sinc (2 * r⁻¹ * x) ∂μ)‖
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : Nontrivial E
k : ℕ
hk : finrank ℝ E = 2 * k
x : E
r : ℝ
⊢ volume (ball x r) = ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k / ↑k !)

Tactic:
rw [volume_ball, hk, pow_mul, pow_mul, sq_sqrt pi_nonneg]
  congr
  simp [Gamma_nat_eq_factorial]

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

Goal state before:
pp: E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst✝ : PseudoMetricSpace E
hS : IsTightMeasureSet S
x : E
⊢ Tendsto (fun r ↦ (Metric.closedBall x r)ᶜ) atTop (Bornology.cobounded E).smallSets

Tactic:
exact (Metric.hasAntitoneBasis_cobounded_compl_closedBall _).tendsto_smallSets

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

Goal state before:
pp: case inl
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 : Subsingleton E
⊢ IsTightMeasureSet S

Tactic:
simp only [IsTightMeasureSet, cocompact_eq_bot, smallSets_bot]
    convert! tendsto_pure_nhds (a := ∅) _
    simp

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 : 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
D : Set (Set α)
D_count : D.Countable
DC : D ⊆ C
hD : μ (⋃₀ D)ᶜ = 0
⊢ D ∪ {∅} ⊆ C ∧ μ (⋃₀ (D ∪ {∅}))ᶜ = 0 ∧ (D ∪ {∅}).Nonempty

Tactic:
simp only [union_subset_iff, DC, singleton_subset_iff, true_and, and_true, hC.empty_mem]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
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
D : Set (Set α)
D_count : D.Countable
DC : D ⊆ C
hD : μ (⋃₀ D)ᶜ = 0
⊢ μ (⋃₀ (D ∪ {∅}))ᶜ = 0 ∧ (D ∪ {∅}).Nonempty
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 μ✝
inst✝ : IsFiniteMeasure ν
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ) (g : (j : κ) → Y j →ᵇ ℝ),
    ∫ (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) ∂ν
f : (i : ι) → X i →ᵇ ℝ≥0
g : (j : κ) → Y j →ᵇ ℝ≥0
μ : Measure (((i : ι) → X i) × ((j : κ) → Y j))
⊢ (∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), (∏ i, ↑((f i) (p.1 i))) * ∏ j, ↑((g j) (p.2 j)) ∂μ).toReal =
    (∫⁻ (a : ((i : ι) → X i) × ((j : κ) → Y j)),
        ENNReal.ofReal ((∏ i, ↑((f i) (a.1 i))) * ∏ j, ↑((g j) (a.2 j))) ∂μ).toReal

Tactic:
simp [Finset.prod_nonneg, ofReal_prod_of_nonneg]

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
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 ∈ C, μ (t ∆ ⋃ i, f i) < ε

Tactic:
have A i : ∃ t ∈ C, μ (t ∆ (f i)) < δ i := hf i _ (δpos i)

Goal state after:
α : 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
A : ∀ (i : ℕ), ∃ t ∈ C, μ (t ∆ f i) < δ i
⊢ ∃ t ∈ C, μ (t ∆ ⋃ i, f i) < ε
Module: Mathlib.MeasureTheory.Measure.PreVariation

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
x✝ : Set X
h : ¬MeasurableSet x✝
⊢ preVariationFun f x✝ = 0

Tactic:
by simp [preVariationFun, h]

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
⊢ x ∈ μ.supportᶜ ↔ x ∈ ⋃₀ {t | IsOpen[inst✝¹] t ∧ μ t = 0}

Tactic:
simp only [Set.mem_compl_iff, Set.mem_sUnion, Set.mem_ofPred_eq, and_right_comm,
    nhds_basis_opens x |>.notMem_measureSupport, fun t ↦ and_comm (b := x ∈ t)]

Goal state after:
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
this : μ (s ∩ t)ᶜ ≤ 0
⊢ False

Tactic:
rw [measure_compl (hs.inter ht) (by simp), measure_univ ‹_›] at this

Goal state after:
α : 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
this : 1 - μ (s ∩ t) ≤ 0
⊢ False
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: case pos
α : 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)
hBn : μ (⋂ n, B n) = 1
x₀ : α
hx₀ : ⋂ n, B n = {x₀}
s : Set α
hs : MeasurableSet s
h : x₀ ∈ s
⊢ μ s = (Measure.dirac x₀) s

pp: case neg
α : 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)
hBn : μ (⋂ n, B n) = 1
x₀ : α
hx₀ : ⋂ n, B n = {x₀}
s : Set α
hs : MeasurableSet s
h : x₀ ∉ s
⊢ μ s = (Measure.dirac x₀) s

Tactic:
· simp [h]
    have : μ {x₀} ≤ μ s := measure_mono (μ := μ) (by grind)
    rw [← hx₀, hBn] at this
    simp_all

Goal state after:
case neg
α : 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)
hBn : μ (⋂ n, B n) = 1
x₀ : α
hx₀ : ⋂ n, B n = {x₀}
s : Set α
hs : MeasurableSet s
h : x₀ ∉ s
⊢ μ s = (Measure.dirac x₀) s
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Defs

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
V : Type u_2
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
⊢ IsSigmaSubadditiveSetFun fun x ↦ ‖μ x‖ₑ

Tactic:
intro s hs
  have hmeas : ∀ i, MeasurableSet (s i).val := fun i => (s i).prop
  simpa [VectorMeasure.of_disjoint_iUnion hmeas hs] using enorm_tsum_le_tsum_enorm

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

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝³ : PseudoMetricSpace 𝓧
inst✝² : OpensMeasurableSpace 𝓧
inst✝¹ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
inst✝ : CompleteSpace 𝓧
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
hnonempty : Nonempty 𝓧
D : ℕ → 𝓧
hD : DenseRange D
u : ℕ → ℝ
hu_anti : StrictAnti u
hu_pos : ∀ (n : ℕ), 0 < u n
hu : Tendsto u atTop (𝓝 0)
m : ℕ
⊢ ⋃ i, ball (D i) (u m) = univ

Tactic:
rw [denseRange_iff] at hD

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)
hnonempty : Nonempty 𝓧
D : ℕ → 𝓧
hD : ∀ (x : 𝓧), ∀ r > 0, ∃ y, dist x (D y) < r
u : ℕ → ℝ
hu_anti : StrictAnti u
hu_pos : ∀ (n : ℕ), 0 < u n
hu : Tendsto u atTop (𝓝 0)
m : ℕ
⊢ ⋃ i, ball (D i) (u m) = univ
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Goal state before:
pp: X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
s : Set X
hs : MeasurableSet s
t : Set X
ht : MeasurableSet t
⊢ μ.variation (t ∩ s) ≤ (μ.restrict s).variation (t ∩ s)

Tactic:
by
      apply variation_apply_le_of_forall_enorm_le (ht.inter hs) (fun u u_meas hu ↦ ?_)
      have : μ u = μ.restrict s u :=
        (VectorMeasure.restrict_eq_self _ hs u_meas (hu.trans inter_subset_right)).symm
      rw [this]
      apply enorm_measure_le_variation

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

Goal state before:
pp: case inr.inr.refine_1
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝³ : PseudoMetricSpace 𝓧
inst✝² : OpensMeasurableSpace 𝓧
inst✝¹ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
inst✝ : CompleteSpace 𝓧
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
hnonempty : Nonempty 𝓧
D : ℕ → 𝓧
hD : DenseRange D
u : ℕ → ℝ
hu_anti : StrictAnti u
hu_pos : ∀ (n : ℕ), 0 < u n
hu : Tendsto u atTop (𝓝 0)
hcov : ∀ (m : ℕ), ⋃ i, ball (D i) (u m) = univ
ε : ℝ≥0∞
εpos : 0 < ε
hεbound : ε ≤ 1
km : ℕ → ℕ
hbound : ∀ (m : ℕ), ∀ μ ∈ S, 1 - ε * 2 ^ (-↑m) < ↑(μ (⋃ i, ⋃ (_ : i ≤ km m), ball (D i) (u m)))
bigK : Set 𝓧 :=
  ⋂ m, ⋃ i, ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m))
bigcalc : ∀ μ ∈ S, ↑μ bigKᶜ ≤ ε
δ : ℝ
δpos : δ > 0
δ_inv : ℕ
hδ_inv : u δ_inv < δ
⊢ ∃ t, t.Finite ∧ bigK ⊆ ⋃ y ∈ t, ball y δ

Tactic:
refine ⟨D '' .Iic (km (δ_inv + 1)), (Set.finite_Iic _).image _, ?_⟩

Goal state after:
case inr.inr.refine_1
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝³ : PseudoMetricSpace 𝓧
inst✝² : OpensMeasurableSpace 𝓧
inst✝¹ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
inst✝ : CompleteSpace 𝓧
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
hnonempty : Nonempty 𝓧
D : ℕ → 𝓧
hD : DenseRange D
u : ℕ → ℝ
hu_anti : StrictAnti u
hu_pos : ∀ (n : ℕ), 0 < u n
hu : Tendsto u atTop (𝓝 0)
hcov : ∀ (m : ℕ), ⋃ i, ball (D i) (u m) = univ
ε : ℝ≥0∞
εpos : 0 < ε
hεbound : ε ≤ 1
km : ℕ → ℕ
hbound : ∀ (m : ℕ), ∀ μ ∈ S, 1 - ε * 2 ^ (-↑m) < ↑(μ (⋃ i, ⋃ (_ : i ≤ km m), ball (D i) (u m)))
bigK : Set 𝓧 :=
  ⋂ m, ⋃ i, ⋃ (_ : i ≤ km (m + 1)), closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball (D i) (u m))
bigcalc : ∀ μ ∈ S, ↑μ bigKᶜ ≤ ε
δ : ℝ
δpos : δ > 0
δ_inv : ℕ
hδ_inv : u δ_inv < δ
⊢ bigK ⊆ ⋃ y ∈ D '' Iic (km (δ_inv + 1)), ball y δ
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ μ s
inst✝ : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
⊢ m ∅ = 0

Tactic:
simpa using h'm ∅ ∅ MeasurableSet.empty MeasurableSet.empty (by simp)

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

Goal state before:
pp: α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ μ s
inst✝ : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
⊢ Filter.Tendsto (fun n ↦ ∑ i ∈ Finset.range n, m (f i)) Filter.atTop (nhds (m (⋃ i, f i)))

Tactic:
apply tendsto_iff_norm_sub_tendsto_zero.2

Goal state after:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ μ s
inst✝ : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
⊢ Filter.Tendsto (fun e ↦ ‖∑ i ∈ Finset.range e, m (f i) - m (⋃ i, f i)‖) Filter.atTop (nhds 0)
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ μ s
inst✝ : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
⊢ Filter.Tendsto (fun e ↦ ‖∑ i ∈ Finset.range e, m (f i) - m (⋃ i, f i)‖) Filter.atTop (nhds 0)

Tactic:
norm_sub_rev,

Goal state after:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ μ s
inst✝ : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
⊢ Filter.Tendsto (fun e ↦ ‖m (⋃ i, f i) - ∑ i ∈ Finset.range e, m (f i)‖) Filter.atTop (nhds 0)
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: case zero
α : 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)
⊢ m (⋃ i ∈ Finset.range 0, f i) = ∑ i ∈ Finset.range 0, m (f i)

Tactic:
simpa using h'm ∅ ∅ MeasurableSet.empty MeasurableSet.empty (by simp)

Goal state after:
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
h'α : Nonempty α
m : AddContent E {s | ∃ u v, u ≤ v ∧ s = Ioc u v} := AddContent.onIoc (Function.rightLim f)
u v : α
huv : u ≤ v
⊢ eVariationOn (Function.rightLim f) (Icc u v) ≠ ∞

Tactic:
exact ((eVariationOn.mono _ (subset_univ _)).trans_lt hf.rightLim.lt_top).ne

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

Goal state before:
pp: case succ
X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
h : μ.semivariation univ = ∞
t : Set X → Set X
t_meas : ∀ (s : Set X), MeasurableSet s → μ.semivariation s = ∞ → MeasurableSet (t s)
t_subs : ∀ (s : Set X), MeasurableSet s → μ.semivariation s = ∞ → t s ⊆ s
t_var : ∀ (s : Set X), MeasurableSet s → μ.semivariation s = ∞ → μ.semivariation (t s) = ∞
ht : ∀ (s : Set X), MeasurableSet s → μ.semivariation s = ∞ → 1 ≤ ‖μ (s \ t s)‖ₑ
s : ℕ → Set X := fun n ↦ t^[n] univ
n : ℕ
ih : MeasurableSet (s n) ∧ μ.semivariation (s n) = ∞
⊢ MeasurableSet (s (n + 1)) ∧ μ.semivariation (s (n + 1)) = ∞

Tactic:
simp only [Function.iterate_succ', Function.comp_apply, s]
      exact ⟨t_meas _ ih.1 ih.2, t_var _ ih.1 ih.2⟩

Goal state after: