-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Lemmas.lean
theorem getElem_insertIdx_loop_gt {as : Array α} {i : Nat} {j : Nat} {hj : j < as.size}
    {k : Nat} {h} (w : i < k) :
    (insertIdx.loop i as ⟨j, hj⟩)[k] =
      if k ≤ j then as[k-1]'(by simp at h; omega) else as[k]'(by simpa using h)

Proof state:
case isFalse
α : Type u_1
as : Array α
i j : Nat
hj : j < as.size
k : Nat
h : k < (insertIdx.loop i as ⟨j, hj⟩).size
w : i < k
h₁ : ¬i < j
⊢ as[k] = if k ≤ j then as[k - 1] else as[k]

Tactic:
have t : ¬ k ≤ j := by omega

Result:
case isFalse
α : Type u_1
as : Array α
i j : Nat
hj : j < as.size
k : Nat
h : k < (insertIdx.loop i as ⟨j, hj⟩).size
w : i < k
h₁ : ¬i < j
t : ¬k ≤ j
⊢ as[k] = if k ≤ j then as[k - 1] else as[k]

Proof state:
case isTrue
α : Type u_1
as : Array α
i j : Nat
hj : j < as.size
k : Nat
h : k < (insertIdx.loop i as ⟨j, hj⟩).size
w : i < k
h₁ : i < j
this : j - 1 < j
⊢ (if k ≤ j - 1 then (as.swap (j - 1) j ⋯ ⋯)[k - 1] else (as.swap (j - 1) j ⋯ ⋯)[k]) =
    if k ≤ j then as[k - 1] else as[k]

Tactic:
rw [getElem_swap]

Result:
case isTrue
α : Type u_1
as : Array α
i j : Nat
hj : j < as.size
k : Nat
h : k < (insertIdx.loop i as ⟨j, hj⟩).size
w : i < k
h₁ : i < j
this : j - 1 < j
⊢ (if k ≤ j - 1 then if k - 1 = j - 1 then as[j] else if k - 1 = j then as[j - 1] else as[k - 1]
    else (as.swap (j - 1) j ⋯ ⋯)[k]) =
    if k ≤ j then as[k - 1] else as[k]

Proof state:
case isTrue.isTrue
α : Type u_1
as : Array α
i j : Nat
hj : j < as.size
k : Nat
h : k < (insertIdx.loop i as ⟨j, hj⟩).size
w : i < k
h₁ : i < j
this : j - 1 < j
h₂ : k ≤ j - 1
t : k ≤ j
⊢ as[k - 1] = if k ≤ j then as[k - 1] else as[k]

Tactic:
simp [t]

Result:
no goals

Proof state:
case isTrue
α : Type u_1
as : Array α
i j : Nat
hj : j < as.size
k : Nat
h : k < (insertIdx.loop i as ⟨j, hj⟩).size
w : i < k
h₁ : i < ↑⟨j, hj⟩
⊢ (let j' := ⟨↑⟨j, hj⟩ - 1, ⋯⟩;
      let as_1 := as.swap ↑j' ↑⟨j, hj⟩ ⋯ ⋯;
      insertIdx.loop i as_1 ⟨↑j', ⋯⟩)[k] =
    if k ≤ j then as[k - 1] else as[k]

Tactic:
simp only

Result:
case isTrue
α : Type u_1
as : Array α
i j : Nat
hj : j < as.size
k : Nat
h : k < (insertIdx.loop i as ⟨j, hj⟩).size
w : i < k
h₁ : i < ↑⟨j, hj⟩
⊢ (insertIdx.loop i (as.swap (j - 1) j ⋯ ⋯) ⟨j - 1, ⋯⟩)[k] = if k ≤ j then as[k - 1] else as[k]

Proof state:
α : Type u_1
as : Array α
i j : Nat
hj : j < as.size
k : Nat
h : k < (insertIdx.loop i as ⟨j, hj⟩).size
w : i < k
h₁ : i < j
this : j - 1 < j
h₂ : ¬k ≤ j - 1
⊢ ¬k = j - 1

Tactic:
omega

Result:
no goals

Proof state:
case isTrue.isFalse
α : Type u_1
as : Array α
i j : Nat
hj : j < as.size
k : Nat
h : k < (insertIdx.loop i as ⟨j, hj⟩).size
w : i < k
h₁ : i < j
this : j - 1 < j
h₂ : ¬k ≤ j - 1
⊢ (as.swap (j - 1) j ⋯ ⋯)[k] = if k ≤ j then as[k - 1] else as[k]

Tactic:
rw [getElem_swap]

Result:
case isTrue.isFalse
α : Type u_1
as : Array α
i j : Nat
hj : j < as.size
k : Nat
h : k < (insertIdx.loop i as ⟨j, hj⟩).size
w : i < k
h₁ : i < j
this : j - 1 < j
h₂ : ¬k ≤ j - 1
⊢ (if k = j - 1 then as[j] else if k = j then as[j - 1] else as[k]) = if k ≤ j then as[k - 1] else as[k]

Proof state:
case isFalse
α : Type u_1
as : Array α
i j : Nat
hj : j < as.size
k : Nat
h : k < (insertIdx.loop i as ⟨j, hj⟩).size
w : i < k
h₁ : ¬i < ↑⟨j, hj⟩
⊢ as[k] = if k ≤ j then as[k - 1] else as[k]

Tactic:
simp only at h₁

Result:
case isFalse
α : Type u_1
as : Array α
i j : Nat
hj : j < as.size
k : Nat
h : k < (insertIdx.loop i as ⟨j, hj⟩).size
w : i < k
h₁ : ¬i < j
⊢ as[k] = if k ≤ j then as[k - 1] else as[k]

Proof state:
case isFalse
α : Type u_1
as : Array α
i j : Nat
hj : j < as.size
k : Nat
h : k < (insertIdx.loop i as ⟨j, hj⟩).size
w : i < k
h₁ : ¬i < j
t : ¬k ≤ j
⊢ as[k] = if k ≤ j then as[k - 1] else as[k]

Tactic:
simp [t]

Result:
no goals

Proof state:
α : Type u_1
as : Array α
i j : Nat
hj : j < as.size
k : Nat
h : k < (insertIdx.loop i as ⟨j, hj⟩).size
w : i < k
h₁ : i < j
this : j - 1 < j
h₂ : k ≤ j - 1
⊢ k ≤ j

Tactic:
omega

Result:
no goals

Proof state:
case isTrue.isFalse
α : Type u_1
as : Array α
i j : Nat
hj : j < as.size
k : Nat
h : k < (insertIdx.loop i as ⟨j, hj⟩).size
w : i < k
h₁ : i < j
this : j - 1 < j
h₂ : ¬k ≤ j - 1
⊢ (if k = j - 1 then as[j] else if k = j then as[j - 1] else as[k]) = if k ≤ j then as[k - 1] else as[k]

Tactic:
rw [if_neg (by omega)]

Result:
case isTrue.isFalse
α : Type u_1
as : Array α
i j : Nat
hj : j < as.size
k : Nat
h : k < (insertIdx.loop i as ⟨j, hj⟩).size
w : i < k
h₁ : i < j
this : j - 1 < j
h₂ : ¬k ≤ j - 1
⊢ (if k = j then as[j - 1] else as[k]) = if k ≤ j then as[k - 1] else as[k]

Proof state:
case isTrue
α : Type u_1
as : Array α
i j : Nat
hj : j < as.size
k : Nat
h : k < (insertIdx.loop i as ⟨j, hj⟩).size
w : i < k
h₁ : i < j
this : j - 1 < j
⊢ (if k ≤ j - 1 then if k - 1 = j - 1 then as[j] else if k - 1 = j then as[j - 1] else as[k - 1]
    else (as.swap (j - 1) j ⋯ ⋯)[k]) =
    if k ≤ j then as[k - 1] else as[k]

Tactic:
split <;> rename_i h₂

Result:
case isTrue.isTrue
α : Type u_1
as : Array α
i j : Nat
hj : j < as.size
k : Nat
h : k < (insertIdx.loop i as ⟨j, hj⟩).size
w : i < k
h₁ : i < j
this : j - 1 < j
h₂ : k ≤ j - 1
⊢ (if k - 1 = j - 1 then as[j] else if k - 1 = j then as[j - 1] else as[k - 1]) = if k ≤ j then as[k - 1] else as[k]

case isTrue.isFalse
α : Type u_1
as : Array α
i j : Nat
hj : j < as.size
k : Nat
h : k < (insertIdx.loop i as ⟨j, hj⟩).size
w : i < k
h₁ : i < j
this : j - 1 < j
h₂ : ¬k ≤ j - 1
⊢ (as.swap (j - 1) j ⋯ ⋯)[k] = if k ≤ j then as[k - 1] else as[k]

Proof state:
α : Type u_1
as : Array α
i j : Nat
hj : j < as.size
k : Nat
h : k < (insertIdx.loop i as ⟨j, hj⟩).size
w : i < k
⊢ (insertIdx.loop i as ⟨j, hj⟩)[k] = if k ≤ j then as[k - 1] else as[k]

Tactic:
unfold insertIdx.loop

Result:
α : Type u_1
as : Array α
i j : Nat
hj : j < as.size
k : Nat
h : k < (insertIdx.loop i as ⟨j, hj⟩).size
w : i < k
⊢ (if i < ↑⟨j, hj⟩ then
        let j' := ⟨↑⟨j, hj⟩ - 1, ⋯⟩;
        let as_1 := as.swap ↑j' ↑⟨j, hj⟩ ⋯ ⋯;
        insertIdx.loop i as_1 ⟨↑j', ⋯⟩
      else as)[k] =
    if k ≤ j then as[k - 1] else as[k]