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

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

State before:
α : 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 ℬ
Tactic:
apply WellFounded.recursion (InvImage.wf familyMeasure wellFounded_lt) 𝒜
State after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r : ℕ
𝒜 : Finset (Finset (Fin n))
⊢ ∀ (x : Finset (Finset (Fin n))),
    (∀ (y : Finset (Finset (Fin n))),
        InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y x →
          Set.Sized r ↑y →
            ∃ ℬ,
              (∂ ℬ).card ≤ (∂ y).card ∧
                y.card = ℬ.card ∧
                  Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ) →
      Set.Sized r ↑x →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ x).card ∧
            x.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r : ℕ
𝒜 : Finset (Finset (Fin n))
⊢ ∀ (x : Finset (Finset (Fin n))),
    (∀ (y : Finset (Finset (Fin n))),
        InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y x →
          Set.Sized r ↑y →
            ∃ ℬ,
              (∂ ℬ).card ≤ (∂ y).card ∧
                y.card = ℬ.card ∧
                  Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ) →
      Set.Sized r ↑x →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ x).card ∧
            x.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
Tactic:
intro A ih h
State after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
⊢ ∃ ℬ,
    (∂ ℬ).card ≤ (∂ A).card ∧
      A.card = ℬ.card ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
⊢ ∃ ℬ,
    (∂ ℬ).card ≤ (∂ A).card ∧
      A.card = ℬ.card ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
Tactic:
set usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  univ.filter fun t ↦ UsefulCompression t.1 t.2 ∧ ¬ IsCompressed t.1 t.2 A
State after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
⊢ ∃ ℬ,
    (∂ ℬ).card ≤ (∂ A).card ∧
      A.card = ℬ.card ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
⊢ ∃ ℬ,
    (∂ ℬ).card ≤ (∂ A).card ∧
      A.card = ℬ.card ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
Tactic:
obtain husable | husable := usable.eq_empty_or_nonempty
State after:
case inl
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable = ∅
⊢ ∃ ℬ,
    (∂ ℬ).card ≤ (∂ A).card ∧
      A.card = ℬ.card ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ

case inr
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable.Nonempty
⊢ ∃ ℬ,
    (∂ ℬ).card ≤ (∂ A).card ∧
      A.card = ℬ.card ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ

State before:
case inr
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable.Nonempty
⊢ ∃ ℬ,
    (∂ ℬ).card ≤ (∂ A).card ∧
      A.card = ℬ.card ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
Tactic:
obtain ⟨⟨U, V⟩, hUV, t⟩ := exists_min_image usable (fun t ↦ t.1.card) husable
State after:
case inr.intro.mk.intro
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable.Nonempty
U V : Finset (Fin n)
hUV : (U, V) ∈ usable
t : ∀ x' ∈ usable, (U, V).1.card ≤ x'.1.card
⊢ ∃ ℬ,
    (∂ ℬ).card ≤ (∂ A).card ∧
      A.card = ℬ.card ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ

State before:
case inr.intro.mk.intro
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable.Nonempty
U V : Finset (Fin n)
hUV : (U, V) ∈ usable
t : ∀ x' ∈ usable, (U, V).1.card ≤ x'.1.card
⊢ ∃ ℬ,
    (∂ ℬ).card ≤ (∂ A).card ∧
      A.card = ℬ.card ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
Tactic:
rw [mem_filter] at hUV
State after:
case inr.intro.mk.intro
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable.Nonempty
U V : Finset (Fin n)
hUV : (U, V) ∈ univ ∧ Finset.UV.UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 A
t : ∀ x' ∈ usable, (U, V).1.card ≤ x'.1.card
⊢ ∃ ℬ,
    (∂ ℬ).card ≤ (∂ A).card ∧
      A.card = ℬ.card ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ

State before:
case inr.intro.mk.intro
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable.Nonempty
U V : Finset (Fin n)
hUV : (U, V) ∈ univ ∧ Finset.UV.UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 A
t : ∀ x' ∈ usable, (U, V).1.card ≤ x'.1.card
⊢ ∃ ℬ,
    (∂ ℬ).card ≤ (∂ A).card ∧
      A.card = ℬ.card ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
Tactic:
have h₂ : ∀ U₁ V₁, UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ A := by
  rintro U₁ V₁ huseful hUcard
  by_contra h
  exact hUcard.not_le $ t ⟨U₁, V₁⟩ $ mem_filter.2 ⟨mem_univ _, huseful, h⟩
State after:
case inr.intro.mk.intro
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable.Nonempty
U V : Finset (Fin n)
hUV : (U, V) ∈ univ ∧ Finset.UV.UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 A
t : ∀ x' ∈ usable, (U, V).1.card ≤ x'.1.card
h₂ : ∀ (U₁ V₁ : Finset (Fin n)), Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ A
⊢ ∃ ℬ,
    (∂ ℬ).card ≤ (∂ A).card ∧
      A.card = ℬ.card ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ

State before:
case inr.intro.mk.intro
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable.Nonempty
U V : Finset (Fin n)
hUV : (U, V) ∈ univ ∧ Finset.UV.UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 A
t : ∀ x' ∈ usable, (U, V).1.card ≤ x'.1.card
h₂ : ∀ (U₁ V₁ : Finset (Fin n)), Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ A
⊢ ∃ ℬ,
    (∂ ℬ).card ≤ (∂ A).card ∧
      A.card = ℬ.card ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
Tactic:
have p1 : (∂ (𝓒 U V A)).card ≤ (∂ A).card := compression_improved _ hUV.2.1 h₂
State after:
case inr.intro.mk.intro
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable.Nonempty
U V : Finset (Fin n)
hUV : (U, V) ∈ univ ∧ Finset.UV.UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 A
t : ∀ x' ∈ usable, (U, V).1.card ≤ x'.1.card
h₂ : ∀ (U₁ V₁ : Finset (Fin n)), Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ A
p1 : (∂ (𝓒 U V A)).card ≤ (∂ A).card
⊢ ∃ ℬ,
    (∂ ℬ).card ≤ (∂ A).card ∧
      A.card = ℬ.card ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ

State before:
case inr.intro.mk.intro
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable.Nonempty
U V : Finset (Fin n)
hUV : (U, V) ∈ univ ∧ Finset.UV.UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 A
t : ∀ x' ∈ usable, (U, V).1.card ≤ x'.1.card
h₂ : ∀ (U₁ V₁ : Finset (Fin n)), Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ A
p1 : (∂ (𝓒 U V A)).card ≤ (∂ A).card
⊢ ∃ ℬ,
    (∂ ℬ).card ≤ (∂ A).card ∧
      A.card = ℬ.card ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
Tactic:
obtain ⟨-, hUV', hu, hv, hmax⟩ := hUV.2.1
State after:
case inr.intro.mk.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable.Nonempty
U V : Finset (Fin n)
hUV : (U, V) ∈ univ ∧ Finset.UV.UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 A
t : ∀ x' ∈ usable, (U, V).1.card ≤ x'.1.card
h₂ : ∀ (U₁ V₁ : Finset (Fin n)), Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ A
p1 : (∂ (𝓒 U V A)).card ≤ (∂ A).card
hUV' : (U, V).1.card = (U, V).2.card
hu : (U, V).1.Nonempty
hv : (U, V).2.Nonempty
hmax : (U, V).1.max' hu < (U, V).2.max' hv
⊢ ∃ ℬ,
    (∂ ℬ).card ≤ (∂ A).card ∧
      A.card = ℬ.card ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ

State before:
case inr.intro.mk.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable.Nonempty
U V : Finset (Fin n)
hUV : (U, V) ∈ univ ∧ Finset.UV.UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 A
t : ∀ x' ∈ usable, (U, V).1.card ≤ x'.1.card
h₂ : ∀ (U₁ V₁ : Finset (Fin n)), Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ A
p1 : (∂ (𝓒 U V A)).card ≤ (∂ A).card
hUV' : (U, V).1.card = (U, V).2.card
hu : (U, V).1.Nonempty
hv : (U, V).2.Nonempty
hmax : (U, V).1.max' hu < (U, V).2.max' hv
⊢ ∃ ℬ,
    (∂ ℬ).card ≤ (∂ A).card ∧
      A.card = ℬ.card ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
Tactic:
unfold InvImage at ih
State after:
case inr.intro.mk.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    (fun x x_1 => x < x_1) (Finset.UV.familyMeasure y) (Finset.UV.familyMeasure A) →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable.Nonempty
U V : Finset (Fin n)
hUV : (U, V) ∈ univ ∧ Finset.UV.UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 A
t : ∀ x' ∈ usable, (U, V).1.card ≤ x'.1.card
h₂ : ∀ (U₁ V₁ : Finset (Fin n)), Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ A
p1 : (∂ (𝓒 U V A)).card ≤ (∂ A).card
hUV' : (U, V).1.card = (U, V).2.card
hu : (U, V).1.Nonempty
hv : (U, V).2.Nonempty
hmax : (U, V).1.max' hu < (U, V).2.max' hv
⊢ ∃ ℬ,
    (∂ ℬ).card ≤ (∂ A).card ∧
      A.card = ℬ.card ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ

State before:
case inr.intro.mk.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    (fun x x_1 => x < x_1) (Finset.UV.familyMeasure y) (Finset.UV.familyMeasure A) →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable.Nonempty
U V : Finset (Fin n)
hUV : (U, V) ∈ univ ∧ Finset.UV.UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 A
t : ∀ x' ∈ usable, (U, V).1.card ≤ x'.1.card
h₂ : ∀ (U₁ V₁ : Finset (Fin n)), Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ A
p1 : (∂ (𝓒 U V A)).card ≤ (∂ A).card
hUV' : (U, V).1.card = (U, V).2.card
hu : (U, V).1.Nonempty
hv : (U, V).2.Nonempty
hmax : (U, V).1.max' hu < (U, V).2.max' hv
⊢ ∃ ℬ,
    (∂ ℬ).card ≤ (∂ A).card ∧
      A.card = ℬ.card ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
Tactic:
obtain ⟨t, q1, q2, q3, q4⟩ := ih (𝓒 U V A)
  (familyMeasure_compression_lt_familyMeasure hmax hUV.2.2) (h.uvCompression hUV')
State after:
case inr.intro.mk.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    (fun x x_1 => x < x_1) (Finset.UV.familyMeasure y) (Finset.UV.familyMeasure A) →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable.Nonempty
U V : Finset (Fin n)
hUV : (U, V) ∈ univ ∧ Finset.UV.UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 A
t✝ : ∀ x' ∈ usable, (U, V).1.card ≤ x'.1.card
h₂ : ∀ (U₁ V₁ : Finset (Fin n)), Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ A
p1 : (∂ (𝓒 U V A)).card ≤ (∂ A).card
hUV' : (U, V).1.card = (U, V).2.card
hu : (U, V).1.Nonempty
hv : (U, V).2.Nonempty
hmax : (U, V).1.max' hu < (U, V).2.max' hv
t : Finset (Finset (Fin n))
q1 : (∂ t).card ≤ (∂ (𝓒 U V A)).card
q2 : (𝓒 U V A).card = t.card
q3 : Set.Sized r ↑t
q4 : ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V t
⊢ ∃ ℬ,
    (∂ ℬ).card ≤ (∂ A).card ∧
      A.card = ℬ.card ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ

State before:
case inr.intro.mk.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    (fun x x_1 => x < x_1) (Finset.UV.familyMeasure y) (Finset.UV.familyMeasure A) →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable.Nonempty
U V : Finset (Fin n)
hUV : (U, V) ∈ univ ∧ Finset.UV.UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 A
t✝ : ∀ x' ∈ usable, (U, V).1.card ≤ x'.1.card
h₂ : ∀ (U₁ V₁ : Finset (Fin n)), Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ A
p1 : (∂ (𝓒 U V A)).card ≤ (∂ A).card
hUV' : (U, V).1.card = (U, V).2.card
hu : (U, V).1.Nonempty
hv : (U, V).2.Nonempty
hmax : (U, V).1.max' hu < (U, V).2.max' hv
t : Finset (Finset (Fin n))
q1 : (∂ t).card ≤ (∂ (𝓒 U V A)).card
q2 : (𝓒 U V A).card = t.card
q3 : Set.Sized r ↑t
q4 : ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V t
⊢ ∃ ℬ,
    (∂ ℬ).card ≤ (∂ A).card ∧
      A.card = ℬ.card ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
Tactic:
exact ⟨t, q1.trans p1, (card_compression _ _ _).symm.trans q2, q3, q4⟩
State after:
no goals

State before:
case inl
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable = ∅
⊢ ∃ ℬ,
    (∂ ℬ).card ≤ (∂ A).card ∧
      A.card = ℬ.card ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
Tactic:
refine' ⟨A, le_rfl, rfl, h, fun U V hUV ↦ _⟩
State after:
case inl
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable = ∅
U V : Finset (Fin n)
hUV : Finset.UV.UsefulCompression U V
⊢ IsCompressed U V A

State before:
case inl
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable = ∅
U V : Finset (Fin n)
hUV : Finset.UV.UsefulCompression U V
⊢ IsCompressed U V A
Tactic:
rw [eq_empty_iff_forall_not_mem] at husable
State after:
case inl
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : ∀ (x : Finset (Fin n) × Finset (Fin n)), x ∉ usable
U V : Finset (Fin n)
hUV : Finset.UV.UsefulCompression U V
⊢ IsCompressed U V A

State before:
case inl
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : ∀ (x : Finset (Fin n) × Finset (Fin n)), x ∉ usable
U V : Finset (Fin n)
hUV : Finset.UV.UsefulCompression U V
⊢ IsCompressed U V A
Tactic:
by_contra h
State after:
case inl
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h✝ : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : ∀ (x : Finset (Fin n) × Finset (Fin n)), x ∉ usable
U V : Finset (Fin n)
hUV : Finset.UV.UsefulCompression U V
h : ¬IsCompressed U V A
⊢ False

State before:
case inl
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h✝ : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : ∀ (x : Finset (Fin n) × Finset (Fin n)), x ∉ usable
U V : Finset (Fin n)
hUV : Finset.UV.UsefulCompression U V
h : ¬IsCompressed U V A
⊢ False
Tactic:
exact husable ⟨U, V⟩ $ mem_filter.2 ⟨mem_univ _, hUV, h⟩
State after:
no goals

State before:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable.Nonempty
U V : Finset (Fin n)
hUV : (U, V) ∈ univ ∧ Finset.UV.UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 A
t : ∀ x' ∈ usable, (U, V).1.card ≤ x'.1.card
⊢ ∀ (U₁ V₁ : Finset (Fin n)), Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ A
Tactic:
rintro U₁ V₁ huseful hUcard
State after:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable.Nonempty
U V : Finset (Fin n)
hUV : (U, V) ∈ univ ∧ Finset.UV.UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 A
t : ∀ x' ∈ usable, (U, V).1.card ≤ x'.1.card
U₁ V₁ : Finset (Fin n)
huseful : Finset.UV.UsefulCompression U₁ V₁
hUcard : U₁.card < U.card
⊢ IsCompressed U₁ V₁ A

State before:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable.Nonempty
U V : Finset (Fin n)
hUV : (U, V) ∈ univ ∧ Finset.UV.UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 A
t : ∀ x' ∈ usable, (U, V).1.card ≤ x'.1.card
U₁ V₁ : Finset (Fin n)
huseful : Finset.UV.UsefulCompression U₁ V₁
hUcard : U₁.card < U.card
⊢ IsCompressed U₁ V₁ A
Tactic:
by_contra h
State after:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h✝ : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable.Nonempty
U V : Finset (Fin n)
hUV : (U, V) ∈ univ ∧ Finset.UV.UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 A
t : ∀ x' ∈ usable, (U, V).1.card ≤ x'.1.card
U₁ V₁ : Finset (Fin n)
huseful : Finset.UV.UsefulCompression U₁ V₁
hUcard : U₁.card < U.card
h : ¬IsCompressed U₁ V₁ A
⊢ False

State before:
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h✝ : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable.Nonempty
U V : Finset (Fin n)
hUV : (U, V) ∈ univ ∧ Finset.UV.UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 A
t : ∀ x' ∈ usable, (U, V).1.card ≤ x'.1.card
U₁ V₁ : Finset (Fin n)
huseful : Finset.UV.UsefulCompression U₁ V₁
hUcard : U₁.card < U.card
h : ¬IsCompressed U₁ V₁ A
⊢ False
Tactic:
exact hUcard.not_le $ t ⟨U₁, V₁⟩ $ mem_filter.2 ⟨mem_univ _, huseful, h⟩
State after:
no goals