α : Type uu
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableEq α
L : List α
a b : α
⊢ (if a = b then Nat.succ (count a L) else count a L) = count a L + if a = b then 1 else 0
α : Type uu
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableEq α
L : List α
a b : α
⊢ count a (orderedInsert r b L) = count a L + if a = b then 1 else 0
rw [(L.perm_orderedInsert r b).count_eq, count_cons]
no goals
α : Type uu
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableEq α
L : List α
a b : α
⊢ (if a = b then Nat.succ (count a L) else count a L) = count a L + if a = b then 1 else 0
split_ifs <;> simp only [Nat.succ_eq_add_one, add_zero]