-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Basic.lean
theorem findIdx?_loop_eq_map_findFinIdx?_loop_val {xs : Array α} {p : α → Bool} {j} :
    findIdx?.loop p xs j = (findFinIdx?.loop p xs j).map (·.val)

Proof state:
case isTrue
α : Type u
xs : Array α
p : α → Bool
j : Nat
h : j < xs.size
h✝ : p (getElem xs j h) = true
⊢ some j = Option.map (fun x => ↑x) (some ⟨j, h⟩)

case isFalse
α : Type u
xs : Array α
p : α → Bool
j : Nat
h : j < xs.size
h✝ : ¬p (getElem xs j h) = true
⊢ findIdx?.loop p xs (j + 1) = Option.map (fun x => ↑x) (findFinIdx?.loop p xs (j + 1))

Tactic:
case isTrue => simp

Result:
case isFalse
α : Type u
xs : Array α
p : α → Bool
j : Nat
h : j < xs.size
h✝ : ¬p (getElem xs j h) = true
⊢ findIdx?.loop p xs (j + 1) = Option.map (fun x => ↑x) (findFinIdx?.loop p xs (j + 1))

Proof state:
α : Type u
xs : Array α
p : α → Bool
j : Nat
⊢ (if h : j < xs.size then ite (p (getElem xs j h) = true) (some j) (findIdx?.loop p xs (j + 1)) else none) =
    Option.map (fun x => ↑x)
      (if h : j < xs.size then ite (p (getElem xs j h) = true) (some ⟨j, h⟩) (findFinIdx?.loop p xs (j + 1)) else none)

Tactic:
split <;> rename_i h

Result:
case isTrue
α : Type u
xs : Array α
p : α → Bool
j : Nat
h : j < xs.size
⊢ ite (p (getElem xs j h) = true) (some j) (findIdx?.loop p xs (j + 1)) =
    Option.map (fun x => ↑x) (ite (p (getElem xs j h) = true) (some ⟨j, h⟩) (findFinIdx?.loop p xs (j + 1)))

case isFalse
α : Type u
xs : Array α
p : α → Bool
j : Nat
h : ¬j < xs.size
⊢ none = Option.map (fun x => ↑x) none

Proof state:
case isFalse
α : Type u
xs : Array α
p : α → Bool
j : Nat
h : ¬j < xs.size
⊢ none = Option.map (fun x => ↑x) none

Tactic:
case isFalse => simp

Result:
no goals

Proof state:
case isTrue
α : Type u
xs : Array α
p : α → Bool
j : Nat
h : j < xs.size
⊢ ite (p (getElem xs j h) = true) (some j) (findIdx?.loop p xs (j + 1)) =
    Option.map (fun x => ↑x) (ite (p (getElem xs j h) = true) (some ⟨j, h⟩) (findFinIdx?.loop p xs (j + 1)))

case isFalse
α : Type u
xs : Array α
p : α → Bool
j : Nat
h : ¬j < xs.size
⊢ none = Option.map (fun x => ↑x) none

Tactic:
case isTrue =>
  split
  case isTrue => simp
  case isFalse =>
    have : xs.size - (j + 1) < xs.size - j := Nat.sub_succ_lt_self xs.size j h
    rw [findIdx?_loop_eq_map_findFinIdx?_loop_val (j := j + 1)]

Result:
case isFalse
α : Type u
xs : Array α
p : α → Bool
j : Nat
h : ¬j < xs.size
⊢ none = Option.map (fun x => ↑x) none

Proof state:
case isFalse
α : Type u
xs : Array α
p : α → Bool
j : Nat
h : j < xs.size
h✝ : ¬p (getElem xs j h) = true
⊢ findIdx?.loop p xs (j + 1) = Option.map (fun x => ↑x) (findFinIdx?.loop p xs (j + 1))

Tactic:
case isFalse =>
  have : xs.size - (j + 1) < xs.size - j := Nat.sub_succ_lt_self xs.size j h
  rw [findIdx?_loop_eq_map_findFinIdx?_loop_val (j := j + 1)]

Result:
no goals

Proof state:
α : Type u
xs : Array α
p : α → Bool
j : Nat
h : j < xs.size
h✝ : ¬p (getElem xs j h) = true
⊢ findIdx?.loop p xs (j + 1) = Option.map (fun x => ↑x) (findFinIdx?.loop p xs (j + 1))

Tactic:
have : xs.size - (j + 1) < xs.size - j := Nat.sub_succ_lt_self xs.size j h

Result:
α : Type u
xs : Array α
p : α → Bool
j : Nat
h : j < xs.size
h✝ : ¬p (getElem xs j h) = true
this : xs.size - (j + 1) < xs.size - j
⊢ findIdx?.loop p xs (j + 1) = Option.map (fun x => ↑x) (findFinIdx?.loop p xs (j + 1))

Proof state:
α : Type u
xs : Array α
p : α → Bool
j : Nat
h : j < xs.size
h✝ : p (getElem xs j h) = true
⊢ some j = Option.map (fun x => ↑x) (some ⟨j, h⟩)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
xs : Array α
p : α → Bool
j : Nat
h : j < xs.size
h✝ : ¬p (getElem xs j h) = true
this : xs.size - (j + 1) < xs.size - j
⊢ findIdx?.loop p xs (j + 1) = Option.map (fun x => ↑x) (findFinIdx?.loop p xs (j + 1))

Tactic:
rw [findIdx?_loop_eq_map_findFinIdx?_loop_val (j := j + 1)]

Result:
no goals

Proof state:
α : Type u
xs : Array α
p : α → Bool
j : Nat
⊢ findIdx?.loop p xs j = Option.map (fun x => ↑x) (findFinIdx?.loop p xs j)

Tactic:
unfold findIdx?.loop

Result:
α : Type u
xs : Array α
p : α → Bool
j : Nat
⊢ (if h : j < xs.size then ite (p (getElem xs j h) = true) (some j) (findIdx?.loop p xs (j + 1)) else none) =
    Option.map (fun x => ↑x) (findFinIdx?.loop p xs j)

Proof state:
α : Type u
xs : Array α
p : α → Bool
j : Nat
h : j < xs.size
⊢ ite (p (getElem xs j h) = true) (some j) (findIdx?.loop p xs (j + 1)) =
    Option.map (fun x => ↑x) (ite (p (getElem xs j h) = true) (some ⟨j, h⟩) (findFinIdx?.loop p xs (j + 1)))

Tactic:
split

Result:
case isTrue
α : Type u
xs : Array α
p : α → Bool
j : Nat
h : j < xs.size
h✝ : p (getElem xs j h) = true
⊢ some j = Option.map (fun x => ↑x) (some ⟨j, h⟩)

case isFalse
α : Type u
xs : Array α
p : α → Bool
j : Nat
h : j < xs.size
h✝ : ¬p (getElem xs j h) = true
⊢ findIdx?.loop p xs (j + 1) = Option.map (fun x => ↑x) (findFinIdx?.loop p xs (j + 1))

Proof state:
α : Type u
xs : Array α
p : α → Bool
j : Nat
h : ¬j < xs.size
⊢ none = Option.map (fun x => ↑x) none

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
xs : Array α
p : α → Bool
j : Nat
⊢ (if h : j < xs.size then ite (p (getElem xs j h) = true) (some j) (findIdx?.loop p xs (j + 1)) else none) =
    Option.map (fun x => ↑x) (findFinIdx?.loop p xs j)

Tactic:
unfold findFinIdx?.loop

Result:
α : Type u
xs : Array α
p : α → Bool
j : Nat
⊢ (if h : j < xs.size then ite (p (getElem xs j h) = true) (some j) (findIdx?.loop p xs (j + 1)) else none) =
    Option.map (fun x => ↑x)
      (if h : j < xs.size then ite (p (getElem xs j h) = true) (some ⟨j, h⟩) (findFinIdx?.loop p xs (j + 1)) else none)