α : Type ?u.84084
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
α : Type ?u.84084
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
refine'
  ⟨fun h => (lt_trichotomy A B).resolve_right fun h₁ => h₁.elim _ (not_lt_of_gt h ∘ z _ _), z A B⟩
α : Type ?u.84084
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
α : Type ?u.84084
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
rintro rfl
no goals
α : Type ?u.84084
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
apply irrefl _ h
α : Type ?u.84084
A✝ B✝ A B : Finset ℕ
⊢ toColex A < toColex B → ∑ i in A, 2 ^ i < ∑ i in B, 2 ^ i
α : Type ?u.84084
A B : Finset ℕ
⊢ ∀ (A B : Finset ℕ), toColex A < toColex B → ∑ i in A, 2 ^ i < ∑ i in B, 2 ^ i
intro A B
α : Type ?u.84084
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
α : Type ?u.84084
A✝ B✝ A B : Finset ℕ
⊢ toColex A < toColex B → ∑ i in A, 2 ^ i < ∑ i in B, 2 ^ i
rw [← sdiff_lt_sdiff_iff_lt, Colex.lt_def]
case intro.intro.intro
α : Type ?u.84084
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
α : Type ?u.84084
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
rintro ⟨k, z, kA, kB⟩
case intro.intro.intro
α : Type ?u.84084
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
case intro.intro.intro
α : Type ?u.84084
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
rw [← sdiff_union_inter A B]
case intro.intro.intro
α : Type ?u.84084
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
case intro.intro.intro
α : Type ?u.84084
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
conv_rhs => rw [← sdiff_union_inter B A]
case intro.intro.intro
α : Type ?u.84084
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
case intro.intro.intro
α : Type ?u.84084
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
rw [sum_union (disjoint_sdiff_inter _ _), sum_union (disjoint_sdiff_inter _ _), inter_comm,
  add_lt_add_iff_right]
case intro.intro.intro
α : Type ?u.84084
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

α : Type ?u.84084
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
case intro.intro.intro
α : Type ?u.84084
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
apply lt_of_lt_of_le (@Nat.sum_two_pow_lt k (A \ B) _)
α : Type ?u.84084
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
α : Type ?u.84084
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
intro x hx
α : Type ?u.84084
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

α : Type ?u.84084
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
α : Type ?u.84084
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
apply lt_of_le_of_ne (le_of_not_lt _)
α : Type ?u.84084
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
α : Type ?u.84084
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
intro kx
α : Type ?u.84084
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
α : Type ?u.84084
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
have := (z kx).1 hx
α : Type ?u.84084
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
α : Type ?u.84084
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
rw [mem_sdiff] at this hx
no goals
α : Type ?u.84084
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
exact hx.2 this.1
no goals
case intro.intro.intro
α : Type ?u.84084
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
apply single_le_sum (fun _ _ => Nat.zero_le _) kB
no goals
α : Type ?u.84084
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
apply ne_of_mem_of_not_mem hx kA