α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
⊢ ∃ s x, r ≤ s
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
⊢ ∃ s x, r ≤ s
let S := { s | IsPartialOrder α s }
case intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
⊢ ∃ s x, r ≤ s
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
⊢ ∃ s x, r ≤ s
obtain ⟨s, hs₁ : IsPartialOrder _ _, rs, hs₂⟩ := zorn_nonempty_partialOrder₀ S hS r ‹_›
case intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
⊢ ∃ s x, r ≤ s
case intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
⊢ ∃ s x, r ≤ s
haveI : IsPartialOrder α s := hs₁
case intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
⊢ ∀ (a b : α), s a b ∨ s b a
case intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
⊢ ∃ s x, r ≤ s
refine ⟨s, { total := ?_, refl := hs₁.refl, trans := hs₁.trans, antisymm := hs₁.antisymm } , rs⟩
case intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
⊢ s x y ∨ s y x
case intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
⊢ ∀ (a b : α), s a b ∨ s b a
intro x y
case intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
⊢ False
case intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
⊢ s x y ∨ s y x
by_contra' h
case intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
⊢ False
case intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
⊢ False
let s' x' y' := s x' y' ∨ s x' x ∧ s y y'
case intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
h : ¬s' x y ∧ ¬s' y x
⊢ False

α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
⊢ s' ∈ S
case intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
⊢ False
rw [← hs₂ s' _ fun _ _ ↦ Or.inl] at h
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
⊢ ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
⊢ ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
rintro c hc₁ hc₂ s hs
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
⊢ ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
⊢ ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
haveI := (hc₁ hs).1
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
⊢ sSup c ∈ S
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
⊢ ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
refine' ⟨sSup c, _, fun z hz => le_sSup hz⟩
case refine'_1
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
⊢ ∀ (a : α), ∃ r, r ∈ c ∧ r a a

case refine'_2
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
⊢ ∀ (a b c_1 : α), (∃ r, r ∈ c ∧ r a b) → (∃ r, r ∈ c ∧ r b c_1) → ∃ r, r ∈ c ∧ r a c_1

case refine'_3
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
⊢ ∀ (a b : α), (∃ r, r ∈ c ∧ r a b) → (∃ r, r ∈ c ∧ r b a) → a = b
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
⊢ sSup c ∈ S
refine'
    { refl := _
      trans := _
      antisymm := _ } <;>
  simp_rw [binary_relation_sSup_iff]
case refine'_1
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
x : α
⊢ ∃ r, r ∈ c ∧ r x x
case refine'_1
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
⊢ ∀ (a : α), ∃ r, r ∈ c ∧ r a a
intro x
no goals
case refine'_1
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
x : α
⊢ ∃ r, r ∈ c ∧ r x x
exact ⟨s, hs, refl x⟩
case refine'_2.intro.intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
x y z : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y z
⊢ ∃ r, r ∈ c ∧ r x z
case refine'_2
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
⊢ ∀ (a b c_1 : α), (∃ r, r ∈ c ∧ r a b) → (∃ r, r ∈ c ∧ r b c_1) → ∃ r, r ∈ c ∧ r a c_1
rintro x y z ⟨s₁, h₁s₁, h₂s₁⟩ ⟨s₂, h₁s₂, h₂s₂⟩
case refine'_2.intro.intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this✝ : IsPreorder α s
x y z : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y z
this : IsPartialOrder α s₁
⊢ ∃ r, r ∈ c ∧ r x z
case refine'_2.intro.intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
x y z : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y z
⊢ ∃ r, r ∈ c ∧ r x z
haveI : IsPartialOrder _ _ := hc₁ h₁s₁
case refine'_2.intro.intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this✝¹ : IsPreorder α s
x y z : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y z
this✝ : IsPartialOrder α s₁
this : IsPartialOrder α s₂
⊢ ∃ r, r ∈ c ∧ r x z
case refine'_2.intro.intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this✝ : IsPreorder α s
x y z : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y z
this : IsPartialOrder α s₁
⊢ ∃ r, r ∈ c ∧ r x z
haveI : IsPartialOrder _ _ := hc₁ h₁s₂
case refine'_2.intro.intro.intro.intro.inl
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this✝¹ : IsPreorder α s
x y z : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y z
this✝ : IsPartialOrder α s₁
this : IsPartialOrder α s₂
h : s₁ ≤ s₂
⊢ ∃ r, r ∈ c ∧ r x z

case refine'_2.intro.intro.intro.intro.inr
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this✝¹ : IsPreorder α s
x y z : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y z
this✝ : IsPartialOrder α s₁
this : IsPartialOrder α s₂
h : s₂ ≤ s₁
⊢ ∃ r, r ∈ c ∧ r x z
case refine'_2.intro.intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this✝¹ : IsPreorder α s
x y z : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y z
this✝ : IsPartialOrder α s₁
this : IsPartialOrder α s₂
⊢ ∃ r, r ∈ c ∧ r x z
cases' hc₂.total h₁s₁ h₁s₂ with h h
no goals
case refine'_2.intro.intro.intro.intro.inl
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this✝¹ : IsPreorder α s
x y z : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y z
this✝ : IsPartialOrder α s₁
this : IsPartialOrder α s₂
h : s₁ ≤ s₂
⊢ ∃ r, r ∈ c ∧ r x z
exact ⟨s₂, h₁s₂, _root_.trans (h _ _ h₂s₁) h₂s₂⟩
no goals
case refine'_2.intro.intro.intro.intro.inr
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this✝¹ : IsPreorder α s
x y z : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y z
this✝ : IsPartialOrder α s₁
this : IsPartialOrder α s₂
h : s₂ ≤ s₁
⊢ ∃ r, r ∈ c ∧ r x z
exact ⟨s₁, h₁s₁, _root_.trans h₂s₁ (h _ _ h₂s₂)⟩
case refine'_3.intro.intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
x y : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y x
⊢ x = y
case refine'_3
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
⊢ ∀ (a b : α), (∃ r, r ∈ c ∧ r a b) → (∃ r, r ∈ c ∧ r b a) → a = b
rintro x y ⟨s₁, h₁s₁, h₂s₁⟩ ⟨s₂, h₁s₂, h₂s₂⟩
case refine'_3.intro.intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this✝ : IsPreorder α s
x y : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y x
this : IsPartialOrder α s₁
⊢ x = y
case refine'_3.intro.intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
x y : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y x
⊢ x = y
haveI : IsPartialOrder _ _ := hc₁ h₁s₁
case refine'_3.intro.intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this✝¹ : IsPreorder α s
x y : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y x
this✝ : IsPartialOrder α s₁
this : IsPartialOrder α s₂
⊢ x = y
case refine'_3.intro.intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this✝ : IsPreorder α s
x y : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y x
this : IsPartialOrder α s₁
⊢ x = y
haveI : IsPartialOrder _ _ := hc₁ h₁s₂
case refine'_3.intro.intro.intro.intro.inl
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this✝¹ : IsPreorder α s
x y : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y x
this✝ : IsPartialOrder α s₁
this : IsPartialOrder α s₂
h : s₁ ≤ s₂
⊢ x = y

case refine'_3.intro.intro.intro.intro.inr
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this✝¹ : IsPreorder α s
x y : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y x
this✝ : IsPartialOrder α s₁
this : IsPartialOrder α s₂
h : s₂ ≤ s₁
⊢ x = y
case refine'_3.intro.intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this✝¹ : IsPreorder α s
x y : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y x
this✝ : IsPartialOrder α s₁
this : IsPartialOrder α s₂
⊢ x = y
cases' hc₂.total h₁s₁ h₁s₂ with h h
no goals
case refine'_3.intro.intro.intro.intro.inl
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this✝¹ : IsPreorder α s
x y : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y x
this✝ : IsPartialOrder α s₁
this : IsPartialOrder α s₂
h : s₁ ≤ s₂
⊢ x = y
exact antisymm (h _ _ h₂s₁) h₂s₂
no goals
case refine'_3.intro.intro.intro.intro.inr
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x x_1 => x ≤ x_1) c
s : α → α → Prop
hs : s ∈ c
this✝¹ : IsPreorder α s
x y : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y x
this✝ : IsPartialOrder α s₁
this : IsPartialOrder α s₂
h : s₂ ≤ s₁
⊢ x = y
apply antisymm h₂s₁ (h _ _ h₂s₂)
no goals
case intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
h : ¬s' x y ∧ ¬s' y x
⊢ False
apply h.1 (Or.inr ⟨refl _, refl _⟩)
case refine'_1
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
⊢ ∀ (a b c : α), s' a b → s' b c → s' a c

case refine'_2
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
⊢ ∀ (a b : α), s' a b → s' b a → a = b
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
⊢ s' ∈ S
refine'
{ refl := fun x ↦ Or.inl (refl _)
  trans := _
  antisymm := _ }
case refine'_1.inl.inl
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
a b c : α
ab : s a b
bc : s b c
⊢ s' a c

case refine'_1.inl.inr.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
a b c : α
ab : s a b
bx : s b x
yc : s y c
⊢ s' a c

case refine'_1.inr.intro.inl
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
a b c : α
ax : s a x
yb : s y b
bc : s b c
⊢ s' a c

case refine'_1.inr.intro.inr.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
a b c : α
ax : s a x
yb : s y b
bx : s b x
yc : s y c
⊢ s' a c

case refine'_2
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
⊢ ∀ (a b : α), s' a b → s' b a → a = b
case refine'_1
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
⊢ ∀ (a b c : α), s' a b → s' b c → s' a c

case refine'_2
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
⊢ ∀ (a b : α), s' a b → s' b a → a = b
rintro a b c (ab | ⟨ax : s a x, yb : s y b⟩) (bc | ⟨bx : s b x, yc : s y c⟩)
case refine'_2.inl.inl
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
a b : α
ab : s a b
ba : s b a
⊢ a = b

case refine'_2.inl.inr.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
a b : α
ab : s a b
bx : s b x
ya : s y a
⊢ a = b

case refine'_2.inr.intro.inl
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
a b : α
ax : s a x
yb : s y b
ba : s b a
⊢ a = b

case refine'_2.inr.intro.inr.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
a b : α
ax : s a x
yb : s y b
bx : s b x
ya : s y a
⊢ a = b
case refine'_2
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
⊢ ∀ (a b : α), s' a b → s' b a → a = b
rintro a b (ab | ⟨ax : s a x, yb : s y b⟩) (ba | ⟨bx : s b x, ya : s y a⟩)
no goals
case refine'_1.inl.inl
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
a b c : α
ab : s a b
bc : s b c
⊢ s' a c
exact Or.inl (_root_.trans ab bc)
no goals
case refine'_1.inl.inr.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
a b c : α
ab : s a b
bx : s b x
yc : s y c
⊢ s' a c
exact Or.inr ⟨_root_.trans ab bx, yc⟩
no goals
case refine'_1.inr.intro.inl
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
a b c : α
ax : s a x
yb : s y b
bc : s b c
⊢ s' a c
exact Or.inr ⟨ax, _root_.trans yb bc⟩
no goals
case refine'_1.inr.intro.inr.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
a b c : α
ax : s a x
yb : s y b
bx : s b x
yc : s y c
⊢ s' a c
exact Or.inr ⟨ax, yc⟩
no goals
case refine'_2.inl.inl
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
a b : α
ab : s a b
ba : s b a
⊢ a = b
exact antisymm ab ba
no goals
case refine'_2.inl.inr.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
a b : α
ab : s a b
bx : s b x
ya : s y a
⊢ a = b
exact (h.2 (_root_.trans ya (_root_.trans ab bx))).elim
no goals
case refine'_2.inr.intro.inl
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
a b : α
ax : s a x
yb : s y b
ba : s b a
⊢ a = b
exact (h.2 (_root_.trans yb (_root_.trans ba ax))).elim
no goals
case refine'_2.inr.intro.inr.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS :
  ∀ (c : Set (α → α → Prop)),
    c ⊆ S →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : α → α → Prop), y ∈ c → ∃ ub, ub ∈ S ∧ ∀ (z : α → α → Prop), z ∈ c → z ≤ ub
s : α → α → Prop
hs₁ : IsPartialOrder α s
rs : r ≤ s
hs₂ : ∀ (z : α → α → Prop), z ∈ S → s ≤ z → z = s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
a b : α
ax : s a x
yb : s y b
bx : s b x
ya : s y a
⊢ a = b
exact (h.2 (_root_.trans yb bx)).elim