does the `variable` keyword also create proofs?

Stream: new members

[Filippo Cozzi]

(sorry if I'm using this site wrong, I am really new to all this)
I'm going through "theorem proving in lean 4" and I have trouble with their choice of terms in the section "quantifiers and equality". In an example they show this:

variable (\alpha : Type) (r : \alpha -> \alpha -> Prop)
variable (trans_r : \forall x y z : \alpha, r x y -> r y z -> r x z)

and then it says that providing trans_r a b c where (a b c : \alpha) yields a proof of transitivity of r. But how is this a proof? How can variable guarantee that a proof trans_r of that type actually exist? Wouldn't this just be the hypothesis that a proof of type r a b -> r b c -> r a c exists, as a way of assuming transitivity for r?
What I mean is, trans_r a b c does not explicitly construct an element/proof of that type, right?

[Ruben Van de Velde]

variable introduces a hypothesis. That is, if you write a theorem after that, it's a theorem whose conclusion is true assuming the transitivity, and someone who wants to use your theorem needs to supply a proof of transitivity

[Filippo Cozzi]

and does having written those variables like this mean that, from that point on, whenever I use r in the hypotheses of a theorem, lean will implicitly also add (trans_r : ...) as a hypothesis? Or do I have to explicitly use trans_r inside the proof of the theorem?

[Robin Arnez]

I believe you have to include trans_r in or something

[Kyle Miller]

A way to be sure is to check the type of the theorem. You can hover over the theorem name or do something like #check yourThmName.

For theorems, you can also be sure what the type will be by seeing what hypotheses are available from within the proof. Using include is a way to make sure certain hypotheses are included even if the theorem statement doesn't otherwise mention them, which is what the auto-inclusion algorithm makes use of.