From 2ed777b2b4fb90856ce74ed8ec1460e650062946 Mon Sep 17 00:00:00 2001
From: Hongyu Ouyang <96765450+casavaca@users.noreply.github.com>
Date: Sat, 23 Mar 2024 00:39:36 -0700
Subject: [PATCH] doc: fix typo in docstring of `left` (#3748)

---
 src/Init/Tactics.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index 416c69bbfa..477e55e6cc 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -224,7 +224,7 @@ the first matching constructor, or else fails.
 syntax (name := constructor) "constructor" : tactic
 
 /--
-Applies the second constructor when
+Applies the first constructor when
 the goal is an inductive type with exactly two constructors, or fails otherwise.
 ```
 example : True ∨ False := by