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

Goal state before:
pp: case bot.bot
h₁ : (⊥, ⊥).1 ≠ 0 ∨ (⊥, ⊥).2 ≠ ⊥
h₂ : (⊥, ⊥).1 ≠ 0 ∨ (⊥, ⊥).2 ≠ ⊤
h₃ : (⊥, ⊥).1 ≠ ⊥ ∨ (⊥, ⊥).2 ≠ 0
h₄ : (⊥, ⊥).1 ≠ ⊤ ∨ (⊥, ⊥).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊥, ⊥)

pp: case bot.coe
a✝ : ℝ
h₁ : (⊥, ↑a✝).1 ≠ 0 ∨ (⊥, ↑a✝).2 ≠ ⊥
h₂ : (⊥, ↑a✝).1 ≠ 0 ∨ (⊥, ↑a✝).2 ≠ ⊤
h₃ : (⊥, ↑a✝).1 ≠ ⊥ ∨ (⊥, ↑a✝).2 ≠ 0
h₄ : (⊥, ↑a✝).1 ≠ ⊤ ∨ (⊥, ↑a✝).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊥, ↑a✝)

pp: case bot.top
h₁ : (⊥, ⊤).1 ≠ 0 ∨ (⊥, ⊤).2 ≠ ⊥
h₂ : (⊥, ⊤).1 ≠ 0 ∨ (⊥, ⊤).2 ≠ ⊤
h₃ : (⊥, ⊤).1 ≠ ⊥ ∨ (⊥, ⊤).2 ≠ 0
h₄ : (⊥, ⊤).1 ≠ ⊤ ∨ (⊥, ⊤).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊥, ⊤)

pp: case coe.bot
a✝ : ℝ
h₁ : (↑a✝, ⊥).1 ≠ 0 ∨ (↑a✝, ⊥).2 ≠ ⊥
h₂ : (↑a✝, ⊥).1 ≠ 0 ∨ (↑a✝, ⊥).2 ≠ ⊤
h₃ : (↑a✝, ⊥).1 ≠ ⊥ ∨ (↑a✝, ⊥).2 ≠ 0
h₄ : (↑a✝, ⊥).1 ≠ ⊤ ∨ (↑a✝, ⊥).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝, ⊥)

pp: case coe.coe
a✝¹ a✝ : ℝ
h₁ : (↑a✝¹, ↑a✝).1 ≠ 0 ∨ (↑a✝¹, ↑a✝).2 ≠ ⊥
h₂ : (↑a✝¹, ↑a✝).1 ≠ 0 ∨ (↑a✝¹, ↑a✝).2 ≠ ⊤
h₃ : (↑a✝¹, ↑a✝).1 ≠ ⊥ ∨ (↑a✝¹, ↑a✝).2 ≠ 0
h₄ : (↑a✝¹, ↑a✝).1 ≠ ⊤ ∨ (↑a✝¹, ↑a✝).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝¹, ↑a✝)

pp: case coe.top
a✝ : ℝ
h₁ : (↑a✝, ⊤).1 ≠ 0 ∨ (↑a✝, ⊤).2 ≠ ⊥
h₂ : (↑a✝, ⊤).1 ≠ 0 ∨ (↑a✝, ⊤).2 ≠ ⊤
h₃ : (↑a✝, ⊤).1 ≠ ⊥ ∨ (↑a✝, ⊤).2 ≠ 0
h₄ : (↑a✝, ⊤).1 ≠ ⊤ ∨ (↑a✝, ⊤).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝, ⊤)

pp: case top.bot
h₁ : (⊤, ⊥).1 ≠ 0 ∨ (⊤, ⊥).2 ≠ ⊥
h₂ : (⊤, ⊥).1 ≠ 0 ∨ (⊤, ⊥).2 ≠ ⊤
h₃ : (⊤, ⊥).1 ≠ ⊥ ∨ (⊤, ⊥).2 ≠ 0
h₄ : (⊤, ⊥).1 ≠ ⊤ ∨ (⊤, ⊥).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ⊥)

pp: case top.coe
a✝ : ℝ
h₁ : (⊤, ↑a✝).1 ≠ 0 ∨ (⊤, ↑a✝).2 ≠ ⊥
h₂ : (⊤, ↑a✝).1 ≠ 0 ∨ (⊤, ↑a✝).2 ≠ ⊤
h₃ : (⊤, ↑a✝).1 ≠ ⊥ ∨ (⊤, ↑a✝).2 ≠ 0
h₄ : (⊤, ↑a✝).1 ≠ ⊤ ∨ (⊤, ↑a✝).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ↑a✝)

pp: case top.top
h₁ : (⊤, ⊤).1 ≠ 0 ∨ (⊤, ⊤).2 ≠ ⊥
h₂ : (⊤, ⊤).1 ≠ 0 ∨ (⊤, ⊤).2 ≠ ⊤
h₃ : (⊤, ⊤).1 ≠ ⊥ ∨ (⊤, ⊤).2 ≠ 0
h₄ : (⊤, ⊤).1 ≠ ⊤ ∨ (⊤, ⊤).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ⊤)

Tactic:
·

Goal state after:
case bot.bot
h₁ : (⊥, ⊥).1 ≠ 0 ∨ (⊥, ⊥).2 ≠ ⊥
h₂ : (⊥, ⊥).1 ≠ 0 ∨ (⊥, ⊥).2 ≠ ⊤
h₃ : (⊥, ⊥).1 ≠ ⊥ ∨ (⊥, ⊥).2 ≠ 0
h₄ : (⊥, ⊥).1 ≠ ⊤ ∨ (⊥, ⊥).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊥, ⊥)
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
inst✝ : Preorder α
s : α → Set β
x : α
⊢ ⋂ y, ⋂ (_ : y ≤ x), dissipate s y ⊆ dissipate s x

pp: case h₂
α : Type u_1
β : Type u_2
inst✝ : Preorder α
s : α → Set β
x : α
⊢ dissipate s x ⊆ ⋂ y, ⋂ (_ : y ≤ x), dissipate s y

Tactic:
·

Goal state after:
case h₁
α : Type u_1
β : Type u_2
inst✝ : Preorder α
s : α → Set β
x : α
⊢ ⋂ y, ⋂ (_ : y ≤ x), dissipate s y ⊆ dissipate s x
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: case h₂
α : Type u_1
β : Type u_2
inst✝ : Preorder α
s : α → Set β
x : α
⊢ dissipate s x ⊆ ⋂ y, ⋂ (_ : y ≤ x), dissipate s y

Tactic:
·

Goal state after:
case h₂
α : Type u_1
β : Type u_2
inst✝ : Preorder α
s : α → Set β
x : α
⊢ dissipate s x ⊆ ⋂ y, ⋂ (_ : y ≤ x), dissipate s y
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ∀ (x : β), (∀ (i i_1 : α), i_1 ≤ i → x ∈ s i_1) → ∀ (i : α), x ∈ s i

pp: case h₂
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ∀ (x : β), (∀ (i : α), x ∈ s i) → ∀ (i i_1 : α), i_1 ≤ i → x ∈ s i_1

Tactic:
·

Goal state after:
case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ∀ (x : β), (∀ (i i_1 : α), i_1 ≤ i → x ∈ s i_1) → ∀ (i : α), x ∈ s i
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: case h₂
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ∀ (x : β), (∀ (i : α), x ∈ s i) → ∀ (i i_1 : α), i_1 ≤ i → x ∈ s i_1

Tactic:
·

Goal state after:
case h₂
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ∀ (x : β), (∀ (i : α), x ∈ s i) → ∀ (i i_1 : α), i_1 ≤ i → x ∈ s i_1
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case bot.coe
a✝ : ℝ
h₁ : (⊥, ↑a✝).1 ≠ 0 ∨ (⊥, ↑a✝).2 ≠ ⊥
h₂ : (⊥, ↑a✝).1 ≠ 0 ∨ (⊥, ↑a✝).2 ≠ ⊤
h₃ : (⊥, ↑a✝).1 ≠ ⊥ ∨ (⊥, ↑a✝).2 ≠ 0
h₄ : (⊥, ↑a✝).1 ≠ ⊤ ∨ (⊥, ↑a✝).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊥, ↑a✝)

pp: case bot.top
h₁ : (⊥, ⊤).1 ≠ 0 ∨ (⊥, ⊤).2 ≠ ⊥
h₂ : (⊥, ⊤).1 ≠ 0 ∨ (⊥, ⊤).2 ≠ ⊤
h₃ : (⊥, ⊤).1 ≠ ⊥ ∨ (⊥, ⊤).2 ≠ 0
h₄ : (⊥, ⊤).1 ≠ ⊤ ∨ (⊥, ⊤).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊥, ⊤)

pp: case coe.bot
a✝ : ℝ
h₁ : (↑a✝, ⊥).1 ≠ 0 ∨ (↑a✝, ⊥).2 ≠ ⊥
h₂ : (↑a✝, ⊥).1 ≠ 0 ∨ (↑a✝, ⊥).2 ≠ ⊤
h₃ : (↑a✝, ⊥).1 ≠ ⊥ ∨ (↑a✝, ⊥).2 ≠ 0
h₄ : (↑a✝, ⊥).1 ≠ ⊤ ∨ (↑a✝, ⊥).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝, ⊥)

pp: case coe.coe
a✝¹ a✝ : ℝ
h₁ : (↑a✝¹, ↑a✝).1 ≠ 0 ∨ (↑a✝¹, ↑a✝).2 ≠ ⊥
h₂ : (↑a✝¹, ↑a✝).1 ≠ 0 ∨ (↑a✝¹, ↑a✝).2 ≠ ⊤
h₃ : (↑a✝¹, ↑a✝).1 ≠ ⊥ ∨ (↑a✝¹, ↑a✝).2 ≠ 0
h₄ : (↑a✝¹, ↑a✝).1 ≠ ⊤ ∨ (↑a✝¹, ↑a✝).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝¹, ↑a✝)

pp: case coe.top
a✝ : ℝ
h₁ : (↑a✝, ⊤).1 ≠ 0 ∨ (↑a✝, ⊤).2 ≠ ⊥
h₂ : (↑a✝, ⊤).1 ≠ 0 ∨ (↑a✝, ⊤).2 ≠ ⊤
h₃ : (↑a✝, ⊤).1 ≠ ⊥ ∨ (↑a✝, ⊤).2 ≠ 0
h₄ : (↑a✝, ⊤).1 ≠ ⊤ ∨ (↑a✝, ⊤).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝, ⊤)

pp: case top.bot
h₁ : (⊤, ⊥).1 ≠ 0 ∨ (⊤, ⊥).2 ≠ ⊥
h₂ : (⊤, ⊥).1 ≠ 0 ∨ (⊤, ⊥).2 ≠ ⊤
h₃ : (⊤, ⊥).1 ≠ ⊥ ∨ (⊤, ⊥).2 ≠ 0
h₄ : (⊤, ⊥).1 ≠ ⊤ ∨ (⊤, ⊥).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ⊥)

pp: case top.coe
a✝ : ℝ
h₁ : (⊤, ↑a✝).1 ≠ 0 ∨ (⊤, ↑a✝).2 ≠ ⊥
h₂ : (⊤, ↑a✝).1 ≠ 0 ∨ (⊤, ↑a✝).2 ≠ ⊤
h₃ : (⊤, ↑a✝).1 ≠ ⊥ ∨ (⊤, ↑a✝).2 ≠ 0
h₄ : (⊤, ↑a✝).1 ≠ ⊤ ∨ (⊤, ↑a✝).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ↑a✝)

pp: case top.top
h₁ : (⊤, ⊤).1 ≠ 0 ∨ (⊤, ⊤).2 ≠ ⊥
h₂ : (⊤, ⊤).1 ≠ 0 ∨ (⊤, ⊤).2 ≠ ⊤
h₃ : (⊤, ⊤).1 ≠ ⊥ ∨ (⊤, ⊤).2 ≠ 0
h₄ : (⊤, ⊤).1 ≠ ⊤ ∨ (⊤, ⊤).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ⊤)

Tactic:
·

Goal state after:
case bot.coe
a✝ : ℝ
h₁ : (⊥, ↑a✝).1 ≠ 0 ∨ (⊥, ↑a✝).2 ≠ ⊥
h₂ : (⊥, ↑a✝).1 ≠ 0 ∨ (⊥, ↑a✝).2 ≠ ⊤
h₃ : (⊥, ↑a✝).1 ≠ ⊥ ∨ (⊥, ↑a✝).2 ≠ 0
h₄ : (⊥, ↑a✝).1 ≠ ⊤ ∨ (⊥, ↑a✝).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊥, ↑a✝)
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case refine_1
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x < k
⊢ 0 ≤ (↑x + 1 + 1) * (↑k + 1)⁻¹

pp: case refine_2
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x < k
⊢ (↑x + 1 + 1) * (↑k + 1)⁻¹ ≤ 1

Tactic:
·

Goal state after:
case refine_1
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x < k
⊢ 0 ≤ (↑x + 1 + 1) * (↑k + 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 γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
⊢ f ⁻¹' v ∈ 𝓝[s] x

pp: case neg
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
⊢ f ⁻¹' v ∈ 𝓝[s] x

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
⊢ f ⁻¹' v ∈ 𝓝[s] x
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case bot.top
h₁ : (⊥, ⊤).1 ≠ 0 ∨ (⊥, ⊤).2 ≠ ⊥
h₂ : (⊥, ⊤).1 ≠ 0 ∨ (⊥, ⊤).2 ≠ ⊤
h₃ : (⊥, ⊤).1 ≠ ⊥ ∨ (⊥, ⊤).2 ≠ 0
h₄ : (⊥, ⊤).1 ≠ ⊤ ∨ (⊥, ⊤).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊥, ⊤)

pp: case coe.bot
a✝ : ℝ
h₁ : (↑a✝, ⊥).1 ≠ 0 ∨ (↑a✝, ⊥).2 ≠ ⊥
h₂ : (↑a✝, ⊥).1 ≠ 0 ∨ (↑a✝, ⊥).2 ≠ ⊤
h₃ : (↑a✝, ⊥).1 ≠ ⊥ ∨ (↑a✝, ⊥).2 ≠ 0
h₄ : (↑a✝, ⊥).1 ≠ ⊤ ∨ (↑a✝, ⊥).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝, ⊥)

pp: case coe.coe
a✝¹ a✝ : ℝ
h₁ : (↑a✝¹, ↑a✝).1 ≠ 0 ∨ (↑a✝¹, ↑a✝).2 ≠ ⊥
h₂ : (↑a✝¹, ↑a✝).1 ≠ 0 ∨ (↑a✝¹, ↑a✝).2 ≠ ⊤
h₃ : (↑a✝¹, ↑a✝).1 ≠ ⊥ ∨ (↑a✝¹, ↑a✝).2 ≠ 0
h₄ : (↑a✝¹, ↑a✝).1 ≠ ⊤ ∨ (↑a✝¹, ↑a✝).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝¹, ↑a✝)

pp: case coe.top
a✝ : ℝ
h₁ : (↑a✝, ⊤).1 ≠ 0 ∨ (↑a✝, ⊤).2 ≠ ⊥
h₂ : (↑a✝, ⊤).1 ≠ 0 ∨ (↑a✝, ⊤).2 ≠ ⊤
h₃ : (↑a✝, ⊤).1 ≠ ⊥ ∨ (↑a✝, ⊤).2 ≠ 0
h₄ : (↑a✝, ⊤).1 ≠ ⊤ ∨ (↑a✝, ⊤).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝, ⊤)

pp: case top.bot
h₁ : (⊤, ⊥).1 ≠ 0 ∨ (⊤, ⊥).2 ≠ ⊥
h₂ : (⊤, ⊥).1 ≠ 0 ∨ (⊤, ⊥).2 ≠ ⊤
h₃ : (⊤, ⊥).1 ≠ ⊥ ∨ (⊤, ⊥).2 ≠ 0
h₄ : (⊤, ⊥).1 ≠ ⊤ ∨ (⊤, ⊥).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ⊥)

pp: case top.coe
a✝ : ℝ
h₁ : (⊤, ↑a✝).1 ≠ 0 ∨ (⊤, ↑a✝).2 ≠ ⊥
h₂ : (⊤, ↑a✝).1 ≠ 0 ∨ (⊤, ↑a✝).2 ≠ ⊤
h₃ : (⊤, ↑a✝).1 ≠ ⊥ ∨ (⊤, ↑a✝).2 ≠ 0
h₄ : (⊤, ↑a✝).1 ≠ ⊤ ∨ (⊤, ↑a✝).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ↑a✝)

pp: case top.top
h₁ : (⊤, ⊤).1 ≠ 0 ∨ (⊤, ⊤).2 ≠ ⊥
h₂ : (⊤, ⊤).1 ≠ 0 ∨ (⊤, ⊤).2 ≠ ⊤
h₃ : (⊤, ⊤).1 ≠ ⊥ ∨ (⊤, ⊤).2 ≠ 0
h₄ : (⊤, ⊤).1 ≠ ⊤ ∨ (⊤, ⊤).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ⊤)

Tactic:
·

Goal state after:
case bot.top
h₁ : (⊥, ⊤).1 ≠ 0 ∨ (⊥, ⊤).2 ≠ ⊥
h₂ : (⊥, ⊤).1 ≠ 0 ∨ (⊥, ⊤).2 ≠ ⊤
h₃ : (⊥, ⊤).1 ≠ ⊥ ∨ (⊥, ⊤).2 ≠ 0
h₄ : (⊥, ⊤).1 ≠ ⊤ ∨ (⊥, ⊤).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊥, ⊤)
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case inl
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert ∅ S
hst : (s ∩ t).Nonempty
hs : s = ∅
⊢ s ∩ t ∈ insert ∅ S

pp: case inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert ∅ S
hst : (s ∩ t).Nonempty
hs : s ∈ S
⊢ s ∩ t ∈ insert ∅ S

Tactic:
·

Goal state after:
case inl
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert ∅ S
hst : (s ∩ t).Nonempty
hs : s = ∅
⊢ s ∩ t ∈ insert ∅ S
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert ∅ S
hst : (s ∩ t).Nonempty
hs : s ∈ S
⊢ s ∩ t ∈ insert ∅ S

Tactic:
·

Goal state after:
case inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert ∅ S
hst : (s ∩ t).Nonempty
hs : s ∈ S
⊢ s ∩ t ∈ insert ∅ S
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case inr.inl
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : (s ∩ t).Nonempty
hs : s ∈ S
ht : t = ∅
⊢ s ∩ t ∈ insert ∅ S

pp: case inr.inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : (s ∩ t).Nonempty
hs : s ∈ S
ht : t ∈ S
⊢ s ∩ t ∈ insert ∅ S

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : (s ∩ t).Nonempty
hs : s ∈ S
ht : t = ∅
⊢ s ∩ t ∈ insert ∅ S
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case inr.inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : (s ∩ t).Nonempty
hs : s ∈ S
ht : t ∈ S
⊢ s ∩ t ∈ insert ∅ S

Tactic:
·

Goal state after:
case inr.inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : (s ∩ t).Nonempty
hs : s ∈ S
ht : t ∈ S
⊢ s ∩ t ∈ insert ∅ S
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case inl
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert univ S
hst : (s ∩ t).Nonempty
hs : s = univ
⊢ s ∩ t ∈ insert univ S

pp: case inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert univ S
hst : (s ∩ t).Nonempty
hs : s ∈ S
⊢ s ∩ t ∈ insert univ S

Tactic:
·

Goal state after:
case inl
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert univ S
hst : (s ∩ t).Nonempty
hs : s = univ
⊢ s ∩ t ∈ insert univ S
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert univ S
hst : (s ∩ t).Nonempty
hs : s ∈ S
⊢ s ∩ t ∈ insert univ S

Tactic:
·

Goal state after:
case inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert univ S
hst : (s ∩ t).Nonempty
hs : s ∈ S
⊢ s ∩ t ∈ insert univ S
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case refine_2
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x < k
⊢ (↑x + 1 + 1) * (↑k + 1)⁻¹ ≤ 1

Tactic:
·

Goal state after:
case refine_2
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x < k
⊢ (↑x + 1 + 1) * (↑k + 1)⁻¹ ≤ 1
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case inr.inl
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : (s ∩ t).Nonempty
hs : s ∈ S
ht : t = univ
⊢ s ∩ t ∈ insert univ S

pp: case inr.inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : (s ∩ t).Nonempty
hs : s ∈ S
ht : t ∈ S
⊢ s ∩ t ∈ insert univ S

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : (s ∩ t).Nonempty
hs : s ∈ S
ht : t = univ
⊢ s ∩ t ∈ insert univ S
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case inr.inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : (s ∩ t).Nonempty
hs : s ∈ S
ht : t ∈ S
⊢ s ∩ t ∈ insert univ S

Tactic:
·

Goal state after:
case inr.inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : (s ∩ t).Nonempty
hs : s ∈ S
ht : t ∈ S
⊢ s ∩ t ∈ insert univ S
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 γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∃ u, f x < u
⊢ f ⁻¹' v ∈ 𝓝[s] x

pp: case neg
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∀ (u : γ), u ≤ f x
⊢ f ⁻¹' v ∈ 𝓝[s] x

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∃ u, f x < u
⊢ f ⁻¹' v ∈ 𝓝[s] x
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case coe.bot
a✝ : ℝ
h₁ : (↑a✝, ⊥).1 ≠ 0 ∨ (↑a✝, ⊥).2 ≠ ⊥
h₂ : (↑a✝, ⊥).1 ≠ 0 ∨ (↑a✝, ⊥).2 ≠ ⊤
h₃ : (↑a✝, ⊥).1 ≠ ⊥ ∨ (↑a✝, ⊥).2 ≠ 0
h₄ : (↑a✝, ⊥).1 ≠ ⊤ ∨ (↑a✝, ⊥).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝, ⊥)

pp: case coe.coe
a✝¹ a✝ : ℝ
h₁ : (↑a✝¹, ↑a✝).1 ≠ 0 ∨ (↑a✝¹, ↑a✝).2 ≠ ⊥
h₂ : (↑a✝¹, ↑a✝).1 ≠ 0 ∨ (↑a✝¹, ↑a✝).2 ≠ ⊤
h₃ : (↑a✝¹, ↑a✝).1 ≠ ⊥ ∨ (↑a✝¹, ↑a✝).2 ≠ 0
h₄ : (↑a✝¹, ↑a✝).1 ≠ ⊤ ∨ (↑a✝¹, ↑a✝).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝¹, ↑a✝)

pp: case coe.top
a✝ : ℝ
h₁ : (↑a✝, ⊤).1 ≠ 0 ∨ (↑a✝, ⊤).2 ≠ ⊥
h₂ : (↑a✝, ⊤).1 ≠ 0 ∨ (↑a✝, ⊤).2 ≠ ⊤
h₃ : (↑a✝, ⊤).1 ≠ ⊥ ∨ (↑a✝, ⊤).2 ≠ 0
h₄ : (↑a✝, ⊤).1 ≠ ⊤ ∨ (↑a✝, ⊤).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝, ⊤)

pp: case top.bot
h₁ : (⊤, ⊥).1 ≠ 0 ∨ (⊤, ⊥).2 ≠ ⊥
h₂ : (⊤, ⊥).1 ≠ 0 ∨ (⊤, ⊥).2 ≠ ⊤
h₃ : (⊤, ⊥).1 ≠ ⊥ ∨ (⊤, ⊥).2 ≠ 0
h₄ : (⊤, ⊥).1 ≠ ⊤ ∨ (⊤, ⊥).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ⊥)

pp: case top.coe
a✝ : ℝ
h₁ : (⊤, ↑a✝).1 ≠ 0 ∨ (⊤, ↑a✝).2 ≠ ⊥
h₂ : (⊤, ↑a✝).1 ≠ 0 ∨ (⊤, ↑a✝).2 ≠ ⊤
h₃ : (⊤, ↑a✝).1 ≠ ⊥ ∨ (⊤, ↑a✝).2 ≠ 0
h₄ : (⊤, ↑a✝).1 ≠ ⊤ ∨ (⊤, ↑a✝).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ↑a✝)

pp: case top.top
h₁ : (⊤, ⊤).1 ≠ 0 ∨ (⊤, ⊤).2 ≠ ⊥
h₂ : (⊤, ⊤).1 ≠ 0 ∨ (⊤, ⊤).2 ≠ ⊤
h₃ : (⊤, ⊤).1 ≠ ⊥ ∨ (⊤, ⊤).2 ≠ 0
h₄ : (⊤, ⊤).1 ≠ ⊤ ∨ (⊤, ⊤).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ⊤)

Tactic:
·

Goal state after:
case coe.bot
a✝ : ℝ
h₁ : (↑a✝, ⊥).1 ≠ 0 ∨ (↑a✝, ⊥).2 ≠ ⊥
h₂ : (↑a✝, ⊥).1 ≠ 0 ∨ (↑a✝, ⊥).2 ≠ ⊤
h₃ : (↑a✝, ⊥).1 ≠ ⊥ ∨ (↑a✝, ⊥).2 ≠ 0
h₄ : (↑a✝, ⊥).1 ≠ ⊤ ∨ (↑a✝, ⊥).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝, ⊥)
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case hgf
R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x ↦ a - x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, a - b⁻¹ ≤ ↑⌊a * b⌋₊ / b

pp: case hfh
R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x ↦ a - x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, ↑⌊a * b⌋₊ / b ≤ a

Tactic:
·

Goal state after:
case hgf
R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x ↦ a - x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, a - b⁻¹ ≤ ↑⌊a * b⌋₊ / b
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case hgf
R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x ↦ a - x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, a - b⁻¹ ≤ ↑⌊a * b⌋₊ / b

Tactic:
refine eventually_atTop.2 ⟨1, fun x hx ↦ ?_⟩
    simp only [le_div_iff₀ (zero_lt_one.trans_le hx), _root_.sub_mul,
      inv_mul_cancel₀ (zero_lt_one.trans_le hx).ne']
    have := Nat.lt_floor_add_one (a * x)
    linarith

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

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∃ u, f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
a : α
lfa : f a > l
fau : f a < u
h : f a ≤ f x
⊢ a ∈ f ⁻¹' v

pp: case inr
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∃ u, f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
a : α
lfa : f a > l
fau : f a < u
h : f x < f a
⊢ a ∈ f ⁻¹' v

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∃ u, f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
a : α
lfa : f a > l
fau : f a < u
h : f a ≤ f x
⊢ a ∈ f ⁻¹' v
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case hfh
R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x ↦ a - x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, ↑⌊a * b⌋₊ / b ≤ a

Tactic:
·

Goal state after:
case hfh
R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x ↦ a - x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, ↑⌊a * b⌋₊ / b ≤ a
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∃ u, f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
a : α
lfa : f a > l
fau : f a < u
h : f x < f a
⊢ a ∈ f ⁻¹' v

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∃ u, f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
a : α
lfa : f a > l
fau : f a < u
h : f x < f a
⊢ a ∈ f ⁻¹' 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 γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∀ (u : γ), u ≤ f x
⊢ f ⁻¹' v ∈ 𝓝[s] x

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∀ (u : γ), u ≤ f x
⊢ f ⁻¹' v ∈ 𝓝[s] x
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℝ
h₁ : (↑a✝¹, ↑a✝).1 ≠ 0 ∨ (↑a✝¹, ↑a✝).2 ≠ ⊥
h₂ : (↑a✝¹, ↑a✝).1 ≠ 0 ∨ (↑a✝¹, ↑a✝).2 ≠ ⊤
h₃ : (↑a✝¹, ↑a✝).1 ≠ ⊥ ∨ (↑a✝¹, ↑a✝).2 ≠ 0
h₄ : (↑a✝¹, ↑a✝).1 ≠ ⊤ ∨ (↑a✝¹, ↑a✝).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝¹, ↑a✝)

pp: case coe.top
a✝ : ℝ
h₁ : (↑a✝, ⊤).1 ≠ 0 ∨ (↑a✝, ⊤).2 ≠ ⊥
h₂ : (↑a✝, ⊤).1 ≠ 0 ∨ (↑a✝, ⊤).2 ≠ ⊤
h₃ : (↑a✝, ⊤).1 ≠ ⊥ ∨ (↑a✝, ⊤).2 ≠ 0
h₄ : (↑a✝, ⊤).1 ≠ ⊤ ∨ (↑a✝, ⊤).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝, ⊤)

pp: case top.bot
h₁ : (⊤, ⊥).1 ≠ 0 ∨ (⊤, ⊥).2 ≠ ⊥
h₂ : (⊤, ⊥).1 ≠ 0 ∨ (⊤, ⊥).2 ≠ ⊤
h₃ : (⊤, ⊥).1 ≠ ⊥ ∨ (⊤, ⊥).2 ≠ 0
h₄ : (⊤, ⊥).1 ≠ ⊤ ∨ (⊤, ⊥).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ⊥)

pp: case top.coe
a✝ : ℝ
h₁ : (⊤, ↑a✝).1 ≠ 0 ∨ (⊤, ↑a✝).2 ≠ ⊥
h₂ : (⊤, ↑a✝).1 ≠ 0 ∨ (⊤, ↑a✝).2 ≠ ⊤
h₃ : (⊤, ↑a✝).1 ≠ ⊥ ∨ (⊤, ↑a✝).2 ≠ 0
h₄ : (⊤, ↑a✝).1 ≠ ⊤ ∨ (⊤, ↑a✝).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ↑a✝)

pp: case top.top
h₁ : (⊤, ⊤).1 ≠ 0 ∨ (⊤, ⊤).2 ≠ ⊥
h₂ : (⊤, ⊤).1 ≠ 0 ∨ (⊤, ⊤).2 ≠ ⊤
h₃ : (⊤, ⊤).1 ≠ ⊥ ∨ (⊤, ⊤).2 ≠ 0
h₄ : (⊤, ⊤).1 ≠ ⊤ ∨ (⊤, ⊤).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ⊤)

Tactic:
·

Goal state after:
case coe.coe
a✝¹ a✝ : ℝ
h₁ : (↑a✝¹, ↑a✝).1 ≠ 0 ∨ (↑a✝¹, ↑a✝).2 ≠ ⊥
h₂ : (↑a✝¹, ↑a✝).1 ≠ 0 ∨ (↑a✝¹, ↑a✝).2 ≠ ⊤
h₃ : (↑a✝¹, ↑a✝).1 ≠ ⊥ ∨ (↑a✝¹, ↑a✝).2 ≠ 0
h₄ : (↑a✝¹, ↑a✝).1 ≠ ⊤ ∨ (↑a✝¹, ↑a✝).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝¹, ↑a✝)
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 γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
⊢ f ⁻¹' v ∈ 𝓝[s] x

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
⊢ f ⁻¹' v ∈ 𝓝[s] x
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case hgf
R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x ↦ a + x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, a ≤ ↑⌈a * b⌉₊ / b

pp: case hfh
R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x ↦ a + x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, ↑⌈a * b⌉₊ / b ≤ a + b⁻¹

Tactic:
·

Goal state after:
case hgf
R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x ↦ a + x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, a ≤ ↑⌈a * b⌉₊ / b