awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v : α
inst_3 : DecidableEq α
a b : α
hb : b ∈ s ∧ compress u v b ∉ s
has : Disjoint u a ∧ v ≤ a
ha : a ∈ s ∧ (a ⊔ u) \ v ∉ s
hab : (a ⊔ u) \ v = compress u v b
⊢ b ∈ s ∧ (if Disjoint u b ∧ v ≤ b then (b ⊔ u) \ v else b) ∉ s

Tactic:
rw [compress] at hb hab

Premises used: UV.compress
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v : α
inst_3 : DecidableEq α
a b : α
hb : b ∈ s ∧ compress u v b ∉ s
has : Disjoint u a ∧ v ≤ a
ha : a ∈ s ∧ (a ⊔ u) \ v ∉ s
hab : (a ⊔ u) \ v = compress u v b
hb₁ : b ∈ s ∧ (if Disjoint u b ∧ v ≤ b then (b ⊔ u) \ v else b) ∉ s
⊢ Disjoint u a ∧ v ≤ a

Tactic:
rw [compress] at hb hab

Premises used: UV.compress
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v : α
inst_3 : DecidableEq α
a b : α
hb : b ∈ s ∧ compress u v b ∉ s
has : Disjoint u a ∧ v ≤ a
ha : a ∈ s ∧ (a ⊔ u) \ v ∉ s
hab : (a ⊔ u) \ v = compress u v b
hb₁ : b ∈ s ∧ (if Disjoint u b ∧ v ≤ b then (b ⊔ u) \ v else b) ∉ s
has₁ : Disjoint u a ∧ v ≤ a
⊢ a ∈ s ∧ (a ⊔ u) \ v ∉ s

Tactic:
rw [compress] at hb hab

Premises used: UV.compress
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v : α
inst_3 : DecidableEq α
a b : α
hb : b ∈ s ∧ compress u v b ∉ s
has : Disjoint u a ∧ v ≤ a
ha : a ∈ s ∧ (a ⊔ u) \ v ∉ s
hab : (a ⊔ u) \ v = compress u v b
hb₁ : b ∈ s ∧ (if Disjoint u b ∧ v ≤ b then (b ⊔ u) \ v else b) ∉ s
has₁ : Disjoint u a ∧ v ≤ a
ha₁ : a ∈ s ∧ (a ⊔ u) \ v ∉ s
⊢ (a ⊔ u) \ v = if Disjoint u b ∧ v ≤ b then (b ⊔ u) \ v else b

Tactic:
rw [compress] at hb hab

Premises used: UV.compress
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v : α
inst_3 : DecidableEq α
a b : α
hb : b ∈ s ∧ (if Disjoint u b ∧ v ≤ b then (b ⊔ u) \ v else b) ∉ s
has : Disjoint u a ∧ v ≤ a
ha : a ∈ s ∧ (a ⊔ u) \ v ∉ s
hab : (a ⊔ u) \ v = if Disjoint u b ∧ v ≤ b then (b ⊔ u) \ v else b
pos : ∀ (hbs : Disjoint u b ∧ v ≤ b) (hb : b ∈ s ∧ (b ⊔ u) \ v ∉ s) (hab : (a ⊔ u) \ v = (b ⊔ u) \ v), a = b
neg : ∀ (hbs : ¬(Disjoint u b ∧ v ≤ b)) (hb : b ∈ s ∧ b ∉ s) (hab : (a ⊔ u) \ v = b), a = b
⊢ a = b

Tactic:
split_ifs at hb hab with hbs
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v : α
inst_3 : DecidableEq α
a b : α
has : Disjoint u a ∧ v ≤ a
ha : a ∈ s ∧ (a ⊔ u) \ v ∉ s
hbs : Disjoint u b ∧ v ≤ b
hb : b ∈ s ∧ (b ⊔ u) \ v ∉ s
hab : (a ⊔ u) \ v = (b ⊔ u) \ v
⊢ a = b

Tactic:
sup_sdiff_injOn u v has hbs hab

Premises used: sup_sdiff_injOn
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v : α
inst_3 : DecidableEq α
a b : α
has : Disjoint u a ∧ v ≤ a
ha : a ∈ s ∧ (a ⊔ u) \ v ∉ s
hbs : Disjoint u b ∧ v ≤ b
hb : b ∈ s ∧ (b ⊔ u) \ v ∉ s
hab : (a ⊔ u) \ v = (b ⊔ u) \ v
⊢ a = b

Tactic:
exact sup_sdiff_injOn u v has hbs hab

Premises used: sup_sdiff_injOn
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v : α
inst_3 : DecidableEq α
a b : α
has : Disjoint u a ∧ v ≤ a
ha : a ∈ s ∧ (a ⊔ u) \ v ∉ s
hbs : ¬(Disjoint u b ∧ v ≤ b)
hb : b ∈ s ∧ b ∉ s
hab : (a ⊔ u) \ v = b
⊢ a = b

Tactic:
(hb.2 hb.1).elim

Premises used: False.elim, And.right, And.left
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v : α
inst_3 : DecidableEq α
a b : α
has : Disjoint u a ∧ v ≤ a
ha : a ∈ s ∧ (a ⊔ u) \ v ∉ s
hbs : ¬(Disjoint u b ∧ v ≤ b)
hb : b ∈ s ∧ b ∉ s
hab : (a ⊔ u) \ v = b
⊢ a = b

Tactic:
exact (hb.2 hb.1).elim

Premises used: False.elim, And.right, And.left
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v : α
inst_3 : DecidableEq α
a b : α
hb : b ∈ s ∧ compress u v b ∉ s
has : ¬(Disjoint u a ∧ v ≤ a)
ha : a ∈ s ∧ a ∉ s
hab : a = compress u v b
⊢ a = b

Tactic:
(ha.2 ha.1).elim

Premises used: False.elim, And.right, And.left
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v : α
inst_3 : DecidableEq α
a b : α
hb : b ∈ s ∧ compress u v b ∉ s
has : ¬(Disjoint u a ∧ v ≤ a)
ha : a ∈ s ∧ a ∉ s
hab : a = compress u v b
⊢ a = b

Tactic:
exact (ha.2 ha.1).elim

Premises used: False.elim, And.right, And.left
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v a : α
inst_3 : DecidableEq α
simp_rw :
  a ∈ {a ∈ s | compress u v a ∈ s} ∪ {a ∈ image (compress u v) s | a ∉ s} ↔
    a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
simp_rw₁ :
  a ∈ {a ∈ s | compress u v a ∈ s} ∨ a ∈ {a ∈ image (compress u v) s | a ∉ s} ↔
    a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
simp_rw₂ :
  a ∈ s ∧ compress u v a ∈ s ∨ a ∈ image (compress u v) s ∧ a ∉ s ↔
    a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
simp_rw₃ :
  a ∈ s ∧ compress u v a ∈ s ∨ (∃ a_1 ∈ s, compress u v a_1 = a) ∧ a ∉ s ↔
    a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ a_1 ∈ s, compress u v a_1 = a
⊢ a ∈ 𝓒 u v s ↔ a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a

Tactic:
simp_rw [compression, mem_union, mem_filter, mem_image, and_comm]

Premises used: Finset.mem_image, UV.compression, and_comm, Finset.mem_filter, Finset.mem_union
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v : α
inst_3 : DecidableEq α
h : IsCompressed u v s
⊢ 𝓒 u v s = s

Tactic:
h

Premises used: UV.IsCompressed
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
inst_3 : DecidableEq α
u : α
s : Finset α
⊢ 𝓒 u u s = s

Tactic:
grind [mem_compression]

Premises used: UV.mem_compression
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
inst_3 : DecidableEq α
u : α
s : Finset α
⊢ IsCompressed u u s

Tactic:
compression_self u s

Premises used: UV.compression_self, UV.IsCompressed
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v : α
inst_3 : DecidableEq α
⊢ Disjoint ({a ∈ s | compress u v a ∈ s}) ({a ∈ image (compress u v) s | a ∉ s})

Tactic:
disjoint_left.2 fun _a ha₁ ha₂ ↦ (mem_filter.1 ha₂).2 (mem_filter.1 ha₁).1

Premises used: Iff.mpr, And.right, And.left, Iff.mp, Finset.mem_filter, Finset.disjoint_left
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v a : α
inst_3 : DecidableEq α
ha : a ∈ s
rw :
  compress u v a ∈ s ∧ compress u v (compress u v a) ∈ s ∨ compress u v a ∉ s ∧ ∃ b ∈ s, compress u v b = compress u v a
⊢ compress u v a ∈ 𝓒 u v s

Tactic:
rw [mem_compression]

Premises used: UV.mem_compression
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v a : α
inst_3 : DecidableEq α
ha : a ∈ s
pos :
  ∀ (h : compress u v a ∈ s),
    compress u v a ∈ s ∧ compress u v (compress u v a) ∈ s ∨
      compress u v a ∉ s ∧ ∃ b ∈ s, compress u v b = compress u v a
neg :
  ∀ (h : compress u v a ∉ s),
    compress u v a ∈ s ∧ compress u v (compress u v a) ∈ s ∨
      compress u v a ∉ s ∧ ∃ b ∈ s, compress u v b = compress u v a
⊢ compress u v a ∈ s ∧ compress u v (compress u v a) ∈ s ∨ compress u v a ∉ s ∧ ∃ b ∈ s, compress u v b = compress u v a

Tactic:
by_cases h : compress u v a ∈ s

Premises used: UV.compress
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v a : α
inst_3 : DecidableEq α
ha : a ∈ s
h : compress u v a ∈ s
pos : compress u v a ∈ s ∧ compress u v a ∈ s ∨ compress u v a ∉ s ∧ ∃ b ∈ s, compress u v b = compress u v a
⊢ compress u v a ∈ s ∧ compress u v (compress u v a) ∈ s ∨ compress u v a ∉ s ∧ ∃ b ∈ s, compress u v b = compress u v a

Tactic:
rw [compress_idem]

Premises used: UV.compress_idem
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v a : α
inst_3 : DecidableEq α
ha : a ∈ s
h : compress u v a ∈ s
⊢ compress u v a ∈ s ∧ compress u v a ∈ s ∨ compress u v a ∉ s ∧ ∃ b ∈ s, compress u v b = compress u v a

Tactic:
Or.inl ⟨h, h⟩

Premises used: And.intro, Or.inl
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v a : α
inst_3 : DecidableEq α
ha : a ∈ s
h : compress u v a ∈ s
⊢ compress u v a ∈ s ∧ compress u v a ∈ s ∨ compress u v a ∉ s ∧ ∃ b ∈ s, compress u v b = compress u v a

Tactic:
exact Or.inl ⟨h, h⟩

Premises used: Or.inl
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v a : α
inst_3 : DecidableEq α
ha : a ∈ s
h : compress u v a ∉ s
⊢ compress u v a ∈ s ∧ compress u v (compress u v a) ∈ s ∨ compress u v a ∉ s ∧ ∃ b ∈ s, compress u v b = compress u v a

Tactic:
Or.inr ⟨h, a, ha, rfl⟩

Premises used: And.intro, Exists.intro, Or.inr, rfl
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v a : α
inst_3 : DecidableEq α
ha : a ∈ s
h : compress u v a ∉ s
⊢ compress u v a ∈ s ∧ compress u v (compress u v a) ∈ s ∨ compress u v a ∉ s ∧ ∃ b ∈ s, compress u v b = compress u v a

Tactic:
exact Or.inr ⟨h, a, ha, rfl⟩

Premises used: Or.inr
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v a : α
inst_3 : DecidableEq α
ha : a ∈ 𝓒 u v s
rw :
  ∀ (ha : a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a),
    compress u v a ∈ s ∧ compress u v (compress u v a) ∈ s ∨
      compress u v a ∉ s ∧ ∃ b ∈ s, compress u v b = compress u v a
⊢ compress u v a ∈ 𝓒 u v s

Tactic:
rw [mem_compression] at ha ⊢

Premises used: UV.mem_compression
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v a : α
inst_3 : DecidableEq α
ha : a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
simp : compress u v a ∈ s ∧ compress u v a ∈ s ∨ compress u v a ∉ s ∧ ∃ b ∈ s, compress u v b = compress u v a
⊢ compress u v a ∈ s ∧ compress u v (compress u v a) ∈ s ∨ compress u v a ∉ s ∧ ∃ b ∈ s, compress u v b = compress u v a

Tactic:
simp only [compress_idem]

Premises used: UV.compress_idem
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v a : α
inst_3 : DecidableEq α
ha : a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
inl :
  a ∈ s →
    ∀ (ha : compress u v a ∈ s),
      compress u v a ∈ s ∧ compress u v a ∈ s ∨ compress u v a ∉ s ∧ ∃ b ∈ s, compress u v b = compress u v a
inr :
  ∀ (b : α) (hb : b ∈ s),
    compress u v b ∉ s →
      compress u v (compress u v b) ∈ s ∧ compress u v (compress u v b) ∈ s ∨
        compress u v (compress u v b) ∉ s ∧ ∃ b_1 ∈ s, compress u v b_1 = compress u v (compress u v b)
⊢ compress u v a ∈ s ∧ compress u v a ∈ s ∨ compress u v a ∉ s ∧ ∃ b ∈ s, compress u v b = compress u v a

Tactic:
obtain ⟨_, ha⟩ | ⟨_, b, hb, rfl⟩ := ha

Premises used: rfl
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v a : α
inst_3 : DecidableEq α
left : a ∈ s
ha : compress u v a ∈ s
⊢ compress u v a ∈ s ∧ compress u v a ∈ s ∨ compress u v a ∉ s ∧ ∃ b ∈ s, compress u v b = compress u v a

Tactic:
Or.inl ⟨ha, ha⟩

Premises used: And.intro, Or.inl
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v a : α
inst_3 : DecidableEq α
left : a ∈ s
ha : compress u v a ∈ s
⊢ compress u v a ∈ s ∧ compress u v a ∈ s ∨ compress u v a ∉ s ∧ ∃ b ∈ s, compress u v b = compress u v a

Tactic:
exact Or.inl ⟨ha, ha⟩

Premises used: Or.inl
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v : α
inst_3 : DecidableEq α
b : α
hb : b ∈ s
left rwa rwa₁ rwa₂ rwa₃ : compress u v b ∉ s
⊢ compress u v (compress u v b) ∉ s

Tactic:
rwa [compress_idem]

Premises used: UV.compress_idem
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v : α
inst_3 : DecidableEq α
b : α
hb : b ∈ s
left : compress u v b ∉ s
⊢ compress u v (compress u v b) ∈ s ∧ compress u v (compress u v b) ∈ s ∨
    compress u v (compress u v b) ∉ s ∧ ∃ b_1 ∈ s, compress u v b_1 = compress u v (compress u v b)

Tactic:
exact Or.inr ⟨by rwa [compress_idem], b, hb, (compress_idem _ _ _).symm⟩

Premises used: Or.inr
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
inst_3 : DecidableEq α
u v : α
s : Finset α
⊢ {a ∈ 𝓒 u v s | compress u v a ∉ 𝓒 u v s} = ∅

Tactic:
have h : {a ∈ 𝓒 u v s | compress u v a ∉ 𝓒 u v s} = ∅ :=
    filter_false_of_mem fun a ha h ↦ h <| compress_mem_compression_of_mem_compression ha
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
inst_3 : DecidableEq α
u v : α
s : Finset α
h : {a ∈ 𝓒 u v s | compress u v a ∉ 𝓒 u v s} = ∅
rw : {a ∈ 𝓒 u v s | compress u v a ∈ 𝓒 u v s} ∪ {a ∈ 𝓒 u v s | compress u v a ∉ 𝓒 u v s} = 𝓒 u v s
⊢ 𝓒 u v (𝓒 u v s) = 𝓒 u v s

Tactic:
rw [compression, filter_image, h, image_empty, ← h]

Premises used: Finset.image_empty, UV.compression, Finset.filter_image
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
inst_3 : DecidableEq α
u v : α
s : Finset α
h : {a ∈ 𝓒 u v s | compress u v a ∉ 𝓒 u v s} = ∅
⊢ {a ∈ 𝓒 u v s | compress u v a ∈ 𝓒 u v s} ∪ {a ∈ 𝓒 u v s | compress u v a ∉ 𝓒 u v s} = 𝓒 u v s

Tactic:
filter_union_filter_not_eq _ (compression u v s)

Premises used: UV.compression, Finset.filter_union_filter_not_eq
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
inst_3 : DecidableEq α
u v : α
s : Finset α
h : {a ∈ 𝓒 u v s | compress u v a ∉ 𝓒 u v s} = ∅
⊢ {a ∈ 𝓒 u v s | compress u v a ∈ 𝓒 u v s} ∪ {a ∈ 𝓒 u v s | compress u v a ∉ 𝓒 u v s} = 𝓒 u v s

Tactic:
exact filter_union_filter_not_eq _ (compression u v s)

Premises used: UV.compression, Finset.filter_union_filter_not_eq
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
inst_3 : DecidableEq α
u v : α
s : Finset α
rw : #({a ∈ s | compress u v a ∈ s} ∪ {a ∈ image (compress u v) s | a ∉ s}) = #s
rw₁ : #({a ∈ s | compress u v a ∈ s}) + #({a ∈ image (compress u v) s | a ∉ s}) = #s
rw₂ : #({a ∈ s | compress u v a ∈ s}) + #(image (compress u v) ({a ∈ s | compress u v a ∉ s})) = #s
rw₃ : #({a ∈ s | compress u v a ∈ s}) + #({a ∈ s | compress u v a ∉ s}) = #s
rw₄ : #({a ∈ s | compress u v a ∈ s} ∪ {a ∈ s | compress u v a ∉ s}) = #s
rw₅ rw₆ : #s = #s
⊢ #(𝓒 u v s) = #s

Tactic:
rw [compression, card_union_of_disjoint compress_disjoint, filter_image,
    card_image_of_injOn compress_injOn, ← card_union_of_disjoint (disjoint_filter_filter_not s _ _),
    filter_union_filter_not_eq]

Premises used: UV.compress_injOn, UV.compression, Finset.disjoint_filter_filter_not, Finset.filter_union_filter_not_eq, Finset.card_image_of_injOn, UV.compress_disjoint, Finset.filter_image, Finset.card_union_of_disjoint
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v a : α
inst_3 : DecidableEq α
h : a ∈ 𝓒 u v s
ha : a ∉ s
⊢ a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a

Tactic:
rw [mem_compression] at h

Premises used: UV.mem_compression
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v a : α
inst_3 : DecidableEq α
h : a ∈ 𝓒 u v s
ha : a ∉ s
h₁ : a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
⊢ a ∉ s

Tactic:
rw [mem_compression] at h

Premises used: UV.mem_compression
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v a : α
inst_3 : DecidableEq α
h : a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
ha : a ∉ s
inl : ∀ (h : a ∈ s ∧ compress u v a ∈ s), u ≤ a
inr : ∀ (b : α) (hb : b ∈ s) (hba : compress u v b = a), u ≤ a
⊢ u ≤ a

Tactic:
obtain h | ⟨-, b, hb, hba⟩ := h
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v a : α
inst_3 : DecidableEq α
ha : a ∉ s
h : a ∈ s ∧ compress u v a ∈ s
⊢ u ≤ a

Tactic:
cases ha h.1

Premises used: And.left
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v a : α
inst_3 : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
hba : (if Disjoint u b ∧ v ≤ b then (b ⊔ u) \ v else b) = a
pos : ∀ (h : Disjoint u b ∧ v ≤ b) (hba : (b ⊔ u) \ v = a), u ≤ a
neg : ∀ (h : ¬(Disjoint u b ∧ v ≤ b)) (hba : b = a), u ≤ a
⊢ u ≤ a

Tactic:
split_ifs at hba with h
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v a : α
inst_3 : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
h : Disjoint u b ∧ v ≤ b
hba : (b ⊔ u) \ v = a
pos : u ≤ b ⊔ u ∧ Disjoint u v
⊢ u ≤ a

Tactic:
rw [← hba, le_sdiff]

Premises used: le_sdiff
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v a : α
inst_3 : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
h : Disjoint u b ∧ v ≤ b
hba : (b ⊔ u) \ v = a
⊢ u ≤ b ⊔ u ∧ Disjoint u v

Tactic:
⟨le_sup_right, h.1.mono_right h.2⟩

Premises used: le_sup_right, And.right, And.left, And.intro, Disjoint.mono_right
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v a : α
inst_3 : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
h : Disjoint u b ∧ v ≤ b
hba : (b ⊔ u) \ v = a
⊢ u ≤ b ⊔ u ∧ Disjoint u v

Tactic:
exact ⟨le_sup_right, h.1.mono_right h.2⟩
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v a : α
inst_3 : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
h : ¬(Disjoint u b ∧ v ≤ b)
hba : b = a
⊢ u ≤ a

Tactic:
cases ne_of_mem_of_not_mem hb ha hba

Premises used: ne_of_mem_of_not_mem
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v a : α
inst_3 : DecidableEq α
h : a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
ha : a ∉ s
inl : ∀ (h : a ∈ s ∧ compress u v a ∈ s), Disjoint v a
inr : ∀ (b : α) (hb : b ∈ s) (hba : compress u v b = a), Disjoint v a
⊢ Disjoint v a

Tactic:
obtain h | ⟨-, b, hb, hba⟩ := h
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v a : α
inst_3 : DecidableEq α
ha : a ∉ s
h : a ∈ s ∧ compress u v a ∈ s
⊢ Disjoint v a

Tactic:
cases ha h.1

Premises used: And.left
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v a : α
inst_3 : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
hba : (if Disjoint u b ∧ v ≤ b then (b ⊔ u) \ v else b) = a
pos : Disjoint u b ∧ v ≤ b → ∀ (hba : (b ⊔ u) \ v = a), Disjoint v a
neg : ¬(Disjoint u b ∧ v ≤ b) → ∀ (hba : b = a), Disjoint v a
⊢ Disjoint v a

Tactic:
split_ifs at hba
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v a : α
inst_3 : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
h : Disjoint u b ∧ v ≤ b
hba : (b ⊔ u) \ v = a
pos : Disjoint v ((b ⊔ u) \ v)
⊢ Disjoint v a

Tactic:
rw [← hba]
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v a : α
inst_3 : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
h : Disjoint u b ∧ v ≤ b
hba : (b ⊔ u) \ v = a
⊢ Disjoint v ((b ⊔ u) \ v)

Tactic:
disjoint_sdiff_self_right

Premises used: disjoint_sdiff_self_right
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
s : Finset α
u v a : α
inst_3 : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
h : Disjoint u b ∧ v ≤ b
hba : (b ⊔ u) \ v = a
⊢ Disjoint v ((b ⊔ u) \ v)

Tactic:
exact disjoint_sdiff_self_right

Premises used: disjoint_sdiff_self_right