A question in MIL at section 2.5

Stream: general

[YUAN Dong]

Hello everyone.

I met a question when finishing the exercises in MIL. It is about the proof of theorem absorb2.
In the solution below, after using le_trans , we want to prove x ⊔ x ⊓ y ≤ x fist. The answer uses sup_le to get 2 new goals ⊢ x ≤ x and ⊢ x ⊓ y ≤ x.
I do not understand why the 2 goals occurs. Does it mean that by default we compute x ⊓ y first in the expression x ⊔ x ⊓ y?

import MIL.Common
import Mathlib.Topology.MetricSpace.Basic

section
variable {α : Type*} [PartialOrder α]
variable (x y z : α)


section
variable {α : Type*} [Lattice α]
variable (x y z : α)


#check (inf_le_left : x ⊓ y ≤ x)
#check (inf_le_right : x ⊓ y ≤ y)
#check (le_inf : z ≤ x → z ≤ y → z ≤ x ⊓ y)
#check x ⊔ y
#check (le_sup_left : x ≤ x ⊔ y)
#check (le_sup_right : y ≤ x ⊔ y)
#check (sup_le : x ≤ z → y ≤ z → x ⊔ y ≤ z)

theorem absorb2 : x ⊔ x ⊓ y = x := by
  apply le_antisymm
  · apply sup_le
    · apply le_refl
    apply inf_le_left
  apply le_sup_left

Here are my thoughts.
I tried to solve the problem by prove x ⊔ x ⊓ y ≤ x ⊔ x = x, so I wrote

theorem absorb2 : x ⊔ x ⊓ y = x := by
  apply le_antisymm
  · apply inf_le_left : x ⊓ y ≤ x
  -- not finished
  apply le_sup_left

But I just got

tactic 'apply' failed, failed to unify
?a ⊓ ?b ≤ ?a
with
x ⊔ x ⊓ y ≤ x

for the line · apply inf_le_left : x ⊓ y ≤ x .
Please tell me Why can not I use inf_le_left here? It made me puzzle.

Best wishes.

[Yaël Dillies]

YUAN Dong said:

Does it mean that by default we compute x ⊓ y first in the expression x ⊔ x ⊓ y?

Yes, exactly. Try hovering over it in the infoview, you will see that x ⊔ x ⊓ y is secretly x ⊔ (x ⊓ y)