-- Mathlib/SetTheory/Ordinal/Topology.lean
theorem accPt_subtype {p o : Ordinal} (S : Set Ordinal) (hpo : p < o) :
    AccPt p (𝓟 S) ↔ AccPt ⟨p, hpo⟩ (𝓟 (Iio o ↓∩ S))

Proof state:
case mpr
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : ∀ U ∈ 𝓝 ⟨p, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨p, hpo⟩
⊢ ∀ U ∈ 𝓝 p, ∃ y ∈ U ∩ S, y ≠ p

Tactic:
intro u hu

Result:
case mpr
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : ∀ U ∈ 𝓝 ⟨p, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨p, hpo⟩
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
⊢ ∃ y ∈ u ∩ S, y ≠ p

Proof state:
case h.right
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : p + 1 < o
ppos : p ≠ 0
h : ¬p.IsLimit
q : Ordinal.{u_1}
hq : p = succ q
y✝ : ↑(Iio o)
mem : y✝ ∈ Ioo ⟨q, ⋯⟩ ⟨p + 1, ho⟩ ∩ Iio o ↓∩ S
aux1 : q < ↑y✝
aux2 : ↑y✝ < p + 1
⊢ ↑y✝ = p

Tactic:
rw [hq] at aux2 ⊢

Result:
case h.right
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : p + 1 < o
ppos : p ≠ 0
h : ¬p.IsLimit
q : Ordinal.{u_1}
hq : p = succ q
y✝ : ↑(Iio o)
mem : y✝ ∈ Ioo ⟨q, ⋯⟩ ⟨p + 1, ho⟩ ∩ Iio o ↓∩ S
aux1 : q < ↑y✝
aux2 : ↑y✝ < succ q + 1
⊢ ↑y✝ = succ q

Proof state:
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : ∀ U ∈ 𝓝 p, ∃ y ∈ U ∩ S, y ≠ p
plim : p.IsLimit
u : Set ↑(Iio o)
hu : u ∈ 𝓝 ⟨p, hpo⟩
l : ↑(Iio o)
hl : l < ⟨p, hpo⟩ ∧ Ioc l ⟨p, hpo⟩ ⊆ u
x : Ordinal.{u_1}
hx : x ∈ Ioo (↑l) (p + 1) ∩ S ∧ x ≠ p
⊢ ⟨x, ⋯⟩ ≤ ⟨p, hpo⟩

Tactic:
exact_mod_cast lt_succ_iff.mp hx.1.1.2

Result:
no goals

Proof state:
case mpr
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : ∀ U ∈ 𝓝 ⟨p, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨p, hpo⟩
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
⊢ ∃ y ∈ u ∩ S, y ≠ p

Tactic:
by_cases ho : p + 1 < o

Result:
case pos
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : ∀ U ∈ 𝓝 ⟨p, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨p, hpo⟩
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : p + 1 < o
⊢ ∃ y ∈ u ∩ S, y ≠ p

case neg
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : ∀ U ∈ 𝓝 ⟨p, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨p, hpo⟩
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : ¬p + 1 < o
⊢ ∃ y ∈ u ∩ S, y ≠ p

Proof state:
case intro
o : Ordinal.{u_1}
S u : Set Ordinal.{u_1}
hpo : 0 < o
h : ∀ U ∈ 𝓝 ⟨0, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨0, hpo⟩
hu : u ∈ 𝓝 0
ho : ¬0 + 1 < o
hp : o = 0 + 1
x : ↑(Iio o)
hx : x ∈ Set.univ ∩ Iio o ↓∩ S ∧ x ≠ ⟨0, hpo⟩
this : ↑x = 0
⊢ False

Tactic:
exact hx.2 (SetCoe.ext this)

Result:
no goals

Proof state:
case h.right
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : p + 1 < o
ppos : p ≠ 0
h : ¬p.IsLimit
q : Ordinal.{u_1}
hq : p = succ q
⊢ ∀ y ∈ Ioo ⟨q, ⋯⟩ ⟨p + 1, ho⟩ ∩ Iio o ↓∩ S, y = ⟨p, hpo⟩

Tactic:
intro _ mem

Result:
case h.right
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : p + 1 < o
ppos : p ≠ 0
h : ¬p.IsLimit
q : Ordinal.{u_1}
hq : p = succ q
y✝ : ↑(Iio o)
mem : y✝ ∈ Ioo ⟨q, ⋯⟩ ⟨p + 1, ho⟩ ∩ Iio o ↓∩ S
⊢ y✝ = ⟨p, hpo⟩

Proof state:
case mpr
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
⊢ AccPt ⟨p, hpo⟩ (𝓟 (Iio o ↓∩ S)) → AccPt p (𝓟 S)

Tactic:
intro h

Result:
case mpr
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : AccPt ⟨p, hpo⟩ (𝓟 (Iio o ↓∩ S))
⊢ AccPt p (𝓟 S)

Proof state:
o : Ordinal.{u_1}
S u : Set Ordinal.{u_1}
hpo : 0 < o
h : ∀ U ∈ 𝓝 ⟨0, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨0, hpo⟩
hu : u ∈ 𝓝 0
ho : 0 + 1 < o
⊢ False

Tactic:
rw [zero_add] at ho

Result:
o : Ordinal.{u_1}
S u : Set Ordinal.{u_1}
hpo : 0 < o
h : ∀ U ∈ 𝓝 ⟨0, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨0, hpo⟩
hu : u ∈ 𝓝 0
ho : 1 < o
⊢ False

Proof state:
case pos.intro.intro
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : ∀ U ∈ 𝓝 ⟨p, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨p, hpo⟩
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : p + 1 < o
ppos : p ≠ 0
plim : p.IsLimit
l : Ordinal.{u_1}
hl : l < p ∧ Ioc l p ⊆ u
x : ↑(Iio o)
hx : x ∈ Ioo ⟨l, ⋯⟩ ⟨p + 1, ho⟩ ∩ Iio o ↓∩ S ∧ x ≠ ⟨p, hpo⟩
⊢ ∃ y ∈ u ∩ S, y ≠ p

Tactic:
use x

Result:
case h
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : ∀ U ∈ 𝓝 ⟨p, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨p, hpo⟩
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : p + 1 < o
ppos : p ≠ 0
plim : p.IsLimit
l : Ordinal.{u_1}
hl : l < p ∧ Ioc l p ⊆ u
x : ↑(Iio o)
hx : x ∈ Ioo ⟨l, ⋯⟩ ⟨p + 1, ho⟩ ∩ Iio o ↓∩ S ∧ x ≠ ⟨p, hpo⟩
⊢ ↑x ∈ u ∩ S ∧ ↑x ≠ p

Proof state:
case intro
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : p + 1 < o
ppos : p ≠ 0
h : ¬p.IsLimit
q : Ordinal.{u_1}
hq : p = succ q
⊢ ∃ U ∈ 𝓝 ⟨p, hpo⟩, ∀ y ∈ U ∩ Iio o ↓∩ S, y = ⟨p, hpo⟩

Tactic:
use (Ioo ⟨q, ((hq ▸ lt_succ q).trans hpo)⟩ ⟨p + 1, ho⟩)

Result:
case h
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : p + 1 < o
ppos : p ≠ 0
h : ¬p.IsLimit
q : Ordinal.{u_1}
hq : p = succ q
⊢ Ioo ⟨q, ⋯⟩ ⟨p + 1, ho⟩ ∈ 𝓝 ⟨p, hpo⟩ ∧ ∀ y ∈ Ioo ⟨q, ⋯⟩ ⟨p + 1, ho⟩ ∩ Iio o ↓∩ S, y = ⟨p, hpo⟩

Proof state:
case h.right
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : p + 1 < o
ppos : p ≠ 0
h : ¬p.IsLimit
q : Ordinal.{u_1}
hq : p = succ q
y✝ : ↑(Iio o)
mem : y✝ ∈ Ioo ⟨q, ⋯⟩ ⟨p + 1, ho⟩ ∩ Iio o ↓∩ S
aux1 : q < ↑y✝
⊢ y✝ = ⟨p, hpo⟩

Tactic:
have aux2 := Subtype.mk_lt_mk.mp mem.1.2

Result:
case h.right
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : p + 1 < o
ppos : p ≠ 0
h : ¬p.IsLimit
q : Ordinal.{u_1}
hq : p = succ q
y✝ : ↑(Iio o)
mem : y✝ ∈ Ioo ⟨q, ⋯⟩ ⟨p + 1, ho⟩ ∩ Iio o ↓∩ S
aux1 : q < ↑y✝
aux2 : ↑y✝ < p + 1
⊢ y✝ = ⟨p, hpo⟩

Proof state:
case mp
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : AccPt p (𝓟 S)
plim : p.IsLimit
⊢ AccPt ⟨p, hpo⟩ (𝓟 (Iio o ↓∩ S))

Tactic:
rw [accPt_iff_nhds] at *

Result:
case mp
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : ∀ U ∈ 𝓝 p, ∃ y ∈ U ∩ S, y ≠ p
plim : p.IsLimit
⊢ ∀ U ∈ 𝓝 ⟨p, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨p, hpo⟩

Proof state:
case h
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : ∀ U ∈ 𝓝 ⟨p, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨p, hpo⟩
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : p + 1 < o
ppos : p ≠ 0
plim : p.IsLimit
l : Ordinal.{u_1}
hl : l < p ∧ Ioc l p ⊆ u
x : ↑(Iio o)
hx : x ∈ Ioo ⟨l, ⋯⟩ ⟨p + 1, ho⟩ ∩ Iio o ↓∩ S ∧ x ≠ ⟨p, hpo⟩
⊢ ↑x ∈ u ∩ S ∧ ↑x ≠ p

Tactic:
exact ⟨⟨hl.2 ⟨hx.1.1.1, lt_succ_iff.mp hx.1.1.2⟩, hx.1.2⟩, fun h ↦ hx.2 (SetCoe.ext h)⟩

Result:
no goals

Proof state:
case h
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : ∀ U ∈ 𝓝 p, ∃ y ∈ U ∩ S, y ≠ p
plim : p.IsLimit
u : Set ↑(Iio o)
hu : u ∈ 𝓝 ⟨p, hpo⟩
l : ↑(Iio o)
hl : l < ⟨p, hpo⟩ ∧ Ioc l ⟨p, hpo⟩ ⊆ u
x : Ordinal.{u_1}
hx : x ∈ Ioo (↑l) (p + 1) ∩ S ∧ x ≠ p
⊢ ⟨x, ⋯⟩ ∈ u ∩ Iio o ↓∩ S

Tactic:
exact ⟨hl.2 ⟨hx.1.1.1, by exact_mod_cast lt_succ_iff.mp hx.1.1.2⟩, hx.1.2⟩

Result:
no goals

Proof state:
case intro
o : Ordinal.{u_1}
S u : Set Ordinal.{u_1}
hpo : 0 < o
h : ∀ U ∈ 𝓝 ⟨0, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨0, hpo⟩
hu : u ∈ 𝓝 0
ho : ¬0 + 1 < o
hp : o = 0 + 1
x : ↑(Iio o)
hx : x ∈ Set.univ ∩ Iio o ↓∩ S ∧ x ≠ ⟨0, hpo⟩
this : ↑x < o
⊢ False

Tactic:
simp_rw [hp, zero_add, lt_one_iff_zero] at this

Result:
case intro
o : Ordinal.{u_1}
S u : Set Ordinal.{u_1}
hpo : 0 < o
h : ∀ U ∈ 𝓝 ⟨0, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨0, hpo⟩
hu : u ∈ 𝓝 0
ho : ¬0 + 1 < o
hp : o = 0 + 1
x : ↑(Iio o)
hx : x ∈ Set.univ ∩ Iio o ↓∩ S ∧ x ≠ ⟨0, hpo⟩
this : ↑x = 0
⊢ False

Proof state:
case pos
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : ∀ U ∈ 𝓝 ⟨p, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨p, hpo⟩
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : p + 1 < o
⊢ ∃ y ∈ u ∩ S, y ≠ p

Tactic:
have ppos : p ≠ 0 := by
  rintro rfl
  rw [zero_add] at ho
  specialize h (Iio ⟨1, ho⟩) (Iio_mem_nhds (Subtype.mk_lt_mk.mpr zero_lt_one))
  obtain ⟨_, h⟩ := h
  exact h.2 <| Subtype.mk_eq_mk.mpr (lt_one_iff_zero.mp h.1.1)

Result:
case pos
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : ∀ U ∈ 𝓝 ⟨p, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨p, hpo⟩
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : p + 1 < o
ppos : p ≠ 0
⊢ ∃ y ∈ u ∩ S, y ≠ p