internlm/Lean-Github huggingface dataset:
Theorem: Packet.children_levels
Proof state before:
case h.left
x y : Nat
p : ¬(IsSingle (Single x) ∧ IsSingle (Single y))
⊢ IsSingle (Single x)

case h.right
x y : Nat
p : ¬(IsSingle (Single x) ∧ IsSingle (Single y))
⊢ IsSingle (Single y)
Tactic:
. exists x
Proof state after:
case h.right
x y : Nat
p : ¬(IsSingle (Single x) ∧ IsSingle (Single y))
⊢ IsSingle (Single y)
Theorem: Packet.children_levels
Proof state before:
case h.right
x y : Nat
p : ¬(IsSingle (Single x) ∧ IsSingle (Single y))
⊢ IsSingle (Single y)
Tactic:
. exists y
Proof state after:
no goals
Theorem: Packet.children_levels
Proof state before:
x : Nat
ys : List Packet
p : ¬(IsSingle (Single x) ∧ IsSingle (Multiple ys))
⊢ levels (children (Single x)) + levels (children (Multiple ys)) < level (Single x) + level (Multiple ys)
Tactic:
apply children_mult_levels
Proof state after:
no goals
Theorem: Packet.children_levels
Proof state before:
y : Packet
xs : List Packet
p : ¬(IsSingle (Multiple xs) ∧ IsSingle y)
⊢ levels (children (Multiple xs)) + levels (children y) < level (Multiple xs) + level y
Tactic:
conv => 
  lhs
  rw [Nat.add_comm]
Proof state after:
y : Packet
xs : List Packet
p : ¬(IsSingle (Multiple xs) ∧ IsSingle y)
⊢ levels (children y) + levels (children (Multiple xs)) < level (Multiple xs) + level y
Theorem: Packet.children_levels
Proof state before:
y : Packet
xs : List Packet
p : ¬(IsSingle (Multiple xs) ∧ IsSingle y)
⊢ levels (children y) + levels (children (Multiple xs)) < level (Multiple xs) + level y
Tactic:
conv => 
  rhs
  rw [Nat.add_comm]
Proof state after:
y : Packet
xs : List Packet
p : ¬(IsSingle (Multiple xs) ∧ IsSingle y)
⊢ levels (children y) + levels (children (Multiple xs)) < level y + level (Multiple xs)
Theorem: Packet.children_levels
Proof state before:
y : Packet
xs : List Packet
p : ¬(IsSingle (Multiple xs) ∧ IsSingle y)
⊢ levels (children y) + levels (children (Multiple xs)) < level y + level (Multiple xs)
Tactic:
apply children_mult_levels
Proof state after:
no goals
Theorem: Packet.sum_lt
Proof state before:
x y : Nat
⊢ x < x + y + 1
Tactic:
rw [Nat.add_assoc]
Proof state after:
x y : Nat
⊢ x < x + (y + 1)
Theorem: Packet.sum_lt
Proof state before:
x y : Nat
⊢ x < x + (y + 1)
Tactic:
apply @Nat.add_lt_add_left 0
Proof state after:
case h
x y : Nat
⊢ 0 < y + 1
Theorem: Packet.sum_lt
Proof state before:
case h
x y : Nat
⊢ 0 < y + 1
Tactic:
apply Nat.zero_lt_succ
Proof state after:
no goals
Theorem: Packet.sum_lt'
Proof state before:
x y : Nat
⊢ x < y + x + 1
Tactic:
rw [Nat.add_comm y x]
Proof state after:
x y : Nat
⊢ x < x + y + 1
Theorem: Packet.sum_lt'
Proof state before:
x y : Nat
⊢ x < x + y + 1
Tactic:
apply sum_lt
Proof state after:
no goals
Theorem: DifListTail
Proof state before:
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
⊢ DifferentList (x :: xs) → DifferentList xs
Tactic:
intros xxs
Proof state after:
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
⊢ DifferentList xs
Theorem: DifListTail
Proof state before:
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
⊢ DifferentList xs
Tactic:
unfold DifferentList
Proof state after:
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
⊢ ∀ (i j : Fin (List.length xs)), List.get xs i = List.get xs j → i = j
Theorem: DifListTail
Proof state before:
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
⊢ ∀ (i j : Fin (List.length xs)), List.get xs i = List.get xs j → i = j
Tactic:
intros i j iej
Proof state after:
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
⊢ i = j
Theorem: DifListTail
Proof state before:
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
⊢ i = j
Tactic:
apply Fin.eq_of_val_eq
Proof state after:
case a
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
⊢ i.val = j.val
Theorem: DifListTail
Proof state before:
case a
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
⊢ i.val = j.val
Tactic:
let i1 := appendFin x xs i
Proof state after:
case a
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
i1 : Fin (List.length (x :: xs)) := appendFin x xs i
⊢ i.val = j.val
Theorem: DifListTail
Proof state before:
case a
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
i1 : Fin (List.length (x :: xs)) := appendFin x xs i
⊢ i.val = j.val
Tactic:
let j1 := appendFin x xs j
Proof state after:
case a
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
i1 : Fin (List.length (x :: xs)) := appendFin x xs i
j1 : Fin (List.length (x :: xs)) := appendFin x xs j
⊢ i.val = j.val
Theorem: DifListTail
Proof state before:
case a
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
i1 : Fin (List.length (x :: xs)) := appendFin x xs i
j1 : Fin (List.length (x :: xs)) := appendFin x xs j
⊢ i.val = j.val
Tactic:
let h1 := xxs i1 j1
Proof state after:
case a
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
i1 : Fin (List.length (x :: xs)) := appendFin x xs i
j1 : Fin (List.length (x :: xs)) := appendFin x xs j
h1 : List.get (x :: xs) i1 = List.get (x :: xs) j1 → i1 = j1 := xxs i1 j1
⊢ i.val = j.val
Theorem: DifListTail
Proof state before:
case a
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
i1 : Fin (List.length (x :: xs)) := appendFin x xs i
j1 : Fin (List.length (x :: xs)) := appendFin x xs j
h1 : List.get (x :: xs) i1 = List.get (x :: xs) j1 → i1 = j1 := xxs i1 j1
⊢ i.val = j.val
Tactic:
simp [List.get] at h1
Proof state after:
case a
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
i1 : Fin (List.length (x :: xs)) := appendFin x xs i
j1 : Fin (List.length (x :: xs)) := appendFin x xs j
h1 : List.get xs { val := i.val, isLt := (_ : Nat.succ i.val ≤ List.length xs) } =
    List.get xs { val := j.val, isLt := (_ : Nat.succ j.val ≤ List.length xs) } →
  appendFin x xs i = appendFin x xs j :=
  xxs i1 j1
⊢ i.val = j.val
Theorem: DifListTail
Proof state before:
case a
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
i1 : Fin (List.length (x :: xs)) := appendFin x xs i
j1 : Fin (List.length (x :: xs)) := appendFin x xs j
h1 : List.get xs { val := i.val, isLt := (_ : Nat.succ i.val ≤ List.length xs) } =
    List.get xs { val := j.val, isLt := (_ : Nat.succ j.val ≤ List.length xs) } →
  appendFin x xs i = appendFin x xs j :=
  xxs i1 j1
⊢ i.val = j.val
Tactic:
let i1ej1 := h1 iej
Proof state after:
case a
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
i1 : Fin (List.length (x :: xs)) := appendFin x xs i
j1 : Fin (List.length (x :: xs)) := appendFin x xs j
h1 : List.get xs { val := i.val, isLt := (_ : Nat.succ i.val ≤ List.length xs) } =
    List.get xs { val := j.val, isLt := (_ : Nat.succ j.val ≤ List.length xs) } →
  appendFin x xs i = appendFin x xs j :=
  xxs i1 j1
i1ej1 : appendFin x xs i = appendFin x xs j := h1 iej
⊢ i.val = j.val
Theorem: DifListTail
Proof state before:
case a
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
i1 : Fin (List.length (x :: xs)) := appendFin x xs i
j1 : Fin (List.length (x :: xs)) := appendFin x xs j
h1 : List.get xs { val := i.val, isLt := (_ : Nat.succ i.val ≤ List.length xs) } =
    List.get xs { val := j.val, isLt := (_ : Nat.succ j.val ≤ List.length xs) } →
  appendFin x xs i = appendFin x xs j :=
  xxs i1 j1
i1ej1 : appendFin x xs i = appendFin x xs j := h1 iej
⊢ i.val = j.val
Tactic:
simp [appendFin] at i1ej1
Proof state after:
case a
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
i1 : Fin (List.length (x :: xs)) := appendFin x xs i
j1 : Fin (List.length (x :: xs)) := appendFin x xs j
h1 : List.get xs { val := i.val, isLt := (_ : Nat.succ i.val ≤ List.length xs) } =
    List.get xs { val := j.val, isLt := (_ : Nat.succ j.val ≤ List.length xs) } →
  appendFin x xs i = appendFin x xs j :=
  xxs i1 j1
i1ej1 : i.val = j.val
⊢ i.val = j.val
Theorem: DifListTail
Proof state before:
case a
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
i1 : Fin (List.length (x :: xs)) := appendFin x xs i
j1 : Fin (List.length (x :: xs)) := appendFin x xs j
h1 : List.get xs { val := i.val, isLt := (_ : Nat.succ i.val ≤ List.length xs) } =
    List.get xs { val := j.val, isLt := (_ : Nat.succ j.val ≤ List.length xs) } →
  appendFin x xs i = appendFin x xs j :=
  xxs i1 j1
i1ej1 : i.val = j.val
⊢ i.val = j.val
Tactic:
exact i1ej1
Proof state after:
no goals
Theorem: DifListShuffle
Proof state before:
α : Type u_1
inst✝ : BEq α
x y : α
xs : List α
⊢ DifferentList (x :: y :: xs) → DifferentList (y :: x :: xs)
Tactic:
intros dl i j iej
Proof state after:
α : Type u_1
inst✝ : BEq α
x y : α
xs : List α
dl : DifferentList (x :: y :: xs)
i j : Fin (List.length (y :: x :: xs))
iej : List.get (y :: x :: xs) i = List.get (y :: x :: xs) j
⊢ i = j
Theorem: DifListShuffle
Proof state before:
α : Type u_1
inst✝ : BEq α
x y : α
xs : List α
dl : DifferentList (x :: y :: xs)
i j : Fin (List.length (y :: x :: xs))
iej : List.get (y :: x :: xs) i = List.get (y :: x :: xs) j
⊢ i = j
Tactic:
rw [shuffledGet i, shuffledGet j] at iej
Proof state after:
α : Type u_1
inst✝ : BEq α
x y : α
xs : List α
dl : DifferentList (x :: y :: xs)
i j : Fin (List.length (y :: x :: xs))
iej : List.get (x :: y :: xs) (shuffleIndex i) = List.get (x :: y :: xs) (shuffleIndex j)
⊢ i = j
Theorem: DifListShuffle
Proof state before:
α : Type u_1
inst✝ : BEq α
x y : α
xs : List α
dl : DifferentList (x :: y :: xs)
i j : Fin (List.length (y :: x :: xs))
iej : List.get (x :: y :: xs) (shuffleIndex i) = List.get (x :: y :: xs) (shuffleIndex j)
⊢ i = j
Tactic:
let siej := dl _ _ iej
Proof state after:
α : Type u_1
inst✝ : BEq α
x y : α
xs : List α
dl : DifferentList (x :: y :: xs)
i j : Fin (List.length (y :: x :: xs))
iej : List.get (x :: y :: xs) (shuffleIndex i) = List.get (x :: y :: xs) (shuffleIndex j)
siej : shuffleIndex i = shuffleIndex j := dl (shuffleIndex i) (shuffleIndex j) iej
⊢ i = j
Theorem: DifListShuffle
Proof state before:
α : Type u_1
inst✝ : BEq α
x y : α
xs : List α
dl : DifferentList (x :: y :: xs)
i j : Fin (List.length (y :: x :: xs))
iej : List.get (x :: y :: xs) (shuffleIndex i) = List.get (x :: y :: xs) (shuffleIndex j)
siej : shuffleIndex i = shuffleIndex j := dl (shuffleIndex i) (shuffleIndex j) iej
⊢ i = j
Tactic:
let ssiej := congrArg shuffleIndex siej
Proof state after:
α : Type u_1
inst✝ : BEq α
x y : α
xs : List α
dl : DifferentList (x :: y :: xs)
i j : Fin (List.length (y :: x :: xs))
iej : List.get (x :: y :: xs) (shuffleIndex i) = List.get (x :: y :: xs) (shuffleIndex j)
siej : shuffleIndex i = shuffleIndex j := dl (shuffleIndex i) (shuffleIndex j) iej
ssiej : shuffleIndex (shuffleIndex i) = shuffleIndex (shuffleIndex j) := congrArg shuffleIndex siej
⊢ i = j
Theorem: DifListShuffle
Proof state before:
α : Type u_1
inst✝ : BEq α
x y : α
xs : List α
dl : DifferentList (x :: y :: xs)
i j : Fin (List.length (y :: x :: xs))
iej : List.get (x :: y :: xs) (shuffleIndex i) = List.get (x :: y :: xs) (shuffleIndex j)
siej : shuffleIndex i = shuffleIndex j := dl (shuffleIndex i) (shuffleIndex j) iej
ssiej : shuffleIndex (shuffleIndex i) = shuffleIndex (shuffleIndex j) := congrArg shuffleIndex siej
⊢ i = j
Tactic:
rw [shuffleCancelable, shuffleCancelable] at ssiej
Proof state after:
α : Type u_1
inst✝ : BEq α
x y : α
xs : List α
dl : DifferentList (x :: y :: xs)
i j : Fin (List.length (y :: x :: xs))
iej : List.get (x :: y :: xs) (shuffleIndex i) = List.get (x :: y :: xs) (shuffleIndex j)
siej : shuffleIndex i = shuffleIndex j := dl (shuffleIndex i) (shuffleIndex j) iej
ssiej : i = j
⊢ i = j
Theorem: DifListShuffle
Proof state before:
α : Type u_1
inst✝ : BEq α
x y : α
xs : List α
dl : DifferentList (x :: y :: xs)
i j : Fin (List.length (y :: x :: xs))
iej : List.get (x :: y :: xs) (shuffleIndex i) = List.get (x :: y :: xs) (shuffleIndex j)
siej : shuffleIndex i = shuffleIndex j := dl (shuffleIndex i) (shuffleIndex j) iej
ssiej : i = j
⊢ i = j
Tactic:
assumption
Proof state after:
no goals
Theorem: DifListHead
Proof 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
Proof state after:
α : Type u_1
da : DecidableEq α
x : α
xs : List α
h : DifferentList (x :: xs)
⊢ (List.all xs fun x_1 => x_1 != x) = true
Theorem: DifListHead
Proof 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
Proof 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
Theorem: DifListHead
Proof 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]
Proof 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
Theorem: DifListHead
Proof 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
Proof state after:
no goals
Theorem: DifListHead
Proof 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]
Proof 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
Theorem: DifListHead
Proof 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
Proof 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
Theorem: DifListHead
Proof 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]
Proof 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
Theorem: DifListHead
Proof 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
Proof state after:
no goals
Theorem: nilDifferent
Proof state before:
α : Type u_1
inst✝ : BEq α
⊢ DifferentList []
Tactic:
unfold DifferentList
Proof state after:
α : Type u_1
inst✝ : BEq α
⊢ ∀ (i j : Fin (List.length [])), List.get [] i = List.get [] j → i = j
Theorem: nilDifferent
Proof state before:
α : Type u_1
inst✝ : BEq α
⊢ ∀ (i j : Fin (List.length [])), List.get [] i = List.get [] j → i = j
Tactic:
intro i
Proof state after:
α : Type u_1
inst✝ : BEq α
i : Fin (List.length [])
⊢ ∀ (j : Fin (List.length [])), List.get [] i = List.get [] j → i = j
Theorem: nilDifferent
Proof state before:
α : Type u_1
inst✝ : BEq α
i : Fin (List.length [])
⊢ ∀ (j : Fin (List.length [])), List.get [] i = List.get [] j → i = j
Tactic:
intros
Proof state after:
α : Type u_1
inst✝ : BEq α
i j✝ : Fin (List.length [])
a✝ : List.get [] i = List.get [] j✝
⊢ i = j✝
Theorem: nilDifferent
Proof state before:
α : Type u_1
inst✝ : BEq α
i j✝ : Fin (List.length [])
a✝ : List.get [] i = List.get [] j✝
⊢ i = j✝
Tactic:
simp [List.length] at i
Proof state after:
α : Type u_1
inst✝ : BEq α
i : Fin 0
j✝ : Fin (List.length [])
a✝ : List.get [] i = List.get [] j✝
⊢ i = j✝
Theorem: nilDifferent
Proof state before:
α : Type u_1
inst✝ : BEq α
i : Fin 0
j✝ : Fin (List.length [])
a✝ : List.get [] i = List.get [] j✝
⊢ i = j✝
Tactic:
cases i.isLt
Proof state after:
no goals
Theorem: listAllCorrect
Proof state before:
α : Type u_1
xs : List α
p : α → Bool
i : Fin (List.length xs)
⊢ List.all xs p = true → p (List.get xs i) = true
Tactic:
intro all
Proof state after:
α : Type u_1
xs : List α
p : α → Bool
i : Fin (List.length xs)
all : List.all xs p = true
⊢ p (List.get xs i) = true
Theorem: listAllCorrect
Proof state before:
α : Type u_1
xs : List α
p : α → Bool
i : Fin (List.length xs)
all : List.all xs p = true
⊢ p (List.get xs i) = true
Tactic:
cases i
Proof state after:
case mk
α : Type u_1
xs : List α
p : α → Bool
all : List.all xs p = true
val✝ : Nat
isLt✝ : val✝ < List.length xs
⊢ p (List.get xs { val := val✝, isLt := isLt✝ }) = true
Theorem: listAllCorrect
Proof state before:
α : Type u_1
xs : List α
p : α → Bool
all : List.all xs p = true
iv : Nat
ilt : iv < List.length xs
⊢ p (List.get xs { val := iv, isLt := ilt }) = true
Tactic:
case mk iv ilt => 
cases xs
. contradiction
. case cons h t =>
  simp [List.all, List.foldr] at all 
  cases all with | intro first rest =>
  cases iv <;> simp [List.get]
  assumption
  case succ iv =>
  apply listAllCorrect
  assumption
Proof state after:
no goals
Theorem: listAllCorrect
Proof state before:
α : Type u_1
xs : List α
p : α → Bool
all : List.all xs p = true
iv : Nat
ilt : iv < List.length xs
⊢ p (List.get xs { val := iv, isLt := ilt }) = true
Tactic:
cases xs
Proof state after:
case nil
α : Type u_1
p : α → Bool
iv : Nat
all : List.all [] p = true
ilt : iv < List.length []
⊢ p (List.get [] { val := iv, isLt := ilt }) = true

case cons
α : Type u_1
p : α → Bool
iv : Nat
head✝ : α
tail✝ : List α
all : List.all (head✝ :: tail✝) p = true
ilt : iv < List.length (head✝ :: tail✝)
⊢ p (List.get (head✝ :: tail✝) { val := iv, isLt := ilt }) = true
Theorem: listAllCorrect
Proof state before:
case nil
α : Type u_1
p : α → Bool
iv : Nat
all : List.all [] p = true
ilt : iv < List.length []
⊢ p (List.get [] { val := iv, isLt := ilt }) = true

case cons
α : Type u_1
p : α → Bool
iv : Nat
head✝ : α
tail✝ : List α
all : List.all (head✝ :: tail✝) p = true
ilt : iv < List.length (head✝ :: tail✝)
⊢ p (List.get (head✝ :: tail✝) { val := iv, isLt := ilt }) = true
Tactic:
. contradiction
Proof state after:
case cons
α : Type u_1
p : α → Bool
iv : Nat
head✝ : α
tail✝ : List α
all : List.all (head✝ :: tail✝) p = true
ilt : iv < List.length (head✝ :: tail✝)
⊢ p (List.get (head✝ :: tail✝) { val := iv, isLt := ilt }) = true
Theorem: listAllCorrect
Proof state before:
case cons
α : Type u_1
p : α → Bool
iv : Nat
head✝ : α
tail✝ : List α
all : List.all (head✝ :: tail✝) p = true
ilt : iv < List.length (head✝ :: tail✝)
⊢ p (List.get (head✝ :: tail✝) { val := iv, isLt := ilt }) = true
Tactic:
. case cons h t =>
  simp [List.all, List.foldr] at all 
  cases all with | intro first rest =>
  cases iv <;> simp [List.get]
  assumption
  case succ iv =>
  apply listAllCorrect
  assumption
Proof state after:
no goals
Theorem: listAllCorrect
Proof state before:
α : Type u_1
p : α → Bool
iv : Nat
h : α
t : List α
all : List.all (h :: t) p = true
ilt : iv < List.length (h :: t)
⊢ p (List.get (h :: t) { val := iv, isLt := ilt }) = true
Tactic:
simp [List.all, List.foldr] at all
Proof state after:
α : Type u_1
p : α → Bool
iv : Nat
h : α
t : List α
ilt : iv < List.length (h :: t)
all : p h = true ∧ List.foldr (fun a r => p a && r) true t = true
⊢ p (List.get (h :: t) { val := iv, isLt := ilt }) = true
Theorem: listAllCorrect
Proof state before:
α : Type u_1
p : α → Bool
iv : Nat
h : α
t : List α
ilt : iv < List.length (h :: t)
all : p h = true ∧ List.foldr (fun a r => p a && r) true t = true
⊢ p (List.get (h :: t) { val := iv, isLt := ilt }) = true
Tactic:
cases all with | intro first rest =>
cases iv <;> simp [List.get]
assumption
case succ iv =>
apply listAllCorrect
assumption
Proof state after:
no goals
Theorem: listAllCorrect
Proof state before:
case intro
α : Type u_1
p : α → Bool
iv : Nat
h : α
t : List α
ilt : iv < List.length (h :: t)
first : p h = true
rest : List.foldr (fun a r => p a && r) true t = true
⊢ p (List.get (h :: t) { val := iv, isLt := ilt }) = true
Tactic:
cases iv <;> simp [List.get]
Proof state after:
case intro.zero
α : Type u_1
p : α → Bool
h : α
t : List α
first : p h = true
rest : List.foldr (fun a r => p a && r) true t = true
ilt : Nat.zero < List.length (h :: t)
⊢ p h = true

case intro.succ
α : Type u_1
p : α → Bool
h : α
t : List α
first : p h = true
rest : List.foldr (fun a r => p a && r) true t = true
n✝ : Nat
ilt : Nat.succ n✝ < List.length (h :: t)
⊢ p (List.get t { val := n✝, isLt := (_ : Nat.succ n✝ ≤ List.length t) }) = true
Theorem: listAllCorrect
Proof state before:
case intro.zero
α : Type u_1
p : α → Bool
h : α
t : List α
first : p h = true
rest : List.foldr (fun a r => p a && r) true t = true
ilt : Nat.zero < List.length (h :: t)
⊢ p h = true

case intro.succ
α : Type u_1
p : α → Bool
h : α
t : List α
first : p h = true
rest : List.foldr (fun a r => p a && r) true t = true
n✝ : Nat
ilt : Nat.succ n✝ < List.length (h :: t)
⊢ p (List.get t { val := n✝, isLt := (_ : Nat.succ n✝ ≤ List.length t) }) = true
Tactic:
assumption
Proof state after:
case intro.succ
α : Type u_1
p : α → Bool
h : α
t : List α
first : p h = true
rest : List.foldr (fun a r => p a && r) true t = true
n✝ : Nat
ilt : Nat.succ n✝ < List.length (h :: t)
⊢ p (List.get t { val := n✝, isLt := (_ : Nat.succ n✝ ≤ List.length t) }) = true
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:
case succ iv =>
apply listAllCorrect
assumption
Proof state after:
no goals