From f1a0918b3f73d847b5dffe1617ed931feff5c25e Mon Sep 17 00:00:00 2001
From: Jonathan Chan <jonathanhwchan@gmail.com>
Date: Wed, 19 Aug 2026 20:44:53 -0400
Subject: [PATCH 1/4] Missing superscripts and subscripts

---
 lean4-unicode-input/src/abbreviations.json | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/lean4-unicode-input/src/abbreviations.json b/lean4-unicode-input/src/abbreviations.json
index cce6fb21..902bb1e5 100644
--- a/lean4-unicode-input/src/abbreviations.json
+++ b/lean4-unicode-input/src/abbreviations.json
@@ -1252,8 +1252,10 @@
     "^z": "ᶻ",
     "^A": "ᴬ",
     "^B": "ᴮ",
+    "^C": "ꟲ",
     "^D": "ᴰ",
     "^E": "ᴱ",
+    "^F": "ꟳ",
     "^G": "ᴳ",
     "^H": "ᴴ",
     "^I": "ᴵ",
@@ -1264,7 +1266,9 @@
     "^N": "ᴺ",
     "^O": "ᴼ",
     "^P": "ᴾ",
+    "^Q": "ꟴ",
     "^R": "ᴿ",
+    "^S": "꟱",
     "^T": "ᵀ",
     "^U": "ᵁ",
     "^V": "ⱽ",
@@ -1360,6 +1364,7 @@
     "^TEL": "℡",
     "^TM": "™",
     "_a": "ₐ",
+    "_c": "𞁞",
     "_e": "ₑ",
     "_h": "ₕ",
     "_i": "ᵢ",

From 098a9109a2b20bbf02bfd2bc3bb1228900ef0bcc Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <13901751+Vtec234@users.noreply.github.com>
Date: Tue, 29 Sep 2026 13:56:03 -0400
Subject: [PATCH 2/4] Update lean4-unicode-input/src/abbreviations.json

---
 lean4-unicode-input/src/abbreviations.json | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/lean4-unicode-input/src/abbreviations.json b/lean4-unicode-input/src/abbreviations.json
index 902bb1e5..f251ac87 100644
--- a/lean4-unicode-input/src/abbreviations.json
+++ b/lean4-unicode-input/src/abbreviations.json
@@ -1380,7 +1380,11 @@
     "_t": "ₜ",
     "_u": "ᵤ",
     "_v": "ᵥ",
-    "_x": "ₓ",
+"_v": "ᵥ",
+"_w": "₝",
+"_x": "ₓ",
+"_y": "₞",
+"_z": "₟",
     "_0": "₀",
     "_1": "₁",
     "_2": "₂",

From 8a9291f8d0721c31061b35f34fbda0894e65e6c5 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <13901751+Vtec234@users.noreply.github.com>
Date: Tue, 29 Sep 2026 13:57:44 -0400
Subject: [PATCH 3/4] Apply suggestion from @Vtec234

---
 lean4-unicode-input/src/abbreviations.json | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/lean4-unicode-input/src/abbreviations.json b/lean4-unicode-input/src/abbreviations.json
index f251ac87..1b9573fd 100644
--- a/lean4-unicode-input/src/abbreviations.json
+++ b/lean4-unicode-input/src/abbreviations.json
@@ -1380,11 +1380,11 @@
     "_t": "ₜ",
     "_u": "ᵤ",
     "_v": "ᵥ",
-"_v": "ᵥ",
-"_w": "₝",
-"_x": "ₓ",
-"_y": "₞",
-"_z": "₟",
+    "_v": "ᵥ",
+    "_w": "₝",
+    "_x": "ₓ",
+    "_y": "₞",
+    "_z": "₟",
     "_0": "₀",
     "_1": "₁",
     "_2": "₂",

From 654e417b6e441326a6b5d338585400987fec016a Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <13901751+Vtec234@users.noreply.github.com>
Date: Tue, 29 Sep 2026 13:58:11 -0400
Subject: [PATCH 4/4] Apply suggestion from @Vtec234

---
 lean4-unicode-input/src/abbreviations.json | 1 -
 1 file changed, 1 deletion(-)

diff --git a/lean4-unicode-input/src/abbreviations.json b/lean4-unicode-input/src/abbreviations.json
index 1b9573fd..7318c16e 100644
--- a/lean4-unicode-input/src/abbreviations.json
+++ b/lean4-unicode-input/src/abbreviations.json
@@ -1380,7 +1380,6 @@
     "_t": "ₜ",
     "_u": "ᵤ",
     "_v": "ᵥ",
-    "_v": "ᵥ",
     "_w": "₝",
     "_x": "ₓ",
     "_y": "₞",