-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem extract_loop_eq_aux (as bs : Array α) (size start : Nat) :
    extract.loop as size start bs = bs ++ extract.loop as size start #[]

Proof state:
α : Type u_1
as : Array α
size : Nat
ih : ∀ (bs : Array α) (start : Nat), extract.loop as size start bs = bs ++ extract.loop as size start #[]
bs : Array α
start : Nat
h : start < as.size
⊢ extract.loop as (size + 1) start bs = bs ++ extract.loop as (size + 1) start #[]

Tactic:
rw [extract_loop_succ (h:=h), ih (bs.push _), push_eq_append_singleton]

Result:
α : Type u_1
as : Array α
size : Nat
ih : ∀ (bs : Array α) (start : Nat), extract.loop as size start bs = bs ++ extract.loop as size start #[]
bs : Array α
start : Nat
h : start < as.size
⊢ bs ++ #[as[start]] ++ extract.loop as size (start + 1) #[] = bs ++ extract.loop as (size + 1) start #[]

Proof state:
α : Type u_1
as : Array α
size : Nat
ih : ∀ (bs : Array α) (start : Nat), extract.loop as size start bs = bs ++ extract.loop as size start #[]
bs : Array α
start : Nat
h : start < as.size
⊢ bs ++ #[as[start]] ++ extract.loop as size (start + 1) #[] = bs ++ extract.loop as (size + 1) start #[]

Tactic:
rw [extract_loop_succ (h:=h), ih (#[].push _), push_eq_append_singleton, empty_append]

Result:
α : Type u_1
as : Array α
size : Nat
ih : ∀ (bs : Array α) (start : Nat), extract.loop as size start bs = bs ++ extract.loop as size start #[]
bs : Array α
start : Nat
h : start < as.size
⊢ bs ++ #[as[start]] ++ extract.loop as size (start + 1) #[] =
    bs ++ (#[as[start]] ++ extract.loop as size (start + 1) #[])

Proof state:
α : Type u_1
as : Array α
size : Nat
ih : ∀ (bs : Array α) (start : Nat), extract.loop as size start bs = bs ++ extract.loop as size start #[]
bs : Array α
start : Nat
h : ¬start < as.size
⊢ bs = bs ++ #[]

Tactic:
rw [append_empty]

Result:
no goals

Proof state:
α : Type u_1
as : Array α
size : Nat
ih : ∀ (bs : Array α) (start : Nat), extract.loop as size start bs = bs ++ extract.loop as size start #[]
bs : Array α
start : Nat
h : start < as.size
⊢ bs ++ #[as[start]] ++ extract.loop as size (start + 1) #[] =
    bs ++ (#[as[start]] ++ extract.loop as size (start + 1) #[])

Tactic:
rw [append_assoc]

Result:
no goals

Proof state:
α : Type u_1
as : Array α
size : Nat
ih : ∀ (bs : Array α) (start : Nat), extract.loop as size start bs = bs ++ extract.loop as size start #[]
bs : Array α
start : Nat
h : ¬start < as.size
⊢ extract.loop as (size + 1) start bs = bs ++ extract.loop as (size + 1) start #[]

Tactic:
rw [extract_loop_of_ge (h:=Nat.le_of_not_lt h)]

Result:
α : Type u_1
as : Array α
size : Nat
ih : ∀ (bs : Array α) (start : Nat), extract.loop as size start bs = bs ++ extract.loop as size start #[]
bs : Array α
start : Nat
h : ¬start < as.size
⊢ bs = bs ++ extract.loop as (size + 1) start #[]

Proof state:
case zero
α : Type u_1
as bs : Array α
start : Nat
⊢ extract.loop as 0 start bs = bs ++ extract.loop as 0 start #[]

Tactic:
rw [extract_loop_zero, extract_loop_zero, append_empty]

Result:
no goals

Proof state:
case succ
α : Type u_1
as : Array α
size : Nat
ih : ∀ (bs : Array α) (start : Nat), extract.loop as size start bs = bs ++ extract.loop as size start #[]
bs : Array α
start : Nat
⊢ extract.loop as (size + 1) start bs = bs ++ extract.loop as (size + 1) start #[]

Tactic:
if h : start < as.size then
  rw [extract_loop_succ (h:=h), ih (bs.push _), push_eq_append_singleton]
  rw [extract_loop_succ (h:=h), ih (#[].push _), push_eq_append_singleton, empty_append]
  rw [append_assoc]
else
  rw [extract_loop_of_ge (h:=Nat.le_of_not_lt h)]
  rw [extract_loop_of_ge (h:=Nat.le_of_not_lt h)]
  rw [append_empty]

Result:
no goals

Proof state:
α : Type u_1
as : Array α
size : Nat
ih : ∀ (bs : Array α) (start : Nat), extract.loop as size start bs = bs ++ extract.loop as size start #[]
bs : Array α
start : Nat
h : ¬start < as.size
⊢ bs = bs ++ extract.loop as (size + 1) start #[]

Tactic:
rw [extract_loop_of_ge (h:=Nat.le_of_not_lt h)]

Result:
α : Type u_1
as : Array α
size : Nat
ih : ∀ (bs : Array α) (start : Nat), extract.loop as size start bs = bs ++ extract.loop as size start #[]
bs : Array α
start : Nat
h : ¬start < as.size
⊢ bs = bs ++ #[]

Proof state:
α : Type u_1
as bs : Array α
size start : Nat
⊢ extract.loop as size start bs = bs ++ extract.loop as size start #[]

Tactic:
induction size using Nat.recAux generalizing start bs with
| zero => rw [extract_loop_zero, extract_loop_zero, append_empty]
| succ size ih =>
  if h : start < as.size then
    rw [extract_loop_succ (h:=h), ih (bs.push _), push_eq_append_singleton]
    rw [extract_loop_succ (h:=h), ih (#[].push _), push_eq_append_singleton, empty_append]
    rw [append_assoc]
  else
    rw [extract_loop_of_ge (h:=Nat.le_of_not_lt h)]
    rw [extract_loop_of_ge (h:=Nat.le_of_not_lt h)]
    rw [append_empty]

Result:
no goals