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

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
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

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
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

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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
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

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
State after:
no goals

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]
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

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
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

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
State after:
no goals

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
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

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
State after:
no goals