S : Set Ordinal
a b : Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
ha : a ∈ S
hb : enumOrd S b < a
⊢ sInf (S ∩ {b_1 | ∀ (c : Ordinal), c < succ b → enumOrd S c < b_1}) ≤ a
S : Set Ordinal
a b : Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
ha : a ∈ S
hb : enumOrd S b < a
⊢ enumOrd S (succ b) ≤ a
rw [enumOrd_def]
no goals
S : Set Ordinal
a b : Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
ha : a ∈ S
hb : enumOrd S b < a
⊢ sInf (S ∩ {b_1 | ∀ (c : Ordinal), c < succ b → enumOrd S c < b_1}) ≤ a
exact
  csInf_le' ⟨ha, fun c hc => ((enumOrd_strictMono hS).monotone (le_of_lt_succ hc)).trans_lt hb⟩