From 2195936a88475d159a1b873307c62f76f098979f Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 20 May 2024 00:19:15 +0200
Subject: [PATCH 01/16] Update Basic.lean

---
 HepLean/AnomalyCancellation/Basic.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/HepLean/AnomalyCancellation/Basic.lean b/HepLean/AnomalyCancellation/Basic.lean
index 382bcb7..651118c 100644
--- a/HepLean/AnomalyCancellation/Basic.lean
+++ b/HepLean/AnomalyCancellation/Basic.lean
@@ -77,7 +77,7 @@ namespace ACCSystemLinear
 structure LinSols (χ : ACCSystemLinear) where
   /-- The underlying charge. -/
   val : χ.1.charges
-  /-- The condition that the charge satifies the linear ACCs. -/
+  /-- The condition that the charge satisfies the linear ACCs. -/
   linearSol : ∀ i : Fin χ.numberLinear, χ.linearACCs i val = 0
 
 /-- Two solutions are equal if the underlying charges are equal. -/
@@ -172,7 +172,7 @@ namespace ACCSystemQuad
 
 /-- The type of solutions to the linear and quadratic ACCs. -/
 structure QuadSols (χ : ACCSystemQuad) extends χ.LinSols where
-  /-- The condition that the charge satifies the quadratic ACCs. -/
+  /-- The condition that the charge satisfies the quadratic ACCs. -/
   quadSol : ∀ i : Fin χ.numberQuadratic, (χ.quadraticACCs i) val = 0
 
 /-- Two `QuadSols` are equal if the underlying charges are equal. -/
@@ -225,7 +225,7 @@ namespace ACCSystem
 
 /-- The type of solutions to the anomaly cancellation conditions. -/
 structure Sols (χ : ACCSystem) extends χ.QuadSols where
-  /-- The condition that the charge satifies the cubic ACC. -/
+  /-- The condition that the charge satisfies the cubic ACC. -/
   cubicSol : χ.cubicACC val = 0
 
 /-- Two solutions are equal if the underlying charges are equal. -/

From 718b1049d123e54f4f1089ac766e2134e3e43965 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 20 May 2024 00:19:16 +0200
Subject: [PATCH 02/16] Update Basic.lean

---
 HepLean/AnomalyCancellation/MSSMNu/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/HepLean/AnomalyCancellation/MSSMNu/Basic.lean b/HepLean/AnomalyCancellation/MSSMNu/Basic.lean
index 839e1d9..1b8ce7c 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/Basic.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/Basic.lean
@@ -206,7 +206,7 @@ lemma accSU2_ext {S T : MSSMCharges.charges}
   rw [hd, hu]
   rfl
 
-/-- The anomaly cancelation condition for SU(3) anomaly. -/
+/-- The anomaly cancellation condition for SU(3) anomaly. -/
 @[simp]
 def accSU3 : MSSMCharges.charges →ₗ[ℚ] ℚ where
   toFun S := ∑ i, (2 * (Q S i) + (U S i) + (D S i))

From 1e0a0487a0ff2b1c2b1745052f6a65d7238ae3b1 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 20 May 2024 00:19:18 +0200
Subject: [PATCH 03/16] Update HyperCharge.lean

---
 HepLean/AnomalyCancellation/MSSMNu/HyperCharge.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/HepLean/AnomalyCancellation/MSSMNu/HyperCharge.lean b/HepLean/AnomalyCancellation/MSSMNu/HyperCharge.lean
index 8af33de..23268af 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/HyperCharge.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/HyperCharge.lean
@@ -8,7 +8,7 @@ import Mathlib.Tactic.Polyrith
 /-!
 # Hypercharge in MSSM.
 
-Relavent definitions for the MSSM hypercharge.
+Relevant definitions for the MSSM hypercharge.
 
 -/
 

From 1da2fd17382e80ed58679b1cb9e1af7540f937ea Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 20 May 2024 00:19:21 +0200
Subject: [PATCH 04/16] Update LineInCubic.lean

---
 HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean b/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
index 834dc5b..db47ec0 100644
--- a/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
@@ -67,7 +67,7 @@ lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n.succ)).LinSols} (h : lineInCubic
   linear_combination 2 / 3 * (lineInCubic_expand h g f hS 1 1) -
    (lineInCubic_expand h g f hS 1 2) / 6
 
-/-- We say a `LinSol` satifies  `lineInCubicPerm` if all its permutations satsify `lineInCubic`. -/
+/-- We say a `LinSol` satisfies  `lineInCubicPerm` if all its permutations satisfy `lineInCubic`. -/
 def lineInCubicPerm (S : (PureU1 (2 * n.succ)).LinSols) : Prop :=
   ∀ (M : (FamilyPermutations (2 * n.succ)).group ),
   lineInCubic ((FamilyPermutations (2 * n.succ)).linSolRep M S)

From 90deb528a2a73863412ffabf5777f17b0a37c1d3 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 20 May 2024 00:19:22 +0200
Subject: [PATCH 05/16] Update LineInPlaneCond.lean

---
 HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean b/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean
index 3d87877..8ea80f4 100644
--- a/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean
+++ b/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean
@@ -12,7 +12,7 @@ import Mathlib.RepresentationTheory.Basic
 /-!
 # Line in plane condition
 
-We say a `LinSol` satifies the `line in plane` condition if for all distinct `i1`, `i2`, `i3` in
+We say a `LinSol` satisfies the `line in plane` condition if for all distinct `i1`, `i2`, `i3` in
 `Fin n`, we have
 `S i1 = S i2`  or  `S i1 = - S i2` or  `2 S i3 + S i1 + S i2 = 0`.
 
@@ -21,7 +21,7 @@ The main reference for this material is
 
 - https://arxiv.org/pdf/1912.04804.pdf
 
-We will show that `n ≥ 4` the `line in plane` condition on solutions inplies the
+We will show that `n ≥ 4` the `line in plane` condition on solutions implies the
 `constAbs` condition.
 
 -/

From a25dcb4d9c0ec84e95fd6a344a2f2b8089c39b74 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 20 May 2024 00:19:24 +0200
Subject: [PATCH 06/16] Update BasisLinear.lean

---
 HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
index ef0361d..30c7570 100644
--- a/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
@@ -10,7 +10,7 @@ import Mathlib.Logic.Equiv.Fin
 /-!
 # Basis of `LinSols` in the odd case
 
-We give a basis of `LinSols` in the odd case. This basis has the special propoerty
+We give a basis of `LinSols` in the odd case. This basis has the special property
 that splits into two planes on which every point is a solution to the ACCs.
 -/
 universe v u

From c768e660a1590272d540546eb7f0d16e8f635c64 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 20 May 2024 00:19:25 +0200
Subject: [PATCH 07/16] Update LineInCubic.lean

---
 HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean b/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
index d7a9000..d5153b5 100644
--- a/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
@@ -16,10 +16,10 @@ import Mathlib.RepresentationTheory.Basic
 # Line In Cubic Odd case
 
 We say that a linear solution satisfies the `lineInCubic` property
-if the line through that point and through the two different planes formed by the baisis of
+if the line through that point and through the two different planes formed by the basis of
 `LinSols` lies in the cubic.
 
-We show that for a solution all its permutations satsfiy this property,
+We show that for a solution all its permutations satisfy this property,
 then the charge must be zero.
 
 The main reference for this file is:
@@ -34,7 +34,7 @@ open BigOperators
 variable {n : ℕ}
 open VectorLikeOddPlane
 
-/-- A  property on `LinSols`, statified if every point on the line between the two planes
+/-- A  property on `LinSols`, satisfied if every point on the line between the two planes
 in the basis through that point is in the cubic. -/
 def lineInCubic (S : (PureU1 (2 * n + 1)).LinSols) : Prop :=
   ∀ (g f : Fin n → ℚ)  (_ : S.val = Pa g f) (a b : ℚ) ,
@@ -64,7 +64,7 @@ lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n + 1)).LinSols} (h : lineInCubic S
 
 
 
-/-- We say a `LinSol` satifies  `lineInCubicPerm` if all its permutations satsify `lineInCubic`. -/
+/-- We say a `LinSol` satisfies  `lineInCubicPerm` if all its permutations satisfy `lineInCubic`. -/
 def lineInCubicPerm (S : (PureU1 (2 * n + 1)).LinSols) : Prop :=
   ∀ (M : (FamilyPermutations (2 * n + 1)).group ),
     lineInCubic ((FamilyPermutations (2 * n + 1)).linSolRep M S)

From a368679152e51e33692309fa10f515285d64d54c Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 20 May 2024 00:19:28 +0200
Subject: [PATCH 08/16] Update Basic.lean

---
 HepLean/AnomalyCancellation/SM/Basic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/HepLean/AnomalyCancellation/SM/Basic.lean b/HepLean/AnomalyCancellation/SM/Basic.lean
index cd71230..5f68cc6 100644
--- a/HepLean/AnomalyCancellation/SM/Basic.lean
+++ b/HepLean/AnomalyCancellation/SM/Basic.lean
@@ -13,7 +13,7 @@ import Mathlib.Logic.Equiv.Fin
 /-!
 # Anomaly cancellation conditions for n family SM.
 
-We define the ACC system for the Standard Model with`n`-famlies and no RHN.
+We define the ACC system for the Standard Model with`n`-families and no RHN.
 
 -/
 
@@ -21,7 +21,7 @@ universe v u
 open Nat
 open BigOperators
 
-/-- Aassociate to each (including RHN) SM fermion a set of charges-/
+/-- Associate to each (including RHN) SM fermion a set of charges-/
 @[simps!]
 def SMCharges (n : ℕ) : ACCSystemCharges := ACCSystemChargesMk (5 * n)
 

From 7515fde40251735fa2b3350183fc1cd07db369df Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 20 May 2024 00:19:30 +0200
Subject: [PATCH 09/16] Update FamilyMaps.lean

---
 HepLean/AnomalyCancellation/SM/FamilyMaps.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/HepLean/AnomalyCancellation/SM/FamilyMaps.lean b/HepLean/AnomalyCancellation/SM/FamilyMaps.lean
index 2dc75d6..37c5bae 100644
--- a/HepLean/AnomalyCancellation/SM/FamilyMaps.lean
+++ b/HepLean/AnomalyCancellation/SM/FamilyMaps.lean
@@ -7,7 +7,7 @@ import HepLean.AnomalyCancellation.SM.Basic
 /-!
 # Family maps for the Standard Model ACCs
 
-We define the a series of maps between the charges for different numbers of famlies.
+We define the a series of maps between the charges for different numbers of families.
 
 -/
 
@@ -84,7 +84,7 @@ other charges zero.  -/
 def familyEmbedding (m n : ℕ) : (SMCharges m).charges →ₗ[ℚ] (SMCharges n).charges :=
   chargesMapOfSpeciesMap (speciesEmbed m n)
 
-/-- For species, the embeddding of the `1`-family charges into the `n`-family charges in
+/-- For species, the embedding of the `1`-family charges into the `n`-family charges in
 a universal manor. -/
 @[simps!]
 def speciesFamilyUniversial (n : ℕ) :
@@ -98,7 +98,7 @@ def speciesFamilyUniversial (n : ℕ) :
     simp [HSMul.hSMul]
     --rw [show Rat.cast a = a from rfl]
 
-/-- The embeddding of the `1`-family charges into the `n`-family charges in
+/-- The embedding of the `1`-family charges into the `n`-family charges in
 a universal manor. -/
 def familyUniversal ( n : ℕ) : (SMCharges 1).charges →ₗ[ℚ] (SMCharges n).charges :=
   chargesMapOfSpeciesMap (speciesFamilyUniversial n)

From e77dd4b09877d8b770cccbde482a8e8275272cae Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 20 May 2024 00:19:31 +0200
Subject: [PATCH 10/16] Update Lemmas.lean

---
 HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean b/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean
index e24ce3a..6288867 100644
--- a/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean
+++ b/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean
@@ -12,7 +12,7 @@ import HepLean.AnomalyCancellation.SM.NoGrav.One.LinearParameterization
 The main result of this file is the conclusion of this paper:
 https://arxiv.org/abs/1907.00514
 
-That eveery solution to the ACCs without gravity satifies for free the gravitational anomaly.
+That eveery solution to the ACCs without gravity satisfies for free the gravitational anomaly.
 -/
 
 universe v u
@@ -67,7 +67,7 @@ lemma accGrav_Q_neq_zero {S : (SMNoGrav 1).Sols} (hQ : Q S.val (0 : Fin 1) ≠ 0
   rw [← hS']
   exact S'.grav_of_cubic hC FLTThree
 
-/-- Any solution to the ACCs without gravity satifies the gravitational ACC.  -/
+/-- Any solution to the ACCs without gravity satisfies the gravitational ACC.  -/
 theorem accGravSatisfied {S : (SMNoGrav 1).Sols} (FLTThree : FermatLastTheoremWith ℚ 3) :
     accGrav S.val = 0 := by
   by_cases hQ : Q S.val (0 : Fin 1)= 0

From 1cd9dd3ed4ef5b422aa9d923963bc7566a257a93 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 20 May 2024 00:19:34 +0200
Subject: [PATCH 11/16] Update FamilyMaps.lean

---
 HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean b/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean
index 8ffd5e8..1c11dca 100644
--- a/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean
+++ b/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean
@@ -7,7 +7,7 @@ import HepLean.AnomalyCancellation.SMNu.Basic
 /-!
 # Family maps for the Standard Model  for RHN ACCs
 
-We define the a series of maps between the charges for different numbers of famlies.
+We define the a series of maps between the charges for different numbers of families.
 
 -/
 
@@ -89,7 +89,7 @@ other charges zero.  -/
 def familyEmbedding (m n : ℕ) : (SMνCharges m).charges →ₗ[ℚ] (SMνCharges n).charges :=
   chargesMapOfSpeciesMap (speciesEmbed m n)
 
-/-- For species, the embeddding of the `1`-family charges into the `n`-family charges in
+/-- For species, the embedding of the `1`-family charges into the `n`-family charges in
 a universal manor. -/
 @[simps!]
 def speciesFamilyUniversial (n : ℕ) :
@@ -103,7 +103,7 @@ def speciesFamilyUniversial (n : ℕ) :
     simp [HSMul.hSMul]
     -- rw [show Rat.cast a = a from rfl]
 
-/-- The embeddding of the `1`-family charges into the `n`-family charges in
+/-- The embedding of the `1`-family charges into the `n`-family charges in
 a universal manor. -/
 def familyUniversal (n : ℕ) : (SMνCharges 1).charges →ₗ[ℚ] (SMνCharges n).charges :=
   chargesMapOfSpeciesMap (speciesFamilyUniversial n)

From ee3c7580b58a479b3de5c44e30f7a7c44abfe64b Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 20 May 2024 00:19:36 +0200
Subject: [PATCH 12/16] Update Basic.lean

---
 HepLean/FlavorPhysics/CKMMatrix/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/HepLean/FlavorPhysics/CKMMatrix/Basic.lean b/HepLean/FlavorPhysics/CKMMatrix/Basic.lean
index 36cba92..611612e 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/Basic.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Basic.lean
@@ -9,7 +9,7 @@ import Mathlib.Tactic.Polyrith
 /-!
 # The CKM Matrix
 
-The definition of the type of CKM matries as unitary $3×3$-matries.
+The definition of the type of CKM matrices as unitary $3×3$-matrices.
 
 An equivalence relation on CKM matrices is defined, where two matrices are equivalent if they are
 related by phase shifts.

From 68888861b976b7c798db3f36321a40053fae1896 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 20 May 2024 08:13:59 -0400
Subject: [PATCH 13/16] Update README.md

---
 README.md | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/README.md b/README.md
index 9712d0d..72011f3 100644
--- a/README.md
+++ b/README.md
@@ -1,5 +1,9 @@
 # High Energy Physics in Lean
 
+[![](https://img.shields.io/badge/Read_The-Docs-green)](https://heplean.github.io/HepLean/)
+[![](https://img.shields.io/badge/PRs-Welcome-green)](https://github.com/HEPLean/HepLean/pulls)
+[![](https://img.shields.io/badge/Lean-Zulip-green)](https://leanprover.zulipchat.com)
+
 A project to digitalize high energy physics.
 
 ## Aims of this project

From f34017713784c35eb260c03c91edc0e3b02408ad Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 21 May 2024 07:15:02 -0400
Subject: [PATCH 14/16] chore: Update gitignore

---
 .gitignore | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/.gitignore b/.gitignore
index 2aa4e22..eb3c204 100644
--- a/.gitignore
+++ b/.gitignore
@@ -2,4 +2,9 @@
 /lake-packages/*
 .lake/packages/*
 .lake/build
-paper
\ No newline at end of file
+# Section: To be ignored, except when updating Lean and MathLib versions
+.lake/lakefile.olean
+.lake/lakefile.olean.trace
+lake-manifest.json
+lakefile.lean
+# End Section.
\ No newline at end of file

From 3bb69f939df6b19a397a00fa6da71d163de8aec2 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 21 May 2024 07:48:06 -0400
Subject: [PATCH 15/16] feat: Add copilot add script

---
 .gitignore                   |  8 +-------
 scripts/add-copilot.sh       | 14 ++++++++++++++
 scripts/copilot_lakefile.txt | 23 +++++++++++++++++++++++
 3 files changed, 38 insertions(+), 7 deletions(-)
 create mode 100755 scripts/add-copilot.sh
 create mode 100644 scripts/copilot_lakefile.txt

diff --git a/.gitignore b/.gitignore
index eb3c204..d701102 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,10 +1,4 @@
 /build
 /lake-packages/*
 .lake/packages/*
-.lake/build
-# Section: To be ignored, except when updating Lean and MathLib versions
-.lake/lakefile.olean
-.lake/lakefile.olean.trace
-lake-manifest.json
-lakefile.lean
-# End Section.
\ No newline at end of file
+.lake/build
\ No newline at end of file
diff --git a/scripts/add-copilot.sh b/scripts/add-copilot.sh
new file mode 100755
index 0000000..8db5a88
--- /dev/null
+++ b/scripts/add-copilot.sh
@@ -0,0 +1,14 @@
+#!/usr/bin/env bash
+
+
+cp ./scripts/copilot_lakefile.txt lakefile.lean
+
+lake update LeanCopilot 
+
+lake exe LeanCopilot/download
+
+lake build 
+
+echo ".........................................................................."
+echo "Please do not push changes to the following files: lakefile.lean, .lake/lakefile.olean, 
+    .lake/lakefile.olean.trace, lake-manifest.json."
diff --git a/scripts/copilot_lakefile.txt b/scripts/copilot_lakefile.txt
new file mode 100644
index 0000000..1c73ce2
--- /dev/null
+++ b/scripts/copilot_lakefile.txt
@@ -0,0 +1,23 @@
+import Lake
+open Lake DSL
+
+package «hep_lean» {
+  -- add any package configuration options here
+}
+
+require mathlib from git
+  "https://github.com/leanprover-community/mathlib4.git"
+
+@[default_target]
+lean_lib «HepLean» {
+  -- add any library configuration options here
+  moreLinkArgs := #[
+    "-L./.lake/packages/LeanCopilot/.lake/build/lib",
+    "-lctranslate2"
+  ]
+}
+
+meta if get_config? env = some "dev" then -- dev is so not everyone has to build it
+require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
+
+require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "v1.2.1"
\ No newline at end of file

From 939623ed058387b0d054c6c2fd63320a30cc3238 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 21 May 2024 08:18:09 -0400
Subject: [PATCH 16/16] docs: update ReadMe file.

---
 README.md              | 31 ++++++++++++++++++++++++++++++-
 scripts/add-copilot.sh |  8 ++++++--
 2 files changed, 36 insertions(+), 3 deletions(-)

diff --git a/README.md b/README.md
index 72011f3..21c32ec 100644
--- a/README.md
+++ b/README.md
@@ -57,4 +57,33 @@ The installation instructions for Lean 4 are given here: https://leanprover-comm
 - Run `lake exe cache get`. The command `lake` should have been installed when you installed Lean.
 - Run `lake build`.
 - Open the directory (not a single file) in Visual Studio Code (or another Lean compatible code editor).
-  
+
+### Adding Lean Copilot (optional)
+
+[Lean Copilot](https://github.com/lean-dojo/LeanCopilot) allows the use of large language models in Lean. Using Lean Copilot with HepLean can be done in the following way:
+
+Either: 
+
+- Run the script `./scripts/add-copilot.sh` 
+
+Or: 
+
+- Copy the file `./scripts/copilot_lakefile.txt` over to `lakefile.lean`,
+- Run `lake update LeanCopilot`,
+- Run `lake exe LeanCopilot/download`,
+- Run `lake build`.
+
+To use LeanCopilot add `import LeanCopilot` to the top of the lean file you are working in. 
+The following commands should then become available to you:
+- `suggest_tactics`,
+- `search_proofs`,
+- `select_premises`.
+
+Adding Lean Copilot will modify a number of files. If you have added Lean Copilot, please do not push changes to the following files:
+
+- `lakefile.lean`,
+- `.lake/lakefile.olean`,
+- `.lake/lakefile.olean.trace`,
+- `lake-manifest.json`.
+
+Please also ensure that there are not any `import LeanCopilot` statements in the lean files.
diff --git a/scripts/add-copilot.sh b/scripts/add-copilot.sh
index 8db5a88..d0cb37e 100755
--- a/scripts/add-copilot.sh
+++ b/scripts/add-copilot.sh
@@ -10,5 +10,9 @@ lake exe LeanCopilot/download
 lake build 
 
 echo ".........................................................................."
-echo "Please do not push changes to the following files: lakefile.lean, .lake/lakefile.olean, 
-    .lake/lakefile.olean.trace, lake-manifest.json."
+echo "Please do not push changes to the following files: 
+     - lakefile.lean
+     - .lake/lakefile.olean
+     - .lake/lakefile.olean.trace
+     - lake-manifest.json
+Please ensure that there are no 'import LeanCopilot' statements in the lean files."