-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem firstM_toArray [Alternative m] (as : List α) (f : α → m β) :
    as.toArray.firstM f = as.firstM f

Proof state:
case succ.isFalse
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Alternative m
as : List α
f : α → m β
i : Nat
ih : i ≤ as.length → firstM.go f as.toArray (as.length - i) = firstM f (drop (as.length - i) as)
h : as.length ≤ as.length - (i + 1)
⊢ i + 1 ≤ as.length → failure = firstM f (drop (as.length - (i + 1)) as)

Tactic:
have : as.length = 0 := by omega

Result:
case succ.isFalse
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Alternative m
as : List α
f : α → m β
i : Nat
ih : i ≤ as.length → firstM.go f as.toArray (as.length - i) = firstM f (drop (as.length - i) as)
h : as.length ≤ as.length - (i + 1)
this : as.length = 0
⊢ i + 1 ≤ as.length → failure = firstM f (drop (as.length - (i + 1)) as)

Proof state:
case succ
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Alternative m
as : List α
f : α → m β
i : Nat
ih : i ≤ as.length → firstM.go f as.toArray (as.length - i) = firstM f (drop (as.length - i) as)
⊢ i + 1 ≤ as.length →
    (if hlt : as.length - (i + 1) < as.toArray.size then
        f as.toArray[as.length - (i + 1)] <|> firstM.go f as.toArray (as.length - (i + 1) + 1)
      else failure) =
      firstM f (drop (as.length - (i + 1)) as)

Tactic:
split <;> rename_i h

Result:
case succ.isTrue
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Alternative m
as : List α
f : α → m β
i : Nat
ih : i ≤ as.length → firstM.go f as.toArray (as.length - i) = firstM f (drop (as.length - i) as)
h : as.length - (i + 1) < as.toArray.size
⊢ i + 1 ≤ as.length →
    (f as.toArray[as.length - (i + 1)] <|> firstM.go f as.toArray (as.length - (i + 1) + 1)) =
      firstM f (drop (as.length - (i + 1)) as)

case succ.isFalse
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Alternative m
as : List α
f : α → m β
i : Nat
ih : i ≤ as.length → firstM.go f as.toArray (as.length - i) = firstM f (drop (as.length - i) as)
h : ¬as.length - (i + 1) < as.toArray.size
⊢ i + 1 ≤ as.length → failure = firstM f (drop (as.length - (i + 1)) as)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Alternative m
as : List α
f : α → m β
i : Nat
ih : i ≤ as.length → firstM.go f as.toArray (as.length - i) = firstM f (drop (as.length - i) as)
h : as.length ≤ as.length - (i + 1)
⊢ as.length = 0

Tactic:
omega

Result:
no goals

Proof state:
case zero
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Alternative m
as : List α
f : α → m β
⊢ 0 ≤ as.length → firstM.go f as.toArray (as.length - 0) = firstM f (drop (as.length - 0) as)

Tactic:
simp [firstM.go]

Result:
no goals

Proof state:
case succ
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Alternative m
as : List α
f : α → m β
i : Nat
ih : i ≤ as.length → firstM.go f as.toArray (as.length - i) = firstM f (drop (as.length - i) as)
⊢ i + 1 ≤ as.length → firstM.go f as.toArray (as.length - (i + 1)) = firstM f (drop (as.length - (i + 1)) as)

Tactic:
unfold firstM.go

Result:
case succ
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Alternative m
as : List α
f : α → m β
i : Nat
ih : i ≤ as.length → firstM.go f as.toArray (as.length - i) = firstM f (drop (as.length - i) as)
⊢ i + 1 ≤ as.length →
    (if hlt : as.length - (i + 1) < as.toArray.size then
        f as.toArray[as.length - (i + 1)] <|> firstM.go f as.toArray (as.length - (i + 1) + 1)
      else failure) =
      firstM f (drop (as.length - (i + 1)) as)

Proof state:
case succ.isTrue
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Alternative m
as : List α
f : α → m β
i : Nat
h : as.length - (i + 1) < as.toArray.size
h' : i + 1 ≤ as.length
ih : firstM.go f as.toArray (as.length - i) = firstM f (drop (as.length - i) as)
⊢ (f as.toArray[as.length - (i + 1)] <|> firstM.go f as.toArray (as.length - (i + 1) + 1)) =
    firstM f (as.toArray.toList[as.length - (i + 1)] :: drop (as.length - (i + 1) + 1) as.toArray.toList)

Tactic:
have : as.length - (i + 1) + 1 = as.length - i := by omega

Result:
case succ.isTrue
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Alternative m
as : List α
f : α → m β
i : Nat
h : as.length - (i + 1) < as.toArray.size
h' : i + 1 ≤ as.length
ih : firstM.go f as.toArray (as.length - i) = firstM f (drop (as.length - i) as)
this : as.length - (i + 1) + 1 = as.length - i
⊢ (f as.toArray[as.length - (i + 1)] <|> firstM.go f as.toArray (as.length - (i + 1) + 1)) =
    firstM f (as.toArray.toList[as.length - (i + 1)] :: drop (as.length - (i + 1) + 1) as.toArray.toList)