case names generated by congr!

Stream: lean4

[Kayla Thomas]

How are the case names generated by cong!? Is there a way to set them? I get things like case a.h.e'_4.

[Mario Carneiro]

does congr! with a b c work?

[Kayla Thomas]

I don't think there is anything to assign to the a b c here.

[Kayla Thomas]

Trying it anyway makes the name longer.

[Kayla Thomas]

In this case it is a congr! 1 to be more exact.

[Mario Carneiro]

It is difficult to say without a MWE

[Mario Carneiro]

what is the goal?

[Kayla Thomas]

D: Type
I: Interpretation D
V': VarAssignment D
vt: VarName
X: PredName
xs: List VarName
V: VarAssignment D
binders: Finset VarName
h2: ∀ (v : VarName), ¬v ∈ binders → V' v = V v
h1: v ∈ xs → ¬t ∈ binders
⊢ Interpretation.pred_const_ I X (List.map (Function.updateIte V v (V' t)) xs) ↔
  Interpretation.pred_const_ I X (List.map V (List.map (fun x => if v = x then t else x) xs))

[Mario Carneiro]

I would not expect congr! 1 to introduce any new names here

[Mario Carneiro]

Oh you mean the subgoals?

[Kayla Thomas]

yeah

[Mario Carneiro]

Mathlib tactics don't try very hard to give the subgoals meaningful names. You should just use \. or next a b c => for each subgoal

[Kayla Thomas]

next a b c?

[Mario Carneiro]

that is essentially a combination of \. and rename_i, it focuses a case and names the variables introduced in that case

[Mario Carneiro]

in this case there probably aren't any

[Kayla Thomas]

Cool. That makes it easier. Thank you.

[Mario Carneiro]

next a b c => ... is also equivalent to case _ a b c => ..., where case foo a b c => ... selects the case named foo and case _ just selects the next case

[Kayla Thomas]

Oh, I didn't know you could do _.

[Kayla Thomas]

Thank you.