fix stage2

Author: leodemoura

src/Init/Data/Fin/Lemmas.lean

@@ -118,7 +118,7 @@ For example, for `x : Fin k` and `n : Nat`,
 it causes `x < n` to be elaborated as `x < ↑n` rather than `↑x < n`,
 silently introducing wraparound arithmetic.
 -/
-@[expose]
+@[expose, instance_reducible]
 def instNatCast (n : Nat) [NeZero n] : NatCast (Fin n) where
   natCast a := Fin.ofNat n a
 
@@ -140,7 +140,7 @@ This is not a global instance, but may be activated locally via `open Fin.IntCas
 
 See the doc-string for `Fin.NatCast.instNatCast` for more details.
 -/
-@[expose]
+@[expose, instance_reducible]
 def instIntCast (n : Nat) [NeZero n] : IntCast (Fin n) where
   intCast := Fin.intCast
 

src/Init/Data/Ord/Basic.lean

@@ -616,14 +616,14 @@ end List
 Constructs an `BEq` instance from an `Ord` instance that asserts that the result of `compare` is
 `Ordering.eq`.
 -/
-@[expose] def beqOfOrd [Ord α] : BEq α where
+@[expose, instance_reducible] def beqOfOrd [Ord α] : BEq α where
   beq a b := (compare a b).isEq
 
 /--
 Constructs an `LT` instance from an `Ord` instance that asserts that the result of `compare` is
 `Ordering.lt`.
 -/
-@[expose] def ltOfOrd [Ord α] : LT α where
+@[expose, instance_reducible] def ltOfOrd [Ord α] : LT α where
   lt a b := compare a b = Ordering.lt
 
 @[inline]

src/Init/Data/Order/FactoriesExtra.lean

@@ -82,7 +82,7 @@ public def _root_.DecidableLT.ofOrd (α : Type u) [LE α] [LT α] [Ord α] [Lawf
 
 /--
 Creates a `BEq α` instance from an `Ord α` instance. -/
-@[inline, expose]
+@[inline, expose, instance_reducible]
 public def _root_.BEq.ofOrd (α : Type u) [Ord α] :
     BEq α where
   beq a b := compare a b = .eq

src/Init/Data/UInt/Basic.lean

@@ -373,7 +373,7 @@ Examples:
  * `(if (5 : UInt16) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : UInt16) < 7) by decide`
 -/
-@[extern "lean_uint16_dec_lt"]
+@[extern "lean_uint16_dec_lt", instance_reducible]
 def UInt16.decLt (a b : UInt16) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
 
@@ -390,7 +390,7 @@ Examples:
  * `(if (5 : UInt16) ≤ 15 then "yes" else "no") = "yes"`
  * `show (7 : UInt16) ≤ 7 by decide`
 -/
-@[extern "lean_uint16_dec_le"]
+@[extern "lean_uint16_dec_le", instance_reducible]
 def UInt16.decLe (a b : UInt16) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
 
@@ -737,7 +737,7 @@ Examples:
  * `(if (5 : UInt64) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : UInt64) < 7) by decide`
 -/
-@[extern "lean_uint64_dec_lt"]
+@[extern "lean_uint64_dec_lt", instance_reducible]
 def UInt64.decLt (a b : UInt64) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
 
@@ -753,7 +753,7 @@ Examples:
  * `(if (5 : UInt64) ≤ 15 then "yes" else "no") = "yes"`
  * `show (7 : UInt64) ≤ 7 by decide`
 -/
-@[extern "lean_uint64_dec_le"]
+@[extern "lean_uint64_dec_le", instance_reducible]
 def UInt64.decLe (a b : UInt64) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))