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

Proof state:
α : Type ?u.113878
as : Array α
i j : Nat
hj : j < as.size
k : Nat
h : k < (insertIdx.loop i as ⟨j, hj⟩).size
h₁ : ¬k < i
h₂ : ¬k = i
⊢ k < as.size

Tactic:
simpa using h

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
h₁ : ¬k < i
h₂ : ¬k = i
⊢ i < k

Tactic:
omega

Result:
no goals

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

Tactic:
rw [getElem_insertIdx_loop_gt (by omega)]

Result:
no goals

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

Tactic:
simp at h

Result:
α : Type ?u.113878
as : Array α
i j : Nat
hj : j < as.size
k : Nat
h₁ : ¬k < i
h₂ : ¬k = i
h : k < as.size
⊢ k - 1 < as.size

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
h₁ : ¬k < i
⊢ (insertIdx.loop i as ⟨j, hj⟩)[k] =
    if h₂ : k = i then if i ≤ j then as[j] else as[i] else if k ≤ j then as[k - 1] else as[k]

Tactic:
split <;> rename_i h₂

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

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

Proof state:
α : Type ?u.113878
as : Array α
i j : Nat
hj : j < as.size
k : Nat
h : k < (insertIdx.loop i as ⟨j, hj⟩).size
h₁ : k < i
⊢ k < as.size

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type ?u.113878
as : Array α
i j : Nat
hj : j < as.size
k : Nat
h : k < (insertIdx.loop i as ⟨j, hj⟩).size
h₁ : ¬k < i
h₂ : k = i
⊢ i < as.size

Tactic:
simpa [h₂] using h

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
h₁ : k < i
⊢ (insertIdx.loop i as ⟨j, hj⟩)[k] = as[k]

Tactic:
rw [getElem_insertIdx_loop_lt h₁]

Result:
no goals

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

Tactic:
subst h₂

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

Proof state:
α : Type ?u.113878
as : Array α
i j : Nat
hj : j < as.size
k : Nat
h₁ : ¬k < i
h₂ : ¬k = i
h : k < as.size
⊢ k - 1 < as.size

Tactic:
omega

Result:
no goals

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

Tactic:
rw [getElem_insertIdx_loop_eq]

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
⊢ (insertIdx.loop i as ⟨j, hj⟩)[k] =
    if h₁ : k < i then as[k]
    else if h₂ : k = i then if i ≤ j then as[j] else as[i] else if k ≤ j then as[k - 1] else as[k]

Tactic:
split <;> rename_i h₁

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
h₁ : k < i
⊢ (insertIdx.loop i as ⟨j, hj⟩)[k] = as[k]

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
h₁ : ¬k < i
⊢ (insertIdx.loop i as ⟨j, hj⟩)[k] =
    if h₂ : k = i then if i ≤ j then as[j] else as[i] else if k ≤ j then as[k - 1] else as[k]