no goals
α : Type u
β : Type v
inst✝ : DistribLattice α
x y z : α
⊢ x ⊓ (y ⊔ z) = x ⊓ (x ⊔ z) ⊓ (y ⊔ z)
rw [inf_sup_self]
no goals
α : Type u
β : Type v
inst✝ : DistribLattice α
x y z : α
⊢ x ⊓ (x ⊔ z) ⊓ (y ⊔ z) = x ⊓ (x ⊓ y ⊔ z)
simp only [inf_assoc, sup_inf_right, eq_self_iff_true]
no goals
α : Type u
β : Type v
inst✝ : DistribLattice α
x y z : α
⊢ x ⊓ (x ⊓ y ⊔ z) = (x ⊔ x ⊓ y) ⊓ (x ⊓ y ⊔ z)
rw [sup_inf_self]
no goals
α : Type u
β : Type v
inst✝ : DistribLattice α
x y z : α
⊢ (x ⊔ x ⊓ y) ⊓ (x ⊓ y ⊔ z) = (x ⊓ y ⊔ x) ⊓ (x ⊓ y ⊔ z)
rw [sup_comm]
no goals
α : Type u
β : Type v
inst✝ : DistribLattice α
x y z : α
⊢ (x ⊓ y ⊔ x) ⊓ (x ⊓ y ⊔ z) = x ⊓ y ⊔ x ⊓ z
rw [sup_inf_left]