[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c : Set α
h : ∀ (c : Set α), IsChain r c → ∃ ub, ∀ (a : α), a ∈ c → r a ub
trans : ∀ {a b c : α}, r a b → r b c → r a c
this✝ : ∃ ub, ∀ (a : α), a ∈ maxChain r → r a ub
ub : α
hub : ∀ (a : α), a ∈ maxChain r → r a ub
a : α
ha : r ub a
this : IsChain r (insert a (maxChain r))
⊢ a ∈ maxChain r
[PROOFSTEP]
rw [maxChain_spec.right this (subset_insert _ _)]
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c : Set α
h : ∀ (c : Set α), IsChain r c → ∃ ub, ∀ (a : α), a ∈ c → r a ub
trans : ∀ {a b c : α}, r a b → r b c → r a c
this✝ : ∃ ub, ∀ (a : α), a ∈ maxChain r → r a ub
ub : α
hub : ∀ (a : α), a ∈ maxChain r → r a ub
a : α
ha : r ub a
this : IsChain r (insert a (maxChain r))
⊢ a ∈ insert a (maxChain r)
[PROOFSTEP]
exact mem_insert _ _
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c✝ : Set α
inst✝ : Preorder α
s : Set α
ih : ∀ (c : Set α), c ⊆ s → IsChain (fun x x_1 => x ≤ x_1) c → ∃ ub, ub ∈ s ∧ ∀ (z : α), z ∈ c → z ≤ ub
c : Set ↑s
hc : IsChain (fun x x_1 => x ≤ x_1) c
⊢ IsChain (fun x x_1 => x ≤ x_1) (Subtype.val '' c)
[PROOFSTEP]
rintro _ ⟨p, hpc, rfl⟩ _ ⟨q, hqc, rfl⟩ hpq
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
r : α → α → Prop
c✝ : Set α
inst✝ : Preorder α
s : Set α
ih : ∀ (c : Set α), c ⊆ s → IsChain (fun x x_1 => x ≤ x_1) c → ∃ ub, ub ∈ s ∧ ∀ (z : α), z ∈ c → z ≤ ub
c : Set ↑s
hc : IsChain (fun x x_1 => x ≤ x_1) c
p : { x // x ∈ s }
hpc : p ∈ c
q : { x // x ∈ s }
hqc : q ∈ c
hpq : ↑p ≠ ↑q
⊢ (fun x x_1 => x ≤ x_1) ↑p ↑q ∨ (fun x x_1 => x ≤ x_1) ↑q ↑p
[PROOFSTEP]
refine' hc hpc hqc fun t => hpq (Subtype.ext_iff.1 t)
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c : Set α
inst✝ : Preorder α
s : Set α
ih :
  ∀ (c : Set α), c ⊆ s → IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : α), y ∈ c → ∃ ub, ub ∈ s ∧ ∀ (z : α), z ∈ c → z ≤ ub
x : α
hxs : x ∈ s
⊢ ∃ m, m ∈ s ∧ x ≤ m ∧ ∀ (z : α), z ∈ s → m ≤ z → z ≤ m
[PROOFSTEP]
have H := zorn_preorder₀ ({y ∈ s | x ≤ y}) fun c hcs hc => ?_
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
r : α → α → Prop
c : Set α
inst✝ : Preorder α
s : Set α
ih :
  ∀ (c : Set α), c ⊆ s → IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : α), y ∈ c → ∃ ub, ub ∈ s ∧ ∀ (z : α), z ∈ c → z ≤ ub
x : α
hxs : x ∈ s
H : ∃ m, m ∈ {y | y ∈ s ∧ x ≤ y} ∧ ∀ (z : α), z ∈ {y | y ∈ s ∧ x ≤ y} → m ≤ z → z ≤ m
⊢ ∃ m, m ∈ s ∧ x ≤ m ∧ ∀ (z : α), z ∈ s → m ≤ z → z ≤ m
[PROOFSTEP]
rcases H with ⟨m, ⟨hms, hxm⟩, hm⟩
[GOAL]
case refine_2.intro.intro.intro
α : Type u_1
β : Type u_2
r : α → α → Prop
c : Set α
inst✝ : Preorder α
s : Set α
ih :
  ∀ (c : Set α), c ⊆ s → IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : α), y ∈ c → ∃ ub, ub ∈ s ∧ ∀ (z : α), z ∈ c → z ≤ ub
x : α
hxs : x ∈ s
m : α
hm : ∀ (z : α), z ∈ {y | y ∈ s ∧ x ≤ y} → m ≤ z → z ≤ m
hms : m ∈ s
hxm : x ≤ m
⊢ ∃ m, m ∈ s ∧ x ≤ m ∧ ∀ (z : α), z ∈ s → m ≤ z → z ≤ m
[PROOFSTEP]
exact ⟨m, hms, hxm, fun z hzs hmz => hm _ ⟨hzs, hxm.trans hmz⟩ hmz⟩
[GOAL]
case refine_1
α : Type u_1
β : Type u_2
r : α → α → Prop
c✝ : Set α
inst✝ : Preorder α
s : Set α
ih :
  ∀ (c : Set α), c ⊆ s → IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : α), y ∈ c → ∃ ub, ub ∈ s ∧ ∀ (z : α), z ∈ c → z ≤ ub
x : α
hxs : x ∈ s
c : Set α
hcs : c ⊆ {y | y ∈ s ∧ x ≤ y}
hc : IsChain (fun x x_1 => x ≤ x_1) c
⊢ ∃ ub, ub ∈ {y | y ∈ s ∧ x ≤ y} ∧ ∀ (z : α), z ∈ c → z ≤ ub
[PROOFSTEP]
rcases c.eq_empty_or_nonempty with (rfl | ⟨y, hy⟩)
[GOAL]
case refine_1.inl
α : Type u_1
β : Type u_2
r : α → α → Prop
c : Set α
inst✝ : Preorder α
s : Set α
ih :
  ∀ (c : Set α), c ⊆ s → IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : α), y ∈ c → ∃ ub, ub ∈ s ∧ ∀ (z : α), z ∈ c → z ≤ ub
x : α
hxs : x ∈ s
hcs : ∅ ⊆ {y | y ∈ s ∧ x ≤ y}
hc : IsChain (fun x x_1 => x ≤ x_1) ∅
⊢ ∃ ub, ub ∈ {y | y ∈ s ∧ x ≤ y} ∧ ∀ (z : α), z ∈ ∅ → z ≤ ub
[PROOFSTEP]
exact ⟨x, ⟨hxs, le_rfl⟩, fun z => False.elim⟩
[GOAL]
case refine_1.inr.intro
α : Type u_1
β : Type u_2
r : α → α → Prop
c✝ : Set α
inst✝ : Preorder α
s : Set α
ih :
  ∀ (c : Set α), c ⊆ s → IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : α), y ∈ c → ∃ ub, ub ∈ s ∧ ∀ (z : α), z ∈ c → z ≤ ub
x : α
hxs : x ∈ s
c : Set α
hcs : c ⊆ {y | y ∈ s ∧ x ≤ y}
hc : IsChain (fun x x_1 => x ≤ x_1) c
y : α
hy : y ∈ c
⊢ ∃ ub, ub ∈ {y | y ∈ s ∧ x ≤ y} ∧ ∀ (z : α), z ∈ c → z ≤ ub
[PROOFSTEP]
rcases ih c (fun z hz => (hcs hz).1) hc y hy with ⟨z, hzs, hz⟩
[GOAL]
case refine_1.inr.intro.intro.intro
α : Type u_1
β : Type u_2
r : α → α → Prop
c✝ : Set α
inst✝ : Preorder α
s : Set α
ih :
  ∀ (c : Set α), c ⊆ s → IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : α), y ∈ c → ∃ ub, ub ∈ s ∧ ∀ (z : α), z ∈ c → z ≤ ub
x : α
hxs : x ∈ s
c : Set α
hcs : c ⊆ {y | y ∈ s ∧ x ≤ y}
hc : IsChain (fun x x_1 => x ≤ x_1) c
y : α
hy : y ∈ c
z : α
hzs : z ∈ s
hz : ∀ (z_1 : α), z_1 ∈ c → z_1 ≤ z
⊢ ∃ ub, ub ∈ {y | y ∈ s ∧ x ≤ y} ∧ ∀ (z : α), z ∈ c → z ≤ ub
[PROOFSTEP]
exact ⟨z, ⟨hzs, (hcs hy).2.trans <| hz _ hy⟩, hz⟩
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c : Set α
inst✝ : Preorder α
a : α
ih :
  ∀ (c : Set α),
    c ⊆ Ici a → IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : α), y ∈ c → ∃ ub, a ≤ ub ∧ ∀ (z : α), z ∈ c → z ≤ ub
x : α
hax : a ≤ x
⊢ ∀ (c : Set α),
    c ⊆ Ici a → IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : α), y ∈ c → ∃ ub, ub ∈ Ici a ∧ ∀ (z : α), z ∈ c → z ≤ ub
[PROOFSTEP]
simpa using ih
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c : Set α
hc : IsChain r c
⊢ ∃ M, IsMaxChain r M ∧ c ⊆ M
[PROOFSTEP]
have H := zorn_subset_nonempty {s | c ⊆ s ∧ IsChain r s} ?_ c ⟨Subset.rfl, hc⟩
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
r : α → α → Prop
c : Set α
hc : IsChain r c
H : ∃ m, m ∈ {s | c ⊆ s ∧ IsChain r s} ∧ c ⊆ m ∧ ∀ (a : Set α), a ∈ {s | c ⊆ s ∧ IsChain r s} → m ⊆ a → a = m
⊢ ∃ M, IsMaxChain r M ∧ c ⊆ M
[PROOFSTEP]
obtain ⟨M, ⟨_, hM₀⟩, hM₁, hM₂⟩ := H
[GOAL]
case refine_2.intro.intro.intro.intro
α : Type u_1
β : Type u_2
r : α → α → Prop
c : Set α
hc : IsChain r c
M : Set α
left✝ : c ⊆ M
hM₀ : IsChain r M
hM₁ : c ⊆ M
hM₂ : ∀ (a : Set α), a ∈ {s | c ⊆ s ∧ IsChain r s} → M ⊆ a → a = M
⊢ ∃ M, IsMaxChain r M ∧ c ⊆ M
[PROOFSTEP]
exact ⟨M, ⟨hM₀, fun d hd hMd => (hM₂ _ ⟨hM₁.trans hMd, hd⟩ hMd).symm⟩, hM₁⟩
[GOAL]
case refine_1
α : Type u_1
β : Type u_2
r : α → α → Prop
c : Set α
hc : IsChain r c
⊢ ∀ (c_1 : Set (Set α)),
    c_1 ⊆ {s | c ⊆ s ∧ IsChain r s} →
      IsChain (fun x x_1 => x ⊆ x_1) c_1 →
        Set.Nonempty c_1 → ∃ ub, ub ∈ {s | c ⊆ s ∧ IsChain r s} ∧ ∀ (s : Set α), s ∈ c_1 → s ⊆ ub
[PROOFSTEP]
rintro cs hcs₀ hcs₁ ⟨s, hs⟩
[GOAL]
case refine_1.intro
α : Type u_1
β : Type u_2
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x x_1 => x ⊆ x_1) cs
s : Set α
hs : s ∈ cs
⊢ ∃ ub, ub ∈ {s | c ⊆ s ∧ IsChain r s} ∧ ∀ (s : Set α), s ∈ cs → s ⊆ ub
[PROOFSTEP]
refine' ⟨⋃₀ cs, ⟨fun _ ha => Set.mem_sUnion_of_mem ((hcs₀ hs).left ha) hs, _⟩, fun _ => Set.subset_sUnion_of_mem⟩
[GOAL]
case refine_1.intro
α : Type u_1
β : Type u_2
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x x_1 => x ⊆ x_1) cs
s : Set α
hs : s ∈ cs
⊢ IsChain r (⋃₀ cs)
[PROOFSTEP]
rintro y ⟨sy, hsy, hysy⟩ z ⟨sz, hsz, hzsz⟩ hyz
[GOAL]
case refine_1.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x x_1 => x ⊆ x_1) cs
s : Set α
hs : s ∈ cs
y : α
sy : Set α
hsy : sy ∈ cs
hysy : y ∈ sy
z : α
sz : Set α
hsz : sz ∈ cs
hzsz : z ∈ sz
hyz : y ≠ z
⊢ r y z ∨ r z y
[PROOFSTEP]
obtain rfl | hsseq := eq_or_ne sy sz
[GOAL]
case refine_1.intro.intro.intro.intro.intro.inl
α : Type u_1
β : Type u_2
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x x_1 => x ⊆ x_1) cs
s : Set α
hs : s ∈ cs
y : α
sy : Set α
hsy : sy ∈ cs
hysy : y ∈ sy
z : α
hyz : y ≠ z
hsz : sy ∈ cs
hzsz : z ∈ sy
⊢ r y z ∨ r z y
[PROOFSTEP]
exact (hcs₀ hsy).right hysy hzsz hyz
[GOAL]
case refine_1.intro.intro.intro.intro.intro.inr
α : Type u_1
β : Type u_2
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x x_1 => x ⊆ x_1) cs
s : Set α
hs : s ∈ cs
y : α
sy : Set α
hsy : sy ∈ cs
hysy : y ∈ sy
z : α
sz : Set α
hsz : sz ∈ cs
hzsz : z ∈ sz
hyz : y ≠ z
hsseq : sy ≠ sz
⊢ r y z ∨ r z y
[PROOFSTEP]
cases' hcs₁ hsy hsz hsseq with h h
[GOAL]
case refine_1.intro.intro.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x x_1 => x ⊆ x_1) cs
s : Set α
hs : s ∈ cs
y : α
sy : Set α
hsy : sy ∈ cs
hysy : y ∈ sy
z : α
sz : Set α
hsz : sz ∈ cs
hzsz : z ∈ sz
hyz : y ≠ z
hsseq : sy ≠ sz
h : (fun x x_1 => x ⊆ x_1) sy sz
⊢ r y z ∨ r z y
[PROOFSTEP]
exact (hcs₀ hsz).right (h hysy) hzsz hyz
[GOAL]
case refine_1.intro.intro.intro.intro.intro.inr.inr
α : Type u_1
β : Type u_2
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x x_1 => x ⊆ x_1) cs
s : Set α
hs : s ∈ cs
y : α
sy : Set α
hsy : sy ∈ cs
hysy : y ∈ sy
z : α
sz : Set α
hsz : sz ∈ cs
hzsz : z ∈ sz
hyz : y ≠ z
hsseq : sy ≠ sz
h : (fun x x_1 => x ⊆ x_1) sz sy
⊢ r y z ∨ r z y
[PROOFSTEP]
exact (hcs₀ hsy).right hysy (h hzsz) hyz


[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⟩)


[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
⊢ ∀ ⦃b : α⦄, b ∈ {a} → r a b → r b a
[PROOFSTEP]
rintro b (rfl : b = a)
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
b✝ b : α
⊢ r b b → r b b
[PROOFSTEP]
exact id
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
inst✝ : IsAntisymm α r
x : α
⊢ x ∈ maximals r s ↔ x ∈ s ∧ ∀ ⦃y : α⦄, y ∈ s → r x y → x = y
[PROOFSTEP]
simp only [maximals, Set.mem_sep_iff, and_congr_right_iff]
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
inst✝ : IsAntisymm α r
x : α
⊢ x ∈ s → ((∀ ⦃b : α⦄, b ∈ s → r x b → r b x) ↔ ∀ ⦃y : α⦄, y ∈ s → r x y → x = y)
[PROOFSTEP]
refine' fun _ ↦ ⟨fun h y hys hxy ↦ antisymm hxy (h hys hxy), fun h y hys hxy ↦ _⟩
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
inst✝ : IsAntisymm α r
x : α
x✝ : x ∈ s
h : ∀ ⦃y : α⦄, y ∈ s → r x y → x = y
y : α
hys : y ∈ s
hxy : r x y
⊢ r y x
[PROOFSTEP]
convert hxy
[GOAL]
case h.e'_1
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
inst✝ : IsAntisymm α r
x : α
x✝ : x ∈ s
h : ∀ ⦃y : α⦄, y ∈ s → r x y → x = y
y : α
hys : y ∈ s
hxy : r x y
⊢ y = x
[PROOFSTEP]
rw [h hys hxy]
[GOAL]
case h.e'_2
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
inst✝ : IsAntisymm α r
x : α
x✝ : x ∈ s
h : ∀ ⦃y : α⦄, y ∈ s → r x y → x = y
y : α
hys : y ∈ s
hxy : r x y
⊢ x = y
[PROOFSTEP]
rw [h hys hxy]
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
inst✝¹ : IsAntisymm α r
x : α
rlt : α → α → Prop
inst✝ : IsNonstrictStrictOrder α r rlt
⊢ x ∈ minimals r s ↔ x ∈ s ∧ ∀ ⦃y : α⦄, rlt y x → ¬y ∈ s
[PROOFSTEP]
simp [minimals, right_iff_left_not_left_of r rlt, not_imp_not, imp.swap (a := _ ∈ _)]
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
inst✝¹ : IsAntisymm α r
x : α
rlt : α → α → Prop
inst✝ : IsNonstrictStrictOrder α r rlt
⊢ x ∈ maximals r s ↔ x ∈ s ∧ ∀ ⦃y : α⦄, rlt x y → ¬y ∈ s
[PROOFSTEP]
simp [maximals, right_iff_left_not_left_of r rlt, not_imp_not, imp.swap (a := _ ∈ _)]
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
inst✝¹ : IsAntisymm α r
inst✝ : IsTrans α r
hts : t ⊆ s
h : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ r y x
⊢ minimals r s = minimals r t
[PROOFSTEP]
refine
  Set.ext fun a ↦ ⟨fun ⟨has, hmin⟩ ↦ ⟨?_, fun b hbt ↦ hmin (hts hbt)⟩, fun ⟨hat, hmin⟩ ↦ ⟨hts hat, fun b hbs hba ↦ ?_⟩⟩
[GOAL]
case refine_1
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b : α
inst✝¹ : IsAntisymm α r
inst✝ : IsTrans α r
hts : t ⊆ s
h : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ r y x
a : α
x✝ : a ∈ minimals r s
has : a ∈ s
hmin : ∀ ⦃b : α⦄, b ∈ s → r b a → r a b
⊢ a ∈ t
[PROOFSTEP]
obtain ⟨a', ha', haa'⟩ := h _ has
[GOAL]
case refine_1.intro.intro
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b : α
inst✝¹ : IsAntisymm α r
inst✝ : IsTrans α r
hts : t ⊆ s
h : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ r y x
a : α
x✝ : a ∈ minimals r s
has : a ∈ s
hmin : ∀ ⦃b : α⦄, b ∈ s → r b a → r a b
a' : α
ha' : a' ∈ t
haa' : r a' a
⊢ a ∈ t
[PROOFSTEP]
rwa [antisymm (hmin (hts ha') haa') haa']
[GOAL]
case refine_2
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
inst✝¹ : IsAntisymm α r
inst✝ : IsTrans α r
hts : t ⊆ s
h : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ r y x
a : α
x✝ : a ∈ minimals r t
hat : a ∈ t
hmin : ∀ ⦃b : α⦄, b ∈ t → r b a → r a b
b : α
hbs : b ∈ s
hba : r b a
⊢ r a b
[PROOFSTEP]
obtain ⟨b', hb't, hb'b⟩ := h b hbs
[GOAL]
case refine_2.intro.intro
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
inst✝¹ : IsAntisymm α r
inst✝ : IsTrans α r
hts : t ⊆ s
h : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ r y x
a : α
x✝ : a ∈ minimals r t
hat : a ∈ t
hmin : ∀ ⦃b : α⦄, b ∈ t → r b a → r a b
b : α
hbs : b ∈ s
hba : r b a
b' : α
hb't : b' ∈ t
hb'b : r b' b
⊢ r a b
[PROOFSTEP]
rwa [antisymm (hmin hb't (Trans.trans hb'b hba)) (Trans.trans hb'b hba)]
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
inst✝ : IsSymm α r
⊢ maximals r s = minimals r s
[PROOFSTEP]
rw [minimals_of_symm, maximals_of_symm]
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
h : Set.Subsingleton s
⊢ maximals r s = s
[PROOFSTEP]
rcases h.eq_empty_or_singleton with (rfl | ⟨x, rfl⟩)
[GOAL]
case inl
α : Type u_1
r r₁ r₂ : α → α → Prop
t : Set α
a b : α
h : Set.Subsingleton ∅
⊢ maximals r ∅ = ∅
case inr.intro α : Type u_1 r r₁ r₂ : α → α → Prop t : Set α a b x : α h : Set.Subsingleton {x} ⊢ maximals r {x} = {x}
[PROOFSTEP]
exacts [minimals_empty _, maximals_singleton _ _]
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
inst✝ : IsAntisymm α r₂
h : ∀ (a b : α), r₁ a b → r₂ a b
a : α
ha : a ∈ maximals r₂ s
b : α
hb : b ∈ s
hab : r₁ a b
⊢ r₁ b a
[PROOFSTEP]
have := eq_of_mem_maximals ha hb (h _ _ hab)
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
inst✝ : IsAntisymm α r₂
h : ∀ (a b : α), r₁ a b → r₂ a b
a : α
ha : a ∈ maximals r₂ s
b : α
hb : b ∈ s
hab : r₁ a b
this : a = b
⊢ r₁ b a
[PROOFSTEP]
subst this
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b : α
inst✝ : IsAntisymm α r₂
h : ∀ (a b : α), r₁ a b → r₂ a b
a : α
ha : a ∈ maximals r₂ s
hb : a ∈ s
hab : r₁ a a
⊢ r₁ a a
[PROOFSTEP]
exact hab
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
inst✝ : IsAntisymm α r₂
h : ∀ (a b : α), r₁ a b → r₂ a b
a : α
ha : a ∈ minimals r₂ s
b : α
hb : b ∈ s
hab : r₁ b a
⊢ r₁ a b
[PROOFSTEP]
have := eq_of_mem_minimals ha hb (h _ _ hab)
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
inst✝ : IsAntisymm α r₂
h : ∀ (a b : α), r₁ a b → r₂ a b
a : α
ha : a ∈ minimals r₂ s
b : α
hb : b ∈ s
hab : r₁ b a
this : a = b
⊢ r₁ a b
[PROOFSTEP]
subst this
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b : α
inst✝ : IsAntisymm α r₂
h : ∀ (a b : α), r₁ a b → r₂ a b
a : α
ha : a ∈ minimals r₂ s
hb : a ∈ s
hab : r₁ a a
⊢ r₁ a a
[PROOFSTEP]
exact hab
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
⊢ maximals r (s ∪ t) ⊆ maximals r s ∪ maximals r t
[PROOFSTEP]
intro a ha
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b a : α
ha : a ∈ maximals r (s ∪ t)
⊢ a ∈ maximals r s ∪ maximals r t
[PROOFSTEP]
obtain h | h := ha.1
[GOAL]
case inl
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b a : α
ha : a ∈ maximals r (s ∪ t)
h : a ∈ s
⊢ a ∈ maximals r s ∪ maximals r t
[PROOFSTEP]
exact Or.inl ⟨h, fun b hb => ha.2 <| Or.inl hb⟩
[GOAL]
case inr
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b a : α
ha : a ∈ maximals r (s ∪ t)
h : a ∈ t
⊢ a ∈ maximals r s ∪ maximals r t
[PROOFSTEP]
exact Or.inr ⟨h, fun b hb => ha.2 <| Or.inr hb⟩
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : r a b
⊢ r b a
[PROOFSTEP]
obtain rfl := h.eq ha hb hab
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b : α
h : IsAntichain r s
a : α
ha hb : a ∈ s
hab : r a a
⊢ r a a
[PROOFSTEP]
exact hab
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
ht : IsAntichain r t
h : maximals r s ⊆ t
hs : ∀ ⦃a : α⦄, a ∈ t → ∃ b, b ∈ maximals r s ∧ r b a
⊢ maximals r s = t
[PROOFSTEP]
refine' h.antisymm fun a ha => _
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b : α
ht : IsAntichain r t
h : maximals r s ⊆ t
hs : ∀ ⦃a : α⦄, a ∈ t → ∃ b, b ∈ maximals r s ∧ r b a
a : α
ha : a ∈ t
⊢ a ∈ maximals r s
[PROOFSTEP]
obtain ⟨b, hb, hr⟩ := hs ha
[GOAL]
case intro.intro
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
ht : IsAntichain r t
h : maximals r s ⊆ t
hs : ∀ ⦃a : α⦄, a ∈ t → ∃ b, b ∈ maximals r s ∧ r b a
a : α
ha : a ∈ t
b : α
hb : b ∈ maximals r s
hr : r b a
⊢ a ∈ maximals r s
[PROOFSTEP]
rwa [of_not_not fun hab => ht (h hb) ha (Ne.symm hab) hr]
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
ht : IsAntichain r t
h : minimals r s ⊆ t
hs : ∀ ⦃a : α⦄, a ∈ t → ∃ b, b ∈ minimals r s ∧ r a b
⊢ minimals r s = t
[PROOFSTEP]
refine' h.antisymm fun a ha => _
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b : α
ht : IsAntichain r t
h : minimals r s ⊆ t
hs : ∀ ⦃a : α⦄, a ∈ t → ∃ b, b ∈ minimals r s ∧ r a b
a : α
ha : a ∈ t
⊢ a ∈ minimals r s
[PROOFSTEP]
obtain ⟨b, hb, hr⟩ := hs ha
[GOAL]
case intro.intro
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
ht : IsAntichain r t
h : minimals r s ⊆ t
hs : ∀ ⦃a : α⦄, a ∈ t → ∃ b, b ∈ minimals r s ∧ r a b
a : α
ha : a ∈ t
b : α
hb : b ∈ minimals r s
hr : r a b
⊢ a ∈ minimals r s
[PROOFSTEP]
rwa [of_not_not fun hab => ht ha (h hb) hab hr]
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
inst✝ : PartialOrder α
hs : IsAntichain (fun x x_1 => x ≤ x_1) s
a : α
x✝ : a ∈ minimals (fun x x_1 => x ≤ x_1) ↑(upperClosure s)
b : α
hb : b ∈ s
hba : b ≤ a
right✝ : ∀ ⦃b : α⦄, b ∈ ↑(upperClosure s) → (fun x x_1 => x ≤ x_1) b a → (fun x x_1 => x ≤ x_1) a b
⊢ a ∈ s
[PROOFSTEP]
rwa [eq_of_mem_minimals ‹a ∈ _› (subset_upperClosure hb) hba]
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
inst✝ : PartialOrder α
hs : IsAntichain (fun x x_1 => x ≤ x_1) s
a : α
ha : a ∈ s
b : α
x✝ : b ∈ ↑(upperClosure s)
hba : (fun x x_1 => x ≤ x_1) b a
c : α
hc : c ∈ s
hcb : c ≤ b
⊢ (fun x x_1 => x ≤ x_1) a b
[PROOFSTEP]
rwa [hs.eq' ha hc (hcb.trans hba)]
[GOAL]
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f : α → β
r : α → α → Prop
s : β → β → Prop
x : Set α
hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
⊢ minimals s (f '' x) = f '' minimals r x
[PROOFSTEP]
ext a
[GOAL]
case h
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a✝ b : α
inst✝ : PartialOrder α
f : α → β
r : α → α → Prop
s : β → β → Prop
x : Set α
hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
a : β
⊢ a ∈ minimals s (f '' x) ↔ a ∈ f '' minimals r x
[PROOFSTEP]
simp only [minimals, mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
[GOAL]
case h
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a✝ b : α
inst✝ : PartialOrder α
f : α → β
r : α → α → Prop
s : β → β → Prop
x : Set α
hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
a : β
⊢ a ∈ {a | (∃ x_1, x_1 ∈ x ∧ f x_1 = a) ∧ ∀ (a_1 : α), a_1 ∈ x → s (f a_1) a → s a (f a_1)} ↔
    ∃ x_1, x_1 ∈ {a | a ∈ x ∧ ∀ ⦃b : α⦄, b ∈ x → r b a → r a b} ∧ f x_1 = a
[PROOFSTEP]
constructor
[GOAL]
case h.mp
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a✝ b : α
inst✝ : PartialOrder α
f : α → β
r : α → α → Prop
s : β → β → Prop
x : Set α
hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
a : β
⊢ a ∈ {a | (∃ x_1, x_1 ∈ x ∧ f x_1 = a) ∧ ∀ (a_1 : α), a_1 ∈ x → s (f a_1) a → s a (f a_1)} →
    ∃ x_1, x_1 ∈ {a | a ∈ x ∧ ∀ ⦃b : α⦄, b ∈ x → r b a → r a b} ∧ f x_1 = a
[PROOFSTEP]
rintro ⟨⟨a, ha, rfl⟩, h⟩
[GOAL]
case h.mp.intro.intro.intro
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a✝ b : α
inst✝ : PartialOrder α
f : α → β
r : α → α → Prop
s : β → β → Prop
x : Set α
hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
a : α
ha : a ∈ x
h : ∀ (a_1 : α), a_1 ∈ x → s (f a_1) (f a) → s (f a) (f a_1)
⊢ ∃ x_1, x_1 ∈ {a | a ∈ x ∧ ∀ ⦃b : α⦄, b ∈ x → r b a → r a b} ∧ f x_1 = f a
[PROOFSTEP]
exact ⟨a, ⟨ha, fun y hy hya ↦ (hf ha hy).mpr (h _ hy ((hf hy ha).mp hya))⟩, rfl⟩
[GOAL]
case h.mpr
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a✝ b : α
inst✝ : PartialOrder α
f : α → β
r : α → α → Prop
s : β → β → Prop
x : Set α
hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
a : β
⊢ (∃ x_1, x_1 ∈ {a | a ∈ x ∧ ∀ ⦃b : α⦄, b ∈ x → r b a → r a b} ∧ f x_1 = a) →
    a ∈ {a | (∃ x_1, x_1 ∈ x ∧ f x_1 = a) ∧ ∀ (a_2 : α), a_2 ∈ x → s (f a_2) a → s a (f a_2)}
[PROOFSTEP]
rintro ⟨a, ⟨⟨ha, h⟩, rfl⟩⟩
[GOAL]
case h.mpr.intro.intro.intro
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a✝ b : α
inst✝ : PartialOrder α
f : α → β
r : α → α → Prop
s : β → β → Prop
x : Set α
hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
a : α
ha : a ∈ x
h : ∀ ⦃b : α⦄, b ∈ x → r b a → r a b
⊢ f a ∈ {a | (∃ x_1, x_1 ∈ x ∧ f x_1 = a) ∧ ∀ (a_1 : α), a_1 ∈ x → s (f a_1) a → s a (f a_1)}
[PROOFSTEP]
exact ⟨⟨_, ha, rfl⟩, fun y hy hya ↦ (hf ha hy).mp (h hy ((hf hy ha).mpr hya))⟩
[GOAL]
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f✝ : α → β
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
x : Set α
⊢ minimals s (↑f '' x) = ↑f '' minimals r x
[PROOFSTEP]
rw [minimals_image_of_rel_iff_rel]
[GOAL]
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f✝ : α → β
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
x : Set α
⊢ ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (↑f a) (↑f a'))
[PROOFSTEP]
simp [f.map_rel_iff]
[GOAL]
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f : α → β
r : α → α → Prop
s : β → β → Prop
x : Set α
hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
y : Set β
⊢ x ∩ f ⁻¹' minimals s (f '' x ∩ y) = minimals r (x ∩ f ⁻¹' y)
[PROOFSTEP]
ext a
[GOAL]
case h
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a✝ b : α
inst✝ : PartialOrder α
f : α → β
r : α → α → Prop
s : β → β → Prop
x : Set α
hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
y : Set β
a : α
⊢ a ∈ x ∩ f ⁻¹' minimals s (f '' x ∩ y) ↔ a ∈ minimals r (x ∩ f ⁻¹' y)
[PROOFSTEP]
simp only [minimals, mem_inter_iff, mem_image, and_imp, forall_exists_index, forall_apply_eq_imp_iff₂,
  preimage_setOf_eq, mem_setOf_eq, mem_preimage]
[GOAL]
case h
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a✝ b : α
inst✝ : PartialOrder α
f : α → β
r : α → α → Prop
s : β → β → Prop
x : Set α
hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
y : Set β
a : α
⊢ (a ∈ x ∧
      ((∃ x_1, x_1 ∈ x ∧ f x_1 = f a) ∧ f a ∈ y) ∧
        ∀ (a_1 : α), a_1 ∈ x → f a_1 ∈ y → s (f a_1) (f a) → s (f a) (f a_1)) ↔
    (a ∈ x ∧ f a ∈ y) ∧ ∀ ⦃b : α⦄, b ∈ x → f b ∈ y → r b a → r a b
[PROOFSTEP]
exact
  ⟨fun ⟨hax, ⟨_, hay⟩, h2⟩ ↦
    ⟨⟨hax, hay⟩, fun a₁ ha₁ ha₁y ha₁a ↦ (hf hax ha₁).mpr (h2 _ ha₁ ha₁y ((hf ha₁ hax).mp ha₁a))⟩, fun ⟨⟨hax, hay⟩, h⟩ ↦
    ⟨hax, ⟨⟨_, hax, rfl⟩, hay⟩, fun a' ha' ha'y hsa' ↦ (hf hax ha').mp (h ha' ha'y ((hf ha' hax).mpr hsa'))⟩⟩
[GOAL]
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f : α → β
r : α → α → Prop
s : β → β → Prop
x : Set α
y : Set β
hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
hy : y ⊆ f '' x
⊢ x ∩ f ⁻¹' minimals s y = minimals r (x ∩ f ⁻¹' y)
[PROOFSTEP]
rw [← inter_eq_self_of_subset_right hy, inter_minimals_preimage_inter_eq_of_rel_iff_rel_on hf, preimage_inter, ←
  inter_assoc, inter_eq_self_of_subset_left (subset_preimage_image f x)]
[GOAL]
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f✝ : α → β
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
x : Set α
y : Set β
⊢ ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (↑f a) (↑f a'))
[PROOFSTEP]
simp [f.map_rel_iff]
[GOAL]
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f✝ : α → β
r : α → α → Prop
s : β → β → Prop
y : Set β
x : Set α
f : r ↪r s
h : y ⊆ ↑f '' x
⊢ x ∩ ↑f ⁻¹' minimals s y = minimals r (x ∩ ↑f ⁻¹' y)
[PROOFSTEP]
rw [inter_preimage_minimals_eq_of_rel_iff_rel_on_of_subset _ h]
[GOAL]
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f✝ : α → β
r : α → α → Prop
s : β → β → Prop
y : Set β
x : Set α
f : r ↪r s
h : y ⊆ ↑f '' x
⊢ ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (↑f a) (↑f a'))
[PROOFSTEP]
simp [f.map_rel_iff]
[GOAL]
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f✝ : α → β
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
y : Set β
⊢ minimals r (↑f ⁻¹' y) = ↑f ⁻¹' minimals s (y ∩ range ↑f)
[PROOFSTEP]
convert (f.inter_preimage_minimals_eq univ y).symm
[GOAL]
case h.e'_2.h.e'_3
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f✝ : α → β
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
y : Set β
⊢ ↑f ⁻¹' y = univ ∩ ↑f ⁻¹' y
case h.e'_3
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f✝ : α → β
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
y : Set β
⊢ ↑f ⁻¹' minimals s (y ∩ range ↑f) = univ ∩ ↑f ⁻¹' minimals s (↑f '' univ ∩ y)
[PROOFSTEP]
simp [univ_inter]
[GOAL]
case h.e'_3
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f✝ : α → β
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
y : Set β
⊢ ↑f ⁻¹' minimals s (y ∩ range ↑f) = univ ∩ ↑f ⁻¹' minimals s (↑f '' univ ∩ y)
[PROOFSTEP]
simp [inter_comm]
[GOAL]
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f : α → β
r : α → α → Prop
s : β → β → Prop
x : Set α
hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
y : Set β
⊢ x ∩ f ⁻¹' maximals s (f '' x ∩ y) = maximals r (x ∩ f ⁻¹' y)
[PROOFSTEP]
apply inter_minimals_preimage_inter_eq_of_rel_iff_rel_on
[GOAL]
case hf
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f : α → β
r : α → α → Prop
s : β → β → Prop
x : Set α
hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
y : Set β
⊢ ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a' a ↔ s (f a') (f a))
[PROOFSTEP]
exact fun _ _ a b ↦ hf b a
[GOAL]
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f : α → β
r : α → α → Prop
s : β → β → Prop
x : Set α
y : Set β
hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
hy : y ⊆ f '' x
⊢ x ∩ f ⁻¹' maximals s y = maximals r (x ∩ f ⁻¹' y)
[PROOFSTEP]
apply inter_preimage_minimals_eq_of_rel_iff_rel_on_of_subset _ hy
[GOAL]
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f : α → β
r : α → α → Prop
s : β → β → Prop
x : Set α
y : Set β
hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
hy : y ⊆ f '' x
⊢ ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a' a ↔ s (f a') (f a))
[PROOFSTEP]
exact fun _ _ a b ↦ hf b a
[GOAL]
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f✝ : α → β
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
x : Set α
y : Set β
⊢ ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a' a ↔ s (↑f a') (↑f a))
[PROOFSTEP]
simp [f.map_rel_iff]
[GOAL]
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f✝ : α → β
r : α → α → Prop
s : β → β → Prop
y : Set β
x : Set α
f : r ↪r s
h : y ⊆ ↑f '' x
⊢ x ∩ ↑f ⁻¹' maximals s y = maximals r (x ∩ ↑f ⁻¹' y)
[PROOFSTEP]
rw [inter_preimage_maximals_eq_of_rel_iff_rel_on_of_subset _ h]
[GOAL]
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f✝ : α → β
r : α → α → Prop
s : β → β → Prop
y : Set β
x : Set α
f : r ↪r s
h : y ⊆ ↑f '' x
⊢ ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (↑f a) (↑f a'))
[PROOFSTEP]
simp [f.map_rel_iff]
[GOAL]
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f✝ : α → β
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
y : Set β
⊢ maximals r (↑f ⁻¹' y) = ↑f ⁻¹' maximals s (y ∩ range ↑f)
[PROOFSTEP]
convert (f.inter_preimage_maximals_eq univ y).symm
[GOAL]
case h.e'_2.h.e'_3
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f✝ : α → β
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
y : Set β
⊢ ↑f ⁻¹' y = univ ∩ ↑f ⁻¹' y
case h.e'_3
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f✝ : α → β
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
y : Set β
⊢ ↑f ⁻¹' maximals s (y ∩ range ↑f) = univ ∩ ↑f ⁻¹' maximals s (↑f '' univ ∩ y)
[PROOFSTEP]
simp [univ_inter]
[GOAL]
case h.e'_3
β : Type u_2
α : Type u_1
r✝ r₁ r₂ : α → α → Prop
s✝ t : Set α
a b : α
inst✝ : PartialOrder α
f✝ : α → β
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
y : Set β
⊢ ↑f ⁻¹' maximals s (y ∩ range ↑f) = univ ∩ ↑f ⁻¹' maximals s (↑f '' univ ∩ y)
[PROOFSTEP]
simp [inter_comm]
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
inst✝¹ inst✝ : PartialOrder α
a b : α
hab : a ≤ b
⊢ minimals (fun x x_1 => x ≤ x_1) (Icc a b) = {a}
[PROOFSTEP]
simp_rw [Icc, and_comm (a := (a ≤ _))]
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
inst✝¹ inst✝ : PartialOrder α
a b : α
hab : a ≤ b
⊢ minimals (fun x x_1 => x ≤ x_1) {x | x ≤ b ∧ a ≤ x} = {a}
[PROOFSTEP]
exact maximals_Icc (α := αᵒᵈ) hab
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
inst✝¹ inst✝ : PartialOrder α
a b : α
hab : a < b
⊢ minimals (fun x x_1 => x ≤ x_1) (Ico a b) = {a}
[PROOFSTEP]
simp_rw [Ico, and_comm (a := _ ≤ _)]
[GOAL]
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
inst✝¹ inst✝ : PartialOrder α
a b : α
hab : a < b
⊢ minimals (fun x x_1 => x ≤ x_1) {x | x < b ∧ a ≤ x} = {a}
[PROOFSTEP]
exact maximals_Ioc (α := αᵒᵈ) hab


[GOAL]
p q : Prop
⊢ p ≤ q ∨ q ≤ p
[PROOFSTEP]
by_cases h : q
[GOAL]
case pos
p q : Prop
h : q
⊢ p ≤ q ∨ q ≤ p
[PROOFSTEP]
simp [h]
[GOAL]
case neg
p q : Prop
h : ¬q
⊢ p ≤ q ∨ q ≤ p
[PROOFSTEP]
simp [h]
[GOAL]
⊢ LinearOrder Prop
[PROOFSTEP]
classical exact Lattice.toLinearOrder Prop
[GOAL]
⊢ LinearOrder Prop
[PROOFSTEP]
exact Lattice.toLinearOrder Prop
[GOAL]
ι : Type u_1
α' : ι → Type u_2
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ Disjoint f g ↔ ∀ (i : ι), Disjoint (f i) (g i)
[PROOFSTEP]
classical
constructor
· intro h i x hf hg
  refine' (update_le_iff.mp <| h (update_le_iff.mpr ⟨hf, fun _ _ => _⟩) (update_le_iff.mpr ⟨hg, fun _ _ => _⟩)).1
  · exact bot_le
  · exact bot_le
· intro h x hf hg i
  apply h i (hf i) (hg i)
[GOAL]
ι : Type u_1
α' : ι → Type u_2
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ Disjoint f g ↔ ∀ (i : ι), Disjoint (f i) (g i)
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
α' : ι → Type u_2
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ Disjoint f g → ∀ (i : ι), Disjoint (f i) (g i)
[PROOFSTEP]
intro h i x hf hg
[GOAL]
case mp
ι : Type u_1
α' : ι → Type u_2
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : Disjoint f g
i : ι
x : α' i
hf : x ≤ f i
hg : x ≤ g i
⊢ x ≤ ⊥
[PROOFSTEP]
refine' (update_le_iff.mp <| h (update_le_iff.mpr ⟨hf, fun _ _ => _⟩) (update_le_iff.mpr ⟨hg, fun _ _ => _⟩)).1
[GOAL]
case mp.refine'_1
ι : Type u_1
α' : ι → Type u_2
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : Disjoint f g
i : ι
x : α' i
hf : x ≤ f i
hg : x ≤ g i
x✝¹ : ι
x✝ : x✝¹ ≠ i
⊢ ?mp.refine'_2 x✝¹ ≤ f x✝¹
[PROOFSTEP]
exact bot_le
[GOAL]
case mp.refine'_3
ι : Type u_1
α' : ι → Type u_2
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : Disjoint f g
i : ι
x : α' i
hf : x ≤ f i
hg : x ≤ g i
x✝¹ : ι
x✝ : x✝¹ ≠ i
⊢ ⊥ ≤ g x✝¹
[PROOFSTEP]
exact bot_le
[GOAL]
case mpr
ι : Type u_1
α' : ι → Type u_2
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ (∀ (i : ι), Disjoint (f i) (g i)) → Disjoint f g
[PROOFSTEP]
intro h x hf hg i
[GOAL]
case mpr
ι : Type u_1
α' : ι → Type u_2
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : ∀ (i : ι), Disjoint (f i) (g i)
x : (i : ι) → α' i
hf : x ≤ f
hg : x ≤ g
i : ι
⊢ x i ≤ ⊥ i
[PROOFSTEP]
apply h i (hf i) (hg i)
[GOAL]
ι : Type u_1
α' : ι → Type u_2
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → BoundedOrder (α' i)
f g : (i : ι) → α' i
⊢ IsCompl f g ↔ ∀ (i : ι), IsCompl (f i) (g i)
[PROOFSTEP]
simp_rw [_root_.isCompl_iff, disjoint_iff, codisjoint_iff, forall_and]
[GOAL]
P Q : Prop
⊢ IsCompl P Q ↔ ¬(P ↔ Q)
[PROOFSTEP]
rw [_root_.isCompl_iff, Prop.disjoint_iff, Prop.codisjoint_iff, not_iff]
[GOAL]
P Q : Prop
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
[PROOFSTEP]
by_cases P
[GOAL]
P Q : Prop
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
[PROOFSTEP]
by_cases P
[GOAL]
case pos
P Q : Prop
h : P
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
[PROOFSTEP]
by_cases Q
[GOAL]
case pos
P Q : Prop
h : P
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
[PROOFSTEP]
by_cases Q
[GOAL]
case neg
P Q : Prop
h : ¬P
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
[PROOFSTEP]
by_cases Q
[GOAL]
case neg
P Q : Prop
h : ¬P
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
[PROOFSTEP]
by_cases Q
[GOAL]
case pos
P Q : Prop
h✝ : P
h : Q
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
[PROOFSTEP]
simp [*]
[GOAL]
case neg
P Q : Prop
h✝ : P
h : ¬Q
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
[PROOFSTEP]
simp [*]
[GOAL]
case pos
P Q : Prop
h✝ : ¬P
h : Q
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
[PROOFSTEP]
simp [*]
[GOAL]
case neg
P Q : Prop
h✝ : ¬P
h : ¬Q
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
[PROOFSTEP]
simp [*]