-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Lemmas.lean
theorem getElem_insertIdx_loop_lt {as : Array α} {i : Nat} {j : Fin as.size} {k : Nat} {h}
    (w : k < i) :
    (insertIdx.loop i as j)[k] = as[k]'(by simpa using h)

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

Tactic:
split <;> rename_i h₃

Result:
case isTrue.isFalse.isTrue
α : Type u_1
as : Array α
i : Nat
j : Fin as.size
k : Nat
h : k < (insertIdx.loop i as j).size
w : k < i
h₁ : i < ↑j
h₂ : ¬k = ↑j - 1
h₃ : k = ↑j
⊢ as[↑j - 1] = as[k]

case isTrue.isFalse.isFalse
α : Type u_1
as : Array α
i : Nat
j : Fin as.size
k : Nat
h : k < (insertIdx.loop i as j).size
w : k < i
h₁ : i < ↑j
h₂ : ¬k = ↑j - 1
h₃ : ¬k = ↑j
⊢ as[k] = as[k]

Proof state:
α : Type ?u.22856
as : Array α
i : Nat
j : Fin as.size
k : Nat
h : k < (insertIdx.loop i as j).size
w : k < i
⊢ k < as.size

Tactic:
simpa using h

Result:
no goals

Proof state:
case isTrue.isFalse.isTrue
α : Type u_1
as : Array α
i : Nat
j : Fin as.size
k : Nat
h : k < (insertIdx.loop i as j).size
w : k < i
h₁ : i < ↑j
h₂ : ¬k = ↑j - 1
h₃ : k = ↑j
⊢ as[↑j - 1] = as[k]

Tactic:
omega

Result:
no goals

Proof state:
case isTrue
α : Type u_1
as : Array α
i : Nat
j : Fin as.size
k : Nat
h : k < (insertIdx.loop i as j).size
w : k < i
h₁ : i < ↑j
⊢ (if k = ↑j - 1 then as[↑j] else if k = ↑j then as[↑j - 1] else as[k]) = as[k]

Tactic:
split <;> rename_i h₂

Result:
case isTrue.isTrue
α : Type u_1
as : Array α
i : Nat
j : Fin as.size
k : Nat
h : k < (insertIdx.loop i as j).size
w : k < i
h₁ : i < ↑j
h₂ : k = ↑j - 1
⊢ as[↑j] = as[k]

case isTrue.isFalse
α : Type u_1
as : Array α
i : Nat
j : Fin as.size
k : Nat
h : k < (insertIdx.loop i as j).size
w : k < i
h₁ : i < ↑j
h₂ : ¬k = ↑j - 1
⊢ (if k = ↑j then as[↑j - 1] else as[k]) = as[k]

Proof state:
case isTrue
α : Type u_1
as : Array α
i : Nat
j : Fin as.size
k : Nat
h : k < (insertIdx.loop i as j).size
w : k < i
h₁ : i < ↑j
⊢ (as.swap (↑j - 1) ↑j ⋯ ⋯)[k] = as[k]

Tactic:
rw [getElem_swap]

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

Proof state:
α : Type u_1
as : Array α
i : Nat
j : Fin as.size
k : Nat
h : k < (insertIdx.loop i as j).size
w : k < i
⊢ (insertIdx.loop i as j)[k] = as[k]

Tactic:
unfold insertIdx.loop

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

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

Tactic:
simp only

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

Proof state:
case isTrue.isTrue
α : Type u_1
as : Array α
i : Nat
j : Fin as.size
k : Nat
h : k < (insertIdx.loop i as j).size
h₂✝ : k = ↑j - 1
w : ↑j - 1 < i
h₁ : i < ↑j
h₂ : k = ↑j - 1
⊢ as[↑j] = as[↑j - 1]

Tactic:
omega

Result:
no goals

Proof state:
case isFalse
α : Type u_1
as : Array α
i : Nat
j : Fin as.size
k : Nat
h : k < (insertIdx.loop i as j).size
w : k < i
h₁ : ¬i < ↑j
⊢ as[k] = as[k]

Tactic:
rfl

Result:
no goals

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

Tactic:
rw [getElem_insertIdx_loop_lt w]

Result:
case isTrue
α : Type u_1
as : Array α
i : Nat
j : Fin as.size
k : Nat
h : k < (insertIdx.loop i as j).size
w : k < i
h₁ : i < ↑j
⊢ (as.swap (↑j - 1) ↑j ⋯ ⋯)[k] = as[k]

Proof state:
case isTrue.isFalse.isFalse
α : Type u_1
as : Array α
i : Nat
j : Fin as.size
k : Nat
h : k < (insertIdx.loop i as j).size
w : k < i
h₁ : i < ↑j
h₂ : ¬k = ↑j - 1
h₃ : ¬k = ↑j
⊢ as[k] = as[k]

Tactic:
simp_all

Result:
no goals

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

Tactic:
split <;> rename_i h₁

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

case isFalse
α : Type u_1
as : Array α
i : Nat
j : Fin as.size
k : Nat
h : k < (insertIdx.loop i as j).size
w : k < i
h₁ : ¬i < ↑j
⊢ as[k] = as[k]

Proof state:
case isTrue.isTrue
α : Type u_1
as : Array α
i : Nat
j : Fin as.size
k : Nat
h : k < (insertIdx.loop i as j).size
w : k < i
h₁ : i < ↑j
h₂ : k = ↑j - 1
⊢ as[↑j] = as[k]

Tactic:
simp_all

Result:
case isTrue.isTrue
α : Type u_1
as : Array α
i : Nat
j : Fin as.size
k : Nat
h : k < (insertIdx.loop i as j).size
h₂✝ : k = ↑j - 1
w : ↑j - 1 < i
h₁ : i < ↑j
h₂ : k = ↑j - 1
⊢ as[↑j] = as[↑j - 1]