Support autoParam in structure fields

[dselsam]

The following work:

def FooD (x y : Nat) (h : x = y := by rfl) : Unit := ()

example : Unit := FooD 1 1

inductive FooI where
  | mk (x y : Nat) (h : x = y := by rfl)

example : FooI := FooI.mk 1 1

But this does not:

structure FooS where
  x : Nat
  y : Nat
  h : x = y := by rfl -- error: type mismatch

[sgouezel]

A weird example of the above, which is used a lot in mathlib, is when a field is defined in some structure foo, and the autoParam is provided in a structure extending foo. Like in

structure FooS where
  x : Nat
  y : Nat
  h : x = y

structure BarS extends FooS where 
  h' : x = y
  h := h'

The reason is that BarS may include new axioms that make it possible to prove automatically h from other fields, while it wasn't the case in FooS.