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

Goal state before:
pp: case a
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
k : Set X
hk : IsCompact k
μ : Measure X
inst✝³ : IsFiniteMeasureOnCompacts μ
inst✝² : μ.InnerRegularCompactLTTop
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
f : X → ℝ
f_cont : Continuous f
f_comp : HasCompactSupport f
⊢ EqOn f 1 k → 0 ≤ f → μ k ≤ ENNReal.ofReal (∫ (x : X), f x ∂μ)

Tactic:
fk

Goal state after:
case a
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
k : Set X
hk : IsCompact k
μ : Measure X
inst✝³ : IsFiniteMeasureOnCompacts μ
inst✝² : μ.InnerRegularCompactLTTop
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
f : X → ℝ
f_cont : Continuous f
f_comp : HasCompactSupport f
fk : EqOn f 1 k
⊢ 0 ≤ f → μ k ≤ ENNReal.ofReal (∫ (x : X), f x ∂μ)
Module: Mathlib.Order.Interval.Set.Union

Goal state before:
pp: X : Type u_1
inst✝ : LinearOrder X
a : ℕ → X
N : ℕ
ih : Ioc (a 0) (a N) ⊆ ⋃ i ∈ Finset.range N, Ioc (a i) (a (i + 1))
⊢ Ioc (a 0) (a N) ∪ Ioc (a N) (a (N + 1)) ⊆ ⋃ i ∈ Finset.range (N + 1), Ioc (a i) (a (i + 1))

Tactic:
by simpa [Finset.range_add_one] using
                  union_subset_union_right (Ioc (a N) (a (N + 1))) ih

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

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
⊢ h / 2 *
      (∑ k ∈ Finset.range (N - 1), f (a + ↑(k + 1) * h) + f (a + ↑0 * h) +
        (∑ x ∈ Finset.range (N - 1), f (a + (↑x + 1) * h) + f (a + (↑(N - 1) + 1) * h))) =
    h * ((f a + f (a + ↑(N - 1 + 1) * h)) / 2 + ∑ x ∈ Finset.range (N - 1 + 1 - 1), f (a + (↑x + 1) * h))

Tactic:
add_add_add_comm,

Goal state after:
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
⊢ h / 2 *
      (∑ k ∈ Finset.range (N - 1), f (a + ↑(k + 1) * h) + ∑ x ∈ Finset.range (N - 1), f (a + (↑x + 1) * h) +
        (f (a + ↑0 * h) + f (a + (↑(N - 1) + 1) * h))) =
    h * ((f a + f (a + ↑(N - 1 + 1) * h)) / 2 + ∑ x ∈ Finset.range (N - 1 + 1 - 1), f (a + (↑x + 1) * h))
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
⊢ {f | ∀ x ∈ K, 1 ≤ f x}.Nonempty

Tactic:
have hIsCompact_closure_interior : IsCompact (closure (interior V)) := by
    apply IsCompact.of_isClosed_subset hVcp isClosed_closure
    nth_rw 2 [← closure_eq_iff_isClosed.mpr (IsCompact.isClosed hVcp)]
    exact closure_mono interior_subset

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
hIsCompact_closure_interior : IsCompact (closure (interior V))
⊢ {f | ∀ x ∈ K, 1 ≤ f x}.Nonempty
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : s₀ᶜ ∪ s₁ᶜ = univ
hst : s₀ ∪ s₁ ⊆ t
so : Fin 2 → Set X := fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
x : X
hx : x ∈ t
⊢ ∃ i, x ∈ if i = 0 then s₀ᶜ else s₁ᶜ

Tactic:
have h : x ∈ s₀ᶜ ∨ x ∈ s₁ᶜ := by
      rw [← mem_union, disj]
      exact mem_univ _

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : s₀ᶜ ∪ s₁ᶜ = univ
hst : s₀ ∪ s₁ ⊆ t
so : Fin 2 → Set X := fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
x : X
hx : x ∈ t
h : x ∈ s₀ᶜ ∨ x ∈ s₁ᶜ
⊢ ∃ i, x ∈ if i = 0 then s₀ᶜ else s₁ᶜ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / ↑N
ak : ℕ → ℝ := fun k ↦ a + ↑k * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + ↑N * h
this : ∀ k ∈ Finset.range N, |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ ζ / 12 * h ^ 3
⊢ ∑ k ∈ Finset.range N, ζ / 12 * h ^ 3 = ↑N * (ζ / 12 * h ^ 3)

Tactic:
by simp [sum_const]

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

Goal state before:
pp: f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / ↑N
ak : ℕ → ℝ := fun k ↦ a + ↑k * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + ↑N * h
k : ℕ
hk : k < N
⊢ a ≤ ak k

Tactic:
simp only [ak, le_add_iff_nonneg_right]

Goal state after:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / ↑N
ak : ℕ → ℝ := fun k ↦ a + ↑k * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + ↑N * h
k : ℕ
hk : k < N
⊢ 0 ≤ ↑k * h
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / ↑N
ak : ℕ → ℝ := fun k ↦ a + ↑k * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + ↑N * h
k : ℕ
hk : k < N
h1 : a ≤ ak k
h2 : ak (k + 1) ≤ b
h3 : Set.Icc (ak k) (ak (k + 1)) ⊆ Set.Icc a b
h4 : ak k < ak (k + 1)
h5 :
  EqOn (_root_.derivWithin f (Set.Icc a b)) (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1))))
    (Set.Icc (ak k) (ak (k + 1)))
h6 :
  EqOn (iteratedDerivWithin 2 f (Set.Icc a b)) (iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))))
    (Set.Icc (ak k) (ak (k + 1)))
h7 : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x| ≤ ζ
⊢ |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ ζ / 12 * h ^ 3

Tactic:
refine (trapezoidal_error_le_of_lt' (ζ := ζ) h4 (h_df.mono h3) ?_ h7).trans_eq ?_

Goal state after:
case refine_1
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / ↑N
ak : ℕ → ℝ := fun k ↦ a + ↑k * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + ↑N * h
k : ℕ
hk : k < N
h1 : a ≤ ak k
h2 : ak (k + 1) ≤ b
h3 : Set.Icc (ak k) (ak (k + 1)) ⊆ Set.Icc a b
h4 : ak k < ak (k + 1)
h5 :
  EqOn (_root_.derivWithin f (Set.Icc a b)) (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1))))
    (Set.Icc (ak k) (ak (k + 1)))
h6 :
  EqOn (iteratedDerivWithin 2 f (Set.Icc a b)) (iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))))
    (Set.Icc (ak k) (ak (k + 1)))
h7 : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x| ≤ ζ
⊢ DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1)))) (Set.Icc (ak k) (ak (k + 1)))

case refine_2
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / ↑N
ak : ℕ → ℝ := fun k ↦ a + ↑k * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + ↑N * h
k : ℕ
hk : k < N
h1 : a ≤ ak k
h2 : ak (k + 1) ≤ b
h3 : Set.Icc (ak k) (ak (k + 1)) ⊆ Set.Icc a b
h4 : ak k < ak (k + 1)
h5 :
  EqOn (_root_.derivWithin f (Set.Icc a b)) (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1))))
    (Set.Icc (ak k) (ak (k + 1)))
h6 :
  EqOn (iteratedDerivWithin 2 f (Set.Icc a b)) (iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))))
    (Set.Icc (ak k) (ak (k + 1)))
h7 : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x| ≤ ζ
⊢ (ak (k + 1) - ak k) ^ 3 * ζ / 12 = ζ / 12 * h ^ 3
Module: Mathlib.MeasureTheory.Integral.TorusIntegral

Goal state before:
pp: n : ℕ
E : Type u_1
inst✝ : NormedAddCommGroup E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
⊢ TorusIntegrable f c 0

Tactic:
rw [TorusIntegrable, torusMap_zero_radius]

Goal state after:
n : ℕ
E : Type u_1
inst✝ : NormedAddCommGroup E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
⊢ IntegrableOn (fun θ ↦ f (const (Fin n → ℝ) c θ)) (Icc 0 fun x ↦ 2 * π) volume
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
μ ν : Measure X
inst✝¹ : μ.Regular
inst✝ : ν.Regular
hμν : ∀ (f : X →C_c ℝ≥0), ∫ (x : X), ↑(f x) ∂μ = ∫ (x : X), ↑(f x) ∂ν
⊢ μ = ν

Tactic:
apply Measure.ext_of_integral_eq_on_compactlySupported

Goal state after:
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : T2Space X
inst✝⁴ : LocallyCompactSpace X
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
μ ν : Measure X
inst✝¹ : μ.Regular
inst✝ : ν.Regular
hμν : ∀ (f : X →C_c ℝ≥0), ∫ (x : X), ↑(f x) ∂μ = ∫ (x : X), ↑(f x) ∂ν
⊢ ∀ (f : X →C_c ℝ), ∫ (x : X), f x ∂μ = ∫ (x : X), f x ∂ν
Module: Mathlib.MeasureTheory.Integral.TorusIntegral

Goal state before:
pp: case hf
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := (MeasurableEquiv.piFinSuccAbove (fun x ↦ ℝ) i).symm
hem : MeasurePreserving (⇑e) volume volume
heπ : (⇑e ⁻¹' Icc 0 fun x ↦ 2 * π) = Icc 0 (2 * π) ×ˢ Icc 0 fun x ↦ 2 * π
⊢ IntegrableOn (fun x ↦ (∏ i, ↑(R i) * cexp (↑(e x i) * I) * I) • f (torusMap c R (e x)))
    (Icc 0 (2 * π) ×ˢ Icc 0 fun x ↦ 2 * π) (volume.prod volume)

Tactic:
· have := hf.function_integrable
    rwa [← hem.integrableOn_comp_preimage e.measurableEmbedding, heπ] at this

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Card

Goal state before:
pp: case basic
α : Type u
s : Set (Set α)
t u : Set α
hu : u ∈ s
⊢ u ∈ generateMeasurableRec s (ω_ 1)

Tactic:
exact self_subset_generateMeasurableRec s _ hu

Goal state after:
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:
by rw [← add_assoc, le_add_iff_nonneg_right]; exact le_of_lt hε'.1

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

Goal state before:
pp: α : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
inst✝ : OpensMeasurableSpace α
f : α →ᵇ ℝ
μ : Measure α
f_nn : 0 ≤ᵐ[μ] ⇑f
hf : HasFiniteIntegral (⇑f) μ
⊢ ∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Ioc 0 ‖f‖, μ.real {a | t ≤ f a}

Tactic:
rw [Integrable.integral_eq_integral_Ioc_meas_le (M := ‖f‖) ?_ f_nn ?_]
  · exact ⟨f.continuous.measurable.aestronglyMeasurable, hf⟩
  · exact Eventually.of_forall (fun x ↦ BoundedContinuousFunction.apply_le_norm f x)

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : volume A ≠ ∞
μ : ProbabilityMeasure Ω
t : ℝ
⊢ ∃ R > 0, ↑μ (thickening R {a | t ≤ f a}) ≠ ∞

pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : volume A ≠ ∞
μ : ProbabilityMeasure Ω
t : ℝ
⊢ IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] {a | t ≤ f a}

Tactic:
· exact ⟨1, ⟨Real.zero_lt_one, measure_ne_top _ _⟩⟩

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : volume A ≠ ∞
μ : ProbabilityMeasure Ω
t : ℝ
⊢ IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] {a | t ≤ f a}
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✝³ : 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
⊢ K.indicator 1 x ≤ f x

Tactic:
by_cases hx : x ∈ K

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

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.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✝² : LocallyCompactSpace X
inst✝¹ : μ.Regular
inst✝ : ν.Regular
hμν : ∀ (f : X →C_c ℝ), ∫ (x : X), f x ∂μ = ∫ (x : X), f x ∂ν
⊢ ∀ (U : Set X), IsCompact U → μ U = ν U

Tactic:
intro K hK

Goal state after:
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 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 ∂μ'

Tactic:
simp only [BoundedContinuousFunction.compContinuous_apply, ContinuousMap.coe_mk]

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 ↑x ∂μ'
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
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
this : (map (⇑e.symm) μ).IsHaarMeasure
⊢ ∫ (a : G), f a ∂comap (⇑e) μ = mulEquivHaarChar φ • ∫ (a : G), f a ∂μ

Tactic:
have : (map (e.symm) μ).Regular := Regular.map φ.symm.toHomeomorph

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
f : G → ℝ
φ : G ≃ₜ* G
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
this✝ : (map (⇑e.symm) μ).IsHaarMeasure
this : (map (⇑e.symm) μ).Regular
⊢ ∫ (a : G), f a ∂comap (⇑e) μ = mulEquivHaarChar φ • ∫ (a : G), f a ∂μ
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
P : ProbabilityMeasure Ω
ε : ℝ
ε_pos : ε > 0
third_ε_pos : 0 < ε / 3
third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)
Es : ℕ → Set Ω
Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)
Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)
Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3
Es_cover : ⋃ n, Es n = univ
Es_disjoint : Pairwise fun n m ↦ Disjoint (Es n) (Es m)
N : ℕ
hN : ↑P (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)
Js_finite : {J | J ⊆ Iio N}.Finite
Gs : Set (Set Ω) := ⋯
Gs_open :
  ∀ (J : Set ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening (ε / 3) (⋃ j ∈ J, Es j))
mem_nhds_P :
  ∀ (G : Set Ω),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G → {Q | ↑P G < ↑Q G + ENNReal.ofReal (ε / 3)} ∈ 𝓝 P
Q : ProbabilityMeasure Ω
δ : ℝ
B : Set Ω
δ_gt : 2 * (ε / 3) < δ
x✝ : MeasurableSet B
JB : Set ℕ := ⋯
hQ : ↑P (⋃ i ∈ JB, thickening (ε / 3) (Es i)) < ↑Q (⋃ i ∈ JB, thickening (ε / 3) (Es i)) + ENNReal.ofReal (ε / 3)
B_subset : B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ (⋃ j ∈ Iio N, Es j)ᶜ
subset_thickB : ⋃ i ∈ JB, thickening (ε / 3) (Es i) ⊆ thickening δ B
⊢ ↑Q (⋃ i ∈ JB, thickening (ε / 3) (Es i)) + ENNReal.ofReal (ε / 3) + ENNReal.ofReal (ε / 3) ≤
    ↑(ofMeasure Q).toMeasure (thickening δ B) + ENNReal.ofReal δ

Tactic:
rw [add_assoc, ← ENNReal.ofReal_add third_ε_pos.le third_ε_pos.le, ← two_mul]

Goal state after:
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
P : ProbabilityMeasure Ω
ε : ℝ
ε_pos : ε > 0
third_ε_pos : 0 < ε / 3
third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)
Es : ℕ → Set Ω
Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)
Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)
Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3
Es_cover : ⋃ n, Es n = univ
Es_disjoint : Pairwise fun n m ↦ Disjoint (Es n) (Es m)
N : ℕ
hN : ↑P (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)
Js_finite : {J | J ⊆ Iio N}.Finite
Gs : Set (Set Ω) := (fun J ↦ thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J | J ⊆ Iio N}
Gs_open :
  ∀ (J : Set ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening (ε / 3) (⋃ j ∈ J, Es j))
mem_nhds_P :
  ∀ (G : Set Ω),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G → {Q | ↑P G < ↑Q G + ENNReal.ofReal (ε / 3)} ∈ 𝓝 P
Q : ProbabilityMeasure Ω
δ : ℝ
B : Set Ω
δ_gt : 2 * (ε / 3) < δ
x✝ : MeasurableSet B
JB : Set ℕ := {i | (B ∩ Es i).Nonempty ∧ i ∈ Iio N}
hQ : ↑P (⋃ i ∈ JB, thickening (ε / 3) (Es i)) < ↑Q (⋃ i ∈ JB, thickening (ε / 3) (Es i)) + ENNReal.ofReal (ε / 3)
B_subset : B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ (⋃ j ∈ Iio N, Es j)ᶜ
subset_thickB : ⋃ i ∈ JB, thickening (ε / 3) (Es i) ⊆ thickening δ B
⊢ ↑Q (⋃ i ∈ JB, thickening (ε / 3) (Es i)) + ENNReal.ofReal (2 * (ε / 3)) ≤
    ↑(ofMeasure Q).toMeasure (thickening δ B) + ENNReal.ofReal δ
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
inst✝ : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C} ∈ f
g : E →C_c ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
⊢ ∫ (x : E), -‖g.toBoundedContinuousFunction‖ ∂↑μ ≤ ∫ (x : E), g x ∂↑μ

Tactic:
gcongr
        · simp
        · exact g.continuous.integrable_of_hasCompactSupport g.hasCompactSupport
        · intro x
          apply neg_le_of_abs_le
          exact g.toBoundedContinuousFunction.norm_coe_le_norm x

Goal state after:
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
inst✝ : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C} ∈ f
g : E →C_c ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
⊢ ∫ (x : E), ‖g.toBoundedContinuousFunction‖ ∂↑μ ≤ ↑C * ‖g.toBoundedContinuousFunction‖

Tactic:
simp only [integral_const, smul_eq_mul]
        gcongr
        exact hμ

Goal state after: