no goals
α : Type u
β : Type v
inst✝ : LinearOrder α
a b c d : α
⊢ a ≤ b ⊔ c ↔ a ≤ b ∨ a ≤ c
exact ⟨fun h =>
  (le_total c b).imp
    (fun bc => by rwa [sup_eq_left.2 bc] at h)
    (fun bc => by rwa [sup_eq_right.2 bc] at h),
  fun h => h.elim le_sup_of_le_left le_sup_of_le_right⟩
no goals
α : Type u
β : Type v
inst✝ : LinearOrder α
a b c d : α
h : a ≤ b ⊔ c
bc : c ≤ b
⊢ a ≤ b
rwa [sup_eq_left.2 bc] at h
no goals
α : Type u
β : Type v
inst✝ : LinearOrder α
a b c d : α
h : a ≤ b ⊔ c
bc : b ≤ c
⊢ a ≤ c
rwa [sup_eq_right.2 bc] at h