-- Mathlib/SetTheory/Ordinal/Topology.lean
theorem isAcc_iff (o : Ordinal) (S : Set Ordinal) : o.IsAcc S ↔
    o ≠ 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty

Proof state:
case h
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
p : Ordinal.{u_1}
plt : p < o
x : Ordinal.{u_1}
hx : x ∈ Ioo p (o + 1) ∩ S ∧ x ≠ o
⊢ x ∈ S ∩ Ioo p o

Tactic:
refine ⟨hx.1.2, ⟨hx.1.1.1, lt_of_le_of_ne ?_ hx.2⟩⟩

Result:
case h
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
p : Ordinal.{u_1}
plt : p < o
x : Ordinal.{u_1}
hx : x ∈ Ioo p (o + 1) ∩ S ∧ x ≠ o
⊢ x ≤ o

Proof state:
case mp.left.intro
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 0, ∃ y ∈ U ∩ S, y ≠ 0
x : Ordinal.{u_1}
hx : x ∈ Iio 1 ∩ S ∧ x ≠ 0
⊢ False

Tactic:
exact hx.2 <| lt_one_iff_zero.mp hx.1.1

Result:
no goals

Proof state:
case mpr.intro.intro
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
u : Set Ordinal.{u_1}
umem : u ∈ 𝓝 o
l : Ordinal.{u_1}
hl : l < o ∧ Ioc l o ⊆ u
x : Ordinal.{u_1}
hx : x ∈ S ∩ Ioo l o
⊢ ∃ y ∈ u ∩ S, y ≠ o

Tactic:
use x

Result:
case h
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
u : Set Ordinal.{u_1}
umem : u ∈ 𝓝 o
l : Ordinal.{u_1}
hl : l < o ∧ Ioc l o ⊆ u
x : Ordinal.{u_1}
hx : x ∈ S ∩ Ioo l o
⊢ x ∈ u ∩ S ∧ x ≠ o

Proof state:
case mp
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
⊢ ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty

Tactic:
constructor

Result:
case mp.left
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
⊢ ¬o = 0

case mp.right
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
⊢ ∀ p < o, (S ∩ Ioo p o).Nonempty

Proof state:
case mp.left
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 0, ∃ y ∈ U ∩ S, y ≠ 0
⊢ False

Tactic:
obtain ⟨x, hx⟩ := h (Iio 1) (Iio_mem_nhds zero_lt_one)

Result:
case mp.left.intro
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 0, ∃ y ∈ U ∩ S, y ≠ 0
x : Ordinal.{u_1}
hx : x ∈ Iio 1 ∩ S ∧ x ≠ 0
⊢ False

Proof state:
case h
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
p : Ordinal.{u_1}
plt : p < o
x : Ordinal.{u_1}
hx : x ∈ Ioo p (o + 1) ∩ S ∧ x ≠ o
this : x < o + 1
⊢ x ≤ o

Tactic:
rwa [← succ_eq_add_one, lt_succ_iff] at this

Result:
no goals

Proof state:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
⊢ AccPt o (𝓟 S) ↔ ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty

Tactic:
constructor

Result:
case mp
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
⊢ AccPt o (𝓟 S) → ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty

case mpr
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
⊢ (¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty) → AccPt o (𝓟 S)

Proof state:
case mpr
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
⊢ (¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty) → AccPt o (𝓟 S)

Tactic:
rw [accPt_iff_nhds]

Result:
case mpr
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
⊢ (¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty) → ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o

Proof state:
case mpr.intro
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
u : Set Ordinal.{u_1}
umem : u ∈ 𝓝 o
l : Ordinal.{u_1}
hl : l < o ∧ Ioc l o ⊆ u
⊢ ∃ y ∈ u ∩ S, y ≠ o

Tactic:
obtain ⟨x, hx⟩ := h.2 l hl.1

Result:
case mpr.intro.intro
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
u : Set Ordinal.{u_1}
umem : u ∈ 𝓝 o
l : Ordinal.{u_1}
hl : l < o ∧ Ioc l o ⊆ u
x : Ordinal.{u_1}
hx : x ∈ S ∩ Ioo l o
⊢ ∃ y ∈ u ∩ S, y ≠ o

Proof state:
case h
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
p : Ordinal.{u_1}
plt : p < o
x : Ordinal.{u_1}
hx : x ∈ Ioo p (o + 1) ∩ S ∧ x ≠ o
⊢ x ≤ o

Tactic:
have := hx.1.1.2

Result:
case h
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
p : Ordinal.{u_1}
plt : p < o
x : Ordinal.{u_1}
hx : x ∈ Ioo p (o + 1) ∩ S ∧ x ≠ o
this : x < o + 1
⊢ x ≤ o

Proof state:
case mp
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
⊢ (∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o) → ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty

Tactic:
intro h

Result:
case mp
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
⊢ ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty

Proof state:
case h
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
u : Set Ordinal.{u_1}
umem : u ∈ 𝓝 o
l : Ordinal.{u_1}
hl : l < o ∧ Ioc l o ⊆ u
x : Ordinal.{u_1}
hx : x ∈ S ∩ Ioo l o
⊢ x ∈ u ∩ S ∧ x ≠ o

Tactic:
exact ⟨⟨hl.2 ⟨hx.2.1, hx.2.2.le⟩, hx.1⟩, hx.2.2.ne⟩

Result:
no goals

Proof state:
case mp.left
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
⊢ ¬o = 0

Tactic:
rintro rfl

Result:
case mp.left
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 0, ∃ y ∈ U ∩ S, y ≠ 0
⊢ False

Proof state:
case mpr
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
⊢ (¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty) → ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o

Tactic:
intro h u umem

Result:
case mpr
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
u : Set Ordinal.{u_1}
umem : u ∈ 𝓝 o
⊢ ∃ y ∈ u ∩ S, y ≠ o

Proof state:
case mpr
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
u : Set Ordinal.{u_1}
umem : u ∈ 𝓝 o
⊢ ∃ y ∈ u ∩ S, y ≠ o

Tactic:
obtain ⟨l, hl⟩ := exists_Ioc_subset_of_mem_nhds umem ⟨0, Ordinal.pos_iff_ne_zero.mpr h.1⟩

Result:
case mpr.intro
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
u : Set Ordinal.{u_1}
umem : u ∈ 𝓝 o
l : Ordinal.{u_1}
hl : l < o ∧ Ioc l o ⊆ u
⊢ ∃ y ∈ u ∩ S, y ≠ o

Proof state:
case mp.right
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
p : Ordinal.{u_1}
plt : p < o
⊢ (S ∩ Ioo p o).Nonempty

Tactic:
obtain ⟨x, hx⟩ := h (Ioo p (o + 1)) <| Ioo_mem_nhds plt (lt_succ o)

Result:
case mp.right.intro
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
p : Ordinal.{u_1}
plt : p < o
x : Ordinal.{u_1}
hx : x ∈ Ioo p (o + 1) ∩ S ∧ x ≠ o
⊢ (S ∩ Ioo p o).Nonempty

Proof state:
case mp
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
⊢ AccPt o (𝓟 S) → ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty

Tactic:
rw [accPt_iff_nhds]

Result:
case mp
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
⊢ (∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o) → ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty

Proof state:
case mp.right.intro
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
p : Ordinal.{u_1}
plt : p < o
x : Ordinal.{u_1}
hx : x ∈ Ioo p (o + 1) ∩ S ∧ x ≠ o
⊢ (S ∩ Ioo p o).Nonempty

Tactic:
use x

Result:
case h
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
p : Ordinal.{u_1}
plt : p < o
x : Ordinal.{u_1}
hx : x ∈ Ioo p (o + 1) ∩ S ∧ x ≠ o
⊢ x ∈ S ∩ Ioo p o

Proof state:
case mp.right
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
⊢ ∀ p < o, (S ∩ Ioo p o).Nonempty

Tactic:
intro p plt

Result:
case mp.right
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
p : Ordinal.{u_1}
plt : p < o
⊢ (S ∩ Ioo p o).Nonempty

Proof state:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
⊢ o.IsAcc S ↔ o ≠ 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty

Tactic:
dsimp [IsAcc]

Result:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
⊢ AccPt o (𝓟 S) ↔ ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty