[GOAL]
α : Type u_1
inst✝ : CircularOrder α
a b c : α
⊢ sbtw a b c ↔ ¬btw c b a
[PROOFSTEP]
rw [sbtw_iff_btw_not_btw]
[GOAL]
α : Type u_1
inst✝ : CircularOrder α
a b c : α
⊢ btw a b c ∧ ¬btw c b a ↔ ¬btw c b a
[PROOFSTEP]
exact and_iff_right_of_imp (btw_total _ _ _).resolve_left
[GOAL]
α : Type u_1
inst✝ : CircularOrder α
a b : α
⊢ (cIcc a b)ᶜ = cIoo b a
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
inst✝ : CircularOrder α
a b x✝ : α
⊢ x✝ ∈ (cIcc a b)ᶜ ↔ x✝ ∈ cIoo b a
[PROOFSTEP]
rw [Set.mem_cIoo, sbtw_iff_not_btw, cIcc, mem_compl_iff, mem_setOf]
[GOAL]
α : Type u_1
inst✝ : CircularOrder α
a b : α
⊢ (cIoo a b)ᶜ = cIcc b a
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
inst✝ : CircularOrder α
a b x✝ : α
⊢ x✝ ∈ (cIoo a b)ᶜ ↔ x✝ ∈ cIcc b a
[PROOFSTEP]
rw [Set.mem_cIcc, btw_iff_not_sbtw, cIoo, mem_compl_iff, mem_setOf]
[GOAL]
α : Type u_1
inst✝ : Preorder α
a b c : α
h : btw a b c
⊢ btw b c a
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
inst✝ : Preorder α
a b c : α
h : btw a b c
⊢ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b ∨ a ≤ b ∧ b ≤ c
[PROOFSTEP]
rwa [← or_assoc, or_comm]
[GOAL]
α : Type u_1
inst✝ : Preorder α
a b c : α
⊢ sbtw a b c ↔ btw a b c ∧ ¬btw c b a
[PROOFSTEP]
simp_rw [lt_iff_le_not_le]
[GOAL]
α : Type u_1
inst✝ : 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)
[PROOFSTEP]
have h1 := le_trans a b c
[GOAL]
α : Type u_1
inst✝ : Preorder α
a b c : α
h1 : 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)
[PROOFSTEP]
have h2 := le_trans b c a
[GOAL]
α : Type u_1
inst✝ : Preorder α
a b c : α
h1 : a ≤ b → b ≤ c → a ≤ c
h2 : 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)
[PROOFSTEP]
have h3 := le_trans c a b
[GOAL]
α : Type u_1
inst✝ : Preorder α
a b c : α
h1 : a ≤ b → b ≤ c → a ≤ c
h2 : b ≤ c → c ≤ a → b ≤ a
h3 : 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)
[PROOFSTEP]
revert h1 h2 h3
[GOAL]
α : Type u_1
inst✝ : Preorder α
a b c : α
⊢ (a ≤ b → b ≤ c → a ≤ c) →
    (b ≤ c → c ≤ a → b ≤ a) →
      (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))
[PROOFSTEP]
generalize (a ≤ b) = p1
[GOAL]
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 : Prop
⊢ (p1 → b ≤ c → a ≤ c) →
    (b ≤ c → c ≤ a → b ≤ a) →
      (c ≤ a → p1 → c ≤ b) →
        ((p1 ∧ ¬b ≤ a) ∧ b ≤ c ∧ ¬c ≤ b ∨ (b ≤ c ∧ ¬c ≤ b) ∧ c ≤ a ∧ ¬a ≤ c ∨ (c ≤ a ∧ ¬a ≤ c) ∧ p1 ∧ ¬b ≤ a ↔
          (p1 ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ p1) ∧ ¬(c ≤ b ∧ b ≤ a ∨ b ≤ a ∧ a ≤ c ∨ a ≤ c ∧ c ≤ b))
[PROOFSTEP]
generalize (b ≤ a) = p2
[GOAL]
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 : Prop
⊢ (p1 → b ≤ c → a ≤ c) →
    (b ≤ c → c ≤ a → p2) →
      (c ≤ a → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ b ≤ c ∧ ¬c ≤ b ∨ (b ≤ c ∧ ¬c ≤ b) ∧ c ≤ a ∧ ¬a ≤ c ∨ (c ≤ a ∧ ¬a ≤ c) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ a ≤ c ∨ a ≤ c ∧ c ≤ b))
[PROOFSTEP]
generalize (a ≤ c) = p3
[GOAL]
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 : Prop
⊢ (p1 → b ≤ c → p3) →
    (b ≤ c → c ≤ a → p2) →
      (c ≤ a → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ b ≤ c ∧ ¬c ≤ b ∨ (b ≤ c ∧ ¬c ≤ b) ∧ c ≤ a ∧ ¬p3 ∨ (c ≤ a ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
generalize (c ≤ a) = p4
[GOAL]
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 : Prop
⊢ (p1 → b ≤ c → p3) →
    (b ≤ c → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ b ≤ c ∧ ¬c ≤ b ∨ (b ≤ c ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ b ≤ c ∨ b ≤ c ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
generalize (b ≤ c) = p5
[GOAL]
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p1
[GOAL]
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p1
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h : p1
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p2
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h : p1
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p2
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h : ¬p1
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p2
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h : ¬p1
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p2
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝ : p1
h : p2
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p3
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝ : p1
h : p2
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p3
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝ : p1
h : ¬p2
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p3
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝ : p1
h : ¬p2
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p3
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝ : ¬p1
h : p2
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p3
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝ : ¬p1
h : p2
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p3
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝ : ¬p1
h : ¬p2
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p3
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝ : ¬p1
h : ¬p2
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p3
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝¹ : p1
h✝ : p2
h : p3
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p4
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝¹ : p1
h✝ : p2
h : p3
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p4
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝¹ : p1
h✝ : p2
h : ¬p3
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p4
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝¹ : p1
h✝ : p2
h : ¬p3
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p4
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝¹ : p1
h✝ : ¬p2
h : p3
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p4
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝¹ : p1
h✝ : ¬p2
h : p3
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p4
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝¹ : p1
h✝ : ¬p2
h : ¬p3
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p4
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝¹ : p1
h✝ : ¬p2
h : ¬p3
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p4
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝¹ : ¬p1
h✝ : p2
h : p3
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p4
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝¹ : ¬p1
h✝ : p2
h : p3
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p4
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝¹ : ¬p1
h✝ : p2
h : ¬p3
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p4
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝¹ : ¬p1
h✝ : p2
h : ¬p3
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p4
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝¹ : ¬p1
h✝ : ¬p2
h : p3
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p4
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝¹ : ¬p1
h✝ : ¬p2
h : p3
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p4
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝¹ : ¬p1
h✝ : ¬p2
h : ¬p3
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p4
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝¹ : ¬p1
h✝ : ¬p2
h : ¬p3
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p4
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝² : p1
h✝¹ : p2
h✝ : p3
h : p4
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p5
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝² : p1
h✝¹ : p2
h✝ : p3
h : p4
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p5
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝² : p1
h✝¹ : p2
h✝ : p3
h : ¬p4
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p5
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝² : p1
h✝¹ : p2
h✝ : p3
h : ¬p4
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p5
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝² : p1
h✝¹ : p2
h✝ : ¬p3
h : p4
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p5
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝² : p1
h✝¹ : p2
h✝ : ¬p3
h : p4
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p5
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝² : p1
h✝¹ : p2
h✝ : ¬p3
h : ¬p4
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p5
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝² : p1
h✝¹ : p2
h✝ : ¬p3
h : ¬p4
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p5
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝² : p1
h✝¹ : ¬p2
h✝ : p3
h : p4
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p5
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝² : p1
h✝¹ : ¬p2
h✝ : p3
h : p4
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p5
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝² : p1
h✝¹ : ¬p2
h✝ : p3
h : ¬p4
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p5
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝² : p1
h✝¹ : ¬p2
h✝ : p3
h : ¬p4
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p5
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝² : p1
h✝¹ : ¬p2
h✝ : ¬p3
h : p4
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p5
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝² : p1
h✝¹ : ¬p2
h✝ : ¬p3
h : p4
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p5
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝² : p1
h✝¹ : ¬p2
h✝ : ¬p3
h : ¬p4
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p5
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝² : p1
h✝¹ : ¬p2
h✝ : ¬p3
h : ¬p4
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p5
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝² : ¬p1
h✝¹ : p2
h✝ : p3
h : p4
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p5
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝² : ¬p1
h✝¹ : p2
h✝ : p3
h : p4
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p5
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝² : ¬p1
h✝¹ : p2
h✝ : p3
h : ¬p4
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p5
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝² : ¬p1
h✝¹ : p2
h✝ : p3
h : ¬p4
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p5
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝² : ¬p1
h✝¹ : p2
h✝ : ¬p3
h : p4
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p5
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝² : ¬p1
h✝¹ : p2
h✝ : ¬p3
h : p4
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p5
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝² : ¬p1
h✝¹ : p2
h✝ : ¬p3
h : ¬p4
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p5
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝² : ¬p1
h✝¹ : p2
h✝ : ¬p3
h : ¬p4
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p5
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝² : ¬p1
h✝¹ : ¬p2
h✝ : p3
h : p4
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p5
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝² : ¬p1
h✝¹ : ¬p2
h✝ : p3
h : p4
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p5
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝² : ¬p1
h✝¹ : ¬p2
h✝ : p3
h : ¬p4
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p5
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝² : ¬p1
h✝¹ : ¬p2
h✝ : p3
h : ¬p4
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p5
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝² : ¬p1
h✝¹ : ¬p2
h✝ : ¬p3
h : p4
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p5
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝² : ¬p1
h✝¹ : ¬p2
h✝ : ¬p3
h : p4
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p5
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝² : ¬p1
h✝¹ : ¬p2
h✝ : ¬p3
h : ¬p4
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p5
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝² : ¬p1
h✝¹ : ¬p2
h✝ : ¬p3
h : ¬p4
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
by_cases p5
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝³ : p1
h✝² : p2
h✝¹ : p3
h✝ : p4
h : p5
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝³ : p1
h✝² : p2
h✝¹ : p3
h✝ : p4
h : ¬p5
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
simp [*]
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝³ : p1
h✝² : p2
h✝¹ : p3
h✝ : ¬p4
h : p5
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝³ : p1
h✝² : p2
h✝¹ : p3
h✝ : ¬p4
h : ¬p5
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
simp [*]
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝³ : p1
h✝² : p2
h✝¹ : ¬p3
h✝ : p4
h : p5
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝³ : p1
h✝² : p2
h✝¹ : ¬p3
h✝ : p4
h : ¬p5
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
simp [*]
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝³ : p1
h✝² : p2
h✝¹ : ¬p3
h✝ : ¬p4
h : p5
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝³ : p1
h✝² : p2
h✝¹ : ¬p3
h✝ : ¬p4
h : ¬p5
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
simp [*]
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝³ : p1
h✝² : ¬p2
h✝¹ : p3
h✝ : p4
h : p5
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝³ : p1
h✝² : ¬p2
h✝¹ : p3
h✝ : p4
h : ¬p5
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
simp [*]
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝³ : p1
h✝² : ¬p2
h✝¹ : p3
h✝ : ¬p4
h : p5
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝³ : p1
h✝² : ¬p2
h✝¹ : p3
h✝ : ¬p4
h : ¬p5
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
simp [*]
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝³ : p1
h✝² : ¬p2
h✝¹ : ¬p3
h✝ : p4
h : p5
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝³ : p1
h✝² : ¬p2
h✝¹ : ¬p3
h✝ : p4
h : ¬p5
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
simp [*]
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝³ : p1
h✝² : ¬p2
h✝¹ : ¬p3
h✝ : ¬p4
h : p5
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝³ : p1
h✝² : ¬p2
h✝¹ : ¬p3
h✝ : ¬p4
h : ¬p5
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
simp [*]
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝³ : ¬p1
h✝² : p2
h✝¹ : p3
h✝ : p4
h : p5
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝³ : ¬p1
h✝² : p2
h✝¹ : p3
h✝ : p4
h : ¬p5
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
simp [*]
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝³ : ¬p1
h✝² : p2
h✝¹ : p3
h✝ : ¬p4
h : p5
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝³ : ¬p1
h✝² : p2
h✝¹ : p3
h✝ : ¬p4
h : ¬p5
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
simp [*]
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝³ : ¬p1
h✝² : p2
h✝¹ : ¬p3
h✝ : p4
h : p5
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝³ : ¬p1
h✝² : p2
h✝¹ : ¬p3
h✝ : p4
h : ¬p5
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
simp [*]
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝³ : ¬p1
h✝² : p2
h✝¹ : ¬p3
h✝ : ¬p4
h : p5
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝³ : ¬p1
h✝² : p2
h✝¹ : ¬p3
h✝ : ¬p4
h : ¬p5
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
simp [*]
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝³ : ¬p1
h✝² : ¬p2
h✝¹ : p3
h✝ : p4
h : p5
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝³ : ¬p1
h✝² : ¬p2
h✝¹ : p3
h✝ : p4
h : ¬p5
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
simp [*]
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝³ : ¬p1
h✝² : ¬p2
h✝¹ : p3
h✝ : ¬p4
h : p5
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝³ : ¬p1
h✝² : ¬p2
h✝¹ : p3
h✝ : ¬p4
h : ¬p5
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
simp [*]
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝³ : ¬p1
h✝² : ¬p2
h✝¹ : ¬p3
h✝ : p4
h : p5
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝³ : ¬p1
h✝² : ¬p2
h✝¹ : ¬p3
h✝ : p4
h : ¬p5
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
simp [*]
[GOAL]
case pos
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝³ : ¬p1
h✝² : ¬p2
h✝¹ : ¬p3
h✝ : ¬p4
h : p5
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
inst✝ : Preorder α
a b c : α
p1 p2 p3 p4 p5 : Prop
h✝³ : ¬p1
h✝² : ¬p2
h✝¹ : ¬p3
h✝ : ¬p4
h : ¬p5
⊢ (p1 → p5 → p3) →
    (p5 → p4 → p2) →
      (p4 → p1 → c ≤ b) →
        ((p1 ∧ ¬p2) ∧ p5 ∧ ¬c ≤ b ∨ (p5 ∧ ¬c ≤ b) ∧ p4 ∧ ¬p3 ∨ (p4 ∧ ¬p3) ∧ p1 ∧ ¬p2 ↔
          (p1 ∧ p5 ∨ p5 ∧ p4 ∨ p4 ∧ p1) ∧ ¬(c ≤ b ∧ p2 ∨ p2 ∧ p3 ∨ p3 ∧ c ≤ b))
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
inst✝ : Preorder α
a b c d : α
⊢ sbtw a b c → sbtw b d c → sbtw a d c
[PROOFSTEP]
rintro (⟨hab, hbc⟩ | ⟨hbc, hca⟩ | ⟨hca, hab⟩) (⟨hbd, hdc⟩ | ⟨hdc, hcb⟩ | ⟨hcb, hbd⟩)
[GOAL]
case inl.intro.inl.intro
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hbd : b < d
hdc : d < c
⊢ sbtw a d c
[PROOFSTEP]
exact Or.inl ⟨hab.trans hbd, hdc⟩
[GOAL]
case inl.intro.inr.inl.intro
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hdc : d < c
hcb : c < b
⊢ sbtw a d c
[PROOFSTEP]
exact (hbc.not_lt hcb).elim
[GOAL]
case inl.intro.inr.inr.intro
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hcb : c < b
hbd : b < d
⊢ sbtw a d c
[PROOFSTEP]
exact (hbc.not_lt hcb).elim
[GOAL]
case inr.inl.intro.inl.intro
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hbd : b < d
hdc : d < c
⊢ sbtw a d c
[PROOFSTEP]
exact Or.inr (Or.inl ⟨hdc, hca⟩)
[GOAL]
case inr.inl.intro.inr.inl.intro
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hdc : d < c
hcb : c < b
⊢ sbtw a d c
[PROOFSTEP]
exact Or.inr (Or.inl ⟨hdc, hca⟩)
[GOAL]
case inr.inl.intro.inr.inr.intro
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hcb : c < b
hbd : b < d
⊢ sbtw a d c
[PROOFSTEP]
exact (hbc.not_lt hcb).elim
[GOAL]
case inr.inr.intro.inl.intro
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hbd : b < d
hdc : d < c
⊢ sbtw a d c
[PROOFSTEP]
exact Or.inr (Or.inl ⟨hdc, hca⟩)
[GOAL]
case inr.inr.intro.inr.inl.intro
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hdc : d < c
hcb : c < b
⊢ sbtw a d c
[PROOFSTEP]
exact Or.inr (Or.inl ⟨hdc, hca⟩)
[GOAL]
case inr.inr.intro.inr.inr.intro
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
⊢ sbtw a d c
[PROOFSTEP]
exact Or.inr (Or.inr ⟨hca, hab.trans hbd⟩)
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
src✝ : CircularPreorder α := Preorder.toCircularPreorder α
a b c : α
⊢ btw a b c → btw c b a → a = b ∨ b = c ∨ c = a
[PROOFSTEP]
rintro (⟨hab, hbc⟩ | ⟨hbc, hca⟩ | ⟨hca, hab⟩) (⟨hcb, hba⟩ | ⟨hba, hac⟩ | ⟨hac, hcb⟩)
[GOAL]
case inl.intro.inl.intro
α : Type u_1
inst✝ : PartialOrder α
src✝ : CircularPreorder α := Preorder.toCircularPreorder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hcb : c ≤ b
hba : b ≤ a
⊢ a = b ∨ b = c ∨ c = a
[PROOFSTEP]
exact Or.inl (hab.antisymm hba)
[GOAL]
case inl.intro.inr.inl.intro
α : Type u_1
inst✝ : PartialOrder α
src✝ : CircularPreorder α := Preorder.toCircularPreorder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hba : b ≤ a
hac : a ≤ c
⊢ a = b ∨ b = c ∨ c = a
[PROOFSTEP]
exact Or.inl (hab.antisymm hba)
[GOAL]
case inl.intro.inr.inr.intro
α : Type u_1
inst✝ : PartialOrder α
src✝ : CircularPreorder α := Preorder.toCircularPreorder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hac : a ≤ c
hcb : c ≤ b
⊢ a = b ∨ b = c ∨ c = a
[PROOFSTEP]
exact Or.inr (Or.inl <| hbc.antisymm hcb)
[GOAL]
case inr.inl.intro.inl.intro
α : Type u_1
inst✝ : PartialOrder α
src✝ : CircularPreorder α := Preorder.toCircularPreorder α
a b c : α
hbc : b ≤ c
hca : c ≤ a
hcb : c ≤ b
hba : b ≤ a
⊢ a = b ∨ b = c ∨ c = a
[PROOFSTEP]
exact Or.inr (Or.inl <| hbc.antisymm hcb)
[GOAL]
case inr.inl.intro.inr.inl.intro
α : Type u_1
inst✝ : PartialOrder α
src✝ : CircularPreorder α := Preorder.toCircularPreorder α
a b c : α
hbc : b ≤ c
hca : c ≤ a
hba : b ≤ a
hac : a ≤ c
⊢ a = b ∨ b = c ∨ c = a
[PROOFSTEP]
exact Or.inr (Or.inr <| hca.antisymm hac)
[GOAL]
case inr.inl.intro.inr.inr.intro
α : Type u_1
inst✝ : PartialOrder α
src✝ : CircularPreorder α := Preorder.toCircularPreorder α
a b c : α
hbc : b ≤ c
hca : c ≤ a
hac : a ≤ c
hcb : c ≤ b
⊢ a = b ∨ b = c ∨ c = a
[PROOFSTEP]
exact Or.inr (Or.inl <| hbc.antisymm hcb)
[GOAL]
case inr.inr.intro.inl.intro
α : Type u_1
inst✝ : PartialOrder α
src✝ : CircularPreorder α := Preorder.toCircularPreorder α
a b c : α
hca : c ≤ a
hab : a ≤ b
hcb : c ≤ b
hba : b ≤ a
⊢ a = b ∨ b = c ∨ c = a
[PROOFSTEP]
exact Or.inl (hab.antisymm hba)
[GOAL]
case inr.inr.intro.inr.inl.intro
α : Type u_1
inst✝ : PartialOrder α
src✝ : CircularPreorder α := Preorder.toCircularPreorder α
a b c : α
hca : c ≤ a
hab : a ≤ b
hba : b ≤ a
hac : a ≤ c
⊢ a = b ∨ b = c ∨ c = a
[PROOFSTEP]
exact Or.inl (hab.antisymm hba)
[GOAL]
case inr.inr.intro.inr.inr.intro
α : Type u_1
inst✝ : PartialOrder α
src✝ : CircularPreorder α := Preorder.toCircularPreorder α
a b c : α
hca : c ≤ a
hab : a ≤ b
hac : a ≤ c
hcb : c ≤ b
⊢ a = b ∨ b = c ∨ c = a
[PROOFSTEP]
exact Or.inr (Or.inr <| hca.antisymm hac)
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
src✝ : CircularPartialOrder α := PartialOrder.toCircularPartialOrder α
a b c : α
⊢ btw a b c ∨ btw c b a
[PROOFSTEP]
cases' le_total a b with hab hba
[GOAL]
case inl
α : Type u_1
inst✝ : LinearOrder α
src✝ : CircularPartialOrder α := PartialOrder.toCircularPartialOrder α
a b c : α
hab : a ≤ b
⊢ btw a b c ∨ btw c b a
[PROOFSTEP]
cases' le_total b c with hbc hcb
[GOAL]
case inr
α : Type u_1
inst✝ : LinearOrder α
src✝ : CircularPartialOrder α := PartialOrder.toCircularPartialOrder α
a b c : α
hba : b ≤ a
⊢ btw a b c ∨ btw c b a
[PROOFSTEP]
cases' le_total b c with hbc hcb
[GOAL]
case inl.inl
α : Type u_1
inst✝ : LinearOrder α
src✝ : CircularPartialOrder α := PartialOrder.toCircularPartialOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ btw a b c ∨ btw c b a
[PROOFSTEP]
cases' le_total c a with hca hac
[GOAL]
case inl.inr
α : Type u_1
inst✝ : LinearOrder α
src✝ : CircularPartialOrder α := PartialOrder.toCircularPartialOrder α
a b c : α
hab : a ≤ b
hcb : c ≤ b
⊢ btw a b c ∨ btw c b a
[PROOFSTEP]
cases' le_total c a with hca hac
[GOAL]
case inr.inl
α : Type u_1
inst✝ : LinearOrder α
src✝ : CircularPartialOrder α := PartialOrder.toCircularPartialOrder α
a b c : α
hba : b ≤ a
hbc : b ≤ c
⊢ btw a b c ∨ btw c b a
[PROOFSTEP]
cases' le_total c a with hca hac
[GOAL]
case inr.inr
α : Type u_1
inst✝ : LinearOrder α
src✝ : CircularPartialOrder α := PartialOrder.toCircularPartialOrder α
a b c : α
hba : b ≤ a
hcb : c ≤ b
⊢ btw a b c ∨ btw c b a
[PROOFSTEP]
cases' le_total c a with hca hac
[GOAL]
case inl.inl.inl
α : Type u_1
inst✝ : LinearOrder α
src✝ : CircularPartialOrder α := PartialOrder.toCircularPartialOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hca : c ≤ a
⊢ btw a b c ∨ btw c b a
[PROOFSTEP]
exact Or.inl (Or.inl ⟨hab, hbc⟩)
[GOAL]
case inl.inl.inr
α : Type u_1
inst✝ : LinearOrder α
src✝ : CircularPartialOrder α := PartialOrder.toCircularPartialOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hac : a ≤ c
⊢ btw a b c ∨ btw c b a
[PROOFSTEP]
exact Or.inl (Or.inl ⟨hab, hbc⟩)
[GOAL]
case inl.inr.inl
α : Type u_1
inst✝ : LinearOrder α
src✝ : CircularPartialOrder α := PartialOrder.toCircularPartialOrder α
a b c : α
hab : a ≤ b
hcb : c ≤ b
hca : c ≤ a
⊢ btw a b c ∨ btw c b a
[PROOFSTEP]
exact Or.inl (Or.inr <| Or.inr ⟨hca, hab⟩)
[GOAL]
case inl.inr.inr
α : Type u_1
inst✝ : LinearOrder α
src✝ : CircularPartialOrder α := PartialOrder.toCircularPartialOrder α
a b c : α
hab : a ≤ b
hcb : c ≤ b
hac : a ≤ c
⊢ btw a b c ∨ btw c b a
[PROOFSTEP]
exact Or.inr (Or.inr <| Or.inr ⟨hac, hcb⟩)
[GOAL]
case inr.inl.inl
α : Type u_1
inst✝ : LinearOrder α
src✝ : CircularPartialOrder α := PartialOrder.toCircularPartialOrder α
a b c : α
hba : b ≤ a
hbc : b ≤ c
hca : c ≤ a
⊢ btw a b c ∨ btw c b a
[PROOFSTEP]
exact Or.inl (Or.inr <| Or.inl ⟨hbc, hca⟩)
[GOAL]
case inr.inl.inr
α : Type u_1
inst✝ : LinearOrder α
src✝ : CircularPartialOrder α := PartialOrder.toCircularPartialOrder α
a b c : α
hba : b ≤ a
hbc : b ≤ c
hac : a ≤ c
⊢ btw a b c ∨ btw c b a
[PROOFSTEP]
exact Or.inr (Or.inr <| Or.inl ⟨hba, hac⟩)
[GOAL]
case inr.inr.inl
α : Type u_1
inst✝ : LinearOrder α
src✝ : CircularPartialOrder α := PartialOrder.toCircularPartialOrder α
a b c : α
hba : b ≤ a
hcb : c ≤ b
hca : c ≤ a
⊢ btw a b c ∨ btw c b a
[PROOFSTEP]
exact Or.inr (Or.inl ⟨hcb, hba⟩)
[GOAL]
case inr.inr.inr
α : Type u_1
inst✝ : LinearOrder α
src✝ : CircularPartialOrder α := PartialOrder.toCircularPartialOrder α
a b c : α
hba : b ≤ a
hcb : c ≤ b
hac : a ≤ c
⊢ btw a b c ∨ btw c b a
[PROOFSTEP]
exact Or.inr (Or.inr <| Or.inl ⟨hba, hac⟩)
