English
If p holds for all elements of s, then p holds for all elements of s.set n x, provided p x holds for the updated element.
Русский
Если p выполняется для всех элементов s, то p выполняется для всех элементов s.set n x, если при этом p x для обновлённого элемента.
LaTeX
$$$\forall s\,\forall p,\ (\forall (x:α),\ x\in s\Rightarrow p x) \rightarrow \forall y\in (s.set n x),\ p y$$$
Lean4
theorem set_all {p : α → Prop} {s : Seq α} (h_all : ∀ x ∈ s, p x) {n : ℕ} {x : α} (hx : p x) : ∀ y ∈ (s.set n x), p y :=
by
intro y hy
simp only [mem_iff_exists_get?] at hy
obtain ⟨m, hy⟩ := hy
rcases eq_or_ne n m with (rfl | h_nm)
· by_cases h_term : s.TerminatedAt n
· simp [get?_set_of_terminatedAt _ h_term] at hy
· simp_all [get?_set_of_not_terminatedAt _ h_term]
· rw [get?_set_of_ne _ _ h_nm.symm] at hy
apply h_all _ (get?_mem hy.symm)
