From f518efc81c7d6a1cd1f305e7bcbbaa6ce33153fc Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Wed, 24 Jul 2024 11:06:26 +0200
Subject: [PATCH] Update LetIntros.lean

---
 server/GameServer/Tactic/LetIntros.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/server/GameServer/Tactic/LetIntros.lean b/server/GameServer/Tactic/LetIntros.lean
index 473e0b7..ed94df0 100644
--- a/server/GameServer/Tactic/LetIntros.lean
+++ b/server/GameServer/Tactic/LetIntros.lean
@@ -44,7 +44,7 @@ def _root_.Lean.MVarId.letIntros (mvarId : MVarId) : MetaM (Array FVarId × MVar
     mvarId.introNP n
 
 /--
-`let_intros` introduces all `let` statements that are preceeding the proof. Concretely
+`let_intros` introduces all `let` statements that are preceding the proof. Concretely
 it does a subset of what `intros` does.
 
 If names are provided, it will introduce as many `let` statements as there are names.