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)
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 : s ∩ u = t
neg₁ : t.erase a = t
neg₂ neg₃ neg₄ neg₅ : a ∉ t
⊢ insert a s ∩ u = t

Tactic:
rwa [insert_inter_of_notMem hu.2, hsu, erase_eq_self]

Premises used: Finset.insert_inter_of_notMem, And.right, Finset.erase_eq_self
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
t : Finset α
ht : t ⊆ s
obtain : ∀ (u : Finset α) (hu : u ∈ 𝓓 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 α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
hu : u ∈ 𝓓 a 𝒜
ht : s ∩ u ⊆ s
⊢ u ∈ 𝒜 ∧ u.erase a ∈ 𝒜 ∨ u ∉ 𝒜 ∧ insert a u ∈ 𝒜

Tactic:
rw [Down.mem_compression] at hu

Premises used: Down.mem_compression
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
hu : u ∈ 𝓓 a 𝒜
ht : s ∩ u ⊆ s
hu₁ : u ∈ 𝒜 ∧ u.erase a ∈ 𝒜 ∨ u ∉ 𝒜 ∧ insert a u ∈ 𝒜
⊢ s ∩ u ⊆ s

Tactic:
rw [Down.mem_compression] at hu

Premises used: Down.mem_compression
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
hu : u ∈ 𝒜 ∧ u.erase a ∈ 𝒜 ∨ u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ht : s ∩ u ⊆ s
inl : ∀ (hu : u ∈ 𝒜 ∧ u.erase a ∈ 𝒜), ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
inr : ∀ (hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜), ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u

Tactic:
obtain hu | hu := hu
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∈ 𝒜 ∧ u.erase a ∈ 𝒜
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u

Tactic:
⟨u, hu.1, rfl⟩

Premises used: And.left, And.intro, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∈ 𝒜 ∧ u.erase a ∈ 𝒜
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u

Tactic:
exact ⟨u, hu.1, rfl⟩
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
pos : ∀ (ha : a ∈ s), ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
neg : ∀ (ha : a ∉ s), ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u

Tactic:
by_cases ha : a ∈ s
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
pos : ∀ (v : Finset α) (hv : v ∈ 𝓓 a 𝒜) (hsv : s ∩ v = insert a (s ∩ u)), ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u

Tactic:
obtain ⟨v, hv, hsv⟩ := hs <| insert_subset ha ht

Premises used: Finset.insert_subset
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
v : Finset α
hv : v ∈ 𝓓 a 𝒜
hsv : s ∩ v = insert a (s ∩ u)
⊢ v ∈ 𝒜 ∧ v.erase a ∈ 𝒜 ∨ v ∉ 𝒜 ∧ insert a v ∈ 𝒜

Tactic:
rw [Down.mem_compression] at hv

Premises used: Down.mem_compression
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
v : Finset α
hv : v ∈ 𝓓 a 𝒜
hsv : s ∩ v = insert a (s ∩ u)
hv₁ : v ∈ 𝒜 ∧ v.erase a ∈ 𝒜 ∨ v ∉ 𝒜 ∧ insert a v ∈ 𝒜
⊢ s ∩ v = insert a (s ∩ u)

Tactic:
rw [Down.mem_compression] at hv

Premises used: Down.mem_compression
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
v : Finset α
hv : v ∈ 𝒜 ∧ v.erase a ∈ 𝒜 ∨ v ∉ 𝒜 ∧ insert a v ∈ 𝒜
hsv : s ∩ v = insert a (s ∩ u)
pos : ∀ (hv : v ∈ 𝒜 ∧ v.erase a ∈ 𝒜), ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
pos₁ : ∀ (hv : v ∉ 𝒜 ∧ insert a v ∈ 𝒜), ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u

Tactic:
obtain hv | hv := hv
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
v : Finset α
hsv : s ∩ v = insert a (s ∩ u)
hv : v ∈ 𝒜 ∧ v.erase a ∈ 𝒜
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u

Tactic:
⟨erase v a, hv.2, ?_⟩

Premises used: And.right, And.intro, Exists.intro, Finset.erase
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
v : Finset α
hsv : s ∩ v = insert a (s ∩ u)
hv : v ∈ 𝒜 ∧ v.erase a ∈ 𝒜
pos : s ∩ v.erase a = s ∩ u
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u

Tactic:
refine ⟨erase v a, hv.2, ?_⟩
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
v : Finset α
hsv : s ∩ v = insert a (s ∩ u)
hv : v ∈ 𝒜 ∧ v.erase a ∈ 𝒜
pos : a ∉ s ∩ u
⊢ s ∩ v.erase a = s ∩ u

Tactic:
rw [inter_erase, hsv, erase_insert]

Premises used: Finset.inter_erase, Finset.erase_insert
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha_1 : a ∈ s
v : Finset α
hsv : s ∩ v = insert a (s ∩ u)
hv : v ∈ 𝒜 ∧ v.erase a ∈ 𝒜
ha : a ∈ s ∩ u
pos :
  ∀ (hu : u ∉ 𝒜 ∧ u ∈ 𝒜) (ha : a ∈ s) (v : Finset α) (hsv : s ∩ v = insert a (s ∩ u)) (hv : v ∈ 𝒜 ∧ v.erase a ∈ 𝒜)
    (ha : a ∈ s ∩ u), False
⊢ False

Tactic:
rw [insert_eq_self.2 (mem_inter.1 ha).2] at hu

Premises used: Iff.mpr, Finset.insert_eq_self, And.right, Iff.mp, Finset.mem_inter
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ u ∈ 𝒜
ha_1 : a ∈ s
v : Finset α
hsv : s ∩ v = insert a (s ∩ u)
hv : v ∈ 𝒜 ∧ v.erase a ∈ 𝒜
ha : a ∈ s ∩ u
⊢ False

Tactic:
hu.1 hu.2

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ u ∈ 𝒜
ha_1 : a ∈ s
v : Finset α
hsv : s ∩ v = insert a (s ∩ u)
hv : v ∈ 𝒜 ∧ v.erase a ∈ 𝒜
ha : a ∈ s ∩ u
⊢ False

Tactic:
exact hu.1 hu.2

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
v : Finset α
hsv : s ∩ v = insert a (s ∩ u)
hv : v ∉ 𝒜 ∧ insert a v ∈ 𝒜
pos : ∀ (hv : v ∉ 𝒜 ∧ v ∈ 𝒜), ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
rw : a ∈ s ∩ v
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u

Tactic:
rw [insert_eq_self.2 <| inter_subset_right (s₁ := s) ?_] at hv

Premises used: Iff.mpr, Finset.inter_subset_right, Finset.insert_eq_self
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
v : Finset α
hsv : s ∩ v = insert a (s ∩ u)
hv : v ∉ 𝒜 ∧ v ∈ 𝒜
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u

Tactic:
cases hv.1 hv.2

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
v : Finset α
hsv : s ∩ v = insert a (s ∩ u)
hv : v ∉ 𝒜 ∧ insert a v ∈ 𝒜
rw : a ∈ insert a (s ∩ u)
⊢ a ∈ s ∩ v

Tactic:
rw [hsv]
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
v : Finset α
hsv : s ∩ v = insert a (s ∩ u)
hv : v ∉ 𝒜 ∧ insert a v ∈ 𝒜
⊢ a ∈ insert a (s ∩ u)

Tactic:
mem_insert_self _ _

Premises used: Finset.mem_insert_self
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
v : Finset α
hsv : s ∩ v = insert a (s ∩ u)
hv : v ∉ 𝒜 ∧ insert a v ∈ 𝒜
⊢ a ∈ insert a (s ∩ u)

Tactic:
exact mem_insert_self _ _

Premises used: Finset.mem_insert_self
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∉ s
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u

Tactic:
⟨insert a u, hu.2, ?_⟩

Premises used: Insert.insert, And.right, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∉ s
neg : s ∩ insert a u = s ∩ u
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u

Tactic:
refine ⟨insert a u, hu.2, ?_⟩
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∉ s
neg neg₁ : s ∩ u = s ∩ u
⊢ s ∩ insert a u = s ∩ u

Tactic:
rw [inter_insert_of_notMem ha]

Premises used: Finset.inter_insert_of_notMem
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
simp : ∀ ⦃x : Finset α⦄, (𝓓 a 𝒜).Shatters x → 𝒜.Shatters x
⊢ (𝓓 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 α
a : α
𝒜 : Finset (Finset α)
⊢ ∀ ⦃x : Finset α⦄, (𝓓 a 𝒜).Shatters x → 𝒜.Shatters x

Tactic:
fun s hs ↦ hs.of_compression

Premises used: Finset.Shatters.of_compression
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ ∀ ⦃x : Finset α⦄, (𝓓 a 𝒜).Shatters x → 𝒜.Shatters x

Tactic:
exact fun s hs ↦ hs.of_compression
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜ℬ : 𝒜 ⊆ ℬ
⊢ 𝒜.shatterer.sup card ≤ ℬ.shatterer.sup card

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
hs : 𝒜.Shatters s
⊢ #s ≤ 𝒜.vcDim

Tactic:
le_sup <| mem_shatterer.2 hs

Premises used: Iff.mpr, Finset.mem_shatterer, Finset.vcDim, Finset.le_sup
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ (𝓓 a 𝒜).vcDim ≤ 𝒜.vcDim

Tactic:
sup_mono <| shatterer_compress_subset_shatterer _ _

Premises used: Finset.shatterer_compress_subset_shatterer, Finset.sup_mono, Finset.vcDim
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
inst_1 : Fintype α
simp_rw : #𝒜.shatterer ≤ ∑ x ∈ Iic 𝒜.vcDim, card.{u_1} (α := Finset α) (powersetCard x univ)
⊢ #𝒜.shatterer ≤ ∑ k ∈ Iic 𝒜.vcDim, (Fintype.card α).choose k

Tactic:
simp_rw [← card_univ, ← card_powersetCard]

Premises used: Finset.card_univ, Finset.card_powersetCard
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
inst_1 : Fintype α
⊢ #𝒜.shatterer ≤ ∑ x ∈ Iic 𝒜.vcDim, card.{u_1} (α := Finset α) (powersetCard x univ)

Tactic:
(card_le_card fun s hs ↦ mem_biUnion.2 ⟨#s, ?_⟩).trans card_biUnion_le

Premises used: Iff.mpr, Finset.card_le_card, Exists.intro, Finset.card, Finset.card_biUnion_le, LE.le.trans, Finset.mem_biUnion
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
inst_1 : Fintype α
refine :
  ∀ (s : Finset α) (hs : s ∈ 𝒜.shatterer),
    #s ∈ Iic 𝒜.vcDim ∧ Membership.mem (γ := Finset (Finset α)) (powersetCard (#s) univ) s
⊢ #𝒜.shatterer ≤ ∑ x ∈ Iic 𝒜.vcDim, card.{u_1} (α := Finset α) (powersetCard x univ)

Tactic:
refine (card_le_card fun s hs ↦ mem_biUnion.2 ⟨#s, ?_⟩).trans card_biUnion_le

Premises used: Iff.mpr, Finset.card_le_card, Exists.intro, Finset.card, Finset.card_biUnion_le, LE.le.trans, Finset.mem_biUnion
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
inst_1 : Fintype α
s : Finset α
hs : s ∈ 𝒜.shatterer
⊢ #s ∈ Iic 𝒜.vcDim ∧ Membership.mem (γ := Finset (Finset α)) (powersetCard (#s) univ) s

Tactic:
⟨mem_Iic.2 (mem_shatterer.1 hs).card_le_vcDim, mem_powersetCard_univ.2 rfl⟩

Premises used: Iff.mpr, Finset.Shatters.card_le_vcDim, Finset.mem_Iic, And.intro, Finset.mem_powersetCard_univ, Iff.mp, rfl, Finset.mem_shatterer
-- Module: Mathlib.Combinatorics.SetFamily.Shatter
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
inst_1 : Fintype α
s : Finset α
hs : s ∈ 𝒜.shatterer
⊢ #s ∈ Iic 𝒜.vcDim ∧ Membership.mem (γ := Finset (Finset α)) (powersetCard (#s) univ) s

Tactic:
exact ⟨mem_Iic.2 (mem_shatterer.1 hs).card_le_vcDim, mem_powersetCard_univ.2 rfl⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
⊢ IsAcyclic.{u_1} (V := V) ⊥

Tactic:
fun _a _w hw ↦ hw.ne_bot rfl

Premises used: SimpleGraph.IsAcyclic, SimpleGraph.Walk.IsCycle.ne_bot, Not, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := V) (β := V') (⇑f : (a : V) → V')
h : G'.IsAcyclic
⊢ G.IsAcyclic

Tactic:
fun _ _ ↦ map_isCycle_iff_of_injective hinj |>.not.mp <| h _

Premises used: SimpleGraph.Walk.map, SimpleGraph.IsAcyclic, SimpleGraph.Walk.map_isCycle_iff_of_injective, Iff.not, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
f : G ↪g G'
h : G'.IsAcyclic
⊢ G.IsAcyclic

Tactic:
h.comap f f.injective

Premises used: SimpleGraph.IsAcyclic.comap
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
f : G ≃g G'
⊢ G.IsAcyclic ↔ G'.IsAcyclic

Tactic:
⟨fun h ↦ h.embedding f.symm, fun h ↦ h.embedding f⟩

Premises used: SimpleGraph.IsAcyclic.embedding, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
f : G ≃g G'
⊢ G.IsTree ↔ G'.IsTree

Tactic:
⟨fun ⟨hc, ha⟩ ↦ ⟨f.connected_iff.mp hc, f.isAcyclic_iff.mp ha⟩,
   fun ⟨hc, ha⟩ ↦ ⟨f.connected_iff.mpr hc, f.isAcyclic_iff.mpr ha⟩⟩

Premises used: Iff.mpr, SimpleGraph.IsTree, _private.0.SimpleGraph.Iso.isTree_iff.match_1, SimpleGraph.Iso.isAcyclic_iff, SimpleGraph.Iso.connected_iff, Iff.intro, Iff.mp, SimpleGraph.IsTree.mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
f : V ↪ V'
h : IsAcyclic.{u_2} (V := V') (SimpleGraph.map (⇑f : (a : V) → V') G)
⊢ G.IsAcyclic

Tactic:
h.embedding <| SimpleGraph.Embedding.map ..

Premises used: SimpleGraph.IsAcyclic.embedding, SimpleGraph.Embedding.map
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
f : V' ↪ V
h : G.IsAcyclic
⊢ IsAcyclic.{u_2} (V := V') (SimpleGraph.comap (⇑f : (a : V') → V) G)

Tactic:
h.embedding <| SimpleGraph.Embedding.comap ..

Premises used: SimpleGraph.IsAcyclic.embedding, SimpleGraph.Embedding.comap
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
s : Set V
⊢ (SimpleGraph.induce s G).IsAcyclic

Tactic:
h.of_comap _

Premises used: SimpleGraph.IsAcyclic.of_comap
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
H : G.Subgraph
⊢ H.coe.IsAcyclic

Tactic:
h.comap _ H.hom_injective

Premises used: SimpleGraph.Subgraph.hom_injective, SimpleGraph.IsAcyclic.comap
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
G G' : SimpleGraph V
hsub : G ≤ G'
h : G'.IsAcyclic
⊢ G.IsAcyclic

Tactic:
h.comap ⟨_, fun h ↦ hsub h⟩ Function.injective_id

Premises used: Function.injective_id, RelHom.mk, SimpleGraph.IsAcyclic.comap
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
Hs : Set (SimpleGraph V)
hHs : Hs.Nonempty
h_dir : DirectedOn (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) Hs
u v u_1 : V
⊢ ∀ (e : Sym2 V),
    Membership.mem (γ := List (Sym2 V)) (edges (G := sSup Hs) (u := u_1) nil) e → e ∈ hHs.some (s := Hs).edgeSet

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
Hs : Set (SimpleGraph V)
hHs : Hs.Nonempty
h_dir : DirectedOn (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) Hs
u v u_1 : V
⊢ ∃ H ∈ Hs, ∀ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := sSup Hs) (u := u_1) nil) e → e ∈ H.edgeSet

Tactic:
exact ⟨hHs.some, hHs.some_mem, by simp⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
Hs : Set (SimpleGraph V)
hHs : Hs.Nonempty
h_dir : DirectedOn (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) Hs
u_1 v_1 u v w : V
h_adj : (sSup Hs).Adj u v
p : (sSup Hs).Walk v w
ih : ∃ H ∈ Hs, ∀ e ∈ p.edges, e ∈ H.edgeSet
cons :
  ∀ (H₁ : SimpleGraph V) (hH₁ : H₁ ∈ Hs) (ih : ∀ e ∈ p.edges, e ∈ H₁.edgeSet),
    ∃ H ∈ Hs, ∀ e ∈ (Walk.cons h_adj p).edges, e ∈ H.edgeSet
⊢ ∃ H ∈ Hs, ∀ e ∈ (Walk.cons h_adj p).edges, e ∈ H.edgeSet

Tactic:
obtain ⟨H₁, hH₁, ih⟩ := ih
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
Hs : Set (SimpleGraph V)
hHs : Hs.Nonempty
h_dir : DirectedOn (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) Hs
u_1 v_1 u v w : V
h_adj : (sSup Hs).Adj u v
p : (sSup Hs).Walk v w
H₁ : SimpleGraph V
hH₁ : H₁ ∈ Hs
ih : ∀ e ∈ p.edges, e ∈ H₁.edgeSet
⊢ ∃ H₂ ∈ Hs, H₂.Adj u v

Tactic:
h_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
Hs : Set (SimpleGraph V)
hHs : Hs.Nonempty
h_dir : DirectedOn (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) Hs
u_1 v_1 u v w : V
h_adj : (sSup Hs).Adj u v
p : (sSup Hs).Walk v w
H₁ : SimpleGraph V
hH₁ : H₁ ∈ Hs
ih : ∀ e ∈ p.edges, e ∈ H₁.edgeSet
cons :
  ∀ (H₂ : SimpleGraph V) (hH₂ : H₂ ∈ Hs) (h_adj : H₂.Adj u v),
    ∃ H ∈ Hs, ∀ e ∈ edges (u := u) (Walk.cons ⋯ p), e ∈ H.edgeSet
⊢ ∃ H ∈ Hs, ∀ e ∈ (Walk.cons h_adj p).edges, e ∈ H.edgeSet

Tactic:
obtain ⟨H₂, hH₂, h_adj⟩ : ∃ H₂ ∈ Hs, H₂.Adj u v := h_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
Hs : Set (SimpleGraph V)
hHs : Hs.Nonempty
h_dir : DirectedOn (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) Hs
u_1 v_1 u v w : V
p : (sSup Hs).Walk v w
H₁ : SimpleGraph V
hH₁ : H₁ ∈ Hs
ih : ∀ e ∈ p.edges, e ∈ H₁.edgeSet
H₂ : SimpleGraph V
hH₂ : H₂ ∈ Hs
h_adj : H₂.Adj u v
cons :
  ∀ (H : SimpleGraph V) (hH : H ∈ Hs) (h₁ : H₁ ≤ H) (h₂ : H₂ ≤ H),
    ∃ H ∈ Hs, ∀ e ∈ edges (u := u) (Walk.cons ⋯ p), e ∈ H.edgeSet
⊢ ∃ H ∈ Hs, ∀ e ∈ edges (u := u) (Walk.cons ⋯ p), e ∈ H.edgeSet

Tactic:
obtain ⟨H, hH, h₁, h₂⟩ := h_dir H₁ hH₁ H₂ hH₂
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
Hs : Set (SimpleGraph V)
hHs : Hs.Nonempty
h_dir : DirectedOn (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) Hs
u_1 v_1 u v w : V
p : (sSup Hs).Walk v w
H₁ : SimpleGraph V
hH₁ : H₁ ∈ Hs
ih : ∀ e ∈ p.edges, e ∈ H₁.edgeSet
H₂ : SimpleGraph V
hH₂ : H₂ ∈ Hs
h_adj : H₂.Adj u v
H : SimpleGraph V
hH : H ∈ Hs
h₁ : H₁ ≤ H
h₂ : H₂ ≤ H
⊢ ∃ H ∈ Hs, ∀ e ∈ edges (u := u) (cons ⋯ p), e ∈ H.edgeSet

Tactic:
simpa using ⟨H, hH, (le_iff_adj.mp h₂) _ _ h_adj, fun a ha => edgeSet_mono h₁ (ih a ha)⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
Hs : Set (SimpleGraph V)
hHs : Hs.Nonempty
h_dir : DirectedOn (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) Hs
u v : V
p : (sSup Hs).Walk u v
nil :
  ∀ {u : V},
    ∃ H ∈ Hs,
      ∀ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := sSup Hs) (u := u) Walk.nil) e → e ∈ H.edgeSet
cons :
  ∀ {u v w : V} (h_adj : (sSup Hs).Adj u v) (p : (sSup Hs).Walk v w) (ih : ∃ H ∈ Hs, ∀ e ∈ p.edges, e ∈ H.edgeSet),
    ∃ H ∈ Hs, ∀ e ∈ (Walk.cons h_adj p).edges, e ∈ H.edgeSet
⊢ ∃ H ∈ Hs, ∀ e ∈ p.edges, e ∈ H.edgeSet

Tactic:
induction p with
  | nil => exact ⟨hHs.some, hHs.some_mem, by simp⟩
  | @cons u v w h_adj p ih =>
    obtain ⟨H₁, hH₁, ih⟩ := ih
    obtain ⟨H₂, hH₂, h_adj⟩ : ∃ H₂ ∈ Hs, H₂.Adj u v := h_adj
    obtain ⟨H, hH, h₁, h₂⟩ := h_dir H₁ hH₁ H₂ hH₂
    simpa using ⟨H, hH, (le_iff_adj.mp h₂) _ _ h_adj, fun a ha => edgeSet_mono h₁ (ih a ha)⟩

Premises used: SimpleGraph.Walk.cons, SimpleGraph.Walk.nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
Hs : Set (SimpleGraph V)
h_acyc : ∀ H ∈ Hs, H.IsAcyclic
h_dir : DirectedOn (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) Hs
inl :
  ∀ (h_acyc : ∀ (H : SimpleGraph V), Membership.mem (γ := Set (SimpleGraph V)) ∅ H → H.IsAcyclic)
    (h_dir : DirectedOn (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) ∅), IsAcyclic.{u_1} (V := V) (sSup ∅)
inr : ∀ (hnemp : Hs.Nonempty), (sSup Hs).IsAcyclic
⊢ (sSup Hs).IsAcyclic

Tactic:
rcases Hs.eq_empty_or_nonempty with rfl | hnemp

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
h_acyc : ∀ (H : SimpleGraph V), Membership.mem (γ := Set (SimpleGraph V)) ∅ H → H.IsAcyclic
h_dir : DirectedOn (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) ∅
⊢ IsAcyclic.{u_1} (V := V) (sSup ∅)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
Hs : Set (SimpleGraph V)
h_acyc : ∀ H ∈ Hs, H.IsAcyclic
h_dir : DirectedOn (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) Hs
hnemp : Hs.Nonempty
u : V
p : (sSup Hs).Walk u u
hp : p.IsCycle
inr : ∀ (H : SimpleGraph V) (hH : H ∈ Hs) (hpH : ∀ e ∈ p.edges, e ∈ H.edgeSet), False
⊢ False

Tactic:
obtain ⟨H, hH, hpH⟩ := p.exists_mem_contains_edges_of_directed Hs hnemp h_dir

Premises used: _private.0.SimpleGraph.Walk.exists_mem_contains_edges_of_directed
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
Hs : Set (SimpleGraph V)
h_acyc : ∀ H ∈ Hs, H.IsAcyclic
h_dir : DirectedOn (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) Hs
hnemp : Hs.Nonempty
u : V
p : (sSup Hs).Walk u u
hp : p.IsCycle
H : SimpleGraph V
hH : H ∈ Hs
hpH : ∀ e ∈ p.edges, e ∈ H.edgeSet
⊢ False

Tactic:
h_acyc H hH (p.transfer H hpH) <| Walk.IsCycle.transfer hp hpH

Premises used: SimpleGraph.Walk.IsCycle.transfer, SimpleGraph.Walk.transfer
-- Module: Mathlib.Combinatorics.SimpleGraph.Acyclic
Goal:
V : Type u_1
Hs : Set (SimpleGraph V)
h_acyc : ∀ H ∈ Hs, H.IsAcyclic
h_dir : DirectedOn (fun (x1 x2 : SimpleGraph V) ↦ x1 ≤ x2) Hs
hnemp : Hs.Nonempty
u : V
p : (sSup Hs).Walk u u
hp : p.IsCycle
H : SimpleGraph V
hH : H ∈ Hs
hpH : ∀ e ∈ p.edges, e ∈ H.edgeSet
⊢ False

Tactic:
exact h_acyc H hH (p.transfer H hpH) <| Walk.IsCycle.transfer hp hpH

Premises used: SimpleGraph.Walk.IsCycle.transfer, SimpleGraph.Walk.transfer