From b9b91407a3eedc42a7521e3f17a239e0e70b1f58 Mon Sep 17 00:00:00 2001
From: ChrisHughes24 <chrishughes24@gmail.com>
Date: Fri, 13 Jan 2023 11:38:13 +0000
Subject: [PATCH 01/19] chore(data/multiset/sort): make has_repr a meta
 instance to reduce imports

---
 src/data/finset/sort.lean   | 2 +-
 src/data/list/cycle.lean    | 2 +-
 src/data/multiset/sort.lean | 7 ++++---
 3 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/data/finset/sort.lean b/src/data/finset/sort.lean
index 1ced1d74ff4f2..c293a1d344bf9 100644
--- a/src/data/finset/sort.lean
+++ b/src/data/finset/sort.lean
@@ -211,6 +211,6 @@ by simp only [order_emb_of_card_le, rel_embedding.coe_trans, finset.order_emb_of
 
 end sort_linear_order
 
-instance [has_repr α] : has_repr (finset α) := ⟨λ s, repr s.1⟩
+meta instance [has_repr α] : has_repr (finset α) := ⟨λ s, repr s.1⟩
 
 end finset
diff --git a/src/data/list/cycle.lean b/src/data/list/cycle.lean
index 60dc82c3a7e7b..d282af2629920 100644
--- a/src/data/list/cycle.lean
+++ b/src/data/list/cycle.lean
@@ -732,7 +732,7 @@ via `#eval`, when over representatble types. For example, the cycle `(2 1 4 3)`
 as `c[1, 4, 3, 2]`. The representation of the cycle sorts the elements by the string value of the
 underlying element. This representation also supports cycles that can contain duplicates.
 -/
-instance [has_repr α] : has_repr (cycle α) :=
+meta instance [has_repr α] : has_repr (cycle α) :=
 ⟨λ s, "c[" ++ string.intercalate ", " ((s.map repr).lists.sort (≤)).head ++ "]"⟩
 
 /-- `chain R s` means that `R` holds between adjacent elements of `s`.
diff --git a/src/data/multiset/sort.lean b/src/data/multiset/sort.lean
index df8ecbe0d9e4b..dcff89148c65e 100644
--- a/src/data/multiset/sort.lean
+++ b/src/data/multiset/sort.lean
@@ -5,7 +5,6 @@ Authors: Mario Carneiro
 -/
 import data.list.sort
 import data.multiset.basic
-import data.string.basic
 
 /-!
 # Construct a sorted list from a multiset.
@@ -50,7 +49,9 @@ list.merge_sort_singleton r a
 
 end sort
 
-instance [has_repr α] : has_repr (multiset α) :=
-⟨λ s, "{" ++ string.intercalate ", " ((s.map repr).sort (≤)) ++ "}"⟩
+meta instance [has_repr α] : has_repr (multiset α) :=
+⟨λ s, "{" ++ string.intercalate ", "
+    (@multiset.sort string (λ s₁ s₂, s₁.to_list ≤ s₂.to_list)
+      undefined undefined undefined undefined (s.map repr) ) ++ "}"⟩
 
 end multiset

From 21bd006d314aea39d6cf8dd98694dbf297a77023 Mon Sep 17 00:00:00 2001
From: ChrisHughes24 <chrishughes24@gmail.com>
Date: Fri, 13 Jan 2023 11:40:23 +0000
Subject: [PATCH 02/19] fix build

---
 src/data/pnat/factors.lean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/data/pnat/factors.lean b/src/data/pnat/factors.lean
index 40fd6f53fc58c..9dc4a1a40959d 100644
--- a/src/data/pnat/factors.lean
+++ b/src/data/pnat/factors.lean
@@ -24,12 +24,15 @@ the multiplicity of `p` in this factors multiset being the p-adic valuation of `
 /-- The type of multisets of prime numbers.  Unique factorization
  gives an equivalence between this set and ℕ+, as we will formalize
  below. -/
- @[derive [inhabited, has_repr, canonically_ordered_add_monoid, distrib_lattice,
+ @[derive [inhabited, canonically_ordered_add_monoid, distrib_lattice,
   semilattice_sup, order_bot, has_sub, has_ordered_sub]]
 def prime_multiset := multiset nat.primes
 
 namespace prime_multiset
 
+meta instance : has_repr prime_multiset :=
+by delta prime_multiset; apply_instance
+
 /-- The multiset consisting of a single prime -/
 def of_prime (p : nat.primes) : prime_multiset := ({p} : multiset nat.primes)
 

From a41838434490f12783329e0b18d0604b21833327 Mon Sep 17 00:00:00 2001
From: ChrisHughes24 <chrishughes24@gmail.com>
Date: Fri, 13 Jan 2023 12:27:46 +0000
Subject: [PATCH 03/19] fix build

---
 src/data/list/cycle.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/data/list/cycle.lean b/src/data/list/cycle.lean
index d282af2629920..73c24e3f7f70e 100644
--- a/src/data/list/cycle.lean
+++ b/src/data/list/cycle.lean
@@ -733,7 +733,7 @@ as `c[1, 4, 3, 2]`. The representation of the cycle sorts the elements by the st
 underlying element. This representation also supports cycles that can contain duplicates.
 -/
 meta instance [has_repr α] : has_repr (cycle α) :=
-⟨λ s, "c[" ++ string.intercalate ", " ((s.map repr).lists.sort (≤)).head ++ "]"⟩
+⟨λ s, repr s.lists⟩
 
 /-- `chain R s` means that `R` holds between adjacent elements of `s`.
 

From e218fdd63cd45096f7156391867bbe549203eca2 Mon Sep 17 00:00:00 2001
From: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
Date: Fri, 13 Jan 2023 13:34:54 +0000
Subject: [PATCH 04/19] Update src/data/multiset/sort.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
---
 src/data/multiset/sort.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/data/multiset/sort.lean b/src/data/multiset/sort.lean
index dcff89148c65e..128356ced59d4 100644
--- a/src/data/multiset/sort.lean
+++ b/src/data/multiset/sort.lean
@@ -50,8 +50,6 @@ list.merge_sort_singleton r a
 end sort
 
 meta instance [has_repr α] : has_repr (multiset α) :=
-⟨λ s, "{" ++ string.intercalate ", "
-    (@multiset.sort string (λ s₁ s₂, s₁.to_list ≤ s₂.to_list)
-      undefined undefined undefined undefined (s.map repr) ) ++ "}"⟩
+⟨λ s, "{" ++ string.intercalate ", " (s.unquot.map repr) ++ "}"⟩
 
 end multiset

From 38a0506067a4e0586986d0558db1123637f6f7bd Mon Sep 17 00:00:00 2001
From: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
Date: Fri, 13 Jan 2023 13:35:02 +0000
Subject: [PATCH 05/19] Update src/data/pnat/factors.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
---
 src/data/pnat/factors.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/data/pnat/factors.lean b/src/data/pnat/factors.lean
index 9dc4a1a40959d..05cda33238916 100644
--- a/src/data/pnat/factors.lean
+++ b/src/data/pnat/factors.lean
@@ -30,6 +30,7 @@ def prime_multiset := multiset nat.primes
 
 namespace prime_multiset
 
+-- `derive` doesn't know to add `meta`
 meta instance : has_repr prime_multiset :=
 by delta prime_multiset; apply_instance
 

From 7b323f2f32ab7b86e0eb1a529ae0af8cb799e0e8 Mon Sep 17 00:00:00 2001
From: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
Date: Fri, 13 Jan 2023 13:35:11 +0000
Subject: [PATCH 06/19] Update src/data/pnat/factors.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
---
 src/data/pnat/factors.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/data/pnat/factors.lean b/src/data/pnat/factors.lean
index 05cda33238916..221d49df0c03a 100644
--- a/src/data/pnat/factors.lean
+++ b/src/data/pnat/factors.lean
@@ -24,7 +24,7 @@ the multiplicity of `p` in this factors multiset being the p-adic valuation of `
 /-- The type of multisets of prime numbers.  Unique factorization
  gives an equivalence between this set and ℕ+, as we will formalize
  below. -/
- @[derive [inhabited, canonically_ordered_add_monoid, distrib_lattice,
+@[derive [inhabited, canonically_ordered_add_monoid, distrib_lattice,
   semilattice_sup, order_bot, has_sub, has_ordered_sub]]
 def prime_multiset := multiset nat.primes
 

From 4c989286f8b8d896f1f41daa54730f45c99601a6 Mon Sep 17 00:00:00 2001
From: ChrisHughes24 <chrishughes24@gmail.com>
Date: Fri, 13 Jan 2023 14:13:00 +0000
Subject: [PATCH 07/19] make the instance non-meta again

---
 src/data/multiset/sort.lean | 15 ++++++++++++---
 1 file changed, 12 insertions(+), 3 deletions(-)

diff --git a/src/data/multiset/sort.lean b/src/data/multiset/sort.lean
index dcff89148c65e..ffd7bdd1e142c 100644
--- a/src/data/multiset/sort.lean
+++ b/src/data/multiset/sort.lean
@@ -49,9 +49,18 @@ list.merge_sort_singleton r a
 
 end sort
 
-meta instance [has_repr α] : has_repr (multiset α) :=
+instance [has_repr α] : has_repr (multiset α) :=
 ⟨λ s, "{" ++ string.intercalate ", "
-    (@multiset.sort string (λ s₁ s₂, s₁.to_list ≤ s₂.to_list)
-      undefined undefined undefined undefined (s.map repr) ) ++ "}"⟩
+    (@multiset.sort string (λ s₁ s₂, s₁.data.map char.val ≤ s₂.data.map char.val) _
+      ⟨λ a b c h₁ h₂, trans h₁ h₂⟩
+      ⟨λ a b h₁ h₂, begin
+        cases a, cases b,
+        dsimp at h₁ h₂,
+        rw [list.map_injective_iff.2 _ (le_antisymm h₁ h₂)],
+        rintros ⟨_, _⟩ ⟨_, _⟩ h,
+        simp at h, simp [h]
+      end⟩
+      ⟨λ a b, is_total.total _ _⟩
+      (s.map repr) ) ++ "}"⟩
 
 end multiset

From 60c1bd6ce128cb47da26b997c4637cc836611b55 Mon Sep 17 00:00:00 2001
From: ChrisHughes24 <chrishughes24@gmail.com>
Date: Fri, 13 Jan 2023 14:16:02 +0000
Subject: [PATCH 08/19] revert changes to other files

---
 src/data/finset/sort.lean  | 2 +-
 src/data/list/cycle.lean   | 4 ++--
 src/data/pnat/factors.lean | 6 +-----
 3 files changed, 4 insertions(+), 8 deletions(-)

diff --git a/src/data/finset/sort.lean b/src/data/finset/sort.lean
index c293a1d344bf9..1ced1d74ff4f2 100644
--- a/src/data/finset/sort.lean
+++ b/src/data/finset/sort.lean
@@ -211,6 +211,6 @@ by simp only [order_emb_of_card_le, rel_embedding.coe_trans, finset.order_emb_of
 
 end sort_linear_order
 
-meta instance [has_repr α] : has_repr (finset α) := ⟨λ s, repr s.1⟩
+instance [has_repr α] : has_repr (finset α) := ⟨λ s, repr s.1⟩
 
 end finset
diff --git a/src/data/list/cycle.lean b/src/data/list/cycle.lean
index 73c24e3f7f70e..60dc82c3a7e7b 100644
--- a/src/data/list/cycle.lean
+++ b/src/data/list/cycle.lean
@@ -732,8 +732,8 @@ via `#eval`, when over representatble types. For example, the cycle `(2 1 4 3)`
 as `c[1, 4, 3, 2]`. The representation of the cycle sorts the elements by the string value of the
 underlying element. This representation also supports cycles that can contain duplicates.
 -/
-meta instance [has_repr α] : has_repr (cycle α) :=
-⟨λ s, repr s.lists⟩
+instance [has_repr α] : has_repr (cycle α) :=
+⟨λ s, "c[" ++ string.intercalate ", " ((s.map repr).lists.sort (≤)).head ++ "]"⟩
 
 /-- `chain R s` means that `R` holds between adjacent elements of `s`.
 
diff --git a/src/data/pnat/factors.lean b/src/data/pnat/factors.lean
index 221d49df0c03a..40fd6f53fc58c 100644
--- a/src/data/pnat/factors.lean
+++ b/src/data/pnat/factors.lean
@@ -24,16 +24,12 @@ the multiplicity of `p` in this factors multiset being the p-adic valuation of `
 /-- The type of multisets of prime numbers.  Unique factorization
  gives an equivalence between this set and ℕ+, as we will formalize
  below. -/
-@[derive [inhabited, canonically_ordered_add_monoid, distrib_lattice,
+ @[derive [inhabited, has_repr, canonically_ordered_add_monoid, distrib_lattice,
   semilattice_sup, order_bot, has_sub, has_ordered_sub]]
 def prime_multiset := multiset nat.primes
 
 namespace prime_multiset
 
--- `derive` doesn't know to add `meta`
-meta instance : has_repr prime_multiset :=
-by delta prime_multiset; apply_instance
-
 /-- The multiset consisting of a single prime -/
 def of_prime (p : nat.primes) : prime_multiset := ({p} : multiset nat.primes)
 

From afb48c26cc695cc633f7418b45ca7b876872a95e Mon Sep 17 00:00:00 2001
From: ChrisHughes24 <chrishughes24@gmail.com>
Date: Fri, 13 Jan 2023 14:17:23 +0000
Subject: [PATCH 09/19] Revert "make the instance non-meta again"

This reverts commit 4c989286f8b8d896f1f41daa54730f45c99601a6.
---
 src/data/multiset/sort.lean | 15 +++------------
 1 file changed, 3 insertions(+), 12 deletions(-)

diff --git a/src/data/multiset/sort.lean b/src/data/multiset/sort.lean
index ffd7bdd1e142c..dcff89148c65e 100644
--- a/src/data/multiset/sort.lean
+++ b/src/data/multiset/sort.lean
@@ -49,18 +49,9 @@ list.merge_sort_singleton r a
 
 end sort
 
-instance [has_repr α] : has_repr (multiset α) :=
+meta instance [has_repr α] : has_repr (multiset α) :=
 ⟨λ s, "{" ++ string.intercalate ", "
-    (@multiset.sort string (λ s₁ s₂, s₁.data.map char.val ≤ s₂.data.map char.val) _
-      ⟨λ a b c h₁ h₂, trans h₁ h₂⟩
-      ⟨λ a b h₁ h₂, begin
-        cases a, cases b,
-        dsimp at h₁ h₂,
-        rw [list.map_injective_iff.2 _ (le_antisymm h₁ h₂)],
-        rintros ⟨_, _⟩ ⟨_, _⟩ h,
-        simp at h, simp [h]
-      end⟩
-      ⟨λ a b, is_total.total _ _⟩
-      (s.map repr) ) ++ "}"⟩
+    (@multiset.sort string (λ s₁ s₂, s₁.to_list ≤ s₂.to_list)
+      undefined undefined undefined undefined (s.map repr) ) ++ "}"⟩
 
 end multiset

From 1c303e18129e5a95cf477b0f0abca8021553861c Mon Sep 17 00:00:00 2001
From: ChrisHughes24 <chrishughes24@gmail.com>
Date: Fri, 13 Jan 2023 14:18:35 +0000
Subject: [PATCH 10/19] meta instance

---
 src/data/multiset/sort.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/data/multiset/sort.lean b/src/data/multiset/sort.lean
index dcff89148c65e..128356ced59d4 100644
--- a/src/data/multiset/sort.lean
+++ b/src/data/multiset/sort.lean
@@ -50,8 +50,6 @@ list.merge_sort_singleton r a
 end sort
 
 meta instance [has_repr α] : has_repr (multiset α) :=
-⟨λ s, "{" ++ string.intercalate ", "
-    (@multiset.sort string (λ s₁ s₂, s₁.to_list ≤ s₂.to_list)
-      undefined undefined undefined undefined (s.map repr) ) ++ "}"⟩
+⟨λ s, "{" ++ string.intercalate ", " (s.unquot.map repr) ++ "}"⟩
 
 end multiset

From 2c8201ff7abd0fa30ab11200f4bfaa5c927f134a Mon Sep 17 00:00:00 2001
From: ChrisHughes24 <chrishughes24@gmail.com>
Date: Fri, 13 Jan 2023 14:19:31 +0000
Subject: [PATCH 11/19] make finset instance meta

---
 src/data/finset/sort.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/data/finset/sort.lean b/src/data/finset/sort.lean
index 1ced1d74ff4f2..c293a1d344bf9 100644
--- a/src/data/finset/sort.lean
+++ b/src/data/finset/sort.lean
@@ -211,6 +211,6 @@ by simp only [order_emb_of_card_le, rel_embedding.coe_trans, finset.order_emb_of
 
 end sort_linear_order
 
-instance [has_repr α] : has_repr (finset α) := ⟨λ s, repr s.1⟩
+meta instance [has_repr α] : has_repr (finset α) := ⟨λ s, repr s.1⟩
 
 end finset

From f0ef658c243bc3fdb9e403b1e7d7b15d906901b1 Mon Sep 17 00:00:00 2001
From: ChrisHughes24 <chrishughes24@gmail.com>
Date: Fri, 13 Jan 2023 14:21:02 +0000
Subject: [PATCH 12/19] fix factors

---
 src/data/pnat/factors.lean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/data/pnat/factors.lean b/src/data/pnat/factors.lean
index 40fd6f53fc58c..6854ad6ed5f6d 100644
--- a/src/data/pnat/factors.lean
+++ b/src/data/pnat/factors.lean
@@ -24,12 +24,15 @@ the multiplicity of `p` in this factors multiset being the p-adic valuation of `
 /-- The type of multisets of prime numbers.  Unique factorization
  gives an equivalence between this set and ℕ+, as we will formalize
  below. -/
- @[derive [inhabited, has_repr, canonically_ordered_add_monoid, distrib_lattice,
+ @[derive [inhabited, canonically_ordered_add_monoid, distrib_lattice,
   semilattice_sup, order_bot, has_sub, has_ordered_sub]]
 def prime_multiset := multiset nat.primes
 
 namespace prime_multiset
 
+-- `@[derive]` doesn't work for `meta` instances
+meta instance : has_repr prime_multiset := by delta prime_multiset; apply_instance
+
 /-- The multiset consisting of a single prime -/
 def of_prime (p : nat.primes) : prime_multiset := ({p} : multiset nat.primes)
 

From a1f4b21abfca56ea7197ccd34d0fccb9d6f0d24d Mon Sep 17 00:00:00 2001
From: ChrisHughes24 <chrishughes24@gmail.com>
Date: Fri, 13 Jan 2023 14:25:12 +0000
Subject: [PATCH 13/19] fix `cycle.lean`

---
 src/data/list/cycle.lean | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/data/list/cycle.lean b/src/data/list/cycle.lean
index 60dc82c3a7e7b..8cfba07a9c6a6 100644
--- a/src/data/list/cycle.lean
+++ b/src/data/list/cycle.lean
@@ -17,8 +17,8 @@ Based on this, we define the quotient of lists by the rotation relation, called
 
 We also define a representation of concrete cycles, available when viewing them in a goal state or
 via `#eval`, when over representatble types. For example, the cycle `(2 1 4 3)` will be shown
-as `c[1, 4, 3, 2]`. The representation of the cycle sorts the elements by the string value of the
-underlying element. This representation also supports cycles that can contain duplicates.
+as `c[2, 1, 4, 3]`. Two equal cycles may be printed differently if their internal representation
+is different.
 
 -/
 
@@ -728,12 +728,12 @@ end decidable
 
 /--
 We define a representation of concrete cycles, available when viewing them in a goal state or
-via `#eval`, when over representatble types. For example, the cycle `(2 1 4 3)` will be shown
-as `c[1, 4, 3, 2]`. The representation of the cycle sorts the elements by the string value of the
-underlying element. This representation also supports cycles that can contain duplicates.
+via `#eval`, when over representable types. For example, the cycle `(2 1 4 3)` will be shown
+as `c[2, 1, 4, 3]`. Two equal cycles may be printed differently if their internal representation
+is different.
 -/
-instance [has_repr α] : has_repr (cycle α) :=
-⟨λ s, "c[" ++ string.intercalate ", " ((s.map repr).lists.sort (≤)).head ++ "]"⟩
+meta instance [has_repr α] : has_repr (cycle α) :=
+⟨λ s, "c[" ++ string.intercalate ", " ((s.map repr).lists.unquot).head ++ "]"⟩
 
 /-- `chain R s` means that `R` holds between adjacent elements of `s`.
 

From f9ada7d67fa02fb745ed69f2fb65c7836f784f23 Mon Sep 17 00:00:00 2001
From: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
Date: Fri, 13 Jan 2023 14:39:33 +0000
Subject: [PATCH 14/19] Update src/data/multiset/sort.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
---
 src/data/multiset/sort.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/data/multiset/sort.lean b/src/data/multiset/sort.lean
index 128356ced59d4..648d975765165 100644
--- a/src/data/multiset/sort.lean
+++ b/src/data/multiset/sort.lean
@@ -49,6 +49,7 @@ list.merge_sort_singleton r a
 
 end sort
 
+-- TODO: use a sort order if available, gh-18166
 meta instance [has_repr α] : has_repr (multiset α) :=
 ⟨λ s, "{" ++ string.intercalate ", " (s.unquot.map repr) ++ "}"⟩
 

From 7ad390b4b7f6cd32b007b4f3052412e80bd2c91e Mon Sep 17 00:00:00 2001
From: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
Date: Fri, 13 Jan 2023 15:11:05 +0000
Subject: [PATCH 15/19] Update src/data/pnat/factors.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
---
 src/data/pnat/factors.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/data/pnat/factors.lean b/src/data/pnat/factors.lean
index 6854ad6ed5f6d..f49517117765b 100644
--- a/src/data/pnat/factors.lean
+++ b/src/data/pnat/factors.lean
@@ -24,7 +24,7 @@ the multiplicity of `p` in this factors multiset being the p-adic valuation of `
 /-- The type of multisets of prime numbers.  Unique factorization
  gives an equivalence between this set and ℕ+, as we will formalize
  below. -/
- @[derive [inhabited, canonically_ordered_add_monoid, distrib_lattice,
+@[derive [inhabited, canonically_ordered_add_monoid, distrib_lattice,
   semilattice_sup, order_bot, has_sub, has_ordered_sub]]
 def prime_multiset := multiset nat.primes
 

From 21358ee0e600949df160814e9bb37cf1f55894e3 Mon Sep 17 00:00:00 2001
From: ChrisHughes24 <chrishughes24@gmail.com>
Date: Fri, 13 Jan 2023 17:29:40 +0000
Subject: [PATCH 16/19] fix

---
 src/group_theory/perm/cycle/concrete.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/group_theory/perm/cycle/concrete.lean b/src/group_theory/perm/cycle/concrete.lean
index 03a7eb22a2180..d52b8721d9ebc 100644
--- a/src/group_theory/perm/cycle/concrete.lean
+++ b/src/group_theory/perm/cycle/concrete.lean
@@ -537,7 +537,7 @@ def iso_cycle' : {f : perm α // is_cycle f} ≃ {s : cycle α // s.nodup ∧ s.
 notation `c[` l:(foldr `, ` (h t, list.cons h t) list.nil `]`) :=
   cycle.form_perm ↑l (cycle.nodup_coe_iff.mpr dec_trivial)
 
-instance repr_perm [has_repr α] : has_repr (perm α) :=
+meta instance repr_perm [has_repr α] : has_repr (perm α) :=
 ⟨λ f, repr (multiset.pmap (λ (g : perm α) (hg : g.is_cycle),
   iso_cycle ⟨g, hg⟩) -- to_cycle is faster?
   (perm.cycle_factors_finset f).val

From 05db679ebd1844d9af8d44e78dc8ccff60f5fba4 Mon Sep 17 00:00:00 2001
From: ChrisHughes24 <chrishughes24@gmail.com>
Date: Fri, 13 Jan 2023 17:45:15 +0000
Subject: [PATCH 17/19] fix test

---
 test/cycle.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/test/cycle.lean b/test/cycle.lean
index 90b5222aa9fb7..ca87123f2a5f4 100644
--- a/test/cycle.lean
+++ b/test/cycle.lean
@@ -1,5 +1,5 @@
 import data.list.cycle
 
 run_cmd guard ("c[1, 4, 3, 2]" = repr (↑[1, 4, 3, 2] : cycle ℕ))
-run_cmd guard ("c[1, 4, 3, 2]" = repr (↑[2, 1, 4, 3] : cycle ℕ))
-run_cmd guard ("c[-1, 2, 1, 4]" = repr (↑[(2 : ℤ), 1, 4, -1] : cycle ℤ))
+run_cmd guard ("c[1, 4, 3, 2]" = repr (↑[1, 4, 3, 2] : cycle ℕ))
+run_cmd guard ("c[-1, 2, 1, 4]" = repr ([(-1 : ℤ), 2, 1, 4] : cycle ℤ))

From a41d5730b2cf96bb80639f34e1ecb83d5c3a4280 Mon Sep 17 00:00:00 2001
From: ChrisHughes24 <chrishughes24@gmail.com>
Date: Fri, 13 Jan 2023 17:50:40 +0000
Subject: [PATCH 18/19] adjut test

---
 test/cycle.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/test/cycle.lean b/test/cycle.lean
index ca87123f2a5f4..c90e8354cd945 100644
--- a/test/cycle.lean
+++ b/test/cycle.lean
@@ -1,5 +1,5 @@
 import data.list.cycle
 
 run_cmd guard ("c[1, 4, 3, 2]" = repr (↑[1, 4, 3, 2] : cycle ℕ))
-run_cmd guard ("c[1, 4, 3, 2]" = repr (↑[1, 4, 3, 2] : cycle ℕ))
-run_cmd guard ("c[-1, 2, 1, 4]" = repr ([(-1 : ℤ), 2, 1, 4] : cycle ℤ))
+run_cmd guard ("c[2, 1, 4, -1]" = repr (↑[(2 : ℤ), 1, 4, -1] : cycle ℤ))
+run_cmd guard ("c[2, 1, 4, -1]" = repr (↑[(2 : ℤ), 1, 4, -1] : cycle ℤ))

From c221d9e351bef56d3817b5db0a997d3466cf1ba1 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Fri, 13 Jan 2023 18:41:42 +0000
Subject: [PATCH 19/19] Update test/cycle.lean

---
 test/cycle.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/cycle.lean b/test/cycle.lean
index c90e8354cd945..bc3424ef5b4bb 100644
--- a/test/cycle.lean
+++ b/test/cycle.lean
@@ -1,5 +1,5 @@
 import data.list.cycle
 
 run_cmd guard ("c[1, 4, 3, 2]" = repr (↑[1, 4, 3, 2] : cycle ℕ))
-run_cmd guard ("c[2, 1, 4, -1]" = repr (↑[(2 : ℤ), 1, 4, -1] : cycle ℤ))
+run_cmd guard ("c[2, 1, 4, 3]" = repr (↑[2, 1, 4, 3] : cycle ℕ))
 run_cmd guard ("c[2, 1, 4, -1]" = repr (↑[(2 : ℤ), 1, 4, -1] : cycle ℤ))