expose_names

Stream: lean4

[Darij Grinberg]

I'm doing a semi-automated casebash in which I run cases on 4 disjunctions and then apply their results. I need the case-hypotheses named so I can simp using them. This here works:

cases h11 <;> cases h12 <;> cases h21 <;> cases h22 <;> expose_names <;> simp [h, h_1, h_2, h_3, not_lt_of_gt h, not_lt_of_gt h_1, not_lt_of_gt h_2, not_lt_of_gt h_3] <;> order

but feels brittle because I'm relying on expose_names to produce the specific names h, h_1, h_2, h_3. What is the right way to do this?

[Aaron Liu]

you could try a simp_all

[Aaron Liu]

you could use rename_i

[Darij Grinberg]

I'd rather avoid unrelated hypotheses

[Darij Grinberg]

oh!

[Darij Grinberg]

rename_i is the answer, thank you!

[Kevin Buzzard]

Can you do obtain \<names,I,want\> := h11 etc?

[Darij Grinberg]

These are disjunctions, though. Does obtain h | h work? (Not having VS open right now)

[Aaron Liu]

It does work probably

[Darij Grinberg]

Thanks @Kevin Buzzard ! works nicely and looks much better