Not enough context in rewrites

Stream: lean4

[Devon Andrews]

I am currently working through "Mathematics in Lean" and reached chapter 2.5, where I need to prove that the distributivity laws a ⊔ (b ⊓ c) = (a ⊔ b) ⊓ (a ⊔ c) and a ⊓ (b ⊔ c) = a ⊓ b ⊔ a ⊓ c are equivalent. Here is my work

variable {α : Type*} [Lattice α]
variable (a b c : α)

example (h : ∀ x y z : α, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z)) : (a ⊔ b) ⊓ (a ⊔ c) = a ⊔ (b ⊓ c) := by
-- Switched sides in the theorem statement!
  calc
    (a ⊔ b) ⊓ (a ⊔ c) = ((a ⊔ b) ⊓ a) ⊔ ((a ⊔ b) ⊓ c) := by rw [h (a ⊔ b) a c]
    _ = (a ⊓ (a ⊔ b)) ⊔ (c ⊓ (a ⊔ b)) := by rw [inf_comm, inf_comm] -- Not enough context!
    _ = a ⊔ (c ⊓ (a ⊔ b)) := by rw [inf_sup_self]
    _ = a ⊔ ((c ⊓ a) ⊔ (c ⊓ b)) := by rw [h c a b]
    _ = a ⊔ ((a ⊓ c) ⊔ (c ⊓ b)) := by rw [inf_comm]
    _ = (a ⊔ (a ⊓ c)) ⊔ (b ⊓ c) := by rw [← sup_assoc] -- Not enough context!
    _ = a ⊔ (b ⊓ c) := by rw [sup_inf_self]

1. I found it easier to repeatedly apply h and simplify the right side of a ⊔ (b ⊓ c) = (a ⊔ b) ⊓ (a ⊔ c)in order to obtain the left side. However, this seems to "only" prove (a ⊔ b) ⊓ (a ⊔ c) = a ⊔ (b ⊓ c) (which is the same equation, but with reversed sides). I "fixed" this issue by switching both sides in the theorem statement itself. I was wondering how to tell lean that I want to prove the goal "the other way around".
2. Some rewrites require more context for lean to know how to apply the theorems the way I want to. I peaked into the solution and @inf_comm _ _ (a ⊔ b) seems to do the trick. I guess that the _'s are placeholders which I leave lean to figure out for itself. I was wondering how to fill these placeholders myself, i.e. what is the manual way to do these rewrites?

[Yaël Dillies]

You can rw [eq_comm]

[Kevin Buzzard]

docs#inf_comm

[Kevin Buzzard]

You can also write inf_comm (a := a \sup b) if you want to avoid the @

[Devon Andrews]

Sorry, question 2 had in fact multiple subquestions (which are still unanswered):

1. The solution is @inf_comm _ _ (a ⊔ b) or @inf_comm _ _ (a ⊔ b) a if I want to be more precise, but why do I need this format? What makes simply using inf_comm (a ⊔ b) a invalid?
2. If the _'s are placeholders, but what is lean filling in?
3. I don't get the syntax in the proposed alternative inf_comm (a := a ⊔ b). What's going on here?

[Devon Andrews]

Here is my current working solution:

variable {α : Type*} [Lattice α]
variable (a b c : α)

example (h : ∀ x y z : α, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z)) : a ⊔ (b ⊓ c) = (a ⊔ b) ⊓ (a ⊔ c) := by
  rw [@eq_comm α (a ⊔ (b ⊓ c)) ((a ⊔ b) ⊓ (a ⊔ c))]
  calc
    (a ⊔ b) ⊓ (a ⊔ c) = ((a ⊔ b) ⊓ a) ⊔ ((a ⊔ b) ⊓ c) := by rw [h (a ⊔ b) a c]
    _ = (a ⊓ (a ⊔ b)) ⊔ (c ⊓ (a ⊔ b)) := by rw [@inf_comm α _ (a ⊔ b) a, @inf_comm α _ (a ⊔ b) c]
    _ = a ⊔ (c ⊓ (a ⊔ b)) := by rw [@inf_sup_self α _ a b]
    _ = a ⊔ ((c ⊓ a) ⊔ (c ⊓ b)) := by rw [h c a b]
    _ = a ⊔ ((a ⊓ c) ⊔ (b ⊓ c)) := by rw [@inf_comm α _ c a, @inf_comm α _ c b]
    _ = (a ⊔ (a ⊓ c)) ⊔ (b ⊓ c) := by rw [← @sup_assoc α _ a (a ⊓ c) (b ⊓ c)]
    _ = a ⊔ (b ⊓ c) := by rw [@sup_inf_self α _ a c]

I figured out that α fits into the first placeholder.

[Kevin Buzzard]

Do you understand the difference between {} and () inputs to functions? If not then you might want to look at #tpil , it's chapter 6 or so