case nil
α : Type u_1
l l₁✝ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
l₁ : List α
h : ¬a ∈ []
⊢ List.bagInter (a :: l₁) [] = List.bagInter l₁ []

case cons
α : Type u_1
l l₁✝ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
l₁ : List α
head✝ : α
tail✝ : List α
h : ¬a ∈ head✝ :: tail✝
⊢ List.bagInter (a :: l₁) (head✝ :: tail✝) = List.bagInter l₁ (head✝ :: tail✝)
α : Type u_1
l l₁✝ l₂ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
l₁ : List α
h : ¬a ∈ l₂
⊢ List.bagInter (a :: l₁) l₂ = List.bagInter l₁ l₂
cases l₂
no goals
case cons
α : Type u_1
l l₁✝ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
l₁ : List α
head✝ : α
tail✝ : List α
h : ¬a ∈ head✝ :: tail✝
⊢ List.bagInter (a :: l₁) (head✝ :: tail✝) = List.bagInter l₁ (head✝ :: tail✝)
simp only [erase_of_not_mem h, List.bagInter, if_neg (mt mem_of_elem_eq_true h)]
no goals
case nil
α : Type u_1
l l₁✝ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
l₁ : List α
h : ¬a ∈ []
⊢ List.bagInter (a :: l₁) [] = List.bagInter l₁ []
simp only [bagInter_nil]