no goals
case nil
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
i j : ℕ
h₀ : i < length []
h₁ : Nodup []
h₂ : get? [] i = get? [] j
⊢ i = j
cases h₀
case cons.zero.zero
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
h₁ : Nodup (x :: xs)
h₀ : zero < length (x :: xs)
h₂ : get? (x :: xs) zero = get? (x :: xs) zero
⊢ zero = zero

case cons.zero.succ
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
h₁ : Nodup (x :: xs)
h₀ : zero < length (x :: xs)
n✝ : ℕ
h₂ : get? (x :: xs) zero = get? (x :: xs) (succ n✝)
⊢ zero = succ n✝

case cons.succ.zero
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
h₁ : Nodup (x :: xs)
n✝ : ℕ
h₀ : succ n✝ < length (x :: xs)
h₂ : get? (x :: xs) (succ n✝) = get? (x :: xs) zero
⊢ succ n✝ = zero

case cons.succ.succ
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
h₁ : Nodup (x :: xs)
n✝¹ : ℕ
h₀ : succ n✝¹ < length (x :: xs)
n✝ : ℕ
h₂ : get? (x :: xs) (succ n✝¹) = get? (x :: xs) (succ n✝)
⊢ succ n✝¹ = succ n✝
case cons
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
i j : ℕ
h₀ : i < length (x :: xs)
h₁ : Nodup (x :: xs)
h₂ : get? (x :: xs) i = get? (x :: xs) j
⊢ i = j
cases i <;> cases j
case cons.zero.succ
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
h₁ : Nodup (x :: xs)
h₀ : zero < length (x :: xs)
n✝ : ℕ
h₂ : get? (x :: xs) zero = get? (x :: xs) (succ n✝)
⊢ zero = succ n✝

case cons.succ.zero
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
h₁ : Nodup (x :: xs)
n✝ : ℕ
h₀ : succ n✝ < length (x :: xs)
h₂ : get? (x :: xs) (succ n✝) = get? (x :: xs) zero
⊢ succ n✝ = zero

case cons.succ.succ
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
h₁ : Nodup (x :: xs)
n✝¹ : ℕ
h₀ : succ n✝¹ < length (x :: xs)
n✝ : ℕ
h₂ : get? (x :: xs) (succ n✝¹) = get? (x :: xs) (succ n✝)
⊢ succ n✝¹ = succ n✝
case cons.zero.zero
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
h₁ : Nodup (x :: xs)
h₀ : zero < length (x :: xs)
h₂ : get? (x :: xs) zero = get? (x :: xs) zero
⊢ zero = zero

case cons.zero.succ
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
h₁ : Nodup (x :: xs)
h₀ : zero < length (x :: xs)
n✝ : ℕ
h₂ : get? (x :: xs) zero = get? (x :: xs) (succ n✝)
⊢ zero = succ n✝

case cons.succ.zero
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
h₁ : Nodup (x :: xs)
n✝ : ℕ
h₀ : succ n✝ < length (x :: xs)
h₂ : get? (x :: xs) (succ n✝) = get? (x :: xs) zero
⊢ succ n✝ = zero

case cons.succ.succ
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
h₁ : Nodup (x :: xs)
n✝¹ : ℕ
h₀ : succ n✝¹ < length (x :: xs)
n✝ : ℕ
h₂ : get? (x :: xs) (succ n✝¹) = get? (x :: xs) (succ n✝)
⊢ succ n✝¹ = succ n✝
case zero.zero => rfl
case cons.zero.succ
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
h₁ : Nodup (x :: xs)
h₀ : zero < length (x :: xs)
n✝ : ℕ
h₂ : get? (x :: xs) zero = get? (x :: xs) (succ n✝)
⊢ zero = succ n✝

case cons.succ.zero
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
h₁ : Nodup (x :: xs)
n✝ : ℕ
h₀ : succ n✝ < length (x :: xs)
h₂ : get? (x :: xs) (succ n✝) = get? (x :: xs) zero
⊢ succ n✝ = zero
case cons.zero.succ
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
h₁ : Nodup (x :: xs)
h₀ : zero < length (x :: xs)
n✝ : ℕ
h₂ : get? (x :: xs) zero = get? (x :: xs) (succ n✝)
⊢ zero = succ n✝

case cons.succ.zero
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
h₁ : Nodup (x :: xs)
n✝ : ℕ
h₀ : succ n✝ < length (x :: xs)
h₂ : get? (x :: xs) (succ n✝) = get? (x :: xs) zero
⊢ succ n✝ = zero

case cons.succ.succ
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
h₁ : Nodup (x :: xs)
n✝¹ : ℕ
h₀ : succ n✝¹ < length (x :: xs)
n✝ : ℕ
h₂ : get? (x :: xs) (succ n✝¹) = get? (x :: xs) (succ n✝)
⊢ succ n✝¹ = succ n✝
case succ.succ =>
  congr; cases h₁
  apply tail_ih <;> solve_by_elim [lt_of_succ_lt_succ]
case cons.zero.succ.cons
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
h₀ : zero < length (x :: xs)
n✝ : ℕ
h₂ : some x = get? xs n✝
h' : Pairwise (fun x x_1 => x ≠ x_1) xs
h : ∀ (a' : α), a' ∈ xs → x ≠ a'
⊢ zero = succ n✝

case cons.succ.zero.cons
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
n✝ : ℕ
h₀ : succ n✝ < length (x :: xs)
h₂ : get? xs n✝ = some x
h' : Pairwise (fun x x_1 => x ≠ x_1) xs
h : ∀ (a' : α), a' ∈ xs → x ≠ a'
⊢ succ n✝ = zero
case cons.zero.succ
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
h₁ : Nodup (x :: xs)
h₀ : zero < length (x :: xs)
n✝ : ℕ
h₂ : get? (x :: xs) zero = get? (x :: xs) (succ n✝)
⊢ zero = succ n✝

case cons.succ.zero
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
h₁ : Nodup (x :: xs)
n✝ : ℕ
h₀ : succ n✝ < length (x :: xs)
h₂ : get? (x :: xs) (succ n✝) = get? (x :: xs) zero
⊢ succ n✝ = zero
all_goals ( dsimp at h₂; cases' h₁ with _ _ h h')
no goals
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
h₁ : Nodup (x :: xs)
h₀ : zero < length (x :: xs)
h₂ : get? (x :: xs) zero = get? (x :: xs) zero
⊢ zero = zero
rfl
case e_n
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
h₁ : Nodup (x :: xs)
n✝¹ : ℕ
h₀ : succ n✝¹ < length (x :: xs)
n✝ : ℕ
h₂ : get? (x :: xs) (succ n✝¹) = get? (x :: xs) (succ n✝)
⊢ n✝¹ = n✝
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
h₁ : Nodup (x :: xs)
n✝¹ : ℕ
h₀ : succ n✝¹ < length (x :: xs)
n✝ : ℕ
h₂ : get? (x :: xs) (succ n✝¹) = get? (x :: xs) (succ n✝)
⊢ succ n✝¹ = succ n✝
congr
case e_n.cons
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
n✝¹ : ℕ
h₀ : succ n✝¹ < length (x :: xs)
n✝ : ℕ
h₂ : get? (x :: xs) (succ n✝¹) = get? (x :: xs) (succ n✝)
a✝¹ : Pairwise (fun x x_1 => x ≠ x_1) xs
a✝ : ∀ (a' : α), a' ∈ xs → x ≠ a'
⊢ n✝¹ = n✝
case e_n
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
h₁ : Nodup (x :: xs)
n✝¹ : ℕ
h₀ : succ n✝¹ < length (x :: xs)
n✝ : ℕ
h₂ : get? (x :: xs) (succ n✝¹) = get? (x :: xs) (succ n✝)
⊢ n✝¹ = n✝
cases h₁
no goals
case e_n.cons
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
n✝¹ : ℕ
h₀ : succ n✝¹ < length (x :: xs)
n✝ : ℕ
h₂ : get? (x :: xs) (succ n✝¹) = get? (x :: xs) (succ n✝)
a✝¹ : Pairwise (fun x x_1 => x ≠ x_1) xs
a✝ : ∀ (a' : α), a' ∈ xs → x ≠ a'
⊢ n✝¹ = n✝
apply tail_ih <;> solve_by_elim [lt_of_succ_lt_succ]
case cons.succ.zero.cons
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
n✝ : ℕ
h₀ : succ n✝ < length (x :: xs)
h₂ : get? xs n✝ = some x
h' : Pairwise (fun x x_1 => x ≠ x_1) xs
h : ∀ (a' : α), a' ∈ xs → x ≠ a'
⊢ succ n✝ = zero
case cons.succ.zero
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
h₁ : Nodup (x :: xs)
n✝ : ℕ
h₀ : succ n✝ < length (x :: xs)
h₂ : get? (x :: xs) (succ n✝) = get? (x :: xs) zero
⊢ succ n✝ = zero
( dsimp at h₂; cases' h₁ with _ _ h h')
case cons.succ.zero
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
h₁ : Nodup (x :: xs)
n✝ : ℕ
h₀ : succ n✝ < length (x :: xs)
h₂ : get? xs n✝ = some x
⊢ succ n✝ = zero
case cons.succ.zero
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
h₁ : Nodup (x :: xs)
n✝ : ℕ
h₀ : succ n✝ < length (x :: xs)
h₂ : get? (x :: xs) (succ n✝) = get? (x :: xs) zero
⊢ succ n✝ = zero
dsimp at h₂
case cons.succ.zero.cons
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
n✝ : ℕ
h₀ : succ n✝ < length (x :: xs)
h₂ : get? xs n✝ = some x
h' : Pairwise (fun x x_1 => x ≠ x_1) xs
h : ∀ (a' : α), a' ∈ xs → x ≠ a'
⊢ succ n✝ = zero
case cons.succ.zero
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
h₁ : Nodup (x :: xs)
n✝ : ℕ
h₀ : succ n✝ < length (x :: xs)
h₂ : get? xs n✝ = some x
⊢ succ n✝ = zero
cases' h₁ with _ _ h h'
no goals
case cons.zero.succ.cons
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
h₀ : zero < length (x :: xs)
n✝ : ℕ
h₂ : some x = get? xs n✝
h' : Pairwise (fun x x_1 => x ≠ x_1) xs
h : ∀ (a' : α), a' ∈ xs → x ≠ a'
⊢ zero = succ n✝
cases (h x (mem_iff_get?.mpr ⟨_, h₂.symm⟩) rfl)
no goals
case cons.succ.zero.cons
ι : Type ?u.83779
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u
x : α
xs : List α
tail_ih : ∀ {i j : ℕ}, i < length xs → Nodup xs → get? xs i = get? xs j → i = j
n✝ : ℕ
h₀ : succ n✝ < length (x :: xs)
h₂ : get? xs n✝ = some x
h' : Pairwise (fun x x_1 => x ≠ x_1) xs
h : ∀ (a' : α), a' ∈ xs → x ≠ a'
⊢ succ n✝ = zero
cases (h x (mem_iff_get?.mpr ⟨_, h₂⟩) rfl)