-- Mathlib/SetTheory/Ordinal/Topology.lean
theorem isClosedBelow_iff {S : Set Ordinal} {o : Ordinal} : IsClosedBelow S o ↔
    ∀ p < o, IsAcc p S → p ∈ S

Proof state:
case mpr
S : Set Ordinal.{u_1}
o : Ordinal.{u_1}
h : ∀ p < o, p.IsAcc S → p ∈ S
⊢ IsClosed (Iio o ↓∩ S)

Tactic:
rw [isClosed_iff_clusterPt]

Result:
case mpr
S : Set Ordinal.{u_1}
o : Ordinal.{u_1}
h : ∀ p < o, p.IsAcc S → p ∈ S
⊢ ∀ (a : ↑(Iio o)), ClusterPt a (𝓟 (Iio o ↓∩ S)) → a ∈ Iio o ↓∩ S

Proof state:
S : Set Ordinal.{u_1}
o : Ordinal.{u_1}
h : ∀ p < o, p.IsAcc S → p ∈ S
r : ↑(Iio o)
hr : ClusterPt r (𝓟 (Iio o ↓∩ S))
h' : AccPt r (𝓟 (Iio o ↓∩ S))
⊢ r ∈ Iio o ↓∩ S

Tactic:
exact h r.1 r.2 <| (accPt_subtype _ _).mpr h'

Result:
no goals

Proof state:
S : Set Ordinal.{u_1}
o : Ordinal.{u_1}
⊢ IsClosed (Iio o ↓∩ S) ↔ ∀ p < o, p.IsAcc S → p ∈ S

Tactic:
constructor

Result:
case mp
S : Set Ordinal.{u_1}
o : Ordinal.{u_1}
⊢ IsClosed (Iio o ↓∩ S) → ∀ p < o, p.IsAcc S → p ∈ S

case mpr
S : Set Ordinal.{u_1}
o : Ordinal.{u_1}
⊢ (∀ p < o, p.IsAcc S → p ∈ S) → IsClosed (Iio o ↓∩ S)

Proof state:
case mp
S : Set Ordinal.{u_1}
o : Ordinal.{u_1}
h : IsClosed (Iio o ↓∩ S)
p : Ordinal.{u_1}
plto : p < o
hp : p.IsAcc S
this : AccPt ⟨p, plto⟩ (𝓟 (Iio o ↓∩ S))
⊢ p ∈ S

Tactic:
rw [isClosed_iff_clusterPt] at h

Result:
case mp
S : Set Ordinal.{u_1}
o : Ordinal.{u_1}
h : ∀ (a : ↑(Iio o)), ClusterPt a (𝓟 (Iio o ↓∩ S)) → a ∈ Iio o ↓∩ S
p : Ordinal.{u_1}
plto : p < o
hp : p.IsAcc S
this : AccPt ⟨p, plto⟩ (𝓟 (Iio o ↓∩ S))
⊢ p ∈ S

Proof state:
case mp
S : Set Ordinal.{u_1}
o : Ordinal.{u_1}
h : IsClosed (Iio o ↓∩ S)
p : Ordinal.{u_1}
plto : p < o
hp : p.IsAcc S
⊢ p ∈ S

Tactic:
have : AccPt ⟨p, plto⟩ (𝓟 (Iio o ↓∩ S)) := (accPt_subtype _ _).mp hp

Result:
case mp
S : Set Ordinal.{u_1}
o : Ordinal.{u_1}
h : IsClosed (Iio o ↓∩ S)
p : Ordinal.{u_1}
plto : p < o
hp : p.IsAcc S
this : AccPt ⟨p, plto⟩ (𝓟 (Iio o ↓∩ S))
⊢ p ∈ S

Proof state:
case mpr
S : Set Ordinal.{u_1}
o : Ordinal.{u_1}
h : ∀ p < o, p.IsAcc S → p ∈ S
r : ↑(Iio o)
hr : ClusterPt r (𝓟 (Iio o ↓∩ S))
⊢ r ∈ Iio o ↓∩ S

Tactic:
match clusterPt_principal.mp hr with
| .inl h => exact h
| .inr h' => exact h r.1 r.2 <| (accPt_subtype _ _).mpr h'

Result:
no goals

Proof state:
case mpr
S : Set Ordinal.{u_1}
o : Ordinal.{u_1}
h : ∀ p < o, p.IsAcc S → p ∈ S
⊢ ∀ (a : ↑(Iio o)), ClusterPt a (𝓟 (Iio o ↓∩ S)) → a ∈ Iio o ↓∩ S

Tactic:
intro r hr

Result:
case mpr
S : Set Ordinal.{u_1}
o : Ordinal.{u_1}
h : ∀ p < o, p.IsAcc S → p ∈ S
r : ↑(Iio o)
hr : ClusterPt r (𝓟 (Iio o ↓∩ S))
⊢ r ∈ Iio o ↓∩ S

Proof state:
case mp
S : Set Ordinal.{u_1}
o : Ordinal.{u_1}
h : ∀ (a : ↑(Iio o)), ClusterPt a (𝓟 (Iio o ↓∩ S)) → a ∈ Iio o ↓∩ S
p : Ordinal.{u_1}
plto : p < o
hp : p.IsAcc S
this : AccPt ⟨p, plto⟩ (𝓟 (Iio o ↓∩ S))
⊢ p ∈ S

Tactic:
exact h ⟨p, plto⟩ this.clusterPt

Result:
no goals

Proof state:
case mpr
S : Set Ordinal.{u_1}
o : Ordinal.{u_1}
⊢ (∀ p < o, p.IsAcc S → p ∈ S) → IsClosed (Iio o ↓∩ S)

Tactic:
intro h

Result:
case mpr
S : Set Ordinal.{u_1}
o : Ordinal.{u_1}
h : ∀ p < o, p.IsAcc S → p ∈ S
⊢ IsClosed (Iio o ↓∩ S)

Proof state:
S : Set Ordinal.{u_1}
o : Ordinal.{u_1}
h✝ : ∀ p < o, p.IsAcc S → p ∈ S
r : ↑(Iio o)
hr : ClusterPt r (𝓟 (Iio o ↓∩ S))
h : r ∈ Iio o ↓∩ S
⊢ r ∈ Iio o ↓∩ S

Tactic:
exact h

Result:
no goals

Proof state:
S : Set Ordinal.{u_1}
o : Ordinal.{u_1}
⊢ IsClosedBelow S o ↔ ∀ p < o, p.IsAcc S → p ∈ S

Tactic:
dsimp [IsClosedBelow]

Result:
S : Set Ordinal.{u_1}
o : Ordinal.{u_1}
⊢ IsClosed (Iio o ↓∩ S) ↔ ∀ p < o, p.IsAcc S → p ∈ S

Proof state:
case mp
S : Set Ordinal.{u_1}
o : Ordinal.{u_1}
⊢ IsClosed (Iio o ↓∩ S) → ∀ p < o, p.IsAcc S → p ∈ S

Tactic:
intro h p plto hp

Result:
case mp
S : Set Ordinal.{u_1}
o : Ordinal.{u_1}
h : IsClosed (Iio o ↓∩ S)
p : Ordinal.{u_1}
plto : p < o
hp : p.IsAcc S
⊢ p ∈ S