internlm/Lean-Github huggingface dataset:
Theorem: Finset.UV.isInitSeg_of_compressed
Proof state before:
case inl
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := A }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : A.card = B.card
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
hlt : (A \ B).max' hU < (B \ A).max' hV
⊢ (B \ A).max' hV < (A \ B).max' hU
Tactic:
rw [← compress_sdiff_sdiff A B] at hAB hBA
Proof state after:
case inl
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := compress (A \ B) (B \ A) B }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : compress (A \ B) (B \ A) B ≠ B
hAB' : A.card = B.card
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
hlt : (A \ B).max' hU < (B \ A).max' hV
⊢ (B \ A).max' hV < (A \ B).max' hU
Theorem: Finset.UV.isInitSeg_of_compressed
Proof state before:
case inl
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := compress (A \ B) (B \ A) B }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : compress (A \ B) (B \ A) B ≠ B
hAB' : A.card = B.card
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
hlt : (A \ B).max' hU < (B \ A).max' hV
⊢ (B \ A).max' hV < (A \ B).max' hU
Tactic:
cases hBA.not_lt $ toColex_compress_lt_toColex hlt hAB
Proof state after:
no goals
Theorem: Finset.UV.isInitSeg_of_compressed
Proof state before:
case inr.inl
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := A }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : A.card = B.card
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
heq : (A \ B).max' hU = (B \ A).max' hV
⊢ (B \ A).max' hV < (A \ B).max' hU
Tactic:
exact (disjoint_right.1 disj (max'_mem _ hU) $ heq.symm ▸ max'_mem _ _).elim
Proof state after:
no goals
Theorem: Finset.UV.isInitSeg_of_compressed
Proof state before:
case inr.inr
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := A }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : A.card = B.card
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
hgt : (B \ A).max' hV < (A \ B).max' hU
⊢ (B \ A).max' hV < (A \ B).max' hU
Tactic:
assumption
Proof state after:
no goals
Theorem: Finset.UV.familyMeasure_compression_lt_familyMeasure
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : 𝓒 U V 𝒜 ≠ 𝒜
⊢ Finset.UV.familyMeasure (𝓒 U V 𝒜) < Finset.UV.familyMeasure 𝒜
Tactic:
rw [compression] at a ⊢
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
⊢ Finset.UV.familyMeasure (filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜)) <
    Finset.UV.familyMeasure 𝒜
Theorem: Finset.UV.familyMeasure_compression_lt_familyMeasure
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
⊢ Finset.UV.familyMeasure (filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜)) <
    Finset.UV.familyMeasure 𝒜
Tactic:
have q : ∀ Q ∈ 𝒜.filter fun A ↦ compress U V A ∉ 𝒜, compress U V Q ≠ Q := by
  simp_rw [mem_filter]
  intro Q hQ h
  rw [h] at hQ
  exact hQ.2 hQ.1
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
q : ∀ Q ∈ filter (fun A => compress U V A ∉ 𝒜) 𝒜, compress U V Q ≠ Q
⊢ Finset.UV.familyMeasure (filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜)) <
    Finset.UV.familyMeasure 𝒜
Theorem: Finset.UV.familyMeasure_compression_lt_familyMeasure
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
q : ∀ Q ∈ filter (fun A => compress U V A ∉ 𝒜) 𝒜, compress U V Q ≠ Q
⊢ Finset.UV.familyMeasure (filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜)) <
    Finset.UV.familyMeasure 𝒜
Tactic:
have uA : (𝒜.filter fun A => compress U V A ∈ 𝒜) ∪ 𝒜.filter (fun A ↦ compress U V A ∉ 𝒜) = 𝒜 :=
  filter_union_filter_neg_eq _ _
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
q : ∀ Q ∈ filter (fun A => compress U V A ∉ 𝒜) 𝒜, compress U V Q ≠ Q
uA : filter (fun A => compress U V A ∈ 𝒜) 𝒜 ∪ filter (fun A => compress U V A ∉ 𝒜) 𝒜 = 𝒜
⊢ Finset.UV.familyMeasure (filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜)) <
    Finset.UV.familyMeasure 𝒜
Theorem: Finset.UV.familyMeasure_compression_lt_familyMeasure
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
q : ∀ Q ∈ filter (fun A => compress U V A ∉ 𝒜) 𝒜, compress U V Q ≠ Q
uA : filter (fun A => compress U V A ∈ 𝒜) 𝒜 ∪ filter (fun A => compress U V A ∉ 𝒜) 𝒜 = 𝒜
⊢ Finset.UV.familyMeasure (filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜)) <
    Finset.UV.familyMeasure 𝒜
Tactic:
have ne₂ : (𝒜.filter fun A ↦ compress U V A ∉ 𝒜).Nonempty := by
  refine' nonempty_iff_ne_empty.2 fun z ↦ a _
  rw [filter_image, z, image_empty, union_empty]
  rwa [z, union_empty] at uA
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
q : ∀ Q ∈ filter (fun A => compress U V A ∉ 𝒜) 𝒜, compress U V Q ≠ Q
uA : filter (fun A => compress U V A ∈ 𝒜) 𝒜 ∪ filter (fun A => compress U V A ∉ 𝒜) 𝒜 = 𝒜
ne₂ : (filter (fun A => compress U V A ∉ 𝒜) 𝒜).Nonempty
⊢ Finset.UV.familyMeasure (filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜)) <
    Finset.UV.familyMeasure 𝒜
Theorem: Finset.UV.familyMeasure_compression_lt_familyMeasure
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
q : ∀ Q ∈ filter (fun A => compress U V A ∉ 𝒜) 𝒜, compress U V Q ≠ Q
uA : filter (fun A => compress U V A ∈ 𝒜) 𝒜 ∪ filter (fun A => compress U V A ∉ 𝒜) 𝒜 = 𝒜
ne₂ : (filter (fun A => compress U V A ∉ 𝒜) 𝒜).Nonempty
⊢ Finset.UV.familyMeasure (filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜)) <
    Finset.UV.familyMeasure 𝒜
Tactic:
rw [familyMeasure, familyMeasure, sum_union compress_disjoint]
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
q : ∀ Q ∈ filter (fun A => compress U V A ∉ 𝒜) 𝒜, compress U V Q ≠ Q
uA : filter (fun A => compress U V A ∈ 𝒜) 𝒜 ∪ filter (fun A => compress U V A ∉ 𝒜) 𝒜 = 𝒜
ne₂ : (filter (fun A => compress U V A ∉ 𝒜) 𝒜).Nonempty
⊢ ∑ x ∈ filter (fun x => compress U V x ∈ 𝒜) 𝒜, ∑ a ∈ x, 2 ^ ↑a +
      ∑ x ∈ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜), ∑ a ∈ x, 2 ^ ↑a <
    ∑ A ∈ 𝒜, ∑ a ∈ A, 2 ^ ↑a
Theorem: Finset.UV.familyMeasure_compression_lt_familyMeasure
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
q : ∀ Q ∈ filter (fun A => compress U V A ∉ 𝒜) 𝒜, compress U V Q ≠ Q
uA : filter (fun A => compress U V A ∈ 𝒜) 𝒜 ∪ filter (fun A => compress U V A ∉ 𝒜) 𝒜 = 𝒜
ne₂ : (filter (fun A => compress U V A ∉ 𝒜) 𝒜).Nonempty
⊢ ∑ x ∈ filter (fun x => compress U V x ∈ 𝒜) 𝒜, ∑ a ∈ x, 2 ^ ↑a +
      ∑ x ∈ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜), ∑ a ∈ x, 2 ^ ↑a <
    ∑ A ∈ 𝒜, ∑ a ∈ A, 2 ^ ↑a
Tactic:
conv_rhs => rw [← uA]
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
q : ∀ Q ∈ filter (fun A => compress U V A ∉ 𝒜) 𝒜, compress U V Q ≠ Q
uA : filter (fun A => compress U V A ∈ 𝒜) 𝒜 ∪ filter (fun A => compress U V A ∉ 𝒜) 𝒜 = 𝒜
ne₂ : (filter (fun A => compress U V A ∉ 𝒜) 𝒜).Nonempty
⊢ ∑ x ∈ filter (fun x => compress U V x ∈ 𝒜) 𝒜, ∑ a ∈ x, 2 ^ ↑a +
      ∑ x ∈ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜), ∑ a ∈ x, 2 ^ ↑a <
    ∑ A ∈ filter (fun A => compress U V A ∈ 𝒜) 𝒜 ∪ filter (fun A => compress U V A ∉ 𝒜) 𝒜, ∑ a ∈ A, 2 ^ ↑a
Theorem: Finset.UV.familyMeasure_compression_lt_familyMeasure
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
q : ∀ Q ∈ filter (fun A => compress U V A ∉ 𝒜) 𝒜, compress U V Q ≠ Q
uA : filter (fun A => compress U V A ∈ 𝒜) 𝒜 ∪ filter (fun A => compress U V A ∉ 𝒜) 𝒜 = 𝒜
ne₂ : (filter (fun A => compress U V A ∉ 𝒜) 𝒜).Nonempty
⊢ ∑ x ∈ filter (fun x => compress U V x ∈ 𝒜) 𝒜, ∑ a ∈ x, 2 ^ ↑a +
      ∑ x ∈ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜), ∑ a ∈ x, 2 ^ ↑a <
    ∑ A ∈ filter (fun A => compress U V A ∈ 𝒜) 𝒜 ∪ filter (fun A => compress U V A ∉ 𝒜) 𝒜, ∑ a ∈ A, 2 ^ ↑a
Tactic:
rw [sum_union (disjoint_filter_filter_neg _ _ _), add_lt_add_iff_left, filter_image,
  sum_image compress_injOn]
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
q : ∀ Q ∈ filter (fun A => compress U V A ∉ 𝒜) 𝒜, compress U V Q ≠ Q
uA : filter (fun A => compress U V A ∈ 𝒜) 𝒜 ∪ filter (fun A => compress U V A ∉ 𝒜) 𝒜 = 𝒜
ne₂ : (filter (fun A => compress U V A ∉ 𝒜) 𝒜).Nonempty
⊢ ∑ x ∈ filter (fun x => compress U V x ∉ 𝒜) 𝒜, ∑ a ∈ compress U V x, 2 ^ ↑a <
    ∑ x ∈ filter (fun a => compress U V a ∉ 𝒜) 𝒜, ∑ a ∈ x, 2 ^ ↑a
Theorem: Finset.UV.familyMeasure_compression_lt_familyMeasure
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
q : ∀ Q ∈ filter (fun A => compress U V A ∉ 𝒜) 𝒜, compress U V Q ≠ Q
uA : filter (fun A => compress U V A ∈ 𝒜) 𝒜 ∪ filter (fun A => compress U V A ∉ 𝒜) 𝒜 = 𝒜
ne₂ : (filter (fun A => compress U V A ∉ 𝒜) 𝒜).Nonempty
⊢ ∑ x ∈ filter (fun x => compress U V x ∉ 𝒜) 𝒜, ∑ a ∈ compress U V x, 2 ^ ↑a <
    ∑ x ∈ filter (fun a => compress U V a ∉ 𝒜) 𝒜, ∑ a ∈ x, 2 ^ ↑a
Tactic:
refine' sum_lt_sum_of_nonempty ne₂ fun A hA ↦ _
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
q : ∀ Q ∈ filter (fun A => compress U V A ∉ 𝒜) 𝒜, compress U V Q ≠ Q
uA : filter (fun A => compress U V A ∈ 𝒜) 𝒜 ∪ filter (fun A => compress U V A ∉ 𝒜) 𝒜 = 𝒜
ne₂ : (filter (fun A => compress U V A ∉ 𝒜) 𝒜).Nonempty
A : Finset (Fin n)
hA : A ∈ filter (fun x => compress U V x ∉ 𝒜) 𝒜
⊢ ∑ a ∈ compress U V A, 2 ^ ↑a < ∑ a ∈ A, 2 ^ ↑a
Theorem: Finset.UV.familyMeasure_compression_lt_familyMeasure
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
q : ∀ Q ∈ filter (fun A => compress U V A ∉ 𝒜) 𝒜, compress U V Q ≠ Q
uA : filter (fun A => compress U V A ∈ 𝒜) 𝒜 ∪ filter (fun A => compress U V A ∉ 𝒜) 𝒜 = 𝒜
ne₂ : (filter (fun A => compress U V A ∉ 𝒜) 𝒜).Nonempty
A : Finset (Fin n)
hA : A ∈ filter (fun x => compress U V x ∉ 𝒜) 𝒜
⊢ ∑ a ∈ compress U V A, 2 ^ ↑a < ∑ a ∈ A, 2 ^ ↑a
Tactic:
simp_rw [← sum_image Fin.val_injective.injOn]
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
q : ∀ Q ∈ filter (fun A => compress U V A ∉ 𝒜) 𝒜, compress U V Q ≠ Q
uA : filter (fun A => compress U V A ∈ 𝒜) 𝒜 ∪ filter (fun A => compress U V A ∉ 𝒜) 𝒜 = 𝒜
ne₂ : (filter (fun A => compress U V A ∉ 𝒜) 𝒜).Nonempty
A : Finset (Fin n)
hA : A ∈ filter (fun x => compress U V x ∉ 𝒜) 𝒜
⊢ ∑ x ∈ image (fun x => ↑x) (compress U V A), 2 ^ x < ∑ x ∈ image (fun x => ↑x) A, 2 ^ x
Theorem: Finset.UV.familyMeasure_compression_lt_familyMeasure
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
q : ∀ Q ∈ filter (fun A => compress U V A ∉ 𝒜) 𝒜, compress U V Q ≠ Q
uA : filter (fun A => compress U V A ∈ 𝒜) 𝒜 ∪ filter (fun A => compress U V A ∉ 𝒜) 𝒜 = 𝒜
ne₂ : (filter (fun A => compress U V A ∉ 𝒜) 𝒜).Nonempty
A : Finset (Fin n)
hA : A ∈ filter (fun x => compress U V x ∉ 𝒜) 𝒜
⊢ ∑ x ∈ image (fun x => ↑x) (compress U V A), 2 ^ x < ∑ x ∈ image (fun x => ↑x) A, 2 ^ x
Tactic:
rw [geomSum_lt_geomSum_iff_toColex_lt_toColex le_rfl,
  toColex_image_lt_toColex_image Fin.val_strictMono]
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
q : ∀ Q ∈ filter (fun A => compress U V A ∉ 𝒜) 𝒜, compress U V Q ≠ Q
uA : filter (fun A => compress U V A ∈ 𝒜) 𝒜 ∪ filter (fun A => compress U V A ∉ 𝒜) 𝒜 = 𝒜
ne₂ : (filter (fun A => compress U V A ∉ 𝒜) 𝒜).Nonempty
A : Finset (Fin n)
hA : A ∈ filter (fun x => compress U V x ∉ 𝒜) 𝒜
⊢ { ofColex := compress U V A } < { ofColex := A }
Theorem: Finset.UV.familyMeasure_compression_lt_familyMeasure
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
q : ∀ Q ∈ filter (fun A => compress U V A ∉ 𝒜) 𝒜, compress U V Q ≠ Q
uA : filter (fun A => compress U V A ∈ 𝒜) 𝒜 ∪ filter (fun A => compress U V A ∉ 𝒜) 𝒜 = 𝒜
ne₂ : (filter (fun A => compress U V A ∉ 𝒜) 𝒜).Nonempty
A : Finset (Fin n)
hA : A ∈ filter (fun x => compress U V x ∉ 𝒜) 𝒜
⊢ { ofColex := compress U V A } < { ofColex := A }
Tactic:
exact toColex_compress_lt_toColex h $ q _ hA
Proof state after:
no goals
Theorem: Finset.UV.familyMeasure_compression_lt_familyMeasure
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
⊢ ∀ Q ∈ filter (fun A => compress U V A ∉ 𝒜) 𝒜, compress U V Q ≠ Q
Tactic:
simp_rw [mem_filter]
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
⊢ ∀ (Q : Finset (Fin n)), Q ∈ 𝒜 ∧ compress U V Q ∉ 𝒜 → compress U V Q ≠ Q
Theorem: Finset.UV.familyMeasure_compression_lt_familyMeasure
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
⊢ ∀ (Q : Finset (Fin n)), Q ∈ 𝒜 ∧ compress U V Q ∉ 𝒜 → compress U V Q ≠ Q
Tactic:
intro Q hQ h
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h✝ : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
Q : Finset (Fin n)
hQ : Q ∈ 𝒜 ∧ compress U V Q ∉ 𝒜
h : compress U V Q = Q
⊢ False
Theorem: Finset.UV.familyMeasure_compression_lt_familyMeasure
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h✝ : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
Q : Finset (Fin n)
hQ : Q ∈ 𝒜 ∧ compress U V Q ∉ 𝒜
h : compress U V Q = Q
⊢ False
Tactic:
rw [h] at hQ
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h✝ : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
Q : Finset (Fin n)
hQ : Q ∈ 𝒜 ∧ Q ∉ 𝒜
h : compress U V Q = Q
⊢ False
Theorem: Finset.UV.familyMeasure_compression_lt_familyMeasure
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h✝ : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
Q : Finset (Fin n)
hQ : Q ∈ 𝒜 ∧ Q ∉ 𝒜
h : compress U V Q = Q
⊢ False
Tactic:
exact hQ.2 hQ.1
Proof state after:
no goals
Theorem: Finset.UV.familyMeasure_compression_lt_familyMeasure
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
q : ∀ Q ∈ filter (fun A => compress U V A ∉ 𝒜) 𝒜, compress U V Q ≠ Q
uA : filter (fun A => compress U V A ∈ 𝒜) 𝒜 ∪ filter (fun A => compress U V A ∉ 𝒜) 𝒜 = 𝒜
⊢ (filter (fun A => compress U V A ∉ 𝒜) 𝒜).Nonempty
Tactic:
refine' nonempty_iff_ne_empty.2 fun z ↦ a _
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
q : ∀ Q ∈ filter (fun A => compress U V A ∉ 𝒜) 𝒜, compress U V Q ≠ Q
uA : filter (fun A => compress U V A ∈ 𝒜) 𝒜 ∪ filter (fun A => compress U V A ∉ 𝒜) 𝒜 = 𝒜
z : filter (fun A => compress U V A ∉ 𝒜) 𝒜 = ∅
⊢ filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) = 𝒜
Theorem: Finset.UV.familyMeasure_compression_lt_familyMeasure
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
q : ∀ Q ∈ filter (fun A => compress U V A ∉ 𝒜) 𝒜, compress U V Q ≠ Q
uA : filter (fun A => compress U V A ∈ 𝒜) 𝒜 ∪ filter (fun A => compress U V A ∉ 𝒜) 𝒜 = 𝒜
z : filter (fun A => compress U V A ∉ 𝒜) 𝒜 = ∅
⊢ filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) = 𝒜
Tactic:
rw [filter_image, z, image_empty, union_empty]
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
q : ∀ Q ∈ filter (fun A => compress U V A ∉ 𝒜) 𝒜, compress U V Q ≠ Q
uA : filter (fun A => compress U V A ∈ 𝒜) 𝒜 ∪ filter (fun A => compress U V A ∉ 𝒜) 𝒜 = 𝒜
z : filter (fun A => compress U V A ∉ 𝒜) 𝒜 = ∅
⊢ filter (fun x => compress U V x ∈ 𝒜) 𝒜 = 𝒜
Theorem: Finset.UV.familyMeasure_compression_lt_familyMeasure
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
q : ∀ Q ∈ filter (fun A => compress U V A ∉ 𝒜) 𝒜, compress U V Q ≠ Q
uA : filter (fun A => compress U V A ∈ 𝒜) 𝒜 ∪ filter (fun A => compress U V A ∉ 𝒜) 𝒜 = 𝒜
z : filter (fun A => compress U V A ∉ 𝒜) 𝒜 = ∅
⊢ filter (fun x => compress U V x ∈ 𝒜) 𝒜 = 𝒜
Tactic:
rwa [z, union_empty] at uA
Proof state after:
no goals
Theorem: Finset.UV.kruskal_katona_helper
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r ↑𝒜
⊢ ∃ ℬ,
    (∂ ℬ).card ≤ (∂ 𝒜).card ∧
      𝒜.card = ℬ.card ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
Tactic:
revert h
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r : ℕ
𝒜 : Finset (Finset (Fin n))
⊢ Set.Sized r ↑𝒜 →
    ∃ ℬ,
      (∂ ℬ).card ≤ (∂ 𝒜).card ∧
        𝒜.card = ℬ.card ∧
          Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ