mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case succ.succ.inl
b : ℕ
⊢ ⌊logb ↑(b + 1 + 1) ↑0⌋₊ = Nat.log (b + 1 + 1) 0

pp: case succ.succ.inr
n b : ℕ
hn : n ≠ 0
⊢ ⌊logb ↑(b + 1 + 1) ↑n⌋₊ = Nat.log (b + 1 + 1) n

Tactic:
·

Goal state after:
case succ.succ.inl
b : ℕ
⊢ ⌊logb ↑(b + 1 + 1) ↑0⌋₊ = Nat.log (b + 1 + 1) 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case succ.succ.inr
n b : ℕ
hn : n ≠ 0
⊢ ⌊logb ↑(b + 1 + 1) ↑n⌋₊ = Nat.log (b + 1 + 1) n

Tactic:
← Nat.cast_inj (R := ℤ),

Goal state after:
case succ.succ.inr
n b : ℕ
hn : n ≠ 0
⊢ ↑⌊logb ↑(b + 1 + 1) ↑n⌋₊ = ↑(Nat.log (b + 1 + 1) n)
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: n b : ℕ
hn : n ≠ 0
⊢ 1 ≤ n

Tactic:
by lia

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case zero
n : ℕ
⊢ ⌈logb ↑0 ↑n⌉₊ = Nat.clog 0 n

pp: case succ.zero
n : ℕ
⊢ ⌈logb ↑(0 + 1) ↑n⌉₊ = Nat.clog (0 + 1) n

pp: case succ.succ
n b : ℕ
⊢ ⌈logb ↑(b + 1 + 1) ↑n⌉₊ = Nat.clog (b + 1 + 1) n

Tactic:
·

Goal state after:
case zero
n : ℕ
⊢ ⌈logb ↑0 ↑n⌉₊ = Nat.clog 0 n
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case succ.zero
n : ℕ
⊢ ⌈logb ↑(0 + 1) ↑n⌉₊ = Nat.clog (0 + 1) n

pp: case succ.succ
n b : ℕ
⊢ ⌈logb ↑(b + 1 + 1) ↑n⌉₊ = Nat.clog (b + 1 + 1) n

Tactic:
·

Goal state after:
case succ.zero
n : ℕ
⊢ ⌈logb ↑(0 + 1) ↑n⌉₊ = Nat.clog (0 + 1) n
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case succ.succ.inl
b : ℕ
⊢ ⌈logb ↑(b + 1 + 1) ↑0⌉₊ = Nat.clog (b + 1 + 1) 0

pp: case succ.succ.inr
n b : ℕ
hn : n ≠ 0
⊢ ⌈logb ↑(b + 1 + 1) ↑n⌉₊ = Nat.clog (b + 1 + 1) n

Tactic:
·

Goal state after:
case succ.succ.inl
b : ℕ
⊢ ⌈logb ↑(b + 1 + 1) ↑0⌉₊ = Nat.clog (b + 1 + 1) 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case succ.succ.inr
n b : ℕ
hn : n ≠ 0
⊢ ⌈logb ↑(b + 1 + 1) ↑n⌉₊ = Nat.clog (b + 1 + 1) n

Tactic:
← Nat.cast_inj (R := ℤ),

Goal state after:
case succ.succ.inr
n b : ℕ
hn : n ≠ 0
⊢ ↑⌈logb ↑(b + 1 + 1) ↑n⌉₊ = ↑(Nat.clog (b + 1 + 1) n)
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case inr
b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
this : ∀ {b : ℝ}, b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1 → 0 < b → Tendsto (fun x ↦ |logb b x|) atTop atTop
hb₀ : ¬0 < b
⊢ Tendsto (fun x ↦ |logb b x|) atTop atTop

pp: b✝ b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
⊢ Tendsto (fun x ↦ |logb b x|) atTop atTop

Tactic:
·

Goal state after:
case inr
b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
this : ∀ {b : ℝ}, b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1 → 0 < b → Tendsto (fun x ↦ |logb b x|) atTop atTop
hb₀ : ¬0 < b
⊢ Tendsto (fun x ↦ |logb b x|) atTop atTop
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case inr
b✝ b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
this : ∀ {b : ℝ}, b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1 → 0 < b → 1 < b → Tendsto (fun x ↦ |logb b x|) atTop atTop
hb₁ : ¬1 < b
⊢ Tendsto (fun x ↦ |logb b x|) atTop atTop

pp: b✝ b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
hb₁ : 1 < b
⊢ Tendsto (fun x ↦ |logb b x|) atTop atTop

Tactic:
·

Goal state after:
case inr
b✝ b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
this : ∀ {b : ℝ}, b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1 → 0 < b → 1 < b → Tendsto (fun x ↦ |logb b x|) atTop atTop
hb₁ : ¬1 < b
⊢ Tendsto (fun x ↦ |logb b x|) atTop atTop
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
⊢ (∫⁻ (x : X), ↑(f x) ∂μ).toReal = (∫⁻ (a : X), ENNReal.ofReal ↑(f a) ∂μ).toReal

pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
⊢ 0 ≤ᵐ[μ] fun x ↦ ↑(f x)

Tactic:
·

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
⊢ (∫⁻ (x : X), ↑(f x) ∂μ).toReal = (∫⁻ (a : X), ENNReal.ofReal ↑(f a) ∂μ).toReal
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
⊢ 0 ≤ᵐ[μ] fun x ↦ ↑(f x)

Tactic:
·

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
⊢ 0 ≤ᵐ[μ] fun x ↦ ↑(f x)
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b : ℝ
n : ℕ
⊢ Tendsto (fun x ↦ logb b x ^ n / id x) atTop (𝓝 0)

pp: b : ℝ
n : ℕ
⊢ ∀ᶠ (x : ℝ) in atTop, id x = 0 → logb b x ^ n = 0

Tactic:
·

Goal state after:
b : ℝ
n : ℕ
⊢ Tendsto (fun x ↦ logb b x ^ n / id x) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b : ℝ
n : ℕ
⊢ ∀ᶠ (x : ℝ) in atTop, id x = 0 → logb b x ^ n = 0

Tactic:
·

Goal state after:
b : ℝ
n : ℕ
⊢ ∀ᶠ (x : ℝ) in atTop, id x = 0 → logb b x ^ n = 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case pos
b : ℝ
h : b = -1 ∨ b = 0 ∨ b = 1
⊢ logb b =O[⊤] log

pp: case neg
b : ℝ
h : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
⊢ logb b =O[⊤] log

Tactic:
·

Goal state after:
case pos
b : ℝ
h : b = -1 ∨ b = 0 ∨ b = 1
⊢ logb b =O[⊤] log
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case neg
b : ℝ
h : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
⊢ logb b =O[⊤] log

Tactic:
·

Goal state after:
case neg
b : ℝ
h : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
⊢ logb b =O[⊤] log
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case inl
⊢ (fun x ↦ log (0 * x)) =O[atTop] log

pp: case inr
c : ℝ
hc : c ≠ 0
⊢ (fun x ↦ log (c * x)) =O[atTop] log

Tactic:
·

Goal state after:
case inl
⊢ (fun x ↦ log (0 * x)) =O[atTop] log
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case inr
c : ℝ
hc : c ≠ 0
⊢ (fun x ↦ log (c * x)) =O[atTop] log

Tactic:
·

Goal state after:
case inr
c : ℝ
hc : c ≠ 0
⊢ (fun x ↦ log (c * x)) =O[atTop] log
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case mp
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
⊢ ∃ K ⊆ A, IsCompact K ∧ r < μ K

pp: case mpr
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT IsCompact IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
⊢ ∃ K ⊆ A, (IsCompact ∘ closure) K ∧ r < μ K

Tactic:
·

Goal state after:
case mp
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
⊢ ∃ K ⊆ A, IsCompact K ∧ r < μ K
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case mpr
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT IsCompact IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
⊢ ∃ K ⊆ A, (IsCompact ∘ closure) K ∧ r < μ K

Tactic:
·

Goal state after:
case mpr
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT IsCompact IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
⊢ ∃ K ⊆ A, (IsCompact ∘ closure) K ∧ r < μ K
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case mpr.refine_1
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT IsCompact IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
K : Set α
hK1 : K ⊆ A
hK2 : IsCompact K
hK3 : r < μ K
⊢ (IsCompact ∘ closure) (closure K)

pp: case mpr.refine_2
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT IsCompact IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
K : Set α
hK1 : K ⊆ A
hK2 : IsCompact K
hK3 : r < μ K
⊢ r < μ (closure K)

Tactic:
·

Goal state after:
case mpr.refine_1
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT IsCompact IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
K : Set α
hK1 : K ⊆ A
hK2 : IsCompact K
hK3 : r < μ K
⊢ (IsCompact ∘ closure) (closure K)
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case mpr.refine_2
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT IsCompact IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
K : Set α
hK1 : K ⊆ A
hK2 : IsCompact K
hK3 : r < μ K
⊢ r < μ (closure K)

Tactic:
·

Goal state after:
case mpr.refine_2
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT IsCompact IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
K : Set α
hK1 : K ⊆ A
hK2 : IsCompact K
hK3 : r < μ K
⊢ r < μ (closure K)
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: case inl
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
f : X →ᵇ ℝ
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) ⊥ ≤ ∫ (x : X), f x ∂μ
⊢ Tendsto (fun i ↦ ∫ (x : X), f x ∂μs i) ⊥ (𝓝 (∫ (x : X), f x ∂μ))

pp: case inr
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
f : X →ᵇ ℝ
hL : L.NeBot
⊢ Tendsto (fun i ↦ ∫ (x : X), f x ∂μs i) L (𝓝 (∫ (x : X), f x ∂μ))

Tactic:
·

Goal state after:
case inl
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
f : X →ᵇ ℝ
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) ⊥ ≤ ∫ (x : X), f x ∂μ
⊢ Tendsto (fun i ↦ ∫ (x : X), f x ∂μs i) ⊥ (𝓝 (∫ (x : X), f x ∂μ))
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case mp
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
⊢ ∃ K ⊆ A, (IsCompact ∘ closure) K ∧ r < μ K

pp: case mpr
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
⊢ ∃ K ⊆ A, (fun s ↦ IsCompact s ∧ IsClosed s) K ∧ r < μ K

Tactic:
·

Goal state after:
case mp
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
⊢ ∃ K ⊆ A, (IsCompact ∘ closure) K ∧ r < μ K
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case mpr
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
⊢ ∃ K ⊆ A, (fun s ↦ IsCompact s ∧ IsClosed s) K ∧ r < μ K

Tactic:
·

Goal state after:
case mpr
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
⊢ ∃ K ⊆ A, (fun s ↦ IsCompact s ∧ IsClosed s) K ∧ r < μ K
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case mpr.refine_1
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
K : Set α
hK1 : K ⊆ A
hK2 : (IsCompact ∘ closure) K
hK3 : r < μ K
⊢ (fun s ↦ IsCompact s ∧ IsClosed s) (closure K)

pp: case mpr.refine_2
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
K : Set α
hK1 : K ⊆ A
hK2 : (IsCompact ∘ closure) K
hK3 : r < μ K
⊢ r < μ (closure K)

Tactic:
·

Goal state after:
case mpr.refine_1
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
K : Set α
hK1 : K ⊆ A
hK2 : (IsCompact ∘ closure) K
hK3 : r < μ K
⊢ (fun s ↦ IsCompact s ∧ IsClosed s) (closure K)
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case mpr.refine_2
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
K : Set α
hK1 : K ⊆ A
hK2 : (IsCompact ∘ closure) K
hK3 : r < μ K
⊢ r < μ (closure K)

Tactic:
·

Goal state after:
case mpr.refine_2
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
K : Set α
hK1 : K ⊆ A
hK2 : (IsCompact ∘ closure) K
hK3 : r < μ K
⊢ r < μ (closure K)
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
hpq : ∀ (A B : Set α), p A → q B → p (A ∩ B)
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, p K ∧ μ Kᶜ < ε
A : Set α
hA : q A
r : ℝ≥0∞
hr : r < μ A
K' : Set α
hpK' : p K'
hK'_lt : μ K'ᶜ < μ A - r
⊢ μ (A \ (K' ∩ A)) < μ A - r

Tactic:
·

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
hpq : ∀ (A B : Set α), p A → q B → p (A ∩ B)
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, p K ∧ μ Kᶜ < ε
A : Set α
hA : q A
r : ℝ≥0∞
hr : r < μ A
K' : Set α
hpK' : p K'
hK'_lt : μ K'ᶜ < μ A - r
⊢ μ (A \ (K' ∩ A)) < μ A - r
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) L fun i ↦ ∫ (x : X), f x ∂μs i
⊢ ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L

pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) L fun i ↦ ∫ (x : X), f x ∂μs i
⊢ limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ

Tactic:
·

Goal state after:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) L fun i ↦ ∫ (x : X), f x ∂μs i
⊢ ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case refine_1
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε✝ : ℝ≥0∞
hε✝ : 0 < ε✝
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h✝ : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
a✝ : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun n m ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), ⋃ m, f n m = univ
n : ℕ
ε : ℝ≥0∞
hε : 0 < ε
m : ℕ
⊢ NullMeasurableSet (f n m)ᶜ P

pp: case refine_2
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε✝ : ℝ≥0∞
hε✝ : 0 < ε✝
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h✝ : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
a✝ : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun n m ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), ⋃ m, f n m = univ
n : ℕ
ε : ℝ≥0∞
hε : 0 < ε
⊢ ⋂ n_1, (f n n_1)ᶜ = ∅

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε✝ : ℝ≥0∞
hε✝ : 0 < ε✝
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h✝ : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
a✝ : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun n m ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), ⋃ m, f n m = univ
n : ℕ
ε : ℝ≥0∞
hε : 0 < ε
m : ℕ
⊢ NullMeasurableSet (f n m)ᶜ P
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case refine_2
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε✝ : ℝ≥0∞
hε✝ : 0 < ε✝
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h✝ : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
a✝ : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun n m ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), ⋃ m, f n m = univ
n : ℕ
ε : ℝ≥0∞
hε : 0 < ε
⊢ ⋂ n_1, (f n n_1)ᶜ = ∅

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε✝ : ℝ≥0∞
hε✝ : 0 < ε✝
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h✝ : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
a✝ : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun n m ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), ⋃ m, f n m = univ
n : ℕ
ε : ℝ≥0∞
hε : 0 < ε
⊢ ⋂ n_1, (f n n_1)ᶜ = ∅
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) L fun i ↦ ∫ (x : X), f x ∂μs i
⊢ limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ

Tactic:
·

Goal state after:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) L fun i ↦ ∫ (x : X), f x ∂μs i
⊢ limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case refine_1
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ P.InnerRegularWRT IsCompact IsOpen

pp: case refine_2
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ ∀ ⦃s U : Set α⦄, IsCompact s → IsOpen U → IsCompact (s \ U)

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ P.InnerRegularWRT IsCompact IsOpen
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case refine_2
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ ∀ ⦃s U : Set α⦄, IsCompact s → IsOpen U → IsCompact (s \ U)

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ ∀ ⦃s U : Set α⦄, IsCompact s → IsOpen U → IsCompact (s \ U)