Multiple applies/exacts/haves in tactic mode

Stream: new members

[ZainAK283]

In tactic mode, you can combine "intro a" and "intro b" into "intros a b"
Is there a way to do this with apply, exact, and/or have?

[Yury G. Kudryashov]

exact closes the current goal, so what should do multiple exacts?

[Yury G. Kudryashov]

You can use refine instead of multiple applys

[Yury G. Kudryashov]

With mathlib you can write obtain ⟨a, b, c⟩ := (pa, pb, pc) where pa : a, pb : b, pc : c instead of have a := pa, have b := pb, have c := pc but I don't think that this is a good coding style.

[Yury G. Kudryashov]

obtain is have combined with rcases.

[Yury G. Kudryashov]

E.g., it's useful for obtain ⟨N, hN⟩ : ∃ N, ∀ n ≥ N, ... := ...

[Patrick Massot]

@ZainAK283 We would need a more specific question to help you. In a sense you can have "multiple exact" by providing a composite term in one exact. For instance, if your goal is a conjunction P ∧ Q and you
have hP : P and hQ : Q in your context, you can use split, exact hP, exact hQ but you can also use  exact ⟨hP, hQ⟩.

[Patrick Massot]

That being said, SSReflect make heavy use of a "multiple apply" that we don't have when they want to chain applications of lemmas, leaving hypotheses as side goals.

[Mario Carneiro]

exacts is actually a tactic