mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: case inr.inr
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁴ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
X : ι → Ω'' → E
inst✝ : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hXY : TendstoInMeasure μ'' (Y - X) l 0
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
hZ : AEMeasurable Z μ'
hX : ∀ (i : ι), AEMeasurable (X i) μ''
hE : Nonempty E
x₀ : E := hE.some
F : E → ℝ
M : ℝ
hF_bounded : ∀ (x y : E), dist (F x) (F y) ≤ M
L : NNReal
hF_lip : LipschitzWith L F
hF_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] F
hL : 0 < L
⊢ ∀ ε > 0, ∀ᶠ (x : ι) in l, |∫ (ω : E), F ω ∂Measure.map (Y x) μ'' - ∫ (ω : E), F ω ∂Measure.map Z μ'| < ε

Tactic:
suffices ∀ ε > 0, ∀ᶠ n in l, |∫ ω, F ω ∂(μ''.map (Y n)) - ∫ ω, F ω ∂(μ'.map Z)| < L * ε by
    intro ε hε
    convert! this (ε / L) (by positivity)
    field_simp

Goal state after:
case inr.inr
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁴ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
X : ι → Ω'' → E
inst✝ : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hXY : TendstoInMeasure μ'' (Y - X) l 0
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
hZ : AEMeasurable Z μ'
hX : ∀ (i : ι), AEMeasurable (X i) μ''
hE : Nonempty E
x₀ : E := hE.some
F : E → ℝ
M : ℝ
hF_bounded : ∀ (x y : E), dist (F x) (F y) ≤ M
L : NNReal
hF_lip : LipschitzWith L F
hF_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] F
hL : 0 < L
⊢ ∀ ε > 0, ∀ᶠ (n : ι) in l, |∫ (ω : E), F ω ∂Measure.map (Y n) μ'' - ∫ (ω : E), F ω ∂Measure.map Z μ'| < ↑L * ε
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf_indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
h :
  IndepFun (fun a ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (fun a ↦ (AEMeasurable.mk (f k) ⋯ a, AEMeasurable.mk (f l) ⋯ a)) κ μ
a : α
hk : ∀ᵐ (ω : Ω) ∂κ a, f k ω = AEMeasurable.mk (f k) ⋯ ω
hl : ∀ᵐ (ω : Ω) ∂κ a, f l ω = AEMeasurable.mk (f l) ⋯ ω
ω : Ω
hωk : f k ω = AEMeasurable.mk (f k) ⋯ ω
hωl : f l ω = AEMeasurable.mk (f l) ⋯ ω
⊢ (f k ω, AEMeasurable.mk (f l) ⋯ ω) = (f k ω, f l ω)

Tactic:
← hωl

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf_indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
h :
  IndepFun (fun a ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (fun a ↦ (AEMeasurable.mk (f k) ⋯ a, AEMeasurable.mk (f l) ⋯ a)) κ μ
a : α
hk : ∀ᵐ (ω : Ω) ∂κ a, f k ω = AEMeasurable.mk (f k) ⋯ ω
hl : ∀ᵐ (ω : Ω) ∂κ a, f l ω = AEMeasurable.mk (f l) ⋯ ω
ω : Ω
hωk : f k ω = AEMeasurable.mk (f k) ⋯ ω
hωl : f l ω = AEMeasurable.mk (f l) ⋯ ω
⊢ (f k ω, f l ω) = (f k ω, f l ω)
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
𝓕 : Filtration ι m
i : ι
hi : ∃ j > i, Set.Ioo i j = ∅
this✝ : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
⊢ ↑𝓕₊ i = ↑𝓕 i

Tactic:
obtain ⟨j, hij, hIoo⟩ := hi

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
𝓕 : Filtration ι m
i : ι
this✝ : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
j : ι
hij : j > i
hIoo : Set.Ioo i j = ∅
⊢ ↑𝓕₊ i = ↑𝓕 i
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: ι : Type u_1
E : Type u_2
Ω' : Type u_3
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁴ : IsProbabilityMeasure μ'
mE : MeasurableSpace E
Z : Ω' → E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
inst✝ : l.IsCountablyGenerated
X : ι → Ω' → E
h : TendstoInMeasure μ' X l Z
hX : ∀ (i : ι), AEMeasurable (X i) μ'
hZ : AEMeasurable Z μ'
⊢ TendstoInMeasure μ' (X - fun x ↦ Z) l 0

Tactic:
by simpa [tendstoInMeasure_iff_norm] using h

Goal state after:
Module: Mathlib.MeasureTheory.Function.Piecewise

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
s : ι → Set α
f : ι → α → β
inst✝¹ : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst✝ : TopologicalSpace β
hf : ∀ (i : ι), StronglyMeasurable (f i)
Fi : Infinite ι
e : ℕ ≃ ι
g : (n : ℕ) → ι → Fin (n + 1) := fun n i ↦ if hi : ∃ m < n, i = e m then ⟨hi.choose, ⋯⟩ else Fin.last n
sg : ∀ (n : ℕ), Function.Surjective (g n)
G : (n : ℕ) → IndexedPartition fun k ↦ ⋃ i ∈ g n ⁻¹' {k}, s i
⊢ StronglyMeasurable (hs.piecewise f)

Tactic:
refine ⟨fun n => (G n).simpleFunc_piecewise (fun i => ?_) (fun i => (hf (e i)).approx n),
    fun x => ?_⟩

Goal state after:
case neg.refine_1
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
s : ι → Set α
f : ι → α → β
inst✝¹ : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst✝ : TopologicalSpace β
hf : ∀ (i : ι), StronglyMeasurable (f i)
Fi : Infinite ι
e : ℕ ≃ ι
g : (n : ℕ) → ι → Fin (n + 1) := fun n i ↦ if hi : ∃ m < n, i = e m then ⟨hi.choose, ⋯⟩ else Fin.last n
sg : ∀ (n : ℕ), Function.Surjective (g n)
G : (n : ℕ) → IndexedPartition fun k ↦ ⋃ i ∈ g n ⁻¹' {k}, s i
n : ℕ
i : Fin (n + 1)
⊢ MeasurableSet (⋃ i_1 ∈ g n ⁻¹' {i}, s i_1)

case neg.refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
s : ι → Set α
f : ι → α → β
inst✝¹ : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst✝ : TopologicalSpace β
hf : ∀ (i : ι), StronglyMeasurable (f i)
Fi : Infinite ι
e : ℕ ≃ ι
g : (n : ℕ) → ι → Fin (n + 1) := fun n i ↦ if hi : ∃ m < n, i = e m then ⟨hi.choose, ⋯⟩ else Fin.last n
sg : ∀ (n : ℕ), Function.Surjective (g n)
G : (n : ℕ) → IndexedPartition fun k ↦ ⋃ i ∈ g n ⁻¹' {k}, s i
x : α
⊢ Tendsto (fun n ↦ ((fun n ↦ (G n).simpleFunc_piecewise ⋯ fun i ↦ ⋯.approx n) n) x) atTop (nhds (hs.piecewise f x))
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᵐ[μ] AEStronglyMeasurable.mk (f n) ⋯
f' : ℕ → α → β := fun n ↦ AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable f' p μ
hut' : UnifTight f' p μ
g' : α → β := AEStronglyMeasurable.mk g ⋯
hg : StronglyMeasurable g'
hgg' : g =ᵐ[μ] g'
hg'' : MemLp g' p μ
haefg' : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (g' x))
⊢ Tendsto (fun n ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)

Tactic:
have haefg (n : ℕ) : f n - g =ᵐ[μ] f' n - g' := (hff' n).sub hgg'

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᵐ[μ] AEStronglyMeasurable.mk (f n) ⋯
f' : ℕ → α → β := fun n ↦ AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable f' p μ
hut' : UnifTight f' p μ
g' : α → β := AEStronglyMeasurable.mk g ⋯
hg : StronglyMeasurable g'
hgg' : g =ᵐ[μ] g'
hg'' : MemLp g' p μ
haefg' : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (g' x))
haefg : ∀ (n : ℕ), f n - g =ᵐ[μ] f' n - g'
⊢ Tendsto (fun n ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
Λ₁ Λ₂ : (α →C_c ℝ) →ₚ[ℝ] ℝ
h : toNNRealLinear Λ₁ = toNNRealLinear Λ₂
⊢ Λ₁ = Λ₂

Tactic:
ext f

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
Λ₁ Λ₂ : (α →C_c ℝ) →ₚ[ℝ] ℝ
h : toNNRealLinear Λ₁ = toNNRealLinear Λ₂
f : α →C_c ℝ
⊢ Λ₁ f = Λ₂ f
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : TopologicalSpace α
Λ : (α →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
a : ℝ
f : α →C_c ℝ
ha : a ≤ 0
⊢ ↑(Λ (a • f).nnrealPart) - ↑(Λ (-(a • f)).nnrealPart) = (RingHom.id ℝ) a • (↑(Λ f.nnrealPart) - ↑(Λ (-f).nnrealPart))

Tactic:
simp only [RingHom.id_apply, smul_eq_mul, ← (smul_neg a f),
            nnrealPart_smul_neg f ha, nnrealPart_smul_neg (-f) ha, map_smul,
            NNReal.coe_mul, Real.coe_toNNReal', neg_neg, sup_of_le_left (neg_nonneg.mpr ha)]

Goal state after:
case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : TopologicalSpace α
Λ : (α →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
a : ℝ
f : α →C_c ℝ
ha : a ≤ 0
⊢ -a * ↑(Λ (-f).nnrealPart) - -a * ↑(Λ f.nnrealPart) = a * (↑(Λ f.nnrealPart) - ↑(Λ (-f).nnrealPart))
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
Λ : (α →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
⊢ toNNRealLinear (toRealPositiveLinear Λ) = Λ

Tactic:
ext f

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
Λ : (α →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f : α →C_c ℝ≥0
⊢ ↑((toNNRealLinear (toRealPositiveLinear Λ)) f) = ↑(Λ f)
Module: Mathlib.MeasureTheory.Integral.LebesgueNormedSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun x ↦ ↑(f x) • g x) =ᵐ[μ] g'
x : α
hx : ↑(f x) • g x = g' x
h'x : ↑(f x) ≠ 0
⊢ g x = (↑(f x))⁻¹ • g' x

Tactic:
rw [← hx, smul_smul, inv_mul_cancel₀, one_smul]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun x ↦ ↑(f x) • g x) =ᵐ[μ] g'
x : α
hx : ↑(f x) • g x = g' x
h'x : ↑(f x) ≠ 0
⊢ ↑(f x) ≠ 0
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
⊢ h / 2 * (∑ x ∈ Finset.range (N - 1 + 1), f (a + ↑x * h) + ∑ x ∈ Finset.range (N - 1 + 1), f (a + (↑x + 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:
sum_range_succ',

Goal state after:
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 + 1), f (a + (↑x + 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.Order.Interval.Set.Union

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

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

Goal state after:
Module: Mathlib.Order.Interval.Set.Union

Goal state before:

Tactic:
_ ⊆ Ico (a 0) (a N) ∪ Ico (a N) (a (N + 1)) := Ico_subset_Ico_union_Ico
    _ ⊆ _ := by simpa [Finset.range_add_one] using
                  union_subset_union_right (Ico (a N) (a (N + 1))) ih

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

Goal state before:
pp: case pos
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)))
x : ℝ
hx : x ∈ Set.Icc (ak k) (ak (k + 1))
⊢ |iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x| ≤ ζ

Tactic:
← h6 hx,

Goal state after:
case pos
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)))
x : ℝ
hx : x ∈ Set.Icc (ak k) (ak (k + 1))
⊢ |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
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
⊢ ENNReal.ofReal (∫ (a : X), ↑(f a) ∂rieszMeasure Λ) = ↑(Λ 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:
← ENNReal.ofNNReal_toNNReal

Goal state after:
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)

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: case h.refine_2
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ
ε : ℝ
hε : 0 < ε
E : Set X
μ : Content X
hμ : μ.outerMeasure E ≠ ∞
hμ' : MeasurableSet E
c : ℝ
hfE : ∀ x ∈ E, f x < c
hε' : ε.toNNReal ≠ 0
V₁ : Opens X
hV₁ : E ⊆ ↑V₁ ∧ μ.outerMeasure ↑V₁ ≤ μ.outerMeasure E + ↑ε.toNNReal
V₂ : Opens X := { carrier := ⇑f ⁻¹' Iio c, is_open' := ⋯ }
⊢ μ.measure ↑(V₁ ⊓ V₂) ≤ μ.measure E + ENNReal.ofReal ε

Tactic:
· calc
      _ ≤ μ.measure V₁ := by simp [measure_mono]
      _ = μ.outerMeasure V₁ := Content.measure_apply μ (V₁.2.measurableSet)
      _ ≤ μ.outerMeasure E + ε.toNNReal := hV₁.2
      _ = _ := by rw [Content.measure_apply μ hμ', ENNReal.ofNNReal_toNNReal]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_2
mE : MeasurableSpace E
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
X : Type u_3
mX : MeasurableSpace X
μ : Measure X
inst✝ : BorelSpace E
f : X → E
hf : AEMeasurable f μ
r : ℝ
t : E
⊢ charFun (Measure.map (fun x ↦ r • f x) μ) t = charFun (Measure.map f μ) (r • t)

Tactic:
rw [show (fun x ↦ r • (f x)) = (r • ·) ∘ f from rfl, ← AEMeasurable.map_map_of_aemeasurable,
    charFun_map_smul]

Goal state after:
case hg
E : Type u_2
mE : MeasurableSpace E
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
X : Type u_3
mX : MeasurableSpace X
μ : Measure X
inst✝ : BorelSpace E
f : X → E
hf : AEMeasurable f μ
r : ℝ
t : E
⊢ AEMeasurable (fun x ↦ r • x) (Measure.map f μ)

case hf
E : Type u_2
mE : MeasurableSpace E
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
X : Type u_3
mX : MeasurableSpace X
μ : Measure X
inst✝ : BorelSpace E
f : X → E
hf : AEMeasurable f μ
r : ℝ
t : E
⊢ AEMeasurable f μ
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:
conv => arg 2; equals (1 : Y → ↥I) ∘ f => rfl

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
⊢ EqOn (g ∘ f) (1 ∘ f) (f ⁻¹' K)
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: case a
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
x : X
⊢ comap stoneCechUnit (𝓝 (stoneCechUnit x)) ≤ 𝓝 x

Tactic:
simp_rw [le_nhds_iff, ((nhds_basis_opens _).comap _).mem_iff, and_assoc]

Goal state after:
case a
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
x : X
⊢ ∀ (s : Set X), x ∈ s → IsOpen[inst✝¹] s → ∃ i, stoneCechUnit x ∈ i ∧ IsOpen i ∧ stoneCechUnit ⁻¹' i ⊆ s
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
μ ν : Measure Ω
δ : ℝ≥0∞
h :
  ∀ (ε : ℝ≥0∞) (B : Set Ω),
    δ < ε → ε < ∞ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε ∧ ν B ≤ μ (thickening ε.toReal B) + ε
⊢ levyProkhorovEDist μ ν ≤ δ

Tactic:
by_cases δ_top : δ = ∞
  · simp only [δ_top, le_top]
  apply levyProkhorovEDist_le_of_forall_add_pos_le
  intro x B x_pos x_lt_top B_mble
  simpa only [← add_assoc] using h (δ + x) B (ENNReal.lt_add_right δ_top x_pos.ne.symm)
    (by simp only [add_lt_top, Ne.lt_top δ_top, x_lt_top, and_self]) B_mble

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
inst✝¹ : IsTopologicalGroup C
inst✝ : LocallyCompactSpace B
f : CompactlySupportedContinuousMap B E
this : UniformSpace B := IsTopologicalGroup.rightUniformSpace B
b : B
ε : ℝ
hε : ε > 0
U₀ : Set B
hU₀ : IsCompact U₀
hb : U₀ ∈ nhds b
K : Set B
hK : IsCompact K
hf₀ : ∀ x ∉ K, f x = 0
S : Set A := ⇑φ ⁻¹' (U₀⁻¹ * K)
hSc : IsCompact S
δ : ℝ
hδ0 : δ > 0
hδ : ENNReal.ofReal δ * μA S < ENNReal.ofReal ε
hS : ∀ {x : B}, x ∈ U₀ → ∀ {y : A}, y ∉ S → (H.pullback f x) y = 0
⊢ ∀ᶠ (x : B) in nhds b, dist (∫ (a : A), (H.pullback f x) a ∂μA) (∫ (a : A), (H.pullback f b) a ∂μA) < ε

Tactic:
have ha := f.hasCompactSupport.uniformContinuous_of_continuous f.continuous

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
b : B
ε : ℝ
hε : ε > 0
U₀ : Set B
hU₀ : IsCompact U₀
hb : U₀ ∈ nhds b
K : Set B
hK : IsCompact K
hf₀ : ∀ x ∉ K, f x = 0
S : Set A := ⇑φ ⁻¹' (U₀⁻¹ * K)
hSc : IsCompact S
δ : ℝ
hδ0 : δ > 0
hδ : ENNReal.ofReal δ * μA S < ENNReal.ofReal ε
hS : ∀ {x : B}, x ∈ U₀ → ∀ {y : A}, y ∉ S → (H.pullback f x) y = 0
ha : UniformContinuous ⇑f
⊢ ∀ᶠ (x : B) in nhds b, dist (∫ (a : A), (H.pullback f x) a ∂μA) (∫ (a : A), (H.pullback f b) a ∂μA) < ε
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
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:
intro x
          apply le_of_abs_le
          exact g.toBoundedContinuousFunction.norm_coe_le_norm x

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

Goal state before:
pp: case refine_2
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 x ∂↑μ ≤ ↑C * ‖g.toBoundedContinuousFunction‖

Tactic:
calc ∫ x, g x ∂μ
      _ ≤ ∫ (x : E), ‖g.toBoundedContinuousFunction‖ ∂μ := by
        gcongr
        · exact g.continuous.integrable_of_hasCompactSupport g.hasCompactSupport
        · simp
        · intro x
          apply le_of_abs_le
          exact g.toBoundedContinuousFunction.norm_coe_le_norm x
      _ ≤ C * ‖g.toBoundedContinuousFunction‖ := by
        simp only [integral_const, smul_eq_mul]
        gcongr
        exact hμ

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: case e'_3
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
⊢ √π = 2 * (1 / 2 * Gamma (1 / 2))

Tactic:
Gamma_one_half_eq,

Goal state after:
case e'_3
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
⊢ √π = 2 * (1 / 2 * √π)