Merge pull request #40 from jsal13/patch-1

typo: othey -> other
leanprover-community · Nov 1, 2023 · d05c749 · d05c749
2 parents 14ce186 + 59b65de
commit d05c749
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Game/Levels/Implication/L01exact.lean b/Game/Levels/Implication/L01exact.lean
@@ -38,7 +38,7 @@ NewTactic exact
 Introduction
 "
 In this world we'll learn how to prove theorems of the form $P\\implies Q$.
-In othey words, how to prove theorems of the form \"if $P$ is true, then $Q$ is true.\"
+In other words, how to prove theorems of the form \"if $P$ is true, then $Q$ is true.\"
 To do that we need to learn some more tactics.
 
 The `exact` tactic can be used to close a goal which is exactly one of