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

Proof state:
α : Type u_1
as : Array α
i j : Nat
hj : j < as.size
h : i < (insertIdx.loop i as ⟨j, hj⟩).size
h₁✝ : ¬i < ↑⟨j, hj⟩
h₁ : j ≤ i
h' : ¬i = j
⊢ ¬i ≤ j

Tactic:
omega

Result:
no goals

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

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

Result:
case neg
α : Type u_1
as : Array α
i j : Nat
hj : j < as.size
h : i < (insertIdx.loop i as ⟨j, hj⟩).size
h₁✝ : ¬i < ↑⟨j, hj⟩
h₁ : j ≤ i
h' : ¬i = j
t : ¬i ≤ j
⊢ as[i] = if i ≤ j then as[j] else as[i]

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

Tactic:
unfold insertIdx.loop

Result:
α : Type u_1
as : Array α
i j : Nat
hj : j < as.size
h : i < (insertIdx.loop i as ⟨j, hj⟩).size
⊢ (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)[i] =
    if i ≤ j then as[j] else as[i]

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

Tactic:
rw [getElem_insertIdx_loop_eq]

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

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

Tactic:
rw [getElem_swap]

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

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

Tactic:
omega

Result:
no goals

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

Tactic:
simp at h₁

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

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

Tactic:
omega

Result:
no goals

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

Tactic:
simpa using h

Result:
no goals

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

Tactic:
split <;> rename_i h₂

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

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

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

Tactic:
simp

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

Proof state:
case neg
α : Type u_1
as : Array α
i j : Nat
hj : j < as.size
h : i < (insertIdx.loop i as ⟨j, hj⟩).size
h₁✝ : ¬i < ↑⟨j, hj⟩
h₁ : j ≤ i
h' : ¬i = j
t : ¬i ≤ j
⊢ as[i] = if i ≤ j then as[j] else as[i]

Tactic:
simp [t]

Result:
no goals

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

Tactic:
rw [if_pos (by omega)]

Result:
no goals

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

Tactic:
have : j - 1 < j := by omega

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

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

Tactic:
omega

Result:
no goals

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

Tactic:
simp [h']

Result:
no goals

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

Tactic:
simp at h₁

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