ι : Type ?u.108989
α : Type u_1
β : Type ?u.108995
inst✝ : LinearOrder α
s : Set α
hs : IsWf s
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
⊢ ∃ m n, m < n ∧ (fun x x_1 => x ≤ x_1) (f m) (f n)
ι : Type ?u.108989
α : Type u_1
β : Type ?u.108995
inst✝ : LinearOrder α
s : Set α
hs : IsWf s
⊢ IsPwo s
intro f hf
case intro
ι : Type ?u.108989
α : Type u_1
β : Type ?u.108995
inst✝ : LinearOrder α
s : Set α
hs : IsWf s
f : ℕ → ↑s
⊢ ∃ m n, m < n ∧ (fun x x_1 => x ≤ x_1) ((fun i => ↑(f i)) m) ((fun i => ↑(f i)) n)
ι : Type ?u.108989
α : Type u_1
β : Type ?u.108995
inst✝ : LinearOrder α
s : Set α
hs : IsWf s
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
⊢ ∃ m n, m < n ∧ (fun x x_1 => x ≤ x_1) (f m) (f n)
lift f to ℕ → s using hf
case intro.intro.intro.intro
ι : Type ?u.108989
α : Type u_1
β : Type ?u.108995
inst✝ : LinearOrder α
s : Set α
hs : IsWf s
f : ℕ → ↑s
m : ℕ
hm : ∀ (x : ↑s), x ∈ range f → ¬(fun x x_1 => x < x_1) ↑x ↑(f m)
⊢ ∃ m n, m < n ∧ (fun x x_1 => x ≤ x_1) ((fun i => ↑(f i)) m) ((fun i => ↑(f i)) n)
case intro
ι : Type ?u.108989
α : Type u_1
β : Type ?u.108995
inst✝ : LinearOrder α
s : Set α
hs : IsWf s
f : ℕ → ↑s
⊢ ∃ m n, m < n ∧ (fun x x_1 => x ≤ x_1) ((fun i => ↑(f i)) m) ((fun i => ↑(f i)) n)
rcases hs.has_min (range f) (range_nonempty _) with ⟨_, ⟨m, rfl⟩, hm⟩
case intro.intro.intro.intro
ι : Type ?u.108989
α : Type u_1
β : Type ?u.108995
inst✝ : LinearOrder α
s : Set α
hs : IsWf s
f : ℕ → ↑s
m : ℕ
hm : ∀ (i : ℕ), ↑(f m) ≤ ↑(f i)
⊢ ∃ m n, m < n ∧ (fun x x_1 => x ≤ x_1) ((fun i => ↑(f i)) m) ((fun i => ↑(f i)) n)
case intro.intro.intro.intro
ι : Type ?u.108989
α : Type u_1
β : Type ?u.108995
inst✝ : LinearOrder α
s : Set α
hs : IsWf s
f : ℕ → ↑s
m : ℕ
hm : ∀ (x : ↑s), x ∈ range f → ¬(fun x x_1 => x < x_1) ↑x ↑(f m)
⊢ ∃ m n, m < n ∧ (fun x x_1 => x ≤ x_1) ((fun i => ↑(f i)) m) ((fun i => ↑(f i)) n)
simp only [forall_range_iff, not_lt] at hm
no goals
case intro.intro.intro.intro
ι : Type ?u.108989
α : Type u_1
β : Type ?u.108995
inst✝ : LinearOrder α
s : Set α
hs : IsWf s
f : ℕ → ↑s
m : ℕ
hm : ∀ (i : ℕ), ↑(f m) ≤ ↑(f i)
⊢ ∃ m n, m < n ∧ (fun x x_1 => x ≤ x_1) ((fun i => ↑(f i)) m) ((fun i => ↑(f i)) n)
exact ⟨m, m + 1, lt_add_one m, hm _⟩