no goals
case zero
α β : Type u
a : Cardinal
⊢ Nat.zero • a < ℵ₀ ↔ Nat.zero = 0 ∨ a < ℵ₀
simpa using nat_lt_aleph0 0
case succ
α β : Type u
a : Cardinal
n : ℕ
⊢ Nat.succ n • a < ℵ₀ ↔ a < ℵ₀
case succ
α β : Type u
a : Cardinal
n : ℕ
⊢ Nat.succ n • a < ℵ₀ ↔ Nat.succ n = 0 ∨ a < ℵ₀
simp only [Nat.succ_ne_zero, false_or_iff]
case succ.zero
α β : Type u
a : Cardinal
⊢ Nat.succ Nat.zero • a < ℵ₀ ↔ a < ℵ₀

case succ.succ
α β : Type u
a : Cardinal
n : ℕ
ih : Nat.succ n • a < ℵ₀ ↔ a < ℵ₀
⊢ Nat.succ (Nat.succ n) • a < ℵ₀ ↔ a < ℵ₀
case succ
α β : Type u
a : Cardinal
n : ℕ
⊢ Nat.succ n • a < ℵ₀ ↔ a < ℵ₀
induction' n with n ih
no goals
case succ.succ
α β : Type u
a : Cardinal
n : ℕ
ih : Nat.succ n • a < ℵ₀ ↔ a < ℵ₀
⊢ Nat.succ (Nat.succ n) • a < ℵ₀ ↔ a < ℵ₀
rw [succ_nsmul, add_lt_aleph0_iff, ih, and_self_iff]
no goals
case succ.zero
α β : Type u
a : Cardinal
⊢ Nat.succ Nat.zero • a < ℵ₀ ↔ a < ℵ₀
simp