no goals
i : Nat
α✝ : Type u_1
xs : List α✝
j : Nat
h₀ : i < length xs
h₁ : Nodup xs
h₂ : get? xs i = get? xs j
⊢ i = j
induction xs generalizing i j with
| nil => cases h₀
| cons x xs ih =>
  match i, j with
  | 0, 0 => rfl
  | i+1, j+1 => simp; cases h₁ with
    | cons ha h₁ => exact ih (Nat.lt_of_succ_lt_succ h₀) h₁ h₂
  | i+1, 0 => ?_ | 0, j+1 => ?_
  all_goals
    simp at h₂
    cases h₁; rename_i h' h
    have := h x ?_ rfl; cases this
    rw [mem_iff_get?]
  exact ⟨_, h₂⟩; exact ⟨_ , h₂.symm⟩
no goals
case nil
α✝ : Type u_1
i j : Nat
h₀ : i < length []
h₁ : Nodup []
h₂ : get? [] i = get? [] j
⊢ i = j
cases h₀
case cons.refine_1
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {i j : Nat}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
i✝ j : Nat
h₁ : Nodup (x :: xs)
i : Nat
h₀ : i + 1 < length (x :: xs)
h₂ : get? (x :: xs) (i + 1) = get? (x :: xs) 0
⊢ i + 1 = 0

case cons.refine_2
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {i j : Nat}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
i j✝ : Nat
h₁ : Nodup (x :: xs)
j : Nat
h₀ : 0 < length (x :: xs)
h₂ : get? (x :: xs) 0 = get? (x :: xs) (j + 1)
⊢ 0 = j + 1
case cons
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {i j : Nat}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
i j : Nat
h₀ : i < length (x :: xs)
h₁ : Nodup (x :: xs)
h₂ : get? (x :: xs) i = get? (x :: xs) j
⊢ i = j
match i, j with
| 0, 0 => rfl
| i+1, j+1 => simp; cases h₁ with
  | cons ha h₁ => exact ih (Nat.lt_of_succ_lt_succ h₀) h₁ h₂
| i+1, 0 => ?_ | 0, j+1 => ?_
case cons.refine_1.cons.refine_1
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {i j : Nat}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
i✝ j i : Nat
h₀ : i + 1 < length (x :: xs)
h₂ : get? xs i = some x
h' : Pairwise (fun x x_1 => x ≠ x_1) xs
h : ∀ (a' : α✝), a' ∈ xs → x ≠ a'
⊢ ∃ n, get? xs n = some x

case cons.refine_2.cons.refine_1
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {i j : Nat}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
i j✝ j : Nat
h₀ : 0 < length (x :: xs)
h₂ : some x = get? xs j
h' : Pairwise (fun x x_1 => x ≠ x_1) xs
h : ∀ (a' : α✝), a' ∈ xs → x ≠ a'
⊢ ∃ n, get? xs n = some x
case cons.refine_1
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {i j : Nat}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
i✝ j : Nat
h₁ : Nodup (x :: xs)
i : Nat
h₀ : i + 1 < length (x :: xs)
h₂ : get? (x :: xs) (i + 1) = get? (x :: xs) 0
⊢ i + 1 = 0

case cons.refine_2
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {i j : Nat}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
i j✝ : Nat
h₁ : Nodup (x :: xs)
j : Nat
h₀ : 0 < length (x :: xs)
h₂ : get? (x :: xs) 0 = get? (x :: xs) (j + 1)
⊢ 0 = j + 1
all_goals
  simp at h₂
  cases h₁; rename_i h' h
  have := h x ?_ rfl; cases this
  rw [mem_iff_get?]
case cons.refine_2.cons.refine_1
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {i j : Nat}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
i j✝ j : Nat
h₀ : 0 < length (x :: xs)
h₂ : some x = get? xs j
h' : Pairwise (fun x x_1 => x ≠ x_1) xs
h : ∀ (a' : α✝), a' ∈ xs → x ≠ a'
⊢ ∃ n, get? xs n = some x
case cons.refine_1.cons.refine_1
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {i j : Nat}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
i✝ j i : Nat
h₀ : i + 1 < length (x :: xs)
h₂ : get? xs i = some x
h' : Pairwise (fun x x_1 => x ≠ x_1) xs
h : ∀ (a' : α✝), a' ∈ xs → x ≠ a'
⊢ ∃ n, get? xs n = some x

case cons.refine_2.cons.refine_1
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {i j : Nat}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
i j✝ j : Nat
h₀ : 0 < length (x :: xs)
h₂ : some x = get? xs j
h' : Pairwise (fun x x_1 => x ≠ x_1) xs
h : ∀ (a' : α✝), a' ∈ xs → x ≠ a'
⊢ ∃ n, get? xs n = some x
exact ⟨_, h₂⟩
no goals
case cons.refine_2.cons.refine_1
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {i j : Nat}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
i j✝ j : Nat
h₀ : 0 < length (x :: xs)
h₂ : some x = get? xs j
h' : Pairwise (fun x x_1 => x ≠ x_1) xs
h : ∀ (a' : α✝), a' ∈ xs → x ≠ a'
⊢ ∃ n, get? xs n = some x
exact ⟨_ , h₂.symm⟩
no goals
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {i j : Nat}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
i j : Nat
h₁ : Nodup (x :: xs)
h₀ : 0 < length (x :: xs)
h₂ : get? (x :: xs) 0 = get? (x :: xs) 0
⊢ 0 = 0
rfl
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {i j : Nat}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
i✝ j✝ : Nat
h₁ : Nodup (x :: xs)
i j : Nat
h₀ : i + 1 < length (x :: xs)
h₂ : get? (x :: xs) (i + 1) = get? (x :: xs) (j + 1)
⊢ i = j
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {i j : Nat}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
i✝ j✝ : Nat
h₁ : Nodup (x :: xs)
i j : Nat
h₀ : i + 1 < length (x :: xs)
h₂ : get? (x :: xs) (i + 1) = get? (x :: xs) (j + 1)
⊢ i + 1 = j + 1
simp
no goals
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {i j : Nat}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
i✝ j✝ : Nat
h₁ : Nodup (x :: xs)
i j : Nat
h₀ : i + 1 < length (x :: xs)
h₂ : get? (x :: xs) (i + 1) = get? (x :: xs) (j + 1)
⊢ i = j
cases h₁ with
| cons ha h₁ => exact ih (Nat.lt_of_succ_lt_succ h₀) h₁ h₂
no goals
case cons
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {i j : Nat}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
i✝ j✝ i j : Nat
h₀ : i + 1 < length (x :: xs)
h₂ : get? (x :: xs) (i + 1) = get? (x :: xs) (j + 1)
h₁ : Pairwise (fun x x_1 => x ≠ x_1) xs
ha : ∀ (a' : α✝), a' ∈ xs → x ≠ a'
⊢ i = j
exact ih (Nat.lt_of_succ_lt_succ h₀) h₁ h₂
case cons.refine_2
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {i j : Nat}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
i j✝ : Nat
h₁ : Nodup (x :: xs)
j : Nat
h₀ : 0 < length (x :: xs)
h₂ : some x = get? xs j
⊢ 0 = j + 1
case cons.refine_2
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {i j : Nat}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
i j✝ : Nat
h₁ : Nodup (x :: xs)
j : Nat
h₀ : 0 < length (x :: xs)
h₂ : get? (x :: xs) 0 = get? (x :: xs) (j + 1)
⊢ 0 = j + 1
simp at h₂
case cons.refine_2.cons
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {i j : Nat}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
i j✝ j : Nat
h₀ : 0 < length (x :: xs)
h₂ : some x = get? xs j
a✝¹ : Pairwise (fun x x_1 => x ≠ x_1) xs
a✝ : ∀ (a' : α✝), a' ∈ xs → x ≠ a'
⊢ 0 = j + 1
case cons.refine_2
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {i j : Nat}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
i j✝ : Nat
h₁ : Nodup (x :: xs)
j : Nat
h₀ : 0 < length (x :: xs)
h₂ : some x = get? xs j
⊢ 0 = j + 1
cases h₁
case cons.refine_2.cons
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {i j : Nat}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
i j✝ j : Nat
h₀ : 0 < length (x :: xs)
h₂ : some x = get? xs j
h' : Pairwise (fun x x_1 => x ≠ x_1) xs
h : ∀ (a' : α✝), a' ∈ xs → x ≠ a'
⊢ 0 = j + 1
case cons.refine_2.cons
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {i j : Nat}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
i j✝ j : Nat
h₀ : 0 < length (x :: xs)
h₂ : some x = get? xs j
a✝¹ : Pairwise (fun x x_1 => x ≠ x_1) xs
a✝ : ∀ (a' : α✝), a' ∈ xs → x ≠ a'
⊢ 0 = j + 1
rename_i h' h
case cons.refine_2.cons.refine_2
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {i j : Nat}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
i j✝ j : Nat
h₀ : 0 < length (x :: xs)
h₂ : some x = get? xs j
h' : Pairwise (fun x x_1 => x ≠ x_1) xs
h : ∀ (a' : α✝), a' ∈ xs → x ≠ a'
this : False
⊢ 0 = j + 1

case cons.refine_2.cons.refine_1
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {i j : Nat}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
i j✝ j : Nat
h₀ : 0 < length (x :: xs)
h₂ : some x = get? xs j
h' : Pairwise (fun x x_1 => x ≠ x_1) xs
h : ∀ (a' : α✝), a' ∈ xs → x ≠ a'
⊢ x ∈ xs
case cons.refine_2.cons
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {i j : Nat}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
i j✝ j : Nat
h₀ : 0 < length (x :: xs)
h₂ : some x = get? xs j
h' : Pairwise (fun x x_1 => x ≠ x_1) xs
h : ∀ (a' : α✝), a' ∈ xs → x ≠ a'
⊢ 0 = j + 1
have := h x ?_ rfl
case cons.refine_2.cons.refine_1
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {i j : Nat}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
i j✝ j : Nat
h₀ : 0 < length (x :: xs)
h₂ : some x = get? xs j
h' : Pairwise (fun x x_1 => x ≠ x_1) xs
h : ∀ (a' : α✝), a' ∈ xs → x ≠ a'
⊢ x ∈ xs
case cons.refine_2.cons.refine_2
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {i j : Nat}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
i j✝ j : Nat
h₀ : 0 < length (x :: xs)
h₂ : some x = get? xs j
h' : Pairwise (fun x x_1 => x ≠ x_1) xs
h : ∀ (a' : α✝), a' ∈ xs → x ≠ a'
this : False
⊢ 0 = j + 1

case cons.refine_2.cons.refine_1
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {i j : Nat}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
i j✝ j : Nat
h₀ : 0 < length (x :: xs)
h₂ : some x = get? xs j
h' : Pairwise (fun x x_1 => x ≠ x_1) xs
h : ∀ (a' : α✝), a' ∈ xs → x ≠ a'
⊢ x ∈ xs
cases this
case cons.refine_2.cons.refine_1
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {i j : Nat}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
i j✝ j : Nat
h₀ : 0 < length (x :: xs)
h₂ : some x = get? xs j
h' : Pairwise (fun x x_1 => x ≠ x_1) xs
h : ∀ (a' : α✝), a' ∈ xs → x ≠ a'
⊢ ∃ n, get? xs n = some x
case cons.refine_2.cons.refine_1
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {i j : Nat}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
i j✝ j : Nat
h₀ : 0 < length (x :: xs)
h₂ : some x = get? xs j
h' : Pairwise (fun x x_1 => x ≠ x_1) xs
h : ∀ (a' : α✝), a' ∈ xs → x ≠ a'
⊢ x ∈ xs
rw [mem_iff_get?]