-- Mathlib/SetTheory/Ordinal/Topology.lean
theorem isNormal_iff_strictMono_and_continuous (f : Ordinal.{u} → Ordinal.{u}) :
    IsNormal f ↔ StrictMono f ∧ Continuous f

Proof state:
case refine_2.intro
f : Ordinal.{u} → Ordinal.{u}
h✝ : StrictMono f
h' : Continuous f
o : Ordinal.{u}
ho : o.IsLimit
a : Ordinal.{u}
h : ∀ b < o, f b ≤ a
⊢ o ∈ f ⁻¹' Set.Iic a

Tactic:
rw [mem_iff_iSup_of_isClosed (IsClosed.preimage h' (@isClosed_Iic _ _ _ _ a))]

Result:
case refine_2.intro
f : Ordinal.{u} → Ordinal.{u}
h✝ : StrictMono f
h' : Continuous f
o : Ordinal.{u}
ho : o.IsLimit
a : Ordinal.{u}
h : ∀ b < o, f b ≤ a
⊢ ∃ ι, ∃ (_ : Nonempty ι), ∃ f_1, (∀ (i : ι), f_1 i ∈ f ⁻¹' Set.Iic a) ∧ ⨆ i, f_1 i = o

Proof state:
case refine_1
f : Ordinal.{u} → Ordinal.{u}
h : IsNormal f
⊢ Continuous f

Tactic:
rw [continuous_def]

Result:
case refine_1
f : Ordinal.{u} → Ordinal.{u}
h : IsNormal f
⊢ ∀ (s : Set Ordinal.{u}), IsOpen s → IsOpen (f ⁻¹' s)

Proof state:
case refine_1.intro.intro.intro.intro
f : Ordinal.{u} → Ordinal.{u}
h : IsNormal f
s : Set Ordinal.{u}
hs : ∀ o ∈ s, o.IsLimit → ∃ a < o, Set.Ioo a o ⊆ s
o : Ordinal.{u}
ho : o ∈ f ⁻¹' s
ho' : o.IsLimit
a : Ordinal.{u}
has : Set.Ioo a (f o) ⊆ s
b : Ordinal.{u}
hb : b < o
hab : a < f b
⊢ ∃ a < o, Set.Ioo a o ⊆ f ⁻¹' s

Tactic:
exact
  ⟨b, hb, fun c hc =>
    Set.mem_preimage.2 (has ⟨hab.trans (h.strictMono hc.1), h.strictMono hc.2⟩)⟩

Result:
no goals

Proof state:
case refine_1
f : Ordinal.{u} → Ordinal.{u}
h : IsNormal f
⊢ ∀ (s : Set Ordinal.{u}), IsOpen s → IsOpen (f ⁻¹' s)

Tactic:
intro s hs

Result:
case refine_1
f : Ordinal.{u} → Ordinal.{u}
h : IsNormal f
s : Set Ordinal.{u}
hs : IsOpen s
⊢ IsOpen (f ⁻¹' s)

Proof state:
case refine_1.intro.intro
f : Ordinal.{u} → Ordinal.{u}
h : IsNormal f
s : Set Ordinal.{u}
hs : ∀ o ∈ s, o.IsLimit → ∃ a < o, Set.Ioo a o ⊆ s
o : Ordinal.{u}
ho : o ∈ f ⁻¹' s
ho' : o.IsLimit
a : Ordinal.{u}
ha : a < f o
has : Set.Ioo a (f o) ⊆ s
⊢ ∃ a < o, Set.Ioo a o ⊆ f ⁻¹' s

Tactic:
rw [← IsNormal.bsup_eq.{u, u} h ho', lt_bsup] at ha

Result:
case refine_1.intro.intro
f : Ordinal.{u} → Ordinal.{u}
h : IsNormal f
s : Set Ordinal.{u}
hs : ∀ o ∈ s, o.IsLimit → ∃ a < o, Set.Ioo a o ⊆ s
o : Ordinal.{u}
ho : o ∈ f ⁻¹' s
ho' : o.IsLimit
a : Ordinal.{u}
ha : ∃ i, ∃ (_ : i < o), a < f i
has : Set.Ioo a (f o) ⊆ s
⊢ ∃ a < o, Set.Ioo a o ⊆ f ⁻¹' s

Proof state:
case refine_1
f : Ordinal.{u} → Ordinal.{u}
h : IsNormal f
s : Set Ordinal.{u}
hs : ∀ o ∈ s, o.IsLimit → ∃ a < o, Set.Ioo a o ⊆ s
o : Ordinal.{u}
ho : o ∈ f ⁻¹' s
ho' : o.IsLimit
⊢ ∃ a < o, Set.Ioo a o ⊆ f ⁻¹' s

Tactic:
rcases hs _ ho (h.isLimit ho') with ⟨a, ha, has⟩

Result:
case refine_1.intro.intro
f : Ordinal.{u} → Ordinal.{u}
h : IsNormal f
s : Set Ordinal.{u}
hs : ∀ o ∈ s, o.IsLimit → ∃ a < o, Set.Ioo a o ⊆ s
o : Ordinal.{u}
ho : o ∈ f ⁻¹' s
ho' : o.IsLimit
a : Ordinal.{u}
ha : a < f o
has : Set.Ioo a (f o) ⊆ s
⊢ ∃ a < o, Set.Ioo a o ⊆ f ⁻¹' s

Proof state:
case refine_1
f : Ordinal.{u} → Ordinal.{u}
h : IsNormal f
s : Set Ordinal.{u}
hs : IsOpen s
⊢ IsOpen (f ⁻¹' s)

Tactic:
rw [isOpen_iff] at *

Result:
case refine_1
f : Ordinal.{u} → Ordinal.{u}
h : IsNormal f
s : Set Ordinal.{u}
hs : ∀ o ∈ s, o.IsLimit → ∃ a < o, Set.Ioo a o ⊆ s
⊢ ∀ o ∈ f ⁻¹' s, o.IsLimit → ∃ a < o, Set.Ioo a o ⊆ f ⁻¹' s

Proof state:
case refine_2.intro
f : Ordinal.{u} → Ordinal.{u}
h✝ : StrictMono f
h' : Continuous f
o : Ordinal.{u}
ho : o.IsLimit
a : Ordinal.{u}
h : ∀ b < o, f b ≤ a
⊢ f o ≤ a

Tactic:
suffices o ∈ f ⁻¹' Set.Iic a from Set.mem_preimage.1 this

Result:
case refine_2.intro
f : Ordinal.{u} → Ordinal.{u}
h✝ : StrictMono f
h' : Continuous f
o : Ordinal.{u}
ho : o.IsLimit
a : Ordinal.{u}
h : ∀ b < o, f b ≤ a
⊢ o ∈ f ⁻¹' Set.Iic a

Proof state:
f : Ordinal.{u} → Ordinal.{u}
⊢ IsNormal f ↔ StrictMono f ∧ Continuous f

Tactic:
refine ⟨fun h => ⟨h.strictMono, ?_⟩, ?_⟩

Result:
case refine_1
f : Ordinal.{u} → Ordinal.{u}
h : IsNormal f
⊢ Continuous f

case refine_2
f : Ordinal.{u} → Ordinal.{u}
⊢ StrictMono f ∧ Continuous f → IsNormal f

Proof state:
case refine_2
f : Ordinal.{u} → Ordinal.{u}
⊢ StrictMono f ∧ Continuous f → IsNormal f

Tactic:
rw [isNormal_iff_strictMono_limit]

Result:
case refine_2
f : Ordinal.{u} → Ordinal.{u}
⊢ StrictMono f ∧ Continuous f →
    StrictMono f ∧ ∀ (o : Ordinal.{u}), o.IsLimit → ∀ (a : Ordinal.{u}), (∀ b < o, f b ≤ a) → f o ≤ a

Proof state:
case refine_2.intro
f : Ordinal.{u} → Ordinal.{u}
h : StrictMono f
h' : Continuous f
⊢ StrictMono f ∧ ∀ (o : Ordinal.{u}), o.IsLimit → ∀ (a : Ordinal.{u}), (∀ b < o, f b ≤ a) → f o ≤ a

Tactic:
refine ⟨h, fun o ho a h => ?_⟩

Result:
case refine_2.intro
f : Ordinal.{u} → Ordinal.{u}
h✝ : StrictMono f
h' : Continuous f
o : Ordinal.{u}
ho : o.IsLimit
a : Ordinal.{u}
h : ∀ b < o, f b ≤ a
⊢ f o ≤ a

Proof state:
case refine_1.intro.intro
f : Ordinal.{u} → Ordinal.{u}
h : IsNormal f
s : Set Ordinal.{u}
hs : ∀ o ∈ s, o.IsLimit → ∃ a < o, Set.Ioo a o ⊆ s
o : Ordinal.{u}
ho : o ∈ f ⁻¹' s
ho' : o.IsLimit
a : Ordinal.{u}
ha : ∃ i, ∃ (_ : i < o), a < f i
has : Set.Ioo a (f o) ⊆ s
⊢ ∃ a < o, Set.Ioo a o ⊆ f ⁻¹' s

Tactic:
rcases ha with ⟨b, hb, hab⟩

Result:
case refine_1.intro.intro.intro.intro
f : Ordinal.{u} → Ordinal.{u}
h : IsNormal f
s : Set Ordinal.{u}
hs : ∀ o ∈ s, o.IsLimit → ∃ a < o, Set.Ioo a o ⊆ s
o : Ordinal.{u}
ho : o ∈ f ⁻¹' s
ho' : o.IsLimit
a : Ordinal.{u}
has : Set.Ioo a (f o) ⊆ s
b : Ordinal.{u}
hb : b < o
hab : a < f b
⊢ ∃ a < o, Set.Ioo a o ⊆ f ⁻¹' s

Proof state:
case refine_1
f : Ordinal.{u} → Ordinal.{u}
h : IsNormal f
s : Set Ordinal.{u}
hs : ∀ o ∈ s, o.IsLimit → ∃ a < o, Set.Ioo a o ⊆ s
⊢ ∀ o ∈ f ⁻¹' s, o.IsLimit → ∃ a < o, Set.Ioo a o ⊆ f ⁻¹' s

Tactic:
intro o ho ho'

Result:
case refine_1
f : Ordinal.{u} → Ordinal.{u}
h : IsNormal f
s : Set Ordinal.{u}
hs : ∀ o ∈ s, o.IsLimit → ∃ a < o, Set.Ioo a o ⊆ s
o : Ordinal.{u}
ho : o ∈ f ⁻¹' s
ho' : o.IsLimit
⊢ ∃ a < o, Set.Ioo a o ⊆ f ⁻¹' s

Proof state:
case refine_2
f : Ordinal.{u} → Ordinal.{u}
⊢ StrictMono f ∧ Continuous f →
    StrictMono f ∧ ∀ (o : Ordinal.{u}), o.IsLimit → ∀ (a : Ordinal.{u}), (∀ b < o, f b ≤ a) → f o ≤ a

Tactic:
rintro ⟨h, h'⟩

Result:
case refine_2.intro
f : Ordinal.{u} → Ordinal.{u}
h : StrictMono f
h' : Continuous f
⊢ StrictMono f ∧ ∀ (o : Ordinal.{u}), o.IsLimit → ∀ (a : Ordinal.{u}), (∀ b < o, f b ≤ a) → f o ≤ a