Lean4
/-- Construct a partial order from an `isStrictOrder` relation.
See note [reducible non-instances]. -/
abbrev partialOrderOfSO (r) [IsStrictOrder α r] : PartialOrder α
where
le x y := x = y ∨ r x y
lt := r
le_refl _ := Or.inl rfl
le_trans x y z h₁
h₂ :=
match y, z, h₁, h₂ with
| _, _, Or.inl rfl, h₂ => h₂
| _, _, h₁, Or.inl rfl => h₁
| _, _, Or.inr h₁, Or.inr h₂ => Or.inr (_root_.trans h₁ h₂)
le_antisymm x y h₁
h₂ :=
match y, h₁, h₂ with
| _, Or.inl rfl, _ => rfl
| _, _, Or.inl rfl => rfl
| _, Or.inr h₁, Or.inr h₂ => (asymm h₁ h₂).elim
lt_iff_le_not_ge x
y :=
⟨fun h => ⟨Or.inr h, not_or_intro (fun e => by rw [e] at h; exact irrefl _ h) (asymm h)⟩, fun ⟨h₁, h₂⟩ =>
h₁.resolve_left fun e => h₂ <| e ▸ Or.inl rfl⟩
