From 616f7178c8f4ded75e0e30448baabbb132671245 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Mon, 30 Oct 2023 16:31:27 -0700
Subject: [PATCH] close goal in example

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

diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index 47dbac258b5f..7497370f7b1a 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -106,6 +106,7 @@ example : let n := 1; let k := 2; n + k = 3 := by
   /- n✝ : Nat := 1
      k✝ : Nat := 2
      ⊢ n✝ + k✝ = 3 -/
+  rfl
 ```
 -/
 syntax (name := intros) "intros" (ppSpace colGt (ident <|> hole))* : tactic