proving conjunction

Stream: new members

[Michael Beeson]

Say my goal is A \and B. So I split, and give a long proof of A, and in the course of proving A I prove B. Now I finish the
first branch of my split and I would like to say, OK I'm done now because I already proved B. But that environment is gone.
What's the right way to do this?

[Eric Wieser]

start off with have : B := ...?

[Michael Beeson]

If I start with have:B :=
then once I've proved B, that environment will close, and I'll have to repeat the proof of B in order to continue with the proof of A.

[Michael Beeson]

T

[Eric Wieser]

Can you give a #mwe?

[Eric Wieser]

As long as you do the have before the split, then you can use it in both sides

[Michael Beeson]

I can't just move the split down to where B is deduced because there are a lot of rewrites of the goal above that point.

[Eric Wieser]

Rewrites will work on an and

[Eric Wieser]

Although apply will not do what you want

[Michael Beeson]

The rewrites will mess up the form of B. That might be OK, or work-aroundable, in a specific instance, but I thought maybe there is a standard, normal way to do this. If it requires a MWE to understand the question then it's clearly not the case that there's a standard way to do it that everybody but me already knows.

[Michael Beeson]

e.g. some command that says "export this result out of the split".

[Eric Wieser]

Any result that you were able to prove inside one branch of a split could have been proved before you entered the split at all

[Eric Wieser]

I'm asking for a #mwe because this feels like an #xy problem.

[Ruben Van de Velde]

You have goal A \and B, and you're doing split, have : B := ..., { prove A from B }, right? Move the have : B := ... bit before the split

[Mario Carneiro]

Michael Beeson said:

The rewrites will mess up the form of B. That might be OK, or work-aroundable, in a specific instance, but I thought maybe there is a standard, normal way to do this. If it requires a MWE to understand the question then it's clearly not the case that there's a standard way to do it that everybody but me already knows.

The point of the #mwe is to show a version of the problem you are talking about with the necessary features. It can be all foos and bars, it doesn't have to be your real example, but it's a lot easier to understand the exact situation and demonstrate a fix on a concrete problem rather than a prose description of one