From aea33324401c7df0cd166942cd7d723cb45ae6cb Mon Sep 17 00:00:00 2001
From: Vasilii Nesterov <vas.nesterov63@gmail.com>
Date: Mon, 13 Oct 2025 18:51:41 +0300
Subject: [PATCH] remove second type

---
 MathlibTest/order.lean | 10 ++--------
 1 file changed, 2 insertions(+), 8 deletions(-)

diff --git a/MathlibTest/order.lean b/MathlibTest/order.lean
index 07753ca1c74493..4ebb597d9e6f0c 100644
--- a/MathlibTest/order.lean
+++ b/MathlibTest/order.lean
@@ -87,13 +87,7 @@ error: No contradiction found.
 
 Additional diagnostic information may be available using the `set_option trace.order true` command.
 ---
-trace: [order] Working on type ℕ (linear order)
-[order] Collected atoms:
-    #0 := x
-    #1 := y
-[order] Collected facts:
-    #0 ≠ #1
-    #0 ≤ #1
+trace:
 [order] Working on type α (partial order)
 [order] Collected atoms:
     #0 := a ⊓ (b ⊔ c)
@@ -124,7 +118,7 @@ trace: [order] Working on type ℕ (linear order)
     ¬ #0 < #5
 -/
 #guard_msgs in
-example (a b c : α) (x y : Nat) (h : x < y) [Lattice α] : a ⊓ (b ⊔ c) ≤ (a ⊓ b) ⊔ (a ⊓ c) := by
+example (a b c : α) [Lattice α] : a ⊓ (b ⊔ c) ≤ (a ⊓ b) ⊔ (a ⊓ c) := by
   order
 
 -- This used to work when a different matching strategy was used in `order`.