case inl
a✝ b : Cardinal
n m : ℕ
a : Cardinal
h : ℵ₀ ≤ a
⊢ Prime a ↔ ℵ₀ ≤ a ∨ ∃ p, a = ↑p ∧ Nat.Prime p

case inr
a✝ b : Cardinal
n m : ℕ
a : Cardinal
h : a < ℵ₀
⊢ Prime a ↔ ℵ₀ ≤ a ∨ ∃ p, a = ↑p ∧ Nat.Prime p
a✝ b : Cardinal
n m : ℕ
a : Cardinal
⊢ Prime a ↔ ℵ₀ ≤ a ∨ ∃ p, a = ↑p ∧ Nat.Prime p
cases' le_or_lt ℵ₀ a with h h
case inr.intro
a✝ b : Cardinal
n m a : ℕ
h : ↑a < ℵ₀
⊢ Prime ↑a ↔ ℵ₀ ≤ ↑a ∨ ∃ p, ↑a = ↑p ∧ Nat.Prime p
case inr
a✝ b : Cardinal
n m : ℕ
a : Cardinal
h : a < ℵ₀
⊢ Prime a ↔ ℵ₀ ≤ a ∨ ∃ p, a = ↑p ∧ Nat.Prime p
lift a to ℕ using id h
no goals
case inr.intro
a✝ b : Cardinal
n m a : ℕ
h : ↑a < ℵ₀
⊢ Prime ↑a ↔ ℵ₀ ≤ ↑a ∨ ∃ p, ↑a = ↑p ∧ Nat.Prime p
simp [not_le.mpr h]
no goals
case inl
a✝ b : Cardinal
n m : ℕ
a : Cardinal
h : ℵ₀ ≤ a
⊢ Prime a ↔ ℵ₀ ≤ a ∨ ∃ p, a = ↑p ∧ Nat.Prime p
simp [h]