anonymous constructor notation does not make use of default values

-- mathlib3 did not allow relying on default field values when using anonymous constructor notation:
structure Q :=
(n : nat)
(m : nat := 0)

example : Q := ⟨0⟩  -- fails

-- however it did allow using `auto_param`s.
meta def s : tactic unit := `[simp]

structure P :=
(n : nat)
(w : n = 0 . s)

example : P := ⟨0⟩

-- in Lean 4, these have been combined into the same syntax,
-- and neither can be used in anonymous constructor notation:
structure P where
  n : Nat
  w : n = 0 := by simp

example : P := ⟨0⟩  


structure Q where
  n : Nat
  m : Nat := 0

example : Q := ⟨0⟩  

Start with the anonymous constructor examples in the issue and trace the elaboration path for structure fields with default values or tactic values. Done means both P := ⟨0⟩ and Q := ⟨0⟩ examples elaborate successfully.