diff --git a/Batteries/Util/Cache.lean b/Batteries/Util/Cache.lean
index 1c25bb163c..edfac4fe97 100644
--- a/Batteries/Util/Cache.lean
+++ b/Batteries/Util/Cache.lean
@@ -132,7 +132,7 @@ the second will store declarations from imports (and will hopefully be "read-onl
 -/
 @[reducible] def DiscrTreeCache (α : Type) : Type := DeclCache (DiscrTree α × DiscrTree α)
 
-/-- Discrimation tree settings for the `DiscrTreeCache`. -/
+/-- Discrimination tree settings for the `DiscrTreeCache`. -/
 def DiscrTreeCache.config : WhnfCoreConfig := {}
 
 /--
diff --git a/Batteries/Util/CheckTactic.lean b/Batteries/Util/CheckTactic.lean
index cab01de05b..bc97e681cc 100644
--- a/Batteries/Util/CheckTactic.lean
+++ b/Batteries/Util/CheckTactic.lean
@@ -9,7 +9,7 @@ import Lean.Elab.Term
 /-
 This file is the home for commands to tactics behave as expected.
 
-It currently includes two tactixs:
+It currently includes two tactics:
 
 #check_tactic t ~> res
 
diff --git a/Batteries/WF.lean b/Batteries/WF.lean
index 8fef8ad188..7a702665ae 100644
--- a/Batteries/WF.lean
+++ b/Batteries/WF.lean
@@ -91,7 +91,7 @@ end Acc
 namespace WellFounded
 
 /-- Attaches to `x` the proof that `x` is accessible in the given well-founded relation.
-This can be used in recursive function definitions to explicitly use a differerent relation
+This can be used in recursive function definitions to explicitly use a different relation
 than the one inferred by default:
 
 ```