Copying projections through a definition

Stream: Is there code for X?

[Eric Wieser]

In congruence.lean, there are definitions like

  /-- Defining the quotient by a ring congruence relation of a type with a multiplication. -/
  protected def quotient := quotient $ c.to_setoid

  /-- The function on the quotient by a congruence relation `c` induced by a function that is
      constant on `c`'s equivalence classes. -/
  @[elab_as_eliminator]
  protected def lift_on {β} {c : ring_con M} (q : c.quotient) (f : M → β)
    (h : ∀ a b, c a b → f a = f b) : β := quotient.lift_on' q f h

  /-- The binary function on the quotient by a ring congruence relation `c` induced by a binary function
      that is constant on `c`'s equivalence classes. -/
  @[elab_as_eliminator]
  protected def lift_on₂ {β} {c : ring_con M} (q r : c.quotient) (f : M → M → β)
    (h : ∀ a₁ a₂ b₁ b₂, c a₁ b₁ → c a₂ b₂ → f a₁ a₂ = f b₁ b₂) : β := quotient.lift_on₂' q r f h

This seems awfully verbose. Is there a way of telling lean that when I write def quotient := quotient $ c.to_setoid I also want to copy over a bunch of the projections?

[Eric Wieser]

And if not, is there a way I can at least avoid writing out the full lemma each time?