-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem findSomeRevM?_find_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α)
    (i : Nat) (h) :
    findSomeRevM?.find f l.toArray i h = (l.take i).reverse.findSomeM? f

Proof state:
case succ
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
i : Nat
ih : ∀ (l : List α) (h : i ≤ l.toArray.size), findSomeRevM?.find f l.toArray i h = findSomeM? f (take i l).reverse
l : List α
h✝ : i + 1 ≤ l.toArray.size
h : i + 1 ≤ l.length
⊢ (do
      let r ← f l.toArray[i]
      match r with
        | some val => pure r
        | none =>
          let_fun this := ⋯;
          findSomeRevM?.find f l.toArray i this) =
    findSomeM? f (take i l ++ (some l[i]).toList).reverse

Tactic:
simp only [ih, reverse_append]

Result:
case succ
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
i : Nat
ih : ∀ (l : List α) (h : i ≤ l.toArray.size), findSomeRevM?.find f l.toArray i h = findSomeM? f (take i l).reverse
l : List α
h✝ : i + 1 ≤ l.toArray.size
h : i + 1 ≤ l.length
⊢ (do
      let r ← f l.toArray[i]
      match r with
        | some val => pure r
        | none => findSomeM? f (take i l).reverse) =
    findSomeM? f ((some l[i]).toList.reverse ++ (take i l).reverse)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
l : List α
i : Nat
h : i ≤ l.toArray.size
⊢ findSomeRevM?.find f l.toArray i h = findSomeM? f (take i l).reverse

Tactic:
induction i generalizing l with
| zero => simp [Array.findSomeRevM?.find.eq_def]
| succ i ih =>
  rw [size_toArray] at h
  rw [Array.findSomeRevM?.find, take_succ, getElem?_eq_getElem (by omega)]
  simp only [ih, reverse_append]
  congr
  ext1 (_|_) <;> simp

Result:
no goals

Proof state:
case succ.e_a
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
i : Nat
ih : ∀ (l : List α) (h : i ≤ l.toArray.size), findSomeRevM?.find f l.toArray i h = findSomeM? f (take i l).reverse
l : List α
h✝ : i + 1 ≤ l.toArray.size
h : i + 1 ≤ l.length
⊢ (fun r =>
      match r with
      | some val => pure r
      | none => findSomeM? f (take i l).reverse) =
    fun __do_lift =>
    match __do_lift with
    | some b => pure (some b)
    | none => findSomeM? f ([].append (take i l).reverse)

Tactic:
ext1 (_|_) <;> simp

Result:
no goals

Proof state:
case succ
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
i : Nat
ih : ∀ (l : List α) (h : i ≤ l.toArray.size), findSomeRevM?.find f l.toArray i h = findSomeM? f (take i l).reverse
l : List α
h : i + 1 ≤ l.toArray.size
⊢ findSomeRevM?.find f l.toArray (i + 1) h = findSomeM? f (take (i + 1) l).reverse

Tactic:
rw [size_toArray] at h

Result:
case succ
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
i : Nat
ih : ∀ (l : List α) (h : i ≤ l.toArray.size), findSomeRevM?.find f l.toArray i h = findSomeM? f (take i l).reverse
l : List α
h✝ : i + 1 ≤ l.toArray.size
h : i + 1 ≤ l.length
⊢ findSomeRevM?.find f l.toArray (i + 1) h✝ = findSomeM? f (take (i + 1) l).reverse

Proof state:
case succ
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
i : Nat
ih : ∀ (l : List α) (h : i ≤ l.toArray.size), findSomeRevM?.find f l.toArray i h = findSomeM? f (take i l).reverse
l : List α
h✝ : i + 1 ≤ l.toArray.size
h : i + 1 ≤ l.length
⊢ (do
      let r ← f l.toArray[i]
      match r with
        | some val => pure r
        | none => findSomeM? f (take i l).reverse) =
    findSomeM? f ((some l[i]).toList.reverse ++ (take i l).reverse)

Tactic:
congr

Result:
case succ.e_a
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
i : Nat
ih : ∀ (l : List α) (h : i ≤ l.toArray.size), findSomeRevM?.find f l.toArray i h = findSomeM? f (take i l).reverse
l : List α
h✝ : i + 1 ≤ l.toArray.size
h : i + 1 ≤ l.length
⊢ (fun r =>
      match r with
      | some val => pure r
      | none => findSomeM? f (take i l).reverse) =
    fun __do_lift =>
    match __do_lift with
    | some b => pure (some b)
    | none => findSomeM? f ([].append (take i l).reverse)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
i : Nat
ih : ∀ (l : List α) (h : i ≤ l.toArray.size), findSomeRevM?.find f l.toArray i h = findSomeM? f (take i l).reverse
l : List α
h✝ : i + 1 ≤ l.toArray.size
h : i + 1 ≤ l.length
⊢ i < l.length

Tactic:
omega

Result:
no goals

Proof state:
case zero
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
l : List α
h : 0 ≤ l.toArray.size
⊢ findSomeRevM?.find f l.toArray 0 h = findSomeM? f (take 0 l).reverse

Tactic:
simp [Array.findSomeRevM?.find.eq_def]

Result:
no goals

Proof state:
case succ
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
i : Nat
ih : ∀ (l : List α) (h : i ≤ l.toArray.size), findSomeRevM?.find f l.toArray i h = findSomeM? f (take i l).reverse
l : List α
h✝ : i + 1 ≤ l.toArray.size
h : i + 1 ≤ l.length
⊢ findSomeRevM?.find f l.toArray (i + 1) h✝ = findSomeM? f (take (i + 1) l).reverse

Tactic:
rw [Array.findSomeRevM?.find, take_succ, getElem?_eq_getElem (by omega)]

Result:
case succ
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
i : Nat
ih : ∀ (l : List α) (h : i ≤ l.toArray.size), findSomeRevM?.find f l.toArray i h = findSomeM? f (take i l).reverse
l : List α
h✝ : i + 1 ≤ l.toArray.size
h : i + 1 ≤ l.length
⊢ (do
      let r ← f l.toArray[i]
      match r with
        | some val => pure r
        | none =>
          let_fun this := ⋯;
          findSomeRevM?.find f l.toArray i this) =
    findSomeM? f (take i l ++ (some l[i]).toList).reverse