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

State before:
α : Type u_1
inst✝ : DecidableEq α
xs : List α
dl : DifferentList xs
⊢ differs xs = true
Tactic:
cases xs <;> simp [differs]
State after:
case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
dl : DifferentList (head✝ :: tail✝)
⊢ (List.all tail✝ fun x => x != head✝) = true ∧ differs tail✝ = true

State before:
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
dl : DifferentList (h :: t)
⊢ (List.all t fun x => x != h) = true ∧ differs t = true
Tactic:
case cons h t =>
simp [differs] 
constructor
. apply DifListHead dl
. apply correctRight
  apply DifListTail _ dl
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
dl : DifferentList (h :: t)
⊢ (List.all t fun x => x != h) = true ∧ differs t = true
Tactic:
constructor
State after:
case left
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
dl : DifferentList (h :: t)
⊢ (List.all t fun x => x != h) = true

case right
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
dl : DifferentList (h :: t)
⊢ differs t = true

State before:
case left
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
dl : DifferentList (h :: t)
⊢ (List.all t fun x => x != h) = true

case right
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
dl : DifferentList (h :: t)
⊢ differs t = true
Tactic:
. apply DifListHead dl
State after:
case right
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
dl : DifferentList (h :: t)
⊢ differs t = true

State before:
case right
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
dl : DifferentList (h :: t)
⊢ differs t = true
Tactic:
. apply correctRight
  apply DifListTail _ dl
State after:
no goals