-- Mathlib/SetTheory/Ordinal/Topology.lean
theorem enumOrd_isNormal_iff_isClosed (hs : ¬ BddAbove s) :
    IsNormal (enumOrd s) ↔ IsClosed s

Proof state:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
⊢ IsNormal (enumOrd s) ↔ IsClosed s

Tactic:
refine
  ⟨fun h => isClosed_iff_iSup.2 fun {ι} hι f hf => ?_, fun h =>
    (isNormal_iff_strictMono_limit _).2 ⟨Hs, fun a ha o H => ?_⟩⟩

Result:
case refine_1
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsNormal (enumOrd s)
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
⊢ ⨆ i, f i ∈ s

case refine_2
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal.{u}
ha : a.IsLimit
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
⊢ enumOrd s a ≤ o

Proof state:
case refine_2
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal.{u}},
    o ≠ 0 →
      ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s
a : Ordinal.{u}
ha : a.IsLimit
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
⊢ enumOrd s a ≤ a.bsup fun b x => enumOrd s b

Tactic:
obtain ⟨b, hb⟩ := enumOrd_surjective hs (h ha.ne_zero (fun b _ => enumOrd s b)
  fun b _ => enumOrd_mem hs b)

Result:
case refine_2.intro
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal.{u}},
    o ≠ 0 →
      ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s
a : Ordinal.{u}
ha : a.IsLimit
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
b : Ordinal.{u}
hb : enumOrd s b = a.bsup fun b x => enumOrd s b
⊢ enumOrd s a ≤ a.bsup fun b x => enumOrd s b

Proof state:
case refine_2.intro.a
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal.{u}},
    o ≠ 0 →
      ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s
a : Ordinal.{u}
ha : a.IsLimit
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
b : Ordinal.{u}
hb : enumOrd s b = a.bsup fun b x => enumOrd s b
⊢ a ≤ b

Tactic:
by_contra! hba

Result:
case refine_2.intro.a
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal.{u}},
    o ≠ 0 →
      ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s
a : Ordinal.{u}
ha : a.IsLimit
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
b : Ordinal.{u}
hb : enumOrd s b = a.bsup fun b x => enumOrd s b
hba : b < a
⊢ False

Proof state:
case refine_2.intro.a
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal.{u}},
    o ≠ 0 →
      ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s
a : Ordinal.{u}
ha : a.IsLimit
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
b : Ordinal.{u}
hb : enumOrd s b = a.bsup fun b x => enumOrd s b
hba : b < a
⊢ enumOrd s (succ b) ≤ a.bsup fun b x => enumOrd s b

Tactic:
exact le_bsup.{u, u} _ _ (ha.succ_lt hba)

Result:
no goals

Proof state:
case refine_1
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsNormal (enumOrd s)
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal.{u} := fun i => (enumOrdOrderIso s hs).symm ⟨f i, ⋯⟩
⊢ ⨆ i, f i ∈ s

Tactic:
suffices enumOrd s (⨆ i, g i) = ⨆ i, f i by
  rw [← this]
  exact enumOrd_mem hs _

Result:
case refine_1
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsNormal (enumOrd s)
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal.{u} := fun i => (enumOrdOrderIso s hs).symm ⟨f i, ⋯⟩
⊢ enumOrd s (⨆ i, g i) = ⨆ i, f i

Proof state:
case refine_2.intro
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal.{u}},
    o ≠ 0 →
      ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s
a : Ordinal.{u}
ha : a.IsLimit
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
b : Ordinal.{u}
hb : enumOrd s b = a.bsup fun b x => enumOrd s b
⊢ enumOrd s a ≤ a.bsup fun b x => enumOrd s b

Tactic:
rw [← hb]

Result:
case refine_2.intro
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal.{u}},
    o ≠ 0 →
      ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s
a : Ordinal.{u}
ha : a.IsLimit
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
b : Ordinal.{u}
hb : enumOrd s b = a.bsup fun b x => enumOrd s b
⊢ enumOrd s a ≤ enumOrd s b

Proof state:
s : Set Ordinal.{u}
hs : ¬BddAbove s
⊢ IsNormal (enumOrd s) ↔ IsClosed s

Tactic:
have Hs := enumOrd_strictMono hs

Result:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
⊢ IsNormal (enumOrd s) ↔ IsClosed s

Proof state:
case refine_2.intro
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal.{u}},
    o ≠ 0 →
      ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s
a : Ordinal.{u}
ha : a.IsLimit
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
b : Ordinal.{u}
hb : enumOrd s b = a.bsup fun b x => enumOrd s b
⊢ enumOrd s a ≤ enumOrd s b

Tactic:
apply Hs.monotone

Result:
case refine_2.intro.a
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h :
  ∀ {o : Ordinal.{u}},
    o ≠ 0 →
      ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s
a : Ordinal.{u}
ha : a.IsLimit
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
b : Ordinal.{u}
hb : enumOrd s b = a.bsup fun b x => enumOrd s b
⊢ a ≤ b