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

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

State before:
α : Type u_1
inst✝ : BEq α
⊢ ∀ (i j : Fin (List.length [])), List.get [] i = List.get [] j → i = j
Tactic:
intro i
State after:
α : Type u_1
inst✝ : BEq α
i : Fin (List.length [])
⊢ ∀ (j : Fin (List.length [])), List.get [] i = List.get [] j → i = j

State before:
α : Type u_1
inst✝ : BEq α
i : Fin (List.length [])
⊢ ∀ (j : Fin (List.length [])), List.get [] i = List.get [] j → i = j
Tactic:
intros
State after:
α : Type u_1
inst✝ : BEq α
i j✝ : Fin (List.length [])
a✝ : List.get [] i = List.get [] j✝
⊢ i = j✝

State before:
α : Type u_1
inst✝ : BEq α
i j✝ : Fin (List.length [])
a✝ : List.get [] i = List.get [] j✝
⊢ i = j✝
Tactic:
simp [List.length] at i
State after:
α : Type u_1
inst✝ : BEq α
i : Fin 0
j✝ : Fin (List.length [])
a✝ : List.get [] i = List.get [] j✝
⊢ i = j✝

State before:
α : Type u_1
inst✝ : BEq α
i : Fin 0
j✝ : Fin (List.length [])
a✝ : List.get [] i = List.get [] j✝
⊢ i = j✝
Tactic:
cases i.isLt
State after:
no goals