From cc7a6b874b150eac3355ffc812595d1a60764c3b Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 15 Jul 2024 15:10:10 -0400
Subject: [PATCH] refactor: Change git-hub repo for llm

---
 HepLean/AnomalyCancellation/MSSMNu/Basic.lean | 4 ++--
 lakefile.toml                                 | 3 +--
 scripts/openAI_doc_check.lean                 | 4 ++--
 3 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/HepLean/AnomalyCancellation/MSSMNu/Basic.lean b/HepLean/AnomalyCancellation/MSSMNu/Basic.lean
index 3b69995..49883d7 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/Basic.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/Basic.lean
@@ -60,7 +60,7 @@ def toSpeciesMaps' : (Fin 18 → ℚ) ≃ (Fin 6 → Fin 3 → ℚ) :=
     ((@finProdFinEquiv 6 3).arrowCongr (Equiv.refl ℚ))).symm
 
 /-- An equivalence between `MSSMCharges.charges` and `(Fin 6 → Fin 3 → ℚ) × (Fin 2 → ℚ))`.
-This split charges up into the SM and additional fermions, and further splits the SM into
+This splits charges up into the SM and additional fermions, and further splits the SM into
 species. -/
 @[simps!]
 def toSpecies : MSSMCharges.Charges ≃ (Fin 6 → Fin 3 → ℚ) × (Fin 2 → ℚ) :=
@@ -233,7 +233,7 @@ lemma accSU3_ext {S T : MSSMCharges.Charges}
   repeat erw [hj]
   rfl
 
-/-- The acc for `Y²`. -/
+/-- The ACC for `Y²`. -/
 @[simp]
 def accYY : MSSMCharges.Charges →ₗ[ℚ] ℚ where
   toFun S := ∑ i, ((Q S) i + 8 * (U S) i + 2 * (D S) i + 3 * (L S) i
diff --git a/lakefile.toml b/lakefile.toml
index 0fd75e1..0326152 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -17,10 +17,9 @@ rev = "v4.10.0-rc1"
 name = "HepLean"
 
 # -- Optional inclusion of llm. Needed for `openAI_doc_check`
-# TODO: Move over to `leanprover-community/llm` versions there are bumped.  
 #[[require]]
 #name = "llm"
-#git = "https://github.com/jstoobysmith/Lean_llm_fork"
+#git = "https://github.com/leanprover-community/llm"
 #rev = "main"
 
 # -- Optional inclusion of tryAtEachStep
diff --git a/scripts/openAI_doc_check.lean b/scripts/openAI_doc_check.lean
index 3fe0740..b8a07df 100644
--- a/scripts/openAI_doc_check.lean
+++ b/scripts/openAI_doc_check.lean
@@ -17,8 +17,8 @@ import LLM.GPT.API
 This file uses the openAI API to check the doc strings of definitions and theorems in a
 Lean 4 file.
 
-It currently depends on `https://github.com/jstoobysmith/Lean_llm_fork` being imported,
-which is currently not by default.
+This file depends on `https://github.com/leanprover-community/llm` being imported.
+This is not currently done by default.
 
 -/
 open Lean