Style question

Stream: new members

[Antoine Chambert-Loir]

Sometimes, a goal is split into some subgoals, and one would like to be able to use the result of one of them to prove the other ones.
One way is to prove it first, but is there a better way ?

[Johan Commelin]

Not really. There are some hacks, in case you don't want to state the subgoal explicitly. I have sometimes wished that there was better tooling for this.
For example, what you can do right now is:

have aux : _ := _, -- Lean is now confused about the type of `aux`, so there is an open metavariable and there will be two goals
some_tactic_that_creates_more_goals,
{ -- subproof 1
  exact aux },
{ -- subproof 2 (aux is now available in the context)
  tac1, tac2 },
{ -- we still need to prove aux
  abacadabra }

[Johan Commelin]

A sort of special case might be where you replace

some_tactic_that_creates_more_goals,
{ -- subproof 1
  exact aux },

with

refine my_lemma _ _ _ aux _ _ _,
-- now there are N remaining goals, they all have `aux` available in the context

[Mario Carneiro]

you can also write that have line as suffices aux,

[Eric Rodriguez]

flt_regular has a tactic may_assume which is also nice for these sorts of things.