From dceaab485b537ee518d4a455024f6fe32312ceae Mon Sep 17 00:00:00 2001
From: qawbecrdtey <qawbecrdtey@kaist.ac.kr>
Date: Sat, 14 Jan 2023 06:58:23 +0000
Subject: [PATCH] feat: port Data.Rat.Encodable (#1569)

---
 Mathlib.lean                    |  1 +
 Mathlib/Data/Rat/Encodable.lean | 31 +++++++++++++++++++++++++++++++
 2 files changed, 32 insertions(+)
 create mode 100644 Mathlib/Data/Rat/Encodable.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 88c9d6e9e08fe..a997a1006dced 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -355,6 +355,7 @@ import Mathlib.Data.Quot
 import Mathlib.Data.Rat.Basic
 import Mathlib.Data.Rat.Cast
 import Mathlib.Data.Rat.Defs
+import Mathlib.Data.Rat.Encodable
 import Mathlib.Data.Rat.Floor
 import Mathlib.Data.Rat.Init
 import Mathlib.Data.Rat.Lemmas
diff --git a/Mathlib/Data/Rat/Encodable.lean b/Mathlib/Data/Rat/Encodable.lean
new file mode 100644
index 0000000000000..44342fd0bd8b8
--- /dev/null
+++ b/Mathlib/Data/Rat/Encodable.lean
@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2019 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Mario Carneiro
+
+! This file was ported from Lean 3 source module data.rat.encodable
+! leanprover-community/mathlib commit 9003f28797c0664a49e4179487267c494477d853
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Logic.Encodable.Basic
+import Mathlib.Data.Nat.GCD.Basic
+import Mathlib.Data.Rat.Init
+
+/-! # The rationals are `Encodable`.
+
+As a consequence we also get the instance `Countable ℚ`.
+
+This is kept separate from `Data.Rat.Defs` in order to minimize imports.
+-/
+
+
+namespace Rat
+
+instance : Encodable ℚ :=
+  Encodable.ofEquiv (Σn : ℤ, { d : ℕ // 0 < d ∧ n.natAbs.coprime d })
+    ⟨fun ⟨a, b, c, d⟩ => ⟨a, b, Nat.pos_of_ne_zero c, d⟩,
+      fun ⟨a, b, c, d⟩ => ⟨a, b, Nat.pos_iff_ne_zero.mp c, d⟩,
+      fun _ => rfl, fun ⟨_, _, _, _⟩ => rfl⟩
+
+end Rat