case refine'_1
s : Set Ordinal
a : Ordinal
f : Ordinal → Ordinal
h : IsNormal f
⊢ Continuous f

case refine'_2
s : Set Ordinal
a : Ordinal
f : Ordinal → Ordinal
⊢ StrictMono f ∧ Continuous f → IsNormal f
s : Set Ordinal
a : Ordinal
f : Ordinal → Ordinal
⊢ IsNormal f ↔ StrictMono f ∧ Continuous f
refine' ⟨fun h => ⟨h.strictMono, _⟩, _⟩
case refine'_1
s : Set Ordinal
a : Ordinal
f : Ordinal → Ordinal
h : IsNormal f
⊢ ∀ (s : Set Ordinal), IsOpen s → IsOpen (f ⁻¹' s)
case refine'_1
s : Set Ordinal
a : Ordinal
f : Ordinal → Ordinal
h : IsNormal f
⊢ Continuous f
rw [continuous_def]
case refine'_1
s✝ : Set Ordinal
a : Ordinal
f : Ordinal → Ordinal
h : IsNormal f
s : Set Ordinal
hs : IsOpen s
⊢ IsOpen (f ⁻¹' s)
case refine'_1
s : Set Ordinal
a : Ordinal
f : Ordinal → Ordinal
h : IsNormal f
⊢ ∀ (s : Set Ordinal), IsOpen s → IsOpen (f ⁻¹' s)
intro s hs
case refine'_1
s✝ : Set Ordinal
a : Ordinal
f : Ordinal → Ordinal
h : IsNormal f
s : Set Ordinal
hs : ∀ (o : Ordinal), o ∈ s → IsLimit o → ∃ a, a < o ∧ Set.Ioo a o ⊆ s
⊢ ∀ (o : Ordinal), o ∈ f ⁻¹' s → IsLimit o → ∃ a, a < o ∧ Set.Ioo a o ⊆ f ⁻¹' s
case refine'_1
s✝ : Set Ordinal
a : Ordinal
f : Ordinal → Ordinal
h : IsNormal f
s : Set Ordinal
hs : IsOpen s
⊢ IsOpen (f ⁻¹' s)
rw [isOpen_iff] at *
case refine'_1
s✝ : Set Ordinal
a : Ordinal
f : Ordinal → Ordinal
h : IsNormal f
s : Set Ordinal
hs : ∀ (o : Ordinal), o ∈ s → IsLimit o → ∃ a, a < o ∧ Set.Ioo a o ⊆ s
o : Ordinal
ho : o ∈ f ⁻¹' s
ho' : IsLimit o
⊢ ∃ a, a < o ∧ Set.Ioo a o ⊆ f ⁻¹' s
case refine'_1
s✝ : Set Ordinal
a : Ordinal
f : Ordinal → Ordinal
h : IsNormal f
s : Set Ordinal
hs : ∀ (o : Ordinal), o ∈ s → IsLimit o → ∃ a, a < o ∧ Set.Ioo a o ⊆ s
⊢ ∀ (o : Ordinal), o ∈ f ⁻¹' s → IsLimit o → ∃ a, a < o ∧ Set.Ioo a o ⊆ f ⁻¹' s
intro o ho ho'
case refine'_1.intro.intro
s✝ : Set Ordinal
a✝ : Ordinal
f : Ordinal → Ordinal
h : IsNormal f
s : Set Ordinal
hs : ∀ (o : Ordinal), o ∈ s → IsLimit o → ∃ a, a < o ∧ Set.Ioo a o ⊆ s
o : Ordinal
ho : o ∈ f ⁻¹' s
ho' : IsLimit o
a : Ordinal
ha : a < f o
has : Set.Ioo a (f o) ⊆ s
⊢ ∃ a, a < o ∧ Set.Ioo a o ⊆ f ⁻¹' s
case refine'_1
s✝ : Set Ordinal
a : Ordinal
f : Ordinal → Ordinal
h : IsNormal f
s : Set Ordinal
hs : ∀ (o : Ordinal), o ∈ s → IsLimit o → ∃ a, a < o ∧ Set.Ioo a o ⊆ s
o : Ordinal
ho : o ∈ f ⁻¹' s
ho' : IsLimit o
⊢ ∃ a, a < o ∧ Set.Ioo a o ⊆ f ⁻¹' s
rcases hs _ ho (h.isLimit ho') with ⟨a, ha, has⟩
case refine'_1.intro.intro
s✝ : Set Ordinal
a✝ : Ordinal
f : Ordinal → Ordinal
h : IsNormal f
s : Set Ordinal
hs : ∀ (o : Ordinal), o ∈ s → IsLimit o → ∃ a, a < o ∧ Set.Ioo a o ⊆ s
o : Ordinal
ho : o ∈ f ⁻¹' s
ho' : IsLimit o
a : Ordinal
ha : ∃ i hi, a < f i
has : Set.Ioo a (f o) ⊆ s
⊢ ∃ a, a < o ∧ Set.Ioo a o ⊆ f ⁻¹' s
case refine'_1.intro.intro
s✝ : Set Ordinal
a✝ : Ordinal
f : Ordinal → Ordinal
h : IsNormal f
s : Set Ordinal
hs : ∀ (o : Ordinal), o ∈ s → IsLimit o → ∃ a, a < o ∧ Set.Ioo a o ⊆ s
o : Ordinal
ho : o ∈ f ⁻¹' s
ho' : IsLimit o
a : Ordinal
ha : a < f o
has : Set.Ioo a (f o) ⊆ s
⊢ ∃ a, a < o ∧ Set.Ioo a o ⊆ f ⁻¹' s
rw [← IsNormal.bsup_eq.{u, u} h ho', lt_bsup] at ha
case refine'_1.intro.intro.intro.intro
s✝ : Set Ordinal
a✝ : Ordinal
f : Ordinal → Ordinal
h : IsNormal f
s : Set Ordinal
hs : ∀ (o : Ordinal), o ∈ s → IsLimit o → ∃ a, a < o ∧ Set.Ioo a o ⊆ s
o : Ordinal
ho : o ∈ f ⁻¹' s
ho' : IsLimit o
a : Ordinal
has : Set.Ioo a (f o) ⊆ s
b : Ordinal
hb : b < o
hab : a < f b
⊢ ∃ a, a < o ∧ Set.Ioo a o ⊆ f ⁻¹' s
case refine'_1.intro.intro
s✝ : Set Ordinal
a✝ : Ordinal
f : Ordinal → Ordinal
h : IsNormal f
s : Set Ordinal
hs : ∀ (o : Ordinal), o ∈ s → IsLimit o → ∃ a, a < o ∧ Set.Ioo a o ⊆ s
o : Ordinal
ho : o ∈ f ⁻¹' s
ho' : IsLimit o
a : Ordinal
ha : ∃ i hi, a < f i
has : Set.Ioo a (f o) ⊆ s
⊢ ∃ a, a < o ∧ Set.Ioo a o ⊆ f ⁻¹' s
rcases ha with ⟨b, hb, hab⟩
no goals
case refine'_1.intro.intro.intro.intro
s✝ : Set Ordinal
a✝ : Ordinal
f : Ordinal → Ordinal
h : IsNormal f
s : Set Ordinal
hs : ∀ (o : Ordinal), o ∈ s → IsLimit o → ∃ a, a < o ∧ Set.Ioo a o ⊆ s
o : Ordinal
ho : o ∈ f ⁻¹' s
ho' : IsLimit o
a : Ordinal
has : Set.Ioo a (f o) ⊆ s
b : Ordinal
hb : b < o
hab : a < f b
⊢ ∃ a, a < o ∧ Set.Ioo a o ⊆ f ⁻¹' s
exact
  ⟨b, hb, fun c hc =>
    Set.mem_preimage.2 (has ⟨hab.trans (h.strictMono hc.1), h.strictMono hc.2⟩)⟩
case refine'_2
s : Set Ordinal
a : Ordinal
f : Ordinal → Ordinal
⊢ StrictMono f ∧ Continuous f →
    StrictMono f ∧ ∀ (o : Ordinal), IsLimit o → ∀ (a : Ordinal), (∀ (b : Ordinal), b < o → f b ≤ a) → f o ≤ a
case refine'_2
s : Set Ordinal
a : Ordinal
f : Ordinal → Ordinal
⊢ StrictMono f ∧ Continuous f → IsNormal f
rw [isNormal_iff_strictMono_limit]
case refine'_2.intro
s : Set Ordinal
a : Ordinal
f : Ordinal → Ordinal
h : StrictMono f
h' : Continuous f
⊢ StrictMono f ∧ ∀ (o : Ordinal), IsLimit o → ∀ (a : Ordinal), (∀ (b : Ordinal), b < o → f b ≤ a) → f o ≤ a
case refine'_2
s : Set Ordinal
a : Ordinal
f : Ordinal → Ordinal
⊢ StrictMono f ∧ Continuous f →
    StrictMono f ∧ ∀ (o : Ordinal), IsLimit o → ∀ (a : Ordinal), (∀ (b : Ordinal), b < o → f b ≤ a) → f o ≤ a
rintro ⟨h, h'⟩
case refine'_2.intro
s : Set Ordinal
a✝ : Ordinal
f : Ordinal → Ordinal
h✝ : StrictMono f
h' : Continuous f
o : Ordinal
ho : IsLimit o
a : Ordinal
h : ∀ (b : Ordinal), b < o → f b ≤ a
⊢ f o ≤ a
case refine'_2.intro
s : Set Ordinal
a : Ordinal
f : Ordinal → Ordinal
h : StrictMono f
h' : Continuous f
⊢ StrictMono f ∧ ∀ (o : Ordinal), IsLimit o → ∀ (a : Ordinal), (∀ (b : Ordinal), b < o → f b ≤ a) → f o ≤ a
refine' ⟨h, fun o ho a h => _⟩
case refine'_2.intro
s : Set Ordinal
a✝ : Ordinal
f : Ordinal → Ordinal
h✝ : StrictMono f
h' : Continuous f
o : Ordinal
ho : IsLimit o
a : Ordinal
h : ∀ (b : Ordinal), b < o → f b ≤ a
this : o ∈ f ⁻¹' Set.Iic a
⊢ f o ≤ a

case this
s : Set Ordinal
a✝ : Ordinal
f : Ordinal → Ordinal
h✝ : StrictMono f
h' : Continuous f
o : Ordinal
ho : IsLimit o
a : Ordinal
h : ∀ (b : Ordinal), b < o → f b ≤ a
⊢ o ∈ f ⁻¹' Set.Iic a
case refine'_2.intro
s : Set Ordinal
a✝ : Ordinal
f : Ordinal → Ordinal
h✝ : StrictMono f
h' : Continuous f
o : Ordinal
ho : IsLimit o
a : Ordinal
h : ∀ (b : Ordinal), b < o → f b ≤ a
⊢ f o ≤ a
suffices : o ∈ f ⁻¹' Set.Iic a
case this
s : Set Ordinal
a✝ : Ordinal
f : Ordinal → Ordinal
h✝ : StrictMono f
h' : Continuous f
o : Ordinal
ho : IsLimit o
a : Ordinal
h : ∀ (b : Ordinal), b < o → f b ≤ a
⊢ o ∈ f ⁻¹' Set.Iic a
case refine'_2.intro
s : Set Ordinal
a✝ : Ordinal
f : Ordinal → Ordinal
h✝ : StrictMono f
h' : Continuous f
o : Ordinal
ho : IsLimit o
a : Ordinal
h : ∀ (b : Ordinal), b < o → f b ≤ a
this : o ∈ f ⁻¹' Set.Iic a
⊢ f o ≤ a

case this
s : Set Ordinal
a✝ : Ordinal
f : Ordinal → Ordinal
h✝ : StrictMono f
h' : Continuous f
o : Ordinal
ho : IsLimit o
a : Ordinal
h : ∀ (b : Ordinal), b < o → f b ≤ a
⊢ o ∈ f ⁻¹' Set.Iic a
exact Set.mem_preimage.1 this
case this
s : Set Ordinal
a✝ : Ordinal
f : Ordinal → Ordinal
h✝ : StrictMono f
h' : Continuous f
o : Ordinal
ho : IsLimit o
a : Ordinal
h : ∀ (b : Ordinal), b < o → f b ≤ a
⊢ ∃ ι _hι f_1, (∀ (i : ι), f_1 i ∈ f ⁻¹' Set.Iic a) ∧ sup f_1 = o
case this
s : Set Ordinal
a✝ : Ordinal
f : Ordinal → Ordinal
h✝ : StrictMono f
h' : Continuous f
o : Ordinal
ho : IsLimit o
a : Ordinal
h : ∀ (b : Ordinal), b < o → f b ≤ a
⊢ o ∈ f ⁻¹' Set.Iic a
rw [mem_closed_iff_sup (IsClosed.preimage h' (@isClosed_Iic _ _ _ _ a))]