dropWhile_eq_self_iff — Mathlib

English

dropWhile p l = l iff the first element of l does not satisfy p (assuming l is nonempty).

Русский

dropWhile p l = l эквивалентно тому, что первый элемент l не удовлетворяет p (при условии, что l непуст).

LaTeX

$$$\\mathrm{dropWhile}(p, l) = l \\iff \\forall hl: |l|>0, \\; \\lnot p(l[0])$$$

Lean4

@[simp]
theorem dropWhile_eq_self_iff : dropWhile p l = l ↔ ∀ hl : 0 < l.length, ¬p (l[0]'hl) :=
  by
  rcases l with - | ⟨hd, tl⟩
  · simp
  · rw [dropWhile]
    by_cases h_p_hd : p hd
    · simp only [h_p_hd, length_cons, Nat.zero_lt_succ, getElem_cons_zero, not_true_eq_false, imp_false, iff_false]
      intro h
      replace h := congrArg length h
      have := length_dropWhile_le p tl
      simp at h
      cutsat
    · simp [h_p_hd]

Похожие утверждения