Mistake

Stream: lean4

[Noah Noah]

Does someone know why it doesn't work?

axiom le_trans : ∀ a b c, a ≤ b → b ≤ c → a ≤ c

typeclass instance problem is stuck, it is often due to metavariables LE ?m.212

[Adam Topaz]

Can you please read the content of the following links and edit your question accordingly? #backticks #mwe

[Alex J. Best]

The issue is that Lean doesn't know what type a b c should be, what did you want there? Natural numbers, or some arbitrary type with a LE relation (less or equal).
You should check that adding an axiom is really what you want to do though. That is not a usual way of using Lean.
Instead you should probably work by assuming you have some type with a transitive LE relation. Normally we would write variable {X : Type*} [Preorder X] (which is a bit stronger but probably more useful). Then less or equal being transitive is an assumption for the current context, rather than an axiom of mathematics itself!