-- Mathlib/Combinatorics/SetFamily/KruskalKatona.lean
/-- Applying a compression strictly decreases the measure. This helps show that "compress until we
can't any more" is a terminating process. -/
private lemma familyMeasure_compression_lt_familyMeasure {U V : Finset (Fin n)} {hU : U.Nonempty}
    {hV : V.Nonempty} (h : max' U hU < max' V hV) {𝒜 : Finset (Finset (Fin n))} (a : 𝓒 U V 𝒜 ≠ 𝒜) :
    familyMeasure (𝓒 U V 𝒜) < familyMeasure 𝒜

Proof state:
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 a => compress U V a ∈ 𝒜) 𝒜 ∪ filter (fun a => a ∉ 𝒜) (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 a => compress U V a ∈ 𝒜) 𝒜 ∪ filter (fun a => a ∉ 𝒜) (image (compress U V) 𝒜)) <
    Finset.UV.familyMeasure 𝒜

Tactic:
rw [familyMeasure, familyMeasure, sum_union compress_disjoint]

Result:
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 a => compress U V a ∈ 𝒜) 𝒜 ∪ filter (fun a => a ∉ 𝒜) (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 a => compress U V a ∈ 𝒜) 𝒜, ∑ a ∈ x, 2 ^ ↑a +
      ∑ x ∈ filter (fun a => a ∉ 𝒜) (image (compress U V) 𝒜), ∑ a ∈ x, 2 ^ ↑a <
    ∑ A ∈ 𝒜, ∑ a ∈ A, 2 ^ ↑a

Proof state:
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 a => compress U V a ∈ 𝒜) 𝒜 ∪ filter (fun a => a ∉ 𝒜) (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 a => compress U V a ∈ 𝒜) 𝒜, ∑ a ∈ x, 2 ^ ↑a +
      ∑ x ∈ filter (fun a => a ∉ 𝒜) (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]

Result:
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 a => compress U V a ∈ 𝒜) 𝒜 ∪ filter (fun a => a ∉ 𝒜) (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 a => compress U V a ∉ 𝒜) 𝒜, ∑ a ∈ compress U V x, 2 ^ ↑a <
    ∑ x ∈ filter (fun a => compress U V a ∉ 𝒜) 𝒜, ∑ a ∈ x, 2 ^ ↑a

Proof state:
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 a => compress U V a ∈ 𝒜) 𝒜 ∪ filter (fun a => a ∉ 𝒜) (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 a => compress U V a ∉ 𝒜) 𝒜, ∑ 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 ↦ ?_

Result:
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 a => compress U V a ∈ 𝒜) 𝒜 ∪ filter (fun a => a ∉ 𝒜) (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 a => compress U V a ∉ 𝒜) 𝒜
⊢ ∑ a ∈ compress U V A, 2 ^ ↑a < ∑ a ∈ A, 2 ^ ↑a

Proof state:
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 a => compress U V a ∈ 𝒜) 𝒜 ∪ filter (fun a => a ∉ 𝒜) (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 a => compress U V a ∈ 𝒜) 𝒜 ∪ filter (fun a => a ∉ 𝒜) (image (compress U V) 𝒜)) <
    Finset.UV.familyMeasure 𝒜

Tactic:
have ne₂ : {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

Result:
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 a => compress U V a ∈ 𝒜) 𝒜 ∪ filter (fun a => a ∉ 𝒜) (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 a => compress U V a ∈ 𝒜) 𝒜 ∪ filter (fun a => a ∉ 𝒜) (image (compress U V) 𝒜)) <
    Finset.UV.familyMeasure 𝒜

Proof state:
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 a => compress U V a ∈ 𝒜) 𝒜 ∪ filter (fun a => a ∉ 𝒜) (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 ?_

Result:
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 a => compress U V a ∈ 𝒜) 𝒜 ∪ filter (fun a => a ∉ 𝒜) (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 a => compress U V a ∈ 𝒜) 𝒜 ∪ filter (fun a => a ∉ 𝒜) (image (compress U V) 𝒜) = 𝒜

Proof state:
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 a => compress U V a ∈ 𝒜) 𝒜 ∪ filter (fun a => a ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
q : ∀ Q ∈ filter (fun A => compress U V A ∉ 𝒜) 𝒜, compress U V Q ≠ Q
⊢ Finset.UV.familyMeasure (filter (fun a => compress U V a ∈ 𝒜) 𝒜 ∪ filter (fun a => a ∉ 𝒜) (image (compress U V) 𝒜)) <
    Finset.UV.familyMeasure 𝒜

Tactic:
have uA : {A ∈ 𝒜 | compress U V A ∈ 𝒜} ∪ {A ∈ 𝒜 | compress U V A ∉ 𝒜} = 𝒜 :=
  filter_union_filter_neg_eq _ _

Result:
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 a => compress U V a ∈ 𝒜) 𝒜 ∪ filter (fun a => a ∉ 𝒜) (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 a => compress U V a ∈ 𝒜) 𝒜 ∪ filter (fun a => a ∉ 𝒜) (image (compress U V) 𝒜)) <
    Finset.UV.familyMeasure 𝒜