English
ReduceOption equals a singleton [a] precisely when l can be split into an initial block of none's, a single some a, and a trailing block of none's.
Русский
ReduceOption равен единичному списку [a] тогда и только тогда, когда l можно разложить как none... ++ some a :: none...
LaTeX
$$$\operatorname{reduceOption}(l) = [a] \iff \exists m \exists n,\; l = \mathrm{replicate}_m(\mathrm{none}) ++ \mathrm{some}(a) :: \mathrm{replicate}_n(\mathrm{none})$$$
Lean4
theorem reduceOption_eq_singleton_iff (l : List (Option α)) (a : α) :
l.reduceOption = [a] ↔ ∃ m n, l = replicate m none ++ some a :: replicate n none :=
by
dsimp [reduceOption]
constructor
· intro h
rw [filterMap_eq_cons_iff] at h
obtain ⟨l₁, _, l₂, h, hl₁, ⟨⟩, hl₂⟩ := h
rw [filterMap_eq_nil_iff] at hl₂
apply eq_replicate_of_mem at hl₁
apply eq_replicate_of_mem at hl₂
rw [h, hl₁, hl₂]
use l₁.length, l₂.length
· intro ⟨_, _, h⟩
simp only [h, filterMap_append, filterMap_cons_some, filterMap_replicate_of_none, id_eq, nil_append,
Option.some.injEq]
