awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
hs : s ∈ ∂ 𝒜
pos : ∀ (huvs : Disjoint u s ∧ v ≤ s), (s ⊔ u) \ v ∈ ∂ 𝒜
⊢ (if Disjoint u s ∧ v ≤ s then (s ⊔ u) \ v else s) ∈ ∂ 𝒜
have neg : ∀ (huvs : ¬(Disjoint u s ∧ v ≤ s)), s ∈ ∂ 𝒜
Tactic: split_ifs with huvs
-- 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
hs : s ∈ ∂ 𝒜
huvs : Disjoint u s ∧ v ≤ s
⊢ (s ⊔ u) \ v ∈ ∂ 𝒜
have hs'₁ : ∃ s_1 ∈ 𝒜', ∃ a ∈ s_1, s_1.erase a = s
Tactic: rw [mem_shadow_iff] at hs'
Cleared hypotheses: hs', hs, huvs
-- 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
s : Finset α
hs' : ∃ s_1 ∈ 𝒜', ∃ a ∈ s_1, s_1.erase a = s
hs : s ∈ ∂ 𝒜
huvs : Disjoint u s ∧ v ≤ s
⊢ (s ⊔ u) \ v ∈ ∂ 𝒜
have pos : ∀ (t : Finset α) (Ht : t ∈ 𝒜') (a : α) (hat : a ∈ t) (hs : t.erase a ∈ ∂ 𝒜)
  (huvs : Disjoint u (t.erase a) ∧ v ≤ t.erase a), (t.erase a ⊔ u) \ v ∈ ∂ 𝒜
Tactic: obtain ⟨t, Ht, a, hat, rfl⟩ := hs'
Cleared hypotheses: s, hs', hs, huvs
-- 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ≤ t.erase a
⊢ (t.erase a ⊔ u) \ v ∈ ∂ 𝒜
have hav : a ∉ v
Tactic: have hav : a ∉ v := notMem_mono huvs.2 (notMem_erase a t)
-- 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ≤ t.erase a
hav : a ∉ v
⊢ (t.erase a ⊔ u) \ v ∈ ∂ 𝒜
have hvt : v ≤ t
Tactic: have hvt : v ≤ t := huvs.2.trans (erase_subset _ t)
-- 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ≤ t.erase a
hav : a ∉ v
hvt : v ≤ t
⊢ (t.erase a ⊔ u) \ v ∈ ∂ 𝒜
have ht : t ∈ 𝒜
Tactic: have ht : t ∈ 𝒜 := mem_of_mem_compression Ht hvt (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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ≤ t.erase a
hav : a ∉ v
hvt : v ≤ t
ht : t ∈ 𝒜
⊢ (t.erase a ⊔ u) \ v ∈ ∂ 𝒜
have pos : ∀ (hau : a ∈ u), (t.erase a ⊔ u) \ v ∈ ∂ 𝒜
Tactic: by_cases hau : a ∈ 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ≤ t.erase a
hav : a ∉ v
hvt : v ≤ t
ht : t ∈ 𝒜
pos : ∀ (hau : a ∈ u), (t.erase a ⊔ u) \ v ∈ ∂ 𝒜
⊢ (t.erase a ⊔ u) \ v ∈ ∂ 𝒜
have neg : ∀ (hau : a ∉ u), (t.erase a ⊔ u) \ v ∈ ∂ 𝒜
Tactic: by_cases hau : a ∈ 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ≤ t.erase a
hav : a ∉ v
hvt : v ≤ t
ht : t ∈ 𝒜
hau : a ∈ u
⊢ (t.erase a ⊔ u) \ v ∈ ∂ 𝒜
have pos : ∀ (b : α) (hbv : b ∈ v) (Hcomp : IsCompressed (u.erase a) (v.erase b) 𝒜), (t.erase a ⊔ u) \ v ∈ ∂ 𝒜
Tactic: obtain ⟨b, hbv, Hcomp⟩ := huv a hau
-- 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ≤ t.erase a
hav : a ∉ v
hvt : v ≤ t
ht : t ∈ 𝒜
hau : a ∈ u
b : α
hbv : b ∈ v
Hcomp : IsCompressed (u.erase a) (v.erase b) 𝒜
⊢ (t.erase a ⊔ u) \ v ∈ ∂ 𝒜
have pos : insert b ((t.erase a ⊔ u) \ v) ∈ 𝒜
Tactic: refine mem_shadow_iff_insert_mem.2 ⟨b, notMem_sdiff_of_mem_right hbv, ?_⟩
-- 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ≤ t.erase a
hav : a ∉ v
hvt : v ≤ t
ht : t ∈ 𝒜
hau : a ∈ u
b : α
hbv : b ∈ v
Hcomp : IsCompressed (u.erase a) (v.erase b) 𝒜
⊢ insert b ((t.erase a ⊔ u) \ v) ∈ 𝒜
have ht₁ : t ∈ 𝓒 (u.erase a) (v.erase b) 𝒜
Tactic: rw [← Hcomp.eq] at ht
Cleared hypotheses: ht, hbv, Hcomp
-- 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ≤ t.erase a
hav : a ∉ v
hvt : v ≤ t
hau : a ∈ u
b : α
ht : t ∈ 𝓒 (u.erase a) (v.erase b) 𝒜
hbv : b ∈ v
Hcomp : IsCompressed (u.erase a) (v.erase b) 𝒜
⊢ insert b ((t.erase a ⊔ u) \ v) ∈ 𝒜
have hsb : (t ⊔ u.erase a) \ v.erase b ∈ 𝒜
Tactic: have hsb :=
        sup_sdiff_mem_of_mem_compression ht ((erase_subset _ _).trans hvt)
          (disjoint_erase_comm.2 huvs.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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ≤ t.erase a
hav : a ∉ v
hvt : v ≤ t
hau : a ∈ u
b : α
ht : t ∈ 𝓒 (u.erase a) (v.erase b) 𝒜
hbv : b ∈ v
Hcomp : IsCompressed (u.erase a) (v.erase b) 𝒜
hsb : (t ⊔ u.erase a) \ v.erase b ∈ 𝒜
⊢ insert b ((t.erase a ⊔ u) \ v) ∈ 𝒜
have pos : ∀ (hsb : (t ∪ u.erase a) \ v.erase b ∈ 𝒜), insert b ((t.erase a ⊔ u) \ v) ∈ 𝒜
Tactic: rwa [sup_eq_union, sdiff_erase (mem_union_left _ <| hvt hbv), union_erase_of_mem hat, ←
        erase_union_of_mem hau] at hsb
Cleared hypotheses: hsb
-- 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ≤ t.erase a
hav : a ∉ v
hvt : v ≤ t
hau : a ∈ u
b : α
ht : t ∈ 𝓒 (u.erase a) (v.erase b) 𝒜
hbv : b ∈ v
Hcomp : IsCompressed (u.erase a) (v.erase b) 𝒜
hsb : (t ⊔ u.erase a) \ v.erase b ∈ 𝒜
pos : ∀ (hsb : (t ∪ u.erase a) \ v.erase b ∈ 𝒜), insert b ((t.erase a ⊔ u) \ v) ∈ 𝒜
⊢ insert b ((t.erase a ⊔ u) \ v) ∈ 𝒜
have pos₁ : ∀ (hsb : insert b ((t ∪ u.erase a) \ v) ∈ 𝒜), insert b ((t.erase a ⊔ u) \ v) ∈ 𝒜
Tactic: rwa [sup_eq_union, sdiff_erase (mem_union_left _ <| hvt hbv), union_erase_of_mem hat, ←
        erase_union_of_mem hau] at hsb
Cleared hypotheses: hsb
-- 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ≤ t.erase a
hav : a ∉ v
hvt : v ≤ t
hau : a ∈ u
b : α
ht : t ∈ 𝓒 (u.erase a) (v.erase b) 𝒜
hbv : b ∈ v
Hcomp : IsCompressed (u.erase a) (v.erase b) 𝒜
hsb : (t ⊔ u.erase a) \ v.erase b ∈ 𝒜
pos : ∀ (hsb : (t ∪ u.erase a) \ v.erase b ∈ 𝒜), insert b ((t.erase a ⊔ u) \ v) ∈ 𝒜
pos₁ : ∀ (hsb : insert b ((t ∪ u.erase a) \ v) ∈ 𝒜), insert b ((t.erase a ⊔ u) \ v) ∈ 𝒜
⊢ insert b ((t.erase a ⊔ u) \ v) ∈ 𝒜
have pos₂ : ∀ (hsb : insert b ((t ∪ u) \ v) ∈ 𝒜), insert b ((t.erase a ⊔ u) \ v) ∈ 𝒜
Tactic: rwa [sup_eq_union, sdiff_erase (mem_union_left _ <| hvt hbv), union_erase_of_mem hat, ←
        erase_union_of_mem hau] at hsb
Cleared hypotheses: hsb
-- 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ≤ t.erase a
hav : a ∉ v
hvt : v ≤ t
hau : a ∈ u
b : α
ht : t ∈ 𝓒 (u.erase a) (v.erase b) 𝒜
hbv : b ∈ v
Hcomp : IsCompressed (u.erase a) (v.erase b) 𝒜
hsb : (t ⊔ u.erase a) \ v.erase b ∈ 𝒜
pos : ∀ (hsb : (t ∪ u.erase a) \ v.erase b ∈ 𝒜), insert b ((t.erase a ⊔ u) \ v) ∈ 𝒜
pos₁ : ∀ (hsb : insert b ((t ∪ u.erase a) \ v) ∈ 𝒜), insert b ((t.erase a ⊔ u) \ v) ∈ 𝒜
pos₂ : ∀ (hsb : insert b ((t ∪ u) \ v) ∈ 𝒜), insert b ((t.erase a ⊔ u) \ v) ∈ 𝒜
⊢ insert b ((t.erase a ⊔ u) \ v) ∈ 𝒜
have pos₃ : ∀ (hsb : insert b ((t.erase a ∪ u) \ v) ∈ 𝒜), insert b ((t.erase a ⊔ u) \ v) ∈ 𝒜
Tactic: rwa [sup_eq_union, sdiff_erase (mem_union_left _ <| hvt hbv), union_erase_of_mem hat, ←
        erase_union_of_mem hau] at hsb
Cleared hypotheses: hsb
-- 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ≤ t.erase a
hav : a ∉ v
hvt : v ≤ t
ht : t ∈ 𝒜
hau : a ∉ u
⊢ (t.erase a ⊔ u) \ v ∈ ∂ 𝒜
have neg : a ∈ (t ⊔ u) \ v
Tactic: refine mem_shadow_iff.2
        ⟨(t ⊔ u) \ v,
          sup_sdiff_mem_of_mem_compression Ht hvt <| disjoint_of_erase_right hau huvs.1, a, ?_, ?_⟩
-- 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ≤ t.erase a
hav : a ∉ v
hvt : v ≤ t
ht : t ∈ 𝒜
hau : a ∉ u
neg : a ∈ (t ⊔ u) \ v
⊢ (t.erase a ⊔ u) \ v ∈ ∂ 𝒜
have neg₁ : ((t ⊔ u) \ v).erase a = (t.erase a ⊔ u) \ v
Tactic: refine mem_shadow_iff.2
        ⟨(t ⊔ u) \ v,
          sup_sdiff_mem_of_mem_compression Ht hvt <| disjoint_of_erase_right hau huvs.1, a, ?_, ?_⟩
-- 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ≤ t.erase a
hav : a ∉ v
hvt : v ≤ t
ht : t ∈ 𝒜
hau : a ∉ u
⊢ a ∈ (t ⊔ u) \ v
have neg : (a ∈ t ∨ a ∈ u) ∧ a ∉ v
Tactic: rw [sup_eq_union, mem_sdiff, mem_union]
-- 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 𝒜
⊢ ∂ 𝒜' ⊆ 𝓒 u v (∂ 𝒜)
have suffices : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
Tactic: suffices H : ∀ s ∈ ∂ 𝒜',
      s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜' by
    rintro s hs'
    rw [mem_compression]
    by_cases hs : s ∈ 𝒜.shadow
    swap
    · obtain ⟨hus, hvs, h, _⟩ := H _ hs' hs
      exact Or.inr ⟨hs, _, h, compress_of_disjoint_of_le' hvs hus⟩
    refine Or.inl ⟨hs, ?_⟩
    rw [compress]
    split_ifs with huvs
    swap
    · exact hs
    rw [mem_shadow_iff] at hs'
    obtain ⟨t, Ht, a, hat, rfl⟩ := hs'
    have hav : a ∉ v := notMem_mono huvs.2 (notMem_erase a t)
    have hvt : v ≤ t := huvs.2.trans (erase_subset _ t)
    have ht : t ∈ 𝒜 := mem_of_mem_compression Ht hvt (aux huv)
    by_cases hau : a ∈ u
    · obtain ⟨b, hbv, Hcomp⟩ := huv a hau
      refine mem_shadow_iff_insert_mem.2 ⟨b, notMem_sdiff_of_mem_right hbv, ?_⟩
      rw [← Hcomp.eq] at ht
      have hsb :=
        sup_sdiff_mem_of_mem_compression ht ((erase_subset _ _).trans hvt)
          (disjoint_erase_comm.2 huvs.1)
      rwa [sup_eq_union, sdiff_erase (mem_union_left _ <| hvt hbv), union_erase_of_mem hat, ←
        erase_union_of_mem hau] at hsb
    · refine mem_shadow_iff.2
        ⟨(t ⊔ u) \ v,
          sup_sdiff_mem_of_mem_compression Ht hvt <| disjoint_of_erase_right hau huvs.1, a, ?_, ?_⟩
      · rw [sup_eq_union, mem_sdiff, mem_union]
        exact ⟨Or.inl hat, hav⟩
      · simp [← erase_sdiff_comm, erase_union_distrib, erase_eq_of_notMem hau]
-- 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 ∉ ∂ 𝒜
⊢ u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
have m : ∀ y ∉ s, insert y s ∉ 𝒜
Tactic: have m : ∀ y, y ∉ s → insert y s ∉ 𝒜 := fun y h a => hs𝒜 (mem_shadow_iff_insert_mem.2 ⟨y, h, a⟩)
-- 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 ∉ 𝒜
⊢ u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
have obtain : ∀ x ∉ s, insert x s ∈ 𝒜' → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
Tactic: obtain ⟨x, _, _⟩ := mem_shadow_iff_insert_mem.1 hs𝒜'
-- 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 ∈ 𝒜'
⊢ u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
have hus : u ⊆ insert x s
Tactic: have hus : u ⊆ insert x s := le_of_mem_compression_of_notMem ‹_ ∈ 𝒜'› (m _ ‹x ∉ s›)
-- 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
⊢ u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
have hvs : Disjoint v (insert x s)
Tactic: have hvs : Disjoint v (insert x s) := disjoint_of_mem_compression_of_notMem ‹_› (m _ ‹x ∉ s›)
-- 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)
⊢ u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
have this : (insert x s ∪ v) \ u ∈ 𝒜
Tactic: have : (insert x s ∪ v) \ u ∈ 𝒜 := sup_sdiff_mem_of_mem_compression_of_notMem ‹_› (m _ ‹x ∉ s›)
-- 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 : (insert x s ∪ v) \ u ∈ 𝒜
⊢ u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
have hsv : Disjoint s v
Tactic: have hsv : Disjoint s v := hvs.symm.mono_left (subset_insert _ _)
-- 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 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
⊢ u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
have hvu : Disjoint v u
Tactic: have hvu : Disjoint v u := disjoint_of_subset_right hus hvs
-- 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 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
⊢ u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
have hxv : x ∉ v
Tactic: have hxv : x ∉ v := disjoint_right.1 hvs (mem_insert_self _ _)
-- 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 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
⊢ u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
have this₁ : v \ u = v
Tactic: have : v \ u = v := ‹Disjoint v u›.sdiff_eq_left
-- 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 : v \ u = v
hxu : x ∈ u
⊢ False
have obtain : ∀ (y : α) (hyv : y ∈ v) (hxy : IsCompressed (u.erase x) (v.erase y) 𝒜), False
Tactic: obtain ⟨y, hyv, hxy⟩ := huv x hxu
-- 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 : v \ u = v
hxu : x ∈ u
y : α
hyv : y ∈ v
hxy : IsCompressed (u.erase x) (v.erase y) 𝒜
⊢ False
have apply : insert y s ∈ 𝒜
Tactic: apply m y (disjoint_right.1 hsv hyv)
-- 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 : 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 ∈ 𝒜
have sup_sdiff_mem_of_mem_compression : v.erase y ≤ (insert x s ∪ v) \ u
Tactic: refine
        sup_sdiff_mem_of_mem_compression (by rwa [hxy.eq]) ?_
          (disjoint_of_subset_left (erase_subset _ _) 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 : 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 ∪ v) \ u
have rw : v.erase y ≤ insert x s \ u ∪ v
Tactic: rw [union_sdiff_distrib, ‹v \ u = v›]