-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_extract_loop_ge (as bs : Array α) (size start : Nat) (hge : i ≥ bs.size)
    (h : i < (extract.loop as size start bs).size)
    (h' := getElem_extract_loop_ge_aux as bs size start hge h) :
    (extract.loop as size start bs)[i] = as[start + i - bs.size]

Proof state:
α : Type u_1
i : Nat
as : Array α
size : Nat
ih :
  ∀ (bs : Array α) (start : Nat) (hge : i ≥ bs.size) (h : i < (extract.loop as size start bs).size)
    (h' : optParam (start + i - bs.size < as.size) ⋯), (extract.loop as size start bs)[i] = as[start + i - bs.size]
bs : Array α
start : Nat
hge : i ≥ bs.size
h : i < (extract.loop as (size + 1) start bs).size
h' : optParam (start + i - bs.size < as.size) ⋯
this✝ : start < as.size
this : i < (extract.loop as size (start + 1) (bs.push as[start])).size
heq : (extract.loop as (size + 1) start bs)[i] = (extract.loop as size (start + 1) (bs.push as[start]))[i]
hi : bs.size = i
⊢ (extract.loop as size (start + 1) (bs.push as[start]))[i] = as[start + i - bs.size]

Tactic:
cases hi

Result:
case refl
α : Type u_1
as : Array α
size : Nat
bs : Array α
start : Nat
this✝ : start < as.size
ih :
  ∀ (bs_1 : Array α) (start : Nat) (hge : bs.size ≥ bs_1.size) (h : bs.size < (extract.loop as size start bs_1).size)
    (h' : optParam (start + bs.size - bs_1.size < as.size) ⋯),
    (extract.loop as size start bs_1)[bs.size] = as[start + bs.size - bs_1.size]
hge : bs.size ≥ bs.size
h : bs.size < (extract.loop as (size + 1) start bs).size
h' : optParam (start + bs.size - bs.size < as.size) ⋯
this : bs.size < (extract.loop as size (start + 1) (bs.push as[start])).size
heq : (extract.loop as (size + 1) start bs)[bs.size] = (extract.loop as size (start + 1) (bs.push as[start]))[bs.size]
⊢ (extract.loop as size (start + 1) (bs.push as[start]))[bs.size] = as[start + bs.size - bs.size]

Proof state:
case refl
α : Type u_1
as : Array α
size : Nat
bs : Array α
start : Nat
this✝ : start < as.size
ih :
  ∀ (bs_1 : Array α) (start : Nat) (hge : bs.size ≥ bs_1.size) (h : bs.size < (extract.loop as size start bs_1).size)
    (h' : optParam (start + bs.size - bs_1.size < as.size) ⋯),
    (extract.loop as size start bs_1)[bs.size] = as[start + bs.size - bs_1.size]
hge : bs.size ≥ bs.size
h : bs.size < (extract.loop as (size + 1) start bs).size
h' : optParam (start + bs.size - bs.size < as.size) ⋯
this : bs.size < (extract.loop as size (start + 1) (bs.push as[start])).size
heq : (extract.loop as (size + 1) start bs)[bs.size] = (extract.loop as size (start + 1) (bs.push as[start]))[bs.size]
⊢ (extract.loop as size (start + 1) (bs.push as[start]))[bs.size] = as[start + bs.size - bs.size]

Tactic:
have h₁ : bs.size < (bs.push as[start]).size := by rw [size_push]; exact Nat.lt_succ_self ..

Result:
case refl
α : Type u_1
as : Array α
size : Nat
bs : Array α
start : Nat
this✝ : start < as.size
ih :
  ∀ (bs_1 : Array α) (start : Nat) (hge : bs.size ≥ bs_1.size) (h : bs.size < (extract.loop as size start bs_1).size)
    (h' : optParam (start + bs.size - bs_1.size < as.size) ⋯),
    (extract.loop as size start bs_1)[bs.size] = as[start + bs.size - bs_1.size]
hge : bs.size ≥ bs.size
h : bs.size < (extract.loop as (size + 1) start bs).size
h' : optParam (start + bs.size - bs.size < as.size) ⋯
this : bs.size < (extract.loop as size (start + 1) (bs.push as[start])).size
heq : (extract.loop as (size + 1) start bs)[bs.size] = (extract.loop as size (start + 1) (bs.push as[start]))[bs.size]
h₁ : bs.size < (bs.push as[start]).size
⊢ (extract.loop as size (start + 1) (bs.push as[start]))[bs.size] = as[start + bs.size - bs.size]

Proof state:
α : Type u_1
as : Array α
size : Nat
bs : Array α
start : Nat
this✝ : start < as.size
ih :
  ∀ (bs_1 : Array α) (start : Nat) (hge : bs.size ≥ bs_1.size) (h : bs.size < (extract.loop as size start bs_1).size)
    (h' : optParam (start + bs.size - bs_1.size < as.size) ⋯),
    (extract.loop as size start bs_1)[bs.size] = as[start + bs.size - bs_1.size]
hge : bs.size ≥ bs.size
h : bs.size < (extract.loop as (size + 1) start bs).size
h' : optParam (start + bs.size - bs.size < as.size) ⋯
this : bs.size < (extract.loop as size (start + 1) (bs.push as[start])).size
heq : (extract.loop as (size + 1) start bs)[bs.size] = (extract.loop as size (start + 1) (bs.push as[start]))[bs.size]
h₁ : bs.size < (bs.push as[start]).size
⊢ bs.size < (extract.loop as size (start + 1) (bs.push as[start])).size

Tactic:
rw [size_extract_loop]

Result:
α : Type u_1
as : Array α
size : Nat
bs : Array α
start : Nat
this✝ : start < as.size
ih :
  ∀ (bs_1 : Array α) (start : Nat) (hge : bs.size ≥ bs_1.size) (h : bs.size < (extract.loop as size start bs_1).size)
    (h' : optParam (start + bs.size - bs_1.size < as.size) ⋯),
    (extract.loop as size start bs_1)[bs.size] = as[start + bs.size - bs_1.size]
hge : bs.size ≥ bs.size
h : bs.size < (extract.loop as (size + 1) start bs).size
h' : optParam (start + bs.size - bs.size < as.size) ⋯
this : bs.size < (extract.loop as size (start + 1) (bs.push as[start])).size
heq : (extract.loop as (size + 1) start bs)[bs.size] = (extract.loop as size (start + 1) (bs.push as[start]))[bs.size]
h₁ : bs.size < (bs.push as[start]).size
⊢ bs.size < (bs.push as[start]).size + min size (as.size - (start + 1))

Proof state:
α : Type u_1
i : Nat
as : Array α
size : Nat
ih :
  ∀ (bs : Array α) (start : Nat) (hge : i ≥ bs.size) (h : i < (extract.loop as size start bs).size)
    (h' : optParam (start + i - bs.size < as.size) ⋯), (extract.loop as size start bs)[i] = as[start + i - bs.size]
bs : Array α
start : Nat
hge✝ : i ≥ bs.size
h : i < (extract.loop as (size + 1) start bs).size
h' : optParam (start + i - bs.size < as.size) ⋯
this✝ : start < as.size
this : i < (extract.loop as size (start + 1) (bs.push as[start])).size
heq : (extract.loop as (size + 1) start bs)[i] = (extract.loop as size (start + 1) (bs.push as[start]))[i]
hi : ¬bs.size = i
hge : bs.size + 1 ≤ i
⊢ (extract.loop as size (start + 1) (bs.push as[start]))[i] = as[start + i - bs.size]

Tactic:
rw [ih (bs.push as[start]) (start+1) ((size_push ..).symm ▸ hge)]

Result:
α : Type u_1
i : Nat
as : Array α
size : Nat
ih :
  ∀ (bs : Array α) (start : Nat) (hge : i ≥ bs.size) (h : i < (extract.loop as size start bs).size)
    (h' : optParam (start + i - bs.size < as.size) ⋯), (extract.loop as size start bs)[i] = as[start + i - bs.size]
bs : Array α
start : Nat
hge✝ : i ≥ bs.size
h : i < (extract.loop as (size + 1) start bs).size
h' : optParam (start + i - bs.size < as.size) ⋯
this✝ : start < as.size
this : i < (extract.loop as size (start + 1) (bs.push as[start])).size
heq : (extract.loop as (size + 1) start bs)[i] = (extract.loop as size (start + 1) (bs.push as[start]))[i]
hi : ¬bs.size = i
hge : bs.size + 1 ≤ i
⊢ as[start + 1 + i - (bs.push as[start]).size] = as[start + i - bs.size]

Proof state:
α : Type u_1
as : Array α
size : Nat
bs : Array α
start : Nat
this✝ : start < as.size
ih :
  ∀ (bs_1 : Array α) (start : Nat) (hge : bs.size ≥ bs_1.size) (h : bs.size < (extract.loop as size start bs_1).size)
    (h' : optParam (start + bs.size - bs_1.size < as.size) ⋯),
    (extract.loop as size start bs_1)[bs.size] = as[start + bs.size - bs_1.size]
hge : bs.size ≥ bs.size
h : bs.size < (extract.loop as (size + 1) start bs).size
h' : optParam (start + bs.size - bs.size < as.size) ⋯
this : bs.size < (extract.loop as size (start + 1) (bs.push as[start])).size
heq : (extract.loop as (size + 1) start bs)[bs.size] = (extract.loop as size (start + 1) (bs.push as[start]))[bs.size]
h₁ : bs.size < (bs.push as[start]).size
⊢ (bs.push as[start]).size ≤ (bs.push as[start]).size + min size (as.size - (start + 1))

Tactic:
exact Nat.le_add_right ..

Result:
no goals