(a ⊔ b) ⊓ c ≤ a ⊔ (b ⊓ c)

Stream: new members

[anan]

When proving (a ⊔ b) ⊓ c ≤ a ⊔ (b ⊓ c), I got the following error when I wrote rw [inf_sup_right]. What is going on?
tactic 'rewrite' failed, did not find instance of the pattern in the target expression
(?a ⊔ ?b) ⊓ ?c
case a.a
a✝ b✝ c✝ d e f x✝³ y✝³ z✝² w : ℝ
R : Type u_1
inst✝⁷ : Ring R
A : Type u_2
inst✝⁶ : AddGroup A
G : Type u_3
inst✝⁵ : Group G
h✝ : a✝ ≤ b✝
h' : b✝ ≤ c✝
m n : ℕ

rw [inf_sup_right]    -- let (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c)
      apply sup_le
      · apply le_sup_of_le_left
        apply inf_le_left        -- a ⊓ c ≤ a
      · apply le_sup_right       -- b ⊓ c ≤ a ⊔ (b ⊓ c)

[Marcus Rossel]

Could you please post a #mwe?
Also #backticks.

[anan]

The problem lies in the last part of the proof - let (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c)

import Mathlib

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
  apply le_antisymm
  · -- a ⊔ (b ⊓ c) ≤ (a ⊔ b) ⊓ (a ⊔ c)
    apply le_inf
    · exact sup_le_sup_left (inf_le_left : b ⊓ c ≤ b) a
    · exact sup_le_sup_left (inf_le_right : b ⊓ c ≤ c) a
  · -- (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ (b ⊓ c)
    rw [h (a ⊔ b) a c]
    apply sup_le
    · -- (a ⊔ b) ⊓ a ≤ a ⊔ (b ⊓ c)
      rw [inf_comm]
      exact le_sup_of_le_left (inf_le_left : a ⊓ (a ⊔ b) ≤ a)
    · -- (a ⊔ b) ⊓ c ≤ a ⊔ (b ⊓ c)
      rw [inf_sup_right]    -- let (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c)
      apply sup_le
      · apply le_sup_of_le_left
        apply inf_le_left        -- a ⊓ c ≤ a
      · apply le_sup_right       -- b ⊓ c ≤ a ⊔ (b ⊓ c)

[Ruben Van de Velde]

docs#inf_sup_right requires a DistribLattice, which you didn't assume

[Ruben Van de Velde]

In fact, proving this relation seems to be exactly the point of the exercise

[anan]

thank you

[Philippe Duchon]

This is an exercise from Mathematics in Lean, right? The exercise is indeed about proving that either distributivity law implies the other.

[anan]

Philippe Duchon said:

This is an exercise from Mathematics in Lean, right? The exercise is indeed about proving that either distributivity law implies the other.

Yes, this is an exercise from Mathematics in Lean. I’m trying to learn lean programming through this book. If you have any suggestions for learning lean programming, please feel free to share them.