α : Type u_1
inst✝¹ : LT α
inst✝ : DecidableEq α
A B : Finset α
⊢ (∃ k, (∀ {x : α}, k < x → (x ∈ A \ B ↔ x ∈ B \ A)) ∧ ¬k ∈ A \ B ∧ k ∈ B \ A) ↔
    ∃ k, (∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)) ∧ ¬k ∈ A ∧ k ∈ B
α : Type u_1
inst✝¹ : LT α
inst✝ : DecidableEq α
A B : Finset α
⊢ toColex (A \ B) < toColex (B \ A) ↔ toColex A < toColex B
rw [Colex.lt_def, Colex.lt_def]
case h
α : Type u_1
inst✝¹ : LT α
inst✝ : DecidableEq α
A B : Finset α
⊢ ∀ (a : α),
    (∀ {x : α}, a < x → (x ∈ A \ B ↔ x ∈ B \ A)) ∧ ¬a ∈ A \ B ∧ a ∈ B \ A ↔
      (∀ {x : α}, a < x → (x ∈ A ↔ x ∈ B)) ∧ ¬a ∈ A ∧ a ∈ B
α : Type u_1
inst✝¹ : LT α
inst✝ : DecidableEq α
A B : Finset α
⊢ (∃ k, (∀ {x : α}, k < x → (x ∈ A \ B ↔ x ∈ B \ A)) ∧ ¬k ∈ A \ B ∧ k ∈ B \ A) ↔
    ∃ k, (∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)) ∧ ¬k ∈ A ∧ k ∈ B
apply exists_congr
case h
α : Type u_1
inst✝¹ : LT α
inst✝ : DecidableEq α
A B : Finset α
k : α
⊢ (∀ {x : α}, k < x → (x ∈ A \ B ↔ x ∈ B \ A)) ∧ ¬k ∈ A \ B ∧ k ∈ B \ A ↔
    (∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)) ∧ ¬k ∈ A ∧ k ∈ B
case h
α : Type u_1
inst✝¹ : LT α
inst✝ : DecidableEq α
A B : Finset α
⊢ ∀ (a : α),
    (∀ {x : α}, a < x → (x ∈ A \ B ↔ x ∈ B \ A)) ∧ ¬a ∈ A \ B ∧ a ∈ B \ A ↔
      (∀ {x : α}, a < x → (x ∈ A ↔ x ∈ B)) ∧ ¬a ∈ A ∧ a ∈ B
intro k
case h
α : Type u_1
inst✝¹ : LT α
inst✝ : DecidableEq α
A B : Finset α
k : α
⊢ (∀ {x : α}, k < x → (x ∈ A ∧ ¬x ∈ B ↔ x ∈ B ∧ ¬x ∈ A)) ∧ (k ∈ A → k ∈ B) ∧ k ∈ B ∧ ¬k ∈ A ↔
    (∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)) ∧ ¬k ∈ A ∧ k ∈ B
case h
α : Type u_1
inst✝¹ : LT α
inst✝ : DecidableEq α
A B : Finset α
k : α
⊢ (∀ {x : α}, k < x → (x ∈ A \ B ↔ x ∈ B \ A)) ∧ ¬k ∈ A \ B ∧ k ∈ B \ A ↔
    (∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)) ∧ ¬k ∈ A ∧ k ∈ B
simp only [mem_sdiff, not_and, not_not]
case h.mp
α : Type u_1
inst✝¹ : LT α
inst✝ : DecidableEq α
A B : Finset α
k : α
⊢ (∀ {x : α}, k < x → (x ∈ A ∧ ¬x ∈ B ↔ x ∈ B ∧ ¬x ∈ A)) ∧ (k ∈ A → k ∈ B) ∧ k ∈ B ∧ ¬k ∈ A →
    (∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)) ∧ ¬k ∈ A ∧ k ∈ B

case h.mpr
α : Type u_1
inst✝¹ : LT α
inst✝ : DecidableEq α
A B : Finset α
k : α
⊢ (∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)) ∧ ¬k ∈ A ∧ k ∈ B →
    (∀ {x : α}, k < x → (x ∈ A ∧ ¬x ∈ B ↔ x ∈ B ∧ ¬x ∈ A)) ∧ (k ∈ A → k ∈ B) ∧ k ∈ B ∧ ¬k ∈ A
case h
α : Type u_1
inst✝¹ : LT α
inst✝ : DecidableEq α
A B : Finset α
k : α
⊢ (∀ {x : α}, k < x → (x ∈ A ∧ ¬x ∈ B ↔ x ∈ B ∧ ¬x ∈ A)) ∧ (k ∈ A → k ∈ B) ∧ k ∈ B ∧ ¬k ∈ A ↔
    (∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)) ∧ ¬k ∈ A ∧ k ∈ B
constructor
case h.mp.intro.intro.intro
α : Type u_1
inst✝¹ : LT α
inst✝ : DecidableEq α
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ∧ ¬x ∈ B ↔ x ∈ B ∧ ¬x ∈ A)
kAB : k ∈ A → k ∈ B
kB : k ∈ B
kA : ¬k ∈ A
⊢ (∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)) ∧ ¬k ∈ A ∧ k ∈ B
case h.mp
α : Type u_1
inst✝¹ : LT α
inst✝ : DecidableEq α
A B : Finset α
k : α
⊢ (∀ {x : α}, k < x → (x ∈ A ∧ ¬x ∈ B ↔ x ∈ B ∧ ¬x ∈ A)) ∧ (k ∈ A → k ∈ B) ∧ k ∈ B ∧ ¬k ∈ A →
    (∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)) ∧ ¬k ∈ A ∧ k ∈ B
rintro ⟨z, kAB, kB, kA⟩
case h.mp.intro.intro.intro
α : Type u_1
inst✝¹ : LT α
inst✝ : DecidableEq α
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ∧ ¬x ∈ B ↔ x ∈ B ∧ ¬x ∈ A)
kAB : k ∈ A → k ∈ B
kB : k ∈ B
kA : ¬k ∈ A
⊢ ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
case h.mp.intro.intro.intro
α : Type u_1
inst✝¹ : LT α
inst✝ : DecidableEq α
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ∧ ¬x ∈ B ↔ x ∈ B ∧ ¬x ∈ A)
kAB : k ∈ A → k ∈ B
kB : k ∈ B
kA : ¬k ∈ A
⊢ (∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)) ∧ ¬k ∈ A ∧ k ∈ B
refine' ⟨_, kA, kB⟩
case h.mp.intro.intro.intro
α : Type u_1
inst✝¹ : LT α
inst✝ : DecidableEq α
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ∧ ¬x ∈ B ↔ x ∈ B ∧ ¬x ∈ A)
kAB : k ∈ A → k ∈ B
kB : k ∈ B
kA : ¬k ∈ A
x : α
hx : k < x
⊢ x ∈ A ↔ x ∈ B
case h.mp.intro.intro.intro
α : Type u_1
inst✝¹ : LT α
inst✝ : DecidableEq α
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ∧ ¬x ∈ B ↔ x ∈ B ∧ ¬x ∈ A)
kAB : k ∈ A → k ∈ B
kB : k ∈ B
kA : ¬k ∈ A
⊢ ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
intro x hx
case h.mp.intro.intro.intro
α : Type u_1
inst✝¹ : LT α
inst✝ : DecidableEq α
A B : Finset α
k : α
kAB : k ∈ A → k ∈ B
kB : k ∈ B
kA : ¬k ∈ A
x : α
hx : k < x
z : x ∈ A ∧ ¬x ∈ B ↔ x ∈ B ∧ ¬x ∈ A
⊢ x ∈ A ↔ x ∈ B
case h.mp.intro.intro.intro
α : Type u_1
inst✝¹ : LT α
inst✝ : DecidableEq α
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ∧ ¬x ∈ B ↔ x ∈ B ∧ ¬x ∈ A)
kAB : k ∈ A → k ∈ B
kB : k ∈ B
kA : ¬k ∈ A
x : α
hx : k < x
⊢ x ∈ A ↔ x ∈ B
specialize z hx
no goals
case h.mp.intro.intro.intro
α : Type u_1
inst✝¹ : LT α
inst✝ : DecidableEq α
A B : Finset α
k : α
kAB : k ∈ A → k ∈ B
kB : k ∈ B
kA : ¬k ∈ A
x : α
hx : k < x
z : x ∈ A ∧ ¬x ∈ B ↔ x ∈ B ∧ ¬x ∈ A
⊢ x ∈ A ↔ x ∈ B
tauto
case h.mpr.intro.intro
α : Type u_1
inst✝¹ : LT α
inst✝ : DecidableEq α
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
kA : ¬k ∈ A
kB : k ∈ B
⊢ (∀ {x : α}, k < x → (x ∈ A ∧ ¬x ∈ B ↔ x ∈ B ∧ ¬x ∈ A)) ∧ (k ∈ A → k ∈ B) ∧ k ∈ B ∧ ¬k ∈ A
case h.mpr
α : Type u_1
inst✝¹ : LT α
inst✝ : DecidableEq α
A B : Finset α
k : α
⊢ (∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)) ∧ ¬k ∈ A ∧ k ∈ B →
    (∀ {x : α}, k < x → (x ∈ A ∧ ¬x ∈ B ↔ x ∈ B ∧ ¬x ∈ A)) ∧ (k ∈ A → k ∈ B) ∧ k ∈ B ∧ ¬k ∈ A
rintro ⟨z, kA, kB⟩
case h.mpr.intro.intro
α : Type u_1
inst✝¹ : LT α
inst✝ : DecidableEq α
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
kA : ¬k ∈ A
kB : k ∈ B
⊢ ∀ {x : α}, k < x → (x ∈ A ∧ ¬x ∈ B ↔ x ∈ B ∧ ¬x ∈ A)
case h.mpr.intro.intro
α : Type u_1
inst✝¹ : LT α
inst✝ : DecidableEq α
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
kA : ¬k ∈ A
kB : k ∈ B
⊢ (∀ {x : α}, k < x → (x ∈ A ∧ ¬x ∈ B ↔ x ∈ B ∧ ¬x ∈ A)) ∧ (k ∈ A → k ∈ B) ∧ k ∈ B ∧ ¬k ∈ A
refine' ⟨_, fun _ => kB, kB, kA⟩
case h.mpr.intro.intro
α : Type u_1
inst✝¹ : LT α
inst✝ : DecidableEq α
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
kA : ¬k ∈ A
kB : k ∈ B
x : α
hx : k < x
⊢ x ∈ A ∧ ¬x ∈ B ↔ x ∈ B ∧ ¬x ∈ A
case h.mpr.intro.intro
α : Type u_1
inst✝¹ : LT α
inst✝ : DecidableEq α
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
kA : ¬k ∈ A
kB : k ∈ B
⊢ ∀ {x : α}, k < x → (x ∈ A ∧ ¬x ∈ B ↔ x ∈ B ∧ ¬x ∈ A)
intro x hx
no goals
case h.mpr.intro.intro
α : Type u_1
inst✝¹ : LT α
inst✝ : DecidableEq α
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
kA : ¬k ∈ A
kB : k ∈ B
x : α
hx : k < x
⊢ x ∈ A ∧ ¬x ∈ B ↔ x ∈ B ∧ ¬x ∈ A
rw [z hx]