no goals
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
x✝ : List (Sigma β)
h : a ∈ keys []
⊢ kerase a ([] ++ x✝) = kerase a [] ++ x✝
cases h
no goals
α : Type u
β : α → Type v
l l₁✝ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
s : Sigma β
l₁ : List (Sigma β)
l₂ : List (Sigma β)
h₁ : a ∈ keys (s :: l₁)
⊢ kerase a (s :: l₁ ++ l₂) = kerase a (s :: l₁) ++ l₂
if h₂ : a = s.1 then simp [h₂]
else simp at h₁; cases' h₁ with h₁ h₁ <;> [exact absurd h₁ h₂; simp [h₂, kerase_append_left h₁]]
no goals
α : Type u
β : α → Type v
l l₁✝ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
s : Sigma β
l₁ : List (Sigma β)
l₂ : List (Sigma β)
h₁ : a ∈ keys (s :: l₁)
h₂ : a = s.fst
⊢ kerase a (s :: l₁ ++ l₂) = kerase a (s :: l₁) ++ l₂
simp [h₂]
α : Type u
β : α → Type v
l l₁✝ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
s : Sigma β
l₁ : List (Sigma β)
l₂ : List (Sigma β)
h₂ : ¬a = s.fst
h₁ : a = s.fst ∨ a ∈ keys l₁
⊢ kerase a (s :: l₁ ++ l₂) = kerase a (s :: l₁) ++ l₂
α : Type u
β : α → Type v
l l₁✝ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
s : Sigma β
l₁ : List (Sigma β)
l₂ : List (Sigma β)
h₁ : a ∈ keys (s :: l₁)
h₂ : ¬a = s.fst
⊢ kerase a (s :: l₁ ++ l₂) = kerase a (s :: l₁) ++ l₂
simp at h₁
no goals
α : Type u
β : α → Type v
l l₁✝ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
s : Sigma β
l₁ : List (Sigma β)
l₂ : List (Sigma β)
h₂ : ¬a = s.fst
h₁ : a = s.fst ∨ a ∈ keys l₁
⊢ kerase a (s :: l₁ ++ l₂) = kerase a (s :: l₁) ++ l₂
cases' h₁ with h₁ h₁ <;> [exact absurd h₁ h₂; simp [h₂, kerase_append_left h₁]]