char_rmatch_iff — Mathlib

English

For any a, rmatch(char a) x is true only if x equals [a].

Русский

Для любого a rmatch(char a) x истинно тогда, когда x равно [a].

LaTeX

$$$$ rmatch(\\mathrm{char}(a), x) \\text{ is true } \\iff x = [a]. $$$$

Lean4

theorem char_rmatch_iff (a : α) (x : List α) : rmatch (char a) x ↔ x = [a] :=
  by
  rcases x with - | ⟨_, x⟩
  · exact of_decide_eq_true rfl
  · rcases x with - | ⟨head, tail⟩
    · rw [rmatch, deriv, List.singleton_inj]
      split <;> tauto
    · rw [rmatch, rmatch, deriv, cons.injEq]
      split
      · simp_rw [deriv_one, zero_rmatch, reduceCtorEq, and_false]
      · simp_rw [deriv_zero, zero_rmatch, reduceCtorEq, and_false]

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