attribute [intro]

Stream: new members

[Kenny Lau]

What does this attribute do? I saw it here:

inductive Exists {α : Sort u} (p : α → Prop) : Prop
| intro (w : α) (h : p w) : Exists

attribute [intro] Exists.intro

and when I hover it says "introduction rule for backward chaining"