-- Mathlib/Topology/Semicontinuous.lean
theorem lowerSemicontinuousWithinAt_iff_le_liminf {f : α → γ} :
    LowerSemicontinuousWithinAt f s x ↔ f x ≤ liminf f (𝓝[s] x)

Proof state:
case mp
α : Type u_1
inst✝² : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝¹ : CompleteLinearOrder γ
inst✝ : DenselyOrdered γ
f : α → γ
hf : ∀ y < f x, ∀ᶠ (x' : α) in 𝓝[s] x, y < f x'
⊢ f x ≤ liminf f (𝓝[s] x)

Tactic:
contrapose! hf

Result:
case mp
α : Type u_1
inst✝² : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝¹ : CompleteLinearOrder γ
inst✝ : DenselyOrdered γ
f : α → γ
hf : liminf f (𝓝[s] x) < f x
⊢ ∃ y < f x, ¬∀ᶠ (x' : α) in 𝓝[s] x, y < f x'

Proof state:
case mpr
α : Type u_1
inst✝² : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝¹ : CompleteLinearOrder γ
inst✝ : DenselyOrdered γ
f : α → γ
⊢ f x ≤ liminf f (𝓝[s] x) → LowerSemicontinuousWithinAt f s x

Tactic:
exact fun hf y ylt => eventually_lt_of_lt_liminf (ylt.trans_le hf)

Result:
no goals

Proof state:
case mp.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝¹ : CompleteLinearOrder γ
inst✝ : DenselyOrdered γ
f : α → γ
hf : liminf f (𝓝[s] x) < f x
y : γ
lty : liminf f (𝓝[s] x) < y
ylt : y < f x
⊢ ∃ y < f x, ¬∀ᶠ (x' : α) in 𝓝[s] x, y < f x'

Tactic:
use y

Result:
case h
α : Type u_1
inst✝² : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝¹ : CompleteLinearOrder γ
inst✝ : DenselyOrdered γ
f : α → γ
hf : liminf f (𝓝[s] x) < f x
y : γ
lty : liminf f (𝓝[s] x) < y
ylt : y < f x
⊢ y < f x ∧ ¬∀ᶠ (x' : α) in 𝓝[s] x, y < f x'

Proof state:
case mp
α : Type u_1
inst✝² : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝¹ : CompleteLinearOrder γ
inst✝ : DenselyOrdered γ
f : α → γ
hf : LowerSemicontinuousWithinAt f s x
⊢ f x ≤ liminf f (𝓝[s] x)

Tactic:
unfold LowerSemicontinuousWithinAt at hf

Result:
case mp
α : Type u_1
inst✝² : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝¹ : CompleteLinearOrder γ
inst✝ : DenselyOrdered γ
f : α → γ
hf : ∀ y < f x, ∀ᶠ (x' : α) in 𝓝[s] x, y < f x'
⊢ f x ≤ liminf f (𝓝[s] x)

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝¹ : CompleteLinearOrder γ
inst✝ : DenselyOrdered γ
f : α → γ
⊢ LowerSemicontinuousWithinAt f s x ↔ f x ≤ liminf f (𝓝[s] x)

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝² : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝¹ : CompleteLinearOrder γ
inst✝ : DenselyOrdered γ
f : α → γ
⊢ LowerSemicontinuousWithinAt f s x → f x ≤ liminf f (𝓝[s] x)

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

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝¹ : CompleteLinearOrder γ
inst✝ : DenselyOrdered γ
f : α → γ
hf : liminf f (𝓝[s] x) < f x
y : γ
lty : liminf f (𝓝[s] x) < y
ylt : y < f x
h : ∀ᶠ (x' : α) in 𝓝[s] x, y < f x'
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) (𝓝[s] x) f

Tactic:
isBoundedDefault

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝² : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝¹ : CompleteLinearOrder γ
inst✝ : DenselyOrdered γ
f : α → γ
hf : liminf f (𝓝[s] x) < f x
y : γ
lty : liminf f (𝓝[s] x) < y
ylt : y < f x
⊢ y < f x ∧ ¬∀ᶠ (x' : α) in 𝓝[s] x, y < f x'

Tactic:
exact ⟨ylt, fun h => lty.not_le
  (le_liminf_of_le (by isBoundedDefault) (h.mono fun _ hx => le_of_lt hx))⟩

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝² : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝¹ : CompleteLinearOrder γ
inst✝ : DenselyOrdered γ
f : α → γ
⊢ LowerSemicontinuousWithinAt f s x → f x ≤ liminf f (𝓝[s] x)

Tactic:
intro hf

Result:
case mp
α : Type u_1
inst✝² : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝¹ : CompleteLinearOrder γ
inst✝ : DenselyOrdered γ
f : α → γ
hf : LowerSemicontinuousWithinAt f s x
⊢ f x ≤ liminf f (𝓝[s] x)

Proof state:
case mp
α : Type u_1
inst✝² : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝¹ : CompleteLinearOrder γ
inst✝ : DenselyOrdered γ
f : α → γ
hf : liminf f (𝓝[s] x) < f x
⊢ ∃ y < f x, ¬∀ᶠ (x' : α) in 𝓝[s] x, y < f x'

Tactic:
obtain ⟨y, lty, ylt⟩ := exists_between hf

Result:
case mp.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝¹ : CompleteLinearOrder γ
inst✝ : DenselyOrdered γ
f : α → γ
hf : liminf f (𝓝[s] x) < f x
y : γ
lty : liminf f (𝓝[s] x) < y
ylt : y < f x
⊢ ∃ y < f x, ¬∀ᶠ (x' : α) in 𝓝[s] x, y < f x'