Passing implicit arguments explicitly

Stream: new members

[Vivek Rajesh Joshi]

I'm doing an exercise in the "Mathematics in Lean" book, where I have to prove that the infimum operator for a lattice is associative. I wish to create a hypothesis stating x \inf y <= x. How do I do so?

[Kevin Buzzard]

have foo : x \inf y \le x := by
  [insert proof here; I would start by trying `exact?`]

[Vivek Rajesh Joshi]

Got it, thanks. I was expecting the declaration to be similar to have h2 := min_le_left a b, but this works too. Speaking of which, could you tell me why min_le_left takes explicit arguments, while its infimum version is purely implicit?

[Kevin Buzzard]

It might be something to do with one of them being an explicit structure field whereas the other one was made afterwards. What are the exact declarations you're asking about? docs#min_le_left ?

[Eric Wieser]

I think we just don't have clear rules on implicit vs explicit, and as a result it's somewhat random depending on who wrote it and when

[Yury G. Kudryashov]

IMHO, we should change Lattice lemmas to use more explicit arguments.

[Yury G. Kudryashov]

BTW, in Lean 4 you can pass implicit arguments using inf_le_left (a := x) (b := y)

[Yaël Dillies]

Yury G. Kudryashov said:

IMHO, we should change Lattice lemmas to use more explicit arguments.

In fact I believe we should go the other way around

[Yaël Dillies]

I barely ever explicitate the arguments to any lemma with a ≤ conclusion.

[Yaël Dillies]

The many underscores that my proof terms inherit because of this are just noise.

[Yury G. Kudryashov]

As you can see, two very active Lean users have opposite opinions on this question...

[Vivek Rajesh Joshi]

Kevin Buzzard said:

It might be something to do with one of them being an explicit structure field whereas the other one was made afterwards. What are the exact declarations you're asking about? docs#min_le_left ?

I was talking about this one: min_le_left.{u} {α : Type u} [inst✝ : LinearOrder α] (a b : α) : min a b ≤ a
But anyways, I got my question(s) answered, so all's good