## Stream: Is there code for X?

### Topic: Copying projections through a definition

#### Eric Wieser (Sep 17 2020 at 18:31):

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 (Sep 17 2020 at 18:31):

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

Last updated: May 16 2021 at 05:21 UTC