no goals
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : ¬a ∈ keys l
⊢ kerase a l = l
induction' l with _ _ ih <;> [rfl; (simp [not_or] at h; simp [h.1, ih h.2])]
case cons
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h✝ : ¬a ∈ keys l
head✝ : Sigma β
tail✝ : List (Sigma β)
ih : ¬a ∈ keys tail✝ → kerase a tail✝ = tail✝
h : ¬a = head✝.fst ∧ ¬a ∈ keys tail✝
⊢ kerase a (head✝ :: tail✝) = head✝ :: tail✝
case cons
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h✝ : ¬a ∈ keys l
head✝ : Sigma β
tail✝ : List (Sigma β)
ih : ¬a ∈ keys tail✝ → kerase a tail✝ = tail✝
h : ¬a ∈ keys (head✝ :: tail✝)
⊢ kerase a (head✝ :: tail✝) = head✝ :: tail✝
simp [not_or] at h
no goals
case cons
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h✝ : ¬a ∈ keys l
head✝ : Sigma β
tail✝ : List (Sigma β)
ih : ¬a ∈ keys tail✝ → kerase a tail✝ = tail✝
h : ¬a = head✝.fst ∧ ¬a ∈ keys tail✝
⊢ kerase a (head✝ :: tail✝) = head✝ :: tail✝
simp [h.1, ih h.2]