Clearing goal name

Stream: new members

[Alex Meiburg]

How can I clear the name on a current goal? Sometimes after doing a few cases and so on I have a goal named like neg.intro or something, and then further cases get silly tags like neg.intro.pos and neg.intro.neg and I'd prefer to just be able to refer to them as pos and neg. Alternately, if there's a syntax like case _pos => or case *.pos =>, that's fine too

[Joachim Breitner]

Doesn't case pos work? I didn't try, but vaguely remember that the case name only has to be a suffix of the goal name as displayed in the info view.

[Alex Meiburg]

nope, it doesn't. It complains that there's no "pos" tag, just "neg.intro.pos" (and others)

[Joachim Breitner]

Ok, sorry for the noise then.

[Kyle Miller]

It should work -- cases looks for an exact match, and if that fails a suffix, and if that fails a prefix.

[Kyle Miller]

Could you make a #mwe of it not working?

[Alex Meiburg]

import Mathlib.Data.Polynomial.Basic
import Mathlib.Data.Sign

theorem foobar {α : Type*} [LinearOrderedField α] (η : α) : 2 ≥  1 := by
    by_cases hd0 : (η = 37)
    case pos => sorry
    case neg
    {
      cases hcsq1 : SignType.sign η
      case zero => { --zero
        sorry
      }
      case _ => {--neg
        sorry
      }
      case _ => {--pos
        sorry
      }
    }

[Kyle Miller]

Thanks, the error message hints at the problem

Available tags: 'neg.zero._@.Mathlib.foo._hyg.16', 'neg.neg._@.Mathlib.foo._hyg.16', 'neg.pos._@.Mathlib.foo._hyg.16'

Either case needs to be fixed to be able to handle hygienic names, or cases needs to be fixed to not generate tags with hygienic names. I'm not sure which is the right thing, but I'm sure that in any case case zero should work.

[Alex Meiburg]

alright haha. Yeah, I'll admit I have no idea what "hygenic tags" are so I'll leave that for someone else to deal with :) But, since prefixes do work, is there a way for me to clear the tag on the current goal? -- so that instead of 'neg.zero._@.Mathlib.foo._hyg.16' the tag gets named 'zero._@.Mathlib.foo._hyg.16' and then case works

[Kyle Miller]

I'm not sure there's already a tactic for it, but here's one hot off the presses:

import Mathlib.Data.Polynomial.Basic
import Mathlib.Data.Sign

open Lean Elab Tactic in
elab "clear_tag" : tactic => do
  let g ← getMainGoal
  g.setTag Name.anonymous

theorem foobar {α : Type*} [LinearOrderedField α] (η : α) : 2 ≥  1 := by
    by_cases hd0 : (η = 37)
    case pos => sorry
    case neg
    {
      clear_tag
      cases hcsq1 : SignType.sign η
      case zero => { --zero
        sorry
      }
      case _ => {--neg
        sorry
      }
      case _ => {--pos
        sorry
      }
    }

[Alex Meiburg]

Snazzy! :) Thanks!

[Alex Meiburg]

I'll leave this marked "unresolved" in case someone else knows of one in mathlib, or wants to add your clear_tag in a PR. Anyone else, free to close it if desired