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

State before:
α : Type u_1
da : DecidableEq α
x : α
xs : List α
⊢ DifferentList (x :: xs) → (List.all xs fun x_1 => x_1 != x) = true
Tactic:
intros h
State after:
α : Type u_1
da : DecidableEq α
x : α
xs : List α
h : DifferentList (x :: xs)
⊢ (List.all xs fun x_1 => x_1 != x) = true

State before:
α : Type u_1
da : DecidableEq α
x : α
xs : List α
h : DifferentList (x :: xs)
⊢ (List.all xs fun x_1 => x_1 != x) = true
Tactic:
cases xs
State after:
case nil
α : Type u_1
da : DecidableEq α
x : α
h : DifferentList [x]
⊢ (List.all [] fun x_1 => x_1 != x) = true

case cons
α : Type u_1
da : DecidableEq α
x head✝ : α
tail✝ : List α
h : DifferentList (x :: head✝ :: tail✝)
⊢ (List.all (head✝ :: tail✝) fun x_1 => x_1 != x) = true

State before:
case nil
α : Type u_1
da : DecidableEq α
x : α
h : DifferentList [x]
⊢ (List.all [] fun x_1 => x_1 != x) = true

case cons
α : Type u_1
da : DecidableEq α
x head✝ : α
tail✝ : List α
h : DifferentList (x :: head✝ :: tail✝)
⊢ (List.all (head✝ :: tail✝) fun x_1 => x_1 != x) = true
Tactic:
. simp [List.all, List.foldr]
State after:
case cons
α : Type u_1
da : DecidableEq α
x head✝ : α
tail✝ : List α
h : DifferentList (x :: head✝ :: tail✝)
⊢ (List.all (head✝ :: tail✝) fun x_1 => x_1 != x) = true

State before:
case cons
α : Type u_1
da : DecidableEq α
x head✝ : α
tail✝ : List α
h : DifferentList (x :: head✝ :: tail✝)
⊢ (List.all (head✝ :: tail✝) fun x_1 => x_1 != x) = true
Tactic:
. case cons y ys => 
  simp [List.all, List.foldr]
  constructor
  . simp [bne, BEq.beq, decide]
    apply decide_eq_false
    intro yex
    let i: Fin (x :: y :: ys).length := ⟨ 0, Nat.zero_lt_succ _ ⟩
    let j: Fin (x :: y :: ys).length := ⟨ 1, Nat.succ_le_succ (Nat.zero_lt_succ _) ⟩
    let h2 := h i j
    simp [List.get] at h2
    apply h2
    rw [yex]
  . apply DifListHead
    apply DifListTail y
    apply DifListShuffle
    exact h
State after:
no goals

State before:
α : Type u_1
da : DecidableEq α
x y : α
ys : List α
h : DifferentList (x :: y :: ys)
⊢ (List.all (y :: ys) fun x_1 => x_1 != x) = true
Tactic:
simp [List.all, List.foldr]
State after:
α : Type u_1
da : DecidableEq α
x y : α
ys : List α
h : DifferentList (x :: y :: ys)
⊢ (y != x) = true ∧ List.foldr (fun a r => a != x && r) true ys = true

State before:
α : Type u_1
da : DecidableEq α
x y : α
ys : List α
h : DifferentList (x :: y :: ys)
⊢ (y != x) = true ∧ List.foldr (fun a r => a != x && r) true ys = true
Tactic:
constructor
State after:
case left
α : Type u_1
da : DecidableEq α
x y : α
ys : List α
h : DifferentList (x :: y :: ys)
⊢ (y != x) = true

case right
α : Type u_1
da : DecidableEq α
x y : α
ys : List α
h : DifferentList (x :: y :: ys)
⊢ List.foldr (fun a r => a != x && r) true ys = true

State before:
case left
α : Type u_1
da : DecidableEq α
x y : α
ys : List α
h : DifferentList (x :: y :: ys)
⊢ (y != x) = true

case right
α : Type u_1
da : DecidableEq α
x y : α
ys : List α
h : DifferentList (x :: y :: ys)
⊢ List.foldr (fun a r => a != x && r) true ys = true
Tactic:
. simp [bne, BEq.beq, decide]
  apply decide_eq_false
  intro yex
  let i: Fin (x :: y :: ys).length := ⟨ 0, Nat.zero_lt_succ _ ⟩
  let j: Fin (x :: y :: ys).length := ⟨ 1, Nat.succ_le_succ (Nat.zero_lt_succ _) ⟩
  let h2 := h i j
  simp [List.get] at h2
  apply h2
  rw [yex]
State after:
case right
α : Type u_1
da : DecidableEq α
x y : α
ys : List α
h : DifferentList (x :: y :: ys)
⊢ List.foldr (fun a r => a != x && r) true ys = true

State before:
case right
α : Type u_1
da : DecidableEq α
x y : α
ys : List α
h : DifferentList (x :: y :: ys)
⊢ List.foldr (fun a r => a != x && r) true ys = true
Tactic:
. apply DifListHead
  apply DifListTail y
  apply DifListShuffle
  exact h
State after:
no goals