Theorem: List.Index.find_none (Extra/Index/Basic.lean)

State before:
case nil
α✝ : Type u_1
p : [].Index → Bool
i : [].Index
⊢ Index.find? p = none → p i = false
Tactic:
cases i
State after:
no goals

State before:
case cons
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
i : (x :: xs).Index
⊢ Index.find? p = none → p i = false
Tactic:
intro heq
State after:
case cons
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
i : (x :: xs).Index
heq : Index.find? p = none
⊢ p i = false

State before:
case cons
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
i : (x :: xs).Index
heq : Index.find? p = none
⊢ p i = false
Tactic:
simp only [Index.find?, cond, Option.map] at heq
State after:
case cons
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
i : (x :: xs).Index
heq :
  (match p head with
    | true => some head
    | false =>
      match Index.find? fun i => p i.tail with
      | some x_1 => some x_1.tail
      | none => none) =
    none
⊢ p i = false

State before:
case cons
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
i : (x :: xs).Index
heq :
  (match p head with
    | true => some head
    | false =>
      match Index.find? fun i => p i.tail with
      | some x_1 => some x_1.tail
      | none => none) =
    none
⊢ p i = false
Tactic:
split at heq
State after:
case cons.h_1
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
i : (x :: xs).Index
c✝ : Bool
heq✝ : p head = true
heq : some head = none
⊢ p i = false

case cons.h_2
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
i : (x :: xs).Index
c✝ : Bool
heq✝ : p head = false
heq :
  (match Index.find? fun i => p i.tail with
    | some x_1 => some x_1.tail
    | none => none) =
    none
⊢ p i = false

State before:
case cons.h_1
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
i : (x :: xs).Index
c✝ : Bool
heq✝ : p head = true
heq : some head = none
⊢ p i = false
Tactic:
contradiction
State after:
no goals

State before:
case cons.h_2
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
i : (x :: xs).Index
c✝ : Bool
heq✝ : p head = false
heq :
  (match Index.find? fun i => p i.tail with
    | some x_1 => some x_1.tail
    | none => none) =
    none
⊢ p i = false
Tactic:
cases i
State after:
case cons.h_2.head
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
c✝ : Bool
heq✝ : p head = false
heq :
  (match Index.find? fun i => p i.tail with
    | some x_1 => some x_1.tail
    | none => none) =
    none
⊢ p head = false

case cons.h_2.tail
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
c✝ : Bool
heq✝ : p head = false
heq :
  (match Index.find? fun i => p i.tail with
    | some x_1 => some x_1.tail
    | none => none) =
    none
a✝ : xs.Index
⊢ p a✝.tail = false

State before:
case cons.h_2.head
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
c✝ : Bool
heq✝ : p head = false
heq :
  (match Index.find? fun i => p i.tail with
    | some x_1 => some x_1.tail
    | none => none) =
    none
⊢ p head = false
Tactic:
assumption
State after:
no goals

State before:
case cons.h_2.tail
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
c✝ : Bool
heq✝ : p head = false
heq :
  (match Index.find? fun i => p i.tail with
    | some x_1 => some x_1.tail
    | none => none) =
    none
a✝ : xs.Index
⊢ p a✝.tail = false
Tactic:
split at heq
State after:
case cons.h_2.tail.h_1
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
c✝ : Bool
heq✝¹ : p head = false
a✝ : xs.Index
opt✝ : Option xs.Index
x✝ : xs.Index
heq✝ : (Index.find? fun i => p i.tail) = some x✝
heq : some x✝.tail = none
⊢ p a✝.tail = false

case cons.h_2.tail.h_2
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
c✝ : Bool
heq✝¹ : p head = false
a✝ : xs.Index
opt✝ : Option xs.Index
heq✝ : (Index.find? fun i => p i.tail) = none
heq : none = none
⊢ p a✝.tail = false

State before:
case cons.h_2.tail.h_1
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
c✝ : Bool
heq✝¹ : p head = false
a✝ : xs.Index
opt✝ : Option xs.Index
x✝ : xs.Index
heq✝ : (Index.find? fun i => p i.tail) = some x✝
heq : some x✝.tail = none
⊢ p a✝.tail = false
Tactic:
contradiction
State after:
no goals

State before:
case cons.h_2.tail.h_2
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
c✝ : Bool
heq✝¹ : p head = false
a✝ : xs.Index
opt✝ : Option xs.Index
heq✝ : (Index.find? fun i => p i.tail) = none
heq : none = none
⊢ p a✝.tail = false
Tactic:
next h => rw [ih _ h]
State after:
no goals

State before:
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
c✝ : Bool
heq✝ : p head = false
a✝ : xs.Index
opt✝ : Option xs.Index
h : (Index.find? fun i => p i.tail) = none
heq : none = none
⊢ p a✝.tail = false
Tactic:
rw [ih _ h]
State after:
no goals