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

Goal state before:
pp: W : Type u_1
inst✝¹¹ : AddCommGroup W
inst✝¹⁰ : Module ℝ W
inst✝⁹ : TopologicalSpace W
e : AddChar ℝ Circle
V : Type u_2
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module ℝ V
inst✝⁶ : PseudoEMetricSpace V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : CompleteSpace V
inst✝² : SecondCountableTopology V
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
he : Continuous ⇑e
he' : e ≠ 1
hL' : ∀ (v : V), v ≠ 0 → L v ≠ 0
hL : Continuous fun p ↦ (L p.1) p.2
P P' : Measure V
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
h : ∀ (w : W), ∫ (v : V), (char he hL w) v ∂P = ∫ (v : V), (char he hL w) v ∂P'
g✝ : V →ᵇ ℂ
w : AddMonoidAlgebra ℂ W
hw : ⇑g✝ = fun x ↦ w.coeff.sum fun a z ↦ z * ↑(e ((L x) a))
hsum :
  ∀ (P : Measure V) [IsFiniteMeasure P],
    ∫ (v : V), w.coeff.sum fun a z ↦ z * ↑(e ((L v) a)) ∂P = w.coeff.sum fun a z ↦ ∫ (v : V), z * ↑(e ((L v) a)) ∂P
⊢ ∫ (x : V), (fun x ↦ w.coeff.sum fun a z ↦ z * ↑(e ((L x) a))) x ∂P =
    ∫ (x : V), (fun x ↦ w.coeff.sum fun a z ↦ z * ↑(e ((L x) a))) x ∂P'

Tactic:
hsum P,

Goal state after:
W : Type u_1
inst✝¹¹ : AddCommGroup W
inst✝¹⁰ : Module ℝ W
inst✝⁹ : TopologicalSpace W
e : AddChar ℝ Circle
V : Type u_2
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module ℝ V
inst✝⁶ : PseudoEMetricSpace V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : CompleteSpace V
inst✝² : SecondCountableTopology V
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
he : Continuous ⇑e
he' : e ≠ 1
hL' : ∀ (v : V), v ≠ 0 → L v ≠ 0
hL : Continuous fun p ↦ (L p.1) p.2
P P' : Measure V
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
h : ∀ (w : W), ∫ (v : V), (char he hL w) v ∂P = ∫ (v : V), (char he hL w) v ∂P'
g✝ : V →ᵇ ℂ
w : AddMonoidAlgebra ℂ W
hw : ⇑g✝ = fun x ↦ w.coeff.sum fun a z ↦ z * ↑(e ((L x) a))
hsum :
  ∀ (P : Measure V) [IsFiniteMeasure P],
    ∫ (v : V), w.coeff.sum fun a z ↦ z * ↑(e ((L v) a)) ∂P = w.coeff.sum fun a z ↦ ∫ (v : V), z * ↑(e ((L v) a)) ∂P
⊢ (w.coeff.sum fun a z ↦ ∫ (v : V), z * ↑(e ((L v) a)) ∂P) =
    ∫ (x : V), (fun x ↦ w.coeff.sum fun a z ↦ z * ↑(e ((L x) a))) x ∂P'
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_4
F : Type u_5
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : InnerProductSpace ℝ F
mE : MeasurableSpace E
mF : MeasurableSpace F
inst✝⁸ : CompleteSpace E
inst✝⁷ : CompleteSpace F
inst✝⁶ : SecondCountableTopology E
inst✝⁵ : SecondCountableTopology F
inst✝⁴ : BorelSpace E
inst✝³ : BorelSpace F
μ : Measure E
ν : Measure F
ξ : Measure (E × F)
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure ξ
h : ξ = μ.prod ν
⊢ ∀ (t : WithLp 2 (E × F)), charFun (Measure.map (toLp 2) ξ) t = charFun μ t.ofLp.1 * charFun ν t.ofLp.2

Tactic:
rw [h]

Goal state after:
E : Type u_4
F : Type u_5
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : InnerProductSpace ℝ F
mE : MeasurableSpace E
mF : MeasurableSpace F
inst✝⁸ : CompleteSpace E
inst✝⁷ : CompleteSpace F
inst✝⁶ : SecondCountableTopology E
inst✝⁵ : SecondCountableTopology F
inst✝⁴ : BorelSpace E
inst✝³ : BorelSpace F
μ : Measure E
ν : Measure F
ξ : Measure (E × F)
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure ξ
h : ξ = μ.prod ν
⊢ ∀ (t : WithLp 2 (E × F)), charFun (Measure.map (toLp 2) (μ.prod ν)) t = charFun μ t.ofLp.1 * charFun ν t.ofLp.2
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: ι : Type u_6
inst✝⁷ : Fintype ι
E : ι → Type u_7
inst✝⁶ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → InnerProductSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst✝⁴ : ∀ (i : ι), CompleteSpace (E i)
inst✝³ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst✝¹ : ∀ (i : ι), IsFiniteMeasure (μ i)
inst✝ : IsFiniteMeasure ν
h : ν = Measure.pi μ
⊢ ∀ (t : WithLp 2 ((i : ι) → E i)), charFun (Measure.map (toLp 2) ν) t = ∏ i, charFun (μ i) (t.ofLp i)

Tactic:
rw [h]

Goal state after:
ι : Type u_6
inst✝⁷ : Fintype ι
E : ι → Type u_7
inst✝⁶ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → InnerProductSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst✝⁴ : ∀ (i : ι), CompleteSpace (E i)
inst✝³ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst✝¹ : ∀ (i : ι), IsFiniteMeasure (μ i)
inst✝ : IsFiniteMeasure ν
h : ν = Measure.pi μ
⊢ ∀ (t : WithLp 2 ((i : ι) → E i)), charFun (Measure.map (toLp 2) (Measure.pi μ)) t = ∏ i, charFun (μ i) (t.ofLp i)
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: case refine_1
X : Type u
inst✝ : TopologicalSpace X
h : TopologicalSpace.IsTopologicalBasis {s | IsClopen s}
x : X
K : Set X
hK : IsClosed[inst✝] K
hx✝ : x ∉ K
s : Set X
hs : s ∈ {s | IsClopen s}
hx : x ∈ s
hsK : s ⊆ Kᶜ
⊢ Continuous[inst✝, _] (sᶜ.indicator 1)

pp: case refine_2
X : Type u
inst✝ : TopologicalSpace X
h : TopologicalSpace.IsTopologicalBasis {s | IsClopen s}
x✝ : X
K : Set X
hK : IsClosed[inst✝] K
hx✝¹ : x✝ ∉ K
s : Set X
hs : s ∈ {s | IsClopen s}
hx✝ : x✝ ∈ s
hsK : s ⊆ Kᶜ
x : X
hx : x ∈ K
⊢ x ∈ sᶜ

Tactic:
· exact hs.compl.continuous_indicator continuous_const

Goal state after:
case refine_2
X : Type u
inst✝ : TopologicalSpace X
h : TopologicalSpace.IsTopologicalBasis {s | IsClopen s}
x✝ : X
K : Set X
hK : IsClosed[inst✝] K
hx✝¹ : x✝ ∉ K
s : Set X
hs : s ∈ {s | IsClopen s}
hx✝ : x✝ ∈ s
hsK : s ⊆ Kᶜ
x : X
hx : x ∈ K
⊢ x ∈ sᶜ
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
inst✝⁸ : BorelSpace E
inst✝⁷ : SecondCountableTopology E
inst✝⁶ : BorelSpace F
inst✝⁵ : SecondCountableTopology F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
ξ : Measure (E × F)
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure ξ
h : ξ = μ.prod ν
⊢ ∀ (L : StrongDual ℝ (E × F)),
    charFunDual ξ L =
      charFunDual μ (L ∘SL ContinuousLinearMap.inl ℝ E F) * charFunDual ν (L ∘SL ContinuousLinearMap.inr ℝ E F)

Tactic:
rw [h]

Goal state after:
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
inst✝⁸ : BorelSpace E
inst✝⁷ : SecondCountableTopology E
inst✝⁶ : BorelSpace F
inst✝⁵ : SecondCountableTopology F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
ξ : Measure (E × F)
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure ξ
h : ξ = μ.prod ν
⊢ ∀ (L : StrongDual ℝ (E × F)),
    charFunDual (μ.prod ν) L =
      charFunDual μ (L ∘SL ContinuousLinearMap.inl ℝ E F) * charFunDual ν (L ∘SL ContinuousLinearMap.inr ℝ E F)
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
inst✝⁹ : BorelSpace E
inst✝⁸ : SecondCountableTopology E
p : ℝ≥0∞
inst✝⁷ : Fact (1 ≤ p)
inst✝⁶ : BorelSpace F
inst✝⁵ : SecondCountableTopology F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
ξ : Measure (E × F)
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure ξ
h : ξ = μ.prod ν
⊢ ∀ (L : StrongDual ℝ (WithLp p (E × F))),
    charFunDual (Measure.map (toLp p) ξ) 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:
rw [h]

Goal state after:
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
inst✝⁹ : BorelSpace E
inst✝⁸ : SecondCountableTopology E
p : ℝ≥0∞
inst✝⁷ : Fact (1 ≤ p)
inst✝⁶ : BorelSpace F
inst✝⁵ : SecondCountableTopology F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
ξ : Measure (E × F)
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure ξ
h : ξ = μ.prod ν
⊢ ∀ (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)
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: ι : 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)
inst✝⁴ : ∀ (i : ι), BorelSpace (E i)
inst✝³ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝² : ∀ (i : ι), CompleteSpace (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst✝¹ : ∀ (i : ι), IsFiniteMeasure (μ i)
inst✝ : IsFiniteMeasure ν
h : ν = Measure.pi μ
⊢ ∀ (L : StrongDual ℝ ((i : ι) → E i)),
    charFunDual ν L = ∏ i, charFunDual (μ i) (L ∘SL ContinuousLinearMap.single ℝ E i)

Tactic:
rw [h]

Goal state after:
ι : 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)
inst✝⁴ : ∀ (i : ι), BorelSpace (E i)
inst✝³ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝² : ∀ (i : ι), CompleteSpace (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst✝¹ : ∀ (i : ι), IsFiniteMeasure (μ i)
inst✝ : IsFiniteMeasure ν
h : ν = Measure.pi μ
⊢ ∀ (L : StrongDual ℝ ((i : ι) → E i)),
    charFunDual (Measure.pi μ) L = ∏ i, charFunDual (μ i) (L ∘SL ContinuousLinearMap.single ℝ E i)
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)
inst✝⁴ : ∀ (i : ι), BorelSpace (E i)
inst✝³ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝² : ∀ (i : ι), CompleteSpace (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst✝¹ : ∀ (i : ι), IsFiniteMeasure (μ i)
inst✝ : IsFiniteMeasure ν
h : ν = Measure.pi μ
⊢ ∀ (L : StrongDual ℝ (WithLp p ((i : ι) → E i))),
    charFunDual (Measure.map (toLp p) ν) L =
      ∏ i, charFunDual (μ i) (L ∘SL ↑(PiLp.continuousLinearEquiv p ℝ E).symm ∘SL ContinuousLinearMap.single ℝ E i)

Tactic:
rw [h]

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)
inst✝⁴ : ∀ (i : ι), BorelSpace (E i)
inst✝³ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝² : ∀ (i : ι), CompleteSpace (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst✝¹ : ∀ (i : ι), IsFiniteMeasure (μ i)
inst✝ : IsFiniteMeasure ν
h : ν = Measure.pi μ
⊢ ∀ (L : StrongDual ℝ (WithLp p ((i : ι) → E i))),
    charFunDual (Measure.map (toLp p) (Measure.pi μ)) L =
      ∏ i, charFunDual (μ i) (L ∘SL ↑(PiLp.continuousLinearEquiv p ℝ E).symm ∘SL ContinuousLinearMap.single ℝ E i)
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
hs_add_r' : s.toReal + r.toReal = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal
⊢ ν (thickening s.toReal B) + s ≤ μ (thickening r.toReal (thickening s.toReal B)) + r + s

Tactic:
grw [right_measure_le_of_levyProkhorovEDist_lt lt_r isOpen_thickening.measurableSet]

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

Goal state before:
pp: case h.refine_1
ι : Type u_1
α : ι → Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
inst✝³ : (i : ι) → TopologicalSpace (α i)
inst✝² : ∀ (i : ι), SecondCountableTopology (α i)
inst✝¹ : ∀ (i : ι), PseudoMetrizableSpace (α i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t | ∃ s, t = univ.pi s ∧ (∀ (i : ι), MeasurableSet (s i)) ∧ ∀ (i : ι), (μ i) (frontier (s i)) = 0}
this✝ : IsPiSystem S
this : (i : ι) → PseudoMetricSpace (α i) := fun i ↦ pseudoMetrizableSpacePseudoMetric (α i)
u : Set ((i : ι) → α i)
u_open : IsOpen[Pi.topologicalSpace] u
x : (i : ι) → α i
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : ι → ℝ
rpos : ∀ (i : ι), r i ∈ Ioo 0 ε
hr : ∀ (i : ι), ↑(μ i) (frontier (thickening (r i) {x i})) = 0
⊢ (univ.pi fun i ↦ ball (x i) (r i)) ∈ 𝓝 x

pp: case h.refine_2
ι : Type u_1
α : ι → Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
inst✝³ : (i : ι) → TopologicalSpace (α i)
inst✝² : ∀ (i : ι), SecondCountableTopology (α i)
inst✝¹ : ∀ (i : ι), PseudoMetrizableSpace (α i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t | ∃ s, t = univ.pi s ∧ (∀ (i : ι), MeasurableSet (s i)) ∧ ∀ (i : ι), (μ i) (frontier (s i)) = 0}
this✝ : IsPiSystem S
this : (i : ι) → PseudoMetricSpace (α i) := fun i ↦ pseudoMetrizableSpacePseudoMetric (α i)
u : Set ((i : ι) → α i)
u_open : IsOpen[Pi.topologicalSpace] u
x : (i : ι) → α i
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : ι → ℝ
rpos : ∀ (i : ι), r i ∈ Ioo 0 ε
hr : ∀ (i : ι), ↑(μ i) (frontier (thickening (r i) {x i})) = 0
⊢ (univ.pi fun i ↦ ball (x i) (r i)) ⊆ u

Tactic:
· apply IsOpen.mem_nhds
      · exact isOpen_set_pi finite_univ (by simp)
      · simpa using fun i ↦ (rpos i).1

Goal state after:
case h.refine_2
ι : Type u_1
α : ι → Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
inst✝³ : (i : ι) → TopologicalSpace (α i)
inst✝² : ∀ (i : ι), SecondCountableTopology (α i)
inst✝¹ : ∀ (i : ι), PseudoMetrizableSpace (α i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t | ∃ s, t = univ.pi s ∧ (∀ (i : ι), MeasurableSet (s i)) ∧ ∀ (i : ι), (μ i) (frontier (s i)) = 0}
this✝ : IsPiSystem S
this : (i : ι) → PseudoMetricSpace (α i) := fun i ↦ pseudoMetrizableSpacePseudoMetric (α i)
u : Set ((i : ι) → α i)
u_open : IsOpen[Pi.topologicalSpace] u
x : (i : ι) → α i
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : ι → ℝ
rpos : ∀ (i : ι), r i ∈ Ioo 0 ε
hr : ∀ (i : ι), ↑(μ i) (frontier (thickening (r i) {x i})) = 0
⊢ (univ.pi fun i ↦ ball (x i) (r i)) ⊆ u
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
μ' : Measure ↑K := Measure.comap Subtype.val μ
this : CompactSpace ↑K
⊢ ∃ ν, ν.Regular ∧ IsFiniteMeasure ν ∧ ∀ (g : ↑K →ᵇ ℝ), ∫ (x : ↑K), g x ∂μ' = ∫ (x : ↑K), g x ∂ν

Tactic:
exact Measure.exists_regular_eq_of_compactSpace μ'

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar

Goal state before:
pp: G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : LocallyCompactSpace G
inst✝ : CompactSpace G
φ : G ≃ₜ* G
μ : Measure G := haarMeasure { carrier := univ, isCompact' := ⋯, interior_nonempty' := ⋯ }
hμ : μ univ = 1
⊢ μ.haarScalarFactor (map (⇑φ) μ) • 1 = μ.haarScalarFactor (map (⇑φ) μ) • μ (⇑φ ⁻¹' univ)

Tactic:
Set.preimage_univ,

Goal state after:
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : LocallyCompactSpace G
inst✝ : CompactSpace G
φ : G ≃ₜ* G
μ : Measure G := haarMeasure { carrier := univ, isCompact' := ⋯, interior_nonempty' := ⋯ }
hμ : μ univ = 1
⊢ μ.haarScalarFactor (map (⇑φ) μ) • 1 = μ.haarScalarFactor (map (⇑φ) μ) • μ univ
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K) n)
A : ∀ (n : ℕ), IsCompact ((partialSups K) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∈ f
ν : ℕ → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n)).InnerRegular
νK : ∀ (n : ℕ), (ν n) ((partialSups K) n)ᶜ = 0
hν : ∀ (n : ℕ), Tendsto (fun ρ ↦ ρ.restrict (disjointed K n)) (↑f) (𝓝 (ν n))
B : (Measure.sum fun n ↦ ↑(ν n)) univ ≤ ↑C
μ : FiniteMeasure E := ⟨Measure.sum fun n ↦ ↑(ν n), ⋯⟩
g : E →ᵇ ℝ
⊢ ∀ ε > 0, ∀ᶠ (x : FiniteMeasure E) in ↑f, dist (∫ (x : E), g x ∂↑(id x)) (∫ (x : E), g x ∂↑μ) < ε

Tactic:
intro ε εpos

Goal state after:
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K) n)
A : ∀ (n : ℕ), IsCompact ((partialSups K) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∈ f
ν : ℕ → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n)).InnerRegular
νK : ∀ (n : ℕ), (ν n) ((partialSups K) n)ᶜ = 0
hν : ∀ (n : ℕ), Tendsto (fun ρ ↦ ρ.restrict (disjointed K n)) (↑f) (𝓝 (ν n))
B : (Measure.sum fun n ↦ ↑(ν n)) univ ≤ ↑C
μ : FiniteMeasure E := ⟨Measure.sum fun n ↦ ↑(ν n), ⋯⟩
g : E →ᵇ ℝ
ε : ℝ
εpos : ε > 0
⊢ ∀ᶠ (x : FiniteMeasure E) in ↑f, dist (∫ (x : E), g x ∂↑(id x)) (∫ (x : E), g x ∂↑μ) < ε
Module: Mathlib.MeasureTheory.Measure.TightNormed

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

Tactic:
gcongr with i

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

Goal state before:
pp: case refine_2
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 : ∀ (n : ℕ) (r : ℝ), 0 < r → 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖ ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ),
    0 < r → (μ n).real {x | r < |⟪z, x⟫|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖
r : ℝ
hr : 0 < r
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦
    2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖

Tactic:
· refine ⟨4, ?_⟩
        simp only [eventually_map, eventually_atTop]
        exact ⟨0, fun n _ ↦ h_le_4 n r hr⟩

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 < ε
⊢ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ t ∈ C, μ (t ∆ ∅) < ε

Tactic:
intro ε εpos

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 < ε✝
ε : ℝ≥0∞
εpos : 0 < ε
⊢ ∃ t ∈ C, μ (t ∆ ∅) < ε
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 < ε✝
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
Dne : D.Nonempty
f : ℕ → Set α
hD : μ (⋂ n, (accumulate f n)ᶜ) = 0
hf : D = range f
fC : ∀ (n : ℕ), accumulate f n ∈ C
this : ⋃₀ D = ⋃ n, accumulate f n
i : ℕ
⊢ MeasurableSet (accumulate f i)ᶜ

Tactic:
rw [h]

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 < ε✝
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
Dne : D.Nonempty
f : ℕ → Set α
hD : μ (⋂ n, (accumulate f n)ᶜ) = 0
hf : D = range f
fC : ∀ (n : ℕ), accumulate f n ∈ C
this : ⋃₀ D = ⋃ n, accumulate f n
i : ℕ
⊢ MeasurableSet (accumulate f i)ᶜ