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

Goal state before:
pp: case pos
x : EReal
hx : x < ⊤
hx_bot : x = ⊥
⊢ ∃ i', Ico ↑i' ⊤ ⊆ Ici x ∩ {⊤}ᶜ

pp: case neg
x : EReal
hx : x < ⊤
hx_bot : ¬x = ⊥
⊢ ∃ i', Ico ↑i' ⊤ ⊆ Ici x ∩ {⊤}ᶜ

Tactic:
·

Goal state after:
case pos
x : EReal
hx : x < ⊤
hx_bot : x = ⊥
⊢ ∃ i', Ico ↑i' ⊤ ⊆ Ici x ∩ {⊤}ᶜ
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
γ : Type u_4
inst✝ : LinearOrder γ
f : α → γ
⊢ LowerSemicontinuous f ↔ ∀ (y : γ), IsClosed[inst✝¹] (f ⁻¹' Iic y)

Tactic:
by
  rw [lowerSemicontinuous_iff_isOpen_preimage]
  simp only [← isOpen_compl_iff, ← preimage_compl, compl_Iic]

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝ : LinearOrder γ
f : α → γ
⊢ LowerSemicontinuousOn f s ↔ ∀ (b : γ), ∃ v, IsClosed[inst✝¹] v ∧ s ∩ f ⁻¹' Iic b = s ∩ v

Tactic:
by
  simp only [← lowerSemicontinuous_restrict_iff, domRestrict_eq,
      lowerSemicontinuous_iff_isClosed_preimage, preimage_comp,
      isClosed_induced_iff, Subtype.preimage_coe_eq_preimage_coe_iff, eq_comm]

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝ : CompleteLinearOrder γ
f : α → γ
⊢ LowerSemicontinuousWithinAt f s x → f x ≤ liminf f (𝓝[s] x)

pp: case mpr
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝ : CompleteLinearOrder γ
f : α → γ
⊢ f x ≤ liminf f (𝓝[s] x) → LowerSemicontinuousWithinAt f s x

Tactic:
·

Goal state after:
case mp
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝ : CompleteLinearOrder γ
f : α → γ
⊢ LowerSemicontinuousWithinAt f s x → f x ≤ liminf f (𝓝[s] x)
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case inr.inr.inr
a b c : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
hc : a * b < c
a_top : a < ⊤
b0 : 0 < b
b_top : b < ⊤
⊢ ∃ a' ∈ Ioo a ⊤, a' * b < c

Tactic:
·

Goal state after:
case inr.inr.inr
a b c : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
hc : a * b < c
a_top : a < ⊤
b0 : 0 < b
b_top : b < ⊤
⊢ ∃ a' ∈ Ioo a ⊤, a' * b < c
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h'
⊢ ∀ (i' : ℝ), True → ∃ i < ⊤, Ici i ∩ {⊤}ᶜ ⊆ Real.toEReal '' Ici i'

Tactic:
·

Goal state after:
case h'
⊢ ∀ (i' : ℝ), True → ∃ i < ⊤, Ici i ∩ {⊤}ᶜ ⊆ Real.toEReal '' Ici i'
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h
⊢ ∀ (i : EReal), ⊥ < i → ∃ i', True ∧ Real.toEReal '' Iic i' ⊆ Iic i ∩ {⊥}ᶜ

pp: case h'
⊢ ∀ (i' : ℝ), True → ∃ i, ⊥ < i ∧ Iic i ∩ {⊥}ᶜ ⊆ Real.toEReal '' Iic i'

Tactic:
·

Goal state after:
case h
⊢ ∀ (i : EReal), ⊥ < i → ∃ i', True ∧ Real.toEReal '' Iic i' ⊆ Iic i ∩ {⊥}ᶜ
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝ : LinearOrder γ
ι : Type u_5
f : ι → α → γ
ks : IsCompact s
I : Set ι
c : γ
hfi : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
H : s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c = ∅
⊢ ∃ u, ∀ x ∈ s, ∃ i ∈ u, c < f (↑i) x

pp: case refine_2
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝ : LinearOrder γ
ι : Type u_5
f : ι → α → γ
ks : IsCompact s
I : Set ι
c : γ
hfi : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
x✝ : ∃ u, ∀ x ∈ s, ∃ i ∈ u, c < f (↑i) x
u : Finset ↑I
hu : ∀ x ∈ s, ∃ i ∈ u, c < f (↑i) x
⊢ s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c = ∅

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝ : LinearOrder γ
ι : Type u_5
f : ι → α → γ
ks : IsCompact s
I : Set ι
c : γ
hfi : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
H : s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c = ∅
⊢ ∃ u, ∀ x ∈ s, ∃ i ∈ u, c < f (↑i) x
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case pos
x : EReal
hx : ⊥ < x
hx_top : x = ⊤
⊢ ∃ i', Ioc ⊥ ↑i' ⊆ Iic x ∩ {⊥}ᶜ

pp: case neg
x : EReal
hx : ⊥ < x
hx_top : ¬x = ⊤
⊢ ∃ i', Ioc ⊥ ↑i' ⊆ Iic x ∩ {⊥}ᶜ

Tactic:
·

Goal state after:
case pos
x : EReal
hx : ⊥ < x
hx_top : x = ⊤
⊢ ∃ i', Ioc ⊥ ↑i' ⊆ Iic x ∩ {⊥}ᶜ
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝ : LinearOrder γ
ι : Type u_5
f : ι → α → γ
ks : IsCompact s
I : Set ι
c : γ
hfi : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
x✝ : ∃ u, ∀ x ∈ s, ∃ i ∈ u, c < f (↑i) x
u : Finset ↑I
hu : ∀ x ∈ s, ∃ i ∈ u, c < f (↑i) x
⊢ s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c = ∅

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝ : LinearOrder γ
ι : Type u_5
f : ι → α → γ
ks : IsCompact s
I : Set ι
c : γ
hfi : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
x✝ : ∃ u, ∀ x ∈ s, ∃ i ∈ u, c < f (↑i) x
u : Finset ↑I
hu : ∀ x ∈ s, ∃ i ∈ u, c < f (↑i) x
⊢ s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c = ∅
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case inl
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ioo 0 a, ∀ b' ∈ Ioo 0 b, a' * b' ≤ c
d : EReal
dab : d < a * b
d0 : d < 0
⊢ d ≤ c

pp: case inr
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ioo 0 a, ∀ b' ∈ Ioo 0 b, a' * b' ≤ c
d : EReal
dab : d < a * b
d0 : 0 ≤ d
⊢ d ≤ c

Tactic:
·

Goal state after:
case inl
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ioo 0 a, ∀ b' ∈ Ioo 0 b, a' * b' ≤ c
d : EReal
dab : d < a * b
d0 : d < 0
⊢ d ≤ c
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h'
⊢ ∀ (i' : ℝ), True → ∃ i, ⊥ < i ∧ Iic i ∩ {⊥}ᶜ ⊆ Real.toEReal '' Iic i'

Tactic:
·

Goal state after:
case h'
⊢ ∀ (i' : ℝ), True → ∃ i, ⊥ < i ∧ Iic i ∩ {⊥}ᶜ ⊆ Real.toEReal '' Iic i'
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case pos
x : EReal
h_top : x = ⊤
⊢ ContinuousAt toENNReal x

pp: case neg
x : EReal
h_top : ¬x = ⊤
⊢ ContinuousAt toENNReal x

Tactic:
·

Goal state after:
case pos
x : EReal
h_top : x = ⊤
⊢ ContinuousAt toENNReal x
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case pos
x✝ : EReal
h_top : ¬x✝ = ⊤
x : EReal
hx : x ∈ {⊤}ᶜ
h_bot : x = ⊥
⊢ ContinuousAt (fun x ↦ ENNReal.ofReal x.toReal) x

pp: case neg
x✝ : EReal
h_top : ¬x✝ = ⊤
x : EReal
hx : x ∈ {⊤}ᶜ
h_bot : ¬x = ⊥
⊢ ContinuousAt (fun x ↦ ENNReal.ofReal x.toReal) x

Tactic:
·

Goal state after:
case pos
x✝ : EReal
h_top : ¬x✝ = ⊤
x : EReal
hx : x ∈ {⊤}ᶜ
h_bot : x = ⊥
⊢ ContinuousAt (fun x ↦ ENNReal.ofReal x.toReal) x
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : ∑' (i : ℕ), μ (s i) < ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), ↑(ε' i) < ↑ε
i : ℕ
⊢ ∃ f, s i ⊆ ⋃ i, f i ∧ ∑' (i : ℕ), m (f i) < μ (s i) + ↑(ε' i)

Tactic:
have : μ (s i) < μ (s i) + ε' i :=
              ENNReal.lt_add_right (ne_top_of_le_ne_top hb.ne <| ENNReal.le_tsum _)
                (by simpa using (hε' i).ne')

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : ∑' (i : ℕ), μ (s i) < ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), ↑(ε' i) < ↑ε
i : ℕ
this : μ (s i) < μ (s i) + ↑(ε' i)
⊢ ∃ f, s i ⊆ ⋃ i, f i ∧ ∑' (i : ℕ), m (f i) < μ (s i) + ↑(ε' i)
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case mp
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
⊢ (∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x) →
    ∀ (x : α × γ), (x.1 ∈ s → x.2 < f x.1) → ∀ᶠ (a : α × γ) in 𝓝 x, a.1 ∈ s → a.2 < f a.1

pp: case mpr
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
⊢ (∀ (x : α × γ), (x.1 ∈ s → x.2 < f x.1) → ∀ᶠ (a : α × γ) in 𝓝 x, a.1 ∈ s → a.2 < f a.1) →
    ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x

Tactic:
·

Goal state after:
case mp
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
⊢ (∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x) →
    ∀ (x : α × γ), (x.1 ∈ s → x.2 < f x.1) → ∀ᶠ (a : α × γ) in 𝓝 x, a.1 ∈ s → a.2 < f a.1
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
⊢ limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥

pp: α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
⊢ limsup u f + limsup v f ≤ ⊥

Tactic:
·

Goal state after:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
⊢ limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
hf : ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
x : α
y : γ
h : (x, y).1 ∈ s → (x, y).2 < f (x, y).1
hx : x ∈ s
⊢ ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1

pp: case neg
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
hf : ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
x : α
y : γ
h : (x, y).1 ∈ s → (x, y).2 < f (x, y).1
hx : x ∉ s
⊢ ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
hf : ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
x : α
y : γ
h : (x, y).1 ∈ s → (x, y).2 < f (x, y).1
hx : x ∈ s
⊢ ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
⊢ limsup u f + limsup v f ≤ ⊥

Tactic:
·

Goal state after:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
⊢ limsup u f + limsup v f ≤ ⊥
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
hf : ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
x : α
y : γ
h : (x, y).1 ∈ s → (x, y).2 < f (x, y).1
hx : x ∉ s
⊢ ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
hf : ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
x : α
y : γ
h : (x, y).1 ∈ s → (x, y).2 < f (x, y).1
hx : x ∉ s
⊢ ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case inl
α : Type u_3
f : Filter α
u v : α → EReal
a : EReal
ha : limsup u f < a
hb : limsup v f ≤ ⊤
⊢ limsup (u + v) f ≤ a + ⊤

pp: case inr
α : Type u_3
f : Filter α
u v : α → EReal
a b : EReal
ha : limsup u f < a
hb : limsup v f ≤ b
h : b < ⊤
⊢ limsup (u + v) f ≤ a + b

Tactic:
·

Goal state after:
case inl
α : Type u_3
f : Filter α
u v : α → EReal
a : EReal
ha : limsup u f < a
hb : limsup v f ≤ ⊤
⊢ limsup (u + v) f ≤ a + ⊤
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case mpr
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
⊢ (∀ (x : α × γ), (x.1 ∈ s → x.2 < f x.1) → ∀ᶠ (a : α × γ) in 𝓝 x, a.1 ∈ s → a.2 < f a.1) →
    ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x

Tactic:
·

Goal state after:
case mpr
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
⊢ (∀ (x : α × γ), (x.1 ∈ s → x.2 < f x.1) → ∀ᶠ (a : α × γ) in 𝓝 x, a.1 ∈ s → a.2 < f a.1) →
    ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case inr
α : Type u_3
f : Filter α
u v : α → EReal
a b : EReal
ha : limsup u f < a
hb : limsup v f ≤ b
h : b < ⊤
⊢ limsup (u + v) f ≤ a + b

Tactic:
·

Goal state after:
case inr
α : Type u_3
f : Filter α
u v : α → EReal
a b : EReal
ha : limsup u f < a
hb : limsup v f ≤ b
h : b < ⊤
⊢ limsup (u + v) f ≤ a + b
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case inl
α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
h₁ : 0 ≤ 0
h₂ : 0 ≠ ⊤
⊢ limsup (fun x ↦ 0 * u x) f = 0 * limsup u f

pp: case inr
α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ limsup (fun x ↦ c * u x) f = c * limsup u f

Tactic:
·

Goal state after:
case inl
α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
h₁ : 0 ≤ 0
h₂ : 0 ≠ ⊤
⊢ limsup (fun x ↦ 0 * u x) f = 0 * limsup u f
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case inr.a
α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ limsup (fun x ↦ u x * c) f ≤ limsup u f * c

pp: case a
α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ limsup u f * c ≤ limsup (fun x ↦ u x * c) f

Tactic:
·

Goal state after:
case inr.a
α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ limsup (fun x ↦ u x * c) f ≤ limsup u f * c
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case convert_2
𝕜 : Type u_4
inst✝⁵ : DivisionSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
x : 𝕜
⊢ ℕ → 𝕜

pp: case convert_5
𝕜 : Type u_4
inst✝⁵ : DivisionSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
x : 𝕜
n : ℕ
hn : n ≠ 0
⊢ ?convert_2 n = ↑n / (↑n + x)

pp: case convert_6
𝕜 : Type u_4
inst✝⁵ : DivisionSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
x : 𝕜
⊢ Tendsto ?convert_2 atTop (𝓝 1)

Tactic:
·

Goal state after:
case convert_2
𝕜 : Type u_4
inst✝⁵ : DivisionSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
x : 𝕜
⊢ ℕ → 𝕜
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case a
α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ limsup u f * c ≤ limsup (fun x ↦ u x * c) f

Tactic:
·

Goal state after:
case a
α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ limsup u f * c ≤ limsup (fun x ↦ u x * c) f
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case convert_5
𝕜 : Type u_4
inst✝⁵ : DivisionSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
x : 𝕜
n : ℕ
hn : n ≠ 0
⊢ 1 / (1 + x / ↑n) = ↑n / (↑n + x)

pp: case convert_6
𝕜 : Type u_4
inst✝⁵ : DivisionSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
x : 𝕜
⊢ Tendsto (fun n ↦ 1 / (1 + x / ↑n)) atTop (𝓝 1)

Tactic:
·

Goal state after:
case convert_5
𝕜 : Type u_4
inst✝⁵ : DivisionSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
x : 𝕜
n : ℕ
hn : n ≠ 0
⊢ 1 / (1 + x / ↑n) = ↑n / (↑n + x)
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case convert_6
𝕜 : Type u_4
inst✝⁵ : DivisionSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
x : 𝕜
⊢ Tendsto (fun n ↦ 1 / (1 + x / ↑n)) atTop (𝓝 1)

Tactic:
·

Goal state after:
case convert_6
𝕜 : Type u_4
inst✝⁵ : DivisionSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
x : 𝕜
⊢ Tendsto (fun n ↦ 1 / (1 + x / ↑n)) atTop (𝓝 1)
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝⁶ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_5
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : (g ∘ f) x > y
h : ∃ l, l < f x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (g ∘ f) x1 > x2) x' y

pp: case neg
α : Type u_1
inst✝⁶ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_5
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : (g ∘ f) x > y
h : ∀ (l : γ), f x ≤ l
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (g ∘ f) x1 > x2) x' y

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝⁶ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_5
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : (g ∘ f) x > y
h : ∃ l, l < f x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (g ∘ f) x1 > x2) x' y
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case inl
α : Type u_3
u v : α → EReal
hu : ∃ᶠ (x : α) in ⊥, 0 ≤ u x
hv : 0 ≤ᶠ[⊥] v
⊢ limsup u ⊥ * liminf v ⊥ ≤ limsup (u * v) ⊥

pp: case inr
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h✝ : f.NeBot
⊢ limsup u f * liminf v f ≤ limsup (u * v) f

Tactic:
·

Goal state after:
case inl
α : Type u_3
u v : α → EReal
hu : ∃ᶠ (x : α) in ⊥, 0 ≤ u x
hv : 0 ≤ᶠ[⊥] v
⊢ limsup u ⊥ * liminf v ⊥ ≤ limsup (u * v) ⊥
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝⁶ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_5
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : (g ∘ f) x > y
h : ∀ (l : γ), f x ≤ l
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (g ∘ f) x1 > x2) x' y

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝⁶ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_5
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : (g ∘ f) x > y
h : ∀ (l : γ), f x ≤ l
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (g ∘ f) x1 > x2) x' y
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case inl
α : Type u_3
u v : α → EReal
hu : ∃ᶠ (x : α) in ⊥, 0 ≤ u x
hv : 0 ≤ᶠ[⊥] v
h₁ : limsup u ⊥ ≠ 0 ∨ limsup v ⊥ ≠ ⊤
h₂ : limsup u ⊥ ≠ ⊤ ∨ limsup v ⊥ ≠ 0
⊢ limsup (u * v) ⊥ ≤ limsup u ⊥ * limsup v ⊥

pp: case inr
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h₁ : limsup u f ≠ 0 ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ limsup v f ≠ 0
h✝ : f.NeBot
⊢ limsup (u * v) f ≤ limsup u f * limsup v f

Tactic:
·

Goal state after:
case inl
α : Type u_3
u v : α → EReal
hu : ∃ᶠ (x : α) in ⊥, 0 ≤ u x
hv : 0 ≤ᶠ[⊥] v
h₁ : limsup u ⊥ ≠ 0 ∨ limsup v ⊥ ≠ ⊤
h₂ : limsup u ⊥ ≠ ⊤ ∨ limsup v ⊥ ≠ 0
⊢ limsup (u * v) ⊥ ≤ limsup u ⊥ * limsup v ⊥
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case hl
𝕜 : Type u_4
inst✝⁵ : Semifield 𝕜
inst✝⁴ : CharZero 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ (fun k ↦ (a * (↑k)⁻¹ + c) / (b * (↑k)⁻¹ + d)) =ᶠ[atTop] fun k ↦ (a + c * ↑k) / (b + d * ↑k)

pp: case h
𝕜 : Type u_4
inst✝⁵ : Semifield 𝕜
inst✝⁴ : CharZero 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ Tendsto (fun k ↦ (a * (↑k)⁻¹ + c) / (b * (↑k)⁻¹ + d)) atTop (𝓝 (c / d))

Tactic:
·

Goal state after:
case hl
𝕜 : Type u_4
inst✝⁵ : Semifield 𝕜
inst✝⁴ : CharZero 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ (fun k ↦ (a * (↑k)⁻¹ + c) / (b * (↑k)⁻¹ + d)) =ᶠ[atTop] fun k ↦ (a + c * ↑k) / (b + d * ↑k)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h✝ : f.NeBot
u_0 : 0 ≤ limsup u f
h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < limsup v f
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > limsup v f
c : EReal
c_ab : c > a * b
x : α
x_a : u x < a
x_b : v x < b
⊢ 0 x ≤ v x → (u * v) x < c

Tactic:
v_0

Goal state after:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h✝ : f.NeBot
u_0 : 0 ≤ limsup u f
h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < limsup v f
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > limsup v f
c : EReal
c_ab : c > a * b
x : α
x_a : u x < a
x_b : v x < b
v_0 : 0 x ≤ v x
⊢ (u * v) x < c
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∃ l, l < f x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y

pp: case neg
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ¬∃ l, l < f x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∃ l, l < f x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y