chore(Logic/Equiv): change type of sumEquivSigmaBool to simp normal…

… form (#21338)

`simp` eagerly rewrites `Bool.casesOn` to `Bool.rec`, so using the former in the type signature prevents related `simp` lemmas from firing.

See [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60.40.5Bsimp.5D.60.20lemmas.20about.20Equiv.2EsumEquivSigmaBool.20don't.20fire).

Mathlib/Logic/Equiv/Basic.lean

@@ -27,7 +27,7 @@ In this file we continue the work on equivalences begun in `Mathlib/Logic/Equiv/
 * canonical isomorphisms between various types: e.g.,
 
   - `Equiv.sumEquivSigmaBool` is the canonical equivalence between the sum of two types `α ⊕ β`
-    and the sigma-type `Σ b : Bool, b.casesOn α β`;
+    and the sigma-type `Σ b, bif b then β else α`;
 
   - `Equiv.prodSumDistrib : α × (β ⊕ γ) ≃ (α × β) ⊕ (α × γ)` shows that type product and type sum
     satisfy the distributive law up to a canonical equivalence;
@@ -476,7 +476,7 @@ def piOptionEquivProd {α} {β : Option α → Type*} :
 `β` to be types from the same universe, so it cannot be used directly to transfer theorems about
 sigma types to theorems about sum types. In many cases one can use `ULift` to work around this
 difficulty. -/
-def sumEquivSigmaBool (α β) : α ⊕ β ≃ Σ b : Bool, b.casesOn α β :=
+def sumEquivSigmaBool (α β) : α ⊕ β ≃ Σ b, bif b then β else α :=
   ⟨fun s => s.elim (fun x => ⟨false, x⟩) fun x => ⟨true, x⟩, fun s =>
     match s with
     | ⟨false, a⟩ => inl a