refine with holes

Stream: mathlib4

[Jon Eugster]

I think refine in lean3 used to have some sort of wildcard pattern. Is there something similar in Lean/mathlib nowadays?

import Mathlib

example {n : ℕ} [NeZero n] :
    let M := {A : Matrix (Fin n) (Fin n) ℝ | ∑ i, A i 0 = 0}
    Submodule ℝ (Matrix (Fin n) (Fin n) ℝ) := by
  refine { carrier := M, ?.. }  -- `?..` means that it's up to Lean to figure out which goals remain
  · sorry -- all remaining goals appear here
  · sorry
  · sorry
  done

This example is based on some work by @Thomas Murrills, but I'm not aware of this ever making it into mathlib.

Concretely, if the goal is a structure, I am looking for a good way to get one goal per field with the following restrictions:

• Must be a single-line syntax, in "tactic mode".
• Should need to specify the number of fields (because something like refine ⟨⟨⟨M, ?_⟩, ?_⟩, ?_⟩ is too hard to guess)
• Option to directly provide some (non-prop) fields.
• Remaining fields appear in the right order (e.g. constructor puts non-prop fields at the back. I get why, but it can also be really confusing to solve something about a thing ?f you haven't defined yet)

Or what is the recommended way to play around with a structure in tactic mode?

[Mario Carneiro]

you can use refine' with ..

[Jon Eugster]

Oh that's a good shout, I forgot that existed!