## Stream: new members

### Topic: Passing implicit arguments explicitly

#### Vivek Rajesh Joshi (Jul 25 2023 at 18:18):

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 (Jul 25 2023 at 18:27):

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


#### Vivek Rajesh Joshi (Jul 25 2023 at 18:33):

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 (Jul 25 2023 at 19:15):

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 (Jul 25 2023 at 19:46):

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 (Jul 26 2023 at 04:28):

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

#### Yury G. Kudryashov (Jul 26 2023 at 04:29):

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

#### Yaël Dillies (Jul 26 2023 at 13:20):

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 (Jul 26 2023 at 13:21):

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

#### Yaël Dillies (Jul 26 2023 at 13:21):

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

#### Yury G. Kudryashov (Jul 26 2023 at 13:51):

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

#### Vivek Rajesh Joshi (Jul 27 2023 at 09:07):

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

Last updated: Dec 20 2023 at 11:08 UTC