-- 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)
this : as.length = 0
⊢ i + 1 ≤ as.length → failure = firstM f (drop (as.length - (i + 1)) as)

Tactic:
simp_all

Result:
no goals

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

Tactic:
intro i

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Alternative m
as : List α
f : α → m β
i : Nat
⊢ i ≤ as.length → firstM.go f as.toArray (as.length - i) = firstM f (drop (as.length - i) 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
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 (as.toArray.toList[as.length - (i + 1)] :: drop (as.length - (i + 1) + 1) as.toArray.toList)

Tactic:
intro 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
h' : i + 1 ≤ as.length
⊢ (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)

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
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)

Tactic:
rw [drop_eq_getElem_cons 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 (as.toArray.toList[as.length - (i + 1)] :: drop (as.length - (i + 1) + 1) as.toArray.toList)

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 - (i + 1) < as.toArray.size
⊢ i + 1 ≤ as.length → failure = firstM f (drop (as.length - (i + 1)) as)

Tactic:
simp only [size_toArray, Nat.not_lt] at h

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)
⊢ i + 1 ≤ as.length → 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
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
h' : i + 1 ≤ as.length
⊢ (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:
specialize ih (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)
⊢ (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)

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)
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)

Tactic:
simp_all [ih]

Result:
no goals

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 - (i + 1) < as.toArray.size
h' : i + 1 ≤ as.length
⊢ i ≤ as.length

Tactic:
omega

Result:
no goals

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

Tactic:
simpa

Result:
no goals

Proof state:
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)
⊢ as.length - (i + 1) + 1 = as.length - i

Tactic:
omega

Result:
no goals

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

Tactic:
specialize this as.length

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

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Alternative m
as : List α
f : α → m β
⊢ firstM.go f as.toArray 0 = firstM f as

Tactic:
suffices ∀ i, i ≤ as.length → firstM.go f as.toArray (as.length - i) = firstM f (as.drop (as.length - i)) by
  specialize this as.length
  simpa

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Alternative m
as : List α
f : α → m β
⊢ ∀ (i : Nat), i ≤ as.length → firstM.go f as.toArray (as.length - i) = firstM f (drop (as.length - i) as)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Alternative m
as : List α
f : α → m β
⊢ Array.firstM f as.toArray = firstM f as

Tactic:
unfold Array.firstM

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Alternative m
as : List α
f : α → m β
⊢ firstM.go f as.toArray 0 = firstM f as