[GOAL]
α : Type u_1
k : ℕ
A : Finset ℕ
h₁ : ∀ {x : ℕ}, x ∈ A → x < k
⊢ Finset.sum A (Nat.pow 2) < 2 ^ k
[PROOFSTEP]
apply lt_of_le_of_lt (sum_le_sum_of_subset fun t => mem_range.2 ∘ h₁)
[GOAL]
α : Type u_1
k : ℕ
A : Finset ℕ
h₁ : ∀ {x : ℕ}, x ∈ A → x < k
⊢ ∑ x in range k, Nat.pow 2 x < 2 ^ k
[PROOFSTEP]
have z := geom_sum_mul_add 1 k
[GOAL]
α : Type u_1
k : ℕ
A : Finset ℕ
h₁ : ∀ {x : ℕ}, x ∈ A → x < k
z : (∑ i in range k, (1 + 1) ^ i) * 1 + 1 = (1 + 1) ^ k
⊢ ∑ x in range k, Nat.pow 2 x < 2 ^ k
[PROOFSTEP]
rw [mul_one, one_add_one_eq_two] at z
[GOAL]
α : Type u_1
k : ℕ
A : Finset ℕ
h₁ : ∀ {x : ℕ}, x ∈ A → x < k
z : ∑ i in range k, 2 ^ i + 1 = 2 ^ k
⊢ ∑ x in range k, Nat.pow 2 x < 2 ^ k
[PROOFSTEP]
rw [← z]
[GOAL]
α : Type u_1
k : ℕ
A : Finset ℕ
h₁ : ∀ {x : ℕ}, x ∈ A → x < k
z : ∑ i in range k, 2 ^ i + 1 = 2 ^ k
⊢ ∑ x in range k, Nat.pow 2 x < ∑ i in range k, 2 ^ i + 1
[PROOFSTEP]
apply Nat.lt_succ_self
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
⊢ toColex (image f A) < toColex (image f B) ↔ toColex A < toColex B
[PROOFSTEP]
simp only [Colex.lt_def, not_exists, mem_image, exists_prop, not_and]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
⊢ (∃ k,
      (∀ {x : β}, k < x → ((∃ a, a ∈ A ∧ f a = x) ↔ ∃ a, a ∈ B ∧ f a = x)) ∧
        (∀ (x : α), x ∈ A → ¬f x = k) ∧ ∃ a, a ∈ B ∧ f a = k) ↔
    ∃ k, (∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)) ∧ ¬k ∈ A ∧ k ∈ B
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
⊢ (∃ k,
      (∀ {x : β}, k < x → ((∃ a, a ∈ A ∧ f a = x) ↔ ∃ a, a ∈ B ∧ f a = x)) ∧
        (∀ (x : α), x ∈ A → ¬f x = k) ∧ ∃ a, a ∈ B ∧ f a = k) →
    ∃ k, (∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)) ∧ ¬k ∈ A ∧ k ∈ B
[PROOFSTEP]
rintro ⟨k, z, q, k', _, rfl⟩
[GOAL]
case mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k' : α
left✝ : k' ∈ B
z : ∀ {x : β}, f k' < x → ((∃ a, a ∈ A ∧ f a = x) ↔ ∃ a, a ∈ B ∧ f a = x)
q : ∀ (x : α), x ∈ A → ¬f x = f k'
⊢ ∃ k, (∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)) ∧ ¬k ∈ A ∧ k ∈ B
[PROOFSTEP]
exact ⟨k', @fun x hx => by simpa [h₁.injective.eq_iff] using z (h₁ hx), fun t => q _ t rfl, ‹k' ∈ B›⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k' : α
left✝ : k' ∈ B
z : ∀ {x : β}, f k' < x → ((∃ a, a ∈ A ∧ f a = x) ↔ ∃ a, a ∈ B ∧ f a = x)
q : ∀ (x : α), x ∈ A → ¬f x = f k'
x : α
hx : k' < x
⊢ x ∈ A ↔ x ∈ B
[PROOFSTEP]
simpa [h₁.injective.eq_iff] using z (h₁ hx)
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
⊢ (∃ k, (∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)) ∧ ¬k ∈ A ∧ k ∈ B) →
    ∃ k,
      (∀ {x : β}, k < x → ((∃ a, a ∈ A ∧ f a = x) ↔ ∃ a, a ∈ B ∧ f a = x)) ∧
        (∀ (x : α), x ∈ A → ¬f x = k) ∧ ∃ a, a ∈ B ∧ f a = k
[PROOFSTEP]
rintro ⟨k, z, ka, _⟩
[GOAL]
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
⊢ ∃ k,
    (∀ {x : β}, k < x → ((∃ a, a ∈ A ∧ f a = x) ↔ ∃ a, a ∈ B ∧ f a = x)) ∧
      (∀ (x : α), x ∈ A → ¬f x = k) ∧ ∃ a, a ∈ B ∧ f a = k
[PROOFSTEP]
refine' ⟨f k, @fun x hx => _, _, k, ‹k ∈ B›, rfl⟩
[GOAL]
case mpr.intro.intro.intro.refine'_1
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
x : β
hx : f k < x
⊢ (∃ a, a ∈ A ∧ f a = x) ↔ ∃ a, a ∈ B ∧ f a = x
[PROOFSTEP]
constructor
[GOAL]
case mpr.intro.intro.intro.refine'_1.mp
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
x : β
hx : f k < x
⊢ (∃ a, a ∈ A ∧ f a = x) → ∃ a, a ∈ B ∧ f a = x
case mpr.intro.intro.intro.refine'_1.mpr
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
x : β
hx : f k < x
⊢ (∃ a, a ∈ B ∧ f a = x) → ∃ a, a ∈ A ∧ f a = x
[PROOFSTEP]
any_goals
  rintro ⟨x', hx', rfl⟩
  refine' ⟨x', _, rfl⟩
  first
  | rwa [← z _]
  | rwa [z _]
  rwa [StrictMono.lt_iff_lt h₁] at hx
[GOAL]
case mpr.intro.intro.intro.refine'_1.mp
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
x : β
hx : f k < x
⊢ (∃ a, a ∈ A ∧ f a = x) → ∃ a, a ∈ B ∧ f a = x
[PROOFSTEP]
rintro ⟨x', hx', rfl⟩
[GOAL]
case mpr.intro.intro.intro.refine'_1.mp.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
x' : α
hx' : x' ∈ A
hx : f k < f x'
⊢ ∃ a, a ∈ B ∧ f a = f x'
[PROOFSTEP]
refine' ⟨x', _, rfl⟩
[GOAL]
case mpr.intro.intro.intro.refine'_1.mp.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
x' : α
hx' : x' ∈ A
hx : f k < f x'
⊢ x' ∈ B
[PROOFSTEP]
first
| rwa [← z _]
| rwa [z _]
[GOAL]
case mpr.intro.intro.intro.refine'_1.mp.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
x' : α
hx' : x' ∈ A
hx : f k < f x'
⊢ x' ∈ B
[PROOFSTEP]
rwa [← z _]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
x' : α
hx' : x' ∈ A
hx : f k < f x'
⊢ k < x'
[PROOFSTEP]
rwa [StrictMono.lt_iff_lt h₁] at hx
[GOAL]
case mpr.intro.intro.intro.refine'_1.mpr
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
x : β
hx : f k < x
⊢ (∃ a, a ∈ B ∧ f a = x) → ∃ a, a ∈ A ∧ f a = x
[PROOFSTEP]
rintro ⟨x', hx', rfl⟩
[GOAL]
case mpr.intro.intro.intro.refine'_1.mpr.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
x' : α
hx' : x' ∈ B
hx : f k < f x'
⊢ ∃ a, a ∈ A ∧ f a = f x'
[PROOFSTEP]
refine' ⟨x', _, rfl⟩
[GOAL]
case mpr.intro.intro.intro.refine'_1.mpr.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
x' : α
hx' : x' ∈ B
hx : f k < f x'
⊢ x' ∈ A
[PROOFSTEP]
first
| rwa [← z _]
| rwa [z _]
[GOAL]
case mpr.intro.intro.intro.refine'_1.mpr.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
x' : α
hx' : x' ∈ B
hx : f k < f x'
⊢ x' ∈ A
[PROOFSTEP]
rwa [← z _]
[GOAL]
case mpr.intro.intro.intro.refine'_1.mpr.intro.intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
x' : α
hx' : x' ∈ B
hx : f k < f x'
⊢ x' ∈ A
[PROOFSTEP]
rwa [z _]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
x' : α
hx' : x' ∈ B
hx : f k < f x'
⊢ k < x'
[PROOFSTEP]
rwa [StrictMono.lt_iff_lt h₁] at hx
[GOAL]
case mpr.intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
⊢ ∀ (x : α), x ∈ A → ¬f x = f k
[PROOFSTEP]
simp only [h₁.injective, Function.Injective.eq_iff]
[GOAL]
case mpr.intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : DecidableEq β
inst✝ : Preorder β
f : α → β
h₁ : StrictMono f
A B : Finset α
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
ka : ¬k ∈ A
right✝ : k ∈ B
⊢ ∀ (x : α), x ∈ A → ¬x = k
[PROOFSTEP]
exact fun x hx => ne_of_mem_of_not_mem hx ka
[GOAL]
α : Type u_1
n : ℕ
A B : Finset (Fin n)
⊢ toColex (image (fun i => ↑i) A) < toColex (image (fun i => ↑i) B) ↔ toColex A < toColex B
[PROOFSTEP]
refine' Colex.hom_lt_iff _ _ _
[GOAL]
α : Type u_1
n : ℕ
A B : Finset (Fin n)
⊢ StrictMono fun i => ↑i
[PROOFSTEP]
exact (fun x y k => k)
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
⊢ a < b → b < c → a < c
[PROOFSTEP]
rintro ⟨k₁, k₁z, notinA, inB⟩ ⟨k₂, k₂z, notinB, inC⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
k₁ : α
k₁z : ∀ {x : α}, k₁ < x → (x ∈ a ↔ x ∈ b)
notinA : ¬k₁ ∈ a
inB : k₁ ∈ b
k₂ : α
k₂z : ∀ {x : α}, k₂ < x → (x ∈ b ↔ x ∈ c)
notinB : ¬k₂ ∈ b
inC : k₂ ∈ c
⊢ a < c
[PROOFSTEP]
cases' lt_or_gt_of_ne (ne_of_mem_of_not_mem inB notinB) with h h
[GOAL]
case intro.intro.intro.intro.intro.intro.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
k₁ : α
k₁z : ∀ {x : α}, k₁ < x → (x ∈ a ↔ x ∈ b)
notinA : ¬k₁ ∈ a
inB : k₁ ∈ b
k₂ : α
k₂z : ∀ {x : α}, k₂ < x → (x ∈ b ↔ x ∈ c)
notinB : ¬k₂ ∈ b
inC : k₂ ∈ c
h : k₁ < k₂
⊢ a < c
[PROOFSTEP]
refine' ⟨k₂, @fun x hx => _, _, inC⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.inl.refine'_1
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
k₁ : α
k₁z : ∀ {x : α}, k₁ < x → (x ∈ a ↔ x ∈ b)
notinA : ¬k₁ ∈ a
inB : k₁ ∈ b
k₂ : α
k₂z : ∀ {x : α}, k₂ < x → (x ∈ b ↔ x ∈ c)
notinB : ¬k₂ ∈ b
inC : k₂ ∈ c
h : k₁ < k₂
x : α
hx : k₂ < x
⊢ x ∈ a ↔ x ∈ c
case intro.intro.intro.intro.intro.intro.inl.refine'_2
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
k₁ : α
k₁z : ∀ {x : α}, k₁ < x → (x ∈ a ↔ x ∈ b)
notinA : ¬k₁ ∈ a
inB : k₁ ∈ b
k₂ : α
k₂z : ∀ {x : α}, k₂ < x → (x ∈ b ↔ x ∈ c)
notinB : ¬k₂ ∈ b
inC : k₂ ∈ c
h : k₁ < k₂
⊢ ¬k₂ ∈ a
[PROOFSTEP]
rw [← k₂z hx]
[GOAL]
case intro.intro.intro.intro.intro.intro.inl.refine'_1
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
k₁ : α
k₁z : ∀ {x : α}, k₁ < x → (x ∈ a ↔ x ∈ b)
notinA : ¬k₁ ∈ a
inB : k₁ ∈ b
k₂ : α
k₂z : ∀ {x : α}, k₂ < x → (x ∈ b ↔ x ∈ c)
notinB : ¬k₂ ∈ b
inC : k₂ ∈ c
h : k₁ < k₂
x : α
hx : k₂ < x
⊢ x ∈ a ↔ x ∈ b
case intro.intro.intro.intro.intro.intro.inl.refine'_2
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
k₁ : α
k₁z : ∀ {x : α}, k₁ < x → (x ∈ a ↔ x ∈ b)
notinA : ¬k₁ ∈ a
inB : k₁ ∈ b
k₂ : α
k₂z : ∀ {x : α}, k₂ < x → (x ∈ b ↔ x ∈ c)
notinB : ¬k₂ ∈ b
inC : k₂ ∈ c
h : k₁ < k₂
⊢ ¬k₂ ∈ a
[PROOFSTEP]
apply k₁z (Trans.trans h hx)
[GOAL]
case intro.intro.intro.intro.intro.intro.inl.refine'_2
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
k₁ : α
k₁z : ∀ {x : α}, k₁ < x → (x ∈ a ↔ x ∈ b)
notinA : ¬k₁ ∈ a
inB : k₁ ∈ b
k₂ : α
k₂z : ∀ {x : α}, k₂ < x → (x ∈ b ↔ x ∈ c)
notinB : ¬k₂ ∈ b
inC : k₂ ∈ c
h : k₁ < k₂
⊢ ¬k₂ ∈ a
[PROOFSTEP]
rwa [k₁z h]
[GOAL]
case intro.intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
k₁ : α
k₁z : ∀ {x : α}, k₁ < x → (x ∈ a ↔ x ∈ b)
notinA : ¬k₁ ∈ a
inB : k₁ ∈ b
k₂ : α
k₂z : ∀ {x : α}, k₂ < x → (x ∈ b ↔ x ∈ c)
notinB : ¬k₂ ∈ b
inC : k₂ ∈ c
h : k₁ > k₂
⊢ a < c
[PROOFSTEP]
refine' ⟨k₁, @fun x hx => _, notinA, by rwa [← k₂z h]⟩
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
k₁ : α
k₁z : ∀ {x : α}, k₁ < x → (x ∈ a ↔ x ∈ b)
notinA : ¬k₁ ∈ a
inB : k₁ ∈ b
k₂ : α
k₂z : ∀ {x : α}, k₂ < x → (x ∈ b ↔ x ∈ c)
notinB : ¬k₂ ∈ b
inC : k₂ ∈ c
h : k₁ > k₂
⊢ k₁ ∈ c
[PROOFSTEP]
rwa [← k₂z h]
[GOAL]
case intro.intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
k₁ : α
k₁z : ∀ {x : α}, k₁ < x → (x ∈ a ↔ x ∈ b)
notinA : ¬k₁ ∈ a
inB : k₁ ∈ b
k₂ : α
k₂z : ∀ {x : α}, k₂ < x → (x ∈ b ↔ x ∈ c)
notinB : ¬k₂ ∈ b
inC : k₂ ∈ c
h : k₁ > k₂
x : α
hx : k₁ < x
⊢ x ∈ a ↔ x ∈ c
[PROOFSTEP]
rw [k₁z hx]
[GOAL]
case intro.intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
k₁ : α
k₁z : ∀ {x : α}, k₁ < x → (x ∈ a ↔ x ∈ b)
notinA : ¬k₁ ∈ a
inB : k₁ ∈ b
k₂ : α
k₂z : ∀ {x : α}, k₂ < x → (x ∈ b ↔ x ∈ c)
notinB : ¬k₂ ∈ b
inC : k₂ ∈ c
h : k₁ > k₂
x : α
hx : k₁ < x
⊢ x ∈ b ↔ x ∈ c
[PROOFSTEP]
apply k₂z (Trans.trans h hx)
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
⊢ A < B ∨ A = B ∨ B < A
[PROOFSTEP]
by_cases h₁ : A = B
[GOAL]
case pos
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : A = B
⊢ A < B ∨ A = B ∨ B < A
[PROOFSTEP]
tauto
[GOAL]
case neg
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
⊢ A < B ∨ A = B ∨ B < A
[PROOFSTEP]
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)
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
⊢ Finset.Nonempty (A \ B ∪ B \ A)
[PROOFSTEP]
rw [nonempty_iff_ne_empty]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
⊢ A \ B ∪ B \ A ≠ ∅
[PROOFSTEP]
intro a
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
a : A \ B ∪ B \ A = ∅
⊢ False
[PROOFSTEP]
simp only [union_eq_empty_iff, sdiff_eq_empty_iff_subset] at a
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
A B : Colex α
h₁ : ¬A = B
a : A ⊆ B ∧ B ⊆ A
⊢ False
[PROOFSTEP]
apply h₁ (Subset.antisymm a.1 a.2)
[GOAL]
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
[PROOFSTEP]
rcases exists_max_image (A \ B ∪ B \ A) id h with ⟨k, ⟨hk, z⟩⟩
[GOAL]
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
[PROOFSTEP]
simp only [mem_union, mem_sdiff] at hk
[GOAL]
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
[PROOFSTEP]
cases' hk with hk hk
[GOAL]
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
[PROOFSTEP]
right
[GOAL]
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
[PROOFSTEP]
right
[GOAL]
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
[PROOFSTEP]
refine' ⟨k, @fun t th => _, hk.2, hk.1⟩
[GOAL]
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
[PROOFSTEP]
specialize z t
[GOAL]
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
[PROOFSTEP]
by_contra h₂
[GOAL]
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
[PROOFSTEP]
simp only [mem_union, mem_sdiff, id.def] at z
[GOAL]
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
[PROOFSTEP]
rw [not_iff, iff_iff_and_or_not_and_not, not_not, and_comm] at h₂
[GOAL]
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
[PROOFSTEP]
apply not_le_of_lt th (z h₂)
[GOAL]
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
[PROOFSTEP]
left
[GOAL]
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
[PROOFSTEP]
refine' ⟨k, @fun t th => _, hk.2, hk.1⟩
[GOAL]
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
[PROOFSTEP]
specialize z t
[GOAL]
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
[PROOFSTEP]
by_contra h₃
[GOAL]
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
[PROOFSTEP]
simp only [mem_union, mem_sdiff, id.def] at z
[GOAL]
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
[PROOFSTEP]
rw [not_iff, iff_iff_and_or_not_and_not, not_not, and_comm, or_comm] at h₃
[GOAL]
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
[PROOFSTEP]
apply not_le_of_lt th (z h₃)
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
A✝ B✝ : Colex α
A B : Finset α
⊢ toColex A < toColex B ↔ ∃ k, k ∈ B ∧ (∀ (x : α), x ∈ A ∪ B → k < x → (x ∈ A ↔ x ∈ B)) ∧ ¬k ∈ A
[PROOFSTEP]
rw [Colex.lt_def]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
A✝ B✝ : Colex α
A B : Finset α
⊢ (∃ k, (∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)) ∧ ¬k ∈ A ∧ k ∈ B) ↔
    ∃ k, k ∈ B ∧ (∀ (x : α), x ∈ A ∪ B → k < x → (x ∈ A ↔ x ∈ B)) ∧ ¬k ∈ A
[PROOFSTEP]
apply exists_congr
[GOAL]
case h
α : Type u_1
inst✝ : LinearOrder α
A✝ B✝ : Colex α
A B : Finset α
⊢ ∀ (a : α),
    (∀ {x : α}, a < x → (x ∈ A ↔ x ∈ B)) ∧ ¬a ∈ A ∧ a ∈ B ↔
      a ∈ B ∧ (∀ (x : α), x ∈ A ∪ B → a < x → (x ∈ A ↔ x ∈ B)) ∧ ¬a ∈ A
[PROOFSTEP]
simp only [mem_union, exists_prop, or_imp, and_comm (a := _ ∈ B), and_assoc]
[GOAL]
case h
α : Type u_1
inst✝ : LinearOrder α
A✝ B✝ : Colex α
A B : Finset α
⊢ ∀ (a : α),
    (∀ {x : α}, a < x → (x ∈ A ↔ x ∈ B)) ∧ ¬a ∈ A ∧ a ∈ B ↔
      (∀ (x : α), (x ∈ A → a < x → (x ∈ A ↔ x ∈ B)) ∧ (x ∈ B → a < x → (x ∈ A ↔ x ∈ B))) ∧ ¬a ∈ A ∧ a ∈ B
[PROOFSTEP]
intro k
[GOAL]
case h
α : Type u_1
inst✝ : LinearOrder α
A✝ B✝ : Colex α
A B : Finset α
k : α
⊢ (∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)) ∧ ¬k ∈ A ∧ k ∈ B ↔
    (∀ (x : α), (x ∈ A → k < x → (x ∈ A ↔ x ∈ B)) ∧ (x ∈ B → k < x → (x ∈ A ↔ x ∈ B))) ∧ ¬k ∈ A ∧ k ∈ B
[PROOFSTEP]
refine' and_congr_left' (forall_congr' _)
[GOAL]
case h
α : Type u_1
inst✝ : LinearOrder α
A✝ B✝ : Colex α
A B : Finset α
k : α
⊢ ∀ (a : α), k < a → (a ∈ A ↔ a ∈ B) ↔ (a ∈ A → k < a → (a ∈ A ↔ a ∈ B)) ∧ (a ∈ B → k < a → (a ∈ A ↔ a ∈ B))
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
src✝¹ : LT (Colex α) := instLT
src✝ : LE (Colex α) := instLE
A B : Colex α
⊢ A < B ↔ A ≤ B ∧ ¬B ≤ A
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
inst✝ : LinearOrder α
src✝¹ : LT (Colex α) := instLT
src✝ : LE (Colex α) := instLE
A B : Colex α
⊢ A < B → A ≤ B ∧ ¬B ≤ A
[PROOFSTEP]
intro t
[GOAL]
case mp
α : Type u_1
inst✝ : LinearOrder α
src✝¹ : LT (Colex α) := instLT
src✝ : LE (Colex α) := instLE
A B : Colex α
t : A < B
⊢ A ≤ B ∧ ¬B ≤ A
[PROOFSTEP]
refine' ⟨Or.inl t, _⟩
[GOAL]
case mp
α : Type u_1
inst✝ : LinearOrder α
src✝¹ : LT (Colex α) := instLT
src✝ : LE (Colex α) := instLE
A B : Colex α
t : A < B
⊢ ¬B ≤ A
[PROOFSTEP]
rintro (i | rfl)
[GOAL]
case mp.inl
α : Type u_1
inst✝ : LinearOrder α
src✝¹ : LT (Colex α) := instLT
src✝ : LE (Colex α) := instLE
A B : Colex α
t : A < B
i : B < A
⊢ False
[PROOFSTEP]
apply asymm_of _ t i
[GOAL]
case mp.inr
α : Type u_1
inst✝ : LinearOrder α
src✝¹ : LT (Colex α) := instLT
src✝ : LE (Colex α) := instLE
B : Colex α
t : B < B
⊢ False
[PROOFSTEP]
apply irrefl _ t
[GOAL]
case mpr
α : Type u_1
inst✝ : LinearOrder α
src✝¹ : LT (Colex α) := instLT
src✝ : LE (Colex α) := instLE
A B : Colex α
⊢ A ≤ B ∧ ¬B ≤ A → A < B
[PROOFSTEP]
rintro ⟨h₁ | rfl, h₂⟩
[GOAL]
case mpr.intro.inl
α : Type u_1
inst✝ : LinearOrder α
src✝¹ : LT (Colex α) := instLT
src✝ : LE (Colex α) := instLE
A B : Colex α
h₂ : ¬B ≤ A
h₁ : A < B
⊢ A < B
[PROOFSTEP]
apply h₁
[GOAL]
case mpr.intro.inr
α : Type u_1
inst✝ : LinearOrder α
src✝¹ : LT (Colex α) := instLT
src✝ : LE (Colex α) := instLE
A : Colex α
h₂ : ¬A ≤ A
⊢ A < A
[PROOFSTEP]
apply h₂.elim (Or.inr rfl)
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
src✝¹ : LT (Colex α) := instLT
src✝ : LE (Colex α) := instLE
⊢ DecidableRel fun x x_1 => x ≤ x_1
[PROOFSTEP]
letI : DecidableEq (Finset.Colex α) := inferInstanceAs (DecidableEq (Finset α))
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
src✝¹ : LT (Colex α) := instLT
src✝ : LE (Colex α) := instLE
this : DecidableEq (Colex α) := inferInstanceAs (DecidableEq (Finset α))
⊢ DecidableRel fun x x_1 => x ≤ x_1
[PROOFSTEP]
exact fun A B => inferInstanceAs (Decidable (A < B ∨ A = B))
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
h₁ : StrictMono f
A B : Finset α
⊢ toColex (image f A) ≤ toColex (image f B) ↔ toColex A ≤ toColex B
[PROOFSTEP]
rw [le_iff_le_iff_lt_iff_lt, hom_lt_iff h₁]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
t : α
h₁ : toColex A < toColex B
h₂ : ∀ (x : α), x ∈ B → x < t
⊢ ∀ (x : α), x ∈ A → x < t
[PROOFSTEP]
rw [Colex.lt_def] at h₁
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
t : α
h₁ : ∃ k, (∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)) ∧ ¬k ∈ A ∧ k ∈ B
h₂ : ∀ (x : α), x ∈ B → x < t
⊢ ∀ (x : α), x ∈ A → x < t
[PROOFSTEP]
rcases h₁ with ⟨k, z, _, _⟩
[GOAL]
case intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
t : α
h₂ : ∀ (x : α), x ∈ B → x < t
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
left✝ : ¬k ∈ A
right✝ : k ∈ B
⊢ ∀ (x : α), x ∈ A → x < t
[PROOFSTEP]
intro x hx
[GOAL]
case intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
t : α
h₂ : ∀ (x : α), x ∈ B → x < t
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
left✝ : ¬k ∈ A
right✝ : k ∈ B
x : α
hx : x ∈ A
⊢ x < t
[PROOFSTEP]
apply lt_of_not_ge
[GOAL]
case intro.intro.intro.h
α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
t : α
h₂ : ∀ (x : α), x ∈ B → x < t
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
left✝ : ¬k ∈ A
right✝ : k ∈ B
x : α
hx : x ∈ A
⊢ ¬x ≥ t
[PROOFSTEP]
intro a
[GOAL]
case intro.intro.intro.h
α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
t : α
h₂ : ∀ (x : α), x ∈ B → x < t
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
left✝ : ¬k ∈ A
right✝ : k ∈ B
x : α
hx : x ∈ A
a : x ≥ t
⊢ False
[PROOFSTEP]
refine' not_lt_of_ge a (h₂ x _)
[GOAL]
case intro.intro.intro.h
α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
t : α
h₂ : ∀ (x : α), x ∈ B → x < t
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
left✝ : ¬k ∈ A
right✝ : k ∈ B
x : α
hx : x ∈ A
a : x ≥ t
⊢ x ∈ B
[PROOFSTEP]
rwa [← z]
[GOAL]
case intro.intro.intro.h
α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
t : α
h₂ : ∀ (x : α), x ∈ B → x < t
k : α
z : ∀ {x : α}, k < x → (x ∈ A ↔ x ∈ B)
left✝ : ¬k ∈ A
right✝ : k ∈ B
x : α
hx : x ∈ A
a : x ≥ t
⊢ k < x
[PROOFSTEP]
apply lt_of_lt_of_le (h₂ k ‹_›) a
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
⊢ toColex s < toColex {r} ↔ ∀ (x : α), x ∈ s → x < r
[PROOFSTEP]
simp only [lt_def, mem_singleton, ← and_assoc, exists_eq_right]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
⊢ (∀ {x : α}, r < x → (x ∈ s ↔ x = r)) ∧ ¬r ∈ s ↔ ∀ (x : α), x ∈ s → x < r
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
⊢ (∀ {x : α}, r < x → (x ∈ s ↔ x = r)) ∧ ¬r ∈ s → ∀ (x : α), x ∈ s → x < r
[PROOFSTEP]
intro t x hx
[GOAL]
case mp
α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
t : (∀ {x : α}, r < x → (x ∈ s ↔ x = r)) ∧ ¬r ∈ s
x : α
hx : x ∈ s
⊢ x < r
[PROOFSTEP]
rw [← not_le]
[GOAL]
case mp
α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
t : (∀ {x : α}, r < x → (x ∈ s ↔ x = r)) ∧ ¬r ∈ s
x : α
hx : x ∈ s
⊢ ¬r ≤ x
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
t : (∀ {x : α}, r < x → (x ∈ s ↔ x = r)) ∧ ¬r ∈ s
x : α
hx : x ∈ s
h : r ≤ x
⊢ False
[PROOFSTEP]
rcases lt_or_eq_of_le h with (h₁ | rfl)
[GOAL]
case mp.inl
α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
t : (∀ {x : α}, r < x → (x ∈ s ↔ x = r)) ∧ ¬r ∈ s
x : α
hx : x ∈ s
h : r ≤ x
h₁ : r < x
⊢ False
[PROOFSTEP]
exact ne_of_irrefl h₁ ((t.1 h₁).1 hx).symm
[GOAL]
case mp.inr
α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
t : (∀ {x : α}, r < x → (x ∈ s ↔ x = r)) ∧ ¬r ∈ s
hx : r ∈ s
h : r ≤ r
⊢ False
[PROOFSTEP]
exact t.2 hx
[GOAL]
case mpr
α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
⊢ (∀ (x : α), x ∈ s → x < r) → (∀ {x : α}, r < x → (x ∈ s ↔ x = r)) ∧ ¬r ∈ s
[PROOFSTEP]
exact fun h => ⟨fun {z} hz => ⟨fun i => (asymm hz (h _ i)).elim, fun i => (hz.ne' i).elim⟩, by simpa using h r⟩
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
h : ∀ (x : α), x ∈ s → x < r
⊢ ¬r ∈ s
[PROOFSTEP]
simpa using h r
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
⊢ toColex {r} ≤ toColex s ↔ ∃ x, x ∈ s ∧ r ≤ x
[PROOFSTEP]
simp only [← not_lt]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
r : α
s : Finset α
⊢ ¬toColex s < toColex {r} ↔ ∃ x, x ∈ s ∧ ¬x < r
[PROOFSTEP]
simp [lt_singleton_iff_mem_lt]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
r s : α
⊢ toColex {r} < toColex {s} ↔ r < s
[PROOFSTEP]
simp [lt_singleton_iff_mem_lt]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
r s : α
⊢ toColex {r} ≤ toColex {s} ↔ r ≤ s
[PROOFSTEP]
rw [le_iff_le_iff_lt_iff_lt, singleton_lt_iff_lt]
[GOAL]
α : Type u_1
inst✝¹ : LT α
inst✝ : DecidableEq α
A B : Finset α
⊢ toColex (A \ B) < toColex (B \ A) ↔ toColex A < toColex B
[PROOFSTEP]
rw [Colex.lt_def, Colex.lt_def]
[GOAL]
α : 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
[PROOFSTEP]
apply exists_congr
[GOAL]
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
[PROOFSTEP]
intro k
[GOAL]
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
[PROOFSTEP]
simp only [mem_sdiff, not_and, not_not]
[GOAL]
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
[PROOFSTEP]
constructor
[GOAL]
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
[PROOFSTEP]
rintro ⟨z, kAB, kB, kA⟩
[GOAL]
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
[PROOFSTEP]
refine' ⟨_, kA, kB⟩
[GOAL]
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)
[PROOFSTEP]
intro x hx
[GOAL]
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
[PROOFSTEP]
specialize z hx
[GOAL]
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
[PROOFSTEP]
tauto
[GOAL]
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
[PROOFSTEP]
rintro ⟨z, kA, kB⟩
[GOAL]
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
[PROOFSTEP]
refine' ⟨_, fun _ => kB, kB, kA⟩
[GOAL]
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)
[PROOFSTEP]
intro x hx
[GOAL]
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
[PROOFSTEP]
rw [z hx]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
⊢ toColex (A \ B) ≤ toColex (B \ A) ↔ toColex A ≤ toColex B
[PROOFSTEP]
rw [le_iff_le_iff_lt_iff_lt, sdiff_lt_sdiff_iff_lt]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
A : Finset α
hA : Finset.Nonempty A
⊢ toColex ∅ < toColex A
[PROOFSTEP]
rw [Colex.lt_def]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
A : Finset α
hA : Finset.Nonempty A
⊢ ∃ k, (∀ {x : α}, k < x → (x ∈ ∅ ↔ x ∈ A)) ∧ ¬k ∈ ∅ ∧ k ∈ A
[PROOFSTEP]
refine' ⟨max' _ hA, _, by simp, max'_mem _ _⟩
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
A : Finset α
hA : Finset.Nonempty A
⊢ ¬max' A hA ∈ ∅
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
A : Finset α
hA : Finset.Nonempty A
⊢ ∀ {x : α}, max' A hA < x → (x ∈ ∅ ↔ x ∈ A)
[PROOFSTEP]
simp only [false_iff_iff, not_mem_empty]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
A : Finset α
hA : Finset.Nonempty A
⊢ ∀ {x : α}, max' A hA < x → ¬x ∈ A
[PROOFSTEP]
intro x hx t
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
A : Finset α
hA : Finset.Nonempty A
x : α
hx : max' A hA < x
t : x ∈ A
⊢ False
[PROOFSTEP]
apply not_le_of_lt hx (le_max' _ _ t)
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
h : A ⊂ B
⊢ toColex A < toColex B
[PROOFSTEP]
rw [← sdiff_lt_sdiff_iff_lt, sdiff_eq_empty_iff_subset.2 h.1]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
h : A ⊂ B
⊢ toColex ∅ < toColex (B \ A)
[PROOFSTEP]
exact empty_toColex_lt (by simpa [Finset.Nonempty] using exists_of_ssubset h)
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
h : A ⊂ B
⊢ Finset.Nonempty (B \ A)
[PROOFSTEP]
simpa [Finset.Nonempty] using exists_of_ssubset h
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
A : Finset α
⊢ toColex ∅ ≤ toColex A
[PROOFSTEP]
rcases A.eq_empty_or_nonempty with (rfl | hA)
[GOAL]
case inl
α : Type u_1
inst✝ : LinearOrder α
⊢ toColex ∅ ≤ toColex ∅
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u_1
inst✝ : LinearOrder α
A : Finset α
hA : Finset.Nonempty A
⊢ toColex ∅ ≤ toColex A
[PROOFSTEP]
apply (empty_toColex_lt hA).le
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
h : A ⊆ B
⊢ toColex A ≤ toColex B
[PROOFSTEP]
rw [← sdiff_le_sdiff_iff_le, sdiff_eq_empty_iff_subset.2 h]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
h : A ⊆ B
⊢ toColex ∅ ≤ toColex (B \ A)
[PROOFSTEP]
apply empty_toColex_le
[GOAL]
α : Type u_1
A B : Finset ℕ
⊢ ∑ i in A, 2 ^ i < ∑ i in B, 2 ^ i ↔ toColex A < toColex B
[PROOFSTEP]
have z : ∀ A B : Finset ℕ, A.toColex < B.toColex → ∑ i in A, 2 ^ i < ∑ i in B, 2 ^ i :=
  by
  intro A B
  rw [← sdiff_lt_sdiff_iff_lt, Colex.lt_def]
  rintro ⟨k, z, kA, kB⟩
  rw [← sdiff_union_inter A B]
  conv_rhs => rw [← sdiff_union_inter B A]
  rw [sum_union (disjoint_sdiff_inter _ _), sum_union (disjoint_sdiff_inter _ _), inter_comm, add_lt_add_iff_right]
  apply lt_of_lt_of_le (@Nat.sum_two_pow_lt k (A \ B) _)
  · apply single_le_sum (fun _ _ => Nat.zero_le _) kB
  intro x hx
  apply lt_of_le_of_ne (le_of_not_lt _)
  · apply ne_of_mem_of_not_mem hx kA
  intro kx
  have := (z kx).1 hx
  rw [mem_sdiff] at this hx
  exact hx.2 this.1
[GOAL]
α : Type u_1
A B : Finset ℕ
⊢ ∀ (A B : Finset ℕ), toColex A < toColex B → ∑ i in A, 2 ^ i < ∑ i in B, 2 ^ i
[PROOFSTEP]
intro A B
[GOAL]
α : Type u_1
A✝ B✝ A B : Finset ℕ
⊢ toColex A < toColex B → ∑ i in A, 2 ^ i < ∑ i in B, 2 ^ i
[PROOFSTEP]
rw [← sdiff_lt_sdiff_iff_lt, Colex.lt_def]
[GOAL]
α : Type u_1
A✝ B✝ A B : Finset ℕ
⊢ (∃ k, (∀ {x : ℕ}, k < x → (x ∈ A \ B ↔ x ∈ B \ A)) ∧ ¬k ∈ A \ B ∧ k ∈ B \ A) → ∑ i in A, 2 ^ i < ∑ i in B, 2 ^ i
[PROOFSTEP]
rintro ⟨k, z, kA, kB⟩
[GOAL]
case intro.intro.intro
α : Type u_1
A✝ B✝ A B : Finset ℕ
k : ℕ
z : ∀ {x : ℕ}, k < x → (x ∈ A \ B ↔ x ∈ B \ A)
kA : ¬k ∈ A \ B
kB : k ∈ B \ A
⊢ ∑ i in A, 2 ^ i < ∑ i in B, 2 ^ i
[PROOFSTEP]
rw [← sdiff_union_inter A B]
[GOAL]
case intro.intro.intro
α : Type u_1
A✝ B✝ A B : Finset ℕ
k : ℕ
z : ∀ {x : ℕ}, k < x → (x ∈ A \ B ↔ x ∈ B \ A)
kA : ¬k ∈ A \ B
kB : k ∈ B \ A
⊢ ∑ i in A \ B ∪ A ∩ B, 2 ^ i < ∑ i in B, 2 ^ i
[PROOFSTEP]
conv_rhs => rw [← sdiff_union_inter B A]
[GOAL]
α : Type u_1
A✝ B✝ A B : Finset ℕ
k : ℕ
z : ∀ {x : ℕ}, k < x → (x ∈ A \ B ↔ x ∈ B \ A)
kA : ¬k ∈ A \ B
kB : k ∈ B \ A
| ∑ i in B, 2 ^ i
[PROOFSTEP]
rw [← sdiff_union_inter B A]
[GOAL]
α : Type u_1
A✝ B✝ A B : Finset ℕ
k : ℕ
z : ∀ {x : ℕ}, k < x → (x ∈ A \ B ↔ x ∈ B \ A)
kA : ¬k ∈ A \ B
kB : k ∈ B \ A
| ∑ i in B, 2 ^ i
[PROOFSTEP]
rw [← sdiff_union_inter B A]
[GOAL]
α : Type u_1
A✝ B✝ A B : Finset ℕ
k : ℕ
z : ∀ {x : ℕ}, k < x → (x ∈ A \ B ↔ x ∈ B \ A)
kA : ¬k ∈ A \ B
kB : k ∈ B \ A
| ∑ i in B, 2 ^ i
[PROOFSTEP]
rw [← sdiff_union_inter B A]
[GOAL]
case intro.intro.intro
α : Type u_1
A✝ B✝ A B : Finset ℕ
k : ℕ
z : ∀ {x : ℕ}, k < x → (x ∈ A \ B ↔ x ∈ B \ A)
kA : ¬k ∈ A \ B
kB : k ∈ B \ A
⊢ ∑ i in A \ B ∪ A ∩ B, 2 ^ i < ∑ i in B \ A ∪ B ∩ A, 2 ^ i
[PROOFSTEP]
rw [sum_union (disjoint_sdiff_inter _ _), sum_union (disjoint_sdiff_inter _ _), inter_comm, add_lt_add_iff_right]
[GOAL]
case intro.intro.intro
α : Type u_1
A✝ B✝ A B : Finset ℕ
k : ℕ
z : ∀ {x : ℕ}, k < x → (x ∈ A \ B ↔ x ∈ B \ A)
kA : ¬k ∈ A \ B
kB : k ∈ B \ A
⊢ ∑ x in A \ B, 2 ^ x < ∑ x in B \ A, 2 ^ x
[PROOFSTEP]
apply lt_of_lt_of_le (@Nat.sum_two_pow_lt k (A \ B) _)
[GOAL]
case intro.intro.intro
α : Type u_1
A✝ B✝ A B : Finset ℕ
k : ℕ
z : ∀ {x : ℕ}, k < x → (x ∈ A \ B ↔ x ∈ B \ A)
kA : ¬k ∈ A \ B
kB : k ∈ B \ A
⊢ 2 ^ k ≤ ∑ x in B \ A, 2 ^ x
[PROOFSTEP]
apply single_le_sum (fun _ _ => Nat.zero_le _) kB
[GOAL]
α : Type u_1
A✝ B✝ A B : Finset ℕ
k : ℕ
z : ∀ {x : ℕ}, k < x → (x ∈ A \ B ↔ x ∈ B \ A)
kA : ¬k ∈ A \ B
kB : k ∈ B \ A
⊢ ∀ {x : ℕ}, x ∈ A \ B → x < k
[PROOFSTEP]
intro x hx
[GOAL]
α : Type u_1
A✝ B✝ A B : Finset ℕ
k : ℕ
z : ∀ {x : ℕ}, k < x → (x ∈ A \ B ↔ x ∈ B \ A)
kA : ¬k ∈ A \ B
kB : k ∈ B \ A
x : ℕ
hx : x ∈ A \ B
⊢ x < k
[PROOFSTEP]
apply lt_of_le_of_ne (le_of_not_lt _)
[GOAL]
α : Type u_1
A✝ B✝ A B : Finset ℕ
k : ℕ
z : ∀ {x : ℕ}, k < x → (x ∈ A \ B ↔ x ∈ B \ A)
kA : ¬k ∈ A \ B
kB : k ∈ B \ A
x : ℕ
hx : x ∈ A \ B
⊢ x ≠ k
[PROOFSTEP]
apply ne_of_mem_of_not_mem hx kA
[GOAL]
α : Type u_1
A✝ B✝ A B : Finset ℕ
k : ℕ
z : ∀ {x : ℕ}, k < x → (x ∈ A \ B ↔ x ∈ B \ A)
kA : ¬k ∈ A \ B
kB : k ∈ B \ A
x : ℕ
hx : x ∈ A \ B
⊢ ¬k < x
[PROOFSTEP]
intro kx
[GOAL]
α : Type u_1
A✝ B✝ A B : Finset ℕ
k : ℕ
z : ∀ {x : ℕ}, k < x → (x ∈ A \ B ↔ x ∈ B \ A)
kA : ¬k ∈ A \ B
kB : k ∈ B \ A
x : ℕ
hx : x ∈ A \ B
kx : k < x
⊢ False
[PROOFSTEP]
have := (z kx).1 hx
[GOAL]
α : Type u_1
A✝ B✝ A B : Finset ℕ
k : ℕ
z : ∀ {x : ℕ}, k < x → (x ∈ A \ B ↔ x ∈ B \ A)
kA : ¬k ∈ A \ B
kB : k ∈ B \ A
x : ℕ
hx : x ∈ A \ B
kx : k < x
this : x ∈ B \ A
⊢ False
[PROOFSTEP]
rw [mem_sdiff] at this hx
[GOAL]
α : Type u_1
A✝ B✝ A B : Finset ℕ
k : ℕ
z : ∀ {x : ℕ}, k < x → (x ∈ A \ B ↔ x ∈ B \ A)
kA : ¬k ∈ A \ B
kB : k ∈ B \ A
x : ℕ
hx : x ∈ A ∧ ¬x ∈ B
kx : k < x
this : x ∈ B ∧ ¬x ∈ A
⊢ False
[PROOFSTEP]
exact hx.2 this.1
[GOAL]
α : Type u_1
A B : Finset ℕ
z : ∀ (A B : Finset ℕ), toColex A < toColex B → ∑ i in A, 2 ^ i < ∑ i in B, 2 ^ i
⊢ ∑ i in A, 2 ^ i < ∑ i in B, 2 ^ i ↔ toColex A < toColex B
[PROOFSTEP]
refine' ⟨fun h => (lt_trichotomy A B).resolve_right fun h₁ => h₁.elim _ (not_lt_of_gt h ∘ z _ _), z A B⟩
[GOAL]
α : Type u_1
A B : Finset ℕ
z : ∀ (A B : Finset ℕ), toColex A < toColex B → ∑ i in A, 2 ^ i < ∑ i in B, 2 ^ i
h : ∑ i in A, 2 ^ i < ∑ i in B, 2 ^ i
h₁ : A = B ∨ B < A
⊢ A = B → False
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
A : Finset ℕ
z : ∀ (A B : Finset ℕ), toColex A < toColex B → ∑ i in A, 2 ^ i < ∑ i in B, 2 ^ i
h : ∑ i in A, 2 ^ i < ∑ i in A, 2 ^ i
h₁ : A = A ∨ A < A
⊢ False
[PROOFSTEP]
apply irrefl _ h
[GOAL]
α : Type u_1
A B : Finset ℕ
⊢ ∑ i in A, 2 ^ i ≤ ∑ i in B, 2 ^ i ↔ toColex A ≤ toColex B
[PROOFSTEP]
rw [le_iff_le_iff_lt_iff_lt, sum_two_pow_lt_iff_lt]