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

State before:
α : Type u_1
inst✝ : DecidableEq α
xs : List α
p : differs xs = true
⊢ DifferentList xs
Tactic:
cases xs
State after:
case nil
α : Type u_1
inst✝ : DecidableEq α
p : differs [] = true
⊢ DifferentList []

case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
p : differs (head✝ :: tail✝) = true
⊢ DifferentList (head✝ :: tail✝)

State before:
case nil
α : Type u_1
inst✝ : DecidableEq α
p : differs [] = true
⊢ DifferentList []

case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
p : differs (head✝ :: tail✝) = true
⊢ DifferentList (head✝ :: tail✝)
Tactic:
. apply nilDifferent
State after:
case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
p : differs (head✝ :: tail✝) = true
⊢ DifferentList (head✝ :: tail✝)

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
p : differs (head✝ :: tail✝) = true
⊢ DifferentList (head✝ :: tail✝)
Tactic:
. case cons h t => 
  unfold DifferentList
  intros i j iej
  cases i with | mk iv ilt =>
  cases j with | mk jv jlt => 
  apply Fin.eq_of_val_eq
  simp
  cases iv 
  . cases jv
    simp
    case succ j => 
      simp [List.get] at iej
      let xs := differsHead p iej
      contradiction                
  . case succ i => 
    cases jv
    . simp [List.get] at iej
      let xs := differsHead p iej.symm
      contradiction
    . case succ j => 
      simp [List.get] at iej
      simp
      simp [differs] at p
      cases p with | intro _ tdiff =>
      let td := correctLeft t tdiff        
      let u := td _ _ iej
      simp at u
      assumption
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
⊢ DifferentList (h :: t)
Tactic:
unfold DifferentList
State after:
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
⊢ ∀ (i j : Fin (List.length (h :: t))), List.get (h :: t) i = List.get (h :: t) j → i = j

State before:
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
⊢ ∀ (i j : Fin (List.length (h :: t))), List.get (h :: t) i = List.get (h :: t) j → i = j
Tactic:
intros i j iej
State after:
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
i j : Fin (List.length (h :: t))
iej : List.get (h :: t) i = List.get (h :: t) j
⊢ i = j

State before:
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
i j : Fin (List.length (h :: t))
iej : List.get (h :: t) i = List.get (h :: t) j
⊢ i = j
Tactic:
cases i with | mk iv ilt =>
cases j with | mk jv jlt => 
apply Fin.eq_of_val_eq
simp
cases iv 
. cases jv
  simp
  case succ j => 
    simp [List.get] at iej
    let xs := differsHead p iej
    contradiction                
. case succ i => 
  cases jv
  . simp [List.get] at iej
    let xs := differsHead p iej.symm
    contradiction
  . case succ j => 
    simp [List.get] at iej
    simp
    simp [differs] at p
    cases p with | intro _ tdiff =>
    let td := correctLeft t tdiff        
    let u := td _ _ iej
    simp at u
    assumption
State after:
no goals

State before:
case mk
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
j : Fin (List.length (h :: t))
iv : Nat
ilt : iv < List.length (h :: t)
iej : List.get (h :: t) { val := iv, isLt := ilt } = List.get (h :: t) j
⊢ { val := iv, isLt := ilt } = j
Tactic:
cases j with | mk jv jlt => 
apply Fin.eq_of_val_eq
simp
cases iv 
. cases jv
  simp
  case succ j => 
    simp [List.get] at iej
    let xs := differsHead p iej
    contradiction                
. case succ i => 
  cases jv
  . simp [List.get] at iej
    let xs := differsHead p iej.symm
    contradiction
  . case succ j => 
    simp [List.get] at iej
    simp
    simp [differs] at p
    cases p with | intro _ tdiff =>
    let td := correctLeft t tdiff        
    let u := td _ _ iej
    simp at u
    assumption
State after:
no goals

State before:
case mk.mk
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
iv : Nat
ilt : iv < List.length (h :: t)
jv : Nat
jlt : jv < List.length (h :: t)
iej : List.get (h :: t) { val := iv, isLt := ilt } = List.get (h :: t) { val := jv, isLt := jlt }
⊢ { val := iv, isLt := ilt } = { val := jv, isLt := jlt }
Tactic:
apply Fin.eq_of_val_eq
State after:
case mk.mk.a
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
iv : Nat
ilt : iv < List.length (h :: t)
jv : Nat
jlt : jv < List.length (h :: t)
iej : List.get (h :: t) { val := iv, isLt := ilt } = List.get (h :: t) { val := jv, isLt := jlt }
⊢ { val := iv, isLt := ilt }.val = { val := jv, isLt := jlt }.val

State before:
case mk.mk.a
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
iv : Nat
ilt : iv < List.length (h :: t)
jv : Nat
jlt : jv < List.length (h :: t)
iej : List.get (h :: t) { val := iv, isLt := ilt } = List.get (h :: t) { val := jv, isLt := jlt }
⊢ { val := iv, isLt := ilt }.val = { val := jv, isLt := jlt }.val
Tactic:
simp
State after:
case mk.mk.a
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
iv : Nat
ilt : iv < List.length (h :: t)
jv : Nat
jlt : jv < List.length (h :: t)
iej : List.get (h :: t) { val := iv, isLt := ilt } = List.get (h :: t) { val := jv, isLt := jlt }
⊢ iv = jv

State before:
case mk.mk.a
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
iv : Nat
ilt : iv < List.length (h :: t)
jv : Nat
jlt : jv < List.length (h :: t)
iej : List.get (h :: t) { val := iv, isLt := ilt } = List.get (h :: t) { val := jv, isLt := jlt }
⊢ iv = jv
Tactic:
cases iv
State after:
case mk.mk.a.zero
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
jv : Nat
jlt : jv < List.length (h :: t)
ilt : Nat.zero < List.length (h :: t)
iej : List.get (h :: t) { val := Nat.zero, isLt := ilt } = List.get (h :: t) { val := jv, isLt := jlt }
⊢ Nat.zero = jv

case mk.mk.a.succ
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
jv : Nat
jlt : jv < List.length (h :: t)
n✝ : Nat
ilt : Nat.succ n✝ < List.length (h :: t)
iej : List.get (h :: t) { val := Nat.succ n✝, isLt := ilt } = List.get (h :: t) { val := jv, isLt := jlt }
⊢ Nat.succ n✝ = jv

State before:
case mk.mk.a.zero
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
jv : Nat
jlt : jv < List.length (h :: t)
ilt : Nat.zero < List.length (h :: t)
iej : List.get (h :: t) { val := Nat.zero, isLt := ilt } = List.get (h :: t) { val := jv, isLt := jlt }
⊢ Nat.zero = jv

case mk.mk.a.succ
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
jv : Nat
jlt : jv < List.length (h :: t)
n✝ : Nat
ilt : Nat.succ n✝ < List.length (h :: t)
iej : List.get (h :: t) { val := Nat.succ n✝, isLt := ilt } = List.get (h :: t) { val := jv, isLt := jlt }
⊢ Nat.succ n✝ = jv
Tactic:
. cases jv
  simp
  case succ j => 
    simp [List.get] at iej
    let xs := differsHead p iej
    contradiction
State after:
case mk.mk.a.succ
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
jv : Nat
jlt : jv < List.length (h :: t)
n✝ : Nat
ilt : Nat.succ n✝ < List.length (h :: t)
iej : List.get (h :: t) { val := Nat.succ n✝, isLt := ilt } = List.get (h :: t) { val := jv, isLt := jlt }
⊢ Nat.succ n✝ = jv

State before:
case mk.mk.a.succ
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
jv : Nat
jlt : jv < List.length (h :: t)
n✝ : Nat
ilt : Nat.succ n✝ < List.length (h :: t)
iej : List.get (h :: t) { val := Nat.succ n✝, isLt := ilt } = List.get (h :: t) { val := jv, isLt := jlt }
⊢ Nat.succ n✝ = jv
Tactic:
. case succ i => 
  cases jv
  . simp [List.get] at iej
    let xs := differsHead p iej.symm
    contradiction
  . case succ j => 
    simp [List.get] at iej
    simp
    simp [differs] at p
    cases p with | intro _ tdiff =>
    let td := correctLeft t tdiff        
    let u := td _ _ iej
    simp at u
    assumption
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
ilt : Nat.zero < List.length (h :: t)
j : Nat
jlt : Nat.succ j < List.length (h :: t)
iej : List.get (h :: t) { val := Nat.zero, isLt := ilt } = List.get (h :: t) { val := Nat.succ j, isLt := jlt }
⊢ Nat.zero = Nat.succ j
Tactic:
simp [List.get] at iej
State after:
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
ilt : Nat.zero < List.length (h :: t)
j : Nat
jlt : Nat.succ j < List.length (h :: t)
iej : h = List.get t { val := j, isLt := (_ : Nat.succ j ≤ List.length t) }
⊢ Nat.zero = Nat.succ j

State before:
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
ilt : Nat.zero < List.length (h :: t)
j : Nat
jlt : Nat.succ j < List.length (h :: t)
iej : h = List.get t { val := j, isLt := (_ : Nat.succ j ≤ List.length t) }
⊢ Nat.zero = Nat.succ j
Tactic:
let xs := differsHead p iej
State after:
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
ilt : Nat.zero < List.length (h :: t)
j : Nat
jlt : Nat.succ j < List.length (h :: t)
iej : h = List.get t { val := j, isLt := (_ : Nat.succ j ≤ List.length t) }
xs : False := differsHead p iej
⊢ Nat.zero = Nat.succ j

State before:
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
ilt : Nat.zero < List.length (h :: t)
j : Nat
jlt : Nat.succ j < List.length (h :: t)
iej : h = List.get t { val := j, isLt := (_ : Nat.succ j ≤ List.length t) }
xs : False := differsHead p iej
⊢ Nat.zero = Nat.succ j
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
jv : Nat
jlt : jv < List.length (h :: t)
i : Nat
ilt : Nat.succ i < List.length (h :: t)
iej : List.get (h :: t) { val := Nat.succ i, isLt := ilt } = List.get (h :: t) { val := jv, isLt := jlt }
⊢ Nat.succ i = jv
Tactic:
cases jv
State after:
case zero
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
i : Nat
ilt : Nat.succ i < List.length (h :: t)
jlt : Nat.zero < List.length (h :: t)
iej : List.get (h :: t) { val := Nat.succ i, isLt := ilt } = List.get (h :: t) { val := Nat.zero, isLt := jlt }
⊢ Nat.succ i = Nat.zero

case succ
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
i : Nat
ilt : Nat.succ i < List.length (h :: t)
n✝ : Nat
jlt : Nat.succ n✝ < List.length (h :: t)
iej : List.get (h :: t) { val := Nat.succ i, isLt := ilt } = List.get (h :: t) { val := Nat.succ n✝, isLt := jlt }
⊢ Nat.succ i = Nat.succ n✝

State before:
case zero
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
i : Nat
ilt : Nat.succ i < List.length (h :: t)
jlt : Nat.zero < List.length (h :: t)
iej : List.get (h :: t) { val := Nat.succ i, isLt := ilt } = List.get (h :: t) { val := Nat.zero, isLt := jlt }
⊢ Nat.succ i = Nat.zero

case succ
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
i : Nat
ilt : Nat.succ i < List.length (h :: t)
n✝ : Nat
jlt : Nat.succ n✝ < List.length (h :: t)
iej : List.get (h :: t) { val := Nat.succ i, isLt := ilt } = List.get (h :: t) { val := Nat.succ n✝, isLt := jlt }
⊢ Nat.succ i = Nat.succ n✝
Tactic:
. simp [List.get] at iej
  let xs := differsHead p iej.symm
  contradiction
State after:
case succ
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
i : Nat
ilt : Nat.succ i < List.length (h :: t)
n✝ : Nat
jlt : Nat.succ n✝ < List.length (h :: t)
iej : List.get (h :: t) { val := Nat.succ i, isLt := ilt } = List.get (h :: t) { val := Nat.succ n✝, isLt := jlt }
⊢ Nat.succ i = Nat.succ n✝

State before:
case succ
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
i : Nat
ilt : Nat.succ i < List.length (h :: t)
n✝ : Nat
jlt : Nat.succ n✝ < List.length (h :: t)
iej : List.get (h :: t) { val := Nat.succ i, isLt := ilt } = List.get (h :: t) { val := Nat.succ n✝, isLt := jlt }
⊢ Nat.succ i = Nat.succ n✝
Tactic:
. case succ j => 
  simp [List.get] at iej
  simp
  simp [differs] at p
  cases p with | intro _ tdiff =>
  let td := correctLeft t tdiff        
  let u := td _ _ iej
  simp at u
  assumption
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
i : Nat
ilt : Nat.succ i < List.length (h :: t)
j : Nat
jlt : Nat.succ j < List.length (h :: t)
iej : List.get (h :: t) { val := Nat.succ i, isLt := ilt } = List.get (h :: t) { val := Nat.succ j, isLt := jlt }
⊢ Nat.succ i = Nat.succ j
Tactic:
simp [List.get] at iej
State after:
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
i : Nat
ilt : Nat.succ i < List.length (h :: t)
j : Nat
jlt : Nat.succ j < List.length (h :: t)
iej :
  List.get t { val := i, isLt := (_ : Nat.succ i ≤ List.length t) } =
    List.get t { val := j, isLt := (_ : Nat.succ j ≤ List.length t) }
⊢ Nat.succ i = Nat.succ j

State before:
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
i : Nat
ilt : Nat.succ i < List.length (h :: t)
j : Nat
jlt : Nat.succ j < List.length (h :: t)
iej :
  List.get t { val := i, isLt := (_ : Nat.succ i ≤ List.length t) } =
    List.get t { val := j, isLt := (_ : Nat.succ j ≤ List.length t) }
⊢ Nat.succ i = Nat.succ j
Tactic:
simp
State after:
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
i : Nat
ilt : Nat.succ i < List.length (h :: t)
j : Nat
jlt : Nat.succ j < List.length (h :: t)
iej :
  List.get t { val := i, isLt := (_ : Nat.succ i ≤ List.length t) } =
    List.get t { val := j, isLt := (_ : Nat.succ j ≤ List.length t) }
⊢ i = j

State before:
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
i : Nat
ilt : Nat.succ i < List.length (h :: t)
j : Nat
jlt : Nat.succ j < List.length (h :: t)
iej :
  List.get t { val := i, isLt := (_ : Nat.succ i ≤ List.length t) } =
    List.get t { val := j, isLt := (_ : Nat.succ j ≤ List.length t) }
⊢ i = j
Tactic:
simp [differs] at p
State after:
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
i : Nat
ilt : Nat.succ i < List.length (h :: t)
j : Nat
jlt : Nat.succ j < List.length (h :: t)
iej :
  List.get t { val := i, isLt := (_ : Nat.succ i ≤ List.length t) } =
    List.get t { val := j, isLt := (_ : Nat.succ j ≤ List.length t) }
p : (List.all t fun x => x != h) = true ∧ differs t = true
⊢ i = j

State before:
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
i : Nat
ilt : Nat.succ i < List.length (h :: t)
j : Nat
jlt : Nat.succ j < List.length (h :: t)
iej :
  List.get t { val := i, isLt := (_ : Nat.succ i ≤ List.length t) } =
    List.get t { val := j, isLt := (_ : Nat.succ j ≤ List.length t) }
p : (List.all t fun x => x != h) = true ∧ differs t = true
⊢ i = j
Tactic:
cases p with | intro _ tdiff =>
let td := correctLeft t tdiff        
let u := td _ _ iej
simp at u
assumption
State after:
no goals

State before:
case intro
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
i : Nat
ilt : Nat.succ i < List.length (h :: t)
j : Nat
jlt : Nat.succ j < List.length (h :: t)
iej :
  List.get t { val := i, isLt := (_ : Nat.succ i ≤ List.length t) } =
    List.get t { val := j, isLt := (_ : Nat.succ j ≤ List.length t) }
left✝ : (List.all t fun x => x != h) = true
tdiff : differs t = true
⊢ i = j
Tactic:
let td := correctLeft t tdiff
State after:
case intro
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
i : Nat
ilt : Nat.succ i < List.length (h :: t)
j : Nat
jlt : Nat.succ j < List.length (h :: t)
iej :
  List.get t { val := i, isLt := (_ : Nat.succ i ≤ List.length t) } =
    List.get t { val := j, isLt := (_ : Nat.succ j ≤ List.length t) }
left✝ : (List.all t fun x => x != h) = true
tdiff : differs t = true
td : DifferentList t := correctLeft t tdiff
⊢ i = j

State before:
case intro
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
i : Nat
ilt : Nat.succ i < List.length (h :: t)
j : Nat
jlt : Nat.succ j < List.length (h :: t)
iej :
  List.get t { val := i, isLt := (_ : Nat.succ i ≤ List.length t) } =
    List.get t { val := j, isLt := (_ : Nat.succ j ≤ List.length t) }
left✝ : (List.all t fun x => x != h) = true
tdiff : differs t = true
td : DifferentList t := correctLeft t tdiff
⊢ i = j
Tactic:
let u := td _ _ iej
State after:
case intro
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
i : Nat
ilt : Nat.succ i < List.length (h :: t)
j : Nat
jlt : Nat.succ j < List.length (h :: t)
iej :
  List.get t { val := i, isLt := (_ : Nat.succ i ≤ List.length t) } =
    List.get t { val := j, isLt := (_ : Nat.succ j ≤ List.length t) }
left✝ : (List.all t fun x => x != h) = true
tdiff : differs t = true
td : DifferentList t := correctLeft t tdiff
u : { val := i, isLt := (_ : Nat.succ i ≤ List.length t) } = { val := j, isLt := (_ : Nat.succ j ≤ List.length t) } :=
  td { val := i, isLt := List.get._sunfold.proof_1 h t i ilt } { val := j, isLt := List.get._sunfold.proof_1 h t j jlt }
    iej
⊢ i = j

State before:
case intro
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
i : Nat
ilt : Nat.succ i < List.length (h :: t)
j : Nat
jlt : Nat.succ j < List.length (h :: t)
iej :
  List.get t { val := i, isLt := (_ : Nat.succ i ≤ List.length t) } =
    List.get t { val := j, isLt := (_ : Nat.succ j ≤ List.length t) }
left✝ : (List.all t fun x => x != h) = true
tdiff : differs t = true
td : DifferentList t := correctLeft t tdiff
u : { val := i, isLt := (_ : Nat.succ i ≤ List.length t) } = { val := j, isLt := (_ : Nat.succ j ≤ List.length t) } :=
  td { val := i, isLt := List.get._sunfold.proof_1 h t i ilt } { val := j, isLt := List.get._sunfold.proof_1 h t j jlt }
    iej
⊢ i = j
Tactic:
simp at u
State after:
case intro
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
i : Nat
ilt : Nat.succ i < List.length (h :: t)
j : Nat
jlt : Nat.succ j < List.length (h :: t)
iej :
  List.get t { val := i, isLt := (_ : Nat.succ i ≤ List.length t) } =
    List.get t { val := j, isLt := (_ : Nat.succ j ≤ List.length t) }
left✝ : (List.all t fun x => x != h) = true
tdiff : differs t = true
td : DifferentList t := correctLeft t tdiff
u : i = j
⊢ i = j

State before:
case intro
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
i : Nat
ilt : Nat.succ i < List.length (h :: t)
j : Nat
jlt : Nat.succ j < List.length (h :: t)
iej :
  List.get t { val := i, isLt := (_ : Nat.succ i ≤ List.length t) } =
    List.get t { val := j, isLt := (_ : Nat.succ j ≤ List.length t) }
left✝ : (List.all t fun x => x != h) = true
tdiff : differs t = true
td : DifferentList t := correctLeft t tdiff
u : i = j
⊢ i = j
Tactic:
assumption
State after:
no goals