mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Group.ModularCharacter

Goal state before:
pp: G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : LocallyCompactSpace G
g h : G
⊢ modularCharacterFun (g * h) = modularCharacterFun g * modularCharacterFun h

Tactic:
borelize G
  have mul_g_meas : Measurable (· * g) := Measurable.mul_const (fun ⦃_⦄ a ↦ a) g
  have mul_h_meas : Measurable (· * h) := Measurable.mul_const (fun ⦃_⦄ a ↦ a) h
  let ν := MeasureTheory.Measure.haar (G := G)
  symm
  calc
    modularCharacterFun g * modularCharacterFun h =
      modularCharacterFun h * modularCharacterFun g := mul_comm _ _
    _ = haarScalarFactor (map (· * h) (map (· * g) ν)) (map (· * g) ν) *
      modularCharacterFun g := by
      rw [modularCharacterFun_eq_haarScalarFactor (map (· * g) ν) _]
    _ = haarScalarFactor (map (· * h) (map (· * g) ν)) (map (· * g) ν) *
      haarScalarFactor (map (· * g) ν) ν := rfl
    _ = haarScalarFactor (map (· * (g * h)) ν) ν := by simp only [map_map mul_h_meas mul_g_meas,
      comp_mul_right, ← haarScalarFactor_eq_mul]

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

Goal state before:
pp: R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
cts : ContinuousOn ((fun x ↦ ‖x‖) ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ univ)
⊢ ∃ x,
    ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
      ‖circleTransformBoundingFunction R z ↑y‖ ≤ ‖circleTransformBoundingFunction R z ↑x‖

Tactic:
have comp : IsCompact (closedBall z r ×ˢ [[0, 2 * π]]) := by
    apply_rules [IsCompact.prod, ProperSpace.isCompact_closedBall z r, isCompact_uIcc]

Goal state after:
R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
cts : ContinuousOn ((fun x ↦ ‖x‖) ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ univ)
comp : IsCompact (closedBall z r ×ˢ [[0, 2 * π]])
⊢ ∃ x,
    ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
      ‖circleTransformBoundingFunction R z ↑y‖ ≤ ‖circleTransformBoundingFunction R z ↑x‖
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace F
ω : E →L[𝕜] F
a b : E
⊢ ∫ᶜ (x : E) in Path.segment a b, ω = ω (b - a)

Tactic:
by
  let : NormedSpace ℝ F := .restrictScalars ℝ 𝕜 F
  simp [curveIntegral_segment]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue

Goal state before:
pp: a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
this :
  ∀ {a b : ℝ},
    ContinuousOn f [[a, b]] →
      IntervalIntegrable g μ a b →
        (∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x) →
          ¬a = b → a < b → ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
hab : b ≤ a
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (Ι b a), 0 ≤ g x

Tactic:
rwa [uIoc_comm]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue

Goal state before:
pp: a✝ b✝ : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
a b : ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
hab : a < b
s : Set ℝ := Ι a b
hs : s = Ioc a b
hs' : s ⊆ [[a, b]]
hs_conn : IsConnected s
⊢ IntegrableOn (fun x ↦ f x * g x) s μ

Tactic:
← intervalIntegrable_iff

Goal state after:
a✝ b✝ : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
a b : ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
hab : a < b
s : Set ℝ := Ι a b
hs : s = Ioc a b
hs' : s ⊆ [[a, b]]
hs_conn : IsConnected s
⊢ IntervalIntegrable (fun x ↦ f x * g x) μ a b
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue

Goal state before:
pp: a✝ b✝ : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
a b : ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
hab : a < b
s : Set ℝ := Ι a b
hs : s = Ioc a b
hs' : s ⊆ [[a, b]]
hs_conn : IsConnected s
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
⊢ IntegrableOn g s μ

Tactic:
← intervalIntegrable_iff

Goal state after:
a✝ b✝ : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
a b : ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
hab : a < b
s : Set ℝ := Ι a b
hs : s = Ioc a b
hs' : s ⊆ [[a, b]]
hs_conn : IsConnected s
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
⊢ IntervalIntegrable g μ a b
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
hfc : ContinuousOn f (segment ℝ a b)
hfd : ∀ t ∈ Ioo 0 1, LineDifferentiableAt ℝ f ((lineMap a b) t) (b - a)
hf' : ∀ᵐ (t : ℝ), t ∈ Ioo 0 1 → ‖lineDeriv ℝ f ((lineMap a b) t) (b - a)‖ ≤ C
g : ℝ → F := fun t ↦ f ((lineMap a b) t)
hgc : ContinuousOn g (Icc 0 1)
hdg : ∀ t ∈ Ioo 0 1, HasDerivAt g (lineDeriv ℝ f ((lineMap a b) t) (b - a)) t
⊢ ‖g 1 - g 0‖ ≤ C * volume.real {t | t ∈ Ioo 0 1 ∧ deriv g t ≠ 0}

Tactic:
apply norm_sub_le_mul_volume_of_norm_deriv_le_of_le zero_le_one hgc

Goal state after:
case hfd
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
hfc : ContinuousOn f (segment ℝ a b)
hfd : ∀ t ∈ Ioo 0 1, LineDifferentiableAt ℝ f ((lineMap a b) t) (b - a)
hf' : ∀ᵐ (t : ℝ), t ∈ Ioo 0 1 → ‖lineDeriv ℝ f ((lineMap a b) t) (b - a)‖ ≤ C
g : ℝ → F := ⋯
hgc : ContinuousOn g (Icc 0 1)
hdg : ∀ t ∈ Ioo 0 1, HasDerivAt g (lineDeriv ℝ f ((lineMap a b) t) (b - a)) t
⊢ DifferentiableOn ℝ g (Ioo 0 1)

case hnorm
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
hfc : ContinuousOn f (segment ℝ a b)
hfd : ∀ t ∈ Ioo 0 1, LineDifferentiableAt ℝ f ((lineMap a b) t) (b - a)
hf' : ∀ᵐ (t : ℝ), t ∈ Ioo 0 1 → ‖lineDeriv ℝ f ((lineMap a b) t) (b - a)‖ ≤ C
g : ℝ → F := ⋯
hgc : ContinuousOn g (Icc 0 1)
hdg : ∀ t ∈ Ioo 0 1, HasDerivAt g (lineDeriv ℝ f ((lineMap a b) t) (b - a)) t
⊢ ∀ᵐ (t : ℝ), t ∈ Ioo 0 1 → ‖deriv g t‖ ≤ C
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: case e_a.e_a
f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
k : ℕ
hk : k ∈ Finset.range (N - 1)
⊢ f (a + ↑(N - 1 - (1 + k) + 1) * (b - a) / ↑N) = f (b + ↑(k + 1) * (a - b) / ↑N)

Tactic:
add_comm 1,

Goal state after:
case e_a.e_a
f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
k : ℕ
hk : k ∈ Finset.range (N - 1)
⊢ f (a + ↑(N - 1 - (k + 1) + 1) * (b - a) / ↑N) = f (b + ↑(k + 1) * (a - b) / ↑N)
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f : X →C_c ℝ≥0
⊢ ↑(∫ (a : X), ↑(f a) ∂rieszMeasure Λ).toNNReal = ↑(Λ f)

pp: case hfi
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f : X →C_c ℝ≥0
⊢ Integrable (fun x ↦ ↑(f x)) (rieszMeasure Λ)

Tactic:
· rw [ENNReal.coe_inj, Real.toNNReal_of_nonneg (MeasureTheory.integral_nonneg (by intro a; simp)),
       NNReal.eq_iff, NNReal.coe_mk]
    exact integral_rieszMeasure Λ f

Goal state after:
case hfi
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f : X →C_c ℝ≥0
⊢ Integrable (fun x ↦ ↑(f x)) (rieszMeasure Λ)
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
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport ⇑f
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / ↑N
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  tsupport ⇑f = ⋃ j, E j ∧
    univ.PairwiseDisjoint E ∧
      (∀ (n : Fin N), ∀ x ∈ E n, a + ε' * ↑↑n < f x ∧ f x ≤ a + ε' * (↑↑n + 1)) ∧ ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun n ↦ a + ε' * (↑↑n + 1)
hE' : ∀ (n : Fin N), μ (E n) ≠ ∞
V : Fin N → Opens X
hV : ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport ⇑(g n) ⊆ (V n).carrier) ∧
    EqOn (∑ n, ⇑(g n)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), (g n) x ∈ Icc 0 1) ∧ ∀ (n : Fin N), HasCompactSupport ⇑(g n)
n : Fin N
hn : n ∈ Finset.univ
⊢ |a| + a + ε' * (↑↑n + 1) ≤ |a| + y n + ε'

Tactic:
rw [← add_assoc, le_add_iff_nonneg_right]

Goal state after:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport ⇑f
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / ↑N
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  tsupport ⇑f = ⋃ j, E j ∧
    univ.PairwiseDisjoint E ∧
      (∀ (n : Fin N), ∀ x ∈ E n, a + ε' * ↑↑n < f x ∧ f x ≤ a + ε' * (↑↑n + 1)) ∧ ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun n ↦ a + ε' * (↑↑n + 1)
hE' : ∀ (n : Fin N), μ (E n) ≠ ∞
V : Fin N → Opens X
hV : ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport ⇑(g n) ⊆ (V n).carrier) ∧
    EqOn (∑ n, ⇑(g n)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), (g n) x ∈ Icc 0 1) ∧ ∀ (n : Fin N), HasCompactSupport ⇑(g n)
n : Fin N
hn : n ∈ Finset.univ
⊢ 0 ≤ ε'
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : BorelSpace E
r : ℝ
t : E
⊢ ∫ (x : E), cexp (↑⟪r • x, t⟫ * I) ∂μ = ∫ (x : E), cexp (↑⟪x, r • t⟫ * I) ∂μ

Tactic:
inner_smul_right,

Goal state after:
E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : BorelSpace E
r : ℝ
t : E
⊢ ∫ (x : E), cexp (↑⟪r • x, t⟫ * I) ∂μ = ∫ (x : E), cexp (↑(r * ⟪x, t⟫) * I) ∂μ
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; equals (1 : Y → ↥I) ∘ f => rfl

Goal state after:
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: case a
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
x : X
U : Set X
hxU : x ∈ U
hU : IsOpen[inst✝¹] U
f : X → ↑I
hf : Continuous[inst✝¹, _] f
efx : f x = 0
hfU : stoneCechUnit ⁻¹' stoneCechExtend hf ⁻¹' {1}ᶜ ⊆ U
⊢ 0 ∉ {1}

Tactic:
mem_singleton_iff

Goal state after:
case a
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
x : X
U : Set X
hxU : x ∈ U
hU : IsOpen[inst✝¹] U
f : X → ↑I
hf : Continuous[inst✝¹, _] f
efx : f x = 0
hfU : stoneCechUnit ⁻¹' stoneCechExtend hf ⁻¹' {1}ᶜ ⊆ U
⊢ ¬0 = 1
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: case f_bdd
Ω : 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}) + ε
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioc 0 ‖f‖), ‖μ.real {a_1 | a ≤ f a_1}‖ ≤ μ.real univ

Tactic:
· apply Eventually.of_forall <| fun t ↦ ?_
      simp only [Real.norm_eq_abs, abs_of_nonneg measureReal_nonneg]
      exact measureReal_mono (subset_univ _)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
s : Set (α × β)
s_mble : MeasurableSet s
⊢ (μ.prod ν) s = (∫⁻ (y : β), ↑μ ((fun x ↦ (x, y)) ⁻¹' s) ∂↑ν).toNNReal

Tactic:
simp [coeFn_def, Measure.prod_apply_symm s_mble]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
s : Set (α × β)
s_mble : MeasurableSet s
⊢ (μ.prod ν) s = (∫⁻ (y : β), ↑μ ((fun x ↦ (x, y)) ⁻¹' s) ∂↑ν).toNNReal

Tactic:
simp [coeFn_def, Measure.prod_apply_symm s_mble]

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

Goal state before:
pp: case neg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f✝ f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left✝ : StrictAnti εs
εs_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (fun n ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto ((fun ε ↦ ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real (thickening ε {a | t ≤ f a})) ∘ fun n ↦ dist (μs n) ν + εs n)
    atTop (𝓝 (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real {a | t ≤ f a}))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
⊢ ∀ᶠ (n : ℕ) in atTop, ∫ (x : Ω), f x ∂↑(Ps n) ≤ ∫ (x : Ω), f x ∂↑P + δ

Tactic:
filter_upwards [key (aux _), ε_of_room <| Iio_mem_nhds <| half_pos <|
                      mul_pos (inv_pos.mpr norm_f_pos) δ_pos]
      with n hn hn'

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f✝ f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left✝ : StrictAnti εs
εs_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (fun n ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto ((fun ε ↦ ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real (thickening ε {a | t ≤ f a})) ∘ fun n ↦ dist (μs n) ν + εs n)
    atTop (𝓝 (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real {a | t ≤ f a}))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
hn :
  n ∈
    ((fun ε ↦ ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real (thickening ε {a | t ≤ f a})) ∘ fun n ↦ dist (μs n) ν + εs n) ⁻¹'
      Iio ((∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real {a | t ≤ f a}) + δ / 2)
hn' : n ∈ (fun x ↦ dist (μs x) ν + εs x) ⁻¹' Iio (‖f‖⁻¹ * δ / 2)
⊢ ∫ (x : Ω), f x ∂↑(Ps n) ≤ ∫ (x : Ω), f x ∂↑P + δ
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 φ • μ = map (⇑φ.symm) μ

Tactic:
rw [← mulEquivHaarChar_smul_map (map φ.symm μ) φ, map_map]

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
φ : G ≃ₜ* G
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
this : (map (⇑φ.symm) μ).Regular
⊢ mulEquivHaarChar φ • μ = mulEquivHaarChar φ • map (⇑φ ∘ ⇑φ.symm) μ

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.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
inst✝² : T2Space B
inst✝¹ : MeasurableSpace B
inst✝ : BorelSpace B
b : B
this : (map (fun x ↦ b * x) (H.inducedMeasure μA μC)).Regular
f : CompactlySupportedContinuousMap B ℝ
h : ∀ (x : B), f (b * x) = (f.comp (Homeomorph.mulLeft b).toCocompactMap) x
⊢ ∫ (x : B), f (b * x) ∂H.inducedMeasure μA μC = ∫ (x : B), f x ∂H.inducedMeasure μA μC

Tactic:
simp_rw [h, integral_inducedMeasure, integrate_apply]

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
inst✝⁴ : MeasurableSpace C
inst✝³ : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst✝² : T2Space B
inst✝¹ : MeasurableSpace B
inst✝ : BorelSpace B
b : B
this : (map (fun x ↦ b * x) (H.inducedMeasure μA μC)).Regular
f : CompactlySupportedContinuousMap B ℝ
h : ∀ (x : B), f (b * x) = (f.comp (Homeomorph.mulLeft b).toCocompactMap) x
⊢ ∫ (c : C), ((H.pushforward μA) (f.comp (Homeomorph.mulLeft b).toCocompactMap)) c ∂μC =
    ∫ (c : C), ((H.pushforward μA) f) c ∂μC
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: case h₁
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : ↑K → E := ⋯
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := ⋯
T : Set (FiniteMeasure ↑K) := ⋯
⊢ {μ | μ.mass ≤ C ∧ μ Kᶜ = 0} ⊆ F '' T

pp: case h₂
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : ↑K → E := ⋯
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := ⋯
T : Set (FiniteMeasure ↑K) := ⋯
⊢ F '' T ⊆ {μ | μ.mass ≤ C ∧ μ Kᶜ = 0}

Tactic:
· intro μ hμ
      simp only [mem_image]
      refine ⟨μ.comap f, (FiniteMeasure.mass_comap_le _ _).trans hμ.1, ?_⟩
      ext s hs
      simp only [toMeasure_map, F]
      rw [Measure.map_apply measurable_subtype_coe hs]
      simp only [toMeasure_comap]
      rw [Measure.comap_apply _ (Subtype.val_injective), image_preimage_eq_inter_range]
      · rw [← Measure.restrict_apply hs, Measure.restrict_eq_self_of_ae_mem]
        apply (null_iff_toMeasure_null (↑μ) (range f)ᶜ).mp
        rw [rf]
        exact hμ.2
      · exact fun t ht ↦ hf.measurableEmbedding.measurableSet_image' ht
      · exact hf.continuous.measurable hs

Goal state after:
case h₂
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : ↑K → E := ⋯
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := ⋯
T : Set (FiniteMeasure ↑K) := ⋯
⊢ F '' T ⊆ {μ | μ.mass ≤ C ∧ μ Kᶜ = 0}
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 →ᵇ ℝ
ε : ℝ
εpos : ε > 0
⊢ Tendsto (fun n ↦ ∫ (x : E), g x ∂∑ i ∈ Finset.range n, ↑(ν i)) atTop (𝓝 (∑' (i : ℕ), ∫ (x : E), g x ∂↑(ν i)))

Tactic:
simp_rw [integral_finsetSum_measure (fun i hi ↦ g.integrable _)]

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
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, ∫ (a : E), g a ∂↑(ν i)) atTop (𝓝 (∑' (i : ℕ), ∫ (x : E), g x ∂↑(ν i)))
Module: Mathlib.MeasureTheory.Measure.TightNormed

Goal state before:
pp: case inl
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_2
ι : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype ι
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι 𝕜 E
h : ∀ (i : ι), Tendsto (fun r ↦ ⨆ μ ∈ S, μ {x | r < ‖⟪b i, x⟫_𝕜‖}) atTop (𝓝 0)
hE : Subsingleton E
⊢ IsTightMeasureSet S

Tactic:
simp only [IsTightMeasureSet, cocompact_eq_bot, smallSets_bot]

Goal state after:
case inl
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_2
ι : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype ι
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι 𝕜 E
h : ∀ (i : ι), Tendsto (fun r ↦ ⨆ μ ∈ S, μ {x | r < ‖⟪b i, x⟫_𝕜‖}) atTop (𝓝 0)
hE : Subsingleton E
⊢ Tendsto (⨆ μ ∈ S, ⇑μ) (pure ∅) (𝓝 0)