mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: a : ℝ
x✝ : Set ℝ
hav : a ∈ x✝
hv : IsOpen x✝
w✝¹ w✝ : ℝ
hl : w✝¹ < a
hu : a < w✝
h : Ioo w✝¹ w✝ ⊆ x✝
q : ℚ
hlq : w✝¹ < ↑q
hqa : ↑q < a
p : ℚ
hap : a < ↑p
hpu : ↑p < w✝
⊢ ∃ i i_1, ∃ (_ : i < i_1), Ioo ↑q ↑p ∈ {Ioo ↑i ↑i_1}

Tactic:
exact ⟨q, p, Rat.cast_lt.1 <| hqa.trans hap, rfl⟩

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Set α
hs : MeasurableSet s
b : α
hb : ¬f b = 0
⊢ f b * μ (⇑f ⁻¹' {f b} ∩ s) = f b * μ (⇑f ⁻¹' {f b} ∩ s)

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: x ε : ℝ
⊢ TotallyBounded (Ioo (x - ε) (x + ε))

Tactic:
]

Goal state after:
x ε : ℝ
⊢ TotallyBounded (Ioo (x - ε) (x + ε))
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: K : Subfield ℝ
hc : IsClosed ↑K
⊢ closure ↑K = univ

Tactic:
]

Goal state after:
K : Subfield ℝ
hc : IsClosed ↑K
⊢ closure ↑K = univ
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: case refine_1
s : Set ℝ
conn : s.OrdConnected
nt : s.Nontrivial
x : ℝ
hx : x ∈ s
ε : ℝ
ε_pos : ε > 0
z : ℝ
hz : z ∈ s
ne : z ≠ x
lt : z < x
q : ℚ
h₁ : z < ↑q ∧ x - ε < ↑q
h₂ : ↑q < x
⊢ ∃ y ∈ s ∩ range Rat.cast, |y - x| < ε

Tactic:
]

Goal state after:
case refine_1
s : Set ℝ
conn : s.OrdConnected
nt : s.Nontrivial
x : ℝ
hx : x ∈ s
ε : ℝ
ε_pos : ε > 0
z : ℝ
hz : z ∈ s
ne : z ≠ x
lt : z < x
q : ℚ
h₁ : z < ↑q ∧ x - ε < ↑q
h₂ : ↑q < x
⊢ ∃ y ∈ s ∩ range Rat.cast, |y - x| < ε
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ∑ r ∈ f.range, r * μ (⇑f ⁻¹' {r} ∩ s) = ∑ y ∈ f.range, y * μ (⇑f ⁻¹' {y} ∩ s)

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: case refine_2
s : Set ℝ
conn : s.OrdConnected
nt : s.Nontrivial
x : ℝ
hx : x ∈ s
ε : ℝ
ε_pos : ε > 0
z : ℝ
hz : z ∈ s
ne : z ≠ x
lt : x < z
q : ℚ
h₁ : x < ↑q
h₂ : ↑q < z ∧ ↑q < x + ε
⊢ ∃ y ∈ s ∩ range Rat.cast, |y - x| < ε

Tactic:
]

Goal state after:
case refine_2
s : Set ℝ
conn : s.OrdConnected
nt : s.Nontrivial
x : ℝ
hx : x ∈ s
ε : ℝ
ε_pos : ε > 0
z : ℝ
hz : z ∈ s
ne : z ≠ x
lt : x < z
q : ℚ
h₁ : x < ↑q
h₂ : ↑q < z ∧ ↑q < x + ε
⊢ ∃ y ∈ s ∩ range Rat.cast, |y - x| < ε
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
f : ℝ → α
c : ℝ
hp : Periodic f c
hc : c ≠ 0
hf : Continuous[_, inst✝] f
⊢ IsCompact (f '' [[0, 0 + c]])

Tactic:
]

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
f : ℝ → α
c : ℝ
hp : Periodic f c
hc : c ≠ 0
hf : Continuous[_, inst✝] f
⊢ IsCompact (f '' [[0, 0 + c]])
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: f : ℕ → ℝ
k : ℕ
h_mon : MonotoneOn f (Ici k)
h_bdd : BddAbove (range fun x ↦ f (x + k))
⊢ Tendsto f atTop (𝓝 (sSup (f '' Ici k)))

Tactic:
]

Goal state after:
f : ℕ → ℝ
k : ℕ
h_mon : MonotoneOn f (Ici k)
h_bdd : BddAbove (range fun x ↦ f (x + k))
⊢ Tendsto f atTop (𝓝 (sSup (f '' Ici k)))
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: f : ℕ → ℝ
k : ℕ
h_mon : MonotoneOn f {x | k ≤ x}
h_bdd : BddAbove (range fun x ↦ f (x + k))
⊢ Tendsto f atTop (𝓝 (sSup (f '' Ici k)))

Tactic:
← monotone_add_nat_iff_monotoneOn_nat_Ici

Goal state after:
f : ℕ → ℝ
k : ℕ
h_mon : Monotone fun n ↦ f (n + k)
h_bdd : BddAbove (range fun x ↦ f (x + k))
⊢ Tendsto f atTop (𝓝 (sSup (f '' Ici k)))
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: f : ℕ → ℝ
k : ℕ
h_mon : Monotone fun n ↦ f (n + k)
h_bdd : BddAbove (range fun x ↦ f (x + k))
⊢ Tendsto f atTop (𝓝 (sSup (f '' Ici k)))

Tactic:
]

Goal state after:
f : ℕ → ℝ
k : ℕ
h_mon : Monotone fun n ↦ f (n + k)
h_bdd : BddAbove (range fun x ↦ f (x + k))
⊢ Tendsto f atTop (𝓝 (sSup (f '' Ici k)))
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: f : ℕ → ℝ
k : ℕ
h_mon : Monotone fun n ↦ f (n + k)
h_bdd : BddAbove (range fun x ↦ f (x + k))
⊢ Tendsto (fun n ↦ f (n + k)) atTop (𝓝 (⨆ x, f (x + k)))

Tactic:
]

Goal state after:
f : ℕ → ℝ
k : ℕ
h_mon : Monotone fun n ↦ f (n + k)
h_bdd : BddAbove (range fun x ↦ f (x + k))
⊢ Tendsto (fun n ↦ f (n + k)) atTop (𝓝 (⨆ x, f (x + k)))
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
⊢ ∑ x ∈ (const α c).range, x * μ (⇑(const α c) ⁻¹' {x}) = c * μ univ

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
⊢ ∑ x ∈ (const α c).range, x * μ (⇑(const α c) ⁻¹' {x}) = c * μ univ
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: f : ℕ → ℝ
k : ℕ
h_ant : AntitoneOn f (Ici k)
h_bdd : BddBelow (range fun x ↦ f (x + k))
⊢ Tendsto f atTop (𝓝 (sInf (f '' Ici k)))

Tactic:
]

Goal state after:
f : ℕ → ℝ
k : ℕ
h_ant : AntitoneOn f (Ici k)
h_bdd : BddBelow (range fun x ↦ f (x + k))
⊢ Tendsto f atTop (𝓝 (sInf (f '' Ici k)))
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: f : ℕ → ℝ
k : ℕ
h_ant : Antitone fun n ↦ f (n + k)
h_bdd : BddBelow (range fun x ↦ f (x + k))
⊢ Tendsto f atTop (𝓝 (sInf (f '' Ici k)))

Tactic:
]

Goal state after:
f : ℕ → ℝ
k : ℕ
h_ant : Antitone fun n ↦ f (n + k)
h_bdd : BddBelow (range fun x ↦ f (x + k))
⊢ Tendsto f atTop (𝓝 (sInf (f '' Ici k)))
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: f : ℕ → ℝ
k : ℕ
h_ant : Antitone fun n ↦ f (n + k)
h_bdd : BddBelow (range fun x ↦ f (x + k))
⊢ Tendsto (fun n ↦ f (n + k)) atTop (𝓝 (⨅ x, f (x + k)))

Tactic:
]

Goal state after:
f : ℕ → ℝ
k : ℕ
h_ant : Antitone fun n ↦ f (n + k)
h_bdd : BddBelow (range fun x ↦ f (x + k))
⊢ Tendsto (fun n ↦ f (n + k)) atTop (𝓝 (⨅ x, f (x + k)))
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: ι : Type u_1
inst✝² : Preorder ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x1 x2 ↦ x1 ≤ x2
f : ι → ℝ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_mon : Monotone f
h_bdd : BddAbove (range f)
⊢ IsLUB (range f) (⨆ i, f i)

Tactic:
]

Goal state after:
ι : Type u_1
inst✝² : Preorder ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x1 x2 ↦ x1 ≤ x2
f : ι → ℝ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_mon : Monotone f
h_bdd : BddAbove (range f)
⊢ IsLUB (range f) (⨆ i, f i)
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: ι : Type u_1
inst✝² : Preorder ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x1 x2 ↦ x1 ≤ x2
f : ι → ℝ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_ant : Antitone f
h_bdd : BddBelow (range f)
⊢ IsGLB (range f) (⨅ i, f i)

Tactic:
]

Goal state after:
ι : Type u_1
inst✝² : Preorder ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x1 x2 ↦ x1 ≤ x2
f : ι → ℝ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_ant : Antitone f
h_bdd : BddBelow (range f)
⊢ IsGLB (range f) (⨅ i, f i)
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
h✝ : Nonempty α
⊢ c * μ univ = c * μ univ

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: f : ℕ → ℝ
k : ℕ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_mon : MonotoneOn f (Ici k)
h_bdd : BddAbove (f '' Ici k)
⊢ IsLUB (f '' Ici k) (sSup (f '' Ici k))

Tactic:
]

Goal state after:
f : ℕ → ℝ
k : ℕ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_mon : MonotoneOn f (Ici k)
h_bdd : BddAbove (f '' Ici k)
⊢ IsLUB (f '' Ici k) (sSup (f '' Ici k))
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: f : ℕ → ℝ
k : ℕ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_ant : AntitoneOn f (Ici k)
h_bdd : BddBelow (f '' Ici k)
⊢ IsGLB (f '' Ici k) (sInf (f '' Ici k))

Tactic:
]

Goal state after:
f : ℕ → ℝ
k : ℕ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_ant : AntitoneOn f (Ici k)
h_bdd : BddBelow (f '' Ici k)
⊢ IsGLB (f '' Ici k) (sInf (f '' Ici k))
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
⊢ c * μ s = c * μ s

Tactic:
]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ c * μ s = c * μ s

Tactic:
]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f✝ g✝ : α →ₛ ℝ≥0∞
h : f✝ ≤ g✝
f g : α →ₛ ℝ≥0∞
⊢ f.lintegral μ = f.lintegral μ

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Zero β
inst✝ : MeasurableSpace α
f : α →ₛ β
⊢ MeasurableSet (⋃ y ∈ {y ∈ f.range | y ≠ 0}, ⇑f ⁻¹' {y})

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Zero β
inst✝ : MeasurableSpace α
f : α →ₛ β
⊢ MeasurableSet (⋃ y ∈ {y ∈ f.range | y ≠ 0}, ⇑f ⁻¹' {y})
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : Zero β
μ : Measure α
f : α →ₛ β
hf : ∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ∞
⊢ μ (⋃ y ∈ {y ∈ f.range | y ≠ 0}, ⇑f ⁻¹' {y}) < ∞

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : Zero β
μ : Measure α
f : α →ₛ β
hf : ∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ∞
⊢ μ (⋃ y ∈ {y ∈ f.range | y ≠ 0}, ⇑f ⁻¹' {y}) < ∞
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : Zero β
μ : Measure α
f : α →ₛ β
hf : ∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ∞
y : β
hy : y ∈ f.range ∧ y ≠ 0
⊢ μ (⇑f ⁻¹' {y}) < ∞

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : Zero β
μ : Measure α
f : α →ₛ β
hf : ∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ∞
y : β
hy : y ∈ f.range ∧ y ≠ 0
⊢ μ (⇑f ⁻¹' {y}) < ∞
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : Zero β
μ : Measure α
f : α →ₛ β
H : ∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ∞
⊢ μ (⋃ y ∈ {y ∈ f.range | y ≠ 0}, ⇑f ⁻¹' {y}) < ∞

Tactic:
]

Goal state after:
case mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : Zero β
μ : Measure α
f : α →ₛ β
H : ∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ∞
⊢ μ (⋃ y ∈ {y ∈ f.range | y ≠ 0}, ⇑f ⁻¹' {y}) < ∞
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝ : AddZeroClass β
f g : α →ₛ β
hf : f.FinMeasSupp μ
hg : g.FinMeasSupp μ
⊢ (map (fun p ↦ p.1 + p.2) (f.pair g)).FinMeasSupp μ

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝ : AddZeroClass β
f g : α →ₛ β
hf : f.FinMeasSupp μ
hg : g.FinMeasSupp μ
⊢ (map (fun p ↦ p.1 + p.2) (f.pair g)).FinMeasSupp μ
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝ : MulZeroClass β
f g : α →ₛ β
hf : f.FinMeasSupp μ
hg : g.FinMeasSupp μ
⊢ (map (fun p ↦ p.1 * p.2) (f.pair g)).FinMeasSupp μ

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝ : MulZeroClass β
f g : α →ₛ β
hf : f.FinMeasSupp μ
hg : g.FinMeasSupp μ
⊢ (map (fun p ↦ p.1 * p.2) (f.pair g)).FinMeasSupp μ
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this✝ : Countable (Subtype p)
hp : Nonempty (Subtype p)
H : ¬∃ j, s ↑j = ∅
this : ∀ (i : ι'), Countable ↑(s i)
m : Subtype p → Set δ := fun j ↦ {x | BddBelow (range fun i ↦ f (↑i) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
⊢ MeasurableSet (⋂ i, {x | x ∉ m i})

Tactic:
]

Goal state after:
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this✝ : Countable (Subtype p)
hp : Nonempty (Subtype p)
H : ¬∃ j, s ↑j = ∅
this : ∀ (i : ι'), Countable ↑(s i)
m : Subtype p → Set δ := fun j ↦ {x | BddBelow (range fun i ↦ f (↑i) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
⊢ MeasurableSet (⋂ i, {x | x ∉ m i})
Module: Mathlib.Topology.IndicatorConstPointwise

Goal state before:
pp: α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : {b}ᶜ ∈ 𝓝 0
⊢ (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), Tendsto (fun x ↦ i ∈ As x) L (pure (i ∈ A))

Tactic:
]

Goal state after:
α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : {b}ᶜ ∈ 𝓝 0
⊢ (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), Tendsto (fun x ↦ i ∈ As x) L (pure (i ∈ A))
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
b : ℝ≥0∞
h : ∑ x ∈ insert b (f.range \ {0}), x * μ (⇑f ⁻¹' {x}) ≠ ∞
hb : b ≠ 0
⊢ μ (⇑f ⁻¹' {b}) < ∞

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
b : ℝ≥0∞
h : ∑ x ∈ insert b (f.range \ {0}), x * μ (⇑f ⁻¹' {x}) ≠ ∞
hb : b ≠ 0
⊢ μ (⇑f ⁻¹' {b}) < ∞
Module: Mathlib.Topology.IndicatorConstPointwise

Goal state before:
pp: α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
⊢ (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), Tendsto (fun x ↦ i ∈ As x) L (pure (i ∈ A))

Tactic:
]

Goal state after:
α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
⊢ (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), Tendsto (fun x ↦ i ∈ As x) L (pure (i ∈ A))
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hf : f.lintegral μ ≠ ∞
⊢ f.FinMeasSupp μ

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hf : f.lintegral μ ≠ ∞
⊢ f.FinMeasSupp μ
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: ⊢ generateFrom (range Iio) = generateFrom (⋃ a, {Iio ↑a})

Tactic:
]

Goal state after:
⊢ generateFrom (range Iio) = generateFrom (⋃ a, {Iio ↑a})
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: a : ℝ
this : IsLUB (range Rat.cast ∩ Iio a) a
⊢ MeasurableSet (⋃ y ∈ Rat.cast ⁻¹' Iio a, Iio ↑y)

Tactic:
]

Goal state after:
a : ℝ
this : IsLUB (range Rat.cast ∩ Iio a) a
⊢ MeasurableSet (⋃ y ∈ Rat.cast ⁻¹' Iio a, Iio ↑y)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : ∀ (x : α), Tendsto (fun i ↦ f i x) u (𝓝 (g x))
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
s : Set β
h1s : IsClosed[inst✝⁵] s
h2s : s.Nonempty
h3s : s ≠ Set.univ
⊢ ∀ (x : α), Tendsto (fun i ↦ infNndist (f i x) s) u (𝓝 (infNndist (g x) s))

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : ∀ (x : α), Tendsto (fun i ↦ f i x) u (𝓝 (g x))
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
s : Set β
h1s : IsClosed[inst✝⁵] s
h2s : s.Nonempty
h3s : s ≠ Set.univ
⊢ ∀ (x : α), Tendsto (fun i ↦ infNndist (f i x) s) u (𝓝 (infNndist (g x) s))
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: ⊢ generateFrom (range Ioi) = generateFrom (⋃ a, {Ioi ↑a})

Tactic:
]

Goal state after:
⊢ generateFrom (range Ioi) = generateFrom (⋃ a, {Ioi ↑a})
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: a : ℝ
this : IsGLB (range Rat.cast ∩ Ioi a) a
⊢ MeasurableSet (⋃ y ∈ Rat.cast ⁻¹' Ioi a, Ioi ↑y)

Tactic:
]

Goal state after:
a : ℝ
this : IsGLB (range Rat.cast ∩ Ioi a) a
⊢ MeasurableSet (⋃ y ∈ Rat.cast ⁻¹' Ioi a, Ioi ↑y)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: ⊢ generateFrom (range fun a ↦ Ioi ↑a) = generateFrom (range fun a ↦ Iic ↑a)

Tactic:
]

Goal state after:
⊢ generateFrom (range fun a ↦ Ioi ↑a) = generateFrom (range fun a ↦ Iic ↑a)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case refine_1
q : ℚ
⊢ MeasurableSet (Iic ↑q)ᶜ

Tactic:
]

Goal state after:
case refine_1
q : ℚ
⊢ MeasurableSet (Iic ↑q)ᶜ
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case refine_2
q : ℚ
⊢ MeasurableSet (Ioi ↑q)ᶜ

Tactic:
]

Goal state after:
case refine_2
q : ℚ
⊢ MeasurableSet (Ioi ↑q)ᶜ
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ⇑f) (support ⇑g) → motive f → motive g → motive (f + g)
f : α →ₛ γ
s : Finset γ
h : range ⇑f \ {0} = ↑s
⊢ motive f

Tactic:
]

Goal state after:
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ⇑f) (support ⇑g) → motive f → motive g → motive (f + g)
f : α →ₛ γ
s : Finset γ
h : range ⇑f \ {0} = ↑s
⊢ motive f
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this✝ : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
s : Set β
h1s : IsClosed[inst✝⁵] s
h2s : s.Nonempty
h3s : s ≠ Set.univ
this : Measurable fun x ↦ infNndist (g x) s
h4s : g ⁻¹' s = (fun x ↦ infNndist (g x) s) ⁻¹' {0}
⊢ MeasurableSet ((fun x ↦ infNndist (g x) s) ⁻¹' {0})

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this✝ : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
s : Set β
h1s : IsClosed[inst✝⁵] s
h2s : s.Nonempty
h3s : s ≠ Set.univ
this : Measurable fun x ↦ infNndist (g x) s
h4s : g ⁻¹' s = (fun x ↦ infNndist (g x) s) ⁻¹' {0}
⊢ MeasurableSet ((fun x ↦ infNndist (g x) s) ⁻¹' {0})
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: ⊢ generateFrom (range fun a ↦ Iio ↑a) = generateFrom (range fun a ↦ Ici ↑a)

Tactic:
]

Goal state after:
⊢ generateFrom (range fun a ↦ Iio ↑a) = generateFrom (range fun a ↦ Ici ↑a)
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: case empty
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ⇑f) (support ⇑g) → motive f → motive g → motive (f + g)
f : α →ₛ γ
h : ⇑f = Function.const α 0
⊢ motive f

Tactic:
]

Goal state after:
case empty
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ⇑f) (support ⇑g) → motive f → motive g → motive (f + g)
f : α →ₛ γ
h : ⇑f = Function.const α 0
⊢ motive f
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case refine_1
q : ℚ
⊢ MeasurableSet (Ici ↑q)ᶜ

Tactic:
]

Goal state after:
case refine_1
q : ℚ
⊢ MeasurableSet (Ici ↑q)ᶜ
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case refine_2
q : ℚ
⊢ MeasurableSet (Iio ↑q)ᶜ

Tactic:
]

Goal state after:
case refine_2
q : ℚ
⊢ MeasurableSet (Iio ↑q)ᶜ
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : ∀ (x : α), Tendsto (fun i ↦ f i x) u (𝓝 (g x))
x : ℕ → ι
hx : Tendsto x atTop u
⊢ Measurable g

Tactic:
]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : ∀ (x : α), Tendsto (fun i ↦ f i x) u (𝓝 (g x))
x : ℕ → ι
hx : Tendsto x atTop u
⊢ Measurable g
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : ∀ (x : α), Tendsto (fun i ↦ f i x) u (𝓝 (g x))
x : ℕ → ι
hx : Tendsto x atTop u
this : (fun y ↦ liminf (fun n ↦ f (x n) y) atTop) = g
⊢ Measurable fun y ↦ liminf (fun n ↦ f (x n) y) atTop

Tactic:
]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : ∀ (x : α), Tendsto (fun i ↦ f i x) u (𝓝 (g x))
x : ℕ → ι
hx : Tendsto x atTop u
this : (fun y ↦ liminf (fun n ↦ f (x n) y) atTop) = g
⊢ Measurable fun y ↦ liminf (fun n ↦ f (x n) y) atTop