-- Mathlib/SetTheory/Ordinal/Topology.lean
theorem isLimit_of_mem_frontier (ha : a ∈ frontier s) : IsLimit a

Proof state:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha :
  (∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ s).Nonempty) ∧
    ∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ sᶜ).Nonempty
⊢ a.IsLimit

Tactic:
by_contra h

Result:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha :
  (∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ s).Nonempty) ∧
    ∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ sᶜ).Nonempty
h : ¬a.IsLimit
⊢ False

Proof state:
case intro.intro
s : Set Ordinal.{u}
a : Ordinal.{u}
ha :
  (∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ s).Nonempty) ∧
    ∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ sᶜ).Nonempty
h : IsOpen {a}
b : Ordinal.{u}
hb : b ∈ {a}
hb' : b ∈ s
⊢ False

Tactic:
rcases ha.2 _ h rfl with ⟨c, hc, hc'⟩

Result:
case intro.intro.intro.intro
s : Set Ordinal.{u}
a : Ordinal.{u}
ha :
  (∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ s).Nonempty) ∧
    ∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ sᶜ).Nonempty
h : IsOpen {a}
b : Ordinal.{u}
hb : b ∈ {a}
hb' : b ∈ s
c : Ordinal.{u}
hc : c ∈ {a}
hc' : c ∈ sᶜ
⊢ False

Proof state:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha :
  (∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ s).Nonempty) ∧
    ∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ sᶜ).Nonempty
h : IsOpen {a}
⊢ False

Tactic:
rcases ha.1 _ h rfl with ⟨b, hb, hb'⟩

Result:
case intro.intro
s : Set Ordinal.{u}
a : Ordinal.{u}
ha :
  (∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ s).Nonempty) ∧
    ∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ sᶜ).Nonempty
h : IsOpen {a}
b : Ordinal.{u}
hb : b ∈ {a}
hb' : b ∈ s
⊢ False

Proof state:
case intro.intro.intro.intro
s : Set Ordinal.{u}
b : Ordinal.{u}
hb' : b ∈ s
c : Ordinal.{u}
hc' : c ∈ sᶜ
ha :
  (∀ (o : Set Ordinal.{u}), IsOpen o → b ∈ o → (o ∩ s).Nonempty) ∧
    ∀ (o : Set Ordinal.{u}), IsOpen o → b ∈ o → (o ∩ sᶜ).Nonempty
h : IsOpen {b}
hc : c = b
⊢ False

Tactic:
subst hc

Result:
case intro.intro.intro.intro
s : Set Ordinal.{u}
c : Ordinal.{u}
hc' : c ∈ sᶜ
hb' : c ∈ s
ha :
  (∀ (o : Set Ordinal.{u}), IsOpen o → c ∈ o → (o ∩ s).Nonempty) ∧
    ∀ (o : Set Ordinal.{u}), IsOpen o → c ∈ o → (o ∩ sᶜ).Nonempty
h : IsOpen {c}
⊢ False

Proof state:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha :
  (∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ s).Nonempty) ∧
    ∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ sᶜ).Nonempty
h : ¬a.IsLimit
⊢ False

Tactic:
rw [← isOpen_singleton_iff] at h

Result:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha :
  (∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ s).Nonempty) ∧
    ∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ sᶜ).Nonempty
h : IsOpen {a}
⊢ False

Proof state:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : a ∈ frontier s
⊢ a.IsLimit

Tactic:
simp only [frontier_eq_closure_inter_closure, Set.mem_inter_iff, mem_closure_iff] at ha

Result:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha :
  (∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ s).Nonempty) ∧
    ∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ sᶜ).Nonempty
⊢ a.IsLimit

Proof state:
case intro.intro.intro.intro
s : Set Ordinal.{u}
a : Ordinal.{u}
ha :
  (∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ s).Nonempty) ∧
    ∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ sᶜ).Nonempty
h : IsOpen {a}
b : Ordinal.{u}
hb : b = a
hb' : b ∈ s
c : Ordinal.{u}
hc : c = a
hc' : c ∈ sᶜ
⊢ False

Tactic:
subst hb

Result:
case intro.intro.intro.intro
s : Set Ordinal.{u}
b : Ordinal.{u}
hb' : b ∈ s
c : Ordinal.{u}
hc' : c ∈ sᶜ
ha :
  (∀ (o : Set Ordinal.{u}), IsOpen o → b ∈ o → (o ∩ s).Nonempty) ∧
    ∀ (o : Set Ordinal.{u}), IsOpen o → b ∈ o → (o ∩ sᶜ).Nonempty
h : IsOpen {b}
hc : c = b
⊢ False

Proof state:
case intro.intro.intro.intro
s : Set Ordinal.{u}
a : Ordinal.{u}
ha :
  (∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ s).Nonempty) ∧
    ∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ sᶜ).Nonempty
h : IsOpen {a}
b : Ordinal.{u}
hb : b ∈ {a}
hb' : b ∈ s
c : Ordinal.{u}
hc : c ∈ {a}
hc' : c ∈ sᶜ
⊢ False

Tactic:
rw [Set.mem_singleton_iff] at *

Result:
case intro.intro.intro.intro
s : Set Ordinal.{u}
a : Ordinal.{u}
ha :
  (∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ s).Nonempty) ∧
    ∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ sᶜ).Nonempty
h : IsOpen {a}
b : Ordinal.{u}
hb : b = a
hb' : b ∈ s
c : Ordinal.{u}
hc : c = a
hc' : c ∈ sᶜ
⊢ False

Proof state:
case intro.intro.intro.intro
s : Set Ordinal.{u}
c : Ordinal.{u}
hc' : c ∈ sᶜ
hb' : c ∈ s
ha :
  (∀ (o : Set Ordinal.{u}), IsOpen o → c ∈ o → (o ∩ s).Nonempty) ∧
    ∀ (o : Set Ordinal.{u}), IsOpen o → c ∈ o → (o ∩ sᶜ).Nonempty
h : IsOpen {c}
⊢ False

Tactic:
exact hc' hb'

Result:
no goals