diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean
index 16db2812f3..08a09802b7 100644
--- a/src/Init/Classical.lean
+++ b/src/Init/Classical.lean
@@ -195,7 +195,7 @@ end Classical
 /- Export for Mathlib compat. -/
 export Classical (imp_iff_right_iff imp_and_neg_imp_iff and_or_imp not_imp)
 
-/-- Extract an element from a existential statement, using `Classical.choose`. -/
+/-- Extract an element from an existential statement, using `Classical.choose`. -/
 -- This enables projection notation.
 @[reducible] noncomputable def Exists.choose {p : α → Prop} (P : ∃ a, p a) : α := Classical.choose P