From 531fac50d41bfcc634c8c042cb039a4d969fd72c Mon Sep 17 00:00:00 2001
From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Wed, 4 Jan 2023 21:53:10 +0100
Subject: [PATCH] chore: remove references to fixed lean bug

Followup to #1335.
---
 Mathlib/Order/Antichain.lean | 1 -
 Mathlib/Order/Chain.lean     | 1 -
 Mathlib/Order/Zorn.lean      | 1 -
 3 files changed, 3 deletions(-)

diff --git a/Mathlib/Order/Antichain.lean b/Mathlib/Order/Antichain.lean
index c838dc79907a0..a455b6b50165b 100644
--- a/Mathlib/Order/Antichain.lean
+++ b/Mathlib/Order/Antichain.lean
@@ -336,7 +336,6 @@ variable {ι : Type _} {α : ι → Type _} [∀ i, Preorder (α i)] {s t : Set
   {a b c : ∀ i, α i}
 
 
--- Porting note: local notation given a name because of https://github.com/leanprover/lean4/issues/2000
 @[inherit_doc]
 local infixl:50 " ≺ " => StrongLT
 
diff --git a/Mathlib/Order/Chain.lean b/Mathlib/Order/Chain.lean
index 9745d5ca24576..b457f680f3536 100644
--- a/Mathlib/Order/Chain.lean
+++ b/Mathlib/Order/Chain.lean
@@ -44,7 +44,6 @@ section Chain
 variable (r : α → α → Prop)
 
 /-- In this file, we use `≺` as a local notation for any relation `r`. -/
--- Porting note: local notation given a name because of https://github.com/leanprover/lean4/issues/2000
 local infixl:50 " ≺ " => r
 
 /-- A chain is a set `s` satisfying `x ≺ y ∨ x = y ∨ y ≺ x` for all `x y ∈ s`. -/
diff --git a/Mathlib/Order/Zorn.lean b/Mathlib/Order/Zorn.lean
index 97c350d112703..8e4e8e5c83f21 100644
--- a/Mathlib/Order/Zorn.lean
+++ b/Mathlib/Order/Zorn.lean
@@ -71,7 +71,6 @@ open Classical Set
 variable {α β : Type _} {r : α → α → Prop} {c : Set α}
 
 /-- Local notation for the relation being considered. -/
--- Porting note: local notation given a name because of https://github.com/leanprover/lean4/issues/2000
 local infixl:50 " ≺ " => r
 
 /-- **Zorn's lemma**