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

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₁ : Finset.UV.UsefulCompression U V
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
⊢ (∂ (𝓒 U V 𝒜)).card ≤ (∂ 𝒜).card
Tactic:
obtain ⟨UVd, same_size, hU, hV, max_lt⟩ := h₁
State after:
case intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : U.card = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
⊢ (∂ (𝓒 U V 𝒜)).card ≤ (∂ 𝒜).card

State before:
case intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : U.card = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
⊢ (∂ (𝓒 U V 𝒜)).card ≤ (∂ 𝒜).card
Tactic:
refine' card_shadow_compression_le _ _ fun x Hx ↦ ⟨min' V hV, min'_mem _ _, _⟩
State after:
case intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : U.card = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
⊢ IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜

State before:
case intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : U.card = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
⊢ IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜
Tactic:
obtain hU' | hU' := eq_or_lt_of_le (succ_le_iff.2 hU.card_pos)
State after:
case intro.intro.intro.intro.inl
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : U.card = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 = U.card
⊢ IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜

case intro.intro.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : U.card = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 < U.card
⊢ IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜

State before:
case intro.intro.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : U.card = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 < U.card
⊢ IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜
Tactic:
refine' h₂ ⟨UVd.mono (erase_subset _ _) (erase_subset _ _), _, _, _, _⟩ (card_erase_lt_of_mem Hx)
State after:
case intro.intro.intro.intro.inr.refine'_1
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : U.card = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 < U.card
⊢ (U.erase x).card = (V.erase (V.min' hV)).card

case intro.intro.intro.intro.inr.refine'_2
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : U.card = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 < U.card
⊢ (U.erase x).Nonempty

case intro.intro.intro.intro.inr.refine'_3
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : U.card = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 < U.card
⊢ (V.erase (V.min' hV)).Nonempty

case intro.intro.intro.intro.inr.refine'_4
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : U.card = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 < U.card
⊢ (U.erase x).max' ?intro.intro.intro.intro.inr.refine'_2 <
    (V.erase (V.min' hV)).max' ?intro.intro.intro.intro.inr.refine'_3

State before:
case intro.intro.intro.intro.inl
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : U.card = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 = U.card
⊢ IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜
Tactic:
rw [← hU'] at same_size
State after:
case intro.intro.intro.intro.inl
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : succ 0 = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 = U.card
⊢ IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜

State before:
case intro.intro.intro.intro.inl
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : succ 0 = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 = U.card
⊢ IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜
Tactic:
have : erase U x = ∅ := by rw [← Finset.card_eq_zero, card_erase_of_mem Hx, ← hU']
State after:
case intro.intro.intro.intro.inl
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : succ 0 = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 = U.card
this : U.erase x = ∅
⊢ IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜

State before:
case intro.intro.intro.intro.inl
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : succ 0 = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 = U.card
this : U.erase x = ∅
⊢ IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜
Tactic:
have : erase V (min' V hV) = ∅ := by
  rw [← Finset.card_eq_zero, card_erase_of_mem (min'_mem _ _), ← same_size]
State after:
case intro.intro.intro.intro.inl
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : succ 0 = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 = U.card
this✝ : U.erase x = ∅
this : V.erase (V.min' hV) = ∅
⊢ IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜

State before:
case intro.intro.intro.intro.inl
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : succ 0 = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 = U.card
this✝ : U.erase x = ∅
this : V.erase (V.min' hV) = ∅
⊢ IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜
Tactic:
rw [‹erase U x = ∅›, ‹erase V (min' V hV) = ∅›]
State after:
case intro.intro.intro.intro.inl
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : succ 0 = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 = U.card
this✝ : U.erase x = ∅
this : V.erase (V.min' hV) = ∅
⊢ IsCompressed ∅ ∅ 𝒜

State before:
case intro.intro.intro.intro.inl
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : succ 0 = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 = U.card
this✝ : U.erase x = ∅
this : V.erase (V.min' hV) = ∅
⊢ IsCompressed ∅ ∅ 𝒜
Tactic:
exact isCompressed_self _ _
State after:
no goals

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : succ 0 = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 = U.card
⊢ U.erase x = ∅
Tactic:
rw [← Finset.card_eq_zero, card_erase_of_mem Hx, ← hU']
State after:
no goals

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : succ 0 = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 = U.card
this : U.erase x = ∅
⊢ V.erase (V.min' hV) = ∅
Tactic:
rw [← Finset.card_eq_zero, card_erase_of_mem (min'_mem _ _), ← same_size]
State after:
no goals

State before:
case intro.intro.intro.intro.inr.refine'_1
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : U.card = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 < U.card
⊢ (U.erase x).card = (V.erase (V.min' hV)).card
Tactic:
rw [card_erase_of_mem (min'_mem _ _), card_erase_of_mem Hx, same_size]
State after:
no goals

State before:
case intro.intro.intro.intro.inr.refine'_2
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : U.card = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 < U.card
⊢ (U.erase x).Nonempty
Tactic:
rwa [← card_pos, card_erase_of_mem Hx, tsub_pos_iff_lt]
State after:
no goals

State before:
case intro.intro.intro.intro.inr.refine'_3
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : U.card = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 < U.card
⊢ (V.erase (V.min' hV)).Nonempty
Tactic:
rwa [← Finset.card_pos, card_erase_of_mem (min'_mem _ _), ← same_size, tsub_pos_iff_lt]
State after:
no goals

State before:
case intro.intro.intro.intro.inr.refine'_4
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : U.card = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 < U.card
⊢ (U.erase x).max' ⋯ < (V.erase (V.min' hV)).max' ⋯
Tactic:
refine' (Finset.max'_subset _ $ erase_subset _ _).trans_lt (max_lt.trans_le $
  le_max' _ _ $ mem_erase.2 ⟨(min'_lt_max'_of_card _ _).ne', max'_mem _ _⟩)
State after:
case intro.intro.intro.intro.inr.refine'_4
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : U.card = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 < U.card
⊢ 1 < V.card

State before:
case intro.intro.intro.intro.inr.refine'_4
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : U.card = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 < U.card
⊢ 1 < V.card
Tactic:
rwa [← same_size]
State after:
no goals