wlog ... replacing ...?

Stream: mathlib4

[Yury G. Kudryashov]

I'm writing a proof where I have h : NullMeasurableSet s μ and the first step is wlog h' : MeasurableSet s. The first goal generated by wlog has assumptions

h : NullMesaurableSet s μ
this : ∀ {s : Set G},  NullMesaurableSet s μ → (other assumptions) → MeasurableSet s → (main goal)
h' : ¬MeasurableSet s

and the second goal has both

h : NullMeasurableSet s μ
h' : MeasurableSet s

It would be nice to have something like

wlog h' : MeasurableSet s replacing h

generate goals with assumptions

h : NullMesaurableSet s μ
this : ∀ {s : Set G},  (other assumptions) → MeasurableSet s → (main goal)
h' : ¬MeasurableSet s

and

h' : MeasurableSet s

[Yury G. Kudryashov]

In this case, it is easy to show that the other set I'm going to apply this to is both null measurable and measurable but sometimes it's less trivial.

[Yury G. Kudryashov]

@Johan Commelin What do you think about :up:?

[Johan Commelin]

All my meta skills are cargo-culted. I'm not the right person to answer this question.

[Yury G. Kudryashov]

Next stage: reverse cargo-cult about meta skills: think that everyone else's meta skills are in fact cargo-culted too.

[Thomas Murrills]

For my part, this sounds reasonable—we have generalizing h but not generalizing -h, and this would fill that gap. I think replacing is better than generalizing -h since

1. generalizing -h is pretty opaque readability-wise
2. you can't mix - with non-- specifications: generalizing -h1 -h2 ... makes sense, but generalizing -h1 h2 ... doesn't, so it makes sense to specify this by changing the syntax at generalizing instead of at the hypotheses.

However, I wonder why we wouldn't keep h : NullMeasurableSet s μ in the hypotheses of the second goal, even though it would be cleared from the type of this. Is it desirable to eliminate it from the context of the second goal for some reason?

[Yury G. Kudryashov]

Because in my example it's in fact wlog h' : MeasurableSet s generalizing s and I apply this to toMeasurable μ s.

[Yury G. Kudryashov]

While I can prove that the new set is both measurable and null-measurable, it's more natural to skip this proof and drop the weaker assumption I'm not going to use.

[Yury G. Kudryashov]

And if I don't prove that the new set is null-measurable, then I can no longer use this assumption in the second goal.

[Thomas Murrills]

I see! I explored this on !4#5364, which implements this functionality. (The branch name is wlog-replacing.) Currently that's a draft pull request, since I'm not sure this is something we ought to do (but I wanted to see if we could anyway). It probably needs a stress test; feel free to test it out and let me know if it suits your use case.

If people like the functionality, we can make it a real PR.