Theorem: DifListTail (Advent/List/Indexing.lean)

State before:
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
⊢ DifferentList (x :: xs) → DifferentList xs
Tactic:
intros xxs
State after:
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
⊢ DifferentList xs

State before:
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
⊢ DifferentList xs
Tactic:
unfold DifferentList
State after:
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
⊢ ∀ (i j : Fin (List.length xs)), List.get xs i = List.get xs j → i = j

State before:
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
⊢ ∀ (i j : Fin (List.length xs)), List.get xs i = List.get xs j → i = j
Tactic:
intros i j iej
State after:
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
⊢ i = j

State before:
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
⊢ i = j
Tactic:
apply Fin.eq_of_val_eq
State after:
case a
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
⊢ i.val = j.val

State before:
case a
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
⊢ i.val = j.val
Tactic:
let i1 := appendFin x xs i
State after:
case a
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
i1 : Fin (List.length (x :: xs)) := appendFin x xs i
⊢ i.val = j.val

State before:
case a
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
i1 : Fin (List.length (x :: xs)) := appendFin x xs i
⊢ i.val = j.val
Tactic:
let j1 := appendFin x xs j
State after:
case a
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
i1 : Fin (List.length (x :: xs)) := appendFin x xs i
j1 : Fin (List.length (x :: xs)) := appendFin x xs j
⊢ i.val = j.val

State before:
case a
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
i1 : Fin (List.length (x :: xs)) := appendFin x xs i
j1 : Fin (List.length (x :: xs)) := appendFin x xs j
⊢ i.val = j.val
Tactic:
let h1 := xxs i1 j1
State after:
case a
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
i1 : Fin (List.length (x :: xs)) := appendFin x xs i
j1 : Fin (List.length (x :: xs)) := appendFin x xs j
h1 : List.get (x :: xs) i1 = List.get (x :: xs) j1 → i1 = j1 := xxs i1 j1
⊢ i.val = j.val

State before:
case a
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
i1 : Fin (List.length (x :: xs)) := appendFin x xs i
j1 : Fin (List.length (x :: xs)) := appendFin x xs j
h1 : List.get (x :: xs) i1 = List.get (x :: xs) j1 → i1 = j1 := xxs i1 j1
⊢ i.val = j.val
Tactic:
simp [List.get] at h1
State after:
case a
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
i1 : Fin (List.length (x :: xs)) := appendFin x xs i
j1 : Fin (List.length (x :: xs)) := appendFin x xs j
h1 : List.get xs { val := i.val, isLt := (_ : Nat.succ i.val ≤ List.length xs) } =
    List.get xs { val := j.val, isLt := (_ : Nat.succ j.val ≤ List.length xs) } →
  appendFin x xs i = appendFin x xs j :=
  xxs i1 j1
⊢ i.val = j.val

State before:
case a
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
i1 : Fin (List.length (x :: xs)) := appendFin x xs i
j1 : Fin (List.length (x :: xs)) := appendFin x xs j
h1 : List.get xs { val := i.val, isLt := (_ : Nat.succ i.val ≤ List.length xs) } =
    List.get xs { val := j.val, isLt := (_ : Nat.succ j.val ≤ List.length xs) } →
  appendFin x xs i = appendFin x xs j :=
  xxs i1 j1
⊢ i.val = j.val
Tactic:
let i1ej1 := h1 iej
State after:
case a
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
i1 : Fin (List.length (x :: xs)) := appendFin x xs i
j1 : Fin (List.length (x :: xs)) := appendFin x xs j
h1 : List.get xs { val := i.val, isLt := (_ : Nat.succ i.val ≤ List.length xs) } =
    List.get xs { val := j.val, isLt := (_ : Nat.succ j.val ≤ List.length xs) } →
  appendFin x xs i = appendFin x xs j :=
  xxs i1 j1
i1ej1 : appendFin x xs i = appendFin x xs j := h1 iej
⊢ i.val = j.val

State before:
case a
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
i1 : Fin (List.length (x :: xs)) := appendFin x xs i
j1 : Fin (List.length (x :: xs)) := appendFin x xs j
h1 : List.get xs { val := i.val, isLt := (_ : Nat.succ i.val ≤ List.length xs) } =
    List.get xs { val := j.val, isLt := (_ : Nat.succ j.val ≤ List.length xs) } →
  appendFin x xs i = appendFin x xs j :=
  xxs i1 j1
i1ej1 : appendFin x xs i = appendFin x xs j := h1 iej
⊢ i.val = j.val
Tactic:
simp [appendFin] at i1ej1
State after:
case a
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
i1 : Fin (List.length (x :: xs)) := appendFin x xs i
j1 : Fin (List.length (x :: xs)) := appendFin x xs j
h1 : List.get xs { val := i.val, isLt := (_ : Nat.succ i.val ≤ List.length xs) } =
    List.get xs { val := j.val, isLt := (_ : Nat.succ j.val ≤ List.length xs) } →
  appendFin x xs i = appendFin x xs j :=
  xxs i1 j1
i1ej1 : i.val = j.val
⊢ i.val = j.val

State before:
case a
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
i1 : Fin (List.length (x :: xs)) := appendFin x xs i
j1 : Fin (List.length (x :: xs)) := appendFin x xs j
h1 : List.get xs { val := i.val, isLt := (_ : Nat.succ i.val ≤ List.length xs) } =
    List.get xs { val := j.val, isLt := (_ : Nat.succ j.val ≤ List.length xs) } →
  appendFin x xs i = appendFin x xs j :=
  xxs i1 j1
i1ej1 : i.val = j.val
⊢ i.val = j.val
Tactic:
exact i1ej1
State after:
no goals