internlm/Lean-Github huggingface dataset:
Theorem: listAllCorrect
Proof state before:
α : Type u_1
p : α → Bool
h : α
t : List α
first : p h = true
rest : List.foldr (fun a r => p a && r) true t = true
iv : Nat
ilt : Nat.succ iv < List.length (h :: t)
⊢ p (List.get t { val := iv, isLt := (_ : Nat.succ iv ≤ List.length t) }) = true
Tactic:
apply listAllCorrect
Proof state after:
case a
α : Type u_1
p : α → Bool
h : α
t : List α
first : p h = true
rest : List.foldr (fun a r => p a && r) true t = true
iv : Nat
ilt : Nat.succ iv < List.length (h :: t)
⊢ List.all t p = true
Theorem: listAllCorrect
Proof state before:
case a
α : Type u_1
p : α → Bool
h : α
t : List α
first : p h = true
rest : List.foldr (fun a r => p a && r) true t = true
iv : Nat
ilt : Nat.succ iv < List.length (h :: t)
⊢ List.all t p = true
Tactic:
assumption
Proof state after:
no goals
Theorem: differsHead
Proof 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
Proof 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
Theorem: differsHead
Proof 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
Proof 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
Theorem: differsHead
Proof 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
Proof 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
Theorem: differsHead
Proof 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
Proof state after:
no goals
Theorem: differsHead
Proof 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
Proof 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
Theorem: differsHead
Proof 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
Proof 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
Theorem: differsHead
Proof 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
Proof 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
Theorem: differsHead
Proof 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
Proof 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
Theorem: differsHead
Proof 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
Proof state after:
no goals
Theorem: correctLeft
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
xs : List α
p : differs xs = true
⊢ DifferentList xs
Tactic:
cases xs
Proof 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✝)
Theorem: correctLeft
Proof 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
Proof state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
p : differs (head✝ :: tail✝) = true
⊢ DifferentList (head✝ :: tail✝)
Theorem: correctLeft
Proof 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
Proof state after:
no goals
Theorem: correctLeft
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
⊢ DifferentList (h :: t)
Tactic:
unfold DifferentList
Proof 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
Theorem: correctLeft
Proof 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
Proof 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
Theorem: correctLeft
Proof 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
Proof state after:
no goals
Theorem: correctLeft
Proof 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
Proof state after:
no goals
Theorem: correctLeft
Proof 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
Proof 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
Theorem: correctLeft
Proof 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
Proof 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
Theorem: correctLeft
Proof 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
Proof 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
Theorem: correctLeft
Proof 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
Proof 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
Theorem: correctLeft
Proof 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
Proof state after:
no goals
Theorem: correctLeft
Proof 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
Proof 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
Theorem: correctLeft
Proof 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
Proof 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
Theorem: correctLeft
Proof 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
Proof state after:
no goals
Theorem: correctLeft
Proof 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
Proof 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✝
Theorem: correctLeft
Proof 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
Proof 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✝
Theorem: correctLeft
Proof 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
Proof state after:
no goals
Theorem: correctLeft
Proof 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
Proof 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
Theorem: correctLeft
Proof 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
Proof 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
Theorem: correctLeft
Proof 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
Proof 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
Theorem: correctLeft
Proof 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
Proof state after:
no goals
Theorem: correctLeft
Proof 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
Proof 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
Theorem: correctLeft
Proof 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
Proof 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
Theorem: correctLeft
Proof 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
Proof 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