awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 ℬ : Finset (Finset α)
simp_rw :
  Eq (α := Finset (Finset α)) (image (fun (s : Finset α) ↦ s.erase a) ({s ∈ 𝒜 ∪ ℬ | a ∈ s}))
    (image (fun (s : Finset α) ↦ s.erase a) ({s ∈ 𝒜 | a ∈ s}) ∪
      image (fun (s : Finset α) ↦ s.erase a) ({s ∈ ℬ | a ∈ s}))
simp_rw₁ :
  Eq (α := Finset (Finset α)) (image (fun (s : Finset α) ↦ s.erase a) ({s ∈ 𝒜 | a ∈ s} ∪ {s ∈ ℬ | a ∈ s}))
    (image (fun (s : Finset α) ↦ s.erase a) ({s ∈ 𝒜 | a ∈ s}) ∪
      image (fun (s : Finset α) ↦ s.erase a) ({s ∈ ℬ | a ∈ s}))
⊢ memberSubfamily a (𝒜 ∪ ℬ) = memberSubfamily a 𝒜 ∪ memberSubfamily a ℬ

Tactic:
simp_rw [memberSubfamily, filter_union, image_union]

Premises used: Finset.memberSubfamily, Finset.image_union, Finset.filter_union
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
rw : #({s ∈ 𝒜 | a ∈ s}) + #({s ∈ 𝒜 | a ∉ s}) = #𝒜
rw₁ : Set.InjOn (β := Finset α) (fun (s : Finset α) ↦ s.erase a) (↑({s ∈ 𝒜 | a ∈ s}) : Set (Finset α))
⊢ #(memberSubfamily a 𝒜) + #(nonMemberSubfamily a 𝒜) = #𝒜

Tactic:
rw [memberSubfamily, nonMemberSubfamily, card_image_of_injOn]

Premises used: Finset.memberSubfamily, Finset.nonMemberSubfamily, Finset.card_image_of_injOn
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
rw : #({s ∈ 𝒜 | a ∈ s}) + #({a_1 ∈ 𝒜 | a ∉ a_1})
| #𝒜

Tactic:
rw [← card_filter_add_card_filter_not (fun s => (a ∈ s))]

Premises used: Membership.mem, Finset.card_filter_add_card_filter_not
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
conv_rhs : #({s ∈ 𝒜 | a ∈ s}) + #({s ∈ 𝒜 | a ∉ s}) = #𝒜
conv_rhs₁ : #({s ∈ 𝒜 | a ∈ s}) + #({s ∈ 𝒜 | a ∉ s}) = #({s ∈ 𝒜 | a ∈ s}) + #({a_1 ∈ 𝒜 | a ∉ a_1})
⊢ #({s ∈ 𝒜 | a ∈ s}) + #({s ∈ 𝒜 | a ∉ s}) = #𝒜

Tactic:
conv_rhs => rw [← card_filter_add_card_filter_not (fun s => (a ∈ s))]

Premises used: Membership.mem, Finset.card_filter_add_card_filter_not
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
apply : (↑({s ∈ 𝒜 | a ∈ s}) : Set (Finset α)) ⊆ {s : Finset α | a ∈ s}
⊢ Set.InjOn (β := Finset α) (fun (s : Finset α) ↦ s.erase a) (↑({s ∈ 𝒜 | a ∈ s}) : Set (Finset α))

Tactic:
apply (erase_injOn' _).mono

Premises used: Finset.erase_injOn', Set.InjOn.mono
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ (↑({s ∈ 𝒜 | a ∈ s}) : Set (Finset α)) ⊆ {s : Finset α | a ∈ s}

Tactic:
simp
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
h :
  ∀ (s : Finset α),
    s ∈ memberSubfamily a 𝒜 ∪ nonMemberSubfamily a 𝒜 ↔
      Membership.mem (γ := Finset (Finset α)) (image (fun (s : Finset α) ↦ s.erase a) 𝒜) s
⊢ memberSubfamily a 𝒜 ∪ nonMemberSubfamily a 𝒜 = image (fun (s : Finset α) ↦ s.erase a) 𝒜

Tactic:
ext s
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
h : insert a s ∈ 𝒜 ∧ a ∉ s ∨ s ∈ 𝒜 ∧ a ∉ s ↔ ∃ a_1 ∈ 𝒜, a_1.erase a = s
⊢ s ∈ memberSubfamily a 𝒜 ∪ nonMemberSubfamily a 𝒜 ↔
    Membership.mem (γ := Finset (Finset α)) (image (fun (s : Finset α) ↦ s.erase a) 𝒜) s

Tactic:
simp only [mem_union, mem_memberSubfamily, mem_nonMemberSubfamily, mem_image]

Premises used: Finset.mem_image, Finset.mem_nonMemberSubfamily, Finset.mem_union, Finset.mem_memberSubfamily
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
h : insert a s ∈ 𝒜 ∧ a ∉ s ∨ s ∈ 𝒜 ∧ a ∉ s → ∃ a_2 ∈ 𝒜, a_2.erase a = s
h₁ : (∃ a_1 ∈ 𝒜, a_1.erase a = s) → insert a s ∈ 𝒜 ∧ a ∉ s ∨ s ∈ 𝒜 ∧ a ∉ s
⊢ insert a s ∈ 𝒜 ∧ a ∉ s ∨ s ∈ 𝒜 ∧ a ∉ s ↔ ∃ a_1 ∈ 𝒜, a_1.erase a = s

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
h : insert a s ∈ 𝒜 ∧ a ∉ s
⊢ ∃ a_1 ∈ 𝒜, a_1.erase a = s

Tactic:
⟨_, h.1, erase_insert h.2⟩

Premises used: Finset.erase_insert, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
h : insert a s ∈ 𝒜 ∧ a ∉ s
⊢ ∃ a_1 ∈ 𝒜, a_1.erase a = s

Tactic:
exact ⟨_, h.1, erase_insert h.2⟩
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
h : s ∈ 𝒜 ∧ a ∉ s
⊢ ∃ a_1 ∈ 𝒜, a_1.erase a = s

Tactic:
⟨_, h.1, erase_eq_of_notMem h.2⟩

Premises used: And.right, And.left, And.intro, Exists.intro, Finset.erase_eq_of_notMem
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
h : s ∈ 𝒜 ∧ a ∉ s
⊢ ∃ a_1 ∈ 𝒜, a_1.erase a = s

Tactic:
exact ⟨_, h.1, erase_eq_of_notMem h.2⟩
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜
pos : ∀ (ha : a ∈ s), insert a (s.erase a) ∈ 𝒜 ∧ a ∉ s.erase a ∨ s.erase a ∈ 𝒜 ∧ a ∉ s.erase a
neg : ∀ (ha : a ∉ s), insert a (s.erase a) ∈ 𝒜 ∧ a ∉ s.erase a ∨ s.erase a ∈ 𝒜 ∧ a ∉ s.erase a
⊢ insert a (s.erase a) ∈ 𝒜 ∧ a ∉ s.erase a ∨ s.erase a ∈ 𝒜 ∧ a ∉ s.erase a

Tactic:
by_cases ha : a ∈ s
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜
ha : a ∈ s
rwa rwa₁ rwa₂ rwa₃ : s ∈ 𝒜
⊢ insert a (s.erase a) ∈ 𝒜

Tactic:
rwa [insert_erase ha]

Premises used: Finset.insert_erase
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜
ha : a ∈ s
⊢ insert a (s.erase a) ∈ 𝒜 ∧ a ∉ s.erase a ∨ s.erase a ∈ 𝒜 ∧ a ∉ s.erase a

Tactic:
exact Or.inl ⟨by rwa [insert_erase ha], notMem_erase _ _⟩

Premises used: Or.inl
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜
ha : a ∉ s
rwa rwa₁ rwa₂ rwa₃ : s ∈ 𝒜
⊢ s.erase a ∈ 𝒜

Tactic:
rwa [erase_eq_of_notMem ha]

Premises used: Finset.erase_eq_of_notMem
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜
ha : a ∉ s
⊢ insert a (s.erase a) ∈ 𝒜 ∧ a ∉ s.erase a ∨ s.erase a ∈ 𝒜 ∧ a ∉ s.erase a

Tactic:
exact Or.inr ⟨by rwa [erase_eq_of_notMem ha], notMem_erase _ _⟩

Premises used: Or.inr
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : ∀ (a_1 : Finset α), a_1 ∈ memberSubfamily a (memberSubfamily a 𝒜) ↔ Membership.mem (γ := Finset (Finset α)) ∅ a_1
⊢ memberSubfamily a (memberSubfamily a 𝒜) = ∅

Tactic:
ext
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
a_1 : Finset α
⊢ a_1 ∈ memberSubfamily a (memberSubfamily a 𝒜) ↔ Membership.mem (γ := Finset (Finset α)) ∅ a_1

Tactic:
simp
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : ∀ (a_1 : Finset α), a_1 ∈ memberSubfamily a (nonMemberSubfamily a 𝒜) ↔ Membership.mem (γ := Finset (Finset α)) ∅ a_1
⊢ memberSubfamily a (nonMemberSubfamily a 𝒜) = ∅

Tactic:
ext
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
a_1 : Finset α
⊢ a_1 ∈ memberSubfamily a (nonMemberSubfamily a 𝒜) ↔ Membership.mem (γ := Finset (Finset α)) ∅ a_1

Tactic:
simp
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : ∀ (a_1 : Finset α), a_1 ∈ nonMemberSubfamily a (memberSubfamily a 𝒜) ↔ a_1 ∈ memberSubfamily a 𝒜
⊢ nonMemberSubfamily a (memberSubfamily a 𝒜) = memberSubfamily a 𝒜

Tactic:
ext
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
a_1 : Finset α
⊢ a_1 ∈ nonMemberSubfamily a (memberSubfamily a 𝒜) ↔ a_1 ∈ memberSubfamily a 𝒜

Tactic:
simp
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : ∀ (a_1 : Finset α), a_1 ∈ nonMemberSubfamily a (nonMemberSubfamily a 𝒜) ↔ a_1 ∈ nonMemberSubfamily a 𝒜
⊢ nonMemberSubfamily a (nonMemberSubfamily a 𝒜) = nonMemberSubfamily a 𝒜

Tactic:
ext
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
a_1 : Finset α
⊢ a_1 ∈ nonMemberSubfamily a (nonMemberSubfamily a 𝒜) ↔ a_1 ∈ nonMemberSubfamily a 𝒜

Tactic:
simp
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h𝒜 : ∀ s ∈ 𝒜, a ∉ s
h : ∀ (s : Finset α), s ∈ memberSubfamily a (image (insert a) 𝒜) ↔ s ∈ 𝒜
⊢ memberSubfamily a (image (insert a) 𝒜) = 𝒜

Tactic:
ext s
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h𝒜 : ∀ s ∈ 𝒜, a ∉ s
s : Finset α
h : (∃ a_1 ∈ 𝒜, insert a a_1 = insert a s) ∧ a ∉ s ↔ s ∈ 𝒜
⊢ s ∈ memberSubfamily a (image (insert a) 𝒜) ↔ s ∈ 𝒜

Tactic:
simp only [mem_memberSubfamily, mem_image]

Premises used: Finset.mem_image, Finset.mem_memberSubfamily
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h𝒜 : ∀ s ∈ 𝒜, a ∉ s
s : Finset α
⊢ (∃ a_1 ∈ 𝒜, insert a a_1 = insert a s) ∧ a ∉ s ↔ s ∈ 𝒜

Tactic:
⟨?_, fun hs ↦ ⟨⟨s, hs, rfl⟩, h𝒜 _ hs⟩⟩

Premises used: And.intro, Iff.intro, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h𝒜 : ∀ s ∈ 𝒜, a ∉ s
s : Finset α
h : (∃ a_1 ∈ 𝒜, insert a a_1 = insert a s) ∧ a ∉ s → s ∈ 𝒜
⊢ (∃ a_1 ∈ 𝒜, insert a a_1 = insert a s) ∧ a ∉ s ↔ s ∈ 𝒜

Tactic:
refine ⟨?_, fun hs ↦ ⟨⟨s, hs, rfl⟩, h𝒜 _ hs⟩⟩
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h𝒜 : ∀ s ∈ 𝒜, a ∉ s
s : Finset α
hs : a ∉ s
t : Finset α
ht : t ∈ 𝒜
hts : insert a t = insert a s
h h₁ h₂ h₃ : t ∈ 𝒜
⊢ s ∈ 𝒜

Tactic:
rwa [← insert_erase_invOn.2.injOn (h𝒜 _ ht) hs hts]

Premises used: Finset.insert_erase_invOn, And.right, Set.LeftInvOn.injOn
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
⊢ nonMemberSubfamily a (image (insert a) 𝒜) = ∅

Tactic:
simp [eq_empty_iff_forall_notMem]

Premises used: Finset.eq_empty_iff_forall_notMem
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
⊢ memberSubfamily a (image (fun (x : Finset α) ↦ x.erase a) 𝒜) = ∅

Tactic:
simp [eq_empty_iff_forall_notMem,
    (ne_of_mem_of_not_mem' (mem_insert_self _ _) (notMem_erase _ _)).symm]

Premises used: Finset.mem_insert_self, Finset.eq_empty_iff_forall_notMem, Ne.symm, Finset.notMem_erase, ne_of_mem_of_not_mem'
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : ∀ (s : Finset α), s ∈ image (insert a) (memberSubfamily a 𝒜) ↔ s ∈ {s ∈ 𝒜 | a ∈ s}
⊢ image (insert a) (memberSubfamily a 𝒜) = {s ∈ 𝒜 | a ∈ s}

Tactic:
ext s
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
h : (∃ (a_1 : Finset α), (insert a a_1 ∈ 𝒜 ∧ a ∉ a_1) ∧ insert a a_1 = s) ↔ s ∈ 𝒜 ∧ a ∈ s
⊢ s ∈ image (insert a) (memberSubfamily a 𝒜) ↔ s ∈ {s ∈ 𝒜 | a ∈ s}

Tactic:
simp only [mem_memberSubfamily, mem_image, mem_filter]

Premises used: Finset.mem_image, Finset.mem_filter, Finset.mem_memberSubfamily
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
⊢ (∃ (a_1 : Finset α), (insert a a_1 ∈ 𝒜 ∧ a ∉ a_1) ∧ insert a a_1 = s) ↔ s ∈ 𝒜 ∧ a ∈ s

Tactic:
⟨?_, fun ⟨hs, ha⟩ ↦ ⟨erase s a, ⟨?_, notMem_erase _ _⟩, insert_erase ha⟩⟩

Premises used: Membership.mem, Exists, Insert.insert, _private.0.Finset.image_insert_memberSubfamily.match_1, And, And.intro, Iff.intro, Exists.intro, Finset.notMem_erase, Finset.erase, Finset.insert_erase, Eq, Not
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
h : (∃ (a_1 : Finset α), (insert a a_1 ∈ 𝒜 ∧ a ∉ a_1) ∧ insert a a_1 = s) → s ∈ 𝒜 ∧ a ∈ s
h₁ : s ∈ 𝒜 ∧ a ∈ s → ∀ (hs : s ∈ 𝒜) (ha : a ∈ s), insert a (s.erase a) ∈ 𝒜
⊢ (∃ (a_1 : Finset α), (insert a a_1 ∈ 𝒜 ∧ a ∉ a_1) ∧ insert a a_1 = s) ↔ s ∈ 𝒜 ∧ a ∈ s

Tactic:
refine ⟨?_, fun ⟨hs, ha⟩ ↦ ⟨erase s a, ⟨?_, notMem_erase _ _⟩, insert_erase ha⟩⟩
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
hs : insert a s ∈ 𝒜
⊢ insert a s ∈ 𝒜 ∧ a ∈ insert a s

Tactic:
⟨hs, mem_insert_self _ _⟩

Premises used: Finset.mem_insert_self, And.intro
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
hs : insert a s ∈ 𝒜
⊢ insert a s ∈ 𝒜 ∧ a ∈ insert a s

Tactic:
exact ⟨hs, mem_insert_self _ _⟩
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
h_1 : s ∈ 𝒜 ∧ a ∈ s
hs : s ∈ 𝒜
ha : a ∈ s
h h₁ h₂ h₃ : s ∈ 𝒜
⊢ insert a (s.erase a) ∈ 𝒜

Tactic:
rwa [insert_erase ha]

Premises used: Finset.insert_erase
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
𝒜 : Finset (Finset α)
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
u : Finset α := 𝒜.sup id
have : ∀ (hu : ∀ s ∈ 𝒜, s ⊆ u), p 𝒜
⊢ p 𝒜

Tactic:
have hu : ∀ s ∈ 𝒜, s ⊆ u := fun s ↦ le_sup (f := id)
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
𝒜 : Finset (Finset α)
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
u : Finset α := 𝒜.sup id
hu : ∀ s ∈ 𝒜, s ⊆ u
clear_value : ∀ (u : Finset α) (hu : ∀ s ∈ 𝒜, s ⊆ u), p 𝒜
⊢ p 𝒜

Tactic:
clear_value u
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s ⊆ ∅
⊢ ∀ s ∈ 𝒜, s = ∅

Tactic:
simp_rw [subset_empty] at hu

Premises used: Finset.subset_empty
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s = ∅
⊢ 𝒜 = ∅ ∨ 𝒜 = {∅}

Tactic:
rw [← subset_singleton_iff', subset_singleton_iff] at hu

Premises used: Finset.subset_singleton_iff, Finset.subset_singleton_iff'
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
𝒜 : Finset (Finset α)
hu : 𝒜 = ∅ ∨ 𝒜 = {∅}
empty₁ : p ∅
empty₂ : p {∅}
⊢ p 𝒜

Tactic:
obtain rfl | rfl := hu

Premises used: rfl
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
⊢ p ∅

Tactic:
assumption
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
⊢ p {∅}

Tactic:
assumption
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
a : α
u : Finset α
h : a ∉ u
ih : ∀ (𝒜 : Finset (Finset α)) (hu : ∀ s ∈ 𝒜, s ⊆ u), p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s ⊆ insert a u
⊢ p 𝒜

Tactic:
subfamily a (ih _ ?_) (ih _ ?_)
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
a : α
u : Finset α
h : a ∉ u
ih : ∀ (𝒜 : Finset (Finset α)) (hu : ∀ s ∈ 𝒜, s ⊆ u), p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s ⊆ Insert.insert a u
insert : ∀ s ∈ nonMemberSubfamily a 𝒜, s ⊆ u
insert₁ : ∀ s ∈ memberSubfamily a 𝒜, s ⊆ u
⊢ p 𝒜

Tactic:
refine subfamily a (ih _ ?_) (ih _ ?_)
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
a : α
u : Finset α
h : a ∉ u
ih : ∀ (𝒜 : Finset (Finset α)) (hu : ∀ s ∈ 𝒜, s ⊆ u), p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s ⊆ Insert.insert a u
insert : ∀ s ∈ 𝒜, a ∉ s → s ⊆ u
⊢ ∀ s ∈ nonMemberSubfamily a 𝒜, s ⊆ u

Tactic:
simp only [mem_nonMemberSubfamily, and_imp]

Premises used: and_imp, Finset.mem_nonMemberSubfamily
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
a : α
u : Finset α
h : a ∉ u
ih : ∀ (𝒜 : Finset (Finset α)) (hu : ∀ s ∈ 𝒜, s ⊆ u), p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s ⊆ insert a u
⊢ ∀ s ∈ 𝒜, a ∉ s → s ⊆ u

Tactic:
fun s hs has ↦ (subset_insert_iff_of_notMem has).1 <| hu _ hs

Premises used: Finset.subset_insert_iff_of_notMem, Iff.mp
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
a : α
u : Finset α
h : a ∉ u
ih : ∀ (𝒜 : Finset (Finset α)) (hu : ∀ s ∈ 𝒜, s ⊆ u), p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s ⊆ insert a u
⊢ ∀ s ∈ 𝒜, a ∉ s → s ⊆ u

Tactic:
exact fun s hs has ↦ (subset_insert_iff_of_notMem has).1 <| hu _ hs

Premises used: Finset.subset_insert_iff_of_notMem, Iff.mp
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
a : α
u : Finset α
h : a ∉ u
ih : ∀ (𝒜 : Finset (Finset α)) (hu : ∀ s ∈ 𝒜, s ⊆ u), p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s ⊆ Insert.insert a u
insert : ∀ (s : Finset α), Insert.insert a s ∈ 𝒜 → a ∉ s → s ⊆ u
⊢ ∀ s ∈ memberSubfamily a 𝒜, s ⊆ u

Tactic:
simp only [mem_memberSubfamily, and_imp]

Premises used: and_imp, Finset.mem_memberSubfamily
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
a : α
u : Finset α
h : a ∉ u
ih : ∀ (𝒜 : Finset (Finset α)) (hu : ∀ s ∈ 𝒜, s ⊆ u), p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s ⊆ insert a u
⊢ ∀ (s : Finset α), insert a s ∈ 𝒜 → a ∉ s → s ⊆ u

Tactic:
fun s hs ha ↦ (insert_subset_insert_iff ha).1 <| hu _ hs

Premises used: Insert.insert, Iff.mp, Finset.insert_subset_insert_iff
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
a : α
u : Finset α
h : a ∉ u
ih : ∀ (𝒜 : Finset (Finset α)) (hu : ∀ s ∈ 𝒜, s ⊆ u), p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s ⊆ insert a u
⊢ ∀ (s : Finset α), insert a s ∈ 𝒜 → a ∉ s → s ⊆ u

Tactic:
exact fun s hs ha ↦ (insert_subset_insert_iff ha).1 <| hu _ hs

Premises used: Insert.insert, Iff.mp, Finset.insert_subset_insert_iff
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
𝒜 : Finset (Finset α)
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
u : Finset α
hu : ∀ s ∈ 𝒜, s ⊆ u
empty₁ : ∀ (𝒜 : Finset (Finset α)) (hu : ∀ s ∈ 𝒜, s ⊆ ∅), p 𝒜
insert :
  ∀ (a : α) (u : Finset α),
    a ∉ u →
      ∀ (ih : ∀ (𝒜 : Finset (Finset α)) (hu : ∀ s ∈ 𝒜, s ⊆ u), p 𝒜) (𝒜 : Finset (Finset α))
        (hu : ∀ s ∈ 𝒜, s ⊆ Insert.insert a u), p 𝒜
⊢ p 𝒜

Tactic:
induction u using Finset.induction generalizing 𝒜 with
  | empty =>
    simp_rw [subset_empty] at hu
    rw [← subset_singleton_iff', subset_singleton_iff] at hu
    obtain rfl | rfl := hu <;> assumption
  | insert a u _ ih =>
    refine subfamily a (ih _ ?_) (ih _ ?_)
    · simp only [mem_nonMemberSubfamily, and_imp]
      exact fun s hs has ↦ (subset_insert_iff_of_notMem has).1 <| hu _ hs
    · simp only [mem_memberSubfamily, and_imp]
      exact fun s hs ha ↦ (insert_subset_insert_iff ha).1 <| hu _ hs

Premises used: Finset.subset_empty, Finset.subset_insert_iff_of_notMem, and_imp, Insert.insert, Finset.mem_nonMemberSubfamily, Iff.mp, Finset.subset_singleton_iff, Finset.subset_singleton_iff', Finset.mem_memberSubfamily, Finset.insert_subset_insert_iff, rfl
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
𝒜 : Finset (Finset α)
empty : p ∅
singleton_empty : p {∅}
image_insert : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, (∀ s ∈ 𝒜, a ∉ s) → p 𝒜 → p (image (insert a) 𝒜)
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p ({s ∈ 𝒜 | a ∉ s}) → p ({s ∈ 𝒜 | a ∈ s}) → p 𝒜
⊢ p 𝒜

Tactic:
memberFamily_induction_on 𝒜 empty singleton_empty fun a 𝒜 h𝒜₀ h𝒜₁ ↦ subfamily a h𝒜₀ ?_

Premises used: Finset.memberFamily_induction_on
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
𝒜 : Finset (Finset α)
empty : p ∅
singleton_empty : p {∅}
image_insert : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, (∀ s ∈ 𝒜, a ∉ s) → p 𝒜 → p (image (insert a) 𝒜)
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p ({s ∈ 𝒜 | a ∉ s}) → p ({s ∈ 𝒜 | a ∈ s}) → p 𝒜
refine :
  ∀ (a : α) (𝒜 : Finset (Finset α)) (h𝒜₀ : p (nonMemberSubfamily a 𝒜)) (h𝒜₁ : p (memberSubfamily a 𝒜)),
    p ({s ∈ 𝒜 | a ∈ s})
⊢ p 𝒜

Tactic:
refine memberFamily_induction_on 𝒜 empty singleton_empty fun a 𝒜 h𝒜₀ h𝒜₁ ↦ subfamily a h𝒜₀ ?_