S✝ : Set Ordinal
S T : Set Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
hST : S ⊆ T
a : Ordinal
⊢ ∀ (j : Ordinal), (∀ (k : Ordinal), k < j → enumOrd T k ≤ enumOrd S k) → enumOrd T j ≤ enumOrd S j
S✝ : Set Ordinal
S T : Set Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
hST : S ⊆ T
a : Ordinal
⊢ enumOrd T a ≤ enumOrd S a
apply Ordinal.induction a
S✝ : Set Ordinal
S T : Set Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
hST : S ⊆ T
a b : Ordinal
H : ∀ (k : Ordinal), k < b → enumOrd T k ≤ enumOrd S k
⊢ enumOrd T b ≤ enumOrd S b
S✝ : Set Ordinal
S T : Set Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
hST : S ⊆ T
a : Ordinal
⊢ ∀ (j : Ordinal), (∀ (k : Ordinal), k < j → enumOrd T k ≤ enumOrd S k) → enumOrd T j ≤ enumOrd S j
intro b H
S✝ : Set Ordinal
S T : Set Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
hST : S ⊆ T
a b : Ordinal
H : ∀ (k : Ordinal), k < b → enumOrd T k ≤ enumOrd S k
⊢ sInf (T ∩ {b_1 | ∀ (c : Ordinal), c < b → enumOrd T c < b_1}) ≤ enumOrd S b
S✝ : Set Ordinal
S T : Set Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
hST : S ⊆ T
a b : Ordinal
H : ∀ (k : Ordinal), k < b → enumOrd T k ≤ enumOrd S k
⊢ enumOrd T b ≤ enumOrd S b
rw [enumOrd_def]
no goals
S✝ : Set Ordinal
S T : Set Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
hST : S ⊆ T
a b : Ordinal
H : ∀ (k : Ordinal), k < b → enumOrd T k ≤ enumOrd S k
⊢ sInf (T ∩ {b_1 | ∀ (c : Ordinal), c < b → enumOrd T c < b_1}) ≤ enumOrd S b
exact csInf_le' ⟨hST (enumOrd_mem hS b), fun c h => (H c h).trans_lt (enumOrd_strictMono hS h)⟩