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

Proof state:
case h
α : Type u_1
i : Nat
as bs : Array α
size start : Nat
hge : i ≥ bs.size
h : i < (extract.loop as size start bs).size
⊢ min size (as.size - start) ≤ as.size - start

Tactic:
exact Nat.min_le_right ..

Result:
no goals

Proof state:
α : Type u_1
i : Nat
as bs : Array α
size start : Nat
hge : i ≥ bs.size
h : i < (extract.loop as size start bs).size
⊢ (extract.loop as size start bs).size ≤ bs.size + (as.size - start)

Tactic:
rw [size_extract_loop]

Result:
α : Type u_1
i : Nat
as bs : Array α
size start : Nat
hge : i ≥ bs.size
h : i < (extract.loop as size start bs).size
⊢ bs.size + min size (as.size - start) ≤ bs.size + (as.size - start)

Proof state:
α : Type u_1
i : Nat
as bs : Array α
size start : Nat
hge : i ≥ bs.size
h : i < (extract.loop as size start bs).size
⊢ start + i - bs.size < as.size

Tactic:
have h : i < bs.size + (as.size - start) := by
    apply Nat.lt_of_lt_of_le h
    rw [size_extract_loop]
    apply Nat.add_le_add_left
    exact Nat.min_le_right ..

Result:
α : Type u_1
i : Nat
as bs : Array α
size start : Nat
hge : i ≥ bs.size
h✝ : i < (extract.loop as size start bs).size
h : i < bs.size + (as.size - start)
⊢ start + i - bs.size < as.size

Proof state:
α : Type u_1
i : Nat
as bs : Array α
size start : Nat
hge : i ≥ bs.size
h : i < (extract.loop as size start bs).size
⊢ bs.size + min size (as.size - start) ≤ bs.size + (as.size - start)

Tactic:
apply Nat.add_le_add_left

Result:
case h
α : Type u_1
i : Nat
as bs : Array α
size start : Nat
hge : i ≥ bs.size
h : i < (extract.loop as size start bs).size
⊢ min size (as.size - start) ≤ as.size - start

Proof state:
case a
α : Type u_1
i : Nat
as bs : Array α
size start : Nat
hge : i ≥ bs.size
h✝ : i < (extract.loop as size start bs).size
h : i < bs.size + (as.size - start)
⊢ i - bs.size < as.size - start

Tactic:
exact Nat.sub_lt_left_of_lt_add hge h

Result:
no goals

Proof state:
α : Type u_1
i : Nat
as bs : Array α
size start : Nat
hge : i ≥ bs.size
h : i < (extract.loop as size start bs).size
⊢ i < bs.size + (as.size - start)

Tactic:
apply Nat.lt_of_lt_of_le h

Result:
α : Type u_1
i : Nat
as bs : Array α
size start : Nat
hge : i ≥ bs.size
h : i < (extract.loop as size start bs).size
⊢ (extract.loop as size start bs).size ≤ bs.size + (as.size - start)

Proof state:
α : Type u_1
i : Nat
as bs : Array α
size start : Nat
hge : i ≥ bs.size
h✝ : i < (extract.loop as size start bs).size
h : i < bs.size + (as.size - start)
⊢ start + (i - bs.size) < as.size

Tactic:
apply Nat.add_lt_of_lt_sub'

Result:
case a
α : Type u_1
i : Nat
as bs : Array α
size start : Nat
hge : i ≥ bs.size
h✝ : i < (extract.loop as size start bs).size
h : i < bs.size + (as.size - start)
⊢ i - bs.size < as.size - start

Proof state:
α : Type u_1
i : Nat
as bs : Array α
size start : Nat
hge : i ≥ bs.size
h✝ : i < (extract.loop as size start bs).size
h : i < bs.size + (as.size - start)
⊢ start + i - bs.size < as.size

Tactic:
rw [Nat.add_sub_assoc hge]

Result:
α : Type u_1
i : Nat
as bs : Array α
size start : Nat
hge : i ≥ bs.size
h✝ : i < (extract.loop as size start bs).size
h : i < bs.size + (as.size - start)
⊢ start + (i - bs.size) < as.size