awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
refine_3 : (memberSubfamily a 𝒜).shatterer ⊆ 𝒜.shatterer
refine_3₁ : ℬ ⊆ 𝒜.shatterer
⊢ #((memberSubfamily a 𝒜).shatterer ∪ (nonMemberSubfamily a 𝒜).shatterer ∪ ℬ) ≤ #𝒜.shatterer

Tactic:
refine card_mono <| union_subset (union_subset ?_ <| shatterer_mono <| filter_subset _ _) ?_

Premises used: Finset.union_subset, Finset.shatterer_mono, Finset.filter_subset, Finset.card_mono
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
refine_3 : ∀ ⦃x : Finset α⦄, (memberSubfamily a 𝒜).Shatters x → 𝒜.Shatters x
⊢ (memberSubfamily a 𝒜).shatterer ⊆ 𝒜.shatterer

Tactic:
simp only [subset_iff, mem_shatterer]

Premises used: Finset.subset_iff, Finset.mem_shatterer
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s : Finset α
hs : (memberSubfamily a 𝒜).Shatters s
t : Finset α
ht : t ⊆ s
refine_3 : ∀ (u : Finset α) (hu : u ∈ memberSubfamily a 𝒜) (ht : s ∩ u ⊆ s), ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
⊢ ∃ u ∈ 𝒜, s ∩ u = t

Tactic:
obtain ⟨u, hu, rfl⟩ := hs ht

Premises used: rfl
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s : Finset α
hs : (memberSubfamily a 𝒜).Shatters s
u : Finset α
hu : u ∈ memberSubfamily a 𝒜
ht : s ∩ u ⊆ s
⊢ insert a u ∈ 𝒜 ∧ a ∉ u

Tactic:
rw [mem_memberSubfamily] at hu

Premises used: Finset.mem_memberSubfamily
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s : Finset α
hs : (memberSubfamily a 𝒜).Shatters s
u : Finset α
hu : u ∈ memberSubfamily a 𝒜
ht : s ∩ u ⊆ s
hu₁ : insert a u ∈ 𝒜 ∧ a ∉ u
⊢ s ∩ u ⊆ s

Tactic:
rw [mem_memberSubfamily] at hu

Premises used: Finset.mem_memberSubfamily
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s : Finset α
hs : (memberSubfamily a 𝒜).Shatters s
u : Finset α
hu : insert a u ∈ 𝒜 ∧ a ∉ u
ht : s ∩ u ⊆ s
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u

Tactic:
⟨insert a u, hu.1, inter_insert_of_notMem fun ha ↦ ?_⟩

Premises used: Insert.insert, And.left, Finset.inter_insert_of_notMem, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s : Finset α
hs : (memberSubfamily a 𝒜).Shatters s
u : Finset α
hu : insert a u ∈ 𝒜 ∧ a ∉ u
ht : s ∩ u ⊆ s
refine_3 : ∀ (ha : a ∈ s), False
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u

Tactic:
refine ⟨insert a u, hu.1, inter_insert_of_notMem fun ha ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s : Finset α
hs : (memberSubfamily a 𝒜).Shatters s
u : Finset α
hu : insert a u ∈ 𝒜 ∧ a ∉ u
ht : s ∩ u ⊆ s
ha : a ∈ s
refine_3 : ∀ (v : Finset α) (hv : v ∈ memberSubfamily a 𝒜) (hsv : s ∩ v = {a}), False
⊢ False

Tactic:
obtain ⟨v, hv, hsv⟩ := hs.exists_inter_eq_singleton ha

Premises used: Finset.Shatters.exists_inter_eq_singleton
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s : Finset α
hs : (memberSubfamily a 𝒜).Shatters s
u : Finset α
hu : insert a u ∈ 𝒜 ∧ a ∉ u
ht : s ∩ u ⊆ s
ha : a ∈ s
v : Finset α
hv : v ∈ memberSubfamily a 𝒜
hsv : s ∩ v = {a}
⊢ insert a v ∈ 𝒜 ∧ a ∉ v

Tactic:
rw [mem_memberSubfamily] at hv

Premises used: Finset.mem_memberSubfamily
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s : Finset α
hs : (memberSubfamily a 𝒜).Shatters s
u : Finset α
hu : insert a u ∈ 𝒜 ∧ a ∉ u
ht : s ∩ u ⊆ s
ha : a ∈ s
v : Finset α
hv : v ∈ memberSubfamily a 𝒜
hsv : s ∩ v = {a}
hv₁ : insert a v ∈ 𝒜 ∧ a ∉ v
⊢ s ∩ v = {a}

Tactic:
rw [mem_memberSubfamily] at hv

Premises used: Finset.mem_memberSubfamily
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s : Finset α
hs : (memberSubfamily a 𝒜).Shatters s
u : Finset α
hu : insert a u ∈ 𝒜 ∧ a ∉ u
ht : s ∩ u ⊆ s
ha : a ∈ s
v : Finset α
hv : insert a v ∈ 𝒜 ∧ a ∉ v
hsv : s ∩ v = {a}
⊢ insert a v ∈ 𝒜 ∧ ¬s ∩ v ⊆ v

Tactic:
rw [← singleton_subset_iff (a := a), ← hsv] at hv

Premises used: Finset.singleton_subset_iff
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s : Finset α
hs : (memberSubfamily a 𝒜).Shatters s
u : Finset α
hu : insert a u ∈ 𝒜 ∧ a ∉ u
ht : s ∩ u ⊆ s
ha : a ∈ s
v : Finset α
hv : insert a v ∈ 𝒜 ∧ a ∉ v
hsv : s ∩ v = {a}
hv₁ : insert a v ∈ 𝒜 ∧ ¬s ∩ v ⊆ v
⊢ s ∩ v = {a}

Tactic:
rw [← singleton_subset_iff (a := a), ← hsv] at hv

Premises used: Finset.singleton_subset_iff
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s : Finset α
hs : (memberSubfamily a 𝒜).Shatters s
u : Finset α
hu : insert a u ∈ 𝒜 ∧ a ∉ u
ht : s ∩ u ⊆ s
ha : a ∈ s
v : Finset α
hv : insert a v ∈ 𝒜 ∧ ¬s ∩ v ⊆ v
hsv : s ∩ v = {a}
⊢ False

Tactic:
hv.2 inter_subset_right

Premises used: Finset.inter_subset_right, And.right
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s : Finset α
hs : (memberSubfamily a 𝒜).Shatters s
u : Finset α
hu : insert a u ∈ 𝒜 ∧ a ∉ u
ht : s ∩ u ⊆ s
ha : a ∈ s
v : Finset α
hv : insert a v ∈ 𝒜 ∧ ¬s ∩ v ⊆ v
hsv : s ∩ v = {a}
⊢ False

Tactic:
exact hv.2 inter_subset_right

Premises used: Finset.inter_subset_right, And.right
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
⊢ ℬ ⊆ 𝒜.shatterer

Tactic:
forall_mem_image.2 fun s hs ↦ mem_shatterer.2 fun t ht ↦ ?_

Premises used: Iff.mpr, Set.Mem, setOf, Finset.forall_mem_image, Finset.mem_shatterer
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
refine_3 :
  ∀ (s : Finset α) (hs : s ∈ (memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer) (t : Finset α)
    (ht : t ⊆ insert a s), ∃ u ∈ 𝒜, insert a s ∩ u = t
⊢ ℬ ⊆ 𝒜.shatterer

Tactic:
refine forall_mem_image.2 fun s hs ↦ mem_shatterer.2 fun t ht ↦ ?_

Premises used: Iff.mpr, Finset.forall_mem_image, Finset.mem_shatterer
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s : Finset α
hs : s ∈ (memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer
t : Finset α
ht : t ⊆ insert a s
⊢ (memberSubfamily a 𝒜).Shatters s ∧ (nonMemberSubfamily a 𝒜).Shatters s

Tactic:
simp only [mem_inter, mem_shatterer] at hs

Premises used: Finset.mem_inter, Finset.mem_shatterer
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s t : Finset α
ht : t ⊆ insert a s
hs : (memberSubfamily a 𝒜).Shatters s ∧ (nonMemberSubfamily a 𝒜).Shatters s
⊢ t.erase a ⊆ s

Tactic:
rw [subset_insert_iff] at ht

Premises used: Finset.subset_insert_iff
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s t : Finset α
ht : t ⊆ insert a s
hs : (memberSubfamily a 𝒜).Shatters s ∧ (nonMemberSubfamily a 𝒜).Shatters s
ht₁ : t.erase a ⊆ s
⊢ (memberSubfamily a 𝒜).Shatters s ∧ (nonMemberSubfamily a 𝒜).Shatters s

Tactic:
rw [subset_insert_iff] at ht

Premises used: Finset.subset_insert_iff
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s t : Finset α
ht : t.erase a ⊆ s
hs : (memberSubfamily a 𝒜).Shatters s ∧ (nonMemberSubfamily a 𝒜).Shatters s
pos : ∀ (ha : a ∈ t), ∃ u ∈ 𝒜, insert a s ∩ u = t
neg : ∀ (ha : a ∉ t), ∃ u ∈ 𝒜, insert a s ∩ u = t
⊢ ∃ u ∈ 𝒜, insert a s ∩ u = t

Tactic:
by_cases ha : a ∈ t
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s t : Finset α
ht : t.erase a ⊆ s
hs : (memberSubfamily a 𝒜).Shatters s ∧ (nonMemberSubfamily a 𝒜).Shatters s
ha : a ∈ t
pos : ∀ (u : Finset α) (hu : u ∈ memberSubfamily a 𝒜) (hsu : s ∩ u = t.erase a), ∃ u ∈ 𝒜, insert a s ∩ u = t
⊢ ∃ u ∈ 𝒜, insert a s ∩ u = t

Tactic:
obtain ⟨u, hu, hsu⟩ := hs.1 ht

Premises used: And.left
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s t : Finset α
ht : t.erase a ⊆ s
hs : (memberSubfamily a 𝒜).Shatters s ∧ (nonMemberSubfamily a 𝒜).Shatters s
ha : a ∈ t
u : Finset α
hu : u ∈ memberSubfamily a 𝒜
hsu : s ∩ u = t.erase a
⊢ insert a u ∈ 𝒜 ∧ a ∉ u

Tactic:
rw [mem_memberSubfamily] at hu

Premises used: Finset.mem_memberSubfamily
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s t : Finset α
ht : t.erase a ⊆ s
hs : (memberSubfamily a 𝒜).Shatters s ∧ (nonMemberSubfamily a 𝒜).Shatters s
ha : a ∈ t
u : Finset α
hu : u ∈ memberSubfamily a 𝒜
hsu : s ∩ u = t.erase a
hu₁ : insert a u ∈ 𝒜 ∧ a ∉ u
⊢ s ∩ u = t.erase a

Tactic:
rw [mem_memberSubfamily] at hu

Premises used: Finset.mem_memberSubfamily
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s t : Finset α
ht : t.erase a ⊆ s
hs : (memberSubfamily a 𝒜).Shatters s ∧ (nonMemberSubfamily a 𝒜).Shatters s
ha : a ∈ t
u : Finset α
hu : insert a u ∈ 𝒜 ∧ a ∉ u
hsu : s ∩ u = t.erase a
⊢ ∃ u ∈ 𝒜, insert a s ∩ u = t

Tactic:
⟨_, hu.1, ?_⟩

Premises used: And.left, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s t : Finset α
ht : t.erase a ⊆ s
hs : (memberSubfamily a 𝒜).Shatters s ∧ (nonMemberSubfamily a 𝒜).Shatters s
ha : a ∈ t
u : Finset α
hu : insert a u ∈ 𝒜 ∧ a ∉ u
hsu : s ∩ u = t.erase a
pos : insert a s ∩ insert a u = t
⊢ ∃ u ∈ 𝒜, insert a s ∩ u = t

Tactic:
refine ⟨_, hu.1, ?_⟩
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s t : Finset α
ht : t.erase a ⊆ s
hs : (memberSubfamily a 𝒜).Shatters s ∧ (nonMemberSubfamily a 𝒜).Shatters s
ha : a ∈ t
u : Finset α
hu : insert a u ∈ 𝒜 ∧ a ∉ u
hsu : s ∩ u = t.erase a
pos : insert a (s ∩ u) = t
pos₁ : insert a (t.erase a) = t
pos₂ pos₃ : t = t
⊢ insert a s ∩ insert a u = t

Tactic:
rw [← insert_inter_distrib, hsu, insert_erase ha]

Premises used: Finset.insert_inter_distrib, Finset.insert_erase
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s t : Finset α
ht : t.erase a ⊆ s
hs : (memberSubfamily a 𝒜).Shatters s ∧ (nonMemberSubfamily a 𝒜).Shatters s
ha : a ∉ t
neg : ∀ (u : Finset α) (hu : u ∈ nonMemberSubfamily a 𝒜) (hsu : s ∩ u = t.erase a), ∃ u ∈ 𝒜, insert a s ∩ u = t
⊢ ∃ u ∈ 𝒜, insert a s ∩ u = t

Tactic:
obtain ⟨u, hu, hsu⟩ := hs.2 ht

Premises used: And.right
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s t : Finset α
ht : t.erase a ⊆ s
hs : (memberSubfamily a 𝒜).Shatters s ∧ (nonMemberSubfamily a 𝒜).Shatters s
ha : a ∉ t
u : Finset α
hu : u ∈ nonMemberSubfamily a 𝒜
hsu : s ∩ u = t.erase a
⊢ u ∈ 𝒜 ∧ a ∉ u

Tactic:
rw [mem_nonMemberSubfamily] at hu

Premises used: Finset.mem_nonMemberSubfamily
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s t : Finset α
ht : t.erase a ⊆ s
hs : (memberSubfamily a 𝒜).Shatters s ∧ (nonMemberSubfamily a 𝒜).Shatters s
ha : a ∉ t
u : Finset α
hu : u ∈ nonMemberSubfamily a 𝒜
hsu : s ∩ u = t.erase a
hu₁ : u ∈ 𝒜 ∧ a ∉ u
⊢ s ∩ u = t.erase a

Tactic:
rw [mem_nonMemberSubfamily] at hu

Premises used: Finset.mem_nonMemberSubfamily
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s t : Finset α
ht : t.erase a ⊆ s
hs : (memberSubfamily a 𝒜).Shatters s ∧ (nonMemberSubfamily a 𝒜).Shatters s
ha : a ∉ t
u : Finset α
hu : u ∈ 𝒜 ∧ a ∉ u
hsu : s ∩ u = t.erase a
⊢ ∃ u ∈ 𝒜, insert a s ∩ u = t

Tactic:
⟨_, hu.1, ?_⟩

Premises used: And.left, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜_1 : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s t : Finset α
ht : t.erase a ⊆ s
hs : (memberSubfamily a 𝒜).Shatters s ∧ (nonMemberSubfamily a 𝒜).Shatters s
ha : a ∉ t
u : Finset α
hu : u ∈ 𝒜 ∧ a ∉ u
hsu : s ∩ u = t.erase a
neg : insert a s ∩ u = t
⊢ ∃ u ∈ 𝒜, insert a s ∩ u = t

Tactic:
refine ⟨_, hu.1, ?_⟩