obtain tactic creates inaccessible name

Stream: lean4

[Eric Wieser]

This fails, but I'd expect it to succeed:

theorem oops : True := by
  obtain h : True
  · trivial
  exact h

[Mauricio Collares]

Is it just me or does your code contain non-breaking spaces (U+00A0, urlencoded as %C2%A0 in the playground url and shown with a yellow border there)? This is unrelated to h being inaccessible in the version with proper spaces, which I guess is the bug you're asking about.

[Mauricio Collares]

theorem oops : True := by
  obtain h : True
  · trivial
  exact h

[Jovan Gerbscheid]

I complained about a variant of this in #lean4 > RFC: `rcases`/`obtain` should always clear a variable

theorem oops (h : False) : False := by
  obtain h' := h
  exact h' -- fails

[Jon Eugster]

Eric Wieser said:

This fails, but I'd expect it to succeed:

theorem oops : True := by
  obtain h : True
  · trivial
  exact h

it might be that this change already fixes your bug:

diff --git a/src/Lean/Elab/Tactic/RCases.lean b/src/Lean/Elab/Tactic/RCases.lean
index bfad9f98be..fbed5d62a5 100644
--- a/src/Lean/Elab/Tactic/RCases.lean
+++ b/src/Lean/Elab/Tactic/RCases.lean
@@ -449,7 +449,7 @@ def obtainNone (pat : RCasesPatt) (ty : Syntax) (g : MVarId) : TermElabM (List M
   Term.withSynthesize do
     let ty ← Term.elabType ty
     let g₁ ← mkFreshExprMVar (some ty)
-    let (v, g₂) ← (← g.assert (pat.name?.getD default) ty g₁).intro1
+    let (v, g₂) ← (← g.assert (pat.name?.getD default) ty g₁).intro1P
     let gs ← rcasesCore g₂ {} #[] (.fvar v) #[] pat finish
     pure (g₁.mvarId! :: gs.toList)

(it doesn't affect Jovan's issue though)

[Jon Eugster]

Screenshot 2026-02-08 at 01.02.20.png