-- Mathlib/SetTheory/Ordinal/Enum.lean
theorem range_enumOrd (hs : ¬ BddAbove s) : range (enumOrd s) = s

Proof state:
case h.mpr.refine_1
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b | a ≤ enumOrd s b}
ha : a ∈ s
b : Ordinal.{u}
hb : b < sInf t
hb' : a ≤ enumOrd s b
⊢ False

Tactic:
exact hb.not_le (csInf_le' hb')

Result:
no goals

Proof state:
case h.mp.intro
s : Set Ordinal.{u}
hs : ¬BddAbove s
b : Ordinal.{u}
t : Set Ordinal.{u} := {b_1 | enumOrd s b ≤ enumOrd s b_1}
⊢ enumOrd s b ∈ s

Tactic:
exact enumOrd_mem hs b

Result:
no goals

Proof state:
case h.mpr.refine_2
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b | a ≤ enumOrd s b}
ha : a ∈ s
⊢ a ≤ enumOrd s (sInf t)

Tactic:
exact csInf_mem (s := t) ⟨a, (enumOrd_strictMono hs).id_le a⟩

Result:
no goals

Proof state:
case h.mpr
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b | a ≤ enumOrd s b}
ha : a ∈ s
⊢ a ∈ range (enumOrd s)

Tactic:
refine ⟨sInf t, (enumOrd_le_of_forall_lt ha ?_).antisymm ?_⟩

Result:
case h.mpr.refine_1
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b | a ≤ enumOrd s b}
ha : a ∈ s
⊢ ∀ b < sInf t, enumOrd s b < a

case h.mpr.refine_2
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b | a ≤ enumOrd s b}
ha : a ∈ s
⊢ a ≤ enumOrd s (sInf t)

Proof state:
case h.mpr.refine_1
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b | a ≤ enumOrd s b}
ha : a ∈ s
b : Ordinal.{u}
hb : b < sInf t
⊢ enumOrd s b < a

Tactic:
by_contra! hb'

Result:
case h.mpr.refine_1
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b | a ≤ enumOrd s b}
ha : a ∈ s
b : Ordinal.{u}
hb : b < sInf t
hb' : a ≤ enumOrd s b
⊢ False

Proof state:
case h.mpr.refine_1
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b | a ≤ enumOrd s b}
ha : a ∈ s
⊢ ∀ b < sInf t, enumOrd s b < a

Tactic:
intro b hb

Result:
case h.mpr.refine_1
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b | a ≤ enumOrd s b}
ha : a ∈ s
b : Ordinal.{u}
hb : b < sInf t
⊢ enumOrd s b < a

Proof state:
case h
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
⊢ a ∈ range (enumOrd s) ↔ a ∈ s

Tactic:
let t := { b | a ≤ enumOrd s b }

Result:
case h
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b | a ≤ enumOrd s b}
⊢ a ∈ range (enumOrd s) ↔ a ∈ s

Proof state:
s : Set Ordinal.{u}
hs : ¬BddAbove s
⊢ range (enumOrd s) = s

Tactic:
ext a

Result:
case h
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
⊢ a ∈ range (enumOrd s) ↔ a ∈ s

Proof state:
case h.mpr
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b | a ≤ enumOrd s b}
⊢ a ∈ s → a ∈ range (enumOrd s)

Tactic:
intro ha

Result:
case h.mpr
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b | a ≤ enumOrd s b}
ha : a ∈ s
⊢ a ∈ range (enumOrd s)

Proof state:
case h
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b | a ≤ enumOrd s b}
⊢ a ∈ range (enumOrd s) ↔ a ∈ s

Tactic:
constructor

Result:
case h.mp
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b | a ≤ enumOrd s b}
⊢ a ∈ range (enumOrd s) → a ∈ s

case h.mpr
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b | a ≤ enumOrd s b}
⊢ a ∈ s → a ∈ range (enumOrd s)

Proof state:
case h.mp
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b | a ≤ enumOrd s b}
⊢ a ∈ range (enumOrd s) → a ∈ s

Tactic:
rintro ⟨b, rfl⟩

Result:
case h.mp.intro
s : Set Ordinal.{u}
hs : ¬BddAbove s
b : Ordinal.{u}
t : Set Ordinal.{u} := {b_1 | enumOrd s b ≤ enumOrd s b_1}
⊢ enumOrd s b ∈ s