Theorem: Finset.UV.familyMeasure_compression_lt_familyMeasure (LeanCamCombi/KruskalKatona.lean)

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 ⊢
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 𝒜

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
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 𝒜

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 _ _
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 𝒜

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
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 𝒜

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]
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

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]
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

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]
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

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 ↦ _
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

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]
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

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]
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 }

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
State after:
no goals

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]
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

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
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

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
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

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
State after:
no goals

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 _
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) 𝒜) = 𝒜

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]
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 ∈ 𝒜) 𝒜 = 𝒜

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
State after:
no goals