-- Mathlib/Topology/Order/OrderClosed.lean
theorem frontier_le_subset_eq (hf : Continuous f) (hg : Continuous g) :
    frontier { b | f b ≤ g b } ⊆ { b | f b = g b }

Proof state:
case h.e'_4.h.e'_3
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous f
hg : Continuous g
b : β
hb₁ : b ∈ {b | f b ≤ g b}
hb₂ : b ∈ closure {b | f b ≤ g b}ᶜ
⊢ {b | ¬f b ≤ g b} = {b | f b ≤ g b}ᶜ

Tactic:
rfl

Result:
no goals

Proof state:
case h.e'_4.h.e'_3
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous f
hg : Continuous g
b : β
hb₁ : b ∈ {b | f b ≤ g b}
hb₂ : b ∈ closure {b | f b ≤ g b}ᶜ
⊢ {b | g b < f b} = {b | f b ≤ g b}ᶜ

Tactic:
simp only [not_le.symm]

Result:
case h.e'_4.h.e'_3
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous f
hg : Continuous g
b : β
hb₁ : b ∈ {b | f b ≤ g b}
hb₂ : b ∈ closure {b | f b ≤ g b}ᶜ
⊢ {b | ¬f b ≤ g b} = {b | f b ≤ g b}ᶜ

Proof state:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous f
hg : Continuous g
⊢ {b | f b ≤ g b} ∩ closure {b | f b ≤ g b}ᶜ ⊆ {b | f b = g b}

Tactic:
rintro b ⟨hb₁, hb₂⟩

Result:
case intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous f
hg : Continuous g
b : β
hb₁ : b ∈ {b | f b ≤ g b}
hb₂ : b ∈ closure {b | f b ≤ g b}ᶜ
⊢ b ∈ {b | f b = g b}

Proof state:
case intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous f
hg : Continuous g
b : β
hb₁ : b ∈ {b | f b ≤ g b}
hb₂ : b ∈ closure {b | f b ≤ g b}ᶜ
⊢ b ∈ closure {b | g b < f b}

Tactic:
convert hb₂ using 2

Result:
case h.e'_4.h.e'_3
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous f
hg : Continuous g
b : β
hb₁ : b ∈ {b | f b ≤ g b}
hb₂ : b ∈ closure {b | f b ≤ g b}ᶜ
⊢ {b | g b < f b} = {b | f b ≤ g b}ᶜ

Proof state:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous f
hg : Continuous g
⊢ frontier {b | f b ≤ g b} ⊆ {b | f b = g b}

Tactic:
rw [frontier_eq_closure_inter_closure, closure_le_eq hf hg]

Result:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous f
hg : Continuous g
⊢ {b | f b ≤ g b} ∩ closure {b | f b ≤ g b}ᶜ ⊆ {b | f b = g b}

Proof state:
case intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous f
hg : Continuous g
b : β
hb₁ : b ∈ {b | f b ≤ g b}
hb₂ : b ∈ closure {b | f b ≤ g b}ᶜ
⊢ b ∈ {b | f b = g b}

Tactic:
refine le_antisymm hb₁ (closure_lt_subset_le hg hf ?_)

Result:
case intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous f
hg : Continuous g
b : β
hb₁ : b ∈ {b | f b ≤ g b}
hb₂ : b ∈ closure {b | f b ≤ g b}ᶜ
⊢ b ∈ closure {b | g b < f b}