awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
⊢ x ∉ v

Tactic:
have hxv : x ∉ v := disjoint_right.1 hvs (mem_insert_self _ _)
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
⊢ v \ u = v

Tactic:
have : v \ u = v := ‹Disjoint v u›.sdiff_eq_left
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this : v \ u = v
hxu : x ∈ u
obtain : ∀ (y : α) (hyv : y ∈ v) (hxy : IsCompressed (u.erase x) (v.erase y) 𝒜), False
⊢ False

Tactic:
obtain ⟨y, hyv, hxy⟩ := huv x hxu
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this : v \ u = v
hxu : x ∈ u
y : α
hyv : y ∈ v
hxy : IsCompressed (u.erase x) (v.erase y) 𝒜
apply : insert y s ∈ 𝒜
⊢ False

Tactic:
apply m y (disjoint_right.1 hsv hyv)

Premises used: Iff.mp, Finset.disjoint_right
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this : v \ u = v
hxu : x ∈ u
y : α
hyv : y ∈ v
hxy : IsCompressed (u.erase x) (v.erase y) 𝒜
rwa rwa₁ rwa₂ rwa₃ : (insert x s ∪ v) \ u ∈ 𝒜
⊢ (insert x s ∪ v) \ u ∈ 𝓒 (u.erase x) (v.erase y) 𝒜

Tactic:
rwa [hxy.eq]

Premises used: UV.IsCompressed.eq
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this : v \ u = v
hxu : x ∈ u
y : α
hyv : y ∈ v
hxy : IsCompressed (u.erase x) (v.erase y) 𝒜
sup_sdiff_mem_of_mem_compression : v.erase y ≤ (insert x s ∪ v) \ u
⊢ ((insert x s ∪ v) \ u ∪ u.erase x) \ v.erase y ∈ 𝒜

Tactic:
refine
        sup_sdiff_mem_of_mem_compression (by rwa [hxy.eq]) ?_
          (disjoint_of_subset_left (erase_subset _ _) disjoint_sdiff)

Premises used: UV.sup_sdiff_mem_of_mem_compression
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this : v \ u = v
hxu : x ∈ u
y : α
hyv : y ∈ v
hxy : IsCompressed (u.erase x) (v.erase y) 𝒜
rw : v.erase y ≤ insert x s \ u ∪ v
⊢ v.erase y ≤ (insert x s ∪ v) \ u

Tactic:
rw [union_sdiff_distrib, ‹v \ u = v›]

Premises used: Finset.union_sdiff_distrib
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this : v \ u = v
hxu : x ∈ u
y : α
hyv : y ∈ v
hxy : IsCompressed (u.erase x) (v.erase y) 𝒜
⊢ v.erase y ≤ insert x s \ u ∪ v

Tactic:
(erase_subset _ _).trans subset_union_right

Premises used: HasSubset.Subset.trans, Finset.subset_union_right, Finset.erase_subset
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this : v \ u = v
hxu : x ∈ u
y : α
hyv : y ∈ v
hxy : IsCompressed (u.erase x) (v.erase y) 𝒜
⊢ v.erase y ≤ insert x s \ u ∪ v

Tactic:
exact (erase_subset _ _).trans subset_union_right

Premises used: HasSubset.Subset.trans, Finset.subset_union_right, Finset.erase_subset
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this : v \ u = v
hxu : x ∈ u
y : α
hyv : y ∈ v
hxy : IsCompressed (u.erase x) (v.erase y) 𝒜
⊢ ((insert x s ∪ v) \ u ∪ u.erase x) \ v.erase y ∈ 𝒜

Tactic:
have : ((insert x s ∪ v) \ u ∪ erase u x) \ erase v y ∈ 𝒜 := by
      refine
        sup_sdiff_mem_of_mem_compression (by rwa [hxy.eq]) ?_
          (disjoint_of_subset_left (erase_subset _ _) disjoint_sdiff)
      rw [union_sdiff_distrib, ‹v \ u = v›]
      exact (erase_subset _ _).trans subset_union_right
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
hxu : x ∈ u
y : α
hyv : y ∈ v
hxy : IsCompressed (u.erase x) (v.erase y) 𝒜
this : ((insert x s ∪ v) \ u ∪ u.erase x) \ v.erase y ∈ 𝒜
⊢ ((insert x s ∪ v) \ u ∪ u.erase x) \ v.erase y ∈ 𝒜

Tactic:
this
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
hxu : x ∈ u
y : α
hyv : y ∈ v
hxy : IsCompressed (u.erase x) (v.erase y) 𝒜
this : ((insert x s ∪ v) \ u ∪ u.erase x) \ v.erase y ∈ 𝒜
h : insert y s = ((insert x s ∪ v) \ u ∪ u.erase x) \ v.erase y
⊢ insert y s ∈ 𝒜

Tactic:
convert! this using 1
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
hxu : x ∈ u
y : α
hyv : y ∈ v
hxy : IsCompressed (u.erase x) (v.erase y) 𝒜
this : ((insert x s ∪ v) \ u ∪ u.erase x) \ v.erase y ∈ 𝒜
h : insert y s = (insert x s ∪ v).erase x \ v.erase y
h₁ : insert y s = ((insert x s).erase x ∪ v.erase x) \ v.erase y
h₂ : insert y s = (s ∪ v.erase x) \ v.erase y
h₃ : insert y s = (s ∪ v) \ v.erase y
h₄ : insert y s = insert y ((s ∪ v) \ v)
h₅ h₆ : insert y s = insert y s
⊢ insert y s = ((insert x s ∪ v) \ u ∪ u.erase x) \ v.erase y

Tactic:
rw [sdiff_union_erase_cancel (hus.trans subset_union_left) ‹x ∈ u›, erase_union_distrib,
      erase_insert ‹x ∉ s›, erase_eq_of_notMem ‹x ∉ v›, sdiff_erase (mem_union_right _ hyv),
      union_sdiff_cancel_right hsv]

Premises used: HasSubset.Subset.trans, Finset.sdiff_erase, Finset.subset_union_left, Finset.sdiff_union_erase_cancel, Finset.erase_insert, Finset.erase_union_distrib, Finset.union_sdiff_cancel_right, Finset.erase_eq_of_notMem, Finset.mem_union_right
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this : v \ u = v
⊢ x ∉ u

Tactic:
have : x ∉ u := by
    intro hxu
    obtain ⟨y, hyv, hxy⟩ := huv x hxu
    -- If `x ∈ u`, we can get `y ∈ v` so that `𝒜` is `(u.erase x, v.erase y)`-compressed
    apply m y (disjoint_right.1 hsv hyv)
    -- and we will use this `y` to contradict `m`, so we would like to show `insert y s ∈ 𝒜`.
    -- We do this by showing the below
    have : ((insert x s ∪ v) \ u ∪ erase u x) \ erase v y ∈ 𝒜 := by
      refine
        sup_sdiff_mem_of_mem_compression (by rwa [hxy.eq]) ?_
          (disjoint_of_subset_left (erase_subset _ _) disjoint_sdiff)
      rw [union_sdiff_distrib, ‹v \ u = v›]
      exact (erase_subset _ _).trans subset_union_right
    -- and then arguing that it's the same
    convert! this using 1
    rw [sdiff_union_erase_cancel (hus.trans subset_union_left) ‹x ∈ u›, erase_union_distrib,
      erase_insert ‹x ∉ s›, erase_eq_of_notMem ‹x ∉ v›, sdiff_erase (mem_union_right _ hyv),
      union_sdiff_cancel_right hsv]
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
this : x ∉ u
rwa : u.erase x ⊆ s
rwa₁ rwa₂ rwa₃ rwa₄ : u ⊆ insert x s
⊢ u ⊆ s

Tactic:
rwa [← erase_eq_of_notMem ‹x ∉ u›, ← subset_insert_iff]

Premises used: Finset.erase_eq_of_notMem, Finset.subset_insert_iff
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
this : x ∉ u
⊢ u ⊆ s

Tactic:
have hus : u ⊆ s := by rwa [← erase_eq_of_notMem ‹x ∉ u›, ← subset_insert_iff]
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus_1 : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
this : x ∉ u
hus : u ⊆ s
simp_rw :
  u ⊆ s ∧
    Disjoint v s ∧ (∃ a ∉ (s ∪ v) \ u, insert a ((s ∪ v) \ u) ∈ 𝒜) ∧ ¬∃ a ∉ (s ∪ v) \ u, insert a ((s ∪ v) \ u) ∈ 𝒜'
⊢ u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'

Tactic:
simp_rw [mem_shadow_iff_insert_mem]

Premises used: Finset.mem_shadow_iff_insert_mem
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus_1 : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
this : x ∉ u
hus : u ⊆ s
⊢ u ⊆ s ∧
    Disjoint v s ∧ (∃ a ∉ (s ∪ v) \ u, insert a ((s ∪ v) \ u) ∈ 𝒜) ∧ ¬∃ a ∉ (s ∪ v) \ u, insert a ((s ∪ v) \ u) ∈ 𝒜'

Tactic:
⟨hus, hsv.symm, ⟨x, ?_, ?_⟩, ?_⟩

Premises used: Disjoint.symm, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus_1 : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
this : x ∉ u
hus : u ⊆ s
refine_1 : x ∉ (s ∪ v) \ u
refine_2 : insert x ((s ∪ v) \ u) ∈ 𝒜
refine_3 : ¬∃ a ∉ (s ∪ v) \ u, insert a ((s ∪ v) \ u) ∈ 𝒜'
⊢ u ⊆ s ∧
    Disjoint v s ∧ (∃ a ∉ (s ∪ v) \ u, insert a ((s ∪ v) \ u) ∈ 𝒜) ∧ ¬∃ a ∉ (s ∪ v) \ u, insert a ((s ∪ v) \ u) ∈ 𝒜'

Tactic:
refine ⟨hus, hsv.symm, ⟨x, ?_, ?_⟩, ?_⟩
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus_1 : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
this : x ∉ u
hus : u ⊆ s
⊢ x ∉ (s ∪ v) \ u

Tactic:
notMem_sdiff_of_notMem_left (notMem_union.2 ⟨‹x ∉ s›, ‹x ∉ v›⟩)

Premises used: Iff.mpr, Finset.notMem_sdiff_of_notMem_left, Finset.notMem_union, And.intro
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus_1 : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
this : x ∉ u
hus : u ⊆ s
⊢ x ∉ (s ∪ v) \ u

Tactic:
exact notMem_sdiff_of_notMem_left (notMem_union.2 ⟨‹x ∉ s›, ‹x ∉ v›⟩)

Premises used: Iff.mpr, Finset.notMem_sdiff_of_notMem_left, Finset.notMem_union, And.intro
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus_1 : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
this : x ∉ u
hus : u ⊆ s
refine_2 : insert x (s ∪ v) \ u ∈ 𝒜
refine_2₁ refine_2₂ refine_2₃ refine_2₄ : (insert x s ∪ v) \ u ∈ 𝒜
⊢ insert x ((s ∪ v) \ u) ∈ 𝒜

Tactic:
rwa [← insert_sdiff_of_notMem _ ‹x ∉ u›, ← insert_union]

Premises used: Finset.insert_sdiff_of_notMem, Finset.insert_union
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus_1 : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
this : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∉ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
⊢ v ⊆ insert w ((s ∪ v) \ u)

Tactic:
have : v ⊆ insert w ((s ∪ v) \ u) :=
    (subset_sdiff.2 ⟨subset_union_right, hvu⟩).trans (subset_insert _ _)
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus_1 : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
this_3 : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∉ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this : v ⊆ insert w ((s ∪ v) \ u)
pos : ∀ (hwu : w ∈ u), False
neg : ∀ (hwu : w ∉ u), False
⊢ False

Tactic:
by_cases hwu : w ∈ u
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus_1 : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
this_3 : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∉ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∈ u
pos : ∀ (z : α) (hz : z ∈ v) (hxy : IsCompressed (u.erase w) (v.erase z) 𝒜), False
⊢ False

Tactic:
obtain ⟨z, hz, hxy⟩ := huv w hwu
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus_1 : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
this_3 : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∉ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∈ u
z : α
hz : z ∈ v
hxy : IsCompressed (u.erase w) (v.erase z) 𝒜
pos : insert z s ∈ 𝒜
⊢ False

Tactic:
apply m z (disjoint_right.1 hsv hz)

Premises used: Iff.mp, Finset.disjoint_right
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus_1 : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
this_3 : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∉ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∈ u
z : α
hz : z ∈ v
hxy : IsCompressed (u.erase w) (v.erase z) 𝒜
⊢ insert w ((s ∪ v) \ u) ∈ 𝒜

Tactic:
have : insert w ((s ∪ v) \ u) ∈ 𝒜 := mem_of_mem_compression hw𝒜' ‹_› (aux huv)
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus_1 : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
this_3 : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∉ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this_4 : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∈ u
z : α
hz : z ∈ v
hxy : IsCompressed (u.erase w) (v.erase z) 𝒜
this rwa rwa₁ rwa₂ rwa₃ : insert w ((s ∪ v) \ u) ∈ 𝒜
⊢ insert w ((s ∪ v) \ u) ∈ 𝓒 (u.erase w) (v.erase z) 𝒜

Tactic:
rwa [hxy.eq]

Premises used: UV.IsCompressed.eq
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus_1 : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
this_3 : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∉ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this_4 : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∈ u
z : α
hz : z ∈ v
hxy : IsCompressed (u.erase w) (v.erase z) 𝒜
this : insert w ((s ∪ v) \ u) ∈ 𝒜
refine : Disjoint (u.erase w) (insert w ((s ∪ v) \ u))
⊢ (insert w ((s ∪ v) \ u) ∪ u.erase w) \ v.erase z ∈ 𝒜

Tactic:
refine sup_sdiff_mem_of_mem_compression (by rwa [hxy.eq]) ((erase_subset _ _).trans ‹_›) ?_

Premises used: UV.sup_sdiff_mem_of_mem_compression
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus_1 : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
this_3 : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∉ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this_4 : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∈ u
z : α
hz : z ∈ v
hxy : IsCompressed (u.erase w) (v.erase z) 𝒜
this : insert w ((s ∪ v) \ u) ∈ 𝒜
rw : Disjoint (u.erase w) ((s ∪ v) \ u.erase w)
⊢ Disjoint (u.erase w) (insert w ((s ∪ v) \ u))

Tactic:
rw [← sdiff_erase (mem_union_left _ <| hus hwu)]

Premises used: Finset.sdiff_erase, Finset.mem_union_left