case inl
α : Type u_1
β : Type ?u.16370
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3 : c ≤ b
h2 : a = c
⊢ c = a ∨ c = b

case inr
α : Type u_1
β : Type ?u.16370
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3 : c ≤ b
h2 : a < c
⊢ c = a ∨ c = b
α : Type u_1
β : Type ?u.16370
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2 : a ≤ c
h3 : c ≤ b
⊢ c = a ∨ c = b
rcases h2.eq_or_lt with (h2 | h2)
case inr.inl
α : Type u_1
β : Type ?u.16370
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3✝ : c ≤ b
h2 : a < c
h3 : c = b
⊢ c = a ∨ c = b

case inr.inr
α : Type u_1
β : Type ?u.16370
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3✝ : c ≤ b
h2 : a < c
h3 : c < b
⊢ c = a ∨ c = b
case inr
α : Type u_1
β : Type ?u.16370
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3 : c ≤ b
h2 : a < c
⊢ c = a ∨ c = b
rcases h3.eq_or_lt with (h3 | h3)
no goals
case inr.inr
α : Type u_1
β : Type ?u.16370
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3✝ : c ≤ b
h2 : a < c
h3 : c < b
⊢ c = a ∨ c = b
exact (h.2 h2 h3).elim
no goals
case inl
α : Type u_1
β : Type ?u.16370
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3 : c ≤ b
h2 : a = c
⊢ c = a ∨ c = b
exact Or.inl h2.symm
no goals
case inr.inl
α : Type u_1
β : Type ?u.16370
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3✝ : c ≤ b
h2 : a < c
h3 : c = b
⊢ c = a ∨ c = b
exact Or.inr h3