-- 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 : β
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

Tactic:
congr

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
⊢ (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

Tactic:
simp [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
⊢ (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:
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 : β
⊢ 0 < l.length - i

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 : β
⊢ l.length - i - 1 < l.length

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 : β
⊢ (some l[l.length - i - 1]).toList ++ drop (l.length - i) l = l[l.length - i - 1] :: drop (l.length - i) l

Tactic:
simp only [Option.toList_some, singleton_append]

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:
rw [List.drop_sub_one (by omega), List.getElem?_eq_getElem (by omega)]

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 : β
⊢ (some l[l.length - i - 1]).toList ++ drop (l.length - i) 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 : β
⊢ (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

Tactic:
have t : drop (l.length - (i + 1)) l = l[l.length - i - 1] :: drop (l.length - i) l := by
  simp only [Nat.sub_add_eq]
  rw [List.drop_sub_one (by omega), List.getElem?_eq_getElem (by omega)]
  simp only [Option.toList_some, singleton_append]

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
⊢ (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
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' (drop (l.length - i) l) b fun a m b => f a ⋯ b

Tactic:
induction i generalizing l b with
| zero =>
  simp [Array.forIn'.loop]
| succ i ih =>
  simp only [Array.forIn'.loop, size_toArray, getElem_toArray, ih]
  have t : drop (l.length - (i + 1)) l = l[l.length - i - 1] :: drop (l.length - i) l := by
    simp only [Nat.sub_add_eq]
    rw [List.drop_sub_one (by omega), List.getElem?_eq_getElem (by omega)]
    simp only [Option.toList_some, singleton_append]
  simp [t]
  have t : l.length - 1 - i = l.length - i - 1 := by omega
  simp only [t]
  congr

Result:
no goals