α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z : α
hxy : x ≤ y
hinf : y ⊓ z ≤ x ⊓ z
hsup : y ⊔ z ≤ x ⊔ z
h : y ≤ x ⊔ z
⊢ y ⊓ z ≤ x ⊓ z
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z : α
hxy : x ≤ y
hinf : y ⊓ z ≤ x ⊓ z
hsup : y ⊔ z ≤ x ⊔ z
h : y ≤ x ⊔ z
⊢ z ⊓ y ≤ z ⊓ x
rw [inf_comm, @inf_comm _ _ z]
no goals
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z : α
hxy : x ≤ y
hinf : y ⊓ z ≤ x ⊓ z
hsup : y ⊔ z ≤ x ⊔ z
h : y ≤ x ⊔ z
⊢ y ⊓ z ≤ x ⊓ z
exact hinf