awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (hypothesis)
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 y s ∈ 𝒜
have this₁ : ((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
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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 y s ∈ 𝒜
have h : insert y s = ((insert x s ∪ v) \ u ∪ u.erase x) \ v.erase y
Tactic: convert! this using 1
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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 y s = ((insert x s ∪ v) \ u ∪ u.erase x) \ v.erase y
have h : insert y s = (insert x s ∪ v).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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ insert y s = ((insert x s ∪ v) \ u ∪ u.erase x) \ v.erase y
have h₁ : insert y s = ((insert x s).erase x ∪ v.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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ insert y s = ((insert x s ∪ v) \ u ∪ u.erase x) \ v.erase y
have h₂ : insert y s = (s ∪ v.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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ insert y s = ((insert x s ∪ v) \ u ∪ u.erase x) \ v.erase y
have h₃ : insert y s = (s ∪ v) \ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ insert y s = ((insert x s ∪ v) \ u ∪ u.erase x) \ v.erase y
have h₄ : insert y s = insert y ((s ∪ v) \ v)
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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)
⊢ insert y s = ((insert x s ∪ v) \ u ∪ u.erase x) \ v.erase y
have h₅ : insert y s = insert y s
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (hypothesis)
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
⊢ u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
have this₁ : 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
have rwa : u.erase x ⊆ s
Tactic: rwa [← erase_eq_of_notMem ‹x ∉ u›, ← subset_insert_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (hypothesis)
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 ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
have hus₁ : u ⊆ s
Tactic: have hus : u ⊆ s := by rwa [← erase_eq_of_notMem ‹x ∉ u›, ← subset_insert_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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 ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
have 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) ∈ 𝒜'
Tactic: simp_rw [mem_shadow_iff_insert_mem]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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) ∈ 𝒜'
have refine_1 : x ∉ (s ∪ v) \ u
Tactic: refine ⟨hus, hsv.symm, ⟨x, ?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ u ⊆ s ∧
    Disjoint v s ∧ (∃ a ∉ (s ∪ v) \ u, insert a ((s ∪ v) \ u) ∈ 𝒜) ∧ ¬∃ a ∉ (s ∪ v) \ u, insert a ((s ∪ v) \ u) ∈ 𝒜'
have refine_2 : insert x ((s ∪ v) \ u) ∈ 𝒜
Tactic: refine ⟨hus, hsv.symm, ⟨x, ?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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) ∈ 𝒜
⊢ u ⊆ s ∧
    Disjoint v s ∧ (∃ a ∉ (s ∪ v) \ u, insert a ((s ∪ v) \ u) ∈ 𝒜) ∧ ¬∃ a ∉ (s ∪ v) \ u, insert a ((s ∪ v) \ u) ∈ 𝒜'
have refine_3 : ¬∃ a ∉ (s ∪ v) \ u, insert a ((s ∪ v) \ u) ∈ 𝒜'
Tactic: refine ⟨hus, hsv.symm, ⟨x, ?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ insert x ((s ∪ v) \ u) ∈ 𝒜
have refine_2 : insert x (s ∪ v) \ u ∈ 𝒜
Tactic: rwa [← insert_sdiff_of_notMem _ ‹x ∉ u›, ← insert_union]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (hypothesis)
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) ∈ 𝒜'
⊢ False
have this₁ : v ⊆ insert w ((s ∪ v) \ u)
Tactic: have : v ⊆ insert w ((s ∪ v) \ u) :=
    (subset_sdiff.2 ⟨subset_union_right, hvu⟩).trans (subset_insert _ _)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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)
⊢ False
have pos : ∀ (hwu : w ∈ u), False
Tactic: by_cases hwu : w ∈ u
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ False
have neg : ∀ (hwu : w ∉ u), False
Tactic: by_cases hwu : w ∈ u
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ False
have pos : ∀ (z : α) (hz : z ∈ v) (hxy : IsCompressed (u.erase w) (v.erase z) 𝒜), False
Tactic: obtain ⟨z, hz, hxy⟩ := huv w hwu
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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) 𝒜
⊢ False
have pos : insert z s ∈ 𝒜
Tactic: apply m z (disjoint_right.1 hsv hz)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (hypothesis)
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 z s ∈ 𝒜
have this₁ : insert w ((s ∪ v) \ u) ∈ 𝒜
Tactic: have : insert w ((s ∪ v) \ u) ∈ 𝒜 := mem_of_mem_compression hw𝒜' ‹_› (aux huv)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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) ∈ 𝒜
⊢ (insert w ((s ∪ v) \ u) ∪ u.erase w) \ v.erase z ∈ 𝒜
have refine : Disjoint (u.erase w) (insert w ((s ∪ v) \ u))
Tactic: refine sup_sdiff_mem_of_mem_compression (by rwa [hxy.eq]) ((erase_subset _ _).trans ‹_›) ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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) ∈ 𝒜
⊢ Disjoint (u.erase w) (insert w ((s ∪ v) \ u))
have rw : Disjoint (u.erase w) ((s ∪ v) \ u.erase w)
Tactic: rw [← sdiff_erase (mem_union_left _ <| hus hwu)]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (hypothesis)
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) ∈ 𝒜
⊢ insert z s ∈ 𝒜
have this₁ : (insert w ((s ∪ v) \ u) ∪ u.erase w) \ v.erase z ∈ 𝒜
Tactic: have : (insert w ((s ∪ v) \ u) ∪ erase u w) \ erase v z ∈ 𝒜 := by
      refine sup_sdiff_mem_of_mem_compression (by rwa [hxy.eq]) ((erase_subset _ _).trans ‹_›) ?_
      rw [← sdiff_erase (mem_union_left _ <| hus hwu)]
      exact disjoint_sdiff
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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_5 : insert w ((s ∪ v) \ u) ∈ 𝒜
this : (insert w ((s ∪ v) \ u) ∪ u.erase w) \ v.erase z ∈ 𝒜
⊢ insert z s ∈ 𝒜
have h : insert z s = (insert w ((s ∪ v) \ u) ∪ u.erase w) \ v.erase z
Tactic: convert! this using 1