From 580e5e44ec83f44d8e8bc7e0530f951ae5ef6ed8 Mon Sep 17 00:00:00 2001
From: Li Xuanji <xuanji@gmail.com>
Date: Sat, 5 Apr 2025 17:16:59 -0400
Subject: [PATCH 1/3] Add rules

---
 LeanTeXMathlib/Basic.lean | 39 ++++++++++++++++++++++++++++++++++++++-
 test/basic.lean           | 25 +++++++++++++++++++++++++
 2 files changed, 63 insertions(+), 1 deletion(-)

diff --git a/LeanTeXMathlib/Basic.lean b/LeanTeXMathlib/Basic.lean
index c9849ba..b412d80 100644
--- a/LeanTeXMathlib/Basic.lean
+++ b/LeanTeXMathlib/Basic.lean
@@ -126,6 +126,44 @@ latex_pp_app_rules (const := Finset.Ioi)
     let lo ← latexPP lo
     return "(" ++ lo ++ ", \\infty)" |>.resetBP .Infinity .Infinity
 
+latex_pp_app_rules (const := Set.Icc)
+  | _, #[_, _, lo, hi] => do
+    let lo ← latexPP lo
+    let hi ← latexPP hi
+    return "[" ++ lo ++ ", " ++ hi ++ "]" |>.resetBP .Infinity .Infinity
+latex_pp_app_rules (const := Set.Ico)
+  | _, #[_, _, lo, hi] => do
+    let lo ← latexPP lo
+    let hi ← latexPP hi
+    return "[" ++ lo ++ ", " ++ hi ++ ")" |>.resetBP .Infinity .Infinity
+latex_pp_app_rules (const := Set.Ioc)
+  | _, #[_, _, lo, hi] => do
+    let lo ← latexPP lo
+    let hi ← latexPP hi
+    return "(" ++ lo ++ ", " ++ hi ++ "]" |>.resetBP .Infinity .Infinity
+latex_pp_app_rules (const := Set.Ioo)
+  | _, #[_, _, lo, hi] => do
+    let lo ← latexPP lo
+    let hi ← latexPP hi
+    return "(" ++ lo ++ ", " ++ hi ++ ")" |>.resetBP .Infinity .Infinity
+
+latex_pp_app_rules (const := Set.Iio)
+  | _, #[_, _, hi] => do
+    let hi ← latexPP hi
+    return "(-\\infty, " ++ hi ++ ")" |>.resetBP .Infinity .Infinity
+latex_pp_app_rules (const := Set.Iic)
+  | _, #[_, _, lo] => do
+    let lo ← latexPP lo
+    return "(-\\infty, " ++ lo ++ "]" |>.resetBP .Infinity .Infinity
+latex_pp_app_rules (const := Set.Ici)
+  | _, #[_, _, lo] => do
+    let lo ← latexPP lo
+    return "[" ++ lo ++ ", \\infty)" |>.resetBP .Infinity .Infinity
+latex_pp_app_rules (const := Set.Ioi)
+  | _, #[_, _, lo] => do
+    let lo ← latexPP lo
+    return "(" ++ lo ++ ", \\infty)" |>.resetBP .Infinity .Infinity
+
 latex_pp_app_rules (const := Finset.range)
   | _, #[hi] => do
     let hi ← latexPP hi
@@ -181,4 +219,3 @@ latex_pp_app_rules (const := PiTensorProduct)
       let pbody ← latexPP body
       let psum := (← (LatexData.atomString "\\bigotimes" |>.bigger 1).sub (s!"{name.toLatex} \\in " ++ pι) |>.maybeWithTooltip "PiTensorProduct") ++ pbody
       return psum |>.resetBP (rbp := .NonAssoc 0)
-
diff --git a/test/basic.lean b/test/basic.lean
index 67990dc..6deaa36 100644
--- a/test/basic.lean
+++ b/test/basic.lean
@@ -60,6 +60,31 @@ latex_pp_app_rules (kind := any) (paramKinds := params)
 
 #texify Real.arcsin (Real.cos 2)
 
+
+/-- info: (0, \frac{\pi}{2}) -/
+#guard_msgs in #latex Set.Ioo 0 (Real.pi / 2)
+
+/-- info: [0, \frac{\pi}{2}) -/
+#guard_msgs in #latex Set.Ico 0 (Real.pi / 2)
+
+/-- info: (0, \frac{\pi}{2}] -/
+#guard_msgs in #latex Set.Ioc 0 (Real.pi / 2)
+
+/-- info: [0, \frac{\pi}{2}] -/
+#guard_msgs in #latex Set.Icc 0 (Real.pi / 2)
+
+/-- info: (-\infty, 5) -/
+#guard_msgs in #latex Set.Iio 5
+
+/-- info: (-\infty, 5] -/
+#guard_msgs in #latex Set.Iic 5
+
+/-- info: [5, \infty) -/
+#guard_msgs in #latex Set.Ici 5
+
+/-- info: (5, \infty) -/
+#guard_msgs in #latex Set.Ioi 5
+
 open scoped DirectSum
 
 #texify ⨁ i, (Fin i → ℝ)

From eb31a8352523fb944c3ef19fd1b38ff918c255a4 Mon Sep 17 00:00:00 2001
From: Li Xuanji <xuanji@gmail.com>
Date: Sun, 6 Apr 2025 10:47:14 -0400
Subject: [PATCH 2/3] Inv

---
 LeanTeXMathlib/Basic.lean | 5 +++++
 test/basic.lean           | 3 +++
 2 files changed, 8 insertions(+)

diff --git a/LeanTeXMathlib/Basic.lean b/LeanTeXMathlib/Basic.lean
index b412d80..5fe709a 100644
--- a/LeanTeXMathlib/Basic.lean
+++ b/LeanTeXMathlib/Basic.lean
@@ -196,6 +196,11 @@ latex_pp_app_rules (const := Singleton.singleton)
     let a ← LeanTeX.latexPP a
     return "\\{ " ++ a ++ " \\}" |>.resetBP .Infinity .Infinity
 
+latex_pp_app_rules (const := Inv.inv)
+  | _, #[_, _, a] => do
+    let a ← LeanTeX.latexPP a
+    return a.protectRight 100 ++ LatexData.atomString "^{-1}"
+
 latex_pp_app_rules (const := DirectSum)
   | _, #[ι, β, _inst] => do
     let pι ← withExtraSmallness 2 <| latexPP ι
diff --git a/test/basic.lean b/test/basic.lean
index 6deaa36..141131d 100644
--- a/test/basic.lean
+++ b/test/basic.lean
@@ -85,6 +85,9 @@ latex_pp_app_rules (kind := any) (paramKinds := params)
 /-- info: (5, \infty) -/
 #guard_msgs in #latex Set.Ioi 5
 
+/-- info: 3^{-1} -/
+#guard_msgs in #latex (3:ℝ)⁻¹
+
 open scoped DirectSum
 
 #texify ⨁ i, (Fin i → ℝ)

From bb1646b719ec60ce22caaeaa63d614a2d4d267a0 Mon Sep 17 00:00:00 2001
From: Li Xuanji <xuanji@gmail.com>
Date: Sun, 6 Apr 2025 11:09:02 -0400
Subject: [PATCH 3/3] smul

---
 LeanTeXMathlib/Basic.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/LeanTeXMathlib/Basic.lean b/LeanTeXMathlib/Basic.lean
index 5fe709a..2337516 100644
--- a/LeanTeXMathlib/Basic.lean
+++ b/LeanTeXMathlib/Basic.lean
@@ -201,6 +201,12 @@ latex_pp_app_rules (const := Inv.inv)
     let a ← LeanTeX.latexPP a
     return a.protectRight 100 ++ LatexData.atomString "^{-1}"
 
+latex_pp_app_rules (const := HSMul.hSMul)
+  | _, #[_, _, _, _, a, b] => do
+    let a ← LeanTeX.latexPP a
+    let b ← LeanTeX.latexPP b
+    return "(" ++ a ++ " \\cdot " ++ b ++ ")" |>.resetBP .Infinity .Infinity
+
 latex_pp_app_rules (const := DirectSum)
   | _, #[ι, β, _inst] => do
     let pι ← withExtraSmallness 2 <| latexPP ι