-- Mathlib/Combinatorics/SetFamily/Shatter.lean
lemma Shatters.of_compression (hs : (𝓓 a 𝒜).Shatters s) : 𝒜.Shatters s

Proof state:
case pos.intro.intro.inr
α : 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 ∈ 𝒜
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u

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

Result:
case pos.intro.intro.inr
α : 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

α : 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 ∈ s ∩ v

Proof state:
case pos.intro.intro.inl
α : 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 ∈ 𝒜
⊢ s ∩ v.erase a = s ∩ u

Tactic:
rw [inter_erase, hsv, erase_insert]

Result:
case pos.intro.intro.inl
α : 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 ∈ 𝒜
⊢ a ∉ s ∩ u

Proof state:
case intro.intro
α : 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
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u

Tactic:
obtain hu | hu := hu

Result:
case intro.intro.inl
α : 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

case intro.intro.inr
α : 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 ∈ 𝒜
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u

Proof state:
case pos.intro.intro.inr
α : 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

α : 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 ∈ s ∩ v

Tactic:
cases hv.1 hv.2

Result:
α : 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 ∈ s ∩ v

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
t : Finset α
ht : t ⊆ s
⊢ ∃ u ∈ 𝒜, s ∩ u = t

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

Result:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
hu : u ∈ 𝓓 a 𝒜
ht : s ∩ u ⊆ s
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u