internlm/Lean-Github huggingface dataset:
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
case a.mpr.inr.intro.intro.intro.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk✝ : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
hjk : j < k
⊢ insert j t = s ∨ ∃ w ∈ s, w ∉ insert j t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ insert j t ↔ a ∈ s)
Tactic:
refine Or.inr ⟨k, mem_of_mem_erase ‹_›, fun hk ↦ hkt $ mem_of_mem_insert_of_ne hk hjk.ne',
  fun x hx ↦ ?_⟩
Proof state after:
case a.mpr.inr.intro.intro.intro.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk✝ : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
hjk : j < k
x : α
hx : k < x
⊢ x ∈ insert j t ↔ x ∈ s
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
case a.mpr.inr.intro.intro.intro.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk✝ : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
hjk : j < k
x : α
hx : k < x
⊢ x ∈ insert j t ↔ x ∈ s
Tactic:
simpa only [mem_insert, z hx, (hjk.trans hx).ne', mem_erase, Ne, false_or_iff,
  and_iff_right_iff_imp] using fun _ ↦ ((min'_le _ _ $ mem_of_mem_erase hks).trans_lt hx).ne'
Proof state after:
no goals
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
case a.mpr.inr.intro.intro.intro.inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
r₁ : j = k
a : α
ha : a ∈ s
lt : k < a
⊢ a ∈ insert j t
Tactic:
apply mem_insert_of_mem
Proof state after:
case a.mpr.inr.intro.intro.intro.inr.inl.h
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
r₁ : j = k
a : α
ha : a ∈ s
lt : k < a
⊢ a ∈ t
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
case a.mpr.inr.intro.intro.intro.inr.inl.h
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
r₁ : j = k
a : α
ha : a ∈ s
lt : k < a
⊢ a ∈ t
Tactic:
rw [z lt]
Proof state after:
case a.mpr.inr.intro.intro.intro.inr.inl.h
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
r₁ : j = k
a : α
ha : a ∈ s
lt : k < a
⊢ a ∈ s.erase (s.min' hs)
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
case a.mpr.inr.intro.intro.intro.inr.inl.h
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
r₁ : j = k
a : α
ha : a ∈ s
lt : k < a
⊢ a ∈ s.erase (s.min' hs)
Tactic:
refine' mem_erase_of_ne_of_mem (lt_of_le_of_lt _ lt).ne' ha
Proof state after:
case a.mpr.inr.intro.intro.intro.inr.inl.h
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
r₁ : j = k
a : α
ha : a ∈ s
lt : k < a
⊢ s.min' hs ≤ k
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
case a.mpr.inr.intro.intro.intro.inr.inl.h
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
r₁ : j = k
a : α
ha : a ∈ s
lt : k < a
⊢ s.min' hs ≤ k
Tactic:
apply min'_le _ _ (mem_of_mem_erase ‹_›)
Proof state after:
no goals
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
case a.mpr.inr.intro.intro.intro.inr.inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
r₁ : j = k
ha : k ∈ s
⊢ k ∈ insert j t
Tactic:
rw [r₁]
Proof state after:
case a.mpr.inr.intro.intro.intro.inr.inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
r₁ : j = k
ha : k ∈ s
⊢ k ∈ insert k t
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
case a.mpr.inr.intro.intro.intro.inr.inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
r₁ : j = k
ha : k ∈ s
⊢ k ∈ insert k t
Tactic:
apply mem_insert_self
Proof state after:
no goals
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
case a.mpr.inr.intro.intro.intro.inr.inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
r₁ : j = k
a : α
ha : a ∈ s
gt : a < k
⊢ a ∈ insert j t
Tactic:
apply mem_insert_of_mem
Proof state after:
case a.mpr.inr.intro.intro.intro.inr.inr.inr.h
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
r₁ : j = k
a : α
ha : a ∈ s
gt : a < k
⊢ a ∈ t
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
case a.mpr.inr.intro.intro.intro.inr.inr.inr.h
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
r₁ : j = k
a : α
ha : a ∈ s
gt : a < k
⊢ a ∈ t
Tactic:
rw [← r₁] at gt
Proof state after:
case a.mpr.inr.intro.intro.intro.inr.inr.inr.h
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
r₁ : j = k
a : α
ha : a ∈ s
gt : a < j
⊢ a ∈ t
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
case a.mpr.inr.intro.intro.intro.inr.inr.inr.h
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
r₁ : j = k
a : α
ha : a ∈ s
gt : a < j
⊢ a ∈ t
Tactic:
by_contra
Proof state after:
case a.mpr.inr.intro.intro.intro.inr.inr.inr.h
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
r₁ : j = k
a : α
ha : a ∈ s
gt : a < j
x✝ : a ∉ t
⊢ False
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
case a.mpr.inr.intro.intro.intro.inr.inr.inr.h
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
r₁ : j = k
a : α
ha : a ∈ s
gt : a < j
x✝ : a ∉ t
⊢ False
Tactic:
apply (min'_le tᶜ _ _).not_lt gt
Proof state after:
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
r₁ : j = k
a : α
ha : a ∈ s
gt : a < j
x✝ : a ∉ t
⊢ a ∈ tᶜ
Theorem: Finset.Colex.shadow_initSeg
Proof state before:
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t✝ : Finset α
r : ℕ
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : (s.erase (s.min' hs)).card = t.card
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : s.card = (insert j t).card
r₁ : j = k
a : α
ha : a ∈ s
gt : a < j
x✝ : a ∉ t
⊢ a ∈ tᶜ
Tactic:
rwa [mem_compl]
Proof state after:
no goals
Theorem: Finset.Colex.IsInitSeg.shadow
Proof state before:
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
r : ℕ
inst✝ : Finite α
h₁ : IsInitSeg 𝒜 r
⊢ IsInitSeg (∂ 𝒜) (r - 1)
Tactic:
cases nonempty_fintype α
Proof state after:
case intro
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
r : ℕ
inst✝ : Finite α
h₁ : IsInitSeg 𝒜 r
val✝ : Fintype α
⊢ IsInitSeg (∂ 𝒜) (r - 1)
Theorem: Finset.Colex.IsInitSeg.shadow
Proof state before:
case intro
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
r : ℕ
inst✝ : Finite α
h₁ : IsInitSeg 𝒜 r
val✝ : Fintype α
⊢ IsInitSeg (∂ 𝒜) (r - 1)
Tactic:
obtain rfl | hr := Nat.eq_zero_or_pos r
Proof state after:
case intro.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
⊢ IsInitSeg (∂ 𝒜) (0 - 1)

case intro.inr
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
r : ℕ
inst✝ : Finite α
h₁ : IsInitSeg 𝒜 r
val✝ : Fintype α
hr : r > 0
⊢ IsInitSeg (∂ 𝒜) (r - 1)
Theorem: Finset.Colex.IsInitSeg.shadow
Proof state before:
case intro.inr
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
r : ℕ
inst✝ : Finite α
h₁ : IsInitSeg 𝒜 r
val✝ : Fintype α
hr : r > 0
⊢ IsInitSeg (∂ 𝒜) (r - 1)
Tactic:
obtain rfl | h𝒜 := 𝒜.eq_empty_or_nonempty
Proof state after:
case intro.inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
r : ℕ
inst✝ : Finite α
val✝ : Fintype α
hr : r > 0
h₁ : IsInitSeg ∅ r
⊢ IsInitSeg (∂ ∅) (r - 1)

case intro.inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
r : ℕ
inst✝ : Finite α
h₁ : IsInitSeg 𝒜 r
val✝ : Fintype α
hr : r > 0
h𝒜 : 𝒜.Nonempty
⊢ IsInitSeg (∂ 𝒜) (r - 1)
Theorem: Finset.Colex.IsInitSeg.shadow
Proof state before:
case intro.inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
r : ℕ
inst✝ : Finite α
h₁ : IsInitSeg 𝒜 r
val✝ : Fintype α
hr : r > 0
h𝒜 : 𝒜.Nonempty
⊢ IsInitSeg (∂ 𝒜) (r - 1)
Tactic:
obtain ⟨s, rfl, rfl⟩ := h₁.exists_initSeg h𝒜
Proof state after:
case intro.inr.inr.intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t : Finset α
inst✝ : Finite α
val✝ : Fintype α
s : Finset α
hr : s.card > 0
h𝒜 : (initSeg s).Nonempty
h₁ : IsInitSeg (initSeg s) s.card
⊢ IsInitSeg (∂ (initSeg s)) (s.card - 1)
Theorem: Finset.Colex.IsInitSeg.shadow
Proof state before:
case intro.inr.inr.intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t : Finset α
inst✝ : Finite α
val✝ : Fintype α
s : Finset α
hr : s.card > 0
h𝒜 : (initSeg s).Nonempty
h₁ : IsInitSeg (initSeg s) s.card
⊢ IsInitSeg (∂ (initSeg s)) (s.card - 1)
Tactic:
rw [shadow_initSeg (card_pos.1 hr), ← card_erase_of_mem (min'_mem _ _)]
Proof state after:
case intro.inr.inr.intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t : Finset α
inst✝ : Finite α
val✝ : Fintype α
s : Finset α
hr : s.card > 0
h𝒜 : (initSeg s).Nonempty
h₁ : IsInitSeg (initSeg s) s.card
⊢ IsInitSeg (initSeg (s.erase (s.min' ⋯))) (s.erase (s.min' ?m.16021)).card

α : Type u_1
inst✝¹ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t : Finset α
inst✝ : Finite α
val✝ : Fintype α
s : Finset α
hr : s.card > 0
h𝒜 : (initSeg s).Nonempty
h₁ : IsInitSeg (initSeg s) s.card
⊢ s.Nonempty
Theorem: Finset.Colex.IsInitSeg.shadow
Proof state before:
case intro.inr.inr.intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t : Finset α
inst✝ : Finite α
val✝ : Fintype α
s : Finset α
hr : s.card > 0
h𝒜 : (initSeg s).Nonempty
h₁ : IsInitSeg (initSeg s) s.card
⊢ IsInitSeg (initSeg (s.erase (s.min' ⋯))) (s.erase (s.min' ?m.16021)).card

α : Type u_1
inst✝¹ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t : Finset α
inst✝ : Finite α
val✝ : Fintype α
s : Finset α
hr : s.card > 0
h𝒜 : (initSeg s).Nonempty
h₁ : IsInitSeg (initSeg s) s.card
⊢ s.Nonempty
Tactic:
exact isInitSeg_initSeg
Proof state after:
no goals
Theorem: Finset.Colex.IsInitSeg.shadow
Proof state before:
case intro.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
⊢ IsInitSeg (∂ 𝒜) (0 - 1)
Tactic:
have : 𝒜 ⊆ {∅} := fun s hs ↦ by rw [mem_singleton, ← Finset.card_eq_zero]; exact h₁.1 hs
Proof state after:
case intro.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
this : 𝒜 ⊆ {∅}
⊢ IsInitSeg (∂ 𝒜) (0 - 1)
Theorem: Finset.Colex.IsInitSeg.shadow
Proof state before:
case intro.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
this : 𝒜 ⊆ {∅}
⊢ IsInitSeg (∂ 𝒜) (0 - 1)
Tactic:
have := shadow_monotone this
Proof state after:
case intro.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
this✝ : 𝒜 ⊆ {∅}
this : ∂ 𝒜 ≤ ∂ {∅}
⊢ IsInitSeg (∂ 𝒜) (0 - 1)
Theorem: Finset.Colex.IsInitSeg.shadow
Proof state before:
case intro.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
this✝ : 𝒜 ⊆ {∅}
this : ∂ 𝒜 ≤ ∂ {∅}
⊢ IsInitSeg (∂ 𝒜) (0 - 1)
Tactic:
simp only [subset_empty, le_eq_subset, shadow_singleton_empty] at this
Proof state after:
case intro.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
this✝ : 𝒜 ⊆ {∅}
this : ∂ 𝒜 = ∅
⊢ IsInitSeg (∂ 𝒜) (0 - 1)
Theorem: Finset.Colex.IsInitSeg.shadow
Proof state before:
case intro.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
this✝ : 𝒜 ⊆ {∅}
this : ∂ 𝒜 = ∅
⊢ IsInitSeg (∂ 𝒜) (0 - 1)
Tactic:
simp [this]
Proof state after:
no goals
Theorem: Finset.Colex.IsInitSeg.shadow
Proof state before:
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t : Finset α
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
s : Finset α
hs : s ∈ 𝒜
⊢ s ∈ {∅}
Tactic:
rw [mem_singleton, ← Finset.card_eq_zero]
Proof state after:
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t : Finset α
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
s : Finset α
hs : s ∈ 𝒜
⊢ s.card = 0
Theorem: Finset.Colex.IsInitSeg.shadow
Proof state before:
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t : Finset α
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
s : Finset α
hs : s ∈ 𝒜
⊢ s.card = 0
Tactic:
exact h₁.1 hs
Proof state after:
no goals
Theorem: Finset.Colex.IsInitSeg.shadow
Proof state before:
case intro.inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
s t : Finset α
r : ℕ
inst✝ : Finite α
val✝ : Fintype α
hr : r > 0
h₁ : IsInitSeg ∅ r
⊢ IsInitSeg (∂ ∅) (r - 1)
Tactic:
simp
Proof state after:
no goals
Theorem: Finset.UV.toColex_compress_lt_toColex
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : compress U V s ≠ s
⊢ { ofColex := compress U V s } < { ofColex := s }
Tactic:
rw [compress, ite_ne_right_iff] at hA
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ≤ s) ∧ (s ⊔ U) \ V ≠ s
⊢ { ofColex := compress U V s } < { ofColex := s }
Theorem: Finset.UV.toColex_compress_lt_toColex
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ≤ s) ∧ (s ⊔ U) \ V ≠ s
⊢ { ofColex := compress U V s } < { ofColex := s }
Tactic:
rw [compress, if_pos hA.1, lt_iff_exists_forall_lt_mem_iff_mem]
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ≤ s) ∧ (s ⊔ U) \ V ≠ s
⊢ ∃ w ∈ s, w ∉ (s ⊔ U) \ V ∧ ∀ ⦃a : α⦄, w < a → (a ∈ (s ⊔ U) \ V ↔ a ∈ s)
Theorem: Finset.UV.toColex_compress_lt_toColex
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ≤ s) ∧ (s ⊔ U) \ V ≠ s
⊢ ∃ w ∈ s, w ∉ (s ⊔ U) \ V ∧ ∀ ⦃a : α⦄, w < a → (a ∈ (s ⊔ U) \ V ↔ a ∈ s)
Tactic:
refine ⟨_, hA.1.2 $ max'_mem _ hV, not_mem_sdiff_of_mem_right $ max'_mem _ _, fun a ha ↦ ?_⟩
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ≤ s) ∧ (s ⊔ U) \ V ≠ s
a : α
ha : V.max' hV < a
⊢ a ∈ (s ⊔ U) \ V ↔ a ∈ s
Theorem: Finset.UV.toColex_compress_lt_toColex
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ≤ s) ∧ (s ⊔ U) \ V ≠ s
a : α
ha : V.max' hV < a
⊢ a ∈ (s ⊔ U) \ V ↔ a ∈ s
Tactic:
have : a ∉ V := fun H ↦ ha.not_le (le_max' _ _ H)
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ≤ s) ∧ (s ⊔ U) \ V ≠ s
a : α
ha : V.max' hV < a
this : a ∉ V
⊢ a ∈ (s ⊔ U) \ V ↔ a ∈ s
Theorem: Finset.UV.toColex_compress_lt_toColex
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ≤ s) ∧ (s ⊔ U) \ V ≠ s
a : α
ha : V.max' hV < a
this : a ∉ V
⊢ a ∈ (s ⊔ U) \ V ↔ a ∈ s
Tactic:
have : a ∉ U := fun H ↦ ha.not_lt ((le_max' _ _ H).trans_lt h)
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ≤ s) ∧ (s ⊔ U) \ V ≠ s
a : α
ha : V.max' hV < a
this✝ : a ∉ V
this : a ∉ U
⊢ a ∈ (s ⊔ U) \ V ↔ a ∈ s
Theorem: Finset.UV.toColex_compress_lt_toColex
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ≤ s) ∧ (s ⊔ U) \ V ≠ s
a : α
ha : V.max' hV < a
this✝ : a ∉ V
this : a ∉ U
⊢ a ∈ (s ⊔ U) \ V ↔ a ∈ s
Tactic:
simp [‹a ∉ U›, ‹a ∉ V›]
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₁ : 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₁
Proof 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
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
⊢ (∂ (𝓒 U V 𝒜)).card ≤ (∂ 𝒜).card
Tactic:
refine' card_shadow_compression_le _ _ fun x Hx ↦ ⟨min' V hV, min'_mem _ _, _⟩
Proof 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)) 𝒜