kerase_append_left — Mathlib

English

If a ∈ l1.keys, then kerase a (l1 ++ l2) = kerase a l1 ++ l2. This describes how kerase distributes over left concatenation when the key appears in the left part.

Русский

Если a принадлежит l1.keys, то kerase a (l1 ++ l2) = kerase a l1 ++ l2.

LaTeX

$$∀ {l1 l2 : List (Σ β)}, a ∈ l1.keys → kerase a (l1 ++ l2) = kerase a l1 ++ l2$$

Lean4

theorem kerase_append_left {a} : ∀ {l₁ l₂ : List (Sigma β)}, a ∈ l₁.keys → kerase a (l₁ ++ l₂) = kerase a l₁ ++ l₂
  | [], _, h => by cases h
  | s :: l₁, l₂, h₁ => by if h₂ : a = s.1 then simp [h₂] else simp_all [kerase_append_left]

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