a b c : ℕ
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
seed : ℕ
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
⊢ Set.Finite {x | P x} → False
a b c : ℕ
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
seed : ℕ
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
⊢ P n
apply Nat.decreasing_induction_of_infinite h fun hf => _
a b c : ℕ
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
seed : ℕ
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
hf : Set.Finite {x | P x}
⊢ False
a b c : ℕ
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
seed : ℕ
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
⊢ Set.Finite {x | P x} → False
intro hf
case intro.intro
a b c : ℕ
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
seed : ℕ
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
hf : Set.Finite {x | P x}
m : ℕ
hP : m ∈ {x | P x}
hm : ∀ (a' : ℕ), a' ∈ {x | P x} → id m ≤ id a' → id m = id a'
⊢ False
a b c : ℕ
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
seed : ℕ
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
hf : Set.Finite {x | P x}
⊢ False
obtain ⟨m, hP, hm⟩ := hf.exists_maximal_wrt id _ ⟨seed, hs⟩
case intro.intro.intro.intro
a b c : ℕ
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
seed : ℕ
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
hf : Set.Finite {x | P x}
m : ℕ
hP : m ∈ {x | P x}
hm : ∀ (a' : ℕ), a' ∈ {x | P x} → id m ≤ id a' → id m = id a'
y : ℕ
hl : m < y
hy : P y
⊢ False
case intro.intro
a b c : ℕ
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
seed : ℕ
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
hf : Set.Finite {x | P x}
m : ℕ
hP : m ∈ {x | P x}
hm : ∀ (a' : ℕ), a' ∈ {x | P x} → id m ≤ id a' → id m = id a'
⊢ False
obtain ⟨y, hl, hy⟩ := hi m (le_of_not_lt fun hl => hl.ne <| hm seed hs hl.le) hP
no goals
case intro.intro.intro.intro
a b c : ℕ
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
seed : ℕ
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
hf : Set.Finite {x | P x}
m : ℕ
hP : m ∈ {x | P x}
hm : ∀ (a' : ℕ), a' ∈ {x | P x} → id m ≤ id a' → id m = id a'
y : ℕ
hl : m < y
hy : P y
⊢ False
exact hl.ne (hm y hy hl.le)