[GOAL]
α : Type u_1
sel : Set α → Option α
s : Set α
h : sel s = none
⊢ enumerate sel s 0 = none
[PROOFSTEP]
simp [h, enumerate]
[GOAL]
α : Type u_1
sel : Set α → Option α
s : Set α
h : sel s = none
n : ℕ
⊢ enumerate sel s (n + 1) = none
[PROOFSTEP]
simp [h, enumerate]
[GOAL]
α : Type u_1
sel : Set α → Option α
s : Set α
h : sel s = none
n : ℕ
⊢ (do
      let a ← none
      enumerate sel (s \ {a}) n) =
    none
[PROOFSTEP]
rfl
[GOAL]
α : 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
[PROOFSTEP]
cases hs : sel s
[GOAL]
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
[PROOFSTEP]
exact enumerate_eq_none_of_sel sel hs
[GOAL]
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
[PROOFSTEP]
cases m
[GOAL]
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 ≤ Nat.zero
⊢ enumerate sel s Nat.zero = none
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✝
n✝ : ℕ
hm : n + 1 ≤ Nat.succ n✝
⊢ enumerate sel s (Nat.succ n✝) = none
[PROOFSTEP]
case zero => contradiction
[GOAL]
α : 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 ≤ Nat.zero
⊢ enumerate sel s Nat.zero = none
[PROOFSTEP]
case zero => contradiction
[GOAL]
α : 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 ≤ Nat.zero
⊢ enumerate sel s Nat.zero = none
[PROOFSTEP]
contradiction
[GOAL]
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✝
n✝ : ℕ
hm : n + 1 ≤ Nat.succ n✝
⊢ enumerate sel s (Nat.succ n✝) = none
[PROOFSTEP]
case succ m' =>
  simp [hs, enumerate] at h ⊢
  have hm : n ≤ m' := Nat.le_of_succ_le_succ hm
  exact enumerate_eq_none h hm
[GOAL]
α : 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 ≤ Nat.succ m'
⊢ enumerate sel s (Nat.succ m') = none
[PROOFSTEP]
case succ m' =>
  simp [hs, enumerate] at h ⊢
  have hm : n ≤ m' := Nat.le_of_succ_le_succ hm
  exact enumerate_eq_none h hm
[GOAL]
α : 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 ≤ Nat.succ m'
⊢ enumerate sel s (Nat.succ m') = none
[PROOFSTEP]
simp [hs, enumerate] at h ⊢
[GOAL]
α : Type u_1
sel : Set α → Option α
s : Set α
n : ℕ
val✝ : α
hs : sel s = some val✝
m' : ℕ
hm : n + 1 ≤ Nat.succ m'
h :
  (do
      let a ← some val✝
      enumerate sel (s \ {a}) n) =
    none
⊢ (do
      let a ← some val✝
      enumerate sel (s \ {a}) m') =
    none
[PROOFSTEP]
have hm : n ≤ m' := Nat.le_of_succ_le_succ hm
[GOAL]
α : Type u_1
sel : Set α → Option α
s : Set α
n : ℕ
val✝ : α
hs : sel s = some val✝
m' : ℕ
hm✝ : n + 1 ≤ Nat.succ m'
h :
  (do
      let a ← some val✝
      enumerate sel (s \ {a}) n) =
    none
hm : n ≤ m'
⊢ (do
      let a ← some val✝
      enumerate sel (s \ {a}) m') =
    none
[PROOFSTEP]
exact enumerate_eq_none h hm
[GOAL]
α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a : α
⊢ enumerate sel s (n + 1) = some a → a ∈ s
[PROOFSTEP]
cases h : sel s
[GOAL]
case none
α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a : α
h : sel s = none
⊢ enumerate sel s (n + 1) = some a → a ∈ s
case some
α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a val✝ : α
h : sel s = some val✝
⊢ enumerate sel s (n + 1) = some a → a ∈ s
[PROOFSTEP]
case none => simp [enumerate_eq_none_of_sel, h]
[GOAL]
α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a : α
h : sel s = none
⊢ enumerate sel s (n + 1) = some a → a ∈ s
[PROOFSTEP]
case none => simp [enumerate_eq_none_of_sel, h]
[GOAL]
α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a : α
h : sel s = none
⊢ enumerate sel s (n + 1) = some a → a ∈ s
[PROOFSTEP]
simp [enumerate_eq_none_of_sel, h]
[GOAL]
case some
α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a val✝ : α
h : sel s = some val✝
⊢ enumerate sel s (n + 1) = some a → a ∈ s
[PROOFSTEP]
case some a' =>
  simp [enumerate, h]
  exact fun h' : enumerate sel (s \ { a' }) n = some a ↦
    have : a ∈ s \ { a' } := enumerate_mem h_sel h'
    this.left
[GOAL]
α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a a' : α
h : sel s = some a'
⊢ enumerate sel s (n + 1) = some a → a ∈ s
[PROOFSTEP]
case some a' =>
  simp [enumerate, h]
  exact fun h' : enumerate sel (s \ { a' }) n = some a ↦
    have : a ∈ s \ { a' } := enumerate_mem h_sel h'
    this.left
[GOAL]
α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a a' : α
h : sel s = some a'
⊢ enumerate sel s (n + 1) = some a → a ∈ s
[PROOFSTEP]
simp [enumerate, h]
[GOAL]
α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a a' : α
h : sel s = some a'
⊢ (do
        let a ← some a'
        enumerate sel (s \ {a}) n) =
      some a →
    a ∈ s
[PROOFSTEP]
exact fun h' : enumerate sel (s \ { a' }) n = some a ↦
  have : a ∈ s \ { a' } := enumerate_mem h_sel h'
  this.left
[GOAL]
α : Type u_1
sel : Set α → Option α
n₁ n₂ : ℕ
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
h₁ : enumerate sel s n₁ = some a
h₂ : enumerate sel s n₂ = some a
⊢ n₁ = n₂
[PROOFSTEP]
rcases le_total n₁ n₂ with (hn | hn)
[GOAL]
case inl
α : Type u_1
sel : Set α → Option α
n₁ n₂ : ℕ
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
h₁ : enumerate sel s n₁ = some a
h₂ : enumerate sel s n₂ = some a
hn : n₁ ≤ n₂
⊢ n₁ = n₂
case inr
α : Type u_1
sel : Set α → Option α
n₁ n₂ : ℕ
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
h₁ : enumerate sel s n₁ = some a
h₂ : enumerate sel s n₂ = some a
hn : n₂ ≤ n₁
⊢ n₁ = n₂
[PROOFSTEP]
on_goal 2 => swap_var n₁ ↔ n₂, h₁ ↔ h₂
[GOAL]
case inl
α : Type u_1
sel : Set α → Option α
n₁ n₂ : ℕ
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
h₁ : enumerate sel s n₁ = some a
h₂ : enumerate sel s n₂ = some a
hn : n₁ ≤ n₂
⊢ n₁ = n₂
case inr
α : Type u_1
sel : Set α → Option α
n₁ n₂ : ℕ
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
h₁ : enumerate sel s n₁ = some a
h₂ : enumerate sel s n₂ = some a
hn : n₂ ≤ n₁
⊢ n₁ = n₂
[PROOFSTEP]
on_goal 2 => swap_var n₁ ↔ n₂, h₁ ↔ h₂
[GOAL]
case inr
α : Type u_1
sel : Set α → Option α
n₁ n₂ : ℕ
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
h₁ : enumerate sel s n₁ = some a
h₂ : enumerate sel s n₂ = some a
hn : n₂ ≤ n₁
⊢ n₁ = n₂
[PROOFSTEP]
swap_var n₁ ↔ n₂, h₁ ↔ h₂
[GOAL]
case inl
α : Type u_1
sel : Set α → Option α
n₁ n₂ : ℕ
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
h₁ : enumerate sel s n₁ = some a
h₂ : enumerate sel s n₂ = some a
hn : n₁ ≤ n₂
⊢ n₁ = n₂
case inr
α : Type u_1
sel : Set α → Option α
n₂ n₁ : ℕ
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
h₂ : enumerate sel s n₂ = some a
h₁ : enumerate sel s n₁ = some a
hn : n₁ ≤ n₂
⊢ n₂ = n₁
[PROOFSTEP]
all_goals
  rcases Nat.le.dest hn with ⟨m, rfl⟩
  clear hn
  induction n₁ generalizing s
  case zero =>
    cases m
    case zero => rfl
    case succ
      m =>
      have h' : enumerate sel (s \ { a }) m = some a := by simp_all only [enumerate, Nat.zero_eq, Nat.add_eq, zero_add];
        exact h₂
      have : a ∈ s \ { a } := enumerate_mem sel h_sel h'
      simp_all [Set.mem_diff_singleton]
  case succ k ih =>
    cases h : sel s
    case none => simp_all only [add_comm, self_eq_add_left, Nat.add_succ, enumerate_eq_none_of_sel _ h]
    case some
      _ =>
      simp_all only [add_comm, self_eq_add_left, enumerate, Option.some.injEq, Nat.add_succ, enumerate._eq_2,
        Nat.succ.injEq]
      exact ih h₁ h₂
[GOAL]
case inl
α : Type u_1
sel : Set α → Option α
n₁ n₂ : ℕ
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
h₁ : enumerate sel s n₁ = some a
h₂ : enumerate sel s n₂ = some a
hn : n₁ ≤ n₂
⊢ n₁ = n₂
[PROOFSTEP]
rcases Nat.le.dest hn with ⟨m, rfl⟩
[GOAL]
case inl.intro
α : Type u_1
sel : Set α → Option α
n₁ : ℕ
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
h₁ : enumerate sel s n₁ = some a
m : ℕ
h₂ : enumerate sel s (n₁ + m) = some a
hn : n₁ ≤ n₁ + m
⊢ n₁ = n₁ + m
[PROOFSTEP]
clear hn
[GOAL]
case inl.intro
α : Type u_1
sel : Set α → Option α
n₁ : ℕ
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
h₁ : enumerate sel s n₁ = some a
m : ℕ
h₂ : enumerate sel s (n₁ + m) = some a
⊢ n₁ = n₁ + m
[PROOFSTEP]
induction n₁ generalizing s
[GOAL]
case inl.intro.zero
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m : ℕ
s : Set α
h₁ : enumerate sel s Nat.zero = some a
h₂ : enumerate sel s (Nat.zero + m) = some a
⊢ Nat.zero = Nat.zero + m
case inl.intro.succ
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m n✝ : ℕ
n_ih✝ : ∀ {s : Set α}, enumerate sel s n✝ = some a → enumerate sel s (n✝ + m) = some a → n✝ = n✝ + m
s : Set α
h₁ : enumerate sel s (Nat.succ n✝) = some a
h₂ : enumerate sel s (Nat.succ n✝ + m) = some a
⊢ Nat.succ n✝ = Nat.succ n✝ + m
[PROOFSTEP]
case zero =>
  cases m
  case zero => rfl
  case succ
    m =>
    have h' : enumerate sel (s \ { a }) m = some a := by simp_all only [enumerate, Nat.zero_eq, Nat.add_eq, zero_add];
      exact h₂
    have : a ∈ s \ { a } := enumerate_mem sel h_sel h'
    simp_all [Set.mem_diff_singleton]
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m : ℕ
s : Set α
h₁ : enumerate sel s Nat.zero = some a
h₂ : enumerate sel s (Nat.zero + m) = some a
⊢ Nat.zero = Nat.zero + m
[PROOFSTEP]
case zero =>
  cases m
  case zero => rfl
  case succ
    m =>
    have h' : enumerate sel (s \ { a }) m = some a := by simp_all only [enumerate, Nat.zero_eq, Nat.add_eq, zero_add];
      exact h₂
    have : a ∈ s \ { a } := enumerate_mem sel h_sel h'
    simp_all [Set.mem_diff_singleton]
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m : ℕ
s : Set α
h₁ : enumerate sel s Nat.zero = some a
h₂ : enumerate sel s (Nat.zero + m) = some a
⊢ Nat.zero = Nat.zero + m
[PROOFSTEP]
cases m
[GOAL]
case zero
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
h₂ : enumerate sel s (Nat.zero + Nat.zero) = some a
⊢ Nat.zero = Nat.zero + Nat.zero
case succ
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
n✝ : ℕ
h₂ : enumerate sel s (Nat.zero + Nat.succ n✝) = some a
⊢ Nat.zero = Nat.zero + Nat.succ n✝
[PROOFSTEP]
case zero => rfl
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
h₂ : enumerate sel s (Nat.zero + Nat.zero) = some a
⊢ Nat.zero = Nat.zero + Nat.zero
[PROOFSTEP]
case zero => rfl
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
h₂ : enumerate sel s (Nat.zero + Nat.zero) = some a
⊢ Nat.zero = Nat.zero + Nat.zero
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
n✝ : ℕ
h₂ : enumerate sel s (Nat.zero + Nat.succ n✝) = some a
⊢ Nat.zero = Nat.zero + Nat.succ n✝
[PROOFSTEP]
case succ
  m =>
  have h' : enumerate sel (s \ { a }) m = some a := by simp_all only [enumerate, Nat.zero_eq, Nat.add_eq, zero_add];
    exact h₂
  have : a ∈ s \ { a } := enumerate_mem sel h_sel h'
  simp_all [Set.mem_diff_singleton]
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
m : ℕ
h₂ : enumerate sel s (Nat.zero + Nat.succ m) = some a
⊢ Nat.zero = Nat.zero + Nat.succ m
[PROOFSTEP]
case succ
  m =>
  have h' : enumerate sel (s \ { a }) m = some a := by simp_all only [enumerate, Nat.zero_eq, Nat.add_eq, zero_add];
    exact h₂
  have : a ∈ s \ { a } := enumerate_mem sel h_sel h'
  simp_all [Set.mem_diff_singleton]
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
m : ℕ
h₂ : enumerate sel s (Nat.zero + Nat.succ m) = some a
⊢ Nat.zero = Nat.zero + Nat.succ m
[PROOFSTEP]
have h' : enumerate sel (s \ { a }) m = some a := by simp_all only [enumerate, Nat.zero_eq, Nat.add_eq, zero_add];
  exact h₂
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
m : ℕ
h₂ : enumerate sel s (Nat.zero + Nat.succ m) = some a
⊢ enumerate sel (s \ {a}) m = some a
[PROOFSTEP]
simp_all only [enumerate, Nat.zero_eq, Nat.add_eq, zero_add]
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
m : ℕ
h₁ : sel s = some a
h₂ :
  (do
      let a ← some a
      enumerate sel (s \ {a}) m) =
    some a
⊢ enumerate sel (s \ {a}) m = some a
[PROOFSTEP]
exact h₂
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
m : ℕ
h₂ : enumerate sel s (Nat.zero + Nat.succ m) = some a
h' : enumerate sel (s \ {a}) m = some a
⊢ Nat.zero = Nat.zero + Nat.succ m
[PROOFSTEP]
have : a ∈ s \ { a } := enumerate_mem sel h_sel h'
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
m : ℕ
h₂ : enumerate sel s (Nat.zero + Nat.succ m) = some a
h' : enumerate sel (s \ {a}) m = some a
this : a ∈ s \ {a}
⊢ Nat.zero = Nat.zero + Nat.succ m
[PROOFSTEP]
simp_all [Set.mem_diff_singleton]
[GOAL]
case inl.intro.succ
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m n✝ : ℕ
n_ih✝ : ∀ {s : Set α}, enumerate sel s n✝ = some a → enumerate sel s (n✝ + m) = some a → n✝ = n✝ + m
s : Set α
h₁ : enumerate sel s (Nat.succ n✝) = some a
h₂ : enumerate sel s (Nat.succ n✝ + m) = some a
⊢ Nat.succ n✝ = Nat.succ n✝ + m
[PROOFSTEP]
case succ k ih =>
  cases h : sel s
  case none => simp_all only [add_comm, self_eq_add_left, Nat.add_succ, enumerate_eq_none_of_sel _ h]
  case some
    _ =>
    simp_all only [add_comm, self_eq_add_left, enumerate, Option.some.injEq, Nat.add_succ, enumerate._eq_2,
      Nat.succ.injEq]
    exact ih h₁ h₂
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k = k + m
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
⊢ Nat.succ k = Nat.succ k + m
[PROOFSTEP]
case succ k ih =>
  cases h : sel s
  case none => simp_all only [add_comm, self_eq_add_left, Nat.add_succ, enumerate_eq_none_of_sel _ h]
  case some
    _ =>
    simp_all only [add_comm, self_eq_add_left, enumerate, Option.some.injEq, Nat.add_succ, enumerate._eq_2,
      Nat.succ.injEq]
    exact ih h₁ h₂
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k = k + m
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
⊢ Nat.succ k = Nat.succ k + m
[PROOFSTEP]
cases h : sel s
[GOAL]
case none
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k = k + m
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
h : sel s = none
⊢ Nat.succ k = Nat.succ k + m
case some
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k = k + m
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
val✝ : α
h : sel s = some val✝
⊢ Nat.succ k = Nat.succ k + m
[PROOFSTEP]
case none => simp_all only [add_comm, self_eq_add_left, Nat.add_succ, enumerate_eq_none_of_sel _ h]
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k = k + m
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
h : sel s = none
⊢ Nat.succ k = Nat.succ k + m
[PROOFSTEP]
case none => simp_all only [add_comm, self_eq_add_left, Nat.add_succ, enumerate_eq_none_of_sel _ h]
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k = k + m
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
h : sel s = none
⊢ Nat.succ k = Nat.succ k + m
[PROOFSTEP]
simp_all only [add_comm, self_eq_add_left, Nat.add_succ, enumerate_eq_none_of_sel _ h]
[GOAL]
case some
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k = k + m
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
val✝ : α
h : sel s = some val✝
⊢ Nat.succ k = Nat.succ k + m
[PROOFSTEP]
case some
  _ =>
  simp_all only [add_comm, self_eq_add_left, enumerate, Option.some.injEq, Nat.add_succ, enumerate._eq_2,
    Nat.succ.injEq]
  exact ih h₁ h₂
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k = k + m
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
val✝ : α
h : sel s = some val✝
⊢ Nat.succ k = Nat.succ k + m
[PROOFSTEP]
case some
  _ =>
  simp_all only [add_comm, self_eq_add_left, enumerate, Option.some.injEq, Nat.add_succ, enumerate._eq_2,
    Nat.succ.injEq]
  exact ih h₁ h₂
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k = k + m
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
val✝ : α
h : sel s = some val✝
⊢ Nat.succ k = Nat.succ k + m
[PROOFSTEP]
simp_all only [add_comm, self_eq_add_left, enumerate, Option.some.injEq, Nat.add_succ, enumerate._eq_2, Nat.succ.injEq]
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
s : Set α
val✝ : α
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (m + k) = some a → m = 0
h₁ :
  (do
      let a ← some val✝
      enumerate sel (s \ {a}) k) =
    some a
h₂ :
  (do
      let a ← some val✝
      enumerate sel (s \ {a}) (m + k)) =
    some a
h : sel s = some val✝
⊢ m = 0
[PROOFSTEP]
exact ih h₁ h₂
[GOAL]
case inr
α : Type u_1
sel : Set α → Option α
n₂ n₁ : ℕ
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
h₂ : enumerate sel s n₂ = some a
h₁ : enumerate sel s n₁ = some a
hn : n₁ ≤ n₂
⊢ n₂ = n₁
[PROOFSTEP]
rcases Nat.le.dest hn with ⟨m, rfl⟩
[GOAL]
case inr.intro
α : Type u_1
sel : Set α → Option α
n₁ : ℕ
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
h₁ : enumerate sel s n₁ = some a
m : ℕ
h₂ : enumerate sel s (n₁ + m) = some a
hn : n₁ ≤ n₁ + m
⊢ n₁ + m = n₁
[PROOFSTEP]
clear hn
[GOAL]
case inr.intro
α : Type u_1
sel : Set α → Option α
n₁ : ℕ
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
h₁ : enumerate sel s n₁ = some a
m : ℕ
h₂ : enumerate sel s (n₁ + m) = some a
⊢ n₁ + m = n₁
[PROOFSTEP]
induction n₁ generalizing s
[GOAL]
case inr.intro.zero
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m : ℕ
s : Set α
h₁ : enumerate sel s Nat.zero = some a
h₂ : enumerate sel s (Nat.zero + m) = some a
⊢ Nat.zero + m = Nat.zero
case inr.intro.succ
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m n✝ : ℕ
n_ih✝ : ∀ {s : Set α}, enumerate sel s n✝ = some a → enumerate sel s (n✝ + m) = some a → n✝ + m = n✝
s : Set α
h₁ : enumerate sel s (Nat.succ n✝) = some a
h₂ : enumerate sel s (Nat.succ n✝ + m) = some a
⊢ Nat.succ n✝ + m = Nat.succ n✝
[PROOFSTEP]
case zero =>
  cases m
  case zero => rfl
  case succ
    m =>
    have h' : enumerate sel (s \ { a }) m = some a := by simp_all only [enumerate, Nat.zero_eq, Nat.add_eq, zero_add];
      exact h₂
    have : a ∈ s \ { a } := enumerate_mem sel h_sel h'
    simp_all [Set.mem_diff_singleton]
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m : ℕ
s : Set α
h₁ : enumerate sel s Nat.zero = some a
h₂ : enumerate sel s (Nat.zero + m) = some a
⊢ Nat.zero + m = Nat.zero
[PROOFSTEP]
case zero =>
  cases m
  case zero => rfl
  case succ
    m =>
    have h' : enumerate sel (s \ { a }) m = some a := by simp_all only [enumerate, Nat.zero_eq, Nat.add_eq, zero_add];
      exact h₂
    have : a ∈ s \ { a } := enumerate_mem sel h_sel h'
    simp_all [Set.mem_diff_singleton]
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m : ℕ
s : Set α
h₁ : enumerate sel s Nat.zero = some a
h₂ : enumerate sel s (Nat.zero + m) = some a
⊢ Nat.zero + m = Nat.zero
[PROOFSTEP]
cases m
[GOAL]
case zero
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
h₂ : enumerate sel s (Nat.zero + Nat.zero) = some a
⊢ Nat.zero + Nat.zero = Nat.zero
case succ
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
n✝ : ℕ
h₂ : enumerate sel s (Nat.zero + Nat.succ n✝) = some a
⊢ Nat.zero + Nat.succ n✝ = Nat.zero
[PROOFSTEP]
case zero => rfl
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
h₂ : enumerate sel s (Nat.zero + Nat.zero) = some a
⊢ Nat.zero + Nat.zero = Nat.zero
[PROOFSTEP]
case zero => rfl
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
h₂ : enumerate sel s (Nat.zero + Nat.zero) = some a
⊢ Nat.zero + Nat.zero = Nat.zero
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
n✝ : ℕ
h₂ : enumerate sel s (Nat.zero + Nat.succ n✝) = some a
⊢ Nat.zero + Nat.succ n✝ = Nat.zero
[PROOFSTEP]
case succ
  m =>
  have h' : enumerate sel (s \ { a }) m = some a := by simp_all only [enumerate, Nat.zero_eq, Nat.add_eq, zero_add];
    exact h₂
  have : a ∈ s \ { a } := enumerate_mem sel h_sel h'
  simp_all [Set.mem_diff_singleton]
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
m : ℕ
h₂ : enumerate sel s (Nat.zero + Nat.succ m) = some a
⊢ Nat.zero + Nat.succ m = Nat.zero
[PROOFSTEP]
case succ
  m =>
  have h' : enumerate sel (s \ { a }) m = some a := by simp_all only [enumerate, Nat.zero_eq, Nat.add_eq, zero_add];
    exact h₂
  have : a ∈ s \ { a } := enumerate_mem sel h_sel h'
  simp_all [Set.mem_diff_singleton]
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
m : ℕ
h₂ : enumerate sel s (Nat.zero + Nat.succ m) = some a
⊢ Nat.zero + Nat.succ m = Nat.zero
[PROOFSTEP]
have h' : enumerate sel (s \ { a }) m = some a := by simp_all only [enumerate, Nat.zero_eq, Nat.add_eq, zero_add];
  exact h₂
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
m : ℕ
h₂ : enumerate sel s (Nat.zero + Nat.succ m) = some a
⊢ enumerate sel (s \ {a}) m = some a
[PROOFSTEP]
simp_all only [enumerate, Nat.zero_eq, Nat.add_eq, zero_add]
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
m : ℕ
h₁ : sel s = some a
h₂ :
  (do
      let a ← some a
      enumerate sel (s \ {a}) m) =
    some a
⊢ enumerate sel (s \ {a}) m = some a
[PROOFSTEP]
exact h₂
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
m : ℕ
h₂ : enumerate sel s (Nat.zero + Nat.succ m) = some a
h' : enumerate sel (s \ {a}) m = some a
⊢ Nat.zero + Nat.succ m = Nat.zero
[PROOFSTEP]
have : a ∈ s \ { a } := enumerate_mem sel h_sel h'
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s Nat.zero = some a
m : ℕ
h₂ : enumerate sel s (Nat.zero + Nat.succ m) = some a
h' : enumerate sel (s \ {a}) m = some a
this : a ∈ s \ {a}
⊢ Nat.zero + Nat.succ m = Nat.zero
[PROOFSTEP]
simp_all [Set.mem_diff_singleton]
[GOAL]
case inr.intro.succ
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m n✝ : ℕ
n_ih✝ : ∀ {s : Set α}, enumerate sel s n✝ = some a → enumerate sel s (n✝ + m) = some a → n✝ + m = n✝
s : Set α
h₁ : enumerate sel s (Nat.succ n✝) = some a
h₂ : enumerate sel s (Nat.succ n✝ + m) = some a
⊢ Nat.succ n✝ + m = Nat.succ n✝
[PROOFSTEP]
case succ k ih =>
  cases h : sel s
  case none => simp_all only [add_comm, self_eq_add_left, Nat.add_succ, enumerate_eq_none_of_sel _ h]
  case some
    _ =>
    simp_all only [add_comm, self_eq_add_left, enumerate, Option.some.injEq, Nat.add_succ, enumerate._eq_2,
      Nat.succ.injEq]
    exact ih h₁ h₂
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k + m = k
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
⊢ Nat.succ k + m = Nat.succ k
[PROOFSTEP]
case succ k ih =>
  cases h : sel s
  case none => simp_all only [add_comm, self_eq_add_left, Nat.add_succ, enumerate_eq_none_of_sel _ h]
  case some
    _ =>
    simp_all only [add_comm, self_eq_add_left, enumerate, Option.some.injEq, Nat.add_succ, enumerate._eq_2,
      Nat.succ.injEq]
    exact ih h₁ h₂
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k + m = k
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
⊢ Nat.succ k + m = Nat.succ k
[PROOFSTEP]
cases h : sel s
[GOAL]
case none
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k + m = k
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
h : sel s = none
⊢ Nat.succ k + m = Nat.succ k
case some
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k + m = k
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
val✝ : α
h : sel s = some val✝
⊢ Nat.succ k + m = Nat.succ k
[PROOFSTEP]
case none => simp_all only [add_comm, self_eq_add_left, Nat.add_succ, enumerate_eq_none_of_sel _ h]
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k + m = k
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
h : sel s = none
⊢ Nat.succ k + m = Nat.succ k
[PROOFSTEP]
case none => simp_all only [add_comm, self_eq_add_left, Nat.add_succ, enumerate_eq_none_of_sel _ h]
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k + m = k
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
h : sel s = none
⊢ Nat.succ k + m = Nat.succ k
[PROOFSTEP]
simp_all only [add_comm, self_eq_add_left, Nat.add_succ, enumerate_eq_none_of_sel _ h]
[GOAL]
case some
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k + m = k
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
val✝ : α
h : sel s = some val✝
⊢ Nat.succ k + m = Nat.succ k
[PROOFSTEP]
case some
  _ =>
  simp_all only [add_comm, self_eq_add_left, enumerate, Option.some.injEq, Nat.add_succ, enumerate._eq_2,
    Nat.succ.injEq]
  exact ih h₁ h₂
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k + m = k
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
val✝ : α
h : sel s = some val✝
⊢ Nat.succ k + m = Nat.succ k
[PROOFSTEP]
case some
  _ =>
  simp_all only [add_comm, self_eq_add_left, enumerate, Option.some.injEq, Nat.add_succ, enumerate._eq_2,
    Nat.succ.injEq]
  exact ih h₁ h₂
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k + m = k
s : Set α
h₁ : enumerate sel s (Nat.succ k) = some a
h₂ : enumerate sel s (Nat.succ k + m) = some a
val✝ : α
h : sel s = some val✝
⊢ Nat.succ k + m = Nat.succ k
[PROOFSTEP]
simp_all only [add_comm, self_eq_add_left, enumerate, Option.some.injEq, Nat.add_succ, enumerate._eq_2, Nat.succ.injEq]
[GOAL]
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
s : Set α
val✝ : α
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (m + k) = some a → m + k = k
h₁ :
  (do
      let a ← some val✝
      enumerate sel (s \ {a}) k) =
    some a
h₂ :
  (do
      let a ← some val✝
      enumerate sel (s \ {a}) (m + k)) =
    some a
h : sel s = some val✝
⊢ m + k = k
[PROOFSTEP]
exact ih h₁ h₂
