-- Mathlib/Data/Set/Enumerate.lean
theorem enumerate_eq_none :
    ∀ {s n₁ n₂}, enumerate sel s n₁ = none → n₁ ≤ n₂ → enumerate sel s n₂ = none
  | _, 0, _ => fun h _ ↦ enumerate_eq_none_of_sel sel h
  | s, n + 1, m => fun h hm ↦ by
    cases hs : sel s
    · exact enumerate_eq_none_of_sel sel hs
    · cases m with
      | zero => contradiction
      | succ m' =>
        simp? [hs, enumerate] at h ⊢ says
          simp only [enumerate, hs, Option.bind_eq_bind, Option.some_bind] at h ⊢
        have hm : n ≤ m' := Nat.le_of_succ_le_succ hm
        exact enumerate_eq_none h hm

Proof state:
case some.succ
α : Type u_1
sel : Set α → Option α
s : Set α
n : ℕ
h : enumerate sel s (n + 1) = none
val✝ : α
hs : sel s = some val✝
m' : ℕ
hm : n + 1 ≤ m' + 1
⊢ enumerate sel s (m' + 1) = none

Tactic:
simp? [hs, enumerate] at h ⊢ says
  simp only [enumerate, hs, Option.bind_eq_bind, Option.some_bind] at h ⊢

Result:
case some.succ
α : Type u_1
sel : Set α → Option α
s : Set α
n : ℕ
val✝ : α
hs : sel s = some val✝
m' : ℕ
hm : n + 1 ≤ m' + 1
h : enumerate sel (s \ {val✝}) n = none
⊢ enumerate sel (s \ {val✝}) m' = none

Proof state:
case some
α : Type u_1
sel : Set α → Option α
s : Set α
n m : ℕ
h : enumerate sel s (n + 1) = none
hm : n + 1 ≤ m
val✝ : α
hs : sel s = some val✝
⊢ enumerate sel s m = none

Tactic:
cases m with
| zero => contradiction
| succ m' =>
  simp? [hs, enumerate] at h ⊢ says
    simp only [enumerate, hs, Option.bind_eq_bind, Option.some_bind] at h ⊢
  have hm : n ≤ m' := Nat.le_of_succ_le_succ hm
  exact enumerate_eq_none h hm

Result:
no goals

Proof state:
case some.succ
α : Type u_1
sel : Set α → Option α
s : Set α
n : ℕ
h : enumerate sel s (n + 1) = none
val✝ : α
hs : sel s = some val✝
m' : ℕ
hm : n + 1 ≤ m' + 1
⊢ enumerate sel s (m' + 1) = none

Tactic:
simp only [enumerate, hs, Option.bind_eq_bind, Option.some_bind] at h ⊢

Result:
case some.succ
α : Type u_1
sel : Set α → Option α
s : Set α
n : ℕ
val✝ : α
hs : sel s = some val✝
m' : ℕ
hm : n + 1 ≤ m' + 1
h : enumerate sel (s \ {val✝}) n = none
⊢ enumerate sel (s \ {val✝}) m' = none

Proof state:
case some.succ
α : Type u_1
sel : Set α → Option α
s : Set α
n : ℕ
val✝ : α
hs : sel s = some val✝
m' : ℕ
hm : n + 1 ≤ m' + 1
h : enumerate sel (s \ {val✝}) n = none
⊢ enumerate sel (s \ {val✝}) m' = none

Tactic:
have hm : n ≤ m' := Nat.le_of_succ_le_succ hm

Result:
case some.succ
α : Type u_1
sel : Set α → Option α
s : Set α
n : ℕ
val✝ : α
hs : sel s = some val✝
m' : ℕ
hm✝ : n + 1 ≤ m' + 1
h : enumerate sel (s \ {val✝}) n = none
hm : n ≤ m'
⊢ enumerate sel (s \ {val✝}) m' = none

Proof state:
case some.zero
α : Type u_1
sel : Set α → Option α
s : Set α
n : ℕ
h : enumerate sel s (n + 1) = none
val✝ : α
hs : sel s = some val✝
hm : n + 1 ≤ 0
⊢ enumerate sel s 0 = none

Tactic:
contradiction

Result:
no goals

Proof state:
case none
α : Type u_1
sel : Set α → Option α
s : Set α
n m : ℕ
h : enumerate sel s (n + 1) = none
hm : n + 1 ≤ m
hs : sel s = none
⊢ enumerate sel s m = none

Tactic:
exact enumerate_eq_none_of_sel sel hs

Result:
no goals

Proof state:
α : Type u_1
sel : Set α → Option α
s : Set α
n m : ℕ
h : enumerate sel s (n + 1) = none
hm : n + 1 ≤ m
⊢ enumerate sel s m = none

Tactic:
cases hs : sel s

Result:
case none
α : Type u_1
sel : Set α → Option α
s : Set α
n m : ℕ
h : enumerate sel s (n + 1) = none
hm : n + 1 ≤ m
hs : sel s = none
⊢ enumerate sel s m = none

case some
α : Type u_1
sel : Set α → Option α
s : Set α
n m : ℕ
h : enumerate sel s (n + 1) = none
hm : n + 1 ≤ m
val✝ : α
hs : sel s = some val✝
⊢ enumerate sel s m = none

Proof state:
case some.succ
α : Type u_1
sel : Set α → Option α
s : Set α
n : ℕ
val✝ : α
hs : sel s = some val✝
m' : ℕ
hm✝ : n + 1 ≤ m' + 1
h : enumerate sel (s \ {val✝}) n = none
hm : n ≤ m'
⊢ enumerate sel (s \ {val✝}) m' = none

Tactic:
exact enumerate_eq_none h hm

Result:
no goals