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

State before:
α : Type u_1
de : DecidableEq α
x : α
xs : List α
i : Fin (List.length xs)
d : differs (x :: xs) = true
⊢ ¬x = List.get xs i
Tactic:
intro p
State after:
α : Type u_1
de : DecidableEq α
x : α
xs : List α
i : Fin (List.length xs)
d : differs (x :: xs) = true
p : x = List.get xs i
⊢ False

State before:
α : Type u_1
de : DecidableEq α
x : α
xs : List α
i : Fin (List.length xs)
d : differs (x :: xs) = true
p : x = List.get xs i
⊢ False
Tactic:
unfold differs at d
State after:
α : Type u_1
de : DecidableEq α
x : α
xs : List α
i : Fin (List.length xs)
p : x = List.get xs i
d : ((List.all xs fun x_1 => x_1 != x) && differs xs) = true
⊢ False

State before:
α : Type u_1
de : DecidableEq α
x : α
xs : List α
i : Fin (List.length xs)
p : x = List.get xs i
d : ((List.all xs fun x_1 => x_1 != x) && differs xs) = true
⊢ False
Tactic:
simp at d
State after:
α : Type u_1
de : DecidableEq α
x : α
xs : List α
i : Fin (List.length xs)
p : x = List.get xs i
d : (List.all xs fun x_1 => x_1 != x) = true ∧ differs xs = true
⊢ False

State before:
α : Type u_1
de : DecidableEq α
x : α
xs : List α
i : Fin (List.length xs)
p : x = List.get xs i
d : (List.all xs fun x_1 => x_1 != x) = true ∧ differs xs = true
⊢ False
Tactic:
cases d with | intro all _ =>
let une := listAllCorrect i all
simp [bne, BEq.beq] at une
let une := of_decide_eq_false une
rw [p] at une
contradiction
State after:
no goals

State before:
case intro
α : Type u_1
de : DecidableEq α
x : α
xs : List α
i : Fin (List.length xs)
p : x = List.get xs i
all : (List.all xs fun x_1 => x_1 != x) = true
right✝ : differs xs = true
⊢ False
Tactic:
let une := listAllCorrect i all
State after:
case intro
α : Type u_1
de : DecidableEq α
x : α
xs : List α
i : Fin (List.length xs)
p : x = List.get xs i
all : (List.all xs fun x_1 => x_1 != x) = true
right✝ : differs xs = true
une : (List.get xs i != x) = true := listAllCorrect i all
⊢ False

State before:
case intro
α : Type u_1
de : DecidableEq α
x : α
xs : List α
i : Fin (List.length xs)
p : x = List.get xs i
all : (List.all xs fun x_1 => x_1 != x) = true
right✝ : differs xs = true
une : (List.get xs i != x) = true := listAllCorrect i all
⊢ False
Tactic:
simp [bne, BEq.beq] at une
State after:
case intro
α : Type u_1
de : DecidableEq α
x : α
xs : List α
i : Fin (List.length xs)
p : x = List.get xs i
all : (List.all xs fun x_1 => x_1 != x) = true
right✝ : differs xs = true
une : decide (List.get xs i = x) = false
⊢ False

State before:
case intro
α : Type u_1
de : DecidableEq α
x : α
xs : List α
i : Fin (List.length xs)
p : x = List.get xs i
all : (List.all xs fun x_1 => x_1 != x) = true
right✝ : differs xs = true
une : decide (List.get xs i = x) = false
⊢ False
Tactic:
let une := of_decide_eq_false une
State after:
case intro
α : Type u_1
de : DecidableEq α
x : α
xs : List α
i : Fin (List.length xs)
p : x = List.get xs i
all : (List.all xs fun x_1 => x_1 != x) = true
right✝ : differs xs = true
une✝ : decide (List.get xs i = x) = false
une : ¬List.get xs i = x := of_decide_eq_false une✝
⊢ False

State before:
case intro
α : Type u_1
de : DecidableEq α
x : α
xs : List α
i : Fin (List.length xs)
p : x = List.get xs i
all : (List.all xs fun x_1 => x_1 != x) = true
right✝ : differs xs = true
une✝ : decide (List.get xs i = x) = false
une : ¬List.get xs i = x := of_decide_eq_false une✝
⊢ False
Tactic:
rw [p] at une
State after:
case intro
α : Type u_1
de : DecidableEq α
x : α
xs : List α
i : Fin (List.length xs)
p : x = List.get xs i
all : (List.all xs fun x_1 => x_1 != x) = true
right✝ : differs xs = true
une✝ : decide (List.get xs i = x) = false
une : ¬List.get xs i = List.get xs i
⊢ False

State before:
case intro
α : Type u_1
de : DecidableEq α
x : α
xs : List α
i : Fin (List.length xs)
p : x = List.get xs i
all : (List.all xs fun x_1 => x_1 != x) = true
right✝ : differs xs = true
une✝ : decide (List.get xs i = x) = false
une : ¬List.get xs i = List.get xs i
⊢ False
Tactic:
contradiction
State after:
no goals