α : Type u
β : Type v
inst✝ : SemilatticeSup α
a b c d x : α
⊢ (a ≤ x ∧ b ≤ x) ∧ c ≤ x ↔ a ≤ x ∧ b ≤ x ∧ c ≤ x
α : Type u
β : Type v
inst✝ : SemilatticeSup α
a b c d x : α
⊢ a ⊔ b ⊔ c ≤ x ↔ a ⊔ (b ⊔ c) ≤ x
simp only [sup_le_iff]
no goals
α : Type u
β : Type v
inst✝ : SemilatticeSup α
a b c d x : α
⊢ (a ≤ x ∧ b ≤ x) ∧ c ≤ x ↔ a ≤ x ∧ b ≤ x ∧ c ≤ x
rw [and_assoc]