-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Pairwise.lean
theorem getElem?_inj {xs : List α}
    (h₀ : i < xs.length) (h₁ : Nodup xs) (h₂ : xs[i]? = xs[j]?) : i = j

Proof state:
case nil
α : Type u_1
i j : Nat
h₀ : i < [].length
h₁ : [].Nodup
h₂ : [][i]? = [][j]?
⊢ i = j

Tactic:
cases h₀

Result:
no goals

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

Tactic:
simp only [get?_eq_getElem?]

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

Proof state:
case cons.refine_2.cons.refine_1
α : Type u_1
x : α
xs : List α
ih : ∀ {i j : Nat}, i < xs.length → xs.Nodup → xs[i]? = xs[j]? → i = j
i j✝ j : Nat
h₀ : 0 < (x :: xs).length
h₂ : some x = xs[j]?
h' : Pairwise (fun x1 x2 => x1 ≠ x2) xs
h : ∀ (a' : α), a' ∈ xs → x ≠ a'
⊢ x ∈ xs

Tactic:
rw [mem_iff_get?]

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

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

Tactic:
exact ⟨_ , h₂.symm⟩

Result:
no goals

Proof state:
α : Type u_1
x : α
xs : List α
ih : ∀ {i j : Nat}, i < xs.length → xs.Nodup → xs[i]? = xs[j]? → i = j
i j : Nat
h₁ : (x :: xs).Nodup
h₀ : 0 < (x :: xs).length
h₂ : (x :: xs)[0]? = (x :: xs)[0]?
⊢ 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
case cons.refine_2
α : Type u_1
x : α
xs : List α
ih : ∀ {i j : Nat}, i < xs.length → xs.Nodup → xs[i]? = xs[j]? → i = j
i j✝ : Nat
h₁ : (x :: xs).Nodup
j : Nat
h₀ : 0 < (x :: xs).length
h₂ : (x :: xs)[0]? = (x :: xs)[j + 1]?
⊢ 0 = j + 1

Tactic:
simp only [get?_eq_getElem?, getElem?_cons_zero, getElem?_cons_succ] at h₂

Result:
case cons.refine_2
α : Type u_1
x : α
xs : List α
ih : ∀ {i j : Nat}, i < xs.length → xs.Nodup → xs[i]? = xs[j]? → i = j
i j✝ : Nat
h₁ : (x :: xs).Nodup
j : Nat
h₀ : 0 < (x :: xs).length
h₂ : some x = xs[j]?
⊢ 0 = j + 1

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

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

Tactic:
exact ⟨_, h₂⟩

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

Proof state:
case cons.refine_2.cons.refine_2
α : Type u_1
x : α
xs : List α
ih : ∀ {i j : Nat}, i < xs.length → xs.Nodup → xs[i]? = xs[j]? → i = j
i j✝ j : Nat
h₀ : 0 < (x :: xs).length
h₂ : some x = xs[j]?
h' : Pairwise (fun x1 x2 => x1 ≠ x2) 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 < xs.length → xs.Nodup → xs[i]? = xs[j]? → i = j
i j✝ j : Nat
h₀ : 0 < (x :: xs).length
h₂ : some x = xs[j]?
h' : Pairwise (fun x1 x2 => x1 ≠ x2) xs
h : ∀ (a' : α), a' ∈ xs → x ≠ a'
⊢ x ∈ xs

Tactic:
cases this

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

Proof state:
case cons.refine_2.cons
α : Type u_1
x : α
xs : List α
ih : ∀ {i j : Nat}, i < xs.length → xs.Nodup → xs[i]? = xs[j]? → i = j
i j✝ j : Nat
h₀ : 0 < (x :: xs).length
h₂ : some x = xs[j]?
h' : Pairwise (fun x1 x2 => x1 ≠ x2) xs
h : ∀ (a' : α), a' ∈ xs → x ≠ a'
⊢ 0 = j + 1

Tactic:
have := h x ?_ rfl

Result:
case cons.refine_2.cons.refine_2
α : Type u_1
x : α
xs : List α
ih : ∀ {i j : Nat}, i < xs.length → xs.Nodup → xs[i]? = xs[j]? → i = j
i j✝ j : Nat
h₀ : 0 < (x :: xs).length
h₂ : some x = xs[j]?
h' : Pairwise (fun x1 x2 => x1 ≠ x2) 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 < xs.length → xs.Nodup → xs[i]? = xs[j]? → i = j
i j✝ j : Nat
h₀ : 0 < (x :: xs).length
h₂ : some x = xs[j]?
h' : Pairwise (fun x1 x2 => x1 ≠ x2) xs
h : ∀ (a' : α), a' ∈ xs → x ≠ a'
⊢ x ∈ xs

Proof state:
case cons.refine_2
α : Type u_1
x : α
xs : List α
ih : ∀ {i j : Nat}, i < xs.length → xs.Nodup → xs[i]? = xs[j]? → i = j
i j✝ : Nat
h₁ : (x :: xs).Nodup
j : Nat
h₀ : 0 < (x :: xs).length
h₂ : some x = xs[j]?
⊢ 0 = j + 1

Tactic:
cases h₁

Result:
case cons.refine_2.cons
α : Type u_1
x : α
xs : List α
ih : ∀ {i j : Nat}, i < xs.length → xs.Nodup → xs[i]? = xs[j]? → i = j
i j✝ j : Nat
h₀ : 0 < (x :: xs).length
h₂ : some x = xs[j]?
a✝¹ : Pairwise (fun x1 x2 => x1 ≠ x2) xs
a✝ : ∀ (a' : α), a' ∈ xs → x ≠ a'
⊢ 0 = j + 1

Proof state:
case cons.refine_2.cons
α : Type u_1
x : α
xs : List α
ih : ∀ {i j : Nat}, i < xs.length → xs.Nodup → xs[i]? = xs[j]? → i = j
i j✝ j : Nat
h₀ : 0 < (x :: xs).length
h₂ : some x = xs[j]?
a✝¹ : Pairwise (fun x1 x2 => x1 ≠ x2) xs
a✝ : ∀ (a' : α), a' ∈ xs → x ≠ a'
⊢ 0 = j + 1

Tactic:
rename_i h' h

Result:
case cons.refine_2.cons
α : Type u_1
x : α
xs : List α
ih : ∀ {i j : Nat}, i < xs.length → xs.Nodup → xs[i]? = xs[j]? → i = j
i j✝ j : Nat
h₀ : 0 < (x :: xs).length
h₂ : some x = xs[j]?
h' : Pairwise (fun x1 x2 => x1 ≠ x2) xs
h : ∀ (a' : α), a' ∈ xs → x ≠ a'
⊢ 0 = j + 1

Proof state:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ {i j : Nat}, i < xs.length → xs.Nodup → xs[i]? = xs[j]? → i = j
i✝ j✝ i j : Nat
h₀ : i + 1 < (x :: xs).length
h₂ : (x :: xs)[i + 1]? = (x :: xs)[j + 1]?
h₁ : Pairwise (fun x1 x2 => x1 ≠ x2) xs
ha : ∀ (a' : α), a' ∈ xs → x ≠ a'
⊢ i + 1 = j + 1

Tactic:
simp only [getElem?_cons_succ] at h₂

Result:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ {i j : Nat}, i < xs.length → xs.Nodup → xs[i]? = xs[j]? → i = j
i✝ j✝ i j : Nat
h₀ : i + 1 < (x :: xs).length
h₁ : Pairwise (fun x1 x2 => x1 ≠ x2) xs
ha : ∀ (a' : α), a' ∈ xs → x ≠ a'
h₂ : xs[i]? = xs[j]?
⊢ i + 1 = j + 1