α : Type u_1
β : Type ?u.16828
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
⊢ c = a ∨ c = b → a ≤ c ∧ c ≤ b
α : Type u_1
β : Type ?u.16828
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
⊢ a ≤ c ∧ c ≤ b ↔ c = a ∨ c = b
refine' ⟨fun h2 => h.eq_or_eq h2.1 h2.2, _⟩
case inl
α : Type u_1
β : Type ?u.16828
inst✝ : PartialOrder α
b c : α
h : c ⩿ b
⊢ c ≤ c ∧ c ≤ b

case inr
α : Type u_1
β : Type ?u.16828
inst✝ : PartialOrder α
a c : α
h : a ⩿ c
⊢ a ≤ c ∧ c ≤ c
α : Type u_1
β : Type ?u.16828
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
⊢ c = a ∨ c = b → a ≤ c ∧ c ≤ b
rintro (rfl | rfl)
no goals
case inl
α : Type u_1
β : Type ?u.16828
inst✝ : PartialOrder α
b c : α
h : c ⩿ b
⊢ c ≤ c ∧ c ≤ b

case inr
α : Type u_1
β : Type ?u.16828
inst✝ : PartialOrder α
a c : α
h : a ⩿ c
⊢ a ≤ c ∧ c ≤ c
exacts [⟨le_rfl, h.le⟩, ⟨h.le, le_rfl⟩]