α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Preorder α
inst✝ : Nonempty α
s : Set α
h : ∀ (a : α), ∃ b, b ∈ s ∧ a < b
inhabited_h : Inhabited α
⊢ Set.Infinite s
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Preorder α
inst✝ : Nonempty α
s : Set α
h : ∀ (a : α), ∃ b, b ∈ s ∧ a < b
⊢ Set.Infinite s
inhabit α
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Preorder α
inst✝ : Nonempty α
s : Set α
h : ∀ (a : α), ∃ b, b ∈ s ∧ a < b
inhabited_h : Inhabited α
f : ℕ → α :=
  fun n => Nat.recOn n (Exists.choose (_ : ∃ b, b ∈ s ∧ default < b)) fun n a => Exists.choose (_ : ∃ b, b ∈ s ∧ a < b)
⊢ Set.Infinite s
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Preorder α
inst✝ : Nonempty α
s : Set α
h : ∀ (a : α), ∃ b, b ∈ s ∧ a < b
inhabited_h : Inhabited α
⊢ Set.Infinite s
set f : ℕ → α := fun n => Nat.recOn n (h default).choose fun n a => (h a).choose
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Preorder α
inst✝ : Nonempty α
s : Set α
h : ∀ (a : α), ∃ b, b ∈ s ∧ a < b
inhabited_h : Inhabited α
f : ℕ → α :=
  fun n => Nat.recOn n (Exists.choose (_ : ∃ b, b ∈ s ∧ default < b)) fun n a => Exists.choose (_ : ∃ b, b ∈ s ∧ a < b)
hf : ∀ (n : ℕ), f n ∈ s
⊢ Set.Infinite s
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Preorder α
inst✝ : Nonempty α
s : Set α
h : ∀ (a : α), ∃ b, b ∈ s ∧ a < b
inhabited_h : Inhabited α
f : ℕ → α :=
  fun n => Nat.recOn n (Exists.choose (_ : ∃ b, b ∈ s ∧ default < b)) fun n a => Exists.choose (_ : ∃ b, b ∈ s ∧ a < b)
⊢ Set.Infinite s
have hf : ∀ n, f n ∈ s := by rintro (_ | _) <;> exact (h _).choose_spec.1
no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Preorder α
inst✝ : Nonempty α
s : Set α
h : ∀ (a : α), ∃ b, b ∈ s ∧ a < b
inhabited_h : Inhabited α
f : ℕ → α :=
  fun n => Nat.recOn n (Exists.choose (_ : ∃ b, b ∈ s ∧ default < b)) fun n a => Exists.choose (_ : ∃ b, b ∈ s ∧ a < b)
hf : ∀ (n : ℕ), f n ∈ s
⊢ Set.Infinite s
exact infinite_of_injective_forall_mem
  (strictMono_nat_of_lt_succ fun n => (h _).choose_spec.2).injective hf
no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Preorder α
inst✝ : Nonempty α
s : Set α
h : ∀ (a : α), ∃ b, b ∈ s ∧ a < b
inhabited_h : Inhabited α
f : ℕ → α :=
  fun n => Nat.recOn n (Exists.choose (_ : ∃ b, b ∈ s ∧ default < b)) fun n a => Exists.choose (_ : ∃ b, b ∈ s ∧ a < b)
⊢ ∀ (n : ℕ), f n ∈ s
rintro (_ | _) <;> exact (h _).choose_spec.1