-- Mathlib/Data/Set/Enumerate.lean
theorem enumerate_inj {n₁ n₂ : ℕ} {a : α} {s : Set α} (h_sel : ∀ s a, sel s = some a → a ∈ s)
    (h₁ : enumerate sel s n₁ = some a) (h₂ : enumerate sel s n₂ = some a) : n₁ = n₂

Proof state:
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₁

Tactic:
rcases Nat.le.dest hn with ⟨m, rfl⟩

Result:
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₁

Proof state:
case inr.intro.succ.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 (k + 1) = some a
h₂ : enumerate sel s (k + 1 + m) = some a
h : sel s = none
⊢ k + 1 + m = k + 1

Tactic:
simp_all only [add_comm, self_eq_add_left, Nat.add_succ, enumerate_eq_none_of_sel _ h,
  reduceCtorEq]

Result:
no goals

Proof state:
case inr.intro.succ
α : 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 (k + 1) = some a
h₂ : enumerate sel s (k + 1 + m) = some a
⊢ k + 1 + m = k + 1

Tactic:
cases h : sel s with
| none =>
  simp_all only [add_comm, self_eq_add_left, Nat.add_succ, enumerate_eq_none_of_sel _ h,
    reduceCtorEq]
| some =>
  simp_all only [add_comm, self_eq_add_left, enumerate, Option.some.injEq,
                 Nat.add_succ, Nat.succ.injEq]
  exact ih h₁ h₂

Result:
no goals

Proof state:
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₁

Tactic:
all_goals
  rcases Nat.le.dest hn with ⟨m, rfl⟩
  clear hn
  induction n₁ generalizing s with
  | zero =>
    cases m with
    | zero => rfl
    | succ m =>
      have h' : enumerate sel (s \ {a}) m = some a := by
        simp_all only [enumerate, Nat.add_eq, zero_add]; exact h₂
      have : a ∈ s \ {a} := enumerate_mem sel h_sel h'
      simp_all [Set.mem_diff_singleton]
  | succ k ih =>
    cases h : sel s with
    
    | none =>
      simp_all only [add_comm, self_eq_add_left, Nat.add_succ, enumerate_eq_none_of_sel _ h,
        reduceCtorEq]
    | some =>
      simp_all only [add_comm, self_eq_add_left, enumerate, Option.some.injEq,
                     Nat.add_succ, Nat.succ.injEq]
      exact ih h₁ h₂

Result:
no goals

Proof state:
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s 0 = some a
m : ℕ
h₂ : enumerate sel s (0 + (m + 1)) = some a
⊢ enumerate sel (s \ {a}) m = some a

Tactic:
simp_all only [enumerate, Nat.add_eq, zero_add]

Result:
α : 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

Proof state:
α : 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₂

Tactic:
rcases le_total n₁ n₂ with (hn|hn)

Result:
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₂

Proof state:
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₁

Tactic:
clear hn

Result:
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₁

Proof state:
case inr.intro.zero.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 0 = some a
m : ℕ
h₂ : enumerate sel s (0 + (m + 1)) = some a
⊢ 0 + (m + 1) = 0

Tactic:
have h' : enumerate sel (s \ {a}) m = some a := by
  simp_all only [enumerate, Nat.add_eq, zero_add]; exact h₂

Result:
case inr.intro.zero.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 0 = some a
m : ℕ
h₂ : enumerate sel s (0 + (m + 1)) = some a
h' : enumerate sel (s \ {a}) m = some a
⊢ 0 + (m + 1) = 0

Proof state:
case inr.intro.succ.some
α : 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

Tactic:
exact ih h₁ h₂

Result:
no goals

Proof state:
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₁

Tactic:
induction n₁ generalizing s with
| zero =>
  cases m with
  | zero => rfl
  | succ m =>
    have h' : enumerate sel (s \ {a}) m = some a := by
      simp_all only [enumerate, Nat.add_eq, zero_add]; exact h₂
    have : a ∈ s \ {a} := enumerate_mem sel h_sel h'
    simp_all [Set.mem_diff_singleton]
| succ k ih =>
  cases h : sel s with
  
  | none =>
    simp_all only [add_comm, self_eq_add_left, Nat.add_succ, enumerate_eq_none_of_sel _ h,
      reduceCtorEq]
  | some =>
    simp_all only [add_comm, self_eq_add_left, enumerate, Option.some.injEq,
                   Nat.add_succ, Nat.succ.injEq]
    exact ih h₁ h₂

Result:
no goals

Proof state:
case inr.intro.zero.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 0 = some a
h₂ : enumerate sel s (0 + 0) = some a
⊢ 0 + 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
case inr.intro.zero.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 0 = some a
m : ℕ
h₂ : enumerate sel s (0 + (m + 1)) = some a
h' : enumerate sel (s \ {a}) m = some a
this : a ∈ s \ {a}
⊢ 0 + (m + 1) = 0

Tactic:
simp_all [Set.mem_diff_singleton]

Result:
no goals

Proof state:
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 0 = some a
h₂ : enumerate sel s (0 + m) = some a
⊢ 0 + m = 0

Tactic:
cases m with
| zero => rfl
| succ m =>
  have h' : enumerate sel (s \ {a}) m = some a := by
    simp_all only [enumerate, Nat.add_eq, zero_add]; exact h₂
  have : a ∈ s \ {a} := enumerate_mem sel h_sel h'
  simp_all [Set.mem_diff_singleton]

Result:
no goals