remove

mattrobball · mattrobball · commit 42aaec225ea7 · 2025-01-23T11:39:04.000-05:00
diff --git a/Mathlib/Algebra/Order/Interval/Set/Instances.lean b/Mathlib/Algebra/Order/Interval/Set/Instances.lean
@@ -126,15 +126,11 @@ instance commMonoidWithZero {α : Type*} [OrderedCommSemiring α] :
     CommMonoidWithZero (Icc (0 : α) 1) := fast_instance%
   Subtype.coe_injective.commMonoidWithZero _ coe_zero coe_one coe_mul coe_pow
 
-/-- error: (kernel) declaration has metavariables 'Set.Icc.cancelMonoidWithZero' -/
-#guard_msgs in
 instance cancelMonoidWithZero {α : Type*} [OrderedRing α] [NoZeroDivisors α] :
     CancelMonoidWithZero (Icc (0 : α) 1) := fast_instance%
   @Function.Injective.cancelMonoidWithZero α _ NoZeroDivisors.toCancelMonoidWithZero _ _ _ _
     (fun v => v.val) Subtype.coe_injective coe_zero coe_one coe_mul coe_pow
 
-/-- error: (kernel) declaration has metavariables 'Set.Icc.cancelCommMonoidWithZero' -/
-#guard_msgs in
 instance cancelCommMonoidWithZero {α : Type*} [OrderedCommRing α] [NoZeroDivisors α] :
     CancelCommMonoidWithZero (Icc (0 : α) 1) := fast_instance%
   @Function.Injective.cancelCommMonoidWithZero α _ NoZeroDivisors.toCancelCommMonoidWithZero _ _ _ _
diff --git a/Mathlib/Algebra/Order/Nonneg/Ring.lean b/Mathlib/Algebra/Order/Nonneg/Ring.lean
@@ -69,8 +69,6 @@ instance orderedSemiring [OrderedSemiring α] : OrderedSemiring { x : α // 0 
     (fun _ _ => rfl) (fun _ _=> rfl) (fun _ _ => rfl)
     (fun _ _ => rfl) fun _ => rfl
 
-/-- error: unknown free variable '_fvar.19139' -/
-#guard_msgs in
 instance strictOrderedSemiring [StrictOrderedSemiring α] :
     StrictOrderedSemiring { x : α // 0 ≤ x } := fast_instance%
   Subtype.coe_injective.strictOrderedSemiring _ Nonneg.coe_zero Nonneg.coe_one
@@ -86,8 +84,6 @@ instance orderedCommSemiring [OrderedCommSemiring α] :
 instance orderedCommMonoid [OrderedCommSemiring α] : OrderedCommMonoid { x : α // 0 ≤ x } where
   mul_le_mul_left a _ h c := mul_le_mul le_rfl h a.prop c.prop
 
-/-- error: unknown free variable '_fvar.29853' -/
-#guard_msgs in
 instance strictOrderedCommSemiring [StrictOrderedCommSemiring α] :
     StrictOrderedCommSemiring { x : α // 0 ≤ x } := fast_instance%
   Subtype.coe_injective.strictOrderedCommSemiring _ Nonneg.coe_zero Nonneg.coe_one
