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

Goal state before:
pp: case e'_2
κ : Type u_2
Z : Type u_3
Y : κ → Type u_6
mY : (j : κ) → MeasurableSpace (Y j)
inst✝⁸ : (j : κ) → TopologicalSpace (Y j)
inst✝⁷ : ∀ (j : κ), BorelSpace (Y j)
inst✝⁶ : ∀ (j : κ), HasOuterApproxClosed (Y j)
mZ : MeasurableSpace Z
inst✝⁵ : TopologicalSpace Z
inst✝⁴ : BorelSpace Z
inst✝³ : HasOuterApproxClosed Z
inst✝² : Finite κ
μ ν : Measure (Z × ((i : κ) → Y i))
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h :
  ∀ (f : Z →ᵇ ℝ) (g : ((j : κ) → Y j) →ᵇ ℝ),
    ∫ (p : Z × ((i : κ) → Y i)), f p.1 * g p.2 ∂μ = ∫ (p : Z × ((i : κ) → Y i)), f p.1 * g p.2 ∂ν
this : Fintype κ
f : Z →ᵇ ℝ
g : (j : κ) → Y j →ᵇ ℝ
x✝ : Z × ((j : κ) → Y j)
⊢ ∏ j, (g j) (x✝.2 j) = (∏ j, (g j).compContinuous { toFun := Function.eval j, continuous_toFun := ⋯ }) x✝.2

pp: case e'_3
κ : Type u_2
Z : Type u_3
Y : κ → Type u_6
mY : (j : κ) → MeasurableSpace (Y j)
inst✝⁸ : (j : κ) → TopologicalSpace (Y j)
inst✝⁷ : ∀ (j : κ), BorelSpace (Y j)
inst✝⁶ : ∀ (j : κ), HasOuterApproxClosed (Y j)
mZ : MeasurableSpace Z
inst✝⁵ : TopologicalSpace Z
inst✝⁴ : BorelSpace Z
inst✝³ : HasOuterApproxClosed Z
inst✝² : Finite κ
μ ν : Measure (Z × ((i : κ) → Y i))
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h :
  ∀ (f : Z →ᵇ ℝ) (g : ((j : κ) → Y j) →ᵇ ℝ),
    ∫ (p : Z × ((i : κ) → Y i)), f p.1 * g p.2 ∂μ = ∫ (p : Z × ((i : κ) → Y i)), f p.1 * g p.2 ∂ν
this : Fintype κ
f : Z →ᵇ ℝ
g : (j : κ) → Y j →ᵇ ℝ
x✝ : Z × ((j : κ) → Y j)
⊢ ∏ j, (g j) (x✝.2 j) = (∏ j, (g j).compContinuous { toFun := Function.eval j, continuous_toFun := ⋯ }) x✝.2

Tactic:
<;>

Goal state after:
case e'_2
κ : Type u_2
Z : Type u_3
Y : κ → Type u_6
mY : (j : κ) → MeasurableSpace (Y j)
inst✝⁸ : (j : κ) → TopologicalSpace (Y j)
inst✝⁷ : ∀ (j : κ), BorelSpace (Y j)
inst✝⁶ : ∀ (j : κ), HasOuterApproxClosed (Y j)
mZ : MeasurableSpace Z
inst✝⁵ : TopologicalSpace Z
inst✝⁴ : BorelSpace Z
inst✝³ : HasOuterApproxClosed Z
inst✝² : Finite κ
μ ν : Measure (Z × ((i : κ) → Y i))
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h :
  ∀ (f : Z →ᵇ ℝ) (g : ((j : κ) → Y j) →ᵇ ℝ),
    ∫ (p : Z × ((i : κ) → Y i)), f p.1 * g p.2 ∂μ = ∫ (p : Z × ((i : κ) → Y i)), f p.1 * g p.2 ∂ν
this : Fintype κ
f : Z →ᵇ ℝ
g : (j : κ) → Y j →ᵇ ℝ
x✝ : Z × ((j : κ) → Y j)
⊢ ∏ j, (g j) (x✝.2 j) = (∏ j, (g j).compContinuous { toFun := Function.eval j, continuous_toFun := ⋯ }) x✝.2

case e'_3
κ : Type u_2
Z : Type u_3
Y : κ → Type u_6
mY : (j : κ) → MeasurableSpace (Y j)
inst✝⁸ : (j : κ) → TopologicalSpace (Y j)
inst✝⁷ : ∀ (j : κ), BorelSpace (Y j)
inst✝⁶ : ∀ (j : κ), HasOuterApproxClosed (Y j)
mZ : MeasurableSpace Z
inst✝⁵ : TopologicalSpace Z
inst✝⁴ : BorelSpace Z
inst✝³ : HasOuterApproxClosed Z
inst✝² : Finite κ
μ ν : Measure (Z × ((i : κ) → Y i))
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h :
  ∀ (f : Z →ᵇ ℝ) (g : ((j : κ) → Y j) →ᵇ ℝ),
    ∫ (p : Z × ((i : κ) → Y i)), f p.1 * g p.2 ∂μ = ∫ (p : Z × ((i : κ) → Y i)), f p.1 * g p.2 ∂ν
this : Fintype κ
f : Z →ᵇ ℝ
g : (j : κ) → Y j →ᵇ ℝ
x✝ : Z × ((j : κ) → Y j)
⊢ ∏ j, (g j) (x✝.2 j) = (∏ j, (g j).compContinuous { toFun := Function.eval j, continuous_toFun := ⋯ }) x✝.2
Module: Mathlib.MeasureTheory.Measure.Support

Goal state before:
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:
intro x hxK

Goal state after:
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 : X
hxK : x ∈ K
⊢ ∃ t ∈ 𝓝[K] x, μ t = 0
Module: Mathlib.MeasureTheory.Measure.Support

Goal state before:
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:
· intro x hxK
    obtain ⟨U, hUnhds, hU0⟩ := notMem_support_iff_exists.1 (hKsub hxK)
    exact ⟨U, mem_nhdsWithin_of_mem_nhds hUnhds, hU0⟩

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: case inl
α : 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
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
h✝ : μ s = 0
⊢ μ (s ∩ t) = 1

pp: case inr
α : 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
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
hμs : μ s = 1
⊢ μ (s ∩ t) = 1

Tactic:
<;>

Goal state after:
case inl
α : 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
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
h✝ : μ s = 0
⊢ μ (s ∩ t) = 1

case inr
α : 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
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
hμs : μ s = 1
⊢ μ (s ∩ t) = 1
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: case inl.inl
α : 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
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
h✝¹ : μ s = 0
h✝ : μ t = 0
⊢ μ (s ∩ t) = 1

pp: case inl.inr
α : 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
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
h✝ : μ s = 0
hμt : μ t = 1
⊢ μ (s ∩ t) = 1

pp: case inr.inl
α : 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
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
hμs : μ s = 1
h✝ : μ t = 0
⊢ μ (s ∩ t) = 1

pp: case inr.inr
α : 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
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
hμs : μ s = 1
hμt : μ t = 1
⊢ μ (s ∩ t) = 1

Tactic:
<;>

Goal state after:
case inl.inl
α : 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
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
h✝¹ : μ s = 0
h✝ : μ t = 0
⊢ μ (s ∩ t) = 1

case inl.inr
α : 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
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
h✝ : μ s = 0
hμt : μ t = 1
⊢ μ (s ∩ t) = 1

case inr.inl
α : 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
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
hμs : μ s = 1
h✝ : μ t = 0
⊢ μ (s ∩ t) = 1

case inr.inr
α : 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
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
hμs : μ s = 1
hμt : μ t = 1
⊢ μ (s ∩ t) = 1
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: case inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
h✝ : μ s = 0
⊢ μ (s ∩ t) = μ s * μ t

pp: case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
h✝ : μ s = 1
⊢ μ (s ∩ t) = μ s * μ t

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
h✝ : μ s = 0
⊢ μ (s ∩ t) = μ s * μ t

case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
h✝ : μ s = 1
⊢ μ (s ∩ t) = μ s * μ t
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: case inl.inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
h✝¹ : μ s = 0
h✝ : μ t = 0
⊢ μ (s ∩ t) = μ s * μ t

pp: case inl.inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
h✝¹ : μ s = 0
h✝ : μ t = 1
⊢ μ (s ∩ t) = μ s * μ t

pp: case inr.inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
h✝¹ : μ s = 1
h✝ : μ t = 0
⊢ μ (s ∩ t) = μ s * μ t

pp: case inr.inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
h✝¹ : μ s = 1
h✝ : μ t = 1
⊢ μ (s ∩ t) = μ s * μ t

Tactic:
<;>

Goal state after:
case inl.inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
h✝¹ : μ s = 0
h✝ : μ t = 0
⊢ μ (s ∩ t) = μ s * μ t

case inl.inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
h✝¹ : μ s = 0
h✝ : μ t = 1
⊢ μ (s ∩ t) = μ s * μ t

case inr.inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
h✝¹ : μ s = 1
h✝ : μ t = 0
⊢ μ (s ∩ t) = μ s * μ t

case inr.inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
h✝¹ : μ s = 1
h✝ : μ t = 1
⊢ μ (s ∩ t) = μ s * μ t
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

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

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

Tactic:
· exact h₀

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

Goal state before:
pp: case pos
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsUpperSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∈ closure s
⊢ x ∈
    {x |
        (fun x ↦
            Tendsto (fun r ↦ volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0)
              (𝓝 ((closure s).indicator 1 x)))
          x}ᶜ

pp: case neg
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsUpperSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∉ closure s
⊢ x ∈
    {x |
        (fun x ↦
            Tendsto (fun r ↦ volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0)
              (𝓝 ((closure s).indicator 1 x)))
          x}ᶜ

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsUpperSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∈ closure s
⊢ x ∈
    {x |
        (fun x ↦
            Tendsto (fun r ↦ volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0)
              (𝓝 ((closure s).indicator 1 x)))
          x}ᶜ

case neg
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsUpperSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∉ closure s
⊢ x ∈
    {x |
        (fun x ↦
            Tendsto (fun r ↦ volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0)
              (𝓝 ((closure s).indicator 1 x)))
          x}ᶜ
Module: Mathlib.MeasureTheory.Order.UpperLower

Goal state before:
pp: case pos
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsLowerSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∈ closure s
⊢ x ∈
    {x |
        (fun x ↦
            Tendsto (fun r ↦ volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0)
              (𝓝 ((closure s).indicator 1 x)))
          x}ᶜ

pp: case neg
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsLowerSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∉ closure s
⊢ x ∈
    {x |
        (fun x ↦
            Tendsto (fun r ↦ volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0)
              (𝓝 ((closure s).indicator 1 x)))
          x}ᶜ

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsLowerSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∈ closure s
⊢ x ∈
    {x |
        (fun x ↦
            Tendsto (fun r ↦ volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0)
              (𝓝 ((closure s).indicator 1 x)))
          x}ᶜ

case neg
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsLowerSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∉ closure s
⊢ x ∈
    {x |
        (fun x ↦
            Tendsto (fun r ↦ volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0)
              (𝓝 ((closure s).indicator 1 x)))
          x}ᶜ
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)
hempty : univ = ∅
ε : ℝ≥0∞
εpos : 0 < ε
⊢ ∀ μ ∈ {x | ∃ μ ∈ S, ↑μ = x}, μ ∅ᶜ ≤ ε

Tactic:
by simp [hempty]

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

Goal state before:
pp: case h₁
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝³ : TopologicalSpace V
inst✝² : ENormedAddCommMonoid V
inst✝¹ : T2Space V
μ ν : VectorMeasure X V
inst✝ : ContinuousAdd V
E : Set X
x✝ : MeasurableSet E
⊢ ‖μ E‖ₑ ≤ μ.variation E

pp: case h₂
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝³ : TopologicalSpace V
inst✝² : ENormedAddCommMonoid V
inst✝¹ : T2Space V
μ ν : VectorMeasure X V
inst✝ : ContinuousAdd V
E : Set X
x✝ : MeasurableSet E
⊢ ‖ν E‖ₑ ≤ ν.variation E

Tactic:
<;>

Goal state after:
case h₁
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝³ : TopologicalSpace V
inst✝² : ENormedAddCommMonoid V
inst✝¹ : T2Space V
μ ν : VectorMeasure X V
inst✝ : ContinuousAdd V
E : Set X
x✝ : MeasurableSet E
⊢ ‖μ E‖ₑ ≤ μ.variation E

case h₂
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝³ : TopologicalSpace V
inst✝² : ENormedAddCommMonoid V
inst✝¹ : T2Space V
μ ν : VectorMeasure X V
inst✝ : ContinuousAdd V
E : Set X
x✝ : MeasurableSet E
⊢ ‖ν E‖ₑ ≤ ν.variation E
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Goal state before:
pp: case pos
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
x : X
v : V
s : Set X
hs : MeasurableSet s
hx : x ∈ s
⊢ ‖(dirac x v) s‖ₑ ≤ (‖v‖ₑ • Measure.dirac x) s

pp: case neg
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
x : X
v : V
s : Set X
hs : MeasurableSet s
hx : x ∉ s
⊢ ‖(dirac x v) s‖ₑ ≤ (‖v‖ₑ • Measure.dirac x) s

Tactic:
<;>

Goal state after:
case pos
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
x : X
v : V
s : Set X
hs : MeasurableSet s
hx : x ∈ s
⊢ ‖(dirac x v) s‖ₑ ≤ (‖v‖ₑ • Measure.dirac x) s

case neg
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
x : X
v : V
s : Set X
hs : MeasurableSet s
hx : x ∉ s
⊢ ‖(dirac x v) s‖ₑ ≤ (‖v‖ₑ • Measure.dirac x) s
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Goal state before:
pp: case pos
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
x : X
v : V
s : Set X
hs : MeasurableSet s
hx : x ∈ s
⊢ (‖v‖ₑ • Measure.dirac x) s ≤ ‖(dirac x v) s‖ₑ

pp: case neg
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
x : X
v : V
s : Set X
hs : MeasurableSet s
hx : x ∉ s
⊢ (‖v‖ₑ • Measure.dirac x) s ≤ ‖(dirac x v) s‖ₑ

Tactic:
<;>

Goal state after:
case pos
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
x : X
v : V
s : Set X
hs : MeasurableSet s
hx : x ∈ s
⊢ (‖v‖ₑ • Measure.dirac x) s ≤ ‖(dirac x v) s‖ₑ

case neg
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
x : X
v : V
s : Set X
hs : MeasurableSet s
hx : x ∉ s
⊢ (‖v‖ₑ • Measure.dirac x) s ≤ ‖(dirac x v) s‖ₑ
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
a : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : {a} = ⋂ n, Ioc (u n) a
⊢ Tendsto (fun n ↦ hf.vectorMeasure (Ioc (u n) a)) atTop (𝓝 (hf.vectorMeasure (⋂ n, Ioc (u n) a)))

Tactic:
apply VectorMeasure.tendsto_vectorMeasure_iInter_atTop_nat ?_ (fun n ↦ measurableSet_Ioc)

Goal state after:
α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
a : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : {a} = ⋂ n, Ioc (u n) a
⊢ Antitone fun n ↦ Ioc (u n) a
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation

Goal state before:
pp: case h₁
X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
s t : Set X
ℓ : StrongDual ℝ E
hℓ : ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}
⊢ (μ.mapRange ↑ℓ ⋯).variation s ≤ ⨆ ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}, (μ.mapRange ↑ℓ ⋯).variation s

pp: case h₂
X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
s t : Set X
ℓ : StrongDual ℝ E
hℓ : ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}
⊢ (μ.mapRange ↑ℓ ⋯).variation t ≤ ⨆ ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}, (μ.mapRange ↑ℓ ⋯).variation t

Tactic:
<;>

Goal state after:
case h₁
X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
s t : Set X
ℓ : StrongDual ℝ E
hℓ : ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}
⊢ (μ.mapRange ↑ℓ ⋯).variation s ≤ ⨆ ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}, (μ.mapRange ↑ℓ ⋯).variation s

case h₂
X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
s t : Set X
ℓ : StrongDual ℝ E
hℓ : ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}
⊢ (μ.mapRange ↑ℓ ⋯).variation t ≤ ⨆ ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}, (μ.mapRange ↑ℓ ⋯).variation t
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ s ∈ C, MeasurableSet s
M : MeasurableSpace α := generateFrom C
Mle : M ≤ hα
μ' : Measure α := μ.trim Mle
hμ' : μ' = μ.trim Mle
m' : VectorMeasure α E
m'C : ∀ s ∈ C, m' s = m s
hm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ μ' s
m'_le : m'.variation ≤ μ'
this✝ : MeasurableSpace α := hα
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : Pairwise (Function.onFun Disjoint f)
this :
  ∫ᵛ (x : α), μ[fun x ↦ ∑' (d : ℕ), (f d).indicator 1 x | M] x ∂•m' =
    ∫ᵛ (x : α), ∑' (d : ℕ), μ[(f d).indicator 1 | M] x ∂•m'
I : ∑' (i : ℕ), ∫⁻ (a : α), ‖μ[(f i).indicator 1 | M] a‖ₑ ∂μ < ∞
⊢ ∑' (i : ℕ), ∫⁻ (a : α), ‖μ[(f i).indicator 1 | M] a‖ₑ ∂m'.variation ≠ ∞

Tactic:
apply ne_of_lt
        grw [m'_le, hμ']
        have A i : Measurable[M] (fun x ↦ ‖μ[(f i).indicator (1 : α → ℝ) | M] x‖ₑ) := by fun_prop
        simp_rw [lintegral_trim Mle (A _)]
        exact I

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

Goal state before:
pp: case pos
X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
x : X
v : F
s : Set X
hs : MeasurableSet s
hx : x ∈ s
⊢ ((dirac x v).transpose B) s = (dirac x (B.flip v)) s

pp: case neg
X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
x : X
v : F
s : Set X
hs : MeasurableSet s
hx : x ∉ s
⊢ ((dirac x v).transpose B) s = (dirac x (B.flip v)) s

Tactic:
<;>

Goal state after:
case pos
X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
x : X
v : F
s : Set X
hs : MeasurableSet s
hx : x ∈ s
⊢ ((dirac x v).transpose B) s = (dirac x (B.flip v)) s

case neg
X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
x : X
v : F
s : Set X
hs : MeasurableSet s
hx : x ∉ s
⊢ ((dirac x v).transpose B) s = (dirac x (B.flip v)) s
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b : M
t : Set M
ht : t.Finite
⊢ IsLinearSet (a +ᵥ b +ᵥ ↑(closure t))

Tactic:
exact ⟨a + b, t, ht, by rw [vadd_vadd]⟩

Goal state after: