case zero
m✝ n k l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
m : ℕ
⊢ Nat.findGreatest P zero = m ↔ m ≤ zero ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ zero → ¬P n

case succ
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
⊢ Nat.findGreatest P (succ k) = m ↔ m ≤ succ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
m n k l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
⊢ Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
induction' k with k ihk generalizing m
case zero
m✝ n k l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
m : ℕ
⊢ (m ≤ zero ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ zero → ¬P n) ↔ m = Nat.findGreatest P zero
case zero
m✝ n k l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
m : ℕ
⊢ Nat.findGreatest P zero = m ↔ m ≤ zero ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ zero → ¬P n
rw [eq_comm, Iff.comm]
case zero
m✝ n k l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
m : ℕ
⊢ m = 0 → (¬m = 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n = 0 → ¬P n
case zero
m✝ n k l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
m : ℕ
⊢ (m ≤ zero ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ zero → ¬P n) ↔ m = Nat.findGreatest P zero
simp only [zero_eq, nonpos_iff_eq_zero, ne_eq, findGreatest_zero, and_iff_left_iff_imp]
case zero
m n k l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
⊢ (¬0 = 0 → P 0) ∧ ∀ ⦃n : ℕ⦄, 0 < n → n = 0 → ¬P n
case zero
m✝ n k l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
m : ℕ
⊢ m = 0 → (¬m = 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n = 0 → ¬P n
rintro rfl
no goals
case zero
m n k l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
⊢ (¬0 = 0 → P 0) ∧ ∀ ⦃n : ℕ⦄, 0 < n → n = 0 → ¬P n
exact ⟨fun h => (h rfl).elim, fun n hlt heq => (hlt.ne heq.symm).elim⟩
case pos
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
⊢ Nat.findGreatest P (succ k) = m ↔ m ≤ succ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n

case neg
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
⊢ Nat.findGreatest P (succ k) = m ↔ m ≤ succ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
case succ
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
⊢ Nat.findGreatest P (succ k) = m ↔ m ≤ succ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
by_cases hk : P (k + 1)
case pos
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
⊢ k + 1 = m ↔ m ≤ succ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
case pos
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
⊢ Nat.findGreatest P (succ k) = m ↔ m ≤ succ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
rw [findGreatest_eq hk]
case pos.mp
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
⊢ k + 1 = m → m ≤ succ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n

case pos.mpr
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
⊢ (m ≤ succ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n) → k + 1 = m
case pos
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
⊢ k + 1 = m ↔ m ≤ succ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
constructor
case pos.mp
m n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
hk : P (k + 1)
⊢ k + 1 ≤ succ k ∧ (k + 1 ≠ 0 → P (k + 1)) ∧ ∀ ⦃n : ℕ⦄, k + 1 < n → n ≤ succ k → ¬P n
case pos.mp
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
⊢ k + 1 = m → m ≤ succ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
rintro rfl
no goals
case pos.mp
m n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
hk : P (k + 1)
⊢ k + 1 ≤ succ k ∧ (k + 1 ≠ 0 → P (k + 1)) ∧ ∀ ⦃n : ℕ⦄, k + 1 < n → n ≤ succ k → ¬P n
exact ⟨le_rfl, fun _ => hk, fun n hlt hle => (hlt.not_le hle).elim⟩
case pos.mpr.intro.intro
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
hle : m ≤ succ k
h0 : m ≠ 0 → P m
hm : ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
⊢ k + 1 = m
case pos.mpr
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
⊢ (m ≤ succ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n) → k + 1 = m
rintro ⟨hle, h0, hm⟩
case pos.mpr.intro.intro.inl
m n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
hk : P (k + 1)
hle : succ k ≤ succ k
h0 : succ k ≠ 0 → P (succ k)
hm : ∀ ⦃n : ℕ⦄, succ k < n → n ≤ succ k → ¬P n
⊢ k + 1 = succ k

case pos.mpr.intro.intro.inr
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
hle : m ≤ succ k
h0 : m ≠ 0 → P m
hm : ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
hlt : m < succ k
⊢ k + 1 = m
case pos.mpr.intro.intro
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
hle : m ≤ succ k
h0 : m ≠ 0 → P m
hm : ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
⊢ k + 1 = m
rcases Decidable.eq_or_lt_of_le hle with (rfl | hlt)
no goals
case pos.mpr.intro.intro.inl
m n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
hk : P (k + 1)
hle : succ k ≤ succ k
h0 : succ k ≠ 0 → P (succ k)
hm : ∀ ⦃n : ℕ⦄, succ k < n → n ≤ succ k → ¬P n
⊢ k + 1 = succ k

case pos.mpr.intro.intro.inr
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
hle : m ≤ succ k
h0 : m ≠ 0 → P m
hm : ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
hlt : m < succ k
⊢ k + 1 = m
exacts [rfl, (hm hlt le_rfl hk).elim]
case neg
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
⊢ (m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n) ↔
    m ≤ succ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
case neg
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
⊢ Nat.findGreatest P (succ k) = m ↔ m ≤ succ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
rw [findGreatest_of_not hk, ihk]
case neg.mp
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
⊢ (m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n) →
    m ≤ succ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n

case neg.mpr
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
⊢ (m ≤ succ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n) →
    m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
case neg
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
⊢ (m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n) ↔
    m ≤ succ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
constructor
case neg.mp.intro.intro
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
hle : m ≤ k
hP : m ≠ 0 → P m
hm : ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
⊢ m ≤ succ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
case neg.mp
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
⊢ (m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n) →
    m ≤ succ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
rintro ⟨hle, hP, hm⟩
case neg.mp.intro.intro
m✝ n✝ k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
hle✝ : m ≤ k
hP : m ≠ 0 → P m
hm : ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
n : ℕ
hlt : m < n
hle : n ≤ succ k
⊢ ¬P n
case neg.mp.intro.intro
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
hle : m ≤ k
hP : m ≠ 0 → P m
hm : ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
⊢ m ≤ succ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
refine ⟨hle.trans k.le_succ, hP, fun n hlt hle => ?_⟩
case neg.mp.intro.intro.inl
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
hle✝ : m ≤ k
hP : m ≠ 0 → P m
hm : ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
hlt : m < succ k
hle : succ k ≤ succ k
⊢ ¬P (succ k)

case neg.mp.intro.intro.inr
m✝ n✝ k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
hle✝ : m ≤ k
hP : m ≠ 0 → P m
hm : ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
n : ℕ
hlt : m < n
hle : n ≤ succ k
hlt' : n < succ k
⊢ ¬P n
case neg.mp.intro.intro
m✝ n✝ k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
hle✝ : m ≤ k
hP : m ≠ 0 → P m
hm : ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
n : ℕ
hlt : m < n
hle : n ≤ succ k
⊢ ¬P n
rcases Decidable.eq_or_lt_of_le hle with (rfl | hlt')
no goals
case neg.mp.intro.intro.inl
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
hle✝ : m ≤ k
hP : m ≠ 0 → P m
hm : ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
hlt : m < succ k
hle : succ k ≤ succ k
⊢ ¬P (succ k)

case neg.mp.intro.intro.inr
m✝ n✝ k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
hle✝ : m ≤ k
hP : m ≠ 0 → P m
hm : ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
n : ℕ
hlt : m < n
hle : n ≤ succ k
hlt' : n < succ k
⊢ ¬P n
exacts [hk, hm hlt <| lt_succ_iff.1 hlt']
case neg.mpr.intro.intro
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
hle : m ≤ succ k
hP : m ≠ 0 → P m
hm : ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
⊢ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
case neg.mpr
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
⊢ (m ≤ succ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n) →
    m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
rintro ⟨hle, hP, hm⟩
case neg.mpr.intro.intro
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
hle : m ≤ succ k
hP : m ≠ 0 → P m
hm : ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
⊢ m ≠ succ k
case neg.mpr.intro.intro
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
hle : m ≤ succ k
hP : m ≠ 0 → P m
hm : ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
⊢ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
refine ⟨lt_succ_iff.1 (hle.lt_of_ne ?_), hP, fun n hlt hle => hm hlt (hle.trans k.le_succ)⟩
case neg.mpr.intro.intro
m n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
hk : ¬P (k + 1)
hle : succ k ≤ succ k
hP : succ k ≠ 0 → P (succ k)
hm : ∀ ⦃n : ℕ⦄, succ k < n → n ≤ succ k → ¬P n
⊢ False
case neg.mpr.intro.intro
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
hle : m ≤ succ k
hP : m ≠ 0 → P m
hm : ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
⊢ m ≠ succ k
rintro rfl
no goals
case neg.mpr.intro.intro
m n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
hk : ¬P (k + 1)
hle : succ k ≤ succ k
hP : succ k ≠ 0 → P (succ k)
hm : ∀ ⦃n : ℕ⦄, succ k < n → n ≤ succ k → ¬P n
⊢ False
exact hk (hP k.succ_ne_zero)