-- Mathlib/Topology/Semicontinuous.lean
theorem lowerSemicontinuous_iff_isClosed_epigraph {f : α → γ} :
    LowerSemicontinuous f ↔ IsClosed {p : α × γ | f p.1 ≤ p.2}

Proof state:
case mpr
α : Type u_1
inst✝⁴ : TopologicalSpace α
γ : Type u_3
inst✝³ : CompleteLinearOrder γ
inst✝² : DenselyOrdered γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ IsClosed {p | f p.1 ≤ p.2} → ∀ (y : γ), IsClosed (f ⁻¹' Iic y)

Tactic:
exact fun hf y ↦ hf.preimage (Continuous.Prod.mk_left y)

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝⁴ : TopologicalSpace α
γ : Type u_3
inst✝³ : CompleteLinearOrder γ
inst✝² : DenselyOrdered γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ (∀ (x : α), f x ≤ liminf f (𝓝 x)) →
    ∀ (x : α × γ) (F : Filter (α × γ)), F.NeBot → F ≤ 𝓟 {p | f p.1 ≤ p.2} → F ≤ 𝓝 x → x ∈ {p | f p.1 ≤ p.2}

Tactic:
rintro hf ⟨x, y⟩ F F_ne h h'

Result:
case mp.mk
α : Type u_1
inst✝⁴ : TopologicalSpace α
γ : Type u_3
inst✝³ : CompleteLinearOrder γ
inst✝² : DenselyOrdered γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
hf : ∀ (x : α), f x ≤ liminf f (𝓝 x)
x : α
y : γ
F : Filter (α × γ)
F_ne : F.NeBot
h : F ≤ 𝓟 {p | f p.1 ≤ p.2}
h' : F ≤ 𝓝 (x, y)
⊢ (x, y) ∈ {p | f p.1 ≤ p.2}

Proof state:
case mpr
α : Type u_1
inst✝⁴ : TopologicalSpace α
γ : Type u_3
inst✝³ : CompleteLinearOrder γ
inst✝² : DenselyOrdered γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ IsClosed {p | f p.1 ≤ p.2} → LowerSemicontinuous f

Tactic:
rw [lowerSemicontinuous_iff_isClosed_preimage]

Result:
case mpr
α : Type u_1
inst✝⁴ : TopologicalSpace α
γ : Type u_3
inst✝³ : CompleteLinearOrder γ
inst✝² : DenselyOrdered γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ IsClosed {p | f p.1 ≤ p.2} → ∀ (y : γ), IsClosed (f ⁻¹' Iic y)

Proof state:
case mp
α : Type u_1
inst✝⁴ : TopologicalSpace α
γ : Type u_3
inst✝³ : CompleteLinearOrder γ
inst✝² : DenselyOrdered γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ LowerSemicontinuous f → IsClosed {p | f p.1 ≤ p.2}

Tactic:
rw [lowerSemicontinuous_iff_le_liminf, isClosed_iff_forall_filter]

Result:
case mp
α : Type u_1
inst✝⁴ : TopologicalSpace α
γ : Type u_3
inst✝³ : CompleteLinearOrder γ
inst✝² : DenselyOrdered γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ (∀ (x : α), f x ≤ liminf f (𝓝 x)) →
    ∀ (x : α × γ) (F : Filter (α × γ)), F.NeBot → F ≤ 𝓟 {p | f p.1 ≤ p.2} → F ≤ 𝓝 x → x ∈ {p | f p.1 ≤ p.2}

Proof state:
case mp.mk
α : Type u_1
inst✝⁴ : TopologicalSpace α
γ : Type u_3
inst✝³ : CompleteLinearOrder γ
inst✝² : DenselyOrdered γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
hf : ∀ (x : α), f x ≤ liminf f (𝓝 x)
x : α
y : γ
F : Filter (α × γ)
F_ne : F.NeBot
h : F ≤ 𝓟 {p | f p.1 ≤ p.2}
h' : F ≤ 𝓝 (x, y)
⊢ (x, y) ∈ {p | f p.1 ≤ p.2}

Tactic:
rw [nhds_prod_eq, le_prod] at h'

Result:
case mp.mk
α : Type u_1
inst✝⁴ : TopologicalSpace α
γ : Type u_3
inst✝³ : CompleteLinearOrder γ
inst✝² : DenselyOrdered γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
hf : ∀ (x : α), f x ≤ liminf f (𝓝 x)
x : α
y : γ
F : Filter (α × γ)
F_ne : F.NeBot
h : F ≤ 𝓟 {p | f p.1 ≤ p.2}
h' : Tendsto Prod.fst F (𝓝 x) ∧ Tendsto Prod.snd F (𝓝 y)
⊢ (x, y) ∈ {p | f p.1 ≤ p.2}

Proof state:
α : Type u_1
inst✝⁴ : TopologicalSpace α
γ : Type u_3
inst✝³ : CompleteLinearOrder γ
inst✝² : DenselyOrdered γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
hf : ∀ (x : α), f x ≤ liminf f (𝓝 x)
x : α
y : γ
F : Filter (α × γ)
F_ne : F.NeBot
h : F ≤ 𝓟 {p | f p.1 ≤ p.2}
h' : Tendsto Prod.fst F (𝓝 x) ∧ Tendsto Prod.snd F (𝓝 y)
⊢ ∀ᶠ (a : α × γ) in F, (f ∘ Prod.fst) a ≤ a.2

Tactic:
simpa using (eventually_principal.2 fun (_ : α × γ) ↦ id).filter_mono h

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : TopologicalSpace α
γ : Type u_3
inst✝³ : CompleteLinearOrder γ
inst✝² : DenselyOrdered γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ LowerSemicontinuous f ↔ IsClosed {p | f p.1 ≤ p.2}

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝⁴ : TopologicalSpace α
γ : Type u_3
inst✝³ : CompleteLinearOrder γ
inst✝² : DenselyOrdered γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ LowerSemicontinuous f → IsClosed {p | f p.1 ≤ p.2}

case mpr
α : Type u_1
inst✝⁴ : TopologicalSpace α
γ : Type u_3
inst✝³ : CompleteLinearOrder γ
inst✝² : DenselyOrdered γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ IsClosed {p | f p.1 ≤ p.2} → LowerSemicontinuous f

Proof state:
case mp.mk
α : Type u_1
inst✝⁴ : TopologicalSpace α
γ : Type u_3
inst✝³ : CompleteLinearOrder γ
inst✝² : DenselyOrdered γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
hf : ∀ (x : α), f x ≤ liminf f (𝓝 x)
x : α
y : γ
F : Filter (α × γ)
F_ne : F.NeBot
h : F ≤ 𝓟 {p | f p.1 ≤ p.2}
h' : Tendsto Prod.fst F (𝓝 x) ∧ Tendsto Prod.snd F (𝓝 y)
⊢ (x, y) ∈ {p | f p.1 ≤ p.2}

Tactic:
calc f x ≤ liminf f (𝓝 x) := hf x
_ ≤ liminf f (map Prod.fst F) := liminf_le_liminf_of_le h'.1
_ = liminf (f ∘ Prod.fst) F := (Filter.liminf_comp _ _ _).symm
_ ≤ liminf Prod.snd F := liminf_le_liminf <| by
      simpa using (eventually_principal.2 fun (_ : α × γ) ↦ id).filter_mono h
_ = y := h'.2.liminf_eq

Result:
no goals