⊢ StrictMono (ord ∘ aleph) ∧ range (ord ∘ aleph) = {b | ord (card b) = b ∧ ω ≤ b}
⊢ ord ∘ aleph = enumOrd {b | ord (card b) = b ∧ ω ≤ b}
rw [← eq_enumOrd _ ord_card_unbounded']
⊢ range (ord ∘ aleph) = {b | ord (card b) = b ∧ ω ≤ b}
⊢ StrictMono (ord ∘ aleph) ∧ range (ord ∘ aleph) = {b | ord (card b) = b ∧ ω ≤ b}
use aleph_isNormal.strictMono
⊢ (∀ (a : Ordinal), (ord ∘ aleph) a ∈ {b | ord (card b) = b ∧ ω ≤ b}) ∧
    ∀ (b : Ordinal), b ∈ {b | ord (card b) = b ∧ ω ≤ b} → ∃ a, (ord ∘ aleph) a = b
⊢ range (ord ∘ aleph) = {b | ord (card b) = b ∧ ω ≤ b}
rw [range_eq_iff]
case refine'_1
a : Ordinal
⊢ ord (card ((ord ∘ aleph) a)) = (ord ∘ aleph) a

case refine'_2
a : Ordinal
⊢ ω ≤ (ord ∘ aleph) a
⊢ (∀ (a : Ordinal), (ord ∘ aleph) a ∈ {b | ord (card b) = b ∧ ω ≤ b}) ∧
    ∀ (b : Ordinal), b ∈ {b | ord (card b) = b ∧ ω ≤ b} → ∃ a, (ord ∘ aleph) a = b
refine' ⟨fun a => ⟨_, _⟩, fun b hb => eq_aleph_of_eq_card_ord hb.1 hb.2⟩
no goals
case refine'_1
a : Ordinal
⊢ ord (card ((ord ∘ aleph) a)) = (ord ∘ aleph) a
rw [Function.comp_apply, card_ord]
case refine'_2
a : Ordinal
⊢ ℵ₀ ≤ aleph a
case refine'_2
a : Ordinal
⊢ ω ≤ (ord ∘ aleph) a
rw [← ord_aleph0, Function.comp_apply, ord_le_ord]
no goals
case refine'_2
a : Ordinal
⊢ ℵ₀ ≤ aleph a
exact aleph0_le_aleph _