α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
f : (fun x x_1 => x > x_1) ↪r r
k : ℕ
⊢ Nonempty { f_1 // ↑f k ∈ Set.range ↑f_1 }
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
f : (fun x x_1 => x > x_1) ↪r r
k : ℕ
⊢ ¬Acc r (↑f k)
rw [acc_iff_no_decreasing_seq, not_isEmpty_iff]
no goals
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
f : (fun x x_1 => x > x_1) ↪r r
k : ℕ
⊢ Nonempty { f_1 // ↑f k ∈ Set.range ↑f_1 }
exact ⟨⟨f, k, rfl⟩⟩