case pos
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : A = B
⊢ A < B ∨ A = B ∨ B < A

case neg
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
⊢ A < B ∨ A = B ∨ B < A
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
⊢ A < B ∨ A = B ∨ B < A
by_cases h₁ : A = B
case neg
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
⊢ A < B ∨ A = B ∨ B < A
case neg
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
⊢ A < B ∨ A = B ∨ B < A
have h : Finset.Nonempty (A \ B ∪ B \ A) := by
  rw [nonempty_iff_ne_empty]
  intro a
  simp only [union_eq_empty_iff, sdiff_eq_empty_iff_subset] at a
  apply h₁ (Subset.antisymm a.1 a.2)
case neg.intro.intro
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
hk : k ∈ A \ B ∪ B \ A
z : ∀ (x' : α), x' ∈ A \ B ∪ B \ A → id x' ≤ id k
⊢ A < B ∨ A = B ∨ B < A
case neg
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
⊢ A < B ∨ A = B ∨ B < A
rcases exists_max_image (A \ B ∪ B \ A) id h with ⟨k, ⟨hk, z⟩⟩
no goals
case pos
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : A = B
⊢ A < B ∨ A = B ∨ B < A
tauto
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
⊢ A \ B ∪ B \ A ≠ ∅
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
⊢ Finset.Nonempty (A \ B ∪ B \ A)
rw [nonempty_iff_ne_empty]
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
a : A \ B ∪ B \ A = ∅
⊢ False
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
⊢ A \ B ∪ B \ A ≠ ∅
intro a
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
a : A ⊆ B ∧ B ⊆ A
⊢ False
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
a : A \ B ∪ B \ A = ∅
⊢ False
simp only [union_eq_empty_iff, sdiff_eq_empty_iff_subset] at a
no goals
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
a : A ⊆ B ∧ B ⊆ A
⊢ False
apply h₁ (Subset.antisymm a.1 a.2)
case neg.intro.intro
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
z : ∀ (x' : α), x' ∈ A \ B ∪ B \ A → id x' ≤ id k
hk : k ∈ A ∧ ¬k ∈ B ∨ k ∈ B ∧ ¬k ∈ A
⊢ A < B ∨ A = B ∨ B < A
case neg.intro.intro
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
hk : k ∈ A \ B ∪ B \ A
z : ∀ (x' : α), x' ∈ A \ B ∪ B \ A → id x' ≤ id k
⊢ A < B ∨ A = B ∨ B < A
simp only [mem_union, mem_sdiff] at hk
case neg.intro.intro.inl
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
z : ∀ (x' : α), x' ∈ A \ B ∪ B \ A → id x' ≤ id k
hk : k ∈ A ∧ ¬k ∈ B
⊢ A < B ∨ A = B ∨ B < A

case neg.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
z : ∀ (x' : α), x' ∈ A \ B ∪ B \ A → id x' ≤ id k
hk : k ∈ B ∧ ¬k ∈ A
⊢ A < B ∨ A = B ∨ B < A
case neg.intro.intro
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
z : ∀ (x' : α), x' ∈ A \ B ∪ B \ A → id x' ≤ id k
hk : k ∈ A ∧ ¬k ∈ B ∨ k ∈ B ∧ ¬k ∈ A
⊢ A < B ∨ A = B ∨ B < A
cases' hk with hk hk
case neg.intro.intro.inl.h
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
z : ∀ (x' : α), x' ∈ A \ B ∪ B \ A → id x' ≤ id k
hk : k ∈ A ∧ ¬k ∈ B
⊢ A = B ∨ B < A
case neg.intro.intro.inl
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
z : ∀ (x' : α), x' ∈ A \ B ∪ B \ A → id x' ≤ id k
hk : k ∈ A ∧ ¬k ∈ B
⊢ A < B ∨ A = B ∨ B < A
right
case neg.intro.intro.inl.h.h
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
z : ∀ (x' : α), x' ∈ A \ B ∪ B \ A → id x' ≤ id k
hk : k ∈ A ∧ ¬k ∈ B
⊢ B < A
case neg.intro.intro.inl.h
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
z : ∀ (x' : α), x' ∈ A \ B ∪ B \ A → id x' ≤ id k
hk : k ∈ A ∧ ¬k ∈ B
⊢ A = B ∨ B < A
right
case neg.intro.intro.inl.h.h
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
z : ∀ (x' : α), x' ∈ A \ B ∪ B \ A → id x' ≤ id k
hk : k ∈ A ∧ ¬k ∈ B
t : α
th : k < t
⊢ t ∈ B ↔ t ∈ A
case neg.intro.intro.inl.h.h
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
z : ∀ (x' : α), x' ∈ A \ B ∪ B \ A → id x' ≤ id k
hk : k ∈ A ∧ ¬k ∈ B
⊢ B < A
refine' ⟨k, @fun t th => _, hk.2, hk.1⟩
case neg.intro.intro.inl.h.h
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
hk : k ∈ A ∧ ¬k ∈ B
t : α
th : k < t
z : t ∈ A \ B ∪ B \ A → id t ≤ id k
⊢ t ∈ B ↔ t ∈ A
case neg.intro.intro.inl.h.h
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
z : ∀ (x' : α), x' ∈ A \ B ∪ B \ A → id x' ≤ id k
hk : k ∈ A ∧ ¬k ∈ B
t : α
th : k < t
⊢ t ∈ B ↔ t ∈ A
specialize z t
case neg.intro.intro.inl.h.h
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
hk : k ∈ A ∧ ¬k ∈ B
t : α
th : k < t
z : t ∈ A \ B ∪ B \ A → id t ≤ id k
h₂ : ¬(t ∈ B ↔ t ∈ A)
⊢ False
case neg.intro.intro.inl.h.h
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
hk : k ∈ A ∧ ¬k ∈ B
t : α
th : k < t
z : t ∈ A \ B ∪ B \ A → id t ≤ id k
⊢ t ∈ B ↔ t ∈ A
by_contra h₂
case neg.intro.intro.inl.h.h
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
hk : k ∈ A ∧ ¬k ∈ B
t : α
th : k < t
h₂ : ¬(t ∈ B ↔ t ∈ A)
z : t ∈ A ∧ ¬t ∈ B ∨ t ∈ B ∧ ¬t ∈ A → t ≤ k
⊢ False
case neg.intro.intro.inl.h.h
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
hk : k ∈ A ∧ ¬k ∈ B
t : α
th : k < t
z : t ∈ A \ B ∪ B \ A → id t ≤ id k
h₂ : ¬(t ∈ B ↔ t ∈ A)
⊢ False
simp only [mem_union, mem_sdiff, id.def] at z
case neg.intro.intro.inl.h.h
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
hk : k ∈ A ∧ ¬k ∈ B
t : α
th : k < t
h₂ : t ∈ A ∧ ¬t ∈ B ∨ t ∈ B ∧ ¬t ∈ A
z : t ∈ A ∧ ¬t ∈ B ∨ t ∈ B ∧ ¬t ∈ A → t ≤ k
⊢ False
case neg.intro.intro.inl.h.h
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
hk : k ∈ A ∧ ¬k ∈ B
t : α
th : k < t
h₂ : ¬(t ∈ B ↔ t ∈ A)
z : t ∈ A ∧ ¬t ∈ B ∨ t ∈ B ∧ ¬t ∈ A → t ≤ k
⊢ False
rw [not_iff, iff_iff_and_or_not_and_not, not_not, and_comm] at h₂
no goals
case neg.intro.intro.inl.h.h
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
hk : k ∈ A ∧ ¬k ∈ B
t : α
th : k < t
h₂ : t ∈ A ∧ ¬t ∈ B ∨ t ∈ B ∧ ¬t ∈ A
z : t ∈ A ∧ ¬t ∈ B ∨ t ∈ B ∧ ¬t ∈ A → t ≤ k
⊢ False
apply not_le_of_lt th (z h₂)
case neg.intro.intro.inr.h
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
z : ∀ (x' : α), x' ∈ A \ B ∪ B \ A → id x' ≤ id k
hk : k ∈ B ∧ ¬k ∈ A
⊢ A < B
case neg.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
z : ∀ (x' : α), x' ∈ A \ B ∪ B \ A → id x' ≤ id k
hk : k ∈ B ∧ ¬k ∈ A
⊢ A < B ∨ A = B ∨ B < A
left
case neg.intro.intro.inr.h
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
z : ∀ (x' : α), x' ∈ A \ B ∪ B \ A → id x' ≤ id k
hk : k ∈ B ∧ ¬k ∈ A
t : α
th : k < t
⊢ t ∈ A ↔ t ∈ B
case neg.intro.intro.inr.h
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
z : ∀ (x' : α), x' ∈ A \ B ∪ B \ A → id x' ≤ id k
hk : k ∈ B ∧ ¬k ∈ A
⊢ A < B
refine' ⟨k, @fun t th => _, hk.2, hk.1⟩
case neg.intro.intro.inr.h
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
hk : k ∈ B ∧ ¬k ∈ A
t : α
th : k < t
z : t ∈ A \ B ∪ B \ A → id t ≤ id k
⊢ t ∈ A ↔ t ∈ B
case neg.intro.intro.inr.h
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
z : ∀ (x' : α), x' ∈ A \ B ∪ B \ A → id x' ≤ id k
hk : k ∈ B ∧ ¬k ∈ A
t : α
th : k < t
⊢ t ∈ A ↔ t ∈ B
specialize z t
case neg.intro.intro.inr.h
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
hk : k ∈ B ∧ ¬k ∈ A
t : α
th : k < t
z : t ∈ A \ B ∪ B \ A → id t ≤ id k
h₃ : ¬(t ∈ A ↔ t ∈ B)
⊢ False
case neg.intro.intro.inr.h
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
hk : k ∈ B ∧ ¬k ∈ A
t : α
th : k < t
z : t ∈ A \ B ∪ B \ A → id t ≤ id k
⊢ t ∈ A ↔ t ∈ B
by_contra h₃
case neg.intro.intro.inr.h
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
hk : k ∈ B ∧ ¬k ∈ A
t : α
th : k < t
h₃ : ¬(t ∈ A ↔ t ∈ B)
z : t ∈ A ∧ ¬t ∈ B ∨ t ∈ B ∧ ¬t ∈ A → t ≤ k
⊢ False
case neg.intro.intro.inr.h
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
hk : k ∈ B ∧ ¬k ∈ A
t : α
th : k < t
z : t ∈ A \ B ∪ B \ A → id t ≤ id k
h₃ : ¬(t ∈ A ↔ t ∈ B)
⊢ False
simp only [mem_union, mem_sdiff, id.def] at z
case neg.intro.intro.inr.h
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
hk : k ∈ B ∧ ¬k ∈ A
t : α
th : k < t
h₃ : t ∈ A ∧ ¬t ∈ B ∨ t ∈ B ∧ ¬t ∈ A
z : t ∈ A ∧ ¬t ∈ B ∨ t ∈ B ∧ ¬t ∈ A → t ≤ k
⊢ False
case neg.intro.intro.inr.h
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
hk : k ∈ B ∧ ¬k ∈ A
t : α
th : k < t
h₃ : ¬(t ∈ A ↔ t ∈ B)
z : t ∈ A ∧ ¬t ∈ B ∨ t ∈ B ∧ ¬t ∈ A → t ≤ k
⊢ False
rw [not_iff, iff_iff_and_or_not_and_not, not_not, and_comm, or_comm] at h₃
no goals
case neg.intro.intro.inr.h
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
h : Finset.Nonempty (A \ B ∪ B \ A)
k : α
hk : k ∈ B ∧ ¬k ∈ A
t : α
th : k < t
h₃ : t ∈ A ∧ ¬t ∈ B ∨ t ∈ B ∧ ¬t ∈ A
z : t ∈ A ∧ ¬t ∈ B ∨ t ∈ B ∧ ¬t ∈ A → t ≤ k
⊢ False
apply not_le_of_lt th (z h₃)