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

State before:
case nil
α✝ : Type u_1
p : [].Index → Bool
i : [].Index
⊢ Index.find? p = some i → p i = true
Tactic:
contradiction
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 = some i → p i = true
p : (x :: xs).Index → Bool
i : (x :: xs).Index
⊢ Index.find? p = some i → p i = true
Tactic:
intro heq
State after:
case cons
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = some i → p i = true
p : (x :: xs).Index → Bool
i : (x :: xs).Index
heq : Index.find? p = some i
⊢ p i = true

State before:
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = some i → p i = true
p : (x :: xs).Index → Bool
i : (x :: xs).Index
heq : Index.find? p = some i
h : p head = true
⊢ p i = true
Tactic:
simp only [Index.find?, h, cond] at heq
State after:
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = some i → p i = true
p : (x :: xs).Index → Bool
i : (x :: xs).Index
h : p head = true
heq : some head = some i
⊢ p i = true

State before:
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = some i → p i = true
p : (x :: xs).Index → Bool
i : (x :: xs).Index
h : p head = true
heq : some head = some i
⊢ p i = true
Tactic:
rw [←Option.some.inj heq, h]
State after:
no goals

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

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

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

State before:
case h_1
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = some i → p i = true
p : (x :: xs).Index → Bool
i : (x :: xs).Index
h : p head = false
opt✝ : Option xs.Index
x✝ : xs.Index
heq✝ : (Index.find? fun i => p i.tail) = some x✝
heq : some x✝.tail = some i
⊢ p i = true
Tactic:
next h => rw [←Option.some.inj heq, 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 = some i → p i = true
p : (x :: xs).Index → Bool
i : (x :: xs).Index
h✝ : p head = false
opt✝ : Option xs.Index
x✝ : xs.Index
h : (Index.find? fun i => p i.tail) = some x✝
heq : some x✝.tail = some i
⊢ p i = true
Tactic:
rw [←Option.some.inj heq, ih _ h]
State after:
no goals

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