From 917ade67a58b5140aecf3a86c209e0adbafe5d83 Mon Sep 17 00:00:00 2001 From: Chris Wong Date: Mon, 3 Feb 2025 07:17:39 +0000 Subject: [PATCH] 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 | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Logic/Equiv/Basic.lean b/Mathlib/Logic/Equiv/Basic.lean index 42d71d763a3249..75b4bbbc81288c 100644 --- a/Mathlib/Logic/Equiv/Basic.lean +++ b/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