Theorem: Array.findP?_property (Runtime/Utilities/Extensions.lean)

State before:
α : Type u_1
p : α → Bool
a : α
as : Array α
idx : Nat
⊢ findP?.loop idx as p = some a → p a = true
Tactic:
intro h
State after:
α : Type u_1
p : α → Bool
a : α
as : Array α
idx : Nat
h : findP?.loop idx as p = some a
⊢ p a = true

State before:
α : Type u_1
p : α → Bool
a : α
as : Array α
idx : Nat
h : findP?.loop idx as p = some a
⊢ p a = true
Tactic:
unfold findP?.loop at h
State after:
α : Type u_1
p : α → Bool
a : α
as : Array α
idx : Nat
h :
  (if h : idx < size as then
      let a := as[idx];
      if p a = true then some a else findP?.loop (idx + 1) as p
    else none) =
    some a
⊢ p a = true

State before:
α : Type u_1
p : α → Bool
a : α
as : Array α
idx : Nat
h :
  (if h : idx < size as then
      let a := as[idx];
      if p a = true then some a else findP?.loop (idx + 1) as p
    else none) =
    some a
⊢ p a = true
Tactic:
split at h <;> simp at h
State after:
case inl
α : Type u_1
p : α → Bool
a : α
as : Array α
idx : Nat
h✝ : idx < size as
h : (if p as[idx] = true then some as[idx] else findP?.loop (idx + 1) as p) = some a
⊢ p a = true

State before:
α : Type u_1
p : α → Bool
a : α
as : Array α
idx : Nat
hi : idx < size as
h : (if p as[idx] = true then some as[idx] else findP?.loop (idx + 1) as p) = some a
⊢ p a = true
Tactic:
case inl hi =>
  split at h
  case inl => simp_all
  case inr => exact go h
State after:
no goals

State before:
α : Type u_1
p : α → Bool
a : α
as : Array α
idx : Nat
hi : idx < size as
h : (if p as[idx] = true then some as[idx] else findP?.loop (idx + 1) as p) = some a
⊢ p a = true
Tactic:
split at h
State after:
case inl
α : Type u_1
p : α → Bool
a : α
as : Array α
idx : Nat
hi : idx < size as
h✝ : p as[idx] = true
h : some as[idx] = some a
⊢ p a = true

case inr
α : Type u_1
p : α → Bool
a : α
as : Array α
idx : Nat
hi : idx < size as
h✝ : ¬p as[idx] = true
h : findP?.loop (idx + 1) as p = some a
⊢ p a = true

State before:
α : Type u_1
p : α → Bool
a : α
as : Array α
idx : Nat
hi : idx < size as
h✝ : p as[idx] = true
h : some as[idx] = some a
⊢ p a = true
Tactic:
case inl => simp_all
State after:
no goals

State before:
α : Type u_1
p : α → Bool
a : α
as : Array α
idx : Nat
hi : idx < size as
h✝ : ¬p as[idx] = true
h : findP?.loop (idx + 1) as p = some a
⊢ p a = true
Tactic:
case inr => exact go h
State after:
no goals

State before:
α : Type u_1
p : α → Bool
a : α
as : Array α
idx : Nat
hi : idx < size as
h✝ : p as[idx] = true
h : some as[idx] = some a
⊢ p a = true
Tactic:
simp_all
State after:
no goals

State before:
α : Type u_1
p : α → Bool
a : α
as : Array α
idx : Nat
hi : idx < size as
h✝ : ¬p as[idx] = true
h : findP?.loop (idx + 1) as p = some a
⊢ p a = true
Tactic:
exact go h
State after:
no goals