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

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
⊢ IsInitSeg ℬ r
Tactic:
refine' ⟨h₁, _⟩
State after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
⊢ ∀ ⦃s t : Finset α⦄, s ∈ ℬ → { ofColex := t } < { ofColex := s } ∧ t.card = r → t ∈ ℬ

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
⊢ ∀ ⦃s t : Finset α⦄, s ∈ ℬ → { ofColex := t } < { ofColex := s } ∧ t.card = r → t ∈ ℬ
Tactic:
rintro A B hA ⟨hBA, sizeA⟩
State after:
case intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := A }
sizeA : B.card = r
⊢ B ∈ ℬ

State before:
case intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := A }
sizeA : B.card = r
⊢ B ∈ ℬ
Tactic:
by_contra hB
State after:
case intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := A }
sizeA : B.card = r
hB : B ∉ ℬ
⊢ False

State before:
case intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := A }
sizeA : B.card = r
hB : B ∉ ℬ
⊢ False
Tactic:
have hAB : A ≠ B := ne_of_mem_of_not_mem hA hB
State after:
case intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := A }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : A ≠ B
⊢ False

State before:
case intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := A }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : A ≠ B
⊢ False
Tactic:
have hAB' : A.card = B.card := (h₁ hA).trans sizeA.symm
State after:
case intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := A }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : A.card = B.card
⊢ False

State before:
case intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := A }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : A.card = B.card
⊢ False
Tactic:
have hU : (A \ B).Nonempty := sdiff_nonempty.2 fun h ↦ hAB $ eq_of_subset_of_card_le h hAB'.ge
State after:
case intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := A }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : A.card = B.card
hU : (A \ B).Nonempty
⊢ False

State before:
case intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := A }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : A.card = B.card
hU : (A \ B).Nonempty
⊢ False
Tactic:
have hV : (B \ A).Nonempty :=
  sdiff_nonempty.2 fun h ↦ hAB.symm $ eq_of_subset_of_card_le h hAB'.le
State after:
case intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := A }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : A.card = B.card
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
⊢ False

State before:
case intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := A }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : A.card = B.card
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
⊢ False
Tactic:
have disj : Disjoint (B \ A) (A \ B) := disjoint_sdiff.mono_left sdiff_subset
State after:
case intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := A }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : A.card = B.card
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
⊢ False

State before:
case intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := A }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : A.card = B.card
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
smaller : (B \ A).max' hV < (A \ B).max' hU
⊢ False
Tactic:
refine' hB _
State after:
case intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := A }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : A.card = B.card
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
smaller : (B \ A).max' hV < (A \ B).max' hU
⊢ B ∈ ℬ

State before:
case intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := A }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : A.card = B.card
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
smaller : (B \ A).max' hV < (A \ B).max' hU
⊢ B ∈ ℬ
Tactic:
rw [← (h₂ _ _ ⟨disj, card_sdiff_comm hAB'.symm, hV, hU, smaller⟩).eq]
State after:
case intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := A }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : A.card = B.card
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
smaller : (B \ A).max' hV < (A \ B).max' hU
⊢ B ∈ 𝓒 (B \ A) (A \ B) ℬ

State before:
case intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := A }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : A.card = B.card
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
smaller : (B \ A).max' hV < (A \ B).max' hU
⊢ B ∈ 𝓒 (B \ A) (A \ B) ℬ
Tactic:
exact mem_compression.2 (Or.inr ⟨hB, A, hA, compress_sdiff_sdiff _ _⟩)
State after:
no goals

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := A }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : A.card = B.card
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
⊢ (B \ A).max' hV < (A \ B).max' hU
Tactic:
obtain hlt | heq | hgt := lt_trichotomy (max' _ hU) (max' _ hV)
State after:
case inl
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := A }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : A.card = B.card
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
hlt : (A \ B).max' hU < (B \ A).max' hV
⊢ (B \ A).max' hV < (A \ B).max' hU

case inr.inl
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := A }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : A.card = B.card
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
heq : (A \ B).max' hU = (B \ A).max' hV
⊢ (B \ A).max' hV < (A \ B).max' hU

case inr.inr
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := A }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : A.card = B.card
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
hgt : (B \ A).max' hV < (A \ B).max' hU
⊢ (B \ A).max' hV < (A \ B).max' hU

State before:
case inl
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := A }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : A.card = B.card
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
hlt : (A \ B).max' hU < (B \ A).max' hV
⊢ (B \ A).max' hV < (A \ B).max' hU
Tactic:
rw [← compress_sdiff_sdiff A B] at hAB hBA
State after:
case inl
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := compress (A \ B) (B \ A) B }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : compress (A \ B) (B \ A) B ≠ B
hAB' : A.card = B.card
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
hlt : (A \ B).max' hU < (B \ A).max' hV
⊢ (B \ A).max' hV < (A \ B).max' hU

State before:
case inl
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := compress (A \ B) (B \ A) B }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : compress (A \ B) (B \ A) B ≠ B
hAB' : A.card = B.card
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
hlt : (A \ B).max' hU < (B \ A).max' hV
⊢ (B \ A).max' hV < (A \ B).max' hU
Tactic:
cases hBA.not_lt $ toColex_compress_lt_toColex hlt hAB
State after:
no goals

State before:
case inr.inl
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := A }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : A.card = B.card
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
heq : (A \ B).max' hU = (B \ A).max' hV
⊢ (B \ A).max' hV < (A \ B).max' hU
Tactic:
exact (disjoint_right.1 disj (max'_mem _ hU) $ heq.symm ▸ max'_mem _ _).elim
State after:
no goals

State before:
case inr.inr
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := A }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : A.card = B.card
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
hgt : (B \ A).max' hV < (A \ B).max' hU
⊢ (B \ A).max' hV < (A \ B).max' hU
Tactic:
assumption
State after:
no goals