mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: case neg
X : Type u_1
inst✝⁷ : TopologicalSpace X
inst✝⁶ : T2Space X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
μ ν : Measure X
inst✝³ : LocallyCompactSpace X
inst✝² : ν.OuterRegular
inst✝¹ : IsFiniteMeasureOnCompacts ν
inst✝ : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), ∫ (x : X), f x ∂μ ≤ ∫ (x : X), f x ∂ν
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : ν K < ∞
hνK : ν K ≠ ∞
hμK : μ K ≠ ∞
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst✝⁷] V
pV3 : ν V ≤ ν K + ↑ε
VltTop : ν V < ∞
f : X →C_c ℝ
pf1 : EqOn (⇑f) 1 K
pf2 : tsupport ⇑f ⊆ V
pf3 : ∀ (x : X), f x ∈ Icc 0 1
x : X
hx : x ∉ tsupport ⇑f
⊢ f x ≤ V.indicator 1 x

Tactic:
·

Goal state after:
case neg
X : Type u_1
inst✝⁷ : TopologicalSpace X
inst✝⁶ : T2Space X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
μ ν : Measure X
inst✝³ : LocallyCompactSpace X
inst✝² : ν.OuterRegular
inst✝¹ : IsFiniteMeasureOnCompacts ν
inst✝ : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), ∫ (x : X), f x ∂μ ≤ ∫ (x : X), f x ∂ν
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : ν K < ∞
hνK : ν K ≠ ∞
hμK : μ K ≠ ∞
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst✝⁷] V
pV3 : ν V ≤ ν K + ↑ε
VltTop : ν V < ∞
f : X →C_c ℝ
pf1 : EqOn (⇑f) 1 K
pf2 : tsupport ⇑f ⊆ V
pf3 : ∀ (x : X), f x ∈ Icc 0 1
x : X
hx : x ∉ tsupport ⇑f
⊢ f x ≤ V.indicator 1 x
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: case pos
X : Type u_1
inst✝⁷ : TopologicalSpace X
inst✝⁶ : T2Space X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
μ ν : Measure X
inst✝³ : LocallyCompactSpace X
inst✝² : ν.OuterRegular
inst✝¹ : IsFiniteMeasureOnCompacts ν
inst✝ : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), ∫ (x : X), f x ∂μ ≤ ∫ (x : X), f x ∂ν
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : ν K < ∞
hνK : ν K ≠ ∞
hμK : μ K ≠ ∞
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst✝⁷] V
pV3 : ν V ≤ ν K + ↑ε
VltTop : ν V < ∞
f : X →C_c ℝ
pf1 : EqOn (⇑f) 1 K
pf2 : tsupport ⇑f ⊆ V
pf3 : ∀ (x : X), f x ∈ Icc 0 1
hfV : ∀ (x : X), f x ≤ V.indicator 1 x
x : X
hx : x ∈ K
⊢ K.indicator 1 x ≤ f x

pp: case neg
X : Type u_1
inst✝⁷ : TopologicalSpace X
inst✝⁶ : T2Space X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
μ ν : Measure X
inst✝³ : LocallyCompactSpace X
inst✝² : ν.OuterRegular
inst✝¹ : IsFiniteMeasureOnCompacts ν
inst✝ : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), ∫ (x : X), f x ∂μ ≤ ∫ (x : X), f x ∂ν
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : ν K < ∞
hνK : ν K ≠ ∞
hμK : μ K ≠ ∞
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst✝⁷] V
pV3 : ν V ≤ ν K + ↑ε
VltTop : ν V < ∞
f : X →C_c ℝ
pf1 : EqOn (⇑f) 1 K
pf2 : tsupport ⇑f ⊆ V
pf3 : ∀ (x : X), f x ∈ Icc 0 1
hfV : ∀ (x : X), f x ≤ V.indicator 1 x
x : X
hx : x ∉ K
⊢ K.indicator 1 x ≤ f x

Tactic:
·

Goal state after:
case pos
X : Type u_1
inst✝⁷ : TopologicalSpace X
inst✝⁶ : T2Space X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
μ ν : Measure X
inst✝³ : LocallyCompactSpace X
inst✝² : ν.OuterRegular
inst✝¹ : IsFiniteMeasureOnCompacts ν
inst✝ : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), ∫ (x : X), f x ∂μ ≤ ∫ (x : X), f x ∂ν
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : ν K < ∞
hνK : ν K ≠ ∞
hμK : μ K ≠ ∞
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst✝⁷] V
pV3 : ν V ≤ ν K + ↑ε
VltTop : ν V < ∞
f : X →C_c ℝ
pf1 : EqOn (⇑f) 1 K
pf2 : tsupport ⇑f ⊆ V
pf3 : ∀ (x : X), f x ∈ Icc 0 1
hfV : ∀ (x : X), f x ≤ V.indicator 1 x
x : X
hx : x ∈ K
⊢ K.indicator 1 x ≤ f x
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: case neg
X : Type u_1
inst✝⁷ : TopologicalSpace X
inst✝⁶ : T2Space X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
μ ν : Measure X
inst✝³ : LocallyCompactSpace X
inst✝² : ν.OuterRegular
inst✝¹ : IsFiniteMeasureOnCompacts ν
inst✝ : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), ∫ (x : X), f x ∂μ ≤ ∫ (x : X), f x ∂ν
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : ν K < ∞
hνK : ν K ≠ ∞
hμK : μ K ≠ ∞
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst✝⁷] V
pV3 : ν V ≤ ν K + ↑ε
VltTop : ν V < ∞
f : X →C_c ℝ
pf1 : EqOn (⇑f) 1 K
pf2 : tsupport ⇑f ⊆ V
pf3 : ∀ (x : X), f x ∈ Icc 0 1
hfV : ∀ (x : X), f x ≤ V.indicator 1 x
x : X
hx : x ∉ K
⊢ K.indicator 1 x ≤ f x

Tactic:
·

Goal state after:
case neg
X : Type u_1
inst✝⁷ : TopologicalSpace X
inst✝⁶ : T2Space X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
μ ν : Measure X
inst✝³ : LocallyCompactSpace X
inst✝² : ν.OuterRegular
inst✝¹ : IsFiniteMeasureOnCompacts ν
inst✝ : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), ∫ (x : X), f x ∂μ ≤ ∫ (x : X), f x ∂ν
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : ν K < ∞
hνK : ν K ≠ ∞
hμK : μ K ≠ ∞
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst✝⁷] V
pV3 : ν V ≤ ν K + ↑ε
VltTop : ν V < ∞
f : X →C_c ℝ
pf1 : EqOn (⇑f) 1 K
pf2 : tsupport ⇑f ⊆ V
pf3 : ∀ (x : X), f x ∈ Icc 0 1
hfV : ∀ (x : X), f x ≤ V.indicator 1 x
x : X
hx : x ∉ K
⊢ K.indicator 1 x ≤ f x
Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd

Goal state before:
pp: case h.refine_1
α : Type u_1
inst✝⁹ : MeasurableSpace α
β : Type u_2
inst✝⁸ : MeasurableSpace β
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : SecondCountableTopology β
inst✝³ : PseudoMetrizableSpace α
inst✝² : PseudoMetrizableSpace β
inst✝¹ : OpensMeasurableSpace α
inst✝ : OpensMeasurableSpace β
μ : ProbabilityMeasure α × ProbabilityMeasure β
S : Set (Set (α × β)) :=
  {t | ∃ a b, MeasurableSet a ∧ μ.1 (frontier a) = 0 ∧ MeasurableSet b ∧ μ.2 (frontier b) = 0 ∧ t = a ×ˢ b}
this✝¹ : IsPiSystem S
this✝ : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
u : Set (α × β)
u_open : IsOpen[instTopologicalSpaceProd] u
x : α × β
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : ℝ
hr : r ∈ Ioo 0 ε
r' : ℝ
hr' : r' ∈ Ioo 0 ε
μr : ↑μ.1 (frontier (ball x.1 r)) = 0
μr' : ↑μ.2 (frontier (ball x.2 r')) = 0
⊢ ball x.1 r ×ˢ ball x.2 r' ∈ 𝓝 x

pp: case h.refine_2
α : Type u_1
inst✝⁹ : MeasurableSpace α
β : Type u_2
inst✝⁸ : MeasurableSpace β
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : SecondCountableTopology β
inst✝³ : PseudoMetrizableSpace α
inst✝² : PseudoMetrizableSpace β
inst✝¹ : OpensMeasurableSpace α
inst✝ : OpensMeasurableSpace β
μ : ProbabilityMeasure α × ProbabilityMeasure β
S : Set (Set (α × β)) :=
  {t | ∃ a b, MeasurableSet a ∧ μ.1 (frontier a) = 0 ∧ MeasurableSet b ∧ μ.2 (frontier b) = 0 ∧ t = a ×ˢ b}
this✝¹ : IsPiSystem S
this✝ : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
u : Set (α × β)
u_open : IsOpen[instTopologicalSpaceProd] u
x : α × β
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : ℝ
hr : r ∈ Ioo 0 ε
r' : ℝ
hr' : r' ∈ Ioo 0 ε
μr : ↑μ.1 (frontier (ball x.1 r)) = 0
μr' : ↑μ.2 (frontier (ball x.2 r')) = 0
⊢ ball x.1 r ×ˢ ball x.2 r' ⊆ u

Tactic:
·

Goal state after:
case h.refine_1
α : Type u_1
inst✝⁹ : MeasurableSpace α
β : Type u_2
inst✝⁸ : MeasurableSpace β
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : SecondCountableTopology β
inst✝³ : PseudoMetrizableSpace α
inst✝² : PseudoMetrizableSpace β
inst✝¹ : OpensMeasurableSpace α
inst✝ : OpensMeasurableSpace β
μ : ProbabilityMeasure α × ProbabilityMeasure β
S : Set (Set (α × β)) :=
  {t | ∃ a b, MeasurableSet a ∧ μ.1 (frontier a) = 0 ∧ MeasurableSet b ∧ μ.2 (frontier b) = 0 ∧ t = a ×ˢ b}
this✝¹ : IsPiSystem S
this✝ : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
u : Set (α × β)
u_open : IsOpen[instTopologicalSpaceProd] u
x : α × β
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : ℝ
hr : r ∈ Ioo 0 ε
r' : ℝ
hr' : r' ∈ Ioo 0 ε
μr : ↑μ.1 (frontier (ball x.1 r)) = 0
μr' : ↑μ.2 (frontier (ball x.2 r')) = 0
⊢ ball x.1 r ×ˢ ball x.2 r' ∈ 𝓝 x
Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd

Goal state before:
pp: case h.refine_2
α : Type u_1
inst✝⁹ : MeasurableSpace α
β : Type u_2
inst✝⁸ : MeasurableSpace β
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : SecondCountableTopology β
inst✝³ : PseudoMetrizableSpace α
inst✝² : PseudoMetrizableSpace β
inst✝¹ : OpensMeasurableSpace α
inst✝ : OpensMeasurableSpace β
μ : ProbabilityMeasure α × ProbabilityMeasure β
S : Set (Set (α × β)) :=
  {t | ∃ a b, MeasurableSet a ∧ μ.1 (frontier a) = 0 ∧ MeasurableSet b ∧ μ.2 (frontier b) = 0 ∧ t = a ×ˢ b}
this✝¹ : IsPiSystem S
this✝ : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
u : Set (α × β)
u_open : IsOpen[instTopologicalSpaceProd] u
x : α × β
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : ℝ
hr : r ∈ Ioo 0 ε
r' : ℝ
hr' : r' ∈ Ioo 0 ε
μr : ↑μ.1 (frontier (ball x.1 r)) = 0
μr' : ↑μ.2 (frontier (ball x.2 r')) = 0
⊢ ball x.1 r ×ˢ ball x.2 r' ⊆ u

Tactic:
·

Goal state after:
case h.refine_2
α : Type u_1
inst✝⁹ : MeasurableSpace α
β : Type u_2
inst✝⁸ : MeasurableSpace β
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : SecondCountableTopology β
inst✝³ : PseudoMetrizableSpace α
inst✝² : PseudoMetrizableSpace β
inst✝¹ : OpensMeasurableSpace α
inst✝ : OpensMeasurableSpace β
μ : ProbabilityMeasure α × ProbabilityMeasure β
S : Set (Set (α × β)) :=
  {t | ∃ a b, MeasurableSet a ∧ μ.1 (frontier a) = 0 ∧ MeasurableSet b ∧ μ.2 (frontier b) = 0 ∧ t = a ×ˢ b}
this✝¹ : IsPiSystem S
this✝ : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
u : Set (α × β)
u_open : IsOpen[instTopologicalSpaceProd] u
x : α × β
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : ℝ
hr : r ∈ Ioo 0 ε
r' : ℝ
hr' : r' ∈ Ioo 0 ε
μr : ↑μ.1 (frontier (ball x.1 r)) = 0
μr' : ↑μ.2 (frontier (ball x.2 r')) = 0
⊢ ball x.1 r ×ˢ ball x.2 r' ⊆ u
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: case a
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : T2Space X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
μ ν : Measure X
inst✝² : LocallyCompactSpace X
inst✝¹ : μ.Regular
inst✝ : ν.Regular
hμν : ∀ (f : X →C_c ℝ), ∫ (x : X), f x ∂μ = ∫ (x : X), f x ∂ν
K : Set X
hK : IsCompact K
⊢ μ K ≤ ν K

pp: case a
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : T2Space X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
μ ν : Measure X
inst✝² : LocallyCompactSpace X
inst✝¹ : μ.Regular
inst✝ : ν.Regular
hμν : ∀ (f : X →C_c ℝ), ∫ (x : X), f x ∂μ = ∫ (x : X), f x ∂ν
K : Set X
hK : IsCompact K
⊢ ν K ≤ μ K

Tactic:
·

Goal state after:
case a
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : T2Space X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
μ ν : Measure X
inst✝² : LocallyCompactSpace X
inst✝¹ : μ.Regular
inst✝ : ν.Regular
hμν : ∀ (f : X →C_c ℝ), ∫ (x : X), f x ∂μ = ∫ (x : X), f x ∂ν
K : Set X
hK : IsCompact K
⊢ μ K ≤ ν K
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: case a
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : T2Space X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
μ ν : Measure X
inst✝² : LocallyCompactSpace X
inst✝¹ : μ.Regular
inst✝ : ν.Regular
hμν : ∀ (f : X →C_c ℝ), ∫ (x : X), f x ∂μ = ∫ (x : X), f x ∂ν
K : Set X
hK : IsCompact K
⊢ ν K ≤ μ K

Tactic:
·

Goal state after:
case a
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : T2Space X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
μ ν : Measure X
inst✝² : LocallyCompactSpace X
inst✝¹ : μ.Regular
inst✝ : ν.Regular
hμν : ∀ (f : X →C_c ℝ), ∫ (x : X), f x ∂μ = ∫ (x : X), f x ∂ν
K : Set X
hK : IsCompact K
⊢ ν K ≤ μ K
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: case refine_1
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 μ
ν' : Measure ↑K
ν'_reg : ν'.Regular
ν'_fin : IsFiniteMeasure ν'
hν' : ∀ (g : ↑K →ᵇ ℝ), ∫ (x : ↑K), g x ∂μ' = ∫ (x : ↑K), g x ∂ν'
⊢ (Measure.map Subtype.val ν') Kᶜ = 0

pp: case refine_2
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 μ
ν' : Measure ↑K
ν'_reg : ν'.Regular
ν'_fin : IsFiniteMeasure ν'
hν' : ∀ (g : ↑K →ᵇ ℝ), ∫ (x : ↑K), g x ∂μ' = ∫ (x : ↑K), g x ∂ν'
g : X →ᵇ ℝ
⊢ ∫ (x : X), g x ∂μ = ∫ (x : X), g x ∂Measure.map Subtype.val ν'

Tactic:
·

Goal state after:
case refine_1
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 μ
ν' : Measure ↑K
ν'_reg : ν'.Regular
ν'_fin : IsFiniteMeasure ν'
hν' : ∀ (g : ↑K →ᵇ ℝ), ∫ (x : ↑K), g x ∂μ' = ∫ (x : ↑K), g x ∂ν'
⊢ (Measure.map Subtype.val ν') Kᶜ = 0
Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd

Goal state before:
pp: case h'
α : Type u_1
inst✝⁹ : MeasurableSpace α
β : Type u_2
inst✝⁸ : MeasurableSpace β
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : SecondCountableTopology β
inst✝³ : PseudoMetrizableSpace α
inst✝² : PseudoMetrizableSpace β
inst✝¹ : OpensMeasurableSpace α
inst✝ : OpensMeasurableSpace β
μ : ProbabilityMeasure α × ProbabilityMeasure β
S : Set (Set (α × β)) := ⋯
this : IsPiSystem S
⊢ ∀ s ∈ S, Tendsto (fun i ↦ (i.1.prod i.2) s) (𝓝 μ) (𝓝 (((fun μ ↦ μ.1.prod μ.2) μ) s))

Tactic:
·

Goal state after:
case h'
α : Type u_1
inst✝⁹ : MeasurableSpace α
β : Type u_2
inst✝⁸ : MeasurableSpace β
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : SecondCountableTopology β
inst✝³ : PseudoMetrizableSpace α
inst✝² : PseudoMetrizableSpace β
inst✝¹ : OpensMeasurableSpace α
inst✝ : OpensMeasurableSpace β
μ : ProbabilityMeasure α × ProbabilityMeasure β
S : Set (Set (α × β)) := ⋯
this : IsPiSystem S
⊢ ∀ s ∈ S, Tendsto (fun i ↦ (i.1.prod i.2) s) (𝓝 μ) (𝓝 (((fun μ ↦ μ.1.prod μ.2) μ) s))
Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd

Goal state before:
pp: case h'.hf
α : Type u_1
inst✝⁹ : MeasurableSpace α
β : Type u_2
inst✝⁸ : MeasurableSpace β
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : SecondCountableTopology β
inst✝³ : PseudoMetrizableSpace α
inst✝² : PseudoMetrizableSpace β
inst✝¹ : OpensMeasurableSpace α
inst✝ : OpensMeasurableSpace β
μ : ProbabilityMeasure α × ProbabilityMeasure β
S : Set (Set (α × β)) := ⋯
this : IsPiSystem S
a : Set α
b : Set β
ameas : MeasurableSet a
ha : μ.1 (frontier a) = 0
bmeas : MeasurableSet b
hb : μ.2 (frontier b) = 0
⊢ Tendsto (fun x ↦ x.1 a) (𝓝 μ) (𝓝 (μ.1 a))

pp: case hg
α : Type u_1
inst✝⁹ : MeasurableSpace α
β : Type u_2
inst✝⁸ : MeasurableSpace β
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : SecondCountableTopology β
inst✝³ : PseudoMetrizableSpace α
inst✝² : PseudoMetrizableSpace β
inst✝¹ : OpensMeasurableSpace α
inst✝ : OpensMeasurableSpace β
μ : ProbabilityMeasure α × ProbabilityMeasure β
S : Set (Set (α × β)) := ⋯
this : IsPiSystem S
a : Set α
b : Set β
ameas : MeasurableSet a
ha : μ.1 (frontier a) = 0
bmeas : MeasurableSet b
hb : μ.2 (frontier b) = 0
⊢ Tendsto (fun x ↦ x.2 b) (𝓝 μ) (𝓝 (μ.2 b))

Tactic:
·

Goal state after:
case h'.hf
α : Type u_1
inst✝⁹ : MeasurableSpace α
β : Type u_2
inst✝⁸ : MeasurableSpace β
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : SecondCountableTopology β
inst✝³ : PseudoMetrizableSpace α
inst✝² : PseudoMetrizableSpace β
inst✝¹ : OpensMeasurableSpace α
inst✝ : OpensMeasurableSpace β
μ : ProbabilityMeasure α × ProbabilityMeasure β
S : Set (Set (α × β)) := ⋯
this : IsPiSystem S
a : Set α
b : Set β
ameas : MeasurableSet a
ha : μ.1 (frontier a) = 0
bmeas : MeasurableSet b
hb : μ.2 (frontier b) = 0
⊢ Tendsto (fun x ↦ x.1 a) (𝓝 μ) (𝓝 (μ.1 a))
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: case e'_2
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 μ
ν' : Measure ↑K
ν'_reg : ν'.Regular
ν'_fin : IsFiniteMeasure ν'
hν' : ∀ (g : ↑K →ᵇ ℝ), ∫ (x : ↑K), g x ∂μ' = ∫ (x : ↑K), g x ∂ν'
g : X →ᵇ ℝ
⊢ ∫ (x : X), g x ∂μ = ∫ (x : ↑K), (g.compContinuous { toFun := Subtype.val, continuous_toFun := ⋯ }) x ∂μ'

pp: case e'_3
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 μ
ν' : Measure ↑K
ν'_reg : ν'.Regular
ν'_fin : IsFiniteMeasure ν'
hν' : ∀ (g : ↑K →ᵇ ℝ), ∫ (x : ↑K), g x ∂μ' = ∫ (x : ↑K), g x ∂ν'
g : X →ᵇ ℝ
⊢ ∫ (x : X), g x ∂Measure.map Subtype.val ν' =
    ∫ (x : ↑K), (g.compContinuous { toFun := Subtype.val, continuous_toFun := ⋯ }) x ∂ν'

Tactic:
·

Goal state after:
case e'_2
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 μ
ν' : Measure ↑K
ν'_reg : ν'.Regular
ν'_fin : IsFiniteMeasure ν'
hν' : ∀ (g : ↑K →ᵇ ℝ), ∫ (x : ↑K), g x ∂μ' = ∫ (x : ↑K), g x ∂ν'
g : X →ᵇ ℝ
⊢ ∫ (x : X), g x ∂μ = ∫ (x : ↑K), (g.compContinuous { toFun := Subtype.val, continuous_toFun := ⋯ }) x ∂μ'
Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd

Goal state before:
pp: case hg
α : Type u_1
inst✝⁹ : MeasurableSpace α
β : Type u_2
inst✝⁸ : MeasurableSpace β
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : SecondCountableTopology β
inst✝³ : PseudoMetrizableSpace α
inst✝² : PseudoMetrizableSpace β
inst✝¹ : OpensMeasurableSpace α
inst✝ : OpensMeasurableSpace β
μ : ProbabilityMeasure α × ProbabilityMeasure β
S : Set (Set (α × β)) := ⋯
this : IsPiSystem S
a : Set α
b : Set β
ameas : MeasurableSet a
ha : μ.1 (frontier a) = 0
bmeas : MeasurableSet b
hb : μ.2 (frontier b) = 0
⊢ Tendsto (fun x ↦ x.2 b) (𝓝 μ) (𝓝 (μ.2 b))

Tactic:
·

Goal state after:
case hg
α : Type u_1
inst✝⁹ : MeasurableSpace α
β : Type u_2
inst✝⁸ : MeasurableSpace β
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : SecondCountableTopology β
inst✝³ : PseudoMetrizableSpace α
inst✝² : PseudoMetrizableSpace β
inst✝¹ : OpensMeasurableSpace α
inst✝ : OpensMeasurableSpace β
μ : ProbabilityMeasure α × ProbabilityMeasure β
S : Set (Set (α × β)) := ⋯
this : IsPiSystem S
a : Set α
b : Set β
ameas : MeasurableSet a
ha : μ.1 (frontier a) = 0
bmeas : MeasurableSet b
hb : μ.2 (frontier b) = 0
⊢ Tendsto (fun x ↦ x.2 b) (𝓝 μ) (𝓝 (μ.2 b))
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: case e'_3
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 μ
ν' : Measure ↑K
ν'_reg : ν'.Regular
ν'_fin : IsFiniteMeasure ν'
hν' : ∀ (g : ↑K →ᵇ ℝ), ∫ (x : ↑K), g x ∂μ' = ∫ (x : ↑K), g x ∂ν'
g : X →ᵇ ℝ
⊢ ∫ (x : X), g x ∂Measure.map Subtype.val ν' =
    ∫ (x : ↑K), (g.compContinuous { toFun := Subtype.val, continuous_toFun := ⋯ }) x ∂ν'

Tactic:
·

Goal state after:
case e'_3
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 μ
ν' : Measure ↑K
ν'_reg : ν'.Regular
ν'_fin : IsFiniteMeasure ν'
hν' : ∀ (g : ↑K →ᵇ ℝ), ∫ (x : ↑K), g x ∂μ' = ∫ (x : ↑K), g x ∂ν'
g : X →ᵇ ℝ
⊢ ∫ (x : X), g x ∂Measure.map Subtype.val ν' =
    ∫ (x : ↑K), (g.compContinuous { toFun := Subtype.val, continuous_toFun := ⋯ }) x ∂ν'
Module: Mathlib.MeasureTheory.Measure.Haar.Extension

Goal state before:
pp: case pos
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
b : B
ε : ℝ
hε : ε > 0
U₀ : Set B
hU₀ : IsCompact U₀
hb : U₀ ∈ nhds b
K : Set B
hK : IsCompact K
hf₀ : ∀ x ∉ K, f x = 0
S : Set A := ⇑φ ⁻¹' (U₀⁻¹ * K)
hSc : IsCompact S
hS' : μA.real S = 0
⊢ ∃ δ > 0, ENNReal.ofReal δ * ENNReal.ofReal (μA.real S) < ENNReal.ofReal ε

pp: case neg
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
b : B
ε : ℝ
hε : ε > 0
U₀ : Set B
hU₀ : IsCompact U₀
hb : U₀ ∈ nhds b
K : Set B
hK : IsCompact K
hf₀ : ∀ x ∉ K, f x = 0
S : Set A := ⇑φ ⁻¹' (U₀⁻¹ * K)
hSc : IsCompact S
hS' : ¬μA.real S = 0
⊢ ∃ δ > 0, ENNReal.ofReal δ * ENNReal.ofReal (μA.real S) < ENNReal.ofReal ε

Tactic:
·

Goal state after:
case pos
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
b : B
ε : ℝ
hε : ε > 0
U₀ : Set B
hU₀ : IsCompact U₀
hb : U₀ ∈ nhds b
K : Set B
hK : IsCompact K
hf₀ : ∀ x ∉ K, f x = 0
S : Set A := ⇑φ ⁻¹' (U₀⁻¹ * K)
hSc : IsCompact S
hS' : μA.real S = 0
⊢ ∃ δ > 0, ENNReal.ofReal δ * ENNReal.ofReal (μA.real S) < ENNReal.ofReal ε