FormalConjecturesForMathlib.Data.Finset.Powerset

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module

public import Mathlib.Data.Finset.Powerset

@[expose] public sectionnamespace Finsetvariable {α : Type*} [DecidableEq α] {s t : Finset α} {n : ℕ}attribute [gcongr] powersetCard_mono

lemma powersetCard_inter : powersetCard n (s ∩ t) = powersetCard n s ∩ powersetCard n t := byα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αn:ℕ⊢ powersetCard n (s ∩ t) = powersetCard n s ∩ powersetCard n t
  extα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αn:ℕa✝:Finset α⊢ a✝ ∈ powersetCard n (s ∩ t) ↔ a✝ ∈ powersetCard n s ∩ powersetCard n t; simpa [subset_inter_iff] using and_and_rightAll goals completed! 🐙

@[simp] lemma disjoint_powersetCard_powersetCard :
    Disjoint (powersetCard n s) (powersetCard n t) ↔ #(s ∩ t) < n := byα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αn:ℕ⊢ Disjoint (powersetCard n s) (powersetCard n t) ↔ #(s ∩ t) < n
  simp [disjoint_iff_inter_eq_empty, ← powersetCard_inter]All goals completed! 🐙

The (#t + 1)-subsets of s that contain t ⊆ s are exactly the sets insert a t with a ∈ s \ t.


lemma filter_subset_powersetCard_card_add_one (h : t ⊆ s) :
    (powersetCard (#t + 1) s).filter (t ⊆ ·) = (s \ t).image (insert · t) := byα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ s⊢ {x ∈ powersetCard (#t + 1) s | t ⊆ x} = image (fun x ↦ insert x t) (s \ t)
  ext uα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset α⊢ u ∈ {x ∈ powersetCard (#t + 1) s | t ⊆ x} ↔ u ∈ image (fun x ↦ insert x t) (s \ t)
  simp only [mem_filter, mem_powersetCard, mem_image, mem_sdiff]α:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset α⊢ (u ⊆ s ∧ #u = #t + 1) ∧ t ⊆ u ↔ ∃ a, (a ∈ s ∧ a ∉ t) ∧ insert a t = u
  constructormpα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset α⊢ (u ⊆ s ∧ #u = #t + 1) ∧ t ⊆ u → ∃ a, (a ∈ s ∧ a ∉ t) ∧ insert a t = umprα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset α⊢ (∃ a, (a ∈ s ∧ a ∉ t) ∧ insert a t = u) → (u ⊆ s ∧ #u = #t + 1) ∧ t ⊆ u
  ·mpα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset α⊢ (u ⊆ s ∧ #u = #t + 1) ∧ t ⊆ u → ∃ a, (a ∈ s ∧ a ∉ t) ∧ insert a t = u rintro ⟨⟨hus, hu⟩, htu⟩mpα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset αhtu:t ⊆ uhus:u ⊆ shu:#u = #t + 1⊢ ∃ a, (a ∈ s ∧ a ∉ t) ∧ insert a t = u
    have h1 : #(u \ t) = 1 := byα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ s⊢ {x ∈ powersetCard (#t + 1) s | t ⊆ x} = image (fun x ↦ insert x t) (s \ t)mpα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset αhtu:t ⊆ uhus:u ⊆ shu:#u = #t + 1h1:#(u \ t) = 1⊢ ∃ a, (a ∈ s ∧ a ∉ t) ∧ insert a t = u rw [card_sdiff_of_subset htu,α:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset αhtu:t ⊆ uhus:u ⊆ shu:#u = #t + 1⊢ #u - #t = 1α:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset αhtu:t ⊆ uhus:u ⊆ shu:#u = #t + 1⊢ #t + 1 - #t = 1mpα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset αhtu:t ⊆ uhus:u ⊆ shu:#u = #t + 1h1:#(u \ t) = 1⊢ ∃ a, (a ∈ s ∧ a ∉ t) ∧ insert a t = u huα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset αhtu:t ⊆ uhus:u ⊆ shu:#u = #t + 1⊢ #t + 1 - #t = 1α:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset αhtu:t ⊆ uhus:u ⊆ shu:#u = #t + 1⊢ #t + 1 - #t = 1mpα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset αhtu:t ⊆ uhus:u ⊆ shu:#u = #t + 1h1:#(u \ t) = 1⊢ ∃ a, (a ∈ s ∧ a ∉ t) ∧ insert a t = u]α:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset αhtu:t ⊆ uhus:u ⊆ shu:#u = #t + 1⊢ #t + 1 - #t = 1mpα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset αhtu:t ⊆ uhus:u ⊆ shu:#u = #t + 1h1:#(u \ t) = 1⊢ ∃ a, (a ∈ s ∧ a ∉ t) ∧ insert a t = u; omegampα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset αhtu:t ⊆ uhus:u ⊆ shu:#u = #t + 1h1:#(u \ t) = 1⊢ ∃ a, (a ∈ s ∧ a ∉ t) ∧ insert a t = umpα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset αhtu:t ⊆ uhus:u ⊆ shu:#u = #t + 1h1:#(u \ t) = 1⊢ ∃ a, (a ∈ s ∧ a ∉ t) ∧ insert a t = u
    obtain ⟨a, ha⟩ := card_eq_one.1 h1mpα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset αhtu:t ⊆ uhus:u ⊆ shu:#u = #t + 1h1:#(u \ t) = 1a:αha:u \ t = {a}⊢ ∃ a, (a ∈ s ∧ a ∉ t) ∧ insert a t = u
    have hat : a ∈ u \ t := byα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ s⊢ {x ∈ powersetCard (#t + 1) s | t ⊆ x} = image (fun x ↦ insert x t) (s \ t)mpα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset αhtu:t ⊆ uhus:u ⊆ shu:#u = #t + 1h1:#(u \ t) = 1a:αha:u \ t = {a}hat:a ∈ u \ t⊢ ∃ a, (a ∈ s ∧ a ∉ t) ∧ insert a t = u rw [haα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset αhtu:t ⊆ uhus:u ⊆ shu:#u = #t + 1h1:#(u \ t) = 1a:αha:u \ t = {a}⊢ a ∈ {a}α:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset αhtu:t ⊆ uhus:u ⊆ shu:#u = #t + 1h1:#(u \ t) = 1a:αha:u \ t = {a}⊢ a ∈ {a}mpα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset αhtu:t ⊆ uhus:u ⊆ shu:#u = #t + 1h1:#(u \ t) = 1a:αha:u \ t = {a}hat:a ∈ u \ t⊢ ∃ a, (a ∈ s ∧ a ∉ t) ∧ insert a t = u]α:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset αhtu:t ⊆ uhus:u ⊆ shu:#u = #t + 1h1:#(u \ t) = 1a:αha:u \ t = {a}⊢ a ∈ {a}mpα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset αhtu:t ⊆ uhus:u ⊆ shu:#u = #t + 1h1:#(u \ t) = 1a:αha:u \ t = {a}hat:a ∈ u \ t⊢ ∃ a, (a ∈ s ∧ a ∉ t) ∧ insert a t = u; exact mem_singleton_self ampα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset αhtu:t ⊆ uhus:u ⊆ shu:#u = #t + 1h1:#(u \ t) = 1a:αha:u \ t = {a}hat:a ∈ u \ t⊢ ∃ a, (a ∈ s ∧ a ∉ t) ∧ insert a t = umpα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset αhtu:t ⊆ uhus:u ⊆ shu:#u = #t + 1h1:#(u \ t) = 1a:αha:u \ t = {a}hat:a ∈ u \ t⊢ ∃ a, (a ∈ s ∧ a ∉ t) ∧ insert a t = u
    rw [mem_sdiffmpα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset αhtu:t ⊆ uhus:u ⊆ shu:#u = #t + 1h1:#(u \ t) = 1a:αha:u \ t = {a}hat:a ∈ u ∧ a ∉ t⊢ ∃ a, (a ∈ s ∧ a ∉ t) ∧ insert a t = umpα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset αhtu:t ⊆ uhus:u ⊆ shu:#u = #t + 1h1:#(u \ t) = 1a:αha:u \ t = {a}hat:a ∈ u ∧ a ∉ t⊢ ∃ a, (a ∈ s ∧ a ∉ t) ∧ insert a t = u] at hatmpα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset αhtu:t ⊆ uhus:u ⊆ shu:#u = #t + 1h1:#(u \ t) = 1a:αha:u \ t = {a}hat:a ∈ u ∧ a ∉ t⊢ ∃ a, (a ∈ s ∧ a ∉ t) ∧ insert a t = u
    refine ⟨a, ⟨hus hat.1, hat.2⟩, ?_⟩mpα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset αhtu:t ⊆ uhus:u ⊆ shu:#u = #t + 1h1:#(u \ t) = 1a:αha:u \ t = {a}hat:a ∈ u ∧ a ∉ t⊢ insert a t = u
    rw [insert_eq,mpα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset αhtu:t ⊆ uhus:u ⊆ shu:#u = #t + 1h1:#(u \ t) = 1a:αha:u \ t = {a}hat:a ∈ u ∧ a ∉ t⊢ {a} ∪ t = uAll goals completed! 🐙 ← ha,mpα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset αhtu:t ⊆ uhus:u ⊆ shu:#u = #t + 1h1:#(u \ t) = 1a:αha:u \ t = {a}hat:a ∈ u ∧ a ∉ t⊢ u \ t ∪ t = uAll goals completed! 🐙 sdiff_union_of_subset htumpα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset αhtu:t ⊆ uhus:u ⊆ shu:#u = #t + 1h1:#(u \ t) = 1a:αha:u \ t = {a}hat:a ∈ u ∧ a ∉ t⊢ u = uAll goals completed! 🐙]All goals completed! 🐙
  ·mprα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ su:Finset α⊢ (∃ a, (a ∈ s ∧ a ∉ t) ∧ insert a t = u) → (u ⊆ s ∧ #u = #t + 1) ∧ t ⊆ u rintro ⟨a, ⟨has, hat⟩, rfl⟩mprα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ sa:αhas:a ∈ shat:a ∉ t⊢ (insert a t ⊆ s ∧ #(insert a t) = #t + 1) ∧ t ⊆ insert a t
    exact ⟨⟨insert_subset has h, card_insert_of_notMem hat⟩, subset_insert _ _⟩All goals completed! 🐙

A k-subset t of s lies in exactly #s - k of the (k + 1)-subsets of s.


lemma card_filter_subset_powersetCard_card_add_one (h : t ⊆ s) :
    #((powersetCard (#t + 1) s).filter (t ⊆ ·)) = #s - #t := byα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ s⊢ #({x ∈ powersetCard (#t + 1) s | t ⊆ x}) = #s - #t
  rw [filter_subset_powersetCard_card_add_one h,α:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ s⊢ #(image (fun x ↦ insert x t) (s \ t)) = #s - #tα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ s⊢ Set.InjOn (fun x ↦ insert x t) ↑(s \ t) card_image_of_injOn,α:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ s⊢ #(s \ t) = #s - #tα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ s⊢ Set.InjOn (fun x ↦ insert x t) ↑(s \ t)α:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ s⊢ Set.InjOn (fun x ↦ insert x t) ↑(s \ t) card_sdiff_of_subset hα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ s⊢ #s - #t = #s - #tα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ s⊢ Set.InjOn (fun x ↦ insert x t) ↑(s \ t)α:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ s⊢ Set.InjOn (fun x ↦ insert x t) ↑(s \ t)]α:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ s⊢ Set.InjOn (fun x ↦ insert x t) ↑(s \ t)
  intro a ha b _ habα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ sa:αha:a ∈ ↑(s \ t)b:αa✝:b ∈ ↑(s \ t)hab:(fun x ↦ insert x t) a = (fun x ↦ insert x t) b⊢ a = b
  have : a ∈ insert b t := byα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ s⊢ #({x ∈ powersetCard (#t + 1) s | t ⊆ x}) = #s - #tα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ sa:αha:a ∈ ↑(s \ t)b:αa✝:b ∈ ↑(s \ t)hab:(fun x ↦ insert x t) a = (fun x ↦ insert x t) bthis:a ∈ insert b t⊢ a = b
    rw [← show insert a t = insert b t from habα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ sa:αha:a ∈ ↑(s \ t)b:αa✝:b ∈ ↑(s \ t)hab:(fun x ↦ insert x t) a = (fun x ↦ insert x t) b⊢ a ∈ insert a tα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ sa:αha:a ∈ ↑(s \ t)b:αa✝:b ∈ ↑(s \ t)hab:(fun x ↦ insert x t) a = (fun x ↦ insert x t) b⊢ a ∈ insert a tα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ sa:αha:a ∈ ↑(s \ t)b:αa✝:b ∈ ↑(s \ t)hab:(fun x ↦ insert x t) a = (fun x ↦ insert x t) bthis:a ∈ insert b t⊢ a = b]α:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ sa:αha:a ∈ ↑(s \ t)b:αa✝:b ∈ ↑(s \ t)hab:(fun x ↦ insert x t) a = (fun x ↦ insert x t) b⊢ a ∈ insert a tα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ sa:αha:a ∈ ↑(s \ t)b:αa✝:b ∈ ↑(s \ t)hab:(fun x ↦ insert x t) a = (fun x ↦ insert x t) bthis:a ∈ insert b t⊢ a = b
    exact mem_insert_self a tα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ sa:αha:a ∈ ↑(s \ t)b:αa✝:b ∈ ↑(s \ t)hab:(fun x ↦ insert x t) a = (fun x ↦ insert x t) bthis:a ∈ insert b t⊢ a = bα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ sa:αha:a ∈ ↑(s \ t)b:αa✝:b ∈ ↑(s \ t)hab:(fun x ↦ insert x t) a = (fun x ↦ insert x t) bthis:a ∈ insert b t⊢ a = b
  rw [mem_insertα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ sa:αha:a ∈ ↑(s \ t)b:αa✝:b ∈ ↑(s \ t)hab:(fun x ↦ insert x t) a = (fun x ↦ insert x t) bthis:a = b ∨ a ∈ t⊢ a = bα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ sa:αha:a ∈ ↑(s \ t)b:αa✝:b ∈ ↑(s \ t)hab:(fun x ↦ insert x t) a = (fun x ↦ insert x t) bthis:a = b ∨ a ∈ t⊢ a = b] at thisα:Type u_1inst✝:DecidableEq αs:Finset αt:Finset αh:t ⊆ sa:αha:a ∈ ↑(s \ t)b:αa✝:b ∈ ↑(s \ t)hab:(fun x ↦ insert x t) a = (fun x ↦ insert x t) bthis:a = b ∨ a ∈ t⊢ a = b
  exact this.resolve_right (mem_sdiff.1 ha).2All goals completed! 🐙

end Finset