-- 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)
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, ⋯⟩
this : enumOrd s (⨆ i, g i) = ⨆ i, f i
⊢ ⨆ i, f i ∈ s

Tactic:
rw [← this]

Result:
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, ⋯⟩
this : enumOrd s (⨆ i, g i) = ⨆ i, f i
⊢ enumOrd s (⨆ i, g i) ∈ s

Proof state:
case refine_1.e_s.h
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, ⋯⟩
x : ι
⊢ enumOrd s (g x) = f x

Tactic:
change (enumOrdOrderIso s hs _).val = f x

Result:
case refine_1.e_s.h
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, ⋯⟩
x : ι
⊢ ↑((enumOrdOrderIso s hs) (g x)) = f x

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
⊢ ⨆ i, f i ∈ s

Tactic:
let g : ι → Ordinal.{u} := fun i => (enumOrdOrderIso s hs).symm ⟨_, hf i⟩

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, ⋯⟩
⊢ ⨆ i, f i ∈ s

Proof state:
case refine_1.e_s
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, ⋯⟩
⊢ (fun i => enumOrd s (g i)) = fun i => f i

Tactic:
ext x

Result:
case refine_1.e_s.h
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, ⋯⟩
x : ι
⊢ enumOrd s (g x) = f x

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, enumOrd s (g i) = ⨆ i, f i

Tactic:
congr

Result:
case refine_1.e_s
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, ⋯⟩
⊢ (fun i => enumOrd s (g i)) = fun i => f i

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
⊢ False

Tactic:
apply (Hs (lt_succ b)).not_le

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
⊢ enumOrd s (succ b) ≤ enumOrd s b

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 ≤ o

Tactic:
suffices enumOrd s a ≤ bsup.{u, u} a fun b (_ : b < a) => enumOrd s b from
  this.trans (bsup_le H)

Result:
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

Proof state:
case refine_1.e_s.h
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, ⋯⟩
x : ι
⊢ ↑((enumOrdOrderIso s hs) (g x)) = f x

Tactic:
rw [OrderIso.apply_symm_apply]

Result:
no goals

Proof state:
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

Tactic:
rw [isClosed_iff_bsup] at h

Result:
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 ≤ o

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, ⋯⟩
⊢ enumOrd s (⨆ i, g i) = ⨆ i, f i

Tactic:
rw [IsNormal.map_iSup h g]

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, ⋯⟩
⊢ ⨆ i, enumOrd s (g i) = ⨆ i, f i

Proof state:
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, ⋯⟩
this : enumOrd s (⨆ i, g i) = ⨆ i, f i
⊢ enumOrd s (⨆ i, g i) ∈ s

Tactic:
exact enumOrd_mem hs _

Result:
no goals

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) ≤ enumOrd s b

Tactic:
rw [hb]

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
⊢ enumOrd s (succ b) ≤ a.bsup fun b x => enumOrd s b