feat: port Data.List.Count (#1410)

- [x] depends on: #1380

Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: thirdsgames <thirdsgames2018@gmail.com>
Co-authored-by: zeramorphic <zeramorphic@proton.me>
Co-authored-by: zeramorphic <50671761+zeramorphic@users.noreply.github.com>

Author: 4 people

Mathlib.lean

@@ -246,6 +246,7 @@ import Mathlib.Data.List.Basic
 import Mathlib.Data.List.BigOperators.Basic
 import Mathlib.Data.List.Card
 import Mathlib.Data.List.Chain
+import Mathlib.Data.List.Count
 import Mathlib.Data.List.Defs
 import Mathlib.Data.List.Forall2
 import Mathlib.Data.List.Func

Mathlib/Data/Bool/Basic.lean

@@ -82,6 +82,18 @@ theorem decide_eq {p q : Prop} [Decidable p] [Decidable q] : decide p = decide q
 theorem not_false' : ¬false := fun.
 #align bool.not_ff Bool.not_false'
 
+-- Porting note: new theorem
+theorem eq_iff_eq_true_iff {a b : Bool} : a = b ↔ ((a = true) ↔ (b = true)) :=
+by cases a <;> cases b <;> simp
+
+-- Porting note: new theorem
+theorem beq_eq_decide_eq [DecidableEq α]
+  (a b : α) : (a == b) = decide (a = b) := rfl
+
+-- Porting note: new theorem
+theorem beq_comm [BEq α] [LawfulBEq α] {a b : α} : (a == b) = (b == a) :=
+  eq_iff_eq_true_iff.2 (by simp [@eq_comm α])
+
 @[simp]
 theorem default_bool : default = false :=
   rfl