-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem set_eq_take_append_cons_drop (l : List α) (n : Nat) (a : α) :
    l.set n a = if n < l.length then l.take n ++ a :: l.drop (n + 1) else l

Proof state:
case pos
α : Type u_1
l : List α
a : α
m : Nat
h : m < l.length
h' : ¬m < m
⊢ min m l.length ≤ m

Tactic:
exact Nat.min_le_left m l.length

Result:
no goals

Proof state:
α : Type u_1
l : List α
n : Nat
a : α
⊢ l.set n a = if n < l.length then take n l ++ a :: drop (n + 1) l else l

Tactic:
split <;> rename_i h

Result:
case isTrue
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
⊢ l.set n a = take n l ++ a :: drop (n + 1) l

case isFalse
α : Type u_1
l : List α
n : Nat
a : α
h : ¬n < l.length
⊢ l.set n a = l

Proof state:
case neg.intro
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
k : Nat
h' : ¬n + k + 1 < n
h'' : ¬n + k + 1 = n
h''' : n < n + k + 1
p : n + k + 1 - n = k + 1
⊢ l[n + k + 1]? = (a :: drop (n + 1) l)[n + k + 1 - n]?

Tactic:
rw [p]

Result:
case neg.intro
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
k : Nat
h' : ¬n + k + 1 < n
h'' : ¬n + k + 1 = n
h''' : n < n + k + 1
p : n + k + 1 - n = k + 1
⊢ l[n + k + 1]? = (a :: drop (n + 1) l)[k + 1]?

Proof state:
case pos
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
m : Nat
h' : ¬m < n
h'' : m = n
⊢ (l.set n a)[m]? = (take n l ++ a :: drop (n + 1) l)[m]?

Tactic:
subst h''

Result:
case pos
α : Type u_1
l : List α
a : α
m : Nat
h : m < l.length
h' : ¬m < m
⊢ (l.set m a)[m]? = (take m l ++ a :: drop (m + 1) l)[m]?

Proof state:
case neg.intro
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
k : Nat
h' : ¬n + k + 1 < n
h'' : ¬n + k + 1 = n
h''' : n < n + k + 1
⊢ l[n + k + 1]? = (a :: drop (n + 1) l)[n + k + 1 - n]?

Tactic:
have p : n + k + 1 - n = k + 1 := by omega

Result:
case neg.intro
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
k : Nat
h' : ¬n + k + 1 < n
h'' : ¬n + k + 1 = n
h''' : n < n + k + 1
p : n + k + 1 - n = k + 1
⊢ l[n + k + 1]? = (a :: drop (n + 1) l)[n + k + 1 - n]?

Proof state:
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
m : Nat
h' : ¬m < n
h'' : ¬m = n
⊢ n < m

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
l : List α
a : α
m : Nat
h : m < l.length
h' : ¬m < m
⊢ m ≤ l.length

Tactic:
omega

Result:
no goals

Proof state:
case neg
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
m : Nat
h' : ¬m < n
⊢ (l.set n a)[m]? = (take n l ++ a :: drop (n + 1) l)[m]?

Tactic:
by_cases h'' : m = n

Result:
case pos
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
m : Nat
h' : ¬m < n
h'' : m = n
⊢ (l.set n a)[m]? = (take n l ++ a :: drop (n + 1) l)[m]?

case neg
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
m : Nat
h' : ¬m < n
h'' : ¬m = n
⊢ (l.set n a)[m]? = (take n l ++ a :: drop (n + 1) l)[m]?

Proof state:
case isTrue
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
⊢ l.set n a = take n l ++ a :: drop (n + 1) l

Tactic:
ext1 m

Result:
case isTrue.h
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
m : Nat
⊢ (l.set n a)[m]? = (take n l ++ a :: drop (n + 1) l)[m]?

Proof state:
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
m : Nat
h' : m < n
⊢ m < min n l.length

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
m : Nat
h' : ¬m < n
h'' : ¬m = n
h''' : n < m
⊢ n ≠ m

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
m : Nat
h' : ¬m < n
h'' : ¬m = n
h''' : n < m
⊢ n ≤ l.length

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
k : Nat
h' : ¬n + k + 1 < n
h'' : ¬n + k + 1 = n
h''' : n < n + k + 1
⊢ n + k + 1 - n = k + 1

Tactic:
omega

Result:
no goals

Proof state:
case neg
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
m : Nat
h' : ¬m < n
h'' : ¬m = n
h''' : n < m
⊢ l[m]? = (a :: drop (n + 1) l)[m - n]?

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt h'''

Result:
case neg.intro
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
k : Nat
h' : ¬n + k + 1 < n
h'' : ¬n + k + 1 = n
h''' : n < n + k + 1
⊢ l[n + k + 1]? = (a :: drop (n + 1) l)[n + k + 1 - n]?

Proof state:
case isFalse
α : Type u_1
l : List α
n : Nat
a : α
h : ¬n < l.length
⊢ l.set n a = l

Tactic:
rw [set_eq_of_length_le]

Result:
case isFalse.h
α : Type u_1
l : List α
n : Nat
a : α
h : ¬n < l.length
⊢ l.length ≤ n

Proof state:
case neg.intro
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
k : Nat
h' : ¬n + k + 1 < n
h'' : ¬n + k + 1 = n
h''' : n < n + k + 1
p : n + k + 1 - n = k + 1
⊢ l[n + k + 1]? = (a :: drop (n + 1) l)[k + 1]?

Tactic:
rw [getElem?_cons_succ, getElem?_drop]

Result:
case neg.intro
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
k : Nat
h' : ¬n + k + 1 < n
h'' : ¬n + k + 1 = n
h''' : n < n + k + 1
p : n + k + 1 - n = k + 1
⊢ l[n + k + 1]? = l[n + 1 + k]?

Proof state:
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
m : Nat
h' : m < n
⊢ n ≠ m

Tactic:
omega

Result:
no goals

Proof state:
case pos
α : Type u_1
l : List α
a : α
m : Nat
h : m < l.length
h' : ¬m < m
⊢ (l.set m a)[m]? = (take m l ++ a :: drop (m + 1) l)[m]?

Tactic:
rw [getElem?_set_self ‹_›, getElem?_append_right, length_take,
  Nat.min_eq_left (by omega), Nat.sub_self, getElem?_cons_zero]

Result:
case pos
α : Type u_1
l : List α
a : α
m : Nat
h : m < l.length
h' : ¬m < m
⊢ (take m l).length ≤ m

Proof state:
case isTrue.h
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
m : Nat
⊢ (l.set n a)[m]? = (take n l ++ a :: drop (n + 1) l)[m]?

Tactic:
by_cases h' : m < n

Result:
case pos
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
m : Nat
h' : m < n
⊢ (l.set n a)[m]? = (take n l ++ a :: drop (n + 1) l)[m]?

case neg
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
m : Nat
h' : ¬m < n
⊢ (l.set n a)[m]? = (take n l ++ a :: drop (n + 1) l)[m]?

Proof state:
case neg.intro
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
k : Nat
h' : ¬n + k + 1 < n
h'' : ¬n + k + 1 = n
h''' : n < n + k + 1
p : n + k + 1 - n = k + 1
⊢ l[n + k + 1]? = l[n + 1 + k]?

Tactic:
congr 1

Result:
case neg.intro.e_a
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
k : Nat
h' : ¬n + k + 1 < n
h'' : ¬n + k + 1 = n
h''' : n < n + k + 1
p : n + k + 1 - n = k + 1
⊢ n + k + 1 = n + 1 + k

Proof state:
case neg.intro.e_a
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
k : Nat
h' : ¬n + k + 1 < n
h'' : ¬n + k + 1 = n
h''' : n < n + k + 1
p : n + k + 1 - n = k + 1
⊢ n + k + 1 = n + 1 + k

Tactic:
omega

Result:
no goals

Proof state:
case pos
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
m : Nat
h' : m < n
⊢ (l.set n a)[m]? = (take n l ++ a :: drop (n + 1) l)[m]?

Tactic:
rw [getElem?_append_left (by simp [length_take]; omega), getElem?_set_ne (by omega),
  getElem?_take_of_lt h']

Result:
no goals

Proof state:
case neg
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
m : Nat
h' : ¬m < n
h'' : ¬m = n
h''' : n < m
⊢ (l.set n a)[m]? = (take n l ++ a :: drop (n + 1) l)[m]?

Tactic:
rw [getElem?_set_ne (by omega), getElem?_append_right, length_take,
  Nat.min_eq_left (by omega)]

Result:
case neg
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
m : Nat
h' : ¬m < n
h'' : ¬m = n
h''' : n < m
⊢ l[m]? = (a :: drop (n + 1) l)[m - n]?

case neg
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
m : Nat
h' : ¬m < n
h'' : ¬m = n
h''' : n < m
⊢ (take n l).length ≤ m

Proof state:
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
m : Nat
h' : m < n
⊢ m < (take n l).length

Tactic:
simp [length_take]

Result:
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
m : Nat
h' : m < n
⊢ m < min n l.length

Proof state:
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
m : Nat
h' : ¬m < n
h'' : ¬m = n
h''' : n < m
⊢ n ≤ m

Tactic:
omega

Result:
no goals