𝕜 : Type ?u.38
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
⊢ card 𝒜 * r ≤ card ((∂ ) 𝒜) * (Fintype.card α - r + 1)
𝕜 : Type ?u.38
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ card 𝒜 * r ≤ card ((∂ ) 𝒜) * (Fintype.card α - r + 1)
let i : DecidableRel ((. ⊆ .) : Finset α → Finset α → Prop) := fun _ _ => Classical.dec _
case refine'_2
𝕜 : Type ?u.38
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ (∂ ) 𝒜
⊢ card (bipartiteAbove (fun x x_1 => x ⊆ x_1) 𝒜 s) ≤ Fintype.card α - (r - 1)
case refine'_2
𝕜 : Type ?u.38
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ (∂ ) 𝒜
⊢ card (bipartiteAbove (fun x x_1 => x ⊆ x_1) 𝒜 s) ≤ Fintype.card α - r + 1
refine' le_trans _ tsub_tsub_le_tsub_add
case refine'_2
𝕜 : Type ?u.38
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ (∂ ) 𝒜
⊢ card (bipartiteAbove (fun x x_1 => x ⊆ x_1) 𝒜 s) ≤ card (image (fun a => insert a s) (sᶜ))
case refine'_2
𝕜 : Type ?u.38
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ (∂ ) 𝒜
⊢ card (bipartiteAbove (fun x x_1 => x ⊆ x_1) 𝒜 s) ≤ Fintype.card α - (r - 1)
rw [← (Set.Sized.shadow h𝒜) hs, ← card_compl, ← card_image_of_injOn (insert_inj_on' _)]
case refine'_2
𝕜 : Type ?u.38
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ (∂ ) 𝒜
t : Finset α
ht : t ∈ bipartiteAbove (fun x x_1 => x ⊆ x_1) 𝒜 s
⊢ t ∈ image (fun a => insert a s) (sᶜ)
case refine'_2
𝕜 : Type ?u.38
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ (∂ ) 𝒜
⊢ card (bipartiteAbove (fun x x_1 => x ⊆ x_1) 𝒜 s) ≤ card (image (fun a => insert a s) (sᶜ))
refine' card_le_of_subset fun t ht => _
case refine'_2
𝕜 : Type ?u.38
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ (∂ ) 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
⊢ t ∈ image (fun a => insert a s) (sᶜ)
case refine'_2
𝕜 : Type ?u.38
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ (∂ ) 𝒜
t : Finset α
ht : t ∈ bipartiteAbove (fun x x_1 => x ⊆ x_1) 𝒜 s
⊢ t ∈ image (fun a => insert a s) (sᶜ)
rw [mem_bipartiteAbove] at ht
case refine'_2
𝕜 : Type ?u.38
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ (∂ ) 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
this : ¬∅ ∈ 𝒜
⊢ t ∈ image (fun a => insert a s) (sᶜ)
case refine'_2
𝕜 : Type ?u.38
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ (∂ ) 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
⊢ t ∈ image (fun a => insert a s) (sᶜ)
have : ∅ ∉ 𝒜 := by
  rw [← mem_coe, h𝒜.empty_mem_iff, coe_eq_singleton]
  rintro rfl
  rw [shadow_singleton_empty] at hs
  exact not_mem_empty s hs
case refine'_2
𝕜 : Type ?u.38
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ (∂ ) 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
this : ¬∅ ∈ 𝒜
h : ∃ a x, insert a s = t
⊢ t ∈ image (fun a => insert a s) (sᶜ)
case refine'_2
𝕜 : Type ?u.38
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ (∂ ) 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
this : ¬∅ ∈ 𝒜
⊢ t ∈ image (fun a => insert a s) (sᶜ)
have h := exists_eq_insert_iff.2 ⟨ht.2, by
  rw [(sized_shadow_iff this).1 (Set.Sized.shadow h𝒜) ht.1, (Set.Sized.shadow h𝒜) hs]⟩
case refine'_2.intro.intro
𝕜 : Type ?u.38
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ (∂ ) 𝒜
this : ¬∅ ∈ 𝒜
a : α
ha : ¬a ∈ s
ht : insert a s ∈ 𝒜 ∧ s ⊆ insert a s
⊢ insert a s ∈ image (fun a => insert a s) (sᶜ)
case refine'_2
𝕜 : Type ?u.38
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ (∂ ) 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
this : ¬∅ ∈ 𝒜
h : ∃ a x, insert a s = t
⊢ t ∈ image (fun a => insert a s) (sᶜ)
rcases h with ⟨a, ha, rfl⟩
no goals
case refine'_2.intro.intro
𝕜 : Type ?u.38
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ (∂ ) 𝒜
this : ¬∅ ∈ 𝒜
a : α
ha : ¬a ∈ s
ht : insert a s ∈ 𝒜 ∧ s ⊆ insert a s
⊢ insert a s ∈ image (fun a => insert a s) (sᶜ)
exact mem_image_of_mem _ (mem_compl.2 ha)
case refine'_1
𝕜 : Type ?u.38
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ card (image (erase s) s) ≤ card (bipartiteBelow (fun x x_1 => x ⊆ x_1) ((∂ ) 𝒜) s)
case refine'_1
𝕜 : Type ?u.38
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ r ≤ card (bipartiteBelow (fun x x_1 => x ⊆ x_1) ((∂ ) 𝒜) s)
rw [← h𝒜 hs, ← card_image_of_injOn s.erase_injOn]
case refine'_1
𝕜 : Type ?u.38
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ image (erase s) s ⊆ bipartiteBelow (fun x x_1 => x ⊆ x_1) ((∂ ) 𝒜) s
case refine'_1
𝕜 : Type ?u.38
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ card (image (erase s) s) ≤ card (bipartiteBelow (fun x x_1 => x ⊆ x_1) ((∂ ) 𝒜) s)
refine' card_le_of_subset _
case refine'_1
𝕜 : Type ?u.38
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ ∀ (x : α), x ∈ s → erase s x ∈ (∂ ) 𝒜 ∧ erase s x ⊆ s
case refine'_1
𝕜 : Type ?u.38
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ image (erase s) s ⊆ bipartiteBelow (fun x x_1 => x ⊆ x_1) ((∂ ) 𝒜) s
simp_rw [image_subset_iff, mem_bipartiteBelow]
no goals
case refine'_1
𝕜 : Type ?u.38
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ ∀ (x : α), x ∈ s → erase s x ∈ (∂ ) 𝒜 ∧ erase s x ⊆ s
exact fun a ha => ⟨erase_mem_shadow hs ha, erase_subset _ _⟩
𝕜 : Type ?u.38
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ (∂ ) 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
⊢ ¬𝒜 = {∅}
𝕜 : Type ?u.38
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ (∂ ) 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
⊢ ¬∅ ∈ 𝒜
rw [← mem_coe, h𝒜.empty_mem_iff, coe_eq_singleton]
𝕜 : Type ?u.38
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
r : ℕ
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s t : Finset α
h𝒜 : Set.Sized r ↑{∅}
hs : s ∈ (∂ ) {∅}
ht : t ∈ {∅} ∧ s ⊆ t
⊢ False
𝕜 : Type ?u.38
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ (∂ ) 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
⊢ ¬𝒜 = {∅}
rintro rfl
𝕜 : Type ?u.38
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
r : ℕ
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s t : Finset α
h𝒜 : Set.Sized r ↑{∅}
hs : s ∈ ∅
ht : t ∈ {∅} ∧ s ⊆ t
⊢ False
𝕜 : Type ?u.38
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
r : ℕ
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s t : Finset α
h𝒜 : Set.Sized r ↑{∅}
hs : s ∈ (∂ ) {∅}
ht : t ∈ {∅} ∧ s ⊆ t
⊢ False
rw [shadow_singleton_empty] at hs
no goals
𝕜 : Type ?u.38
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
r : ℕ
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s t : Finset α
h𝒜 : Set.Sized r ↑{∅}
hs : s ∈ ∅
ht : t ∈ {∅} ∧ s ⊆ t
⊢ False
exact not_mem_empty s hs
no goals
𝕜 : Type ?u.38
α : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)
s : Finset α
hs : s ∈ (∂ ) 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
this : ¬∅ ∈ 𝒜
⊢ card s + 1 = card t
rw [(sized_shadow_iff this).1 (Set.Sized.shadow h𝒜) ht.1, (Set.Sized.shadow h𝒜) hs]