case mp
S : Set Ordinal
f : Ordinal → Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
⊢ StrictMono f ∧ range f = S → f = enumOrd S

case mpr
S : Set Ordinal
f : Ordinal → Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
⊢ f = enumOrd S → StrictMono f ∧ range f = S
S : Set Ordinal
f : Ordinal → Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
⊢ StrictMono f ∧ range f = S ↔ f = enumOrd S
constructor
case mp.intro
S : Set Ordinal
f : Ordinal → Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
h₁ : StrictMono f
h₂ : range f = S
⊢ f = enumOrd S
case mp
S : Set Ordinal
f : Ordinal → Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
⊢ StrictMono f ∧ range f = S → f = enumOrd S
rintro ⟨h₁, h₂⟩
no goals
case mp.intro
S : Set Ordinal
f : Ordinal → Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
h₁ : StrictMono f
h₂ : range f = S
⊢ f = enumOrd S
rwa [← lt_wf.eq_strictMono_iff_eq_range h₁ (enumOrd_strictMono hS), range_enumOrd hS]
case mpr
S : Set Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
⊢ StrictMono (enumOrd S) ∧ range (enumOrd S) = S
case mpr
S : Set Ordinal
f : Ordinal → Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
⊢ f = enumOrd S → StrictMono f ∧ range f = S
rintro rfl
no goals
case mpr
S : Set Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
⊢ StrictMono (enumOrd S) ∧ range (enumOrd S) = S
exact ⟨enumOrd_strictMono hS, range_enumOrd hS⟩