⊢ StrictMono (ord ∘ aleph') ∧
    (∀ (a : Ordinal), (ord ∘ aleph') a ∈ {b | ord (card b) = b}) ∧
      ∀ (b : Ordinal), b ∈ {b | ord (card b) = b} → ∃ a, (ord ∘ aleph') a = b
⊢ ord ∘ aleph' = enumOrd {b | ord (card b) = b}
rw [← eq_enumOrd _ ord_card_unbounded, range_eq_iff]
no goals
⊢ StrictMono (ord ∘ aleph') ∧
    (∀ (a : Ordinal), (ord ∘ aleph') a ∈ {b | ord (card b) = b}) ∧
      ∀ (b : Ordinal), b ∈ {b | ord (card b) = b} → ∃ a, (ord ∘ aleph') a = b
exact
  ⟨aleph'_isNormal.strictMono,
    ⟨fun a => by
      dsimp
      rw [card_ord], fun b hb => eq_aleph'_of_eq_card_ord hb⟩⟩
a : Ordinal
⊢ ord (card (ord (aleph' a))) = ord (aleph' a)
a : Ordinal
⊢ (ord ∘ aleph') a ∈ {b | ord (card b) = b}
dsimp
no goals
a : Ordinal
⊢ ord (card (ord (aleph' a))) = ord (aleph' a)
rw [card_ord]