no goals
α : Type u_1
l : List α
inst✝ : DecidableEq α
a b : α
⊢ count a (List.erase [] b) = count a [] - if a = b then 1 else 0
simp
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b c : α
l : List α
⊢ count a (if c = b then l else c :: List.erase l b) = count a (c :: l) - if a = b then 1 else 0
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b c : α
l : List α
⊢ count a (List.erase (c :: l) b) = count a (c :: l) - if a = b then 1 else 0
rw [erase_cons]
case pos
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b c : α
l : List α
hc : c = b
⊢ count a (if c = b then l else c :: List.erase l b) = count a (c :: l) - if a = b then 1 else 0

case neg
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b c : α
l : List α
hc : ¬c = b
⊢ count a (if c = b then l else c :: List.erase l b) = count a (c :: l) - if a = b then 1 else 0
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b c : α
l : List α
⊢ count a (if c = b then l else c :: List.erase l b) = count a (c :: l) - if a = b then 1 else 0
by_cases hc : c = b
no goals
case pos
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b c : α
l : List α
hc : c = b
⊢ count a (if c = b then l else c :: List.erase l b) = count a (c :: l) - if a = b then 1 else 0
rw [if_pos hc, hc, count_cons', Nat.add_sub_cancel]
case neg
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b c : α
l : List α
hc : ¬c = b
⊢ ((count a l - if a = b then 1 else 0) + if a = c then 1 else 0) =
    (count a l + if a = c then 1 else 0) - if a = b then 1 else 0
case neg
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b c : α
l : List α
hc : ¬c = b
⊢ count a (if c = b then l else c :: List.erase l b) = count a (c :: l) - if a = b then 1 else 0
rw [if_neg hc, count_cons', count_cons', count_erase a b l]
case pos
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b c : α
l : List α
hc : ¬c = b
ha : a = b
⊢ ((count a l - if a = b then 1 else 0) + if a = c then 1 else 0) =
    (count a l + if a = c then 1 else 0) - if a = b then 1 else 0

case neg
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b c : α
l : List α
hc : ¬c = b
ha : ¬a = b
⊢ ((count a l - if a = b then 1 else 0) + if a = c then 1 else 0) =
    (count a l + if a = c then 1 else 0) - if a = b then 1 else 0
case neg
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b c : α
l : List α
hc : ¬c = b
⊢ ((count a l - if a = b then 1 else 0) + if a = c then 1 else 0) =
    (count a l + if a = c then 1 else 0) - if a = b then 1 else 0
by_cases ha : a = b
case pos
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b c : α
l : List α
hc : ¬a = c
ha : a = b
⊢ ((count a l - if a = b then 1 else 0) + if a = c then 1 else 0) =
    (count a l + if a = c then 1 else 0) - if a = b then 1 else 0
case pos
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b c : α
l : List α
hc : ¬c = b
ha : a = b
⊢ ((count a l - if a = b then 1 else 0) + if a = c then 1 else 0) =
    (count a l + if a = c then 1 else 0) - if a = b then 1 else 0
rw [← ha, eq_comm] at hc
no goals
case pos
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b c : α
l : List α
hc : ¬a = c
ha : a = b
⊢ ((count a l - if a = b then 1 else 0) + if a = c then 1 else 0) =
    (count a l + if a = c then 1 else 0) - if a = b then 1 else 0
rw [if_pos ha, if_neg hc, add_zero, add_zero]
no goals
case neg
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b c : α
l : List α
hc : ¬c = b
ha : ¬a = b
⊢ ((count a l - if a = b then 1 else 0) + if a = c then 1 else 0) =
    (count a l + if a = c then 1 else 0) - if a = b then 1 else 0
rw [if_neg ha, tsub_zero, tsub_zero]