-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem set_append {s t : List α} :
    (s ++ t).set i x = if i < s.length then s.set i x ++ t else s ++ t.set (i - s.length) x

Proof state:
case nil
α : Type u_1
x : α
t : List α
i : Nat
⊢ ([] ++ t).set i x = if i < [].length then [].set i x ++ t else [] ++ t.set (i - [].length) x

Tactic:
simp

Result:
no goals

Proof state:
case cons.zero
α : Type u_1
x : α
t : List α
a : α
as : List α
ih : ∀ {i : Nat}, (as ++ t).set i x = if i < as.length then as.set i x ++ t else as ++ t.set (i - as.length) x
⊢ (a :: as ++ t).set 0 x =
    if 0 < (a :: as).length then (a :: as).set 0 x ++ t else a :: as ++ t.set (0 - (a :: as).length) x

Tactic:
simp

Result:
no goals

Proof state:
case cons.succ
α : Type u_1
x : α
t : List α
a : α
as : List α
ih : ∀ {i : Nat}, (as ++ t).set i x = if i < as.length then as.set i x ++ t else as ++ t.set (i - as.length) x
i : Nat
⊢ (a :: if i < as.length then as.set i x ++ t else as ++ t.set (i - as.length) x) =
    if i < as.length then a :: (as.set i x ++ t) else a :: (as ++ t.set (i + 1 - (as.length + 1)) x)

Tactic:
split

Result:
case cons.succ.isTrue
α : Type u_1
x : α
t : List α
a : α
as : List α
ih : ∀ {i : Nat}, (as ++ t).set i x = if i < as.length then as.set i x ++ t else as ++ t.set (i - as.length) x
i : Nat
h✝ : i < as.length
⊢ a :: (as.set i x ++ t) = a :: (as.set i x ++ t)

case cons.succ.isFalse
α : Type u_1
x : α
t : List α
a : α
as : List α
ih : ∀ {i : Nat}, (as ++ t).set i x = if i < as.length then as.set i x ++ t else as ++ t.set (i - as.length) x
i : Nat
h✝ : ¬i < as.length
⊢ a :: (as ++ t.set (i - as.length) x) = a :: (as ++ t.set (i + 1 - (as.length + 1)) x)

Proof state:
case cons.succ
α : Type u_1
x : α
t : List α
a : α
as : List α
ih : ∀ {i : Nat}, (as ++ t).set i x = if i < as.length then as.set i x ++ t else as ++ t.set (i - as.length) x
i : Nat
⊢ (a :: as ++ t).set (i + 1) x =
    if i + 1 < (a :: as).length then (a :: as).set (i + 1) x ++ t else a :: as ++ t.set (i + 1 - (a :: as).length) x

Tactic:
simp [Nat.add_one_lt_add_one_iff, ih]

Result:
case cons.succ
α : Type u_1
x : α
t : List α
a : α
as : List α
ih : ∀ {i : Nat}, (as ++ t).set i x = if i < as.length then as.set i x ++ t else as ++ t.set (i - as.length) x
i : Nat
⊢ (a :: if i < as.length then as.set i x ++ t else as ++ t.set (i - as.length) x) =
    if i < as.length then a :: (as.set i x ++ t) else a :: (as ++ t.set (i + 1 - (as.length + 1)) x)

Proof state:
case cons.succ.isFalse
α : Type u_1
x : α
t : List α
a : α
as : List α
ih : ∀ {i : Nat}, (as ++ t).set i x = if i < as.length then as.set i x ++ t else as ++ t.set (i - as.length) x
i : Nat
h✝ : ¬i < as.length
⊢ a :: (as ++ t.set (i - as.length) x) = a :: (as ++ t.set (i + 1 - (as.length + 1)) x)

Tactic:
congr 3

Result:
case cons.succ.isFalse.e_tail.e_a.e_a
α : Type u_1
x : α
t : List α
a : α
as : List α
ih : ∀ {i : Nat}, (as ++ t).set i x = if i < as.length then as.set i x ++ t else as ++ t.set (i - as.length) x
i : Nat
h✝ : ¬i < as.length
⊢ i - as.length = i + 1 - (as.length + 1)

Proof state:
case cons.succ.isTrue
α : Type u_1
x : α
t : List α
a : α
as : List α
ih : ∀ {i : Nat}, (as ++ t).set i x = if i < as.length then as.set i x ++ t else as ++ t.set (i - as.length) x
i : Nat
h✝ : i < as.length
⊢ a :: (as.set i x ++ t) = a :: (as.set i x ++ t)

Tactic:
rfl

Result:
no goals

Proof state:
case cons.succ.isFalse.e_tail.e_a.e_a
α : Type u_1
x : α
t : List α
a : α
as : List α
ih : ∀ {i : Nat}, (as ++ t).set i x = if i < as.length then as.set i x ++ t else as ++ t.set (i - as.length) x
i : Nat
h✝ : ¬i < as.length
⊢ i - as.length = i + 1 - (as.length + 1)

Tactic:
rw [Nat.add_sub_add_right]

Result:
no goals