Implicit arguments in commutativity of ⊓ and ⊔

Stream: mathlib4

[Mitchell Lee]

Hi, I'm a beginner, so please forgive me if this is a stupid question. I'm currently working through Mathematics in Lean. One exercise is to prove that in a lattice, ⊓ distributes over ⊔ if and only if ⊔ distributes over ⊓, and one of the steps of the computation I use to prove this is

a ⊔ (c ⊓ a ⊔ c ⊓ b) = a ⊔ (a ⊓ c ⊔ b ⊓ c).

This step easily follows from the fact that the ⊓ operation is commutative (theorem inf_comm https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Lattice.html#inf_comm), so c ⊓ a = a ⊓ c and c ⊓ b = b ⊓ c. Normally, I would just write by rw [inf_comm c a, inf_comm c b] and be done with it, but the arguments to inf_comm are implicit, so I can't do that. I ended up using by simp [inf_comm]; surprisingly, not even by simp worked.

Is it a mistake that the arguments to inf_comm are implicit? All of the other commutativity theorems I found have explicit arguments.

[Jireh Loreaux]

from my perspective, yes, it seems like an oversight that they are implicit. However, you can work around this for now by doing inf_comm (a := c) (b := a). Lean 4 allows you to supply values to named implicit arguments with this syntax.

[Yaël Dillies]

Yes, they should be explicit, but I'm never annoyed enough to fix them

[Yaël Dillies]

#11033

[Mitchell Lee]

Thanks!