-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem forIn'_loop_toArray [Monad m] (l : List α) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) (i : Nat)
    (h : i ≤ l.length) (b : β) :
    Array.forIn'.loop l.toArray f i h b =
      forIn' (l.drop (l.length - i)) b (fun a m b => f a (by simpa using mem_of_mem_drop m) b)

Proof state:
case succ
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
i : Nat
ih :
  ∀ (l : List α) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) (h : i ≤ l.length) (b : β),
    Array.forIn'.loop l.toArray f i h b = forIn' (drop (l.length - i) l) b fun a m b => f a ⋯ b
l : List α
f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)
h : i + 1 ≤ l.length
b : β
⊢ Array.forIn'.loop l.toArray f (i + 1) h b = forIn' (drop (l.length - (i + 1)) l) b fun a m b => f a ⋯ b

Tactic:
simp only [Array.forIn'.loop, size_toArray, getElem_toArray, ih]

Result:
case succ
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
i : Nat
ih :
  ∀ (l : List α) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) (h : i ≤ l.length) (b : β),
    Array.forIn'.loop l.toArray f i h b = forIn' (drop (l.length - i) l) b fun a m b => f a ⋯ b
l : List α
f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)
h : i + 1 ≤ l.length
b : β
⊢ (do
      let __do_lift ← f l[l.length - 1 - i] ⋯ b
      match __do_lift with
        | ForInStep.done b => pure b
        | ForInStep.yield b => forIn' (drop (l.length - i) l) b fun a m b => f a ⋯ b) =
    forIn' (drop (l.length - (i + 1)) l) b fun a m b => f a ⋯ b

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
i : Nat
ih :
  ∀ (l : List α) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) (h : i ≤ l.length) (b : β),
    Array.forIn'.loop l.toArray f i h b = forIn' (drop (l.length - i) l) b fun a m b => f a ⋯ b
l : List α
f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)
h : i + 1 ≤ l.length
b : β
t : drop (l.length - (i + 1)) l = l[l.length - i - 1] :: drop (l.length - i) l
⊢ l.length - 1 - i = l.length - i - 1

Tactic:
omega

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
i : Nat
ih :
  ∀ (l : List α) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) (h : i ≤ l.length) (b : β),
    Array.forIn'.loop l.toArray f i h b = forIn' (drop (l.length - i) l) b fun a m b => f a ⋯ b
l : List α
f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)
h : i + 1 ≤ l.length
b : β
⊢ drop (l.length - (i + 1)) l = l[l.length - i - 1] :: drop (l.length - i) l

Tactic:
simp only [Nat.sub_add_eq]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
i : Nat
ih :
  ∀ (l : List α) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) (h : i ≤ l.length) (b : β),
    Array.forIn'.loop l.toArray f i h b = forIn' (drop (l.length - i) l) b fun a m b => f a ⋯ b
l : List α
f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)
h : i + 1 ≤ l.length
b : β
⊢ drop (l.length - i - 1) l = l[l.length - i - 1] :: drop (l.length - i) l

Proof state:
case succ
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
i : Nat
ih :
  ∀ (l : List α) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) (h : i ≤ l.length) (b : β),
    Array.forIn'.loop l.toArray f i h b = forIn' (drop (l.length - i) l) b fun a m b => f a ⋯ b
l : List α
f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)
h : i + 1 ≤ l.length
b : β
t : drop (l.length - (i + 1)) l = l[l.length - i - 1] :: drop (l.length - i) l
⊢ (do
      let __do_lift ← f l[l.length - 1 - i] ⋯ b
      match __do_lift with
        | ForInStep.done b => pure b
        | ForInStep.yield b => forIn' (drop (l.length - i) l) b fun a m b => f a ⋯ b) =
    do
    let x ← f l[l.length - i - 1] ⋯ b
    match x with
      | ForInStep.done b => pure b
      | ForInStep.yield b => forIn' (drop (l.length - i) l) b fun a' m b => f a' ⋯ b

Tactic:
have t : l.length - 1 - i = l.length - i - 1 := by omega

Result:
case succ
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
i : Nat
ih :
  ∀ (l : List α) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) (h : i ≤ l.length) (b : β),
    Array.forIn'.loop l.toArray f i h b = forIn' (drop (l.length - i) l) b fun a m b => f a ⋯ b
l : List α
f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)
h : i + 1 ≤ l.length
b : β
t✝ : drop (l.length - (i + 1)) l = l[l.length - i - 1] :: drop (l.length - i) l
t : l.length - 1 - i = l.length - i - 1
⊢ (do
      let __do_lift ← f l[l.length - 1 - i] ⋯ b
      match __do_lift with
        | ForInStep.done b => pure b
        | ForInStep.yield b => forIn' (drop (l.length - i) l) b fun a m b => f a ⋯ b) =
    do
    let x ← f l[l.length - i - 1] ⋯ b
    match x with
      | ForInStep.done b => pure b
      | ForInStep.yield b => forIn' (drop (l.length - i) l) b fun a' m b => f a' ⋯ b

Proof state:
case zero
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
l : List α
f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)
h : 0 ≤ l.length
b : β
⊢ Array.forIn'.loop l.toArray f 0 h b = forIn' (drop (l.length - 0) l) b fun a m b => f a ⋯ b

Tactic:
simp [Array.forIn'.loop]

Result:
no goals

Proof state:
case succ
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
i : Nat
ih :
  ∀ (l : List α) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) (h : i ≤ l.length) (b : β),
    Array.forIn'.loop l.toArray f i h b = forIn' (drop (l.length - i) l) b fun a m b => f a ⋯ b
l : List α
f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)
h : i + 1 ≤ l.length
b : β
t✝ : drop (l.length - (i + 1)) l = l[l.length - i - 1] :: drop (l.length - i) l
t : l.length - 1 - i = l.length - i - 1
⊢ (do
      let __do_lift ← f l[l.length - 1 - i] ⋯ b
      match __do_lift with
        | ForInStep.done b => pure b
        | ForInStep.yield b => forIn' (drop (l.length - i) l) b fun a m b => f a ⋯ b) =
    do
    let x ← f l[l.length - i - 1] ⋯ b
    match x with
      | ForInStep.done b => pure b
      | ForInStep.yield b => forIn' (drop (l.length - i) l) b fun a' m b => f a' ⋯ b

Tactic:
simp only [t]

Result:
case succ
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
i : Nat
ih :
  ∀ (l : List α) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) (h : i ≤ l.length) (b : β),
    Array.forIn'.loop l.toArray f i h b = forIn' (drop (l.length - i) l) b fun a m b => f a ⋯ b
l : List α
f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)
h : i + 1 ≤ l.length
b : β
t✝ : drop (l.length - (i + 1)) l = l[l.length - i - 1] :: drop (l.length - i) l
t : l.length - 1 - i = l.length - i - 1
⊢ (do
      let __do_lift ← f l[l.length - i - 1] ⋯ b
      match __do_lift with
        | ForInStep.done b => pure b
        | ForInStep.yield b => forIn' (drop (l.length - i) l) b fun a m b => f a ⋯ b) =
    do
    let x ← f l[l.length - i - 1] ⋯ b
    match x with
      | ForInStep.done b => pure b
      | ForInStep.yield b => forIn' (drop (l.length - i) l) b fun a' m b => f a' ⋯ b

Proof state:
m✝ : Type ?u.3753 → Type ?u.3709
α : Type ?u.3714
β : Type ?u.3753
inst✝ : Monad m✝
l : List α
f : (a : α) → a ∈ l.toArray → β → m✝ (ForInStep β)
i : Nat
h : i ≤ l.length
b✝ : β
a : α
m : a ∈ drop (l.length - i) l
b : β
⊢ a ∈ l.toArray

Tactic:
simpa using mem_of_mem_drop m

Result:
no goals