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

Goal state before:
pp: case e'_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : ∫ (x : Ω), X x ∂P = 0
h1 : ∫ (x : Ω), (X ^ 2) x ∂P = 1
x✝ : ℝ
⊢ x✝ = x✝ - 0

pp: case convert_7
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : ∫ (x : Ω), X x ∂P = 0
h1 : ∫ (x : Ω), (X ^ 2) x ∂P = 1
⊢ ContDiff ℝ (↑2) (charFun (Measure.map X P))

Tactic:
· simp

Goal state after:
case convert_7
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : ∫ (x : Ω), X x ∂P = 0
h1 : ∫ (x : Ω), (X ^ 2) x ∂P = 1
⊢ ContDiff ℝ (↑2) (charFun (Measure.map X P))
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
Y : Type v
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyRegularSpace Y
f : X → Y
hf : IsInducing f
x : X
K : Set Y
hK : IsClosed[inst✝¹] K
hxK : f x ∉ K
g : Y → ↑I
hcf : Continuous[inst✝¹, _] g
egfx : g (f x) = 0
hgK : EqOn g 1 K
| EqOn (g ∘ f) 1 (f ⁻¹' K)

Tactic:
arg 2

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
Y : Type v
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyRegularSpace Y
f : X → Y
hf : IsInducing f
x : X
K : Set Y
hK : IsClosed[inst✝¹] K
hxK : f x ∉ K
g : Y → ↑I
hcf : Continuous[inst✝¹, _] g
egfx : g (f x) = 0
hgK : EqOn g 1 K
| 1
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
⊢ ∫ (x : E), cexp (↑((u • L) x) * I) ∂μ = ∫ (x : E), cexp (↑u * ↑(L x) * I) ∂μ

pp: case hφ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
⊢ AEMeasurable (⇑L) μ

pp: case hfm
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
⊢ AEStronglyMeasurable (fun x ↦ cexp (↑u * ↑x * I)) (Measure.map (⇑L) μ)

Tactic:
· simp

Goal state after:
case hφ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
⊢ AEMeasurable (⇑L) μ

case hfm
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
⊢ AEStronglyMeasurable (fun x ↦ cexp (↑u * ↑x * I)) (Measure.map (⇑L) μ)
Module: Mathlib.MeasureTheory.Measure.DiracProba

Goal state before:
pp: X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
U : Set X
U_nhds : U ∈ 𝓝 x
hU : ∃ᶠ (x : X) in L, x ∉ U
Uint_nhds : interior U ∈ 𝓝 x
⊢ ?m.81 ∉ (interior ?m.77)ᶜ

Tactic:
simpa only [mem_compl_iff, not_not] using mem_of_mem_nhds Uint_nhds

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

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
μ ν : Measure Ω
⊢ levyProkhorovEDist μ ν ≤ max (μ univ) (ν univ)

Tactic:
refine sInf_le fun B _ ↦ ⟨?_, ?_⟩ <;> apply le_add_left <;> simp [measure_mono]

Goal state after:
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]; exact charFunDual_pi

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

Goal state before:
pp: Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
intble₂ : IntegrableOn (fun t ↦ ν.real (thickening ε {a | t ≤ f a})) (Ioc 0 ‖f‖) volume
⊢ ∫ (x : ℝ) in Ioc 0 ‖f‖, ν.real (thickening ε {a | x ≤ f a}) + ε ≤
    (∫ (t : ℝ) in Ioc 0 ‖f‖, ν.real (thickening ε {a | t ≤ f a})) + ε * ‖f‖

Tactic:
integral_add

Goal state after:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
intble₂ : IntegrableOn (fun t ↦ ν.real (thickening ε {a | t ≤ f a})) (Ioc 0 ‖f‖) volume
⊢ (∫ (a : ℝ) in Ioc 0 ‖f‖, ν.real (thickening ε {a_1 | a ≤ f a_1})) + ∫ (a : ℝ) in Ioc 0 ‖f‖, ε ≤
    (∫ (t : ℝ) in Ioc 0 ‖f‖, ν.real (thickening ε {a | t ≤ f a})) + ε * ‖f‖

case hf
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
intble₂ : IntegrableOn (fun t ↦ ν.real (thickening ε {a | t ≤ f a})) (Ioc 0 ‖f‖) volume
⊢ Integrable (fun x ↦ ν.real (thickening ε {a | x ≤ f a})) (volume.restrict (Ioc 0 ‖f‖))

case hg
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
intble₂ : IntegrableOn (fun t ↦ ν.real (thickening ε {a | t ≤ f a})) (Ioc 0 ‖f‖) volume
⊢ Integrable (fun x ↦ ε) (volume.restrict (Ioc 0 ‖f‖))
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
a✝ b c d : E
γ₁ : Path a✝ b
γ₂ : Path c d
s : Set (↑I × ↑I)
t : Set E
ω : E → E →L[ℝ] F
dω : E → E →L[ℝ] E →L[ℝ] F
φ : (↑γ₁).Homotopy ↑γ₂
hs : s.Countable
hφt : ∀ a ∈ Ioo 0 1, ∀ b_1 ∈ Ioo 0 1, φ (a, b_1) ∈ t
hω : ∀ a ∈ Ioo 0 1, ∀ b_1 ∈ Ioo 0 1, (a, b_1) ∉ s → HasFDerivWithinAt ω (dω (φ (a, b_1))) t (φ (a, b_1))
hωc : ContinuousOn ω (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
hdω_symm :
  ∀ a ∈ Ioo 0 1,
    ∀ b_1 ∈ Ioo 0 1,
      (a, b_1) ∉ s →
        ∀ u ∈ tangentConeAt ℝ t (φ (a, b_1)),
          ∀ v ∈ tangentConeAt ℝ t (φ (a, b_1)), ((dω (φ (a, b_1))) u) v = ((dω (φ (a, b_1))) v) u
U : Set (ℝ × ℝ) := Ioo 0 1 ×ˢ Ioo 0 1
hU : U = Ioo 0 1 ×ˢ Ioo 0 1
hinterior : interior (Icc 0 1) = U
hunique : UniqueDiffOn ℝ (Icc 0 1)
hUopen : IsOpen U
hU_subset : U ⊆ Icc 0 1
hclosure : closure U = Icc 0 1
ψ : ℝ × ℝ → E := fun xy ↦ Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2
hcontdiff : ContDiffOn ℝ 2 ψ (Icc 0 1)
hψ : ψ = fun xy ↦ Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2
hψφ : ∀ (a b_1 : ↑I), ψ (↑a, ↑b_1) = φ (a, b_1)
hψ_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ψ
hψUt : MapsTo ψ U t
dψ : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fderivWithin ℝ ψ (Icc 0 1)
s' : Set (ℝ × ℝ) := Prod.map Subtype.val Subtype.val '' s
hs' : s' = Prod.map Subtype.val Subtype.val '' s
hmem_s' : ∀ (x y : ↑I), (↑x, ↑y) ∈ s' ↔ (x, y) ∈ s
hs'c : s'.Countable
hdψ : ∀ a ∈ U, HasFDerivAt ψ (dψ a) a
d2ψ : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ →L[ℝ] E := fderivWithin ℝ dψ (Icc 0 1)
hd2ψ : ∀ a ∈ U, HasFDerivAt dψ (d2ψ a) a
hd2ψ_symm : ∀ a ∈ Icc 0 1, ∀ (x y : ℝ × ℝ), ((d2ψ a) x) y = ((d2ψ a) y) x
η : ℝ × ℝ → ℝ × ℝ →L[ℝ] F := fun a ↦ ω (ψ a) ∘SL dψ a
f : ℝ × ℝ → F := fun a ↦ (η a) (0, 1)
hf : ∀ a ∈ Icc 0 1, f a = (ω (ψ a)) (derivWithin (ψ ∘ fun x ↦ (a.1, x)) I a.2)
g : ℝ × ℝ → F := fun a ↦ -(η a) (1, 0)
hg : ∀ a ∈ Icc 0 1, g a = (ω (ψ a)) (-derivWithin (ψ ∘ fun x ↦ (x, a.2)) I a.1)
dη : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ →L[ℝ] F :=
  fun a ↦ (ContinuousLinearMap.compL ℝ (ℝ × ℝ) E F) (ω (ψ a)) ∘SL d2ψ a + (dω (ψ a)).bilinearComp (dψ a) (dψ a)
hdη : ∀ a ∈ U \ s', HasFDerivAt η (dη a) a
hdη_symm : ∀ a ∈ U \ s', ∀ (u v : ℝ × ℝ), ((dη a) u) v = ((dη a) v) u
f' : ℝ × ℝ → ℝ × ℝ →L[ℝ] F := fun a ↦ (ContinuousLinearMap.apply ℝ F) (0, 1) ∘SL dη a
a : ℝ × ℝ
ha : a ∈ U \ s'
⊢ HasFDerivAt f (f' a) a

Tactic:
exact (ContinuousLinearMap.apply ℝ F (0, 1)).hasFDerivAt.comp a (hdη a ha)

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

Goal state before:
pp: 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
f : CompactlySupportedContinuousMap B E
b : B
h : ψ ((Function.invFun (⇑ψ) (ψ b))⁻¹ * b) = 1
⊢ ∫ (a : A), (H.pullback f (Function.invFun (⇑ψ) (ψ b))) a ∂μA = ∫ (a : A), (H.pullback f b) a ∂μA

Tactic:
rw [← ψ.mem_ker, H.mulExact.monoidHom_ker_eq] at h

Goal state after:
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
f : CompactlySupportedContinuousMap B E
b : B
h : (Function.invFun (⇑ψ) (ψ b))⁻¹ * b ∈ φ.range
⊢ ∫ (a : A), (H.pullback f (Function.invFun (⇑ψ) (ψ b))) a ∂μA = ∫ (a : A), (H.pullback f b) a ∂μA
Module: Mathlib.MeasureTheory.Measure.Haar.Extension

Goal state before:
pp: 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
⊢ Continuous fun c ↦ ∫ (a : A), (H.pullback f (Function.invFun (⇑ψ) c)) a ∂μA

Tactic:
let := IsTopologicalGroup.rightUniformSpace B

Goal state after:
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
⊢ Continuous fun c ↦ ∫ (a : A), (H.pullback f (Function.invFun (⇑ψ) c)) a ∂μA
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
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ.Regular
φ : G ≃ₜ* G
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
this : (map (⇑φ.symm) μ).Regular
⊢ mulEquivHaarChar φ • μ = mulEquivHaarChar φ • map (⇑φ ∘ ⇑φ.symm) μ

pp: case hg
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : LocallyCompactSpace G
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ.Regular
φ : G ≃ₜ* G
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
this : (map (⇑φ.symm) μ).Regular
⊢ Measurable ⇑φ

pp: case hf
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : LocallyCompactSpace G
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ.Regular
φ : G ≃ₜ* G
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
this : (map (⇑φ.symm) μ).Regular
⊢ Measurable ⇑φ.symm

Tactic:
· simp

Goal state after:
case hg
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : LocallyCompactSpace G
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ.Regular
φ : G ≃ₜ* G
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
this : (map (⇑φ.symm) μ).Regular
⊢ Measurable ⇑φ

case hf
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : LocallyCompactSpace G
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ.Regular
φ : G ≃ₜ* G
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
this : (map (⇑φ.symm) μ).Regular
⊢ Measurable ⇑φ.symm
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
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ.Regular
f : G → ℝ
φ : G ≃ₜ* G
⊢ mulEquivHaarChar φ • ∫ (a : G), f a ∂map (⇑φ) μ = ∫ (a : G), f a ∂μ

Tactic:
by
  nth_rw 2 [← mulEquivHaarChar_smul_map μ φ]
  simp

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
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ.Regular
X : Set G
φ : G ≃ₜ* G
⊢ mulEquivHaarChar φ • μ (⇑φ ⁻¹' X) = (mulEquivHaarChar φ • map (⇑φ) μ) X

Tactic:
simp only [Measure.smul_apply, nnreal_smul_coe_apply]

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
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ.Regular
X : Set G
φ : G ≃ₜ* G
⊢ ↑(mulEquivHaarChar φ) * μ (⇑φ ⁻¹' X) = ↑(mulEquivHaarChar φ) * (map (⇑φ) μ) X
Module: Mathlib.MeasureTheory.Measure.Haar.Extension

Goal state before:
pp: 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
inst✝¹ : MeasurableSpace C
inst✝ : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
f g : CompactlySupportedContinuousMap B E
⊢ ∫ (c : C), ((H.pushforward μA) (f + g)) c ∂μC =
    ∫ (c : C), ((H.pushforward μA) f) c ∂μC + ∫ (c : C), ((H.pushforward μA) g) c ∂μC

Tactic:
by
    rw [map_add]
    exact integral_add (pushforward H μA f).integrable (pushforward H μA g).integrable

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

Goal state before:
pp: Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
⊢ ∃ As,
    (∀ (n : ℕ), MeasurableSet (As n)) ∧
      (∀ (n : ℕ), Bornology.IsBounded (As n)) ∧
        (∀ (n : ℕ), diam (As n) ≤ ε) ∧ ⋃ n, As n = univ ∧ Pairwise fun n m ↦ Disjoint (As n) (As m)

Tactic:
by
  cases isEmpty_or_nonempty Ω
  · refine ⟨fun _ ↦ ∅, fun _ ↦ MeasurableSet.empty, fun _ ↦ Bornology.isBounded_empty, ?_, ?_,
            fun _ _ _ ↦ disjoint_of_subsingleton⟩
    · intro n
      simpa only [diam_empty] using ε_pos.le
    · subsingleton
  obtain ⟨xs, xs_dense⟩ := exists_dense_seq Ω
  have half_ε_pos : 0 < ε / 2 := half_pos ε_pos
  set Bs := fun n ↦ Metric.ball (xs n) (ε / 2)
  set As := disjointed Bs
  refine ⟨As, ?_, ?_, ?_, ?_, ?_⟩
  · exact MeasurableSet.disjointed (fun n ↦ measurableSet_ball)
  · exact fun n ↦ Bornology.IsBounded.subset isBounded_ball <| disjointed_subset Bs n
  · intro n
    apply (diam_mono (disjointed_subset Bs n) isBounded_ball).trans
    convert! diam_ball half_ε_pos.le
    ring
  · have aux : ⋃ n, Bs n = univ := by
      convert! DenseRange.iUnion_uniformity_ball xs_dense <| Metric.dist_mem_uniformity half_ε_pos
      exact (ball_eq_ball' _ _).symm
    simpa only [← aux] using iUnion_disjointed
  · exact disjoint_disjointed Bs

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

Goal state before:
pp: case e'_3
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
L : StrongDual ℝ E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (Measure.map (⇑L) μ)
⊢ μ.real {x | r < |L x|} = μ.real (⇑L ⁻¹' {x | r < |x|})

pp: case e'_3
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
L : StrongDual ℝ E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (Measure.map (⇑L) μ)
⊢ MeasurableSet {x | r < |x|}

Tactic:
· simp

Goal state after:
case e'_3
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
L : StrongDual ℝ E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (Measure.map (⇑L) μ)
⊢ MeasurableSet {x | r < |x|}
Module: Mathlib.MeasureTheory.Measure.IntegralCharFun

Goal state before:
pp: case e'_3
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
mE : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
a : E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (Measure.map (fun x ↦ ⟪a, x⟫) μ)
⊢ μ.real {x | r < |⟪a, x⟫|} = μ.real ((fun x ↦ ⟪a, x⟫) ⁻¹' {x | r < |x|})

pp: case e'_3
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
mE : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
a : E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (Measure.map (fun x ↦ ⟪a, x⟫) μ)
⊢ MeasurableSet {x | r < |x|}

Tactic:
· simp

Goal state after:
case e'_3
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
mE : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
a : E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (Measure.map (fun x ↦ ⟪a, x⟫) μ)
⊢ MeasurableSet {x | r < |x|}
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: case hf
E : Type u_1
inst✝⁴ : MeasurableSpace E
inst✝³ : TopologicalSpace E
inst✝² : T2Space E
inst✝¹ : BorelSpace E
inst✝ : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C} ∈ f
g : E →C_c ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
⊢ Integrable (fun x ↦ -‖g.toBoundedContinuousFunction‖) ↑μ

pp: case hg
E : Type u_1
inst✝⁴ : MeasurableSpace E
inst✝³ : TopologicalSpace E
inst✝² : T2Space E
inst✝¹ : BorelSpace E
inst✝ : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C} ∈ f
g : E →C_c ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
⊢ Integrable (fun x ↦ g x) ↑μ

pp: case h
E : Type u_1
inst✝⁴ : MeasurableSpace E
inst✝³ : TopologicalSpace E
inst✝² : T2Space E
inst✝¹ : BorelSpace E
inst✝ : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C} ∈ f
g : E →C_c ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
⊢ (fun x ↦ -‖g.toBoundedContinuousFunction‖) ≤ fun x ↦ g x

Tactic:
· simp

Goal state after:
case hg
E : Type u_1
inst✝⁴ : MeasurableSpace E
inst✝³ : TopologicalSpace E
inst✝² : T2Space E
inst✝¹ : BorelSpace E
inst✝ : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C} ∈ f
g : E →C_c ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
⊢ Integrable (fun x ↦ g x) ↑μ

case h
E : Type u_1
inst✝⁴ : MeasurableSpace E
inst✝³ : TopologicalSpace E
inst✝² : T2Space E
inst✝¹ : BorelSpace E
inst✝ : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C} ∈ f
g : E →C_c ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
⊢ (fun x ↦ -‖g.toBoundedContinuousFunction‖) ≤ fun x ↦ g x
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: case hg
E : Type u_1
inst✝⁴ : MeasurableSpace E
inst✝³ : TopologicalSpace E
inst✝² : T2Space E
inst✝¹ : BorelSpace E
inst✝ : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C} ∈ f
g : E →C_c ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
⊢ Integrable (fun x ↦ ‖g.toBoundedContinuousFunction‖) ↑μ

pp: case h
E : Type u_1
inst✝⁴ : MeasurableSpace E
inst✝³ : TopologicalSpace E
inst✝² : T2Space E
inst✝¹ : BorelSpace E
inst✝ : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C} ∈ f
g : E →C_c ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
⊢ (fun x ↦ g x) ≤ fun x ↦ ‖g.toBoundedContinuousFunction‖

Tactic:
· simp

Goal state after:
case h
E : Type u_1
inst✝⁴ : MeasurableSpace E
inst✝³ : TopologicalSpace E
inst✝² : T2Space E
inst✝¹ : BorelSpace E
inst✝ : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C} ∈ f
g : E →C_c ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
⊢ (fun x ↦ g x) ≤ fun x ↦ ‖g.toBoundedContinuousFunction‖