Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Yaël Dillies

! This file was ported from Lean 3 source module order.circular
! leanprover-community/mathlib commit 213b0cff7bc5ab6696ee07cceec80829ce42efec
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Set.Basic

/-!
# Circular order hierarchy

This file defines circular preorders, circular partial orders and circular orders.

## Hierarchy

* A ternary "betweenness" relation `btw : α → α → α → Prop` forms a `CircularOrder` if it is
- reflexive: `btw a a a`
- cyclic: `btw a b c → btw b c a`
- antisymmetric: `btw a b c → btw c b a → a = b ∨ b = c ∨ c = a`
- total: `btw a b c ∨ btw c b a`
along with a strict betweenness relation `sbtw : α → α → α → Prop` which respects
`sbtw a b c ↔ btw a b c ∧ ¬ btw c b a`, analogously to how `<` and `≤` are related, and is
- transitive: `sbtw a b c → sbtw b d c → sbtw a d c`.
* A `CircularPartialOrder` drops totality.
* A `CircularPreorder` further drops antisymmetry.

The intuition is that a circular order is a circle and `btw a b c` means that going around
clockwise from `a` you reach `b` before `c` (`b` is between `a` and `c` is meaningless on an
unoriented circle). A circular partial order is several, potentially intersecting, circles. A
circular preorder is like a circular partial order, but several points can coexist.

Note that the relations between `CircularPreorder`, `CircularPartialOrder` and `CircularOrder`
are subtler than between `Preorder`, `PartialOrder`, `LinearOrder`. In particular, one cannot
simply extend the `btw` of a `CircularPartialOrder` to make it a `CircularOrder`.

One can translate from usual orders to circular ones by "closing the necklace at infinity". See
`LE.toBtw` and `LT.toSBtw`. Going the other way involves "cutting the necklace" or
"rolling the necklace open".

## Examples

Some concrete circular orders one encounters in the wild are `ZMod n` for `0 < n`, `Circle`,
`Real.Angle`...

## Main definitions

* `Set.cIcc`: Closed-closed circular interval.
* `Set.cIoo`: Open-open circular interval.

## Notes

There's an unsolved diamond on `OrderDual α` here. The instances `LE α → Btw αᵒᵈ` and
`LT α → SBtw αᵒᵈ` can each be inferred in two ways:
* `LE α` → `Btw α` → `Btw αᵒᵈ` vs
`LE α` → `LE αᵒᵈ` → `Btw αᵒᵈ`
* `LT α` → `SBtw α` → `SBtw αᵒᵈ` vs
`LT α` → `LT αᵒᵈ` → `SBtw αᵒᵈ`
The fields are propeq, but not defeq. It is temporarily fixed by turning the circularizing instances
into definitions.

## TODO

Antisymmetry is quite weak in the sense that there's no way to discriminate which two points are
equal. This prevents defining closed-open intervals `cIco` and `cIoc` in the neat `=`-less way. We
currently haven't defined them at all.

What is the correct generality of "rolling the necklace" open? At least, this works for `α × β` and
`β × α` where `α` is a circular order and `β` is a linear order.

What's next is to define circular groups and provide instances for `ZMod n`, the usual circle group
`Circle`, and `RootsOfUnity M`. What conditions do we need on `M` for this last one
to work?

We should have circular order homomorphisms. The typical example is
`days_to_month : days_of_the_year →c months_of_the_year` which relates the circular order of days
and the circular order of months. Is `α →c β` a good notation?

## References

* https://en.wikipedia.org/wiki/Cyclic_order
* https://en.wikipedia.org/wiki/Partial_cyclic_order

## Tags

circular order, cyclic order, circularly ordered set, cyclically ordered set
-/

/-- Syntax typeclass for a betweenness relation. -/
class Btw: {α : Type u_1} → (α → α → α → Prop) → Btw αBtw (α: Type ?u.2α : Type _: Type (?u.2+1)Type _) where
/-- Betweenness for circular orders. `btw a b c` states that `b` is between `a` and `c` (in that
order). -/
btw: {α : Type u_1} → [self : Btw α] → α → α → α → Propbtw : α: Type ?u.2α → α: Type ?u.2α → α: Type ?u.2α → Prop: TypeProp
#align has_btw Btw: Type u_1 → Type u_1Btw

export Btw (btw)

/-- Syntax typeclass for a strict betweenness relation. -/
class SBtw: Type u_1 → Type u_1SBtw (α: Type ?u.18α : Type _: Type (?u.18+1)Type _) where
/-- Strict betweenness for circular orders. `sbtw a b c` states that `b` is strictly between `a`
and `c` (in that order). -/
sbtw: {α : Type u_1} → [self : SBtw α] → α → α → α → Propsbtw : α: Type ?u.18α → α: Type ?u.18α → α: Type ?u.18α → Prop: TypeProp
#align has_sbtw SBtw: Type u_1 → Type u_1SBtw

export SBtw (sbtw)

/-- A circular preorder is the analogue of a preorder where you can loop around. `≤` and `<` are
replaced by ternary relations `btw` and `sbtw`. `btw` is reflexive and cyclic. `sbtw` is transitive.
-/
class CircularPreorder: {α : Type u_1} →
[toBtw : Btw α] →
[toSBtw : SBtw α] →
(∀ (a : α), Btw.btw a a a) →
(∀ {a b c : α}, Btw.btw a b c → Btw.btw b c a) →
autoParam (∀ {a b c : α}, SBtw.sbtw a b c ↔ Btw.btw a b c ∧ ¬Btw.btw c b a) _auto✝ →
(∀ {a b c d : α}, SBtw.sbtw a b c → SBtw.sbtw b d c → SBtw.sbtw a d c) → CircularPreorder αCircularPreorder (α: Type ?u.105α : Type _: Type (?u.105+1)Type _) extends Btw: Type ?u.110 → Type ?u.110Btw α: Type ?u.105α, SBtw: Type ?u.114 → Type ?u.114SBtw α: Type ?u.105α where
/-- `a` is between `a` and `a`. -/
btw_refl: ∀ {α : Type u_1} [self : CircularPreorder α] (a : α), Btw.btw a a abtw_refl (a: αa : α: Type ?u.105α) : btw: α → α → α → Propbtw a: αa a: αa a: αa
/-- If `b` is between `a` and `c`, then `c` is between `b` and `a`.
This is motivated by imagining three points on a circle. -/
btw_cyclic_left: ∀ {α : Type u_1} [self : CircularPreorder α] {a b c : α}, Btw.btw a b c → Btw.btw b c abtw_cyclic_left {a: αa b: αb c: αc : α: Type ?u.105α} : btw: α → α → α → Propbtw a: αa b: αb c: αc → btw: α → α → α → Propbtw b: αb c: αc a: αa
sbtw := fun a: ?m.132a b: ?m.135b c: ?m.138c => btw: α → α → α → Propbtw a: ?m.132a b: ?m.135b c: ?m.138c ∧ ¬btw: α → α → α → Propbtw c: ?m.138c b: ?m.135b a: ?m.132a
/-- Strict betweenness is given by betweenness in one direction and non-betweenness in the other.

I.e., if `b` is between `a` and `c` but not between `c` and `a`, then we say `b` is strictly
between `a` and `c`. -/
sbtw_iff_btw_not_btw: ∀ {α : Type u_1} [self : CircularPreorder α] {a b c : α}, SBtw.sbtw a b c ↔ Btw.btw a b c ∧ ¬Btw.btw c b asbtw_iff_btw_not_btw {a: αa b: αb c: αc : α: Type ?u.105α} : sbtw: α → α → α → Propsbtw a: αa b: αb c: αc ↔ btw: α → α → α → Propbtw a: αa b: αb c: αc ∧ ¬btw: α → α → α → Propbtw c: αc b: αb a: αa := by intros; rfl
/-- For any fixed `c`, `fun a b ↦ sbtw a b c` is a transitive relation.

I.e., given `a` `b` `d` `c` in that "order", if we have `b` strictly between `a` and `c`, and `d`
strictly between `b` and `c`, then `d` is strictly between `a` and `c`. -/
sbtw_trans_left: ∀ {α : Type u_1} [self : CircularPreorder α] {a b c d : α}, SBtw.sbtw a b c → SBtw.sbtw b d c → SBtw.sbtw a d csbtw_trans_left {a: αa b: αb c: αc d: αd : α: Type ?u.105α} : sbtw: α → α → α → Propsbtw a: αa b: αb c: αc → sbtw: α → α → α → Propsbtw b: αb d: αd c: αc → sbtw: α → α → α → Propsbtw a: αa d: αd c: αc
#align circular_preorder CircularPreorder: Type u_1 → Type u_1CircularPreorder

export CircularPreorder (btw_refl btw_cyclic_left sbtw_trans_left)

/-- A circular partial order is the analogue of a partial order where you can loop around. `≤` and
`<` are replaced by ternary relations `btw` and `sbtw`. `btw` is reflexive, cyclic and
antisymmetric. `sbtw` is transitive. -/
class CircularPartialOrder: Type u_1 → Type u_1CircularPartialOrder (α: Type ?u.217α : Type _: Type (?u.217+1)Type _) extends CircularPreorder: Type ?u.222 → Type ?u.222CircularPreorder α: Type ?u.217α where
/-- If `b` is between `a` and `c` and also between `c` and `a`, then at least one pair of points
among `a`, `b`, `c` are identical. -/
btw_antisymm: ∀ {α : Type u_1} [self : CircularPartialOrder α] {a b c : α}, Btw.btw a b c → Btw.btw c b a → a = b ∨ b = c ∨ c = abtw_antisymm {a: αa b: αb c: αc : α: Type ?u.217α} : btw: α → α → α → Propbtw a: αa b: αb c: αc → btw: α → α → α → Propbtw c: αc b: αb a: αa → a: αa = b: αb ∨ b: αb = c: αc ∨ c: αc = a: αa
#align circular_partial_order CircularPartialOrder: Type u_1 → Type u_1CircularPartialOrder

export CircularPartialOrder (btw_antisymm)

/-- A circular order is the analogue of a linear order where you can loop around. `≤` and `<` are
replaced by ternary relations `btw` and `sbtw`. `btw` is reflexive, cyclic, antisymmetric and total.
`sbtw` is transitive. -/
class CircularOrder: {α : Type u_1} →
[toCircularPartialOrder : CircularPartialOrder α] → (∀ (a b c : α), Btw.btw a b c ∨ Btw.btw c b a) → CircularOrder αCircularOrder (α: Type ?u.296α : Type _: Type (?u.296+1)Type _) extends CircularPartialOrder: Type ?u.301 → Type ?u.301CircularPartialOrder α: Type ?u.296α where
/-- For any triple of points, the second is between the other two one way or another. -/
btw_total: ∀ {α : Type u_1} [self : CircularOrder α] (a b c : α), Btw.btw a b c ∨ Btw.btw c b abtw_total : ∀ a: αa b: αb c: αc : α: Type ?u.296α, btw: α → α → α → Propbtw a: αa b: αb c: αc ∨ btw: α → α → α → Propbtw c: αc b: αb a: αa
#align circular_order CircularOrder: Type u_1 → Type u_1CircularOrder

export CircularOrder (btw_total)

/-! ### Circular preorders -/

section CircularPreorder

variable {α: Type ?u.1009α : Type _: Type (?u.922+1)Type _} [CircularPreorder: Type ?u.1012 → Type ?u.1012CircularPreorder α: Type ?u.428α]

theorem btw_rfl: ∀ {α : Type u_1} [inst : CircularPreorder α] {a : α}, btw a a abtw_rfl {a: αa : α: Type ?u.377α} : btw: {α : Type ?u.385} → [self : Btw α] → α → α → α → Propbtw a: αa a: αa a: αa :=
btw_refl: ∀ {α : Type ?u.408} [self : CircularPreorder α] (a : α), btw a a abtw_refl _: ?m.409_
#align btw_rfl btw_rfl: ∀ {α : Type u_1} [inst : CircularPreorder α] {a : α}, btw a a abtw_rfl

-- TODO: `alias` creates a def instead of a lemma.
-- alias btw_cyclic_left        ← has_btw.btw.cyclic_left
theorem Btw.btw.cyclic_left: ∀ {a b c : α}, btw a b c → btw b c aBtw.btw.cyclic_left {a: αa b: αb c: αc : α: Type ?u.428α} (h: btw a b ch : btw: {α : Type ?u.440} → [self : Btw α] → α → α → α → Propbtw a: αa b: αb c: αc) : btw: {α : Type ?u.462} → [self : Btw α] → α → α → α → Propbtw b: αb c: αc a: αa :=
btw_cyclic_left: ∀ {α : Type ?u.481} [self : CircularPreorder α] {a b c : α}, btw a b c → btw b c abtw_cyclic_left h: btw a b ch
#align has_btw.btw.cyclic_left Btw.btw.cyclic_left: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, btw a b c → btw b c aBtw.btw.cyclic_left

theorem btw_cyclic_right: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, btw a b c → btw c a bbtw_cyclic_right {a: αa b: αb c: αc : α: Type ?u.506α} (h: btw a b ch : btw: {α : Type ?u.518} → [self : Btw α] → α → α → α → Propbtw a: αa b: αb c: αc) : btw: {α : Type ?u.540} → [self : Btw α] → α → α → α → Propbtw c: αc a: αa b: αb :=
h: btw a b ch.cyclic_left: ∀ {α : Type ?u.559} [inst : CircularPreorder α] {a b c : α}, btw a b c → btw b c acyclic_left.cyclic_left: ∀ {α : Type ?u.574} [inst : CircularPreorder α] {a b c : α}, btw a b c → btw b c acyclic_left
#align btw_cyclic_right btw_cyclic_right: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, btw a b c → btw c a bbtw_cyclic_right

alias btw_cyclic_right: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, btw a b c → btw c a bbtw_cyclic_right ← Btw.btw.cyclic_right: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, btw a b c → btw c a bBtw.btw.cyclic_right
#align has_btw.btw.cyclic_right Btw.btw.cyclic_right: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, btw a b c → btw c a bBtw.btw.cyclic_right

/-- The order of the `↔` has been chosen so that `rw btw_cyclic` cycles to the right while
`rw ←btw_cyclic` cycles to the left (thus following the prepended arrow). -/
theorem btw_cyclic: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, btw a b c ↔ btw c a bbtw_cyclic {a: αa b: αb c: αc : α: Type ?u.593α} : btw: {α : Type ?u.605} → [self : Btw α] → α → α → α → Propbtw a: αa b: αb c: αc ↔ btw: {α : Type ?u.618} → [self : Btw α] → α → α → α → Propbtw c: αc a: αa b: αb :=
⟨btw_cyclic_right: ∀ {α : Type ?u.633} [inst : CircularPreorder α] {a b c : α}, btw a b c → btw c a bbtw_cyclic_right, btw_cyclic_left: ∀ {α : Type ?u.654} [self : CircularPreorder α] {a b c : α}, btw a b c → btw b c abtw_cyclic_left⟩
#align btw_cyclic btw_cyclic: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, btw a b c ↔ btw c a bbtw_cyclic

theorem sbtw_iff_btw_not_btw: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c ↔ btw a b c ∧ ¬btw c b asbtw_iff_btw_not_btw {a: αa b: αb c: αc : α: Type ?u.672α} : sbtw: {α : Type ?u.684} → [self : SBtw α] → α → α → α → Propsbtw a: αa b: αb c: αc ↔ btw: {α : Type ?u.697} → [self : Btw α] → α → α → α → Propbtw a: αa b: αb c: αc ∧ ¬btw: {α : Type ?u.707} → [self : Btw α] → α → α → α → Propbtw c: αc b: αb a: αa :=
CircularPreorder.sbtw_iff_btw_not_btw: ∀ {α : Type ?u.714} [self : CircularPreorder α] {a b c : α}, sbtw a b c ↔ btw a b c ∧ ¬btw c b aCircularPreorder.sbtw_iff_btw_not_btw
#align sbtw_iff_btw_not_btw sbtw_iff_btw_not_btw: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c ↔ btw a b c ∧ ¬btw c b asbtw_iff_btw_not_btw

theorem btw_of_sbtw: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → btw a b cbtw_of_sbtw {a: αa b: αb c: αc : α: Type ?u.742α} (h: sbtw a b ch : sbtw: {α : Type ?u.754} → [self : SBtw α] → α → α → α → Propsbtw a: αa b: αb c: αc) : btw: {α : Type ?u.776} → [self : Btw α] → α → α → α → Propbtw a: αa b: αb c: αc :=
(sbtw_iff_btw_not_btw: ∀ {α : Type ?u.802} [inst : CircularPreorder α] {a b c : α}, sbtw a b c ↔ btw a b c ∧ ¬btw c b asbtw_iff_btw_not_btw.1: ∀ {a b : Prop}, (a ↔ b) → a → b1 h: sbtw a b ch).1: ∀ {a b : Prop}, a ∧ b → a1
#align btw_of_sbtw btw_of_sbtw: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → btw a b cbtw_of_sbtw

alias btw_of_sbtw: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → btw a b cbtw_of_sbtw ← SBtw.sbtw.btw: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → btw a b cSBtw.sbtw.btw
#align has_sbtw.sbtw.btw SBtw.sbtw.btw: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → btw a b cSBtw.sbtw.btw

theorem not_btw_of_sbtw: ∀ {a b c : α}, sbtw a b c → ¬btw c b anot_btw_of_sbtw {a: αa b: αb c: αc : α: Type ?u.835α} (h: sbtw a b ch : sbtw: {α : Type ?u.847} → [self : SBtw α] → α → α → α → Propsbtw a: αa b: αb c: αc) : ¬btw: {α : Type ?u.869} → [self : Btw α] → α → α → α → Propbtw c: αc b: αb a: αa :=
(sbtw_iff_btw_not_btw: ∀ {α : Type ?u.888} [inst : CircularPreorder α] {a b c : α}, sbtw a b c ↔ btw a b c ∧ ¬btw c b asbtw_iff_btw_not_btw.1: ∀ {a b : Prop}, (a ↔ b) → a → b1 h: sbtw a b ch).2: ∀ {a b : Prop}, a ∧ b → b2
#align not_btw_of_sbtw not_btw_of_sbtw: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → ¬btw c b anot_btw_of_sbtw

alias not_btw_of_sbtw: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → ¬btw c b anot_btw_of_sbtw ← SBtw.sbtw.not_btw: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → ¬btw c b aSBtw.sbtw.not_btw
#align has_sbtw.sbtw.not_btw SBtw.sbtw.not_btw: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → ¬btw c b aSBtw.sbtw.not_btw

theorem not_sbtw_of_btw: ∀ {a b c : α}, btw a b c → ¬sbtw c b anot_sbtw_of_btw {a: αa b: αb c: αc : α: Type ?u.922α} (h: btw a b ch : btw: {α : Type ?u.934} → [self : Btw α] → α → α → α → Propbtw a: αa b: αb c: αc) : ¬sbtw: {α : Type ?u.956} → [self : SBtw α] → α → α → α → Propsbtw c: αc b: αb a: αa := fun h': ?m.976h' => h': ?m.976h'.not_btw: ∀ {α : Type ?u.978} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → ¬btw c b anot_btw h: btw a b ch
#align not_sbtw_of_btw not_sbtw_of_btw: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, btw a b c → ¬sbtw c b anot_sbtw_of_btw

alias not_sbtw_of_btw: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, btw a b c → ¬sbtw c b anot_sbtw_of_btw ← Btw.btw.not_sbtw: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, btw a b c → ¬sbtw c b aBtw.btw.not_sbtw
#align has_btw.btw.not_sbtw Btw.btw.not_sbtw: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, btw a b c → ¬sbtw c b aBtw.btw.not_sbtw

theorem sbtw_of_btw_not_btw: ∀ {a b c : α}, btw a b c → ¬btw c b a → sbtw a b csbtw_of_btw_not_btw {a: αa b: αb c: αc : α: Type ?u.1009α} (habc: btw a b chabc : btw: {α : Type ?u.1021} → [self : Btw α] → α → α → α → Propbtw a: αa b: αb c: αc) (hcba: ¬btw c b ahcba : ¬btw: {α : Type ?u.1043} → [self : Btw α] → α → α → α → Propbtw c: αc b: αb a: αa) : sbtw: {α : Type ?u.1048} → [self : SBtw α] → α → α → α → Propsbtw a: αa b: αb c: αc :=
sbtw_iff_btw_not_btw: ∀ {α : Type ?u.1076} [inst : CircularPreorder α] {a b c : α}, sbtw a b c ↔ btw a b c ∧ ¬btw c b asbtw_iff_btw_not_btw.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 ⟨habc: btw a b chabc, hcba: ¬btw c b ahcba⟩
#align sbtw_of_btw_not_btw sbtw_of_btw_not_btw: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, btw a b c → ¬btw c b a → sbtw a b csbtw_of_btw_not_btw

alias sbtw_of_btw_not_btw: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, btw a b c → ¬btw c b a → sbtw a b csbtw_of_btw_not_btw ← Btw.btw.sbtw_of_not_btw: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, btw a b c → ¬btw c b a → sbtw a b cBtw.btw.sbtw_of_not_btw
#align has_btw.btw.sbtw_of_not_btw Btw.btw.sbtw_of_not_btw: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, btw a b c → ¬btw c b a → sbtw a b cBtw.btw.sbtw_of_not_btw

theorem sbtw_cyclic_left: ∀ {a b c : α}, sbtw a b c → sbtw b c asbtw_cyclic_left {a: αa b: αb c: αc : α: Type ?u.1115α} (h: sbtw a b ch : sbtw: {α : Type ?u.1127} → [self : SBtw α] → α → α → α → Propsbtw a: αa b: αb c: αc) : sbtw: {α : Type ?u.1149} → [self : SBtw α] → α → α → α → Propsbtw b: αb c: αc a: αa :=
h: sbtw a b ch.btw: ∀ {α : Type ?u.1168} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → btw a b cbtw.cyclic_left: ∀ {α : Type ?u.1183} [inst : CircularPreorder α] {a b c : α}, btw a b c → btw b c acyclic_left.sbtw_of_not_btw: ∀ {α : Type ?u.1194} [inst : CircularPreorder α] {a b c : α}, btw a b c → ¬btw c b a → sbtw a b csbtw_of_not_btw fun h': ?m.1208h' => h: sbtw a b ch.not_btw: ∀ {α : Type ?u.1210} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → ¬btw c b anot_btw h': ?m.1208h'.cyclic_left: ∀ {α : Type ?u.1223} [inst : CircularPreorder α] {a b c : α}, btw a b c → btw b c acyclic_left
#align sbtw_cyclic_left sbtw_cyclic_left: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → sbtw b c asbtw_cyclic_left

alias sbtw_cyclic_left: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → sbtw b c asbtw_cyclic_left ← SBtw.sbtw.cyclic_left: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → sbtw b c aSBtw.sbtw.cyclic_left
#align has_sbtw.sbtw.cyclic_left SBtw.sbtw.cyclic_left: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → sbtw b c aSBtw.sbtw.cyclic_left

theorem sbtw_cyclic_right: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → sbtw c a bsbtw_cyclic_right {a: αa b: αb c: αc : α: Type ?u.1244α} (h: sbtw a b ch : sbtw: {α : Type ?u.1256} → [self : SBtw α] → α → α → α → Propsbtw a: αa b: αb c: αc) : sbtw: {α : Type ?u.1278} → [self : SBtw α] → α → α → α → Propsbtw c: αc a: αa b: αb :=
h: sbtw a b ch.cyclic_left: ∀ {α : Type ?u.1297} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → sbtw b c acyclic_left.cyclic_left: ∀ {α : Type ?u.1312} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → sbtw b c acyclic_left
#align sbtw_cyclic_right sbtw_cyclic_right: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → sbtw c a bsbtw_cyclic_right

alias sbtw_cyclic_right: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → sbtw c a bsbtw_cyclic_right ← SBtw.sbtw.cyclic_right: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → sbtw c a bSBtw.sbtw.cyclic_right
#align has_sbtw.sbtw.cyclic_right SBtw.sbtw.cyclic_right: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → sbtw c a bSBtw.sbtw.cyclic_right

/-- The order of the `↔` has been chosen so that `rw sbtw_cyclic` cycles to the right while
`rw ←sbtw_cyclic` cycles to the left (thus following the prepended arrow). -/
theorem sbtw_cyclic: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c ↔ sbtw c a bsbtw_cyclic {a: αa b: αb c: αc : α: Type ?u.1331α} : sbtw: {α : Type ?u.1343} → [self : SBtw α] → α → α → α → Propsbtw a: αa b: αb c: αc ↔ sbtw: {α : Type ?u.1356} → [self : SBtw α] → α → α → α → Propsbtw c: αc a: αa b: αb :=
⟨sbtw_cyclic_right: ∀ {α : Type ?u.1371} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → sbtw c a bsbtw_cyclic_right, sbtw_cyclic_left: ∀ {α : Type ?u.1392} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → sbtw b c asbtw_cyclic_left⟩
#align sbtw_cyclic sbtw_cyclic: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c ↔ sbtw c a bsbtw_cyclic

-- TODO: `alias` creates a def instead of a lemma.
-- alias btw_trans_left        ← has_btw.btw.trans_left
theorem SBtw.sbtw.trans_left: ∀ {a b c d : α}, sbtw a b c → sbtw b d c → sbtw a d cSBtw.sbtw.trans_left {a: αa b: αb c: αc d: αd : α: Type ?u.1410α} (h: sbtw a b ch : sbtw: {α : Type ?u.1424} → [self : SBtw α] → α → α → α → Propsbtw a: αa b: αb c: αc) : sbtw: {α : Type ?u.1447} → [self : SBtw α] → α → α → α → Propsbtw b: αb d: αd c: αc → sbtw: {α : Type ?u.1458} → [self : SBtw α] → α → α → α → Propsbtw a: αa d: αd c: αc :=
sbtw_trans_left: ∀ {α : Type ?u.1480} [self : CircularPreorder α] {a b c d : α}, sbtw a b c → sbtw b d c → sbtw a d csbtw_trans_left h: sbtw a b ch
#align has_sbtw.sbtw.trans_left SBtw.sbtw.trans_left: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c d : α}, sbtw a b c → sbtw b d c → sbtw a d cSBtw.sbtw.trans_left

theorem sbtw_trans_right: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c d : α}, sbtw a b c → sbtw a c d → sbtw a b dsbtw_trans_right {a: αa b: αb c: αc d: αd : α: Type ?u.1512α} (hbc: sbtw a b chbc : sbtw: {α : Type ?u.1526} → [self : SBtw α] → α → α → α → Propsbtw a: αa b: αb c: αc) (hcd: sbtw a c dhcd : sbtw: {α : Type ?u.1548} → [self : SBtw α] → α → α → α → Propsbtw a: αa c: αc d: αd) : sbtw: {α : Type ?u.1560} → [self : SBtw α] → α → α → α → Propsbtw a: αa b: αb d: αd :=
(hbc: sbtw a b chbc.cyclic_left: ∀ {α : Type ?u.1583} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → sbtw b c acyclic_left.trans_left: ∀ {α : Type ?u.1598} [inst : CircularPreorder α] {a b c d : α}, sbtw a b c → sbtw b d c → sbtw a d ctrans_left hcd: sbtw a c dhcd.cyclic_left: ∀ {α : Type ?u.1613} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → sbtw b c acyclic_left).cyclic_right: ∀ {α : Type ?u.1625} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → sbtw c a bcyclic_right
#align sbtw_trans_right sbtw_trans_right: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c d : α}, sbtw a b c → sbtw a c d → sbtw a b dsbtw_trans_right

alias sbtw_trans_right: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c d : α}, sbtw a b c → sbtw a c d → sbtw a b dsbtw_trans_right ← SBtw.sbtw.trans_right: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c d : α}, sbtw a b c → sbtw a c d → sbtw a b dSBtw.sbtw.trans_right
#align has_sbtw.sbtw.trans_right SBtw.sbtw.trans_right: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c d : α}, sbtw a b c → sbtw a c d → sbtw a b dSBtw.sbtw.trans_right

theorem sbtw_asymm: ∀ {a b c : α}, sbtw a b c → ¬sbtw c b asbtw_asymm {a: αa b: αb c: αc : α: Type ?u.1646α} (h: sbtw a b ch : sbtw: {α : Type ?u.1658} → [self : SBtw α] → α → α → α → Propsbtw a: αa b: αb c: αc) : ¬sbtw: {α : Type ?u.1680} → [self : SBtw α] → α → α → α → Propsbtw c: αc b: αb a: αa :=
h: sbtw a b ch.btw: ∀ {α : Type ?u.1692} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → btw a b cbtw.not_sbtw: ∀ {α : Type ?u.1707} [inst : CircularPreorder α] {a b c : α}, btw a b c → ¬sbtw c b anot_sbtw
#align sbtw_asymm sbtw_asymm: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → ¬sbtw c b asbtw_asymm

alias sbtw_asymm: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → ¬sbtw c b asbtw_asymm ← SBtw.sbtw.not_sbtw: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → ¬sbtw c b aSBtw.sbtw.not_sbtw
#align has_sbtw.sbtw.not_sbtw SBtw.sbtw.not_sbtw: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → ¬sbtw c b aSBtw.sbtw.not_sbtw

theorem sbtw_irrefl_left_right: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b : α}, ¬sbtw a b asbtw_irrefl_left_right {a: αa b: αb : α: Type ?u.1734α} : ¬sbtw: {α : Type ?u.1744} → [self : SBtw α] → α → α → α → Propsbtw a: αa b: αb a: αa := fun h: ?m.1763h => h: ?m.1763h.not_btw: ∀ {α : Type ?u.1765} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → ¬btw c b anot_btw h: ?m.1763h.btw: ∀ {α : Type ?u.1787} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → btw a b cbtw
#align sbtw_irrefl_left_right sbtw_irrefl_left_right: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b : α}, ¬sbtw a b asbtw_irrefl_left_right

theorem sbtw_irrefl_left: ∀ {a b : α}, ¬sbtw a a bsbtw_irrefl_left {a: αa b: αb : α: Type ?u.1806α} : ¬sbtw: {α : Type ?u.1816} → [self : SBtw α] → α → α → α → Propsbtw a: αa a: αa b: αb := fun h: ?m.1835h => sbtw_irrefl_left_right: ∀ {α : Type ?u.1837} [inst : CircularPreorder α] {a b : α}, ¬sbtw a b asbtw_irrefl_left_right h: ?m.1835h.cyclic_left: ∀ {α : Type ?u.1845} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → sbtw b c acyclic_left
#align sbtw_irrefl_left sbtw_irrefl_left: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b : α}, ¬sbtw a a bsbtw_irrefl_left

theorem sbtw_irrefl_right: ∀ {a b : α}, ¬sbtw a b bsbtw_irrefl_right {a: αa b: αb : α: Type ?u.1878α} : ¬sbtw: {α : Type ?u.1888} → [self : SBtw α] → α → α → α → Propsbtw a: αa b: αb b: αb := fun h: ?m.1907h => sbtw_irrefl_left_right: ∀ {α : Type ?u.1909} [inst : CircularPreorder α] {a b : α}, ¬sbtw a b asbtw_irrefl_left_right h: ?m.1907h.cyclic_right: ∀ {α : Type ?u.1917} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → sbtw c a bcyclic_right
#align sbtw_irrefl_right sbtw_irrefl_right: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b : α}, ¬sbtw a b bsbtw_irrefl_right

theorem sbtw_irrefl: ∀ (a : α), ¬sbtw a a asbtw_irrefl (a: αa : α: Type ?u.1950α) : ¬sbtw: {α : Type ?u.1958} → [self : SBtw α] → α → α → α → Propsbtw a: αa a: αa a: αa :=
sbtw_irrefl_left_right: ∀ {α : Type ?u.1974} [inst : CircularPreorder α] {a b : α}, ¬sbtw a b asbtw_irrefl_left_right
#align sbtw_irrefl sbtw_irrefl: ∀ {α : Type u_1} [inst : CircularPreorder α] (a : α), ¬sbtw a a asbtw_irrefl

end CircularPreorder

/-! ### Circular partial orders -/

section CircularPartialOrder

variable {α: Type ?u.2003α : Type _: Type (?u.2003+1)Type _} [CircularPartialOrder: Type ?u.2000 → Type ?u.2000CircularPartialOrder α: Type ?u.2003α]

-- TODO: `alias` creates a def instead of a lemma.
-- alias btw_antisymm        ← has_btw.btw.antisymm
theorem Btw.btw.antisymm: ∀ {a b c : α}, btw a b c → btw c b a → a = b ∨ b = c ∨ c = aBtw.btw.antisymm {a: αa b: αb c: αc : α: Type ?u.2003α} (h: btw a b ch : btw: {α : Type ?u.2015} → [self : Btw α] → α → α → α → Propbtw a: αa b: αb c: αc) : btw: {α : Type ?u.2048} → [self : Btw α] → α → α → α → Propbtw c: αc b: αb a: αa → a: αa = b: αb ∨ b: αb = c: αc ∨ c: αc = a: αa :=
btw_antisymm: ∀ {α : Type ?u.2075} [self : CircularPartialOrder α] {a b c : α}, btw a b c → btw c b a → a = b ∨ b = c ∨ c = abtw_antisymm h: btw a b ch
#align has_btw.btw.antisymm Btw.btw.antisymm: ∀ {α : Type u_1} [inst : CircularPartialOrder α] {a b c : α}, btw a b c → btw c b a → a = b ∨ b = c ∨ c = aBtw.btw.antisymm

end CircularPartialOrder

/-! ### Circular orders -/

section CircularOrder

variable {α: Type ?u.2184α : Type _: Type (?u.2452+1)Type _} [CircularOrder: Type ?u.2650 → Type ?u.2650CircularOrder α: Type ?u.2379α]

theorem btw_refl_left_right: ∀ (a b : α), btw a b abtw_refl_left_right (a: αa b: αb : α: Type ?u.2113α) : btw: {α : Type ?u.2123} → [self : Btw α] → α → α → α → Propbtw a: αa b: αb a: αa :=
(or_self_iff: ∀ (p : Prop), p ∨ p ↔ por_self_iff _: Prop_).1: ∀ {a b : Prop}, (a ↔ b) → a → b1 (btw_total: ∀ {α : Type ?u.2171} [self : CircularOrder α] (a b c : α), btw a b c ∨ btw c b abtw_total a: αa b: αb a: αa)
#align btw_refl_left_right btw_refl_left_right: ∀ {α : Type u_1} [inst : CircularOrder α] (a b : α), btw a b abtw_refl_left_right

theorem btw_rfl_left_right: ∀ {a b : α}, btw a b abtw_rfl_left_right {a: αa b: αb : α: Type ?u.2184α} : btw: {α : Type ?u.2194} → [self : Btw α] → α → α → α → Propbtw a: αa b: αb a: αa :=
btw_refl_left_right: ∀ {α : Type ?u.2237} [inst : CircularOrder α] (a b : α), btw a b abtw_refl_left_right _: ?m.2238_ _: ?m.2238_
#align btw_rfl_left_right btw_rfl_left_right: ∀ {α : Type u_1} [inst : CircularOrder α] {a b : α}, btw a b abtw_rfl_left_right

theorem btw_refl_left: ∀ {α : Type u_1} [inst : CircularOrder α] (a b : α), btw a a bbtw_refl_left (a: αa b: αb : α: Type ?u.2257α) : btw: {α : Type ?u.2267} → [self : Btw α] → α → α → α → Propbtw a: αa a: αa b: αb :=
btw_rfl_left_right: ∀ {α : Type ?u.2310} [inst : CircularOrder α] {a b : α}, btw a b abtw_rfl_left_right.cyclic_right: ∀ {α : Type ?u.2317} [inst : CircularPreorder α] {a b c : α}, btw a b c → btw c a bcyclic_right
#align btw_refl_left btw_refl_left: ∀ {α : Type u_1} [inst : CircularOrder α] (a b : α), btw a a bbtw_refl_left

theorem btw_rfl_left: ∀ {a b : α}, btw a a bbtw_rfl_left {a: αa b: αb : α: Type ?u.2379α} : btw: {α : Type ?u.2389} → [self : Btw α] → α → α → α → Propbtw a: αa a: αa b: αb :=
btw_refl_left: ∀ {α : Type ?u.2432} [inst : CircularOrder α] (a b : α), btw a a bbtw_refl_left _: ?m.2433_ _: ?m.2433_
#align btw_rfl_left btw_rfl_left: ∀ {α : Type u_1} [inst : CircularOrder α] {a b : α}, btw a a bbtw_rfl_left

theorem btw_refl_right: ∀ (a b : α), btw a b bbtw_refl_right (a: αa b: αb : α: Type ?u.2452α) : btw: {α : Type ?u.2462} → [self : Btw α] → α → α → α → Propbtw a: αa b: αb b: αb :=
btw_rfl_left_right: ∀ {α : Type ?u.2505} [inst : CircularOrder α] {a b : α}, btw a b abtw_rfl_left_right.cyclic_left: ∀ {α : Type ?u.2512} [inst : CircularPreorder α] {a b c : α}, btw a b c → btw b c acyclic_left
#align btw_refl_right btw_refl_right: ∀ {α : Type u_1} [inst : CircularOrder α] (a b : α), btw a b bbtw_refl_right

theorem btw_rfl_right: ∀ {a b : α}, btw a b bbtw_rfl_right {a: αa b: αb : α: Type ?u.2574α} : btw: {α : Type ?u.2584} → [self : Btw α] → α → α → α → Propbtw a: αa b: αb b: αb :=
btw_refl_right: ∀ {α : Type ?u.2627} [inst : CircularOrder α] (a b : α), btw a b bbtw_refl_right _: ?m.2628_ _: ?m.2628_
#align btw_rfl_right btw_rfl_right: ∀ {α : Type u_1} [inst : CircularOrder α] {a b : α}, btw a b bbtw_rfl_right

theorem sbtw_iff_not_btw: ∀ {a b c : α}, sbtw a b c ↔ ¬btw c b asbtw_iff_not_btw {a: αa b: αb c: αc : α: Type ?u.2647α} : sbtw: {α : Type ?u.2659} → [self : SBtw α] → α → α → α → Propsbtw a: αa b: αb c: αc ↔ ¬btw: {α : Type ?u.2681} → [self : Btw α] → α → α → α → Propbtw c: αc b: αb a: αa := byGoals accomplished! 🐙
α: Type u_1inst✝: CircularOrder αa, b, c: αsbtw a b c ↔ ¬btw c b arw [α: Type u_1inst✝: CircularOrder αa, b, c: αsbtw a b c ↔ ¬btw c b asbtw_iff_btw_not_btw: ∀ {α : Type ?u.2702} [inst : CircularPreorder α] {a b c : α}, sbtw a b c ↔ btw a b c ∧ ¬btw c b asbtw_iff_btw_not_btwα: Type u_1inst✝: CircularOrder αa, b, c: αbtw a b c ∧ ¬btw c b a ↔ ¬btw c b a]α: Type u_1inst✝: CircularOrder αa, b, c: αbtw a b c ∧ ¬btw c b a ↔ ¬btw c b a
α: Type u_1inst✝: CircularOrder αa, b, c: αsbtw a b c ↔ ¬btw c b aexact and_iff_right_of_imp: ∀ {b a : Prop}, (b → a) → (a ∧ b ↔ b)and_iff_right_of_imp (btw_total: ∀ {α : Type ?u.2773} [self : CircularOrder α] (a b c : α), btw a b c ∨ btw c b abtw_total _: ?m.2774_ _: ?m.2774_ _: ?m.2774_).resolve_left: ∀ {a b : Prop}, a ∨ b → ¬a → bresolve_leftGoals accomplished! 🐙
#align sbtw_iff_not_btw sbtw_iff_not_btw: ∀ {α : Type u_1} [inst : CircularOrder α] {a b c : α}, sbtw a b c ↔ ¬btw c b asbtw_iff_not_btw

theorem btw_iff_not_sbtw: ∀ {a b c : α}, btw a b c ↔ ¬sbtw c b abtw_iff_not_sbtw {a: αa b: αb c: αc : α: Type ?u.2806α} : btw: {α : Type ?u.2818} → [self : Btw α] → α → α → α → Propbtw a: αa b: αb c: αc ↔ ¬sbtw: {α : Type ?u.2840} → [self : SBtw α] → α → α → α → Propsbtw c: αc b: αb a: αa :=
iff_not_comm: ∀ {a b : Prop}, (a ↔ ¬b) ↔ (b ↔ ¬a)iff_not_comm.1: ∀ {a b : Prop}, (a ↔ b) → a → b1 sbtw_iff_not_btw: ∀ {α : Type ?u.2866} [inst : CircularOrder α] {a b c : α}, sbtw a b c ↔ ¬btw c b asbtw_iff_not_btw
#align btw_iff_not_sbtw btw_iff_not_sbtw: ∀ {α : Type u_1} [inst : CircularOrder α] {a b c : α}, btw a b c ↔ ¬sbtw c b abtw_iff_not_sbtw

end CircularOrder

/-! ### Circular intervals -/

namespace Set

section CircularPreorder

variable {α: Type ?u.2894α : Type _: Type (?u.2894+1)Type _} [CircularPreorder: Type ?u.2897 → Type ?u.2897CircularPreorder α: Type ?u.2888α]

/-- Closed-closed circular interval -/
def cIcc: α → α → Set αcIcc (a: αa b: αb : α: Type ?u.2894α) : Set: Type ?u.2904 → Type ?u.2904Set α: Type ?u.2894α :=
{ x: ?m.2915x | btw: {α : Type ?u.2917} → [self : Btw α] → α → α → α → Propbtw a: αa x: ?m.2915x b: αb }
#align set.cIcc Set.cIcc: {α : Type u_1} → [inst : CircularPreorder α] → α → α → Set αSet.cIcc

/-- Open-open circular interval -/
def cIoo: α → α → Set αcIoo (a: αa b: αb : α: Type ?u.2949α) : Set: Type ?u.2959 → Type ?u.2959Set α: Type ?u.2949α :=
{ x: ?m.2970x | sbtw: {α : Type ?u.2972} → [self : SBtw α] → α → α → α → Propsbtw a: αa x: ?m.2970x b: αb }
#align set.cIoo Set.cIoo: {α : Type u_1} → [inst : CircularPreorder α] → α → α → Set αSet.cIoo

@[simp]
theorem mem_cIcc: ∀ {a b x : α}, x ∈ cIcc a b ↔ btw a x bmem_cIcc {a: αa b: αb x: αx : α: Type ?u.3004α} : x: αx ∈ cIcc: {α : Type ?u.3021} → [inst : CircularPreorder α] → α → α → Set αcIcc a: αa b: αb ↔ btw: {α : Type ?u.3043} → [self : Btw α] → α → α → α → Propbtw a: αa x: αx b: αb :=
Iff.rfl: ∀ {a : Prop}, a ↔ aIff.rfl
#align set.mem_cIcc Set.mem_cIcc: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b x : α}, x ∈ cIcc a b ↔ btw a x bSet.mem_cIcc

@[simp]
theorem mem_cIoo: ∀ {a b x : α}, x ∈ cIoo a b ↔ sbtw a x bmem_cIoo {a: αa b: αb x: αx : α: Type ?u.3096α} : x: αx ∈ cIoo: {α : Type ?u.3113} → [inst : CircularPreorder α] → α → α → Set αcIoo a: αa b: αb ↔ sbtw: {α : Type ?u.3135} → [self : SBtw α] → α → α → α → Propsbtw a: αa x: αx b: αb :=
Iff.rfl: ∀ {a : Prop}, a ↔ aIff.rfl
#align set.mem_cIoo Set.mem_cIoo: ∀ {α : Type u_1} [inst : CircularPreorder α] {a b x : α}, x ∈ cIoo a b ↔ sbtw a x bSet.mem_cIoo

end CircularPreorder

section CircularOrder

variable {α: Type ?u.3581α : Type _: Type (?u.3284+1)Type _} [CircularOrder: Type ?u.3287 → Type ?u.3287CircularOrder α: Type ?u.3188α]

theorem left_mem_cIcc: ∀ (a b : α), a ∈ cIcc a bleft_mem_cIcc (a: αa b: αb : α: Type ?u.3194α) : a: αa ∈ cIcc: {α : Type ?u.3219} → [inst : CircularPreorder α] → α → α → Set αcIcc a: αa b: αb :=
btw_rfl_left: ∀ {α : Type ?u.3264} [inst : CircularOrder α] {a b : α}, btw a a bbtw_rfl_left
#align set.left_mem_cIcc Set.left_mem_cIcc: ∀ {α : Type u_1} [inst : CircularOrder α] (a b : α), a ∈ cIcc a bSet.left_mem_cIcc

theorem right_mem_cIcc: ∀ {α : Type u_1} [inst : CircularOrder α] (a b : α), b ∈ cIcc a bright_mem_cIcc (a: αa b: αb : α: Type ?u.3284α) : b: αb ∈ cIcc: {α : Type ?u.3309} → [inst : CircularPreorder α] → α → α → Set αcIcc a: αa b: αb :=
btw_rfl_right: ∀ {α : Type ?u.3354} [inst : CircularOrder α] {a b : α}, btw a b bbtw_rfl_right
#align set.right_mem_cIcc Set.right_mem_cIcc: ∀ {α : Type u_1} [inst : CircularOrder α] (a b : α), b ∈ cIcc a bSet.right_mem_cIcc

theorem compl_cIcc: ∀ {α : Type u_1} [inst : CircularOrder α] {a b : α}, cIcc a bᶜ = cIoo b acompl_cIcc {a: αa b: αb : α: Type ?u.3374α} : cIcc: {α : Type ?u.3388} → [inst : CircularPreorder α] → α → α → Set αcIcc a: αa b: αbᶜ = cIoo: {α : Type ?u.3432} → [inst : CircularPreorder α] → α → α → Set αcIoo b: αb a: αa := byGoals accomplished! 🐙
α: Type u_1inst✝: CircularOrder αa, b: αcIcc a bᶜ = cIoo b aextα: Type u_1inst✝: CircularOrder αa, b, x✝: αhx✝ ∈ cIcc a bᶜ ↔ x✝ ∈ cIoo b a
α: Type u_1inst✝: CircularOrder αa, b: αcIcc a bᶜ = cIoo b arw [α: Type u_1inst✝: CircularOrder αa, b, x✝: αhx✝ ∈ cIcc a bᶜ ↔ x✝ ∈ cIoo b aSet.mem_cIoo: ∀ {α : Type ?u.3467} [inst : CircularPreorder α] {a b x : α}, x ∈ cIoo a b ↔ sbtw a x bSet.mem_cIoo,α: Type u_1inst✝: CircularOrder αa, b, x✝: αhx✝ ∈ cIcc a bᶜ ↔ sbtw b x✝ a α: Type u_1inst✝: CircularOrder αa, b, x✝: αhx✝ ∈ cIcc a bᶜ ↔ x✝ ∈ cIoo b asbtw_iff_not_btw: ∀ {α : Type ?u.3526} [inst : CircularOrder α] {a b c : α}, sbtw a b c ↔ ¬btw c b asbtw_iff_not_btwα: Type u_1inst✝: CircularOrder αa, b, x✝: αhx✝ ∈ cIcc a bᶜ ↔ ¬btw a x✝ b]α: Type u_1inst✝: CircularOrder αa, b, x✝: αhx✝ ∈ cIcc a bᶜ ↔ ¬btw a x✝ b
α: Type u_1inst✝: CircularOrder αa, b: αcIcc a bᶜ = cIoo b arflGoals accomplished! 🐙
#align set.compl_cIcc Set.compl_cIcc: ∀ {α : Type u_1} [inst : CircularOrder α] {a b : α}, cIcc a bᶜ = cIoo b aSet.compl_cIcc

theorem compl_cIoo: ∀ {α : Type u_1} [inst : CircularOrder α] {a b : α}, cIoo a bᶜ = cIcc b acompl_cIoo {a: αa b: αb : α: Type ?u.3581α} : cIoo: {α : Type ?u.3595} → [inst : CircularPreorder α] → α → α → Set αcIoo a: αa b: αbᶜ = cIcc: {α : Type ?u.3639} → [inst : CircularPreorder α] → α → α → Set αcIcc b: αb a: αa := byGoals accomplished! 🐙
α: Type u_1inst✝: CircularOrder αa, b: αcIoo a bᶜ = cIcc b aextα: Type u_1inst✝: CircularOrder αa, b, x✝: αhx✝ ∈ cIoo a bᶜ ↔ x✝ ∈ cIcc b a
α: Type u_1inst✝: CircularOrder αa, b: αcIoo a bᶜ = cIcc b arw [α: Type u_1inst✝: CircularOrder αa, b, x✝: αhx✝ ∈ cIoo a bᶜ ↔ x✝ ∈ cIcc b aSet.mem_cIcc: ∀ {α : Type ?u.3674} [inst : CircularPreorder α] {a b x : α}, x ∈ cIcc a b ↔ btw a x bSet.mem_cIcc,α: Type u_1inst✝: CircularOrder αa, b, x✝: αhx✝ ∈ cIoo a bᶜ ↔ btw b x✝ a α: Type u_1inst✝: CircularOrder αa, b, x✝: αhx✝ ∈ cIoo a bᶜ ↔ x✝ ∈ cIcc b abtw_iff_not_sbtw: ∀ {α : Type ?u.3733} [inst : CircularOrder α] {a b c : α}, btw a b c ↔ ¬sbtw c b abtw_iff_not_sbtwα: Type u_1inst✝: CircularOrder αa, b, x✝: αhx✝ ∈ cIoo a bᶜ ↔ ¬sbtw a x✝ b]α: Type u_1inst✝: CircularOrder αa, b, x✝: αhx✝ ∈ cIoo a bᶜ ↔ ¬sbtw a x✝ b
α: Type u_1inst✝: CircularOrder αa, b: αcIoo a bᶜ = cIcc b arflGoals accomplished! 🐙
#align set.compl_cIoo Set.compl_cIoo: ∀ {α : Type u_1} [inst : CircularOrder α] {a b : α}, cIoo a bᶜ = cIcc b aSet.compl_cIoo

end CircularOrder

end Set

/-! ### Circularizing instances -/

/-- The betweenness relation obtained from "looping around" `≤`.
See note [reducible non-instances]. -/
@[reducible]
def LE.toBtw: (α : Type u_1) → [inst : LE α] → Btw αLE.toBtw (α: Type ?u.3788α : Type _: Type (?u.3788+1)Type _) [LE: Type ?u.3791 → Type ?u.3791LE α: Type ?u.3788α] : Btw: Type ?u.3794 → Type ?u.3794Btw α: Type ?u.3788α where
btw a: ?m.3802a b: ?m.3805b c: ?m.3808c := a: ?m.3802a ≤ b: ?m.3805b ∧ b: ?m.3805b ≤ c: ?m.3808c ∨ b: ?m.3805b ≤ c: ?m.3808c ∧ c: ?m.3808c ≤ a: ?m.3802a ∨ c: ?m.3808c ≤ a: ?m.3802a ∧ a: ?m.3802a ≤ b: ?m.3805b
#align has_le.to_has_btw LE.toBtw: (α : Type u_1) → [inst : LE α] → Btw αLE.toBtw

/-- The strict betweenness relation obtained from "looping around" `<`.
See note [reducible non-instances]. -/
@[reducible]
def LT.toSBtw: (α : Type ?u.3876) → [inst : LT α] → SBtw αLT.toSBtw (α: Type ?u.3876α : Type _: Type (?u.3876+1)Type _) [LT: Type ?u.3879 → Type ?u.3879LT α: Type ?u.3876α] : SBtw: Type ?u.3882 → Type ?u.3882SBtw α: Type ?u.3876α where
sbtw a: ?m.3890a b: ?m.3893b c: ?m.3896c := a: ?m.3890a < b: ?m.3893b ∧ b: ?m.3893b < c: ?m.3896c ∨ b: ?m.3893b < c: ?m.3896c ∧ c: ?m.3896c < a: ?m.3890a ∨ c: ?m.3896c < a: ?m.3890a ∧ a: ?m.3890a < b: ?m.3893b
#align has_lt.to_has_sbtw LT.toSBtw: (α : Type u_1) → [inst : LT α] → SBtw αLT.toSBtw

/-- The circular preorder obtained from "looping around" a preorder.
See note [reducible non-instances]. -/
@[reducible]
def Preorder.toCircularPreorder: (α : Type u_1) → [inst : Preorder α] → CircularPreorder αPreorder.toCircularPreorder (α: Type ?u.3964α : Type _: Type (?u.3964+1)Type _) [Preorder: Type ?u.3967 → Type ?u.3967Preorder α: Type ?u.3964α] : CircularPreorder: Type ?u.3970 → Type ?u.3970CircularPreorder α: Type ?u.3964α where
btw a: ?m.3981a b: ?m.3984b c: ?m.3987c := a: ?m.3981a ≤ b: ?m.3984b ∧ b: ?m.3984b ≤ c: ?m.3987c ∨ b: ?m.3984b ≤ c: ?m.3987c ∧ c: ?m.3987c ≤ a: ?m.3981a ∨ c: ?m.3987c ≤ a: ?m.3981a ∧ a: ?m.3981a ≤ b: ?m.3984b
sbtw a: ?m.4026a b: ?m.4029b c: ?m.4032c := a: ?m.4026a < b: ?m.4029b ∧ b: ?m.4029b < c: ?m.4032c ∨ b: ?m.4029b < c: ?m.4032c ∧ c: ?m.4032c < a: ?m.4026a ∨ c: ?m.4032c < a: ?m.4026a ∧ a: ?m.4026a < b: ?m.4029b
btw_refl a: ?m.4066a := Or.inl: ∀ {a b : Prop}, a → a ∨ bOr.inl ⟨le_rfl: ∀ {α : Type ?u.4080} [inst : Preorder α] {a : α}, a ≤ ale_rfl, le_rfl: ∀ {α : Type ?u.4101} [inst : Preorder α] {a : α}, a ≤ ale_rfl⟩
btw_cyclic_left {a: ?m.4119a b: ?m.4122b c: ?m.4125c} h: ?m.4128h := byGoals accomplished! 🐙
α: Type ?u.3964inst✝: Preorder αa, b, c: αh: btw a b cbtw b c adsimpα: Type ?u.3964inst✝: Preorder αa, b, c: αh: btw a b cb ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b ∨ a ≤ b ∧ b ≤ c
α: Type ?u.3964inst✝: Preorder αa, b, c: αh: btw a b cbtw b c arwa [α: Type ?u.3964inst✝: Preorder αa, b, c: αh: btw a b cb ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b ∨ a ≤ b ∧ b ≤ c← or_assoc: ∀ {a b c : Prop}, (a ∨ b) ∨ c ↔ a ∨ b ∨ cor_assoc,α: Type ?u.3964inst✝: Preorder αa, b, c: αh: btw a b c(b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b) ∨ a ≤ b ∧ b ≤ c α: Type ?u.3964inst✝: Preorder αa, b, c: αh: btw a b cb ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b ∨ a ≤ b ∧ b ≤ cor_comm: ∀ {a b : Prop}, a ∨ b ↔ b ∨ aor_commα: Type ?u.3964inst✝: Preorder αa, b, c: αh: btw a b ca ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b]α: Type ?u.3964inst✝: Preorder αa, b, c: αh: btw a b ca ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b
sbtw_trans_left {a: ?m.4160a b: ?m.4163b c: ?m.4166c d: ?m.4169d} := byGoals accomplished! 🐙
α: Type ?u.3964inst✝: Preorder αa, b, c, d: αsbtw a b c → sbtw b d c → sbtw a d crintro (⟨hab, hbc⟩ | ⟨hbc, hca⟩ | ⟨hca, hab⟩): sbtw a b c(⟨hab, hbc⟩: a < b ∧ b < c⟨hab: a < bhab⟨hab, hbc⟩: a < b ∧ b < c, hbc: b < chbc⟨hab, hbc⟩: a < b ∧ b < c⟩⟨hab, hbc⟩ | ⟨hbc, hca⟩ | ⟨hca, hab⟩: sbtw a b c | ⟨hbc, hca⟩: b < c ∧ c < a⟨hbc: b < chbc⟨hbc, hca⟩: b < c ∧ c < a, hca: c < ahca⟨hbc, hca⟩: b < c ∧ c < a⟩⟨hab, hbc⟩ | ⟨hbc, hca⟩ | ⟨hca, hab⟩: sbtw a b c | ⟨hca, hab⟩: c < a ∧ a < b⟨hca: c < ahca⟨hca, hab⟩: c < a ∧ a < b, hab: a < bhab⟨hca, hab⟩: c < a ∧ a < b⟩(⟨hab, hbc⟩ | ⟨hbc, hca⟩ | ⟨hca, hab⟩): sbtw a b c) (⟨hbd, hdc⟩ | ⟨hdc, hcb⟩ | ⟨hcb, hbd⟩): sbtw b d c(⟨hbd, hdc⟩: b < d ∧ d < c⟨hbd: b < dhbd⟨hbd, hdc⟩: b < d ∧ d < c, hdc: d < chdc⟨hbd, hdc⟩: b < d ∧ d < c⟩⟨hbd, hdc⟩ | ⟨hdc, hcb⟩ | ⟨hcb, hbd⟩: d < c ∧ c < b ∨ c < b ∧ b < d | ⟨hdc, hcb⟩: d < c ∧ c < b⟨hdc: d < chdc⟨hdc, hcb⟩: d < c ∧ c < b, hcb: c < bhcb⟨hdc, hcb⟩: d < c ∧ c < b⟩⟨hbd, hdc⟩ | ⟨hdc, hcb⟩ | ⟨hcb, hbd⟩: d < c ∧ c < b ∨ c < b ∧ b < d | ⟨hcb, hbd⟩: c < b ∧ b < d⟨hcb: c < bhcb⟨hcb, hbd⟩: c < b ∧ b < d, hbd: b < dhbd⟨hcb, hbd⟩: c < b ∧ b < d⟩(⟨hbd, hdc⟩ | ⟨hdc, hcb⟩ | ⟨hcb, hbd⟩): sbtw b d c)α: Type ?u.3964inst✝: Preorder αa, b, c, d: αhab: a < bhbc: b < chbd: b < dhdc: d < cinl.intro.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhab: a < bhbc: b < chdc: d < chcb: c < binl.intro.inr.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhab: a < bhbc: b < chcb: c < bhbd: b < dinl.intro.inr.inr.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhbc: b < chca: c < ahbd: b < dhdc: d < cinr.inl.intro.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhbc: b < chca: c < ahdc: d < chcb: c < binr.inl.intro.inr.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhbc: b < chca: c < ahcb: c < bhbd: b < dinr.inl.intro.inr.inr.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhca: c < ahab: a < bhbd: b < dhdc: d < cinr.inr.intro.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhca: c < ahab: a < bhdc: d < chcb: c < binr.inr.intro.inr.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhca: c < ahab: a < bhcb: c < bhbd: b < dinr.inr.intro.inr.inr.introsbtw a d c
α: Type ?u.3964inst✝: Preorder αa, b, c, d: αsbtw a b c → sbtw b d c → sbtw a d c·α: Type ?u.3964inst✝: Preorder αa, b, c, d: αhab: a < bhbc: b < chbd: b < dhdc: d < cinl.intro.inl.introsbtw a d c α: Type ?u.3964inst✝: Preorder αa, b, c, d: αhab: a < bhbc: b < chbd: b < dhdc: d < cinl.intro.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhab: a < bhbc: b < chdc: d < chcb: c < binl.intro.inr.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhab: a < bhbc: b < chcb: c < bhbd: b < dinl.intro.inr.inr.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhbc: b < chca: c < ahbd: b < dhdc: d < cinr.inl.intro.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhbc: b < chca: c < ahdc: d < chcb: c < binr.inl.intro.inr.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhbc: b < chca: c < ahcb: c < bhbd: b < dinr.inl.intro.inr.inr.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhca: c < ahab: a < bhbd: b < dhdc: d < cinr.inr.intro.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhca: c < ahab: a < bhdc: d < chcb: c < binr.inr.intro.inr.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhca: c < ahab: a < bhcb: c < bhbd: b < dinr.inr.intro.inr.inr.introsbtw a d cexact Or.inl: ∀ {a b : Prop}, a → a ∨ bOr.inl ⟨hab: a < bhab.trans: ∀ {α : Type ?u.239719} [inst : Preorder α] {a b c : α}, a < b → b < c → a < ctrans hbd: b < dhbd, hdc: d < chdc⟩Goals accomplished! 🐙
α: Type ?u.3964inst✝: Preorder αa, b, c, d: αsbtw a b c → sbtw b d c → sbtw a d c·α: Type ?u.3964inst✝: Preorder αa, b, c, d: αhab: a < bhbc: b < chdc: d < chcb: c < binl.intro.inr.inl.introsbtw a d c α: Type ?u.3964inst✝: Preorder αa, b, c, d: αhab: a < bhbc: b < chdc: d < chcb: c < binl.intro.inr.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhab: a < bhbc: b < chcb: c < bhbd: b < dinl.intro.inr.inr.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhbc: b < chca: c < ahbd: b < dhdc: d < cinr.inl.intro.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhbc: b < chca: c < ahdc: d < chcb: c < binr.inl.intro.inr.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhbc: b < chca: c < ahcb: c < bhbd: b < dinr.inl.intro.inr.inr.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhca: c < ahab: a < bhbd: b < dhdc: d < cinr.inr.intro.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhca: c < ahab: a < bhdc: d < chcb: c < binr.inr.intro.inr.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhca: c < ahab: a < bhcb: c < bhbd: b < dinr.inr.intro.inr.inr.introsbtw a d cexact (hbc: b < chbc.not_lt: ∀ {α : Type ?u.239736} [inst : Preorder α] {a b : α}, a < b → ¬b < anot_lt hcb: c < bhcb).elim: ∀ {C : Sort ?u.239747}, False → CelimGoals accomplished! 🐙
α: Type ?u.3964inst✝: Preorder αa, b, c, d: αsbtw a b c → sbtw b d c → sbtw a d c·α: Type ?u.3964inst✝: Preorder αa, b, c, d: αhab: a < bhbc: b < chcb: c < bhbd: b < dinl.intro.inr.inr.introsbtw a d c α: Type ?u.3964inst✝: Preorder αa, b, c, d: αhab: a < bhbc: b < chcb: c < bhbd: b < dinl.intro.inr.inr.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhbc: b < chca: c < ahbd: b < dhdc: d < cinr.inl.intro.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhbc: b < chca: c < ahdc: d < chcb: c < binr.inl.intro.inr.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhbc: b < chca: c < ahcb: c < bhbd: b < dinr.inl.intro.inr.inr.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhca: c < ahab: a < bhbd: b < dhdc: d < cinr.inr.intro.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhca: c < ahab: a < bhdc: d < chcb: c < binr.inr.intro.inr.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhca: c < ahab: a < bhcb: c < bhbd: b < dinr.inr.intro.inr.inr.introsbtw a d cexact (hbc: b < chbc.not_lt: ∀ {α : Type ?u.239751} [inst : Preorder α] {a b : α}, a < b → ¬b < anot_lt hcb: c < bhcb).elim: ∀ {C : Sort ?u.239762}, False → CelimGoals accomplished! 🐙
α: Type ?u.3964inst✝: Preorder αa, b, c, d: αsbtw a b c → sbtw b d c → sbtw a d c·α: Type ?u.3964inst✝: Preorder αa, b, c, d: αhbc: b < chca: c < ahbd: b < dhdc: d < cinr.inl.intro.inl.introsbtw a d c α: Type ?u.3964inst✝: Preorder αa, b, c, d: αhbc: b < chca: c < ahbd: b < dhdc: d < cinr.inl.intro.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhbc: b < chca: c < ahdc: d < chcb: c < binr.inl.intro.inr.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhbc: b < chca: c < ahcb: c < bhbd: b < dinr.inl.intro.inr.inr.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhca: c < ahab: a < bhbd: b < dhdc: d < cinr.inr.intro.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhca: c < ahab: a < bhdc: d < chcb: c < binr.inr.intro.inr.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhca: c < ahab: a < bhcb: c < bhbd: b < dinr.inr.intro.inr.inr.introsbtw a d cexact Or.inr: ∀ {a b : Prop}, b → a ∨ bOr.inr (Or.inl: ∀ {a b : Prop}, a → a ∨ bOr.inl ⟨hdc: d < chdc, hca: c < ahca⟩)Goals accomplished! 🐙
α: Type ?u.3964inst✝: Preorder αa, b, c, d: αsbtw a b c → sbtw b d c → sbtw a d c·α: Type ?u.3964inst✝: Preorder αa, b, c, d: αhbc: b < chca: c < ahdc: d < chcb: c < binr.inl.intro.inr.inl.introsbtw a d c α: Type ?u.3964inst✝: Preorder αa, b, c, d: αhbc: b < chca: c < ahdc: d < chcb: c < binr.inl.intro.inr.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhbc: b < chca: c < ahcb: c < bhbd: b < dinr.inl.intro.inr.inr.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhca: c < ahab: a < bhbd: b < dhdc: d < cinr.inr.intro.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhca: c < ahab: a < bhdc: d < chcb: c < binr.inr.intro.inr.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhca: c < ahab: a < bhcb: c < bhbd: b < dinr.inr.intro.inr.inr.introsbtw a d cexact Or.inr: ∀ {a b : Prop}, b → a ∨ bOr.inr (Or.inl: ∀ {a b : Prop}, a → a ∨ bOr.inl ⟨hdc: d < chdc, hca: c < ahca⟩)Goals accomplished! 🐙
α: Type ?u.3964inst✝: Preorder αa, b, c, d: αsbtw a b c → sbtw b d c → sbtw a d c·α: Type ?u.3964inst✝: Preorder αa, b, c, d: αhbc: b < chca: c < ahcb: c < bhbd: b < dinr.inl.intro.inr.inr.introsbtw a d c α: Type ?u.3964inst✝: Preorder αa, b, c, d: αhbc: b < chca: c < ahcb: c < bhbd: b < dinr.inl.intro.inr.inr.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhca: c < ahab: a < bhbd: b < dhdc: d < cinr.inr.intro.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhca: c < ahab: a < bhdc: d < chcb: c < binr.inr.intro.inr.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhca: c < ahab: a < bhcb: c < bhbd: b < dinr.inr.intro.inr.inr.introsbtw a d cexact (hbc: b < chbc.not_lt: ∀ {α : Type ?u.239786} [inst : Preorder α] {a b : α}, a < b → ¬b < anot_lt hcb: c < bhcb).elim: ∀ {C : Sort ?u.239797}, False → CelimGoals accomplished! 🐙
α: Type ?u.3964inst✝: Preorder αa, b, c, d: αsbtw a b c → sbtw b d c → sbtw a d c·α: Type ?u.3964inst✝: Preorder αa, b, c, d: αhca: c < ahab: a < bhbd: b < dhdc: d < cinr.inr.intro.inl.introsbtw a d c α: Type ?u.3964inst✝: Preorder αa, b, c, d: αhca: c < ahab: a < bhbd: b < dhdc: d < cinr.inr.intro.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhca: c < ahab: a < bhdc: d < chcb: c < binr.inr.intro.inr.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhca: c < ahab: a < bhcb: c < bhbd: b < dinr.inr.intro.inr.inr.introsbtw a d cexact Or.inr: ∀ {a b : Prop}, b → a ∨ bOr.inr (Or.inl: ∀ {a b : Prop}, a → a ∨ bOr.inl ⟨hdc: d < chdc, hca: c < ahca⟩)Goals accomplished! 🐙
α: Type ?u.3964inst✝: Preorder αa, b, c, d: αsbtw a b c → sbtw b d c → sbtw a d c·α: Type ?u.3964inst✝: Preorder αa, b, c, d: αhca: c < ahab: a < bhdc: d < chcb: c < binr.inr.intro.inr.inl.introsbtw a d c α: Type ?u.3964inst✝: Preorder αa, b, c, d: αhca: c < ahab: a < bhdc: d < chcb: c < binr.inr.intro.inr.inl.introsbtw a d cα: Type ?u.3964inst✝: Preorder αa, b, c, d: αhca: c < ahab: a < bhcb: c < bhbd: b < dinr.inr.intro.inr.inr.introsbtw a d cexact Or.inr: ∀ {a b : Prop}, b → a ∨ bOr.inr (Or.inl: ∀ {a b : Prop}, a → a ∨ bOr.inl ⟨hdc: d < chdc, hca: c < ahca⟩)Goals accomplished! 🐙
α: Type ?u.3964inst✝: Preorder αa, b, c, d: αsbtw a b c → sbtw b d c → sbtw a d c·α: Type ?u.3964inst✝: Preorder αa, b, c, d: αhca: c < ahab: a < bhcb: c < bhbd: b < dinr.inr.intro.inr.inr.introsbtw a d c α: Type ?u.3964inst✝: Preorder αa, b, c, d: αhca: c < ahab: a < bhcb: c < bhbd: b < dinr.inr.intro.inr.inr.introsbtw a d cexact Or.inr: ∀ {a b : Prop}, b → a ∨ bOr.inr (Or.inr: ∀ {a b : Prop}, b → a ∨ bOr.inr ⟨hca: c < ahca, hab: a < bhab.trans: ∀ {α : Type ?u.239831} [inst : Preorder α] {a b c : α}, a < b → b < c → a < ctrans hbd: b < dhbd⟩)Goals accomplished! 🐙
sbtw_iff_btw_not_btw {a: ?m.4141a b: ?m.4144b c: ?m.4147c} := byGoals accomplished! 🐙
α: Type ?u.3964inst✝: Preorder αa, b, c: αsbtw a b c ↔ btw a b c ∧ ¬btw c b asimp_rw [α: Type ?u.3964inst✝: Preorder αa, b, c: αa < b ∧ b < c ∨ b < c ∧ c < a ∨ c < a ∧ a < b ↔   (a ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b) ∧ ¬(c ≤ b ∧ b ≤ a ∨ b ≤ a ∧ a ≤ c ∨ a ≤ c ∧ c ≤ b)lt_iff_le_not_leα: Type ?u.3964inst✝: Preorder αa, b, c: α(a ≤ b ∧ ¬b ≤ a) ∧ b ≤ c ∧ ¬c ≤ b ∨ (b ≤ c ∧ ¬c ≤ b) ∧ c ≤ a ∧ ¬a ≤ c ∨ (c ≤ a ∧ ¬a ≤ c) ∧ a ≤ b ∧ ¬b ≤ a ↔   (a ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b) ∧ ¬(c ≤ b ∧ b ≤ a ∨ b ≤ a ∧ a ≤ c ∨ a ≤ c ∧ c ≤ b)]α: Type ?u.3964inst✝: Preorder αa, b, c: α(a ≤ b ∧ ¬b ≤ a) ∧ b ≤ c ∧ ¬c ≤ b ∨ (b ≤ c ∧ ¬c ≤ b) ∧ c ≤ a ∧ ¬a ≤ c ∨ (c ≤ a ∧ ¬a ≤ c) ∧ a ≤ b ∧ ¬b ≤ a ↔   (a ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b) ∧ ¬(c ≤ b ∧ b ≤ a ∨ b ≤ a ∧ a ≤ c ∨ a ≤ c ∧ c ≤ b)
α: Type ?u.3964inst✝: Preorder αa, b, c: αsbtw a b c ↔ btw a b c ∧ ¬btw c b ahave := le_trans: ∀ {α : Type ?u.4361} [self : Preorder α] (a b c : α), a ≤ b → b ≤ c → a ≤ cle_trans a: αa b: αb c: αcα: Type ?u.3964inst✝: Preorder αa, b, c: αthis: a ≤ b → b ≤ c → a ≤ c(a ≤ b ∧ ¬b ≤ a) ∧ b ≤ c ∧ ¬c ≤ b ∨ (b ≤ c ∧ ¬c ≤ b) ∧ c ≤ a ∧ ¬a ≤ c ∨ (c ≤ a ∧ ¬a ≤ c) ∧ a ≤ b ∧ ¬b ≤ a ↔   (a ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b) ∧ ¬(c ≤ b ∧ b ≤ a ∨ b ≤ a ∧ a ≤ c ∨ a ≤ c ∧ c ≤ b)
α: Type ?u.3964inst✝: Preorder αa, b, c: αsbtw a b c ↔ btw a b c ∧ ¬btw c b ahave := le_trans: ∀ {α : Type ?u.4381} [self : Preorder α] (a b c : α), a ≤ b → b ≤ c → a ≤ cle_trans b: αb c: αc a: αaα: Type ?u.3964inst✝: Preorder αa, b, c: αthis✝: a ≤ b → b ≤ c → a ≤ cthis: b ≤ c → c ≤ a → b ≤ a(a ≤ b ∧ ¬b ≤ a) ∧ b ≤ c ∧ ¬c ≤ b ∨ (b ≤ c ∧ ¬c ≤ b) ∧ c ≤ a ∧ ¬a ≤ c ∨ (c ≤ a ∧ ¬a ≤ c) ∧ a ≤ b ∧ ¬b ≤ a ↔   (a ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b) ∧ ¬(c ≤ b ∧ b ≤ a ∨ b ≤ a ∧ a ≤ c ∨ a ≤ c ∧ c ≤ b)
α: Type ?u.3964inst✝: Preorder αa, b, c: αsbtw a b c ↔ btw a b c ∧ ¬btw c b ahave := le_trans: ∀ {α : Type ?u.4400} [self : Preorder α] (a b c : α), a ≤ b → b ≤ c → a ≤ cle_trans c: αc a: αa b: αbα: Type ?u.3964inst✝: Preorder αa, b, c: αthis✝¹: a ≤ b → b ≤ c → a ≤ cthis✝: b ≤ c → c ≤ a → b ≤ athis: c ≤ a → a ≤ b → c ≤ b(a ≤ b ∧ ¬b ≤ a) ∧ b ≤ c ∧ ¬c ≤ b ∨ (b ≤ c ∧ ¬c ≤ b) ∧ c ≤ a ∧ ¬a ≤ c ∨ (c ≤ a ∧ ¬a ≤ c) ∧ a ≤ b ∧ ¬b ≤ a ↔   (a ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b) ∧ ¬(c ≤ b ∧ b ≤ a ∨ b ≤ a ∧ a ≤ c ∨ a ≤ c ∧ c ≤ b)
α: Type ?u.3964inst✝: Preorder αa, b, c: αsbtw a b c ↔ btw a b c ∧ ¬btw c b atautoGoals accomplished! 🐙
#align preorder.to_circular_preorder Preorder.toCircularPreorder: (α : Type u_1) → [inst : Preorder α] → CircularPreorder αPreorder.toCircularPreorder

/-- The circular partial order obtained from "looping around" a partial order.
See note [reducible non-instances]. -/
@[reducible]
def PartialOrder.toCircularPartialOrder: (α : Type u_1) → [inst : PartialOrder α] → CircularPartialOrder αPartialOrder.toCircularPartialOrder (α: Type ?u.241064α : Type _: Type (?u.241064+1)Type _) [PartialOrder: Type ?u.241067 → Type ?u.241067PartialOrder α: Type ?u.241064α] : CircularPartialOrder: Type ?u.241070 → Type ?u.241070CircularPartialOrder α: Type ?u.241064α :=
{ Preorder.toCircularPreorder: (α : Type ?u.241076) → [inst : Preorder α] → CircularPreorder αPreorder.toCircularPreorder α: Type ?u.241064α with
btw_antisymm := fun {a: ?m.241180a b: ?m.241183b c: ?m.241186c} => byGoals accomplished! 🐙
α: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αbtw a b c → btw c b a → a = b ∨ b = c ∨ c = arintro (⟨hab, hbc⟩ | ⟨hbc, hca⟩ | ⟨hca, hab⟩): btw a b c(⟨hab, hbc⟩: a ≤ b ∧ b ≤ c⟨hab: a ≤ bhab⟨hab, hbc⟩: a ≤ b ∧ b ≤ c, hbc: b ≤ chbc⟨hab, hbc⟩: a ≤ b ∧ b ≤ c⟩⟨hab, hbc⟩ | ⟨hbc, hca⟩ | ⟨hca, hab⟩: btw a b c | ⟨hbc, hca⟩: b ≤ c ∧ c ≤ a⟨hbc: b ≤ chbc⟨hbc, hca⟩: b ≤ c ∧ c ≤ a, hca: c ≤ ahca⟨hbc, hca⟩: b ≤ c ∧ c ≤ a⟩⟨hab, hbc⟩ | ⟨hbc, hca⟩ | ⟨hca, hab⟩: btw a b c | ⟨hca, hab⟩: c ≤ a ∧ a ≤ b⟨hca: c ≤ ahca⟨hca, hab⟩: c ≤ a ∧ a ≤ b, hab: a ≤ bhab⟨hca, hab⟩: c ≤ a ∧ a ≤ b⟩(⟨hab, hbc⟩ | ⟨hbc, hca⟩ | ⟨hca, hab⟩): btw a b c) (⟨hcb, hba⟩ | ⟨hba, hac⟩ | ⟨hac, hcb⟩): btw c b a(⟨hcb, hba⟩: c ≤ b ∧ b ≤ a⟨hcb: c ≤ bhcb⟨hcb, hba⟩: c ≤ b ∧ b ≤ a, hba: b ≤ ahba⟨hcb, hba⟩: c ≤ b ∧ b ≤ a⟩⟨hcb, hba⟩ | ⟨hba, hac⟩ | ⟨hac, hcb⟩: btw c b a | ⟨hba, hac⟩: b ≤ a ∧ a ≤ c⟨hba: b ≤ ahba⟨hba, hac⟩: b ≤ a ∧ a ≤ c, hac: a ≤ chac⟨hba, hac⟩: b ≤ a ∧ a ≤ c⟩⟨hcb, hba⟩ | ⟨hba, hac⟩ | ⟨hac, hcb⟩: btw c b a | ⟨hac, hcb⟩: a ≤ c ∧ c ≤ b⟨hac: a ≤ chac⟨hac, hcb⟩: a ≤ c ∧ c ≤ b, hcb: c ≤ bhcb⟨hac, hcb⟩: a ≤ c ∧ c ≤ b⟩(⟨hcb, hba⟩ | ⟨hba, hac⟩ | ⟨hac, hcb⟩): btw c b a)α: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhab: a ≤ bhbc: b ≤ chcb: c ≤ bhba: b ≤ ainl.intro.inl.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhab: a ≤ bhbc: b ≤ chba: b ≤ ahac: a ≤ cinl.intro.inr.inl.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhab: a ≤ bhbc: b ≤ chac: a ≤ chcb: c ≤ binl.intro.inr.inr.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhbc: b ≤ chca: c ≤ ahcb: c ≤ bhba: b ≤ ainr.inl.intro.inl.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhbc: b ≤ chca: c ≤ ahba: b ≤ ahac: a ≤ cinr.inl.intro.inr.inl.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhbc: b ≤ chca: c ≤ ahac: a ≤ chcb: c ≤ binr.inl.intro.inr.inr.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhca: c ≤ ahab: a ≤ bhcb: c ≤ bhba: b ≤ ainr.inr.intro.inl.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhca: c ≤ ahab: a ≤ bhba: b ≤ ahac: a ≤ cinr.inr.intro.inr.inl.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhca: c ≤ ahab: a ≤ bhac: a ≤ chcb: c ≤ binr.inr.intro.inr.inr.introa = b ∨ b = c ∨ c = a
α: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αbtw a b c → btw c b a → a = b ∨ b = c ∨ c = a·α: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhab: a ≤ bhbc: b ≤ chcb: c ≤ bhba: b ≤ ainl.intro.inl.introa = b ∨ b = c ∨ c = a α: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhab: a ≤ bhbc: b ≤ chcb: c ≤ bhba: b ≤ ainl.intro.inl.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhab: a ≤ bhbc: b ≤ chba: b ≤ ahac: a ≤ cinl.intro.inr.inl.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhab: a ≤ bhbc: b ≤ chac: a ≤ chcb: c ≤ binl.intro.inr.inr.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhbc: b ≤ chca: c ≤ ahcb: c ≤ bhba: b ≤ ainr.inl.intro.inl.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhbc: b ≤ chca: c ≤ ahba: b ≤ ahac: a ≤ cinr.inl.intro.inr.inl.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhbc: b ≤ chca: c ≤ ahac: a ≤ chcb: c ≤ binr.inl.intro.inr.inr.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhca: c ≤ ahab: a ≤ bhcb: c ≤ bhba: b ≤ ainr.inr.intro.inl.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhca: c ≤ ahab: a ≤ bhba: b ≤ ahac: a ≤ cinr.inr.intro.inr.inl.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhca: c ≤ ahab: a ≤ bhac: a ≤ chcb: c ≤ binr.inr.intro.inr.inr.introa = b ∨ b = c ∨ c = aexact Or.inl: ∀ {a b : Prop}, a → a ∨ bOr.inl (hab: a ≤ bhab.antisymm: ∀ {α : Type ?u.241632} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = bantisymm hba: b ≤ ahba)Goals accomplished! 🐙
α: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αbtw a b c → btw c b a → a = b ∨ b = c ∨ c = a·α: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhab: a ≤ bhbc: b ≤ chba: b ≤ ahac: a ≤ cinl.intro.inr.inl.introa = b ∨ b = c ∨ c = a α: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhab: a ≤ bhbc: b ≤ chba: b ≤ ahac: a ≤ cinl.intro.inr.inl.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhab: a ≤ bhbc: b ≤ chac: a ≤ chcb: c ≤ binl.intro.inr.inr.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhbc: b ≤ chca: c ≤ ahcb: c ≤ bhba: b ≤ ainr.inl.intro.inl.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhbc: b ≤ chca: c ≤ ahba: b ≤ ahac: a ≤ cinr.inl.intro.inr.inl.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhbc: b ≤ chca: c ≤ ahac: a ≤ chcb: c ≤ binr.inl.intro.inr.inr.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhca: c ≤ ahab: a ≤ bhcb: c ≤ bhba: b ≤ ainr.inr.intro.inl.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhca: c ≤ ahab: a ≤ bhba: b ≤ ahac: a ≤ cinr.inr.intro.inr.inl.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhca: c ≤ ahab: a ≤ bhac: a ≤ chcb: c ≤ binr.inr.intro.inr.inr.introa = b ∨ b = c ∨ c = aexact Or.inl: ∀ {a b : Prop}, a → a ∨ bOr.inl (hab: a ≤ bhab.antisymm: ∀ {α : Type ?u.241656} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = bantisymm hba: b ≤ ahba)Goals accomplished! 🐙
α: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αbtw a b c → btw c b a → a = b ∨ b = c ∨ c = a·α: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhab: a ≤ bhbc: b ≤ chac: a ≤ chcb: c ≤ binl.intro.inr.inr.introa = b ∨ b = c ∨ c = a α: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhab: a ≤ bhbc: b ≤ chac: a ≤ chcb: c ≤ binl.intro.inr.inr.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhbc: b ≤ chca: c ≤ ahcb: c ≤ bhba: b ≤ ainr.inl.intro.inl.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhbc: b ≤ chca: c ≤ ahba: b ≤ ahac: a ≤ cinr.inl.intro.inr.inl.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhbc: b ≤ chca: c ≤ ahac: a ≤ chcb: c ≤ binr.inl.intro.inr.inr.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhca: c ≤ ahab: a ≤ bhcb: c ≤ bhba: b ≤ ainr.inr.intro.inl.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhca: c ≤ ahab: a ≤ bhba: b ≤ ahac: a ≤ cinr.inr.intro.inr.inl.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhca: c ≤ ahab: a ≤ bhac: a ≤ chcb: c ≤ binr.inr.intro.inr.inr.introa = b ∨ b = c ∨ c = aexact Or.inr: ∀ {a b : Prop}, b → a ∨ bOr.inr (Or.inl: ∀ {a b : Prop}, a → a ∨ bOr.inl <| hbc: b ≤ chbc.antisymm: ∀ {α : Type ?u.241671} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = bantisymm hcb: c ≤ bhcb)Goals accomplished! 🐙
α: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αbtw a b c → btw c b a → a = b ∨ b = c ∨ c = a·α: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhbc: b ≤ chca: c ≤ ahcb: c ≤ bhba: b ≤ ainr.inl.intro.inl.introa = b ∨ b = c ∨ c = a α: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhbc: b ≤ chca: c ≤ ahcb: c ≤ bhba: b ≤ ainr.inl.intro.inl.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhbc: b ≤ chca: c ≤ ahba: b ≤ ahac: a ≤ cinr.inl.intro.inr.inl.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhbc: b ≤ chca: c ≤ ahac: a ≤ chcb: c ≤ binr.inl.intro.inr.inr.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhca: c ≤ ahab: a ≤ bhcb: c ≤ bhba: b ≤ ainr.inr.intro.inl.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhca: c ≤ ahab: a ≤ bhba: b ≤ ahac: a ≤ cinr.inr.intro.inr.inl.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhca: c ≤ ahab: a ≤ bhac: a ≤ chcb: c ≤ binr.inr.intro.inr.inr.introa = b ∨ b = c ∨ c = aexact Or.inr: ∀ {a b : Prop}, b → a ∨ bOr.inr (Or.inl: ∀ {a b : Prop}, a → a ∨ bOr.inl <| hbc: b ≤ chbc.antisymm: ∀ {α : Type ?u.241686} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = bantisymm hcb: c ≤ bhcb)Goals accomplished! 🐙
α: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αbtw a b c → btw c b a → a = b ∨ b = c ∨ c = a·α: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhbc: b ≤ chca: c ≤ ahba: b ≤ ahac: a ≤ cinr.inl.intro.inr.inl.introa = b ∨ b = c ∨ c = a α: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhbc: b ≤ chca: c ≤ ahba: b ≤ ahac: a ≤ cinr.inl.intro.inr.inl.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhbc: b ≤ chca: c ≤ ahac: a ≤ chcb: c ≤ binr.inl.intro.inr.inr.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhca: c ≤ ahab: a ≤ bhcb: c ≤ bhba: b ≤ ainr.inr.intro.inl.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhca: c ≤ ahab: a ≤ bhba: b ≤ ahac: a ≤ cinr.inr.intro.inr.inl.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhca: c ≤ ahab: a ≤ bhac: a ≤ chcb: c ≤ binr.inr.intro.inr.inr.introa = b ∨ b = c ∨ c = aexact Or.inr: ∀ {a b : Prop}, b → a ∨ bOr.inr (Or.inr: ∀ {a b : Prop}, b → a ∨ bOr.inr <| hca: c ≤ ahca.antisymm: ∀ {α : Type ?u.241701} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = bantisymm hac: a ≤ chac)Goals accomplished! 🐙
α: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αbtw a b c → btw c b a → a = b ∨ b = c ∨ c = a·α: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhbc: b ≤ chca: c ≤ ahac: a ≤ chcb: c ≤ binr.inl.intro.inr.inr.introa = b ∨ b = c ∨ c = a α: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhbc: b ≤ chca: c ≤ ahac: a ≤ chcb: c ≤ binr.inl.intro.inr.inr.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhca: c ≤ ahab: a ≤ bhcb: c ≤ bhba: b ≤ ainr.inr.intro.inl.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhca: c ≤ ahab: a ≤ bhba: b ≤ ahac: a ≤ cinr.inr.intro.inr.inl.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhca: c ≤ ahab: a ≤ bhac: a ≤ chcb: c ≤ binr.inr.intro.inr.inr.introa = b ∨ b = c ∨ c = aexact Or.inr: ∀ {a b : Prop}, b → a ∨ bOr.inr (Or.inl: ∀ {a b : Prop}, a → a ∨ bOr.inl <| hbc: b ≤ chbc.antisymm: ∀ {α : Type ?u.241716} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = bantisymm hcb: c ≤ bhcb)Goals accomplished! 🐙
α: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αbtw a b c → btw c b a → a = b ∨ b = c ∨ c = a·α: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhca: c ≤ ahab: a ≤ bhcb: c ≤ bhba: b ≤ ainr.inr.intro.inl.introa = b ∨ b = c ∨ c = a α: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhca: c ≤ ahab: a ≤ bhcb: c ≤ bhba: b ≤ ainr.inr.intro.inl.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhca: c ≤ ahab: a ≤ bhba: b ≤ ahac: a ≤ cinr.inr.intro.inr.inl.introa = b ∨ b = c ∨ c = aα: Type ?u.241064inst✝: PartialOrder αsrc✝:= Preorder.toCircularPreorder α: CircularPreorder αa, b, c: αhca: c ≤ ahab: a ≤ bhac: a ≤ chcb: c ≤ binr.inr.intro.inr.inr.introa = b ∨ b = c ∨ c = aexact Or.inl: ∀ {a b : Prop}, a → a ∨ bOr.inl (```