awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
h : t ⊆ s
hs : 𝒜.Shatters s
v : Finset α
hv : v ∈ 𝒜
hu : s ∩ v ⊆ t
⊢ ∃ u ∈ 𝒜, t ∩ u = s ∩ v

Tactic:
exact ⟨v, hv, inf_congr_right hu <| inf_le_of_left_le h⟩
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
⊢ ∃ t ∈ 𝒜, s ⊆ t

Tactic:
let ⟨t, ht, hst⟩ := h Subset.rfl; ⟨t, ht, inter_eq_left.1 hst⟩

Premises used: _private.0.Finset.Shatters.exists_superset.match_1, Finset.Subset.rfl, Membership.mem, Exists, HasSubset.Subset, And, And.intro, Exists.intro, Iff.mp, Finset.inter_eq_left
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : ∀ t ⊆ s, t ∈ 𝒜
⊢ 𝒜.Shatters s

Tactic:
fun t ht ↦ ⟨t, h _ ht, inter_eq_right.2 ht⟩

Premises used: Iff.mpr, And.intro, Finset.inter_eq_right, Exists.intro, Finset.Shatters
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
⊢ 𝒜.Nonempty

Tactic:
let ⟨t, ht, _⟩ := h Subset.rfl; ⟨t, ht⟩

Premises used: _private.0.Finset.Shatters.exists_superset.match_1, Finset.Subset.rfl, Exists.intro, Finset.Nonempty
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
h : 𝒜.Nonempty
t : Finset α
ht : t ⊆ ∅
s : Finset α
hs : s ∈ 𝒜
rwa : ∅ = t
rwa₁ : t = ∅
rwa₂ rwa₃ rwa₄ rwa₅ : t ⊆ ∅
⊢ ∅ ∩ s = t

Tactic:
rwa [empty_inter, eq_comm, ← subset_empty]

Premises used: Finset.empty_inter, Finset.subset_empty, eq_comm
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
u : Finset α
left : u ∈ 𝒜
⊢ s ∩ u ⊆ s

Tactic:
inter_subset_left

Premises used: Finset.inter_subset_left
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
u : Finset α
left : u ∈ 𝒜
⊢ s ∩ u ⊆ s

Tactic:
exact inter_subset_left

Premises used: Finset.inter_subset_left
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
h₁ : ∀ (t : Finset α), Membership.mem (γ := Finset (Finset α)) (image (fun (t : Finset α) ↦ s ∩ t) 𝒜) t ↔ t ∈ s.powerset
⊢ image (fun (t : Finset α) ↦ s ∩ t) 𝒜 = s.powerset

Tactic:
ext t
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
t : Finset α
h₁ : (∃ a ∈ 𝒜, s ∩ a = t) ↔ t ∈ s.powerset
h₂ : (∃ a ∈ 𝒜, s ∩ a = t) ↔ t ⊆ s
h₃ h₄ : (∃ a ∈ 𝒜, s ∩ a = t) ↔ ∃ u ∈ 𝒜, s ∩ u = t
⊢ Membership.mem (γ := Finset (Finset α)) (image (fun (t : Finset α) ↦ s ∩ t) 𝒜) t ↔ t ∈ s.powerset

Tactic:
rw [mem_image, mem_powerset, h.subset_iff]

Premises used: Finset.mem_image, Finset.Shatters.subset_iff, Finset.mem_powerset
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : image (fun (t : Finset α) ↦ s ∩ t) 𝒜 = s.powerset
t : Finset α
ht : t ⊆ s
rwa : ∀ (ht : t ∈ s.powerset), ∃ u ∈ 𝒜, s ∩ u = t
rwa₁ : ∀ (ht : Membership.mem (γ := Finset (Finset α)) (image (fun (t : Finset α) ↦ s ∩ t) 𝒜) t), ∃ u ∈ 𝒜, s ∩ u = t
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (ht : ∃ a ∈ 𝒜, s ∩ a = t), ∃ u ∈ 𝒜, s ∩ u = t
⊢ ∃ u ∈ 𝒜, s ∩ u = t

Tactic:
rwa [← mem_powerset, ← h, mem_image] at ht

Premises used: Finset.mem_image, Finset.mem_powerset
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
inst_1 : Fintype α
⊢ Shatters univ s

Tactic:
shatters_of_forall_subset fun _ _ ↦ mem_univ _

Premises used: Finset.mem_univ, Finset.shatters_of_forall_subset
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
inst_1 : Fintype α
rw : Eq (α := Finset (Finset α)) (image (fun (t : Finset α) ↦ univ ∩ t) 𝒜) univ ↔ 𝒜 = univ
⊢ 𝒜.Shatters univ ↔ 𝒜 = univ

Tactic:
rw [shatters_iff, powerset_univ]

Premises used: Finset.shatters_iff, Finset.powerset_univ
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
inst_1 : Fintype α
simp_rw : Eq (α := Finset (Finset α)) (image (fun (t : Finset α) ↦ t) 𝒜) univ ↔ 𝒜 = univ
⊢ Eq (α := Finset (Finset α)) (image (fun (t : Finset α) ↦ univ ∩ t) 𝒜) univ ↔ 𝒜 = univ

Tactic:
simp_rw [univ_inter, image_id']

Premises used: Finset.image_id', Finset.univ_inter
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ 𝒜.shatterer ↔ 𝒜.Shatters s

Tactic:
mem_filter.trans <| and_iff_right_of_imp fun h ↦ ?_

Premises used: Set.Mem, setOf, Iff.trans, Finset.mem_filter, and_iff_right_of_imp
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
refine : ∀ (h : 𝒜.Shatters s), s ∈ 𝒜.biUnion powerset
⊢ s ∈ 𝒜.shatterer ↔ 𝒜.Shatters s

Tactic:
refine mem_filter.trans <| and_iff_right_of_imp fun h ↦ ?_

Premises used: Iff.trans, Finset.mem_filter, and_iff_right_of_imp
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
simp_rw : ∃ a ∈ 𝒜, s ⊆ a
⊢ s ∈ 𝒜.biUnion powerset

Tactic:
simp_rw [mem_biUnion, mem_powerset]

Premises used: Finset.mem_powerset, Finset.mem_biUnion
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
⊢ ∃ a ∈ 𝒜, s ⊆ a

Tactic:
h.exists_superset

Premises used: Finset.Shatters.exists_superset
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
⊢ ∃ a ∈ 𝒜, s ⊆ a

Tactic:
exact h.exists_superset

Premises used: Finset.Shatters.exists_superset
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h : 𝒜 ⊆ ℬ
x : Finset α
⊢ x ∈ 𝒜.shatterer → x ∈ ℬ.shatterer

Tactic:
simpa using Shatters.mono_left h

Premises used: Finset.Shatters.mono_left
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
h : IsLowerSet (↑𝒜 : Set (Finset α))
⊢ 𝒜 ⊆ 𝒜.shatterer

Tactic:
fun _s hs ↦ mem_shatterer.2 fun t ht ↦ ⟨t, h ht hs, inter_eq_right.2 ht⟩

Premises used: Iff.mpr, And.intro, Finset.inter_eq_right, Exists.intro, Finset.mem_shatterer
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
⊢ t ≤ s → s ∈ (↑𝒜.shatterer : Set (Finset α)) → t ∈ (↑𝒜.shatterer : Set (Finset α))

Tactic:
simpa using Shatters.mono_right

Premises used: Finset.Shatters.mono_right
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
⊢ 𝒜.shatterer = 𝒜 ↔ IsLowerSet (↑𝒜 : Set (Finset α))

Tactic:
⟨fun h ↦ ?_, fun h ↦ Subset.antisymm (fun s hs ↦ ?_) <| subset_shatterer h⟩

Premises used: Iff.intro, Finset.subset_shatterer, Finset.Subset.antisymm
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
refine_1 : ∀ (h : 𝒜.shatterer = 𝒜), IsLowerSet (↑𝒜 : Set (Finset α))
refine_2 : ∀ (h : IsLowerSet (↑𝒜 : Set (Finset α))) (s : Finset α) (hs : s ∈ 𝒜.shatterer), s ∈ 𝒜
⊢ 𝒜.shatterer = 𝒜 ↔ IsLowerSet (↑𝒜 : Set (Finset α))

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ Subset.antisymm (fun s hs ↦ ?_) <| subset_shatterer h⟩
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
h : 𝒜.shatterer = 𝒜
refine_1 : IsLowerSet (↑𝒜.shatterer : Set (Finset α))
⊢ IsLowerSet (↑𝒜 : Set (Finset α))

Tactic:
rw [← h]
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
h : 𝒜.shatterer = 𝒜
⊢ IsLowerSet (↑𝒜.shatterer : Set (Finset α))

Tactic:
isLowerSet_shatterer _

Premises used: Finset.isLowerSet_shatterer
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
h : 𝒜.shatterer = 𝒜
⊢ IsLowerSet (↑𝒜.shatterer : Set (Finset α))

Tactic:
exact isLowerSet_shatterer _

Premises used: Finset.isLowerSet_shatterer
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
h : IsLowerSet (↑𝒜 : Set (Finset α))
s : Finset α
hs : s ∈ 𝒜.shatterer
refine_2 : ∀ (t : Finset α) (ht : t ∈ 𝒜) (hst : s ⊆ t), s ∈ 𝒜
⊢ s ∈ 𝒜

Tactic:
obtain ⟨t, ht, hst⟩ := (mem_shatterer.1 hs).exists_superset

Premises used: Finset.Shatters.exists_superset, Iff.mp, Finset.mem_shatterer
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
h : IsLowerSet (↑𝒜 : Set (Finset α))
s : Finset α
hs : s ∈ 𝒜.shatterer
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
⊢ s ∈ 𝒜

Tactic:
h hst ht
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
h : IsLowerSet (↑𝒜 : Set (Finset α))
s : Finset α
hs : s ∈ 𝒜.shatterer
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
⊢ s ∈ 𝒜

Tactic:
exact h hst ht
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
⊢ 𝒜.shatterer.shatterer = 𝒜.shatterer

Tactic:
simp
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
simp_rw : s ∈ 𝒜.shatterer.shatterer ↔ s ∈ 𝒜.shatterer
⊢ 𝒜.shatterer.Shatters s ↔ 𝒜.Shatters s

Tactic:
simp_rw [← mem_shatterer, shatterer_idem]

Premises used: Finset.shatterer_idem, Finset.mem_shatterer
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
a : α
h : ∀ t ∈ 𝒜, a ∉ t
ht : 𝒜.Shatters t
obtain : ∀ (u : Finset α) (hu : u ∈ 𝒜) (htu : t ⊆ u), a ∉ t
⊢ a ∉ t

Tactic:
obtain ⟨u, hu, htu⟩ := ht.exists_superset

Premises used: Finset.Shatters.exists_superset
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
a : α
h : ∀ t ∈ 𝒜, a ∉ t
ht : 𝒜.Shatters t
u : Finset α
hu : u ∈ 𝒜
htu : t ⊆ u
⊢ a ∉ t

Tactic:
notMem_mono htu <| h u hu

Premises used: Finset.notMem_mono
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
a : α
h : ∀ t ∈ 𝒜, a ∉ t
ht : 𝒜.Shatters t
u : Finset α
hu : u ∈ 𝒜
htu : t ⊆ u
⊢ a ∉ t

Tactic:
exact notMem_mono htu <| h u hu

Premises used: Finset.notMem_mono
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
⊢ #𝒜 ≤ #𝒜.shatterer

Tactic:
memberFamily_induction_on 𝒜 ?_ ?_ ?_

Premises used: Finset.memberFamily_induction_on
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
refine_1 : card.{u_1} (α := Finset α) ∅ ≤ card.{u_1} (α := Finset α) (shatterer ∅)
refine_2 : card (α := Finset α) {∅} ≤ card (α := Finset α) {∅}
refine_3 :
  ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄,
    #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer →
      #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer → #𝒜 ≤ #𝒜.shatterer
⊢ #𝒜 ≤ #𝒜.shatterer

Tactic:
refine memberFamily_induction_on 𝒜 ?_ ?_ ?_
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
⊢ card.{u_1} (α := Finset α) ∅ ≤ card.{u_1} (α := Finset α) (shatterer ∅)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
⊢ card (α := Finset α) {∅} ≤ card (α := Finset α) {∅}

Tactic:
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)
⊢ #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)

Tactic:
card_image_of_injOn <| insert_erase_invOn.2.injOn.mono ?_

Premises used: Finset.insert_erase_invOn, And.right, Set.InjOn.mono, Finset.card_image_of_injOn, Set.LeftInvOn.injOn
-- 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)
refine :
  (↑((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer) : Set (Finset α)) ⊆ {s : Finset α | a ∉ s}
⊢ #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)

Tactic:
refine card_image_of_injOn <| insert_erase_invOn.2.injOn.mono ?_

Premises used: Finset.insert_erase_invOn, And.right, Set.InjOn.mono, Finset.card_image_of_injOn, Set.LeftInvOn.injOn
-- 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)
simp : ∀ (x : Finset α), (memberSubfamily a 𝒜).Shatters x → (nonMemberSubfamily a 𝒜).Shatters x → a ∉ x
⊢ (↑((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer) : Set (Finset α)) ⊆ {s : Finset α | a ∉ s}

Tactic:
simp only [coe_inter, Set.subset_def, Set.mem_inter_iff, mem_coe, Set.mem_setOf_eq, and_imp,
      mem_shatterer]

Premises used: Set.subset_def, and_imp, Set.mem_inter_iff, Set.mem_setOf_eq, Finset.coe_inter, Finset.mem_coe, 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)
⊢ ∀ (x : Finset α), (memberSubfamily a 𝒜).Shatters x → (nonMemberSubfamily a 𝒜).Shatters x → a ∉ x

Tactic:
fun s _ ↦ aux (fun t ht ↦ (mem_filter.1 ht).2)

Premises used: _private.0.Finset.aux, And.right, Iff.mp, Finset.mem_filter
-- 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)
⊢ ∀ (x : Finset α), (memberSubfamily a 𝒜).Shatters x → (nonMemberSubfamily a 𝒜).Shatters x → a ∉ x

Tactic:
exact fun s _ ↦ aux (fun t ht ↦ (mem_filter.1 ht).2)

Premises used: _private.0.Finset.aux, And.right, Iff.mp, Finset.mem_filter
-- 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)
⊢ #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)

Tactic:
have hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer) := by
    refine card_image_of_injOn <| insert_erase_invOn.2.injOn.mono ?_
    simp only [coe_inter, Set.subset_def, Set.mem_inter_iff, mem_coe, Set.mem_setOf_eq, and_imp,
      mem_shatterer]
    exact fun s _ ↦ aux (fun t ht ↦ (mem_filter.1 ht).2)
-- 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 𝒜) + #(nonMemberSubfamily a 𝒜) ≤ #𝒜.shatterer
⊢ #𝒜 ≤ #𝒜.shatterer

Tactic:
rw [← card_memberSubfamily_add_card_nonMemberSubfamily a]

Premises used: Finset.card_memberSubfamily_add_card_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)
⊢ #(memberSubfamily a 𝒜) + #(nonMemberSubfamily a 𝒜) ≤ #𝒜.shatterer

Tactic:
(Nat.add_le_add ih₁ ih₀).trans ?_

Premises used: Nat.add_le_add, LE.le.trans
-- 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 + #(nonMemberSubfamily a 𝒜).shatterer ≤ #𝒜.shatterer
⊢ #(memberSubfamily a 𝒜) + #(nonMemberSubfamily a 𝒜) ≤ #𝒜.shatterer

Tactic:
refine (Nat.add_le_add ih₁ ih₀).trans ?_

Premises used: Nat.add_le_add, LE.le.trans
-- 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 ∪ (nonMemberSubfamily a 𝒜).shatterer ∪ ℬ) ≤ #𝒜.shatterer
refine_3₁ : Disjoint ((memberSubfamily a 𝒜).shatterer ∪ (nonMemberSubfamily a 𝒜).shatterer) ℬ
⊢ #(memberSubfamily a 𝒜).shatterer + #(nonMemberSubfamily a 𝒜).shatterer ≤ #𝒜.shatterer

Tactic:
rw [← card_union_add_card_inter, ← hℬ, ← card_union_of_disjoint]

Premises used: Finset.card_union_add_card_inter, Finset.card_union_of_disjoint
-- 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 :
  ∀ ⦃a_1 : Finset α⦄,
    (memberSubfamily a 𝒜).Shatters a_1 ∨ (nonMemberSubfamily a 𝒜).Shatters a_1 →
      ∀ x ∈ (memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer, ¬insert a x = a_1
⊢ Disjoint ((memberSubfamily a 𝒜).shatterer ∪ (nonMemberSubfamily a 𝒜).shatterer) ℬ

Tactic:
simp only [ℬ, disjoint_left, mem_union, mem_shatterer, mem_image, not_exists, not_and]

Premises used: Finset.mem_image, not_exists, Finset.mem_union, Finset.disjoint_left, not_and, 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 (insert a s)
⊢ False

Tactic:
aux (fun t ht ↦ (mem_memberSubfamily.1 ht).2) hs <| mem_insert_self _ _

Premises used: Finset.mem_insert_self, _private.0.Finset.aux, And.right, Iff.mp, 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 (insert a s)
⊢ False

Tactic:
exact aux (fun t ht ↦ (mem_memberSubfamily.1 ht).2) hs <| mem_insert_self _ _

Premises used: Finset.mem_insert_self, _private.0.Finset.aux, And.right, Iff.mp, 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 : (nonMemberSubfamily a 𝒜).Shatters (insert a s)
⊢ False

Tactic:
aux (fun t ht ↦ (mem_nonMemberSubfamily.1 ht).2) hs <| mem_insert_self _ _

Premises used: Finset.mem_insert_self, Finset.mem_nonMemberSubfamily, _private.0.Finset.aux, And.right, Iff.mp
-- 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 : (nonMemberSubfamily a 𝒜).Shatters (insert a s)
⊢ False

Tactic:
exact aux (fun t ht ↦ (mem_nonMemberSubfamily.1 ht).2) hs <| mem_insert_self _ _

Premises used: Finset.mem_insert_self, Finset.mem_nonMemberSubfamily, _private.0.Finset.aux, And.right, Iff.mp
-- 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)
⊢ #((memberSubfamily a 𝒜).shatterer ∪ (nonMemberSubfamily a 𝒜).shatterer ∪ ℬ) ≤ #𝒜.shatterer

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

Premises used: Finset.union_subset, Finset.shatterer_mono, Finset.filter_subset, Finset.card_mono