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

State before:
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
⊢ p (search h)
Tactic:
unfold search
State after:
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
⊢ p
    (match hi : Index.find? fun i => decide ((fun i => p i) i) with
    | some i => i
    | none => absurd h ⋯)

State before:
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
⊢ p
    (match hi : Index.find? fun i => decide ((fun i => p i) i) with
    | some i => i
    | none => absurd h ⋯)
Tactic:
split
State after:
case h_1
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
i✝ : xs.Index
heq✝ : (Index.find? fun i => decide ((fun i => p i) i)) = some i✝
⊢ p i✝

case h_2
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
heq✝ : (Index.find? fun i => decide ((fun i => p i) i)) = none
⊢ p (absurd h ⋯)

State before:
case h_1
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
i✝ : xs.Index
heq✝ : (Index.find? fun i => decide ((fun i => p i) i)) = some i✝
⊢ p i✝

case h_2
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
heq✝ : (Index.find? fun i => decide ((fun i => p i) i)) = none
⊢ p (absurd h ⋯)
Tactic:
next h =>
  apply of_decide_eq_true
  exact find_some _ h
State after:
case h_2
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
heq✝ : (Index.find? fun i => decide ((fun i => p i) i)) = none
⊢ p (absurd h ⋯)

State before:
case h_2
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
heq✝ : (Index.find? fun i => decide ((fun i => p i) i)) = none
⊢ p (absurd h ⋯)
Tactic:
next f =>
  absurd h
  intro ⟨j, hj⟩
  have := find_none j f
  rw [decide_eq_true hj] at this
  contradiction
State after:
no goals

State before:
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h✝ : ∃ i, p i
i✝ : xs.Index
h : (Index.find? fun i => decide ((fun i => p i) i)) = some i✝
⊢ p i✝
Tactic:
apply of_decide_eq_true
State after:
case a
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h✝ : ∃ i, p i
i✝ : xs.Index
h : (Index.find? fun i => decide ((fun i => p i) i)) = some i✝
⊢ decide (p i✝) = true

State before:
case a
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h✝ : ∃ i, p i
i✝ : xs.Index
h : (Index.find? fun i => decide ((fun i => p i) i)) = some i✝
⊢ decide (p i✝) = true
Tactic:
exact find_some _ h
State after:
no goals

State before:
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
f : (Index.find? fun i => decide ((fun i => p i) i)) = none
⊢ p (absurd h ⋯)
Tactic:
absurd h
State after:
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
f : (Index.find? fun i => decide ((fun i => p i) i)) = none
⊢ ¬∃ i, p i

State before:
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
f : (Index.find? fun i => decide ((fun i => p i) i)) = none
⊢ ¬∃ i, p i
Tactic:
intro ⟨j, hj⟩
State after:
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
f : (Index.find? fun i => decide ((fun i => p i) i)) = none
j : xs.Index
hj : p j
⊢ False

State before:
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
f : (Index.find? fun i => decide ((fun i => p i) i)) = none
j : xs.Index
hj : p j
⊢ False
Tactic:
have := find_none j f
State after:
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
f : (Index.find? fun i => decide ((fun i => p i) i)) = none
j : xs.Index
hj : p j
this : decide ((fun i => p i) j) = false
⊢ False

State before:
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
f : (Index.find? fun i => decide ((fun i => p i) i)) = none
j : xs.Index
hj : p j
this : decide ((fun i => p i) j) = false
⊢ False
Tactic:
rw [decide_eq_true hj] at this
State after:
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
f : (Index.find? fun i => decide ((fun i => p i) i)) = none
j : xs.Index
hj : p j
this : true = false
⊢ False

State before:
α✝ : Type u_1
xs : List α✝
p : xs.Index → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
f : (Index.find? fun i => decide ((fun i => p i) i)) = none
j : xs.Index
hj : p j
this : true = false
⊢ False
Tactic:
contradiction
State after:
no goals