no goals
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a₁ a₂ : α
l : List (Sigma β)
h : a₁ ≠ a₂
p✝ : a₁ ∈ keys l
w✝² : β a₂
w✝¹ w✝ : List (Sigma β)
left✝ : ¬a₂ ∈ keys w✝¹
p : a₁ ∈ keys (w✝¹ ++ { fst := a₂, snd := w✝² } :: w✝)
q : a₂ ∈ keys (w✝¹ ++ { fst := a₂, snd := w✝² } :: w✝)
⊢ a₁ ∈ keys (w✝¹ ++ w✝)
simpa [keys, h] using p
no goals
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a₁ a₂ : α
l : List (Sigma β)
h : a₁ ≠ a₂
p : a₁ ∈ keys l
q : ¬a₂ ∈ keys l
⊢ a₁ ∈ keys (kerase a₂ l)
simp [q, p]