chore: fix the names of some Bool lemmas (#7841)

Author: astrainfinita

Mathlib/Combinatorics/SimpleGraph/Basic.lean

@@ -145,7 +145,7 @@ def SimpleGraph.mk' {V : Type u} :
     simp only [mk.injEq, Subtype.mk.injEq]
     intro h
     funext v w
-    simpa [Bool.coe_bool_iff] using congr_fun₂ h v w
+    simpa [Bool.coe_iff_coe] using congr_fun₂ h v w
 
 /-- We can enumerate simple graphs by enumerating all functions `V → V → Bool`
 and filtering on whether they are symmetric and irreflexive. -/

Mathlib/Computability/RegularExpressions.lean

@@ -238,7 +238,7 @@ theorem char_rmatch_iff (a : α) (x : List α) : rmatch (char a) x ↔ x = [a] :
 theorem add_rmatch_iff (P Q : RegularExpression α) (x : List α) :
     (P + Q).rmatch x ↔ P.rmatch x ∨ Q.rmatch x := by
   induction' x with _ _ ih generalizing P Q
-  · simp only [rmatch, matchEpsilon, Bool.or_coe_iff]
+  · simp only [rmatch, matchEpsilon, Bool.coe_or_iff]
   · repeat' rw [rmatch]
     rw [deriv_add]
     exact ih _ _
@@ -252,7 +252,7 @@ theorem mul_rmatch_iff (P Q : RegularExpression α) (x : List α) :
     · intro h
       refine' ⟨[], [], rfl, _⟩
       rw [rmatch, rmatch]
-      rwa [Bool.and_coe_iff] at h
+      rwa [Bool.coe_and_iff] at h
     · rintro ⟨t, u, h₁, h₂⟩
       cases' List.append_eq_nil.1 h₁.symm with ht hu
       subst ht

Mathlib/Data/Bool/AllAny.lean

@@ -27,7 +27,7 @@ namespace List
 theorem all_iff_forall {p : α → Bool} : all l p ↔ ∀ a ∈ l, p a := by
   induction' l with a l ih
   · exact iff_of_true rfl (forall_mem_nil _)
-  simp only [all_cons, Bool.and_coe_iff, ih, forall_mem_cons]
+  simp only [all_cons, Bool.coe_and_iff, ih, forall_mem_cons]
 #align list.all_iff_forall List.all_iff_forall
 
 theorem all_iff_forall_prop : (all l fun a => p a) ↔ ∀ a ∈ l, p a := by
@@ -42,7 +42,7 @@ theorem all_iff_forall_prop : (all l fun a => p a) ↔ ∀ a ∈ l, p a := by
 theorem any_iff_exists {p : α → Bool} : any l p ↔ ∃ a ∈ l, p a := by
   induction' l with a l ih
   · exact iff_of_false Bool.not_false' (not_exists_mem_nil _)
-  simp only [any_cons, Bool.or_coe_iff, ih, exists_mem_cons_iff]
+  simp only [any_cons, Bool.coe_or_iff, ih, exists_mem_cons_iff]
 #align list.any_iff_exists List.any_iff_exists
 
 theorem any_iff_exists_prop : (any l fun a => p a) ↔ ∃ a ∈ l, p a := by simp [any_iff_exists]

Mathlib/Data/Bool/Basic.lean

@@ -138,8 +138,8 @@ theorem cond_not {α} (b : Bool) (t e : α) : cond (!b) t e = cond b e t := by c
 theorem not_ne_id : not ≠ id := fun h ↦ false_ne_true <| congrFun h true
 #align bool.bnot_ne_id Bool.not_ne_id
 
-theorem coe_bool_iff : ∀ {a b : Bool}, (a ↔ b) ↔ a = b := by decide
-#align bool.coe_bool_iff Bool.coe_bool_iff
+theorem coe_iff_coe : ∀ {a b : Bool}, (a ↔ b) ↔ a = b := by decide
+#align bool.coe_bool_iff Bool.coe_iff_coe
 
 theorem eq_true_of_ne_false : ∀ {a : Bool}, a ≠ false → a = true := by decide
 #align bool.eq_tt_of_ne_ff Bool.eq_true_of_ne_false

Mathlib/Init/Data/Bool/Lemmas.lean

@@ -161,16 +161,16 @@ theorem decide_congr {p q : Prop} [Decidable p] [Decidable q] (h : p ↔ q) :
   | true => exact decide_true (h.2 <| of_decide_true h')
 #align to_bool_congr Bool.decide_congr
 
-theorem or_coe_iff (a b : Bool) : a || b ↔ a ∨ b := by simp
-#align bor_coe_iff Bool.or_coe_iff
+theorem coe_or_iff (a b : Bool) : a || b ↔ a ∨ b := by simp
+#align bor_coe_iff Bool.coe_or_iff
 
-theorem and_coe_iff (a b : Bool) : a && b ↔ a ∧ b := by simp
-#align band_coe_iff Bool.and_coe_iff
+theorem coe_and_iff (a b : Bool) : a && b ↔ a ∧ b := by simp
+#align band_coe_iff Bool.coe_and_iff
 
 @[simp]
-theorem xor_coe_iff (a b : Bool) : xor a b ↔ Xor' (a = true) (b = true) := by
+theorem coe_xor_iff (a b : Bool) : xor a b ↔ Xor' (a = true) (b = true) := by
   cases a <;> cases b <;> exact by decide
-#align bxor_coe_iff Bool.xor_coe_iff
+#align bxor_coe_iff Bool.coe_xor_iff
 
 @[simp]
 theorem ite_eq_true_distrib (c : Prop) [Decidable c] (a b : Bool) :