Structure inheritance

Stream: mathlib4

[Yaël Dillies]

What's the Lean 4 syntax to inherit fields from two existing ones? I tried

{ ‹LinearOrderedCommGroup α›,
  ..OrderedCommGroup.to_OrderedCancelCommMonoid }

in mathlib4#913, with little success.

[Floris van Doorn]

I believe it's {foo1, foo2 with }