protected constructors

Stream: lean4

[Yakov Pechersky]

In mathlib3, we sometimes protect inductive constructors like so (from src#lift_rel.inl):

/-- Lifts pointwise two relations between `α` and `γ` and between `β` and `δ` to a relation between
`α ⊕ β` and `γ ⊕ δ`. -/
inductive lift_rel (r : α → γ → Prop) (s : β → δ → Prop) : α ⊕ β → γ ⊕ δ → Prop
| inl {a c} : r a c → lift_rel (inl a) (inl c)
| inr {b d} : s b d → lift_rel (inr b) (inr d)

attribute [protected] lift_rel.inl lift_rel.inr

What would be the equivalent for lean4 in this snippet?

namespace Sum

/-- Lifts pointwise two relations between `α` and `γ` and between `β` and `δ` to a relation between
`α ⊕ β` and `γ ⊕ δ`. -/
inductive LiftRel (r : α → γ → Prop) (s : β → δ → Prop) : Sum α β → Sum γ δ → Prop
| inl {a c} : r a c → LiftRel r s (.inl a) (.inl c)
| inr {b d} : s b d → LiftRel r s (.inr b) (.inr d)

end Sum

[Mario Carneiro]

/-- Lifts pointwise two relations between `α` and `γ` and between `β` and `δ` to a relation between
`α ⊕ β` and `γ ⊕ δ`. -/
inductive LiftRel (r : α → γ → Prop) (s : β → δ → Prop) : Sum α β → Sum γ δ → Prop
| protected inl {a c} : r a c → LiftRel r s (.inl a) (.inl c)
| protected inr {b d} : s b d → LiftRel r s (.inr b) (.inr d)