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

Tactic:
conv_rhs => rw [← 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
⊢ ∑ 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

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 : Finset (Fin n)
hQ : Q ∈ 𝒜 ∧ compress U V Q ∉ 𝒜
h : compress U V Q = Q
⊢ False

Tactic:
rw [h] at hQ

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 : Finset (Fin n)
hQ : Q ∈ 𝒜 ∧ Q ∉ 𝒜
h : compress U V Q = Q
⊢ False

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
A : Finset (Fin n)
hA : A ∈ filter (fun a => compress U V a ∉ 𝒜) 𝒜
⊢ ∑ x ∈ image Fin.val (compress U V A), 2 ^ x < ∑ x ∈ image Fin.val A, 2 ^ x

Tactic:
rw [geomSum_lt_geomSum_iff_toColex_lt_toColex le_rfl,
  toColex_image_lt_toColex_image Fin.val_strictMono]

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 ∉ 𝒜) 𝒜
⊢ { ofColex := compress U V A } < { ofColex := 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) 𝒜) ≠ 𝒜
⊢ Finset.UV.familyMeasure (filter (fun a => compress U V a ∈ 𝒜) 𝒜 ∪ filter (fun a => a ∉ 𝒜) (image (compress U V) 𝒜)) <
    Finset.UV.familyMeasure 𝒜

Tactic:
have q : ∀ Q ∈ {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

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
⊢ 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 : 𝓒 U V 𝒜 ≠ 𝒜
⊢ Finset.UV.familyMeasure (𝓒 U V 𝒜) < Finset.UV.familyMeasure 𝒜

Tactic:
rw [compression] at 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) 𝒜) ≠ 𝒜
⊢ 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 : Finset (Fin n)
hQ : Q ∈ 𝒜 ∧ Q ∉ 𝒜
h : compress U V Q = Q
⊢ False

Tactic:
exact hQ.2 hQ.1

Result:
no goals

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

Tactic:
rw [filter_image, z, image_empty, union_empty]

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

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
A : Finset (Fin n)
hA : A ∈ filter (fun a => compress U V a ∉ 𝒜) 𝒜
⊢ { ofColex := compress U V A } < { ofColex := A }

Tactic:
exact toColex_compress_lt_toColex h <| q _ hA

Result:
no goals

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 ∉ 𝒜) 𝒜 = 𝒜
z : filter (fun A => compress U V A ∉ 𝒜) 𝒜 = ∅
⊢ filter (fun a => compress U V a ∈ 𝒜) 𝒜 = 𝒜

Tactic:
rwa [z, union_empty] at uA

Result:
no goals