-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Lemmas.lean
theorem getElem_insertIdx (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α)
    (k) (h' : k < (as.insertIdx i v).size) :
    (as.insertIdx i v)[k] =
      if h₁ : k < i then
        as[k]'(by omega)
      else
        if h₂ : k = i then
          v
        else
          as[k - 1]'(by simp at h'; omega)

Proof state:
α : Type u_1
as : Array α
i : Nat
h : i ≤ as.size
v : α
k : Nat
h' : k < (as.insertIdx i v h).size
⊢ (if h₁ : k < i then (as.push v)[k]
    else
      if h₂ : k = i then if i ≤ as.size then (as.push v)[as.size] else (as.push v)[i]
      else if k ≤ as.size then (as.push v)[k - 1] else (as.push v)[k]) =
    if h₁ : k < i then as[k] else if h₂ : k = i then v else as[k - 1]

Tactic:
simp only [size_insertIdx] at h'

Result:
α : Type u_1
as : Array α
i : Nat
h : i ≤ as.size
v : α
k : Nat
h'✝ : k < (as.insertIdx i v h).size
h' : k < as.size + 1
⊢ (if h₁ : k < i then (as.push v)[k]
    else
      if h₂ : k = i then if i ≤ as.size then (as.push v)[as.size] else (as.push v)[i]
      else if k ≤ as.size then (as.push v)[k - 1] else (as.push v)[k]) =
    if h₁ : k < i then as[k] else if h₂ : k = i then v else as[k - 1]

Proof state:
α : Type ?u.120154
as : Array α
i : Nat
h : i ≤ as.size
v : α
k : Nat
h' : k < (as.insertIdx i v h).size
h₁ : ¬k < i
h₂ : ¬k = i
⊢ k - 1 < as.size

Tactic:
simp at h'

Result:
α : Type ?u.120154
as : Array α
i : Nat
h : i ≤ as.size
v : α
k : Nat
h₁ : ¬k < i
h₂ : ¬k = i
h' : k < as.size + 1
⊢ k - 1 < as.size

Proof state:
α : Type u_1
as : Array α
i : Nat
h : i ≤ as.size
v : α
k : Nat
h'✝ : k < (as.insertIdx i v h).size
h' : k < as.size + 1
⊢ (if h₁ : k < i then (as.push v)[k]
    else
      if h₂ : k = i then if i ≤ as.size then (as.push v)[as.size] else (as.push v)[i]
      else if k ≤ as.size then (as.push v)[k - 1] else (as.push v)[k]) =
    if h₁ : k < i then as[k] else if h₂ : k = i then v else as[k - 1]

Tactic:
replace h' : k ≤ as.size := by omega

Result:
α : Type u_1
as : Array α
i : Nat
h : i ≤ as.size
v : α
k : Nat
h'✝ : k < (as.insertIdx i v h).size
h' : k ≤ as.size
⊢ (if h₁ : k < i then (as.push v)[k]
    else
      if h₂ : k = i then if i ≤ as.size then (as.push v)[as.size] else (as.push v)[i]
      else if k ≤ as.size then (as.push v)[k - 1] else (as.push v)[k]) =
    if h₁ : k < i then as[k] else if h₂ : k = i then v else as[k - 1]

Proof state:
case isFalse.isFalse
α : Type u_1
as : Array α
i : Nat
h : i ≤ as.size
v : α
k : Nat
h'✝ : k < (as.insertIdx i v h).size
h' : k ≤ as.size
h₁ : ¬k < i
h₂ : ¬k = i
⊢ (if h : k - 1 < as.size then as[k - 1] else v) = as[k - 1]

Tactic:
split <;> rename_i h₃

Result:
case isFalse.isFalse.isTrue
α : Type u_1
as : Array α
i : Nat
h : i ≤ as.size
v : α
k : Nat
h'✝ : k < (as.insertIdx i v h).size
h' : k ≤ as.size
h₁ : ¬k < i
h₂ : ¬k = i
h₃ : k - 1 < as.size
⊢ as[k - 1] = as[k - 1]

case isFalse.isFalse.isFalse
α : Type u_1
as : Array α
i : Nat
h : i ≤ as.size
v : α
k : Nat
h'✝ : k < (as.insertIdx i v h).size
h' : k ≤ as.size
h₁ : ¬k < i
h₂ : ¬k = i
h₃ : ¬k - 1 < as.size
⊢ v = as[k - 1]

Proof state:
α : Type u_1
as : Array α
i : Nat
h : i ≤ as.size
v : α
k : Nat
h'✝ : k < (as.insertIdx i v h).size
h' : k ≤ as.size
⊢ (if k < i then if h : k < as.size then as[k] else v
    else if k = i then v else if h : k - 1 < as.size then as[k - 1] else v) =
    if h₁ : k < i then as[k] else if h₂ : k = i then v else as[k - 1]

Tactic:
split <;> rename_i h₁

Result:
case isTrue
α : Type u_1
as : Array α
i : Nat
h : i ≤ as.size
v : α
k : Nat
h'✝ : k < (as.insertIdx i v h).size
h' : k ≤ as.size
h₁ : k < i
⊢ (if h : k < as.size then as[k] else v) = as[k]

case isFalse
α : Type u_1
as : Array α
i : Nat
h : i ≤ as.size
v : α
k : Nat
h'✝ : k < (as.insertIdx i v h).size
h' : k ≤ as.size
h₁ : ¬k < i
⊢ (if k = i then v else if h : k - 1 < as.size then as[k - 1] else v) = if h₂ : k = i then v else as[k - 1]

Proof state:
case isFalse.isTrue
α : Type u_1
as : Array α
i : Nat
h : i ≤ as.size
v : α
k : Nat
h'✝ : k < (as.insertIdx i v h).size
h' : k ≤ as.size
h₁ : ¬k < i
h₂ : k = i
⊢ v = v

Tactic:
simp [h₂]

Result:
no goals

Proof state:
α : Type ?u.120154
as : Array α
i : Nat
h : i ≤ as.size
v : α
k : Nat
h' : k < (as.insertIdx i v h).size
h₁ : k < i
⊢ k < as.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
as : Array α
i : Nat
h : i ≤ as.size
v : α
k : Nat
h'✝ : k < (as.insertIdx i v h).size
h' : k < as.size + 1
⊢ k ≤ as.size

Tactic:
omega

Result:
no goals

Proof state:
case isFalse
α : Type u_1
as : Array α
i : Nat
h : i ≤ as.size
v : α
k : Nat
h'✝ : k < (as.insertIdx i v h).size
h' : k ≤ as.size
h₁ : ¬k < i
⊢ (if k = i then v else if h : k - 1 < as.size then as[k - 1] else v) = if h₂ : k = i then v else as[k - 1]

Tactic:
split <;> rename_i h₂

Result:
case isFalse.isTrue
α : Type u_1
as : Array α
i : Nat
h : i ≤ as.size
v : α
k : Nat
h'✝ : k < (as.insertIdx i v h).size
h' : k ≤ as.size
h₁ : ¬k < i
h₂ : k = i
⊢ v = v

case isFalse.isFalse
α : Type u_1
as : Array α
i : Nat
h : i ≤ as.size
v : α
k : Nat
h'✝ : k < (as.insertIdx i v h).size
h' : k ≤ as.size
h₁ : ¬k < i
h₂ : ¬k = i
⊢ (if h : k - 1 < as.size then as[k - 1] else v) = as[k - 1]

Proof state:
α : Type u_1
as : Array α
i : Nat
h : i ≤ as.size
v : α
k : Nat
h'✝ : k < (as.insertIdx i v h).size
h' : k ≤ as.size
⊢ (if h₁ : k < i then (as.push v)[k]
    else
      if h₂ : k = i then if i ≤ as.size then (as.push v)[as.size] else (as.push v)[i]
      else if k ≤ as.size then (as.push v)[k - 1] else (as.push v)[k]) =
    if h₁ : k < i then as[k] else if h₂ : k = i then v else as[k - 1]

Tactic:
simp only [getElem_push, h, ↓reduceIte, Nat.lt_irrefl, ↓reduceDIte, h', dite_eq_ite]

Result:
α : Type u_1
as : Array α
i : Nat
h : i ≤ as.size
v : α
k : Nat
h'✝ : k < (as.insertIdx i v h).size
h' : k ≤ as.size
⊢ (if k < i then if h : k < as.size then as[k] else v
    else if k = i then v else if h : k - 1 < as.size then as[k - 1] else v) =
    if h₁ : k < i then as[k] else if h₂ : k = i then v else as[k - 1]

Proof state:
case isTrue
α : Type u_1
as : Array α
i : Nat
h : i ≤ as.size
v : α
k : Nat
h'✝ : k < (as.insertIdx i v h).size
h' : k ≤ as.size
h₁ : k < i
⊢ (if h : k < as.size then as[k] else v) = as[k]

Tactic:
rw [dif_pos (by omega)]

Result:
no goals

Proof state:
α : Type u_1
as : Array α
i : Nat
h : i ≤ as.size
v : α
k : Nat
h' : k < (as.insertIdx i v h).size
⊢ (as.insertIdx i v h)[k] = if h₁ : k < i then as[k] else if h₂ : k = i then v else as[k - 1]

Tactic:
unfold insertIdx

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

Proof state:
α : Type ?u.120154
as : Array α
i : Nat
h : i ≤ as.size
v : α
k : Nat
h₁ : ¬k < i
h₂ : ¬k = i
h' : k < as.size + 1
⊢ k - 1 < as.size

Tactic:
omega

Result:
no goals

Proof state:
case isFalse.isFalse.isFalse
α : Type u_1
as : Array α
i : Nat
h : i ≤ as.size
v : α
k : Nat
h'✝ : k < (as.insertIdx i v h).size
h' : k ≤ as.size
h₁ : ¬k < i
h₂ : ¬k = i
h₃ : ¬k - 1 < as.size
⊢ v = as[k - 1]

Tactic:
omega

Result:
no goals

Proof state:
case isFalse.isFalse.isTrue
α : Type u_1
as : Array α
i : Nat
h : i ≤ as.size
v : α
k : Nat
h'✝ : k < (as.insertIdx i v h).size
h' : k ≤ as.size
h₁ : ¬k < i
h₂ : ¬k = i
h₃ : k - 1 < as.size
⊢ as[k - 1] = as[k - 1]

Tactic:
rfl

Result:
no goals