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

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

State before:
α : Type u_1
inst✝ : BEq α
x y : α
xs : List α
dl : DifferentList (x :: y :: xs)
i j : Fin (List.length (y :: x :: xs))
iej : List.get (y :: x :: xs) i = List.get (y :: x :: xs) j
⊢ i = j
Tactic:
rw [shuffledGet i, shuffledGet j] at iej
State after:
α : Type u_1
inst✝ : BEq α
x y : α
xs : List α
dl : DifferentList (x :: y :: xs)
i j : Fin (List.length (y :: x :: xs))
iej : List.get (x :: y :: xs) (shuffleIndex i) = List.get (x :: y :: xs) (shuffleIndex j)
⊢ i = j

State before:
α : Type u_1
inst✝ : BEq α
x y : α
xs : List α
dl : DifferentList (x :: y :: xs)
i j : Fin (List.length (y :: x :: xs))
iej : List.get (x :: y :: xs) (shuffleIndex i) = List.get (x :: y :: xs) (shuffleIndex j)
⊢ i = j
Tactic:
let siej := dl _ _ iej
State after:
α : Type u_1
inst✝ : BEq α
x y : α
xs : List α
dl : DifferentList (x :: y :: xs)
i j : Fin (List.length (y :: x :: xs))
iej : List.get (x :: y :: xs) (shuffleIndex i) = List.get (x :: y :: xs) (shuffleIndex j)
siej : shuffleIndex i = shuffleIndex j := dl (shuffleIndex i) (shuffleIndex j) iej
⊢ i = j

State before:
α : Type u_1
inst✝ : BEq α
x y : α
xs : List α
dl : DifferentList (x :: y :: xs)
i j : Fin (List.length (y :: x :: xs))
iej : List.get (x :: y :: xs) (shuffleIndex i) = List.get (x :: y :: xs) (shuffleIndex j)
siej : shuffleIndex i = shuffleIndex j := dl (shuffleIndex i) (shuffleIndex j) iej
⊢ i = j
Tactic:
let ssiej := congrArg shuffleIndex siej
State after:
α : Type u_1
inst✝ : BEq α
x y : α
xs : List α
dl : DifferentList (x :: y :: xs)
i j : Fin (List.length (y :: x :: xs))
iej : List.get (x :: y :: xs) (shuffleIndex i) = List.get (x :: y :: xs) (shuffleIndex j)
siej : shuffleIndex i = shuffleIndex j := dl (shuffleIndex i) (shuffleIndex j) iej
ssiej : shuffleIndex (shuffleIndex i) = shuffleIndex (shuffleIndex j) := congrArg shuffleIndex siej
⊢ i = j

State before:
α : Type u_1
inst✝ : BEq α
x y : α
xs : List α
dl : DifferentList (x :: y :: xs)
i j : Fin (List.length (y :: x :: xs))
iej : List.get (x :: y :: xs) (shuffleIndex i) = List.get (x :: y :: xs) (shuffleIndex j)
siej : shuffleIndex i = shuffleIndex j := dl (shuffleIndex i) (shuffleIndex j) iej
ssiej : shuffleIndex (shuffleIndex i) = shuffleIndex (shuffleIndex j) := congrArg shuffleIndex siej
⊢ i = j
Tactic:
rw [shuffleCancelable, shuffleCancelable] at ssiej
State after:
α : Type u_1
inst✝ : BEq α
x y : α
xs : List α
dl : DifferentList (x :: y :: xs)
i j : Fin (List.length (y :: x :: xs))
iej : List.get (x :: y :: xs) (shuffleIndex i) = List.get (x :: y :: xs) (shuffleIndex j)
siej : shuffleIndex i = shuffleIndex j := dl (shuffleIndex i) (shuffleIndex j) iej
ssiej : i = j
⊢ i = j

State before:
α : Type u_1
inst✝ : BEq α
x y : α
xs : List α
dl : DifferentList (x :: y :: xs)
i j : Fin (List.length (y :: x :: xs))
iej : List.get (x :: y :: xs) (shuffleIndex i) = List.get (x :: y :: xs) (shuffleIndex j)
siej : shuffleIndex i = shuffleIndex j := dl (shuffleIndex i) (shuffleIndex j) iej
ssiej : i = j
⊢ i = j
Tactic:
assumption
State after:
no goals