-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem_insert (l : List α) (a : α) (i : Nat) (h : i < l.length) :
    (l.insert a)[i]'(Nat.lt_of_lt_of_le h length_le_length_insert) =
      if a ∈ l then l[i] else if i = 0 then a else l[i-1]'(Nat.lt_of_le_of_lt (Nat.pred_le _) h)

Proof state:
case x
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
i : Nat
h : i < l.length
⊢ (if a ∈ l then l[i]? else if i = 0 then some a else l[i - 1]?) =
    some (if a ∈ l then l[i] else if i = 0 then a else l[i - 1])

Tactic:
split

Result:
case x.isTrue
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
i : Nat
h : i < l.length
h✝ : a ∈ l
⊢ l[i]? = some l[i]

case x.isFalse
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
i : Nat
h : i < l.length
h✝ : ¬a ∈ l
⊢ (if i = 0 then some a else l[i - 1]?) = some (if i = 0 then a else l[i - 1])

Proof state:
case x.isFalse.isFalse
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
i : Nat
h : i < l.length
h✝¹ : ¬a ∈ l
h✝ : ¬i = 0
⊢ l[i - 1]? = some l[i - 1]

Tactic:
have h' : i - 1 < l.length := Nat.lt_of_le_of_lt (Nat.pred_le _) h

Result:
case x.isFalse.isFalse
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
i : Nat
h : i < l.length
h✝¹ : ¬a ∈ l
h✝ : ¬i = 0
h' : i - 1 < l.length
⊢ l[i - 1]? = some l[i - 1]

Proof state:
case x
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
i : Nat
h : i < l.length
⊢ some (List.insert a l)[i] = some (if a ∈ l then l[i] else if i = 0 then a else l[i - 1])

Tactic:
rw [← getElem?_eq_getElem, getElem?_insert]

Result:
case x
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
i : Nat
h : i < l.length
⊢ (if a ∈ l then l[i]? else if i = 0 then some a else l[i - 1]?) =
    some (if a ∈ l then l[i] else if i = 0 then a else l[i - 1])

Proof state:
case x.isTrue
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
i : Nat
h : i < l.length
h✝ : a ∈ l
⊢ l[i]? = some l[i]

Tactic:
simp [getElem?_eq_getElem, h]

Result:
no goals

Proof state:
case x.isFalse.isFalse
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
i : Nat
h : i < l.length
h✝¹ : ¬a ∈ l
h✝ : ¬i = 0
h' : i - 1 < l.length
⊢ l[i - 1]? = some l[i - 1]

Tactic:
simp [getElem?_eq_getElem, h']

Result:
no goals

Proof state:
case x.isFalse.isTrue
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
i : Nat
h : i < l.length
h✝¹ : ¬a ∈ l
h✝ : i = 0
⊢ some a = some a

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
i : Nat
h : i < l.length
⊢ (List.insert a l)[i] = if a ∈ l then l[i] else if i = 0 then a else l[i - 1]

Tactic:
apply Option.some.inj

Result:
case x
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
i : Nat
h : i < l.length
⊢ some (List.insert a l)[i] = some (if a ∈ l then l[i] else if i = 0 then a else l[i - 1])

Proof state:
case x.isFalse
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
i : Nat
h : i < l.length
h✝ : ¬a ∈ l
⊢ (if i = 0 then some a else l[i - 1]?) = some (if i = 0 then a else l[i - 1])

Tactic:
split

Result:
case x.isFalse.isTrue
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
i : Nat
h : i < l.length
h✝¹ : ¬a ∈ l
h✝ : i = 0
⊢ some a = some a

case x.isFalse.isFalse
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
i : Nat
h : i < l.length
h✝¹ : ¬a ∈ l
h✝ : ¬i = 0
⊢ l[i - 1]? = some l[i - 1]