Controlling behavior of "and_intros" / "constructor" tactics

Stream: new members

[Nathan]

example {p k : ℕ} (hp : Nat.Prime p) (hk : 0 < k) : IsPrimePow (p^k) := by
  exists p, k; and_intros

This produces too many goals. On the other hand, constructor produces too few. Can we get finer control?

[Aaron Liu]

You can refine with exactly the amount of holes you want

[Nathan]

oh yeah refine ⟨?_, ?_, ?_⟩ works, thanks :pray: