From 420d0f2a3fa8666b24a606d031684ffdc2efc25d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 14 Feb 2022 11:37:23 -0800
Subject: [PATCH] fix: make sure `noConfusionTypeEnum` and `noConfusionEnum`
 fully reduce even reducibility setting is set to `TransparencyMode.reducible`

The previous definition would not fully reduce since `ite` and `dite`
are not tagged as `[reducible]`.

see issue #1016
---
 src/Init/Core.lean | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 8315f7bdb8..9fa94ec949 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -446,14 +446,17 @@ instance {c : Prop} {t : c → Prop} {e : ¬c → Prop} [dC : Decidable c] [dT :
   | isFalse hc => dE hc
 
 /- Auxiliary definitions for generating compact `noConfusion` for enumeration types -/
-abbrev noConfusionTypeEnum {α : Sort u} {β : Sort v} [DecidableEq β] (f : α → β) (P : Sort w) (x y : α) : Sort w :=
-  if f x = f y then P → P else P
+abbrev noConfusionTypeEnum {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f : α → β) (P : Sort w) (x y : α) : Sort w :=
+  Decidable.casesOn (motive := fun _ => Sort w) (inst (f x) (f y))
+    (fun _ => P)
+    (fun _ => P → P)
 
-abbrev noConfusionEnum {α : Sort u} {β : Sort v} [DecidableEq β] (f : α → β) {P : Sort w} {x y : α} (h : x = y) : noConfusionTypeEnum f P x y :=
-  if h' : f x = f y then
-    cast (@if_pos _ _ h' _ (P → P) (P)).symm (fun (h : P) => h)
-  else
-    False.elim (h' (congrArg f h))
+abbrev noConfusionEnum {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f : α → β) {P : Sort w} {x y : α} (h : x = y) : noConfusionTypeEnum f P x y :=
+  Decidable.casesOn
+    (motive := fun (inst : Decidable (f x = f y)) => Decidable.casesOn (motive := fun _ => Sort w) inst (fun _ => P) (fun _ => P → P))
+    (inst (f x) (f y))
+    (fun h' => False.elim (h' (congrArg f h)))
+    (fun h' => fun x => x)
 
 /- Inhabited -/