Theorem: List.Nodup.get_inj (Fifteen/Data/List/Basic.lean)

State before:
α : Type u
β : Type v
l : List α
nodup : Nodup l
i j : Nat
hi : i < length l
hj : j < length l
h : l[i] = l[j]
⊢ i = j
Tactic:
induction l generalizing i j with
| nil => cases hi
| cons a l IH =>
  cases nodup with | cons ha nodup =>
  specialize IH nodup
  cases i <;> cases j <;> dsimp at h
  . rfl
  . exfalso
    suffices a ∈ l from ha a this rfl
    exact List.mem_iff_get.mpr ⟨_, h.symm⟩
  . exfalso
    suffices a ∈ l from ha a this rfl
    exact List.mem_iff_get.mpr ⟨_, h⟩
  . exact congrArg Nat.succ <| IH _ _ h
State after:
no goals

State before:
case nil
α : Type u
β : Type v
nodup : Nodup []
i j : Nat
hi : i < length []
hj : j < length []
h : [][i] = [][j]
⊢ i = j
Tactic:
cases hi
State after:
no goals

State before:
case cons
α : Type u
β : Type v
a : α
l : List α
IH : Nodup l → ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
nodup : Nodup (a :: l)
i j : Nat
hi : i < length (a :: l)
hj : j < length (a :: l)
h : (a :: l)[i] = (a :: l)[j]
⊢ i = j
Tactic:
cases nodup with | cons ha nodup =>
specialize IH nodup
cases i <;> cases j <;> dsimp at h
. rfl
. exfalso
  suffices a ∈ l from ha a this rfl
  exact List.mem_iff_get.mpr ⟨_, h.symm⟩
. exfalso
  suffices a ∈ l from ha a this rfl
  exact List.mem_iff_get.mpr ⟨_, h⟩
. exact congrArg Nat.succ <| IH _ _ h
State after:
no goals

State before:
case cons.cons
α : Type u
β : Type v
a : α
l : List α
IH : Nodup l → ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
i j : Nat
hi : i < length (a :: l)
hj : j < length (a :: l)
h : (a :: l)[i] = (a :: l)[j]
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
⊢ i = j
Tactic:
specialize IH nodup
State after:
case cons.cons
α : Type u
β : Type v
a : α
l : List α
i j : Nat
hi : i < length (a :: l)
hj : j < length (a :: l)
h : (a :: l)[i] = (a :: l)[j]
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
⊢ i = j

State before:
case cons.cons
α : Type u
β : Type v
a : α
l : List α
i j : Nat
hi : i < length (a :: l)
hj : j < length (a :: l)
h : (a :: l)[i] = (a :: l)[j]
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
⊢ i = j
Tactic:
cases i <;> cases j <;> dsimp at h
State after:
case cons.cons.zero.zero
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
hi hj : Nat.zero < length (a :: l)
h : a = a
⊢ Nat.zero = Nat.zero

case cons.cons.zero.succ
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
hi : Nat.zero < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h : a = get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ Nat.zero = Nat.succ n✝

case cons.cons.succ.zero
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < length (a :: l)
hj : Nat.zero < length (a :: l)
h : get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) } = a
⊢ Nat.succ n✝ = Nat.zero

case cons.cons.succ.succ
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h :
  get l { val := n✝¹, isLt := (_ : Nat.succ n✝¹ ≤ length l) } =
    get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ Nat.succ n✝¹ = Nat.succ n✝

State before:
case cons.cons.zero.zero
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
hi hj : Nat.zero < length (a :: l)
h : a = a
⊢ Nat.zero = Nat.zero

case cons.cons.zero.succ
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
hi : Nat.zero < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h : a = get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ Nat.zero = Nat.succ n✝

case cons.cons.succ.zero
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < length (a :: l)
hj : Nat.zero < length (a :: l)
h : get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) } = a
⊢ Nat.succ n✝ = Nat.zero

case cons.cons.succ.succ
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h :
  get l { val := n✝¹, isLt := (_ : Nat.succ n✝¹ ≤ length l) } =
    get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ Nat.succ n✝¹ = Nat.succ n✝
Tactic:
. rfl
State after:
case cons.cons.zero.succ
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
hi : Nat.zero < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h : a = get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ Nat.zero = Nat.succ n✝

case cons.cons.succ.zero
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < length (a :: l)
hj : Nat.zero < length (a :: l)
h : get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) } = a
⊢ Nat.succ n✝ = Nat.zero

case cons.cons.succ.succ
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h :
  get l { val := n✝¹, isLt := (_ : Nat.succ n✝¹ ≤ length l) } =
    get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ Nat.succ n✝¹ = Nat.succ n✝

State before:
case cons.cons.zero.succ
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
hi : Nat.zero < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h : a = get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ Nat.zero = Nat.succ n✝

case cons.cons.succ.zero
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < length (a :: l)
hj : Nat.zero < length (a :: l)
h : get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) } = a
⊢ Nat.succ n✝ = Nat.zero

case cons.cons.succ.succ
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h :
  get l { val := n✝¹, isLt := (_ : Nat.succ n✝¹ ≤ length l) } =
    get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ Nat.succ n✝¹ = Nat.succ n✝
Tactic:
. exfalso
  suffices a ∈ l from ha a this rfl
  exact List.mem_iff_get.mpr ⟨_, h.symm⟩
State after:
case cons.cons.succ.zero
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < length (a :: l)
hj : Nat.zero < length (a :: l)
h : get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) } = a
⊢ Nat.succ n✝ = Nat.zero

case cons.cons.succ.succ
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h :
  get l { val := n✝¹, isLt := (_ : Nat.succ n✝¹ ≤ length l) } =
    get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ Nat.succ n✝¹ = Nat.succ n✝

State before:
case cons.cons.succ.zero
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < length (a :: l)
hj : Nat.zero < length (a :: l)
h : get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) } = a
⊢ Nat.succ n✝ = Nat.zero

case cons.cons.succ.succ
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h :
  get l { val := n✝¹, isLt := (_ : Nat.succ n✝¹ ≤ length l) } =
    get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ Nat.succ n✝¹ = Nat.succ n✝
Tactic:
. exfalso
  suffices a ∈ l from ha a this rfl
  exact List.mem_iff_get.mpr ⟨_, h⟩
State after:
case cons.cons.succ.succ
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h :
  get l { val := n✝¹, isLt := (_ : Nat.succ n✝¹ ≤ length l) } =
    get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ Nat.succ n✝¹ = Nat.succ n✝

State before:
case cons.cons.succ.succ
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h :
  get l { val := n✝¹, isLt := (_ : Nat.succ n✝¹ ≤ length l) } =
    get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ Nat.succ n✝¹ = Nat.succ n✝
Tactic:
. exact congrArg Nat.succ <| IH _ _ h
State after:
no goals

State before:
case cons.cons.zero.zero
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
hi hj : Nat.zero < length (a :: l)
h : a = a
⊢ Nat.zero = Nat.zero
Tactic:
rfl
State after:
no goals

State before:
case cons.cons.zero.succ
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
hi : Nat.zero < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h : a = get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ Nat.zero = Nat.succ n✝
Tactic:
exfalso
State after:
case cons.cons.zero.succ.h
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
hi : Nat.zero < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h : a = get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ False

State before:
case cons.cons.zero.succ.h
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
hi : Nat.zero < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h : a = get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ False
Tactic:
suffices a ∈ l from ha a this rfl
State after:
case cons.cons.zero.succ.h
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
hi : Nat.zero < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h : a = get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ a ∈ l

State before:
case cons.cons.zero.succ.h
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
hi : Nat.zero < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h : a = get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ a ∈ l
Tactic:
exact List.mem_iff_get.mpr ⟨_, h.symm⟩
State after:
no goals

State before:
case cons.cons.succ.zero
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < length (a :: l)
hj : Nat.zero < length (a :: l)
h : get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) } = a
⊢ Nat.succ n✝ = Nat.zero
Tactic:
exfalso
State after:
case cons.cons.succ.zero.h
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < length (a :: l)
hj : Nat.zero < length (a :: l)
h : get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) } = a
⊢ False

State before:
case cons.cons.succ.zero.h
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < length (a :: l)
hj : Nat.zero < length (a :: l)
h : get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) } = a
⊢ False
Tactic:
suffices a ∈ l from ha a this rfl
State after:
case cons.cons.succ.zero.h
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < length (a :: l)
hj : Nat.zero < length (a :: l)
h : get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) } = a
⊢ a ∈ l

State before:
case cons.cons.succ.zero.h
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < length (a :: l)
hj : Nat.zero < length (a :: l)
h : get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) } = a
⊢ a ∈ l
Tactic:
exact List.mem_iff_get.mpr ⟨_, h⟩
State after:
no goals

State before:
case cons.cons.succ.succ
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h :
  get l { val := n✝¹, isLt := (_ : Nat.succ n✝¹ ≤ length l) } =
    get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ Nat.succ n✝¹ = Nat.succ n✝
Tactic:
exact congrArg Nat.succ <| IH _ _ h
State after:
no goals