internlm/Lean-Github huggingface dataset:
Theorem: Finset.UV.compression_improved
Proof 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)
Proof 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)) 𝒜
Theorem: Finset.UV.compression_improved
Proof 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)
Proof 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
Theorem: Finset.UV.compression_improved
Proof 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
Proof 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)) 𝒜
Theorem: Finset.UV.compression_improved
Proof 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']
Proof 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)) 𝒜
Theorem: Finset.UV.compression_improved
Proof 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]
Proof 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)) 𝒜
Theorem: Finset.UV.compression_improved
Proof 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) = ∅›]
Proof 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 ∅ ∅ 𝒜
Theorem: Finset.UV.compression_improved
Proof 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 _ _
Proof state after:
no goals
Theorem: Finset.UV.compression_improved
Proof 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']
Proof state after:
no goals
Theorem: Finset.UV.compression_improved
Proof 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]
Proof state after:
no goals
Theorem: Finset.UV.compression_improved
Proof 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]
Proof state after:
no goals
Theorem: Finset.UV.compression_improved
Proof 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]
Proof state after:
no goals
Theorem: Finset.UV.compression_improved
Proof 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]
Proof state after:
no goals
Theorem: Finset.UV.compression_improved
Proof 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 _ _⟩)
Proof 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
Theorem: Finset.UV.compression_improved
Proof 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]
Proof state after:
no goals
Theorem: Finset.UV.isInitSeg_of_compressed
Proof 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₁, _⟩
Proof 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 ∈ ℬ
Theorem: Finset.UV.isInitSeg_of_compressed
Proof 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⟩
Proof 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 ∈ ℬ
Theorem: Finset.UV.isInitSeg_of_compressed
Proof 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
Proof 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
Theorem: Finset.UV.isInitSeg_of_compressed
Proof 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
Proof 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
Theorem: Finset.UV.isInitSeg_of_compressed
Proof 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
Proof 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
Theorem: Finset.UV.isInitSeg_of_compressed
Proof 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
Proof 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
Theorem: Finset.UV.isInitSeg_of_compressed
Proof 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
Proof 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
Theorem: Finset.UV.isInitSeg_of_compressed
Proof 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
Proof 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
Theorem: Finset.UV.isInitSeg_of_compressed
Proof 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 _
Proof 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 ∈ ℬ
Theorem: Finset.UV.isInitSeg_of_compressed
Proof 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]
Proof 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) ℬ
Theorem: Finset.UV.isInitSeg_of_compressed
Proof 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 _ _⟩)
Proof state after:
no goals
Theorem: Finset.UV.isInitSeg_of_compressed
Proof 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)
Proof 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