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

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

Tactic:
rw [extract_loop_succ (h:=h), ih, size_push, Nat.add_assoc, ←Nat.add_min_add_left,
  Nat.sub_succ, Nat.one_add, Nat.one_add, Nat.succ_pred_eq_of_pos (Nat.sub_pos_of_lt h)]

Result:
no goals

Proof state:
α : Type u_1
as : Array α
size : Nat
ih : ∀ (bs : Array α) (start : Nat), (extract.loop as size start bs).size = bs.size + min size (as.size - start)
bs : Array α
start : Nat
h✝ : ¬start < as.size
h : as.size ≤ start
⊢ (extract.loop as (size + 1) start bs).size = bs.size + min (size + 1) (as.size - start)

Tactic:
rw [extract_loop_of_ge (h:=h), Nat.sub_eq_zero_of_le h, Nat.min_zero, Nat.add_zero]

Result:
no goals

Proof state:
α : Type u_1
as bs : Array α
size start : Nat
⊢ (extract.loop as size start bs).size = bs.size + min size (as.size - start)

Tactic:
induction size using Nat.recAux generalizing start bs with
| zero => rw [extract_loop_zero, Nat.zero_min, Nat.add_zero]
| succ size ih =>
  if h : start < as.size then
    rw [extract_loop_succ (h:=h), ih, size_push, Nat.add_assoc, ←Nat.add_min_add_left,
      Nat.sub_succ, Nat.one_add, Nat.one_add, Nat.succ_pred_eq_of_pos (Nat.sub_pos_of_lt h)]
  else
    have h := Nat.le_of_not_gt h
    rw [extract_loop_of_ge (h:=h), Nat.sub_eq_zero_of_le h, Nat.min_zero, Nat.add_zero]

Result:
no goals

Proof state:
case zero
α : Type u_1
as bs : Array α
start : Nat
⊢ (extract.loop as 0 start bs).size = bs.size + min 0 (as.size - start)

Tactic:
rw [extract_loop_zero, Nat.zero_min, Nat.add_zero]

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).size = bs.size + min size (as.size - start)
bs : Array α
start : Nat
⊢ (extract.loop as (size + 1) start bs).size = bs.size + min (size + 1) (as.size - start)

Tactic:
if h : start < as.size then
  rw [extract_loop_succ (h:=h), ih, size_push, Nat.add_assoc, ←Nat.add_min_add_left,
    Nat.sub_succ, Nat.one_add, Nat.one_add, Nat.succ_pred_eq_of_pos (Nat.sub_pos_of_lt h)]
else
  have h := Nat.le_of_not_gt h
  rw [extract_loop_of_ge (h:=h), Nat.sub_eq_zero_of_le h, Nat.min_zero, Nat.add_zero]

Result:
no goals

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

Tactic:
have h := Nat.le_of_not_gt h

Result:
α : Type u_1
as : Array α
size : Nat
ih : ∀ (bs : Array α) (start : Nat), (extract.loop as size start bs).size = bs.size + min size (as.size - start)
bs : Array α
start : Nat
h✝ : ¬start < as.size
h : as.size ≤ start
⊢ (extract.loop as (size + 1) start bs).size = bs.size + min (size + 1) (as.size - start)