Theorem: List.nodup_of_get_inj (Fifteen/Data/List/Basic.lean)

State before:
α : Type u
β : Type v
l : List α
h : ∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j
⊢ Nodup l
Tactic:
induction l with
| nil => exact .nil
| cons a l IH =>
  refine .cons ?_ (IH fun i j hi hj hl => ?_)
  . intro _ hmem heq; cases heq
    have ⟨⟨i,hi⟩,hl⟩ := List.mem_iff_get.mp hmem
    have : i+1 = 0 :=
      h (i+1) 0 (Nat.succ_lt_succ hi) l.length.zero_lt_succ hl
    cases this
  . apply Nat.succ.inj
    exact h (i+1) (j+1) (Nat.succ_lt_succ hi) (Nat.succ_lt_succ hj) hl
State after:
no goals

State before:
case nil
α : Type u
β : Type v
h : ∀ (i j : Nat) (x : i < length []) (x_1 : j < length []), [][i] = [][j] → i = j
⊢ Nodup []
Tactic:
exact .nil
State after:
no goals

State before:
case cons
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
⊢ Nodup (a :: l)
Tactic:
refine .cons ?_ (IH fun i j hi hj hl => ?_)
State after:
case cons.refine_1
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
⊢ ∀ (a' : α), a' ∈ l → a ≠ a'

case cons.refine_2
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
i j : Nat
hi : i < length l
hj : j < length l
hl : l[i] = l[j]
⊢ i = j

State before:
case cons.refine_1
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
⊢ ∀ (a' : α), a' ∈ l → a ≠ a'

case cons.refine_2
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
i j : Nat
hi : i < length l
hj : j < length l
hl : l[i] = l[j]
⊢ i = j
Tactic:
. intro _ hmem heq; cases heq
  have ⟨⟨i,hi⟩,hl⟩ := List.mem_iff_get.mp hmem
  have : i+1 = 0 :=
    h (i+1) 0 (Nat.succ_lt_succ hi) l.length.zero_lt_succ hl
  cases this
State after:
case cons.refine_2
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
i j : Nat
hi : i < length l
hj : j < length l
hl : l[i] = l[j]
⊢ i = j

State before:
case cons.refine_2
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
i j : Nat
hi : i < length l
hj : j < length l
hl : l[i] = l[j]
⊢ i = j
Tactic:
. apply Nat.succ.inj
  exact h (i+1) (j+1) (Nat.succ_lt_succ hi) (Nat.succ_lt_succ hj) hl
State after:
no goals

State before:
case cons.refine_1
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
⊢ ∀ (a' : α), a' ∈ l → a ≠ a'
Tactic:
intro _ hmem heq
State after:
case cons.refine_1
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
a'✝ : α
hmem : a'✝ ∈ l
heq : a = a'✝
⊢ False

State before:
case cons.refine_1
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
a'✝ : α
hmem : a'✝ ∈ l
heq : a = a'✝
⊢ False
Tactic:
cases heq
State after:
case cons.refine_1.refl
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
hmem : a ∈ l
⊢ False

State before:
case cons.refine_1.refl
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
hmem : a ∈ l
⊢ False
Tactic:
have ⟨⟨i,hi⟩,hl⟩ := List.mem_iff_get.mp hmem
State after:
case cons.refine_1.refl
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
hmem : a ∈ l
i : Nat
hi : i < length l
hl : get l { val := i, isLt := hi } = a
⊢ False

State before:
case cons.refine_1.refl
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
hmem : a ∈ l
i : Nat
hi : i < length l
hl : get l { val := i, isLt := hi } = a
⊢ False
Tactic:
have : i+1 = 0 :=
  h (i+1) 0 (Nat.succ_lt_succ hi) l.length.zero_lt_succ hl
State after:
case cons.refine_1.refl
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
hmem : a ∈ l
i : Nat
hi : i < length l
hl : get l { val := i, isLt := hi } = a
this : i + 1 = 0
⊢ False

State before:
case cons.refine_1.refl
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
hmem : a ∈ l
i : Nat
hi : i < length l
hl : get l { val := i, isLt := hi } = a
this : i + 1 = 0
⊢ False
Tactic:
cases this
State after:
no goals

State before:
case cons.refine_2
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
i j : Nat
hi : i < length l
hj : j < length l
hl : l[i] = l[j]
⊢ i = j
Tactic:
apply Nat.succ.inj
State after:
case cons.refine_2.x
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
i j : Nat
hi : i < length l
hj : j < length l
hl : l[i] = l[j]
⊢ Nat.succ i = Nat.succ j

State before:
case cons.refine_2.x
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
i j : Nat
hi : i < length l
hj : j < length l
hl : l[i] = l[j]
⊢ Nat.succ i = Nat.succ j
Tactic:
exact h (i+1) (j+1) (Nat.succ_lt_succ hi) (Nat.succ_lt_succ hj) hl
State after:
no goals