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 lt_sup_of_lt_left lt_sup_of_lt_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