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 a : α
inst_3 : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
h : ¬(Disjoint u b ∧ v ≤ b)
hba : b = a
⊢ Disjoint v 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), (a ⊔ v) \ u ∈ s
inr : ∀ (b : α) (hb : b ∈ s) (hba : compress u v b = a), (a ⊔ v) \ u ∈ s
⊢ (a ⊔ v) \ u ∈ s

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
⊢ (a ⊔ v) \ u ∈ s

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), (a ⊔ v) \ u ∈ s
neg : ∀ (h : ¬(Disjoint u b ∧ v ≤ b)) (hba : b = a), (a ⊔ v) \ u ∈ s
⊢ (a ⊔ v) \ u ∈ s

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 : ((b ⊔ u) \ v ⊔ v) \ u ∈ s
pos₁ : (b ⊔ u) \ u ∈ s
pos₂ : b \ u ∈ s
pos₃ pos₄ pos₅ pos₆ : b ∈ s
⊢ (a ⊔ v) \ u ∈ s

Tactic:
rwa [← hba, sdiff_sup_cancel (le_sup_of_le_left h.2), sup_sdiff_right_self,
      h.1.symm.sdiff_eq_left]

Premises used: sdiff_sup_cancel, sup_sdiff_right_self, le_sup_of_le_left, Disjoint.sdiff_eq_left, Disjoint.symm, 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 α
ha : a ∉ s
b : α
hb : b ∈ s
h : ¬(Disjoint u b ∧ v ≤ b)
hba : b = a
⊢ (a ⊔ v) \ u ∈ s

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 α
ha : a ∈ 𝓒 u v s
hva : v ≤ a
hua : Disjoint u a
⊢ a ∈ s ∧ (a ⊔ u) \ v ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a

Tactic:
rw [mem_compression, compress_of_disjoint_of_le hua hva] at ha

Premises used: UV.compress_of_disjoint_of_le, 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 ∈ 𝓒 u v s
hva : v ≤ a
hua : Disjoint u a
ha₁ : a ∈ s ∧ (a ⊔ u) \ v ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
⊢ v ≤ a

Tactic:
rw [mem_compression, compress_of_disjoint_of_le hua hva] at ha

Premises used: UV.compress_of_disjoint_of_le, 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 ∈ 𝓒 u v s
hva : v ≤ a
hua : Disjoint u a
ha₁ : a ∈ s ∧ (a ⊔ u) \ v ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
hva₁ : v ≤ a
⊢ Disjoint u a

Tactic:
rw [mem_compression, compress_of_disjoint_of_le hua hva] at ha

Premises used: UV.compress_of_disjoint_of_le, 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 ∧ (a ⊔ u) \ v ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
hva : v ≤ a
hua : Disjoint u a
inl : a ∈ s → ∀ (ha : (a ⊔ u) \ v ∈ s), (a ⊔ u) \ v ∈ s
inr :
  ∀ (b : α) (hb : b ∈ s) (hva : v ≤ compress u v b) (hua : Disjoint u (compress u v b)),
    compress u v b ∉ s → (compress u v b ⊔ u) \ v ∈ s
⊢ (a ⊔ u) \ v ∈ s

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 α
hva : v ≤ a
hua : Disjoint u a
left : a ∈ s
ha : (a ⊔ u) \ v ∈ s
⊢ (a ⊔ u) \ v ∈ s

Tactic:
ha
-- 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 α
hva : v ≤ a
hua : Disjoint u a
left : a ∈ s
ha : (a ⊔ u) \ v ∈ s
⊢ (a ⊔ u) \ v ∈ s

Tactic:
exact ha
-- 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
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left : compress u v b ∉ s
this : Disjoint u (u \ v)
rwa : ∀ (this : Disjoint u u), u = ⊥
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : u = ⊥), u = ⊥
⊢ u = ⊥

Tactic:
rwa [(hua.mono_right hva).sdiff_eq_left, disjoint_self] at this

Premises used: Disjoint.sdiff_eq_left, disjoint_self, 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 : α
inst_3 : DecidableEq α
b : α
hb : b ∈ s
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left : compress u v b ∉ s
suffices : Disjoint u (u \ v)
⊢ u = ⊥

Tactic:
suffices Disjoint u (u \ v) by rwa [(hua.mono_right hva).sdiff_eq_left, disjoint_self] at this
-- 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
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left : compress u v b ∉ s
⊢ Disjoint u (u \ v)

Tactic:
hua.mono_right ?_

Premises used: 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 : α
inst_3 : DecidableEq α
b : α
hb : b ∈ s
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left : compress u v b ∉ s
refine : u \ v ≤ compress u v b
⊢ Disjoint u (u \ v)

Tactic:
refine hua.mono_right ?_

Premises used: 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 : α
inst_3 : DecidableEq α
b : α
hb : b ∈ s
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left : compress u v b ∉ s
rw : u \ v ≤ (compress u v b ⊔ u) \ v
⊢ u \ v ≤ compress u v b

Tactic:
rw [← compress_idem, compress_of_disjoint_of_le hua hva]

Premises used: UV.compress_of_disjoint_of_le, 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
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left : compress u v b ∉ s
⊢ u \ v ≤ (compress u v b ⊔ u) \ v

Tactic:
sdiff_le_sdiff_right le_sup_right

Premises used: sdiff_le_sdiff_right, le_sup_right
-- 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
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left : compress u v b ∉ s
⊢ u \ v ≤ (compress u v b ⊔ u) \ v

Tactic:
exact sdiff_le_sdiff_right le_sup_right

Premises used: sdiff_le_sdiff_right, le_sup_right
-- 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
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left : compress u v b ∉ s
⊢ u = ⊥

Tactic:
have hu : u = ⊥ := by
    suffices Disjoint u (u \ v) by rwa [(hua.mono_right hva).sdiff_eq_left, disjoint_self] at this
    refine hua.mono_right ?_
    rw [← compress_idem, compress_of_disjoint_of_le hua hva]
    exact sdiff_le_sdiff_right le_sup_right
-- 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
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left : compress u v b ∉ s
hu : u = ⊥
rw : Disjoint v v
⊢ v = ⊥

Tactic:
rw [← disjoint_self]

Premises used: disjoint_self
-- 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
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left : compress u v b ∉ s
hu : u = ⊥
apply : Disjoint v (compress u v b)
⊢ Disjoint v v

Tactic:
apply Disjoint.mono_right hva

Premises used: 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 : α
inst_3 : DecidableEq α
b : α
hb : b ∈ s
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left : compress u v b ∉ s
hu : u = ⊥
rw : Disjoint v ((compress u v b ⊔ u) \ v)
⊢ Disjoint v (compress u v b)

Tactic:
rw [← compress_idem, compress_of_disjoint_of_le hua hva]

Premises used: UV.compress_of_disjoint_of_le, 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
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left : compress u v b ∉ s
hu : u = ⊥
⊢ Disjoint v ((compress u 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 : α
inst_3 : DecidableEq α
b : α
hb : b ∈ s
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left : compress u v b ∉ s
hu : u = ⊥
⊢ Disjoint v ((compress u v b ⊔ u) \ v)

Tactic:
exact 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 : α
inst_3 : DecidableEq α
b : α
hb : b ∈ s
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left : compress u v b ∉ s
hu : u = ⊥
⊢ v = ⊥

Tactic:
have hv : v = ⊥ := by
    rw [← disjoint_self]
    apply Disjoint.mono_right hva
    rw [← compress_idem, compress_of_disjoint_of_le hua hva]
    exact 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 : α
inst_3 : DecidableEq α
b : α
hb : b ∈ s
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left : compress u v b ∉ s
hu : u = ⊥
hv : v = ⊥
inr : (compress ⊥ v b ⊔ ⊥) \ v ∈ s
inr₁ : (compress ⊥ ⊥ b ⊔ ⊥) \ ⊥ ∈ s
inr₂ : (b ⊔ ⊥) \ ⊥ ∈ s
inr₃ : b \ ⊥ ∈ s
inr₄ inr₅ inr₆ inr₇ : b ∈ s
⊢ (compress u v b ⊔ u) \ v ∈ s

Tactic:
rwa [hu, hv, compress_self, sup_bot_eq, sdiff_bot]

Premises used: UV.compress_self, sup_bot_eq, sdiff_bot
-- 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
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
⊢ a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a

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 ∈ 𝓒 u v s
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
ha₁ : a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
⊢ v ≤ a

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 ∈ 𝓒 u v s
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
ha₁ : a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
hva₁ : v ≤ a
⊢ v = ⊥ → u = ⊥

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
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
inl : ∀ (ha : a ∈ s ∧ compress u v a ∈ s), a ∈ s
inr : a ∉ s → ∀ (b : α) (hb : b ∈ s) (h : compress u v b = a), a ∈ s
⊢ a ∈ s

Tactic:
obtain ha | ⟨_, b, hb, h⟩ := ha
-- 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 α
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
ha : a ∈ s ∧ compress u v a ∈ s
⊢ a ∈ s

Tactic:
ha.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 α
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
ha : a ∈ s ∧ compress u v a ∈ s
⊢ a ∈ s

Tactic:
exact ha.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 α
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
left : a ∉ s
b : α
hb : b ∈ s
h : (if Disjoint u b ∧ v ≤ b then (b ⊔ u) \ v else b) = a
pos : Disjoint u b ∧ v ≤ b → ∀ (h : (b ⊔ u) \ v = a), a ∈ s
neg : ¬(Disjoint u b ∧ v ≤ b) → ∀ (h : b = a), a ∈ s
⊢ a ∈ s

Tactic:
split_ifs at 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 α
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
left : a ∉ s
b : α
hb : b ∈ s
h_1 : Disjoint u b ∧ v ≤ b
h : (b ⊔ u) \ v = a
⊢ v = ⊥

Tactic:
rw [← h, le_sdiff_right] at hva

Premises used: le_sdiff_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 α
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
left : a ∉ s
b : α
hb : b ∈ s
h_1 : Disjoint u b ∧ v ≤ b
h : (b ⊔ u) \ v = a
hva₁ : v = ⊥
⊢ b ∈ s

Tactic:
rw [← h, le_sdiff_right] at hva

Premises used: le_sdiff_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 α
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
left : a ∉ s
b : α
hb : b ∈ s
h_1 : Disjoint u b ∧ v ≤ b
h : (b ⊔ u) \ v = a
hva₁ : v = ⊥
hb₁ : b ∈ s
⊢ Disjoint u b ∧ v ≤ b

Tactic:
rw [← h, le_sdiff_right] at hva

Premises used: le_sdiff_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 α
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
left : a ∉ s
b : α
hb : b ∈ s
h_1 : Disjoint u b ∧ v ≤ b
h : (b ⊔ u) \ v = a
hva₁ : v = ⊥
hb₁ : b ∈ s
h₁ : Disjoint u b ∧ v ≤ b
⊢ (b ⊔ u) \ v = a

Tactic:
rw [← h, le_sdiff_right] at hva

Premises used: le_sdiff_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 α
hvu : v = ⊥ → u = ⊥
left : a ∉ s
b : α
hva : v = ⊥
hb : b ∈ s
h_1 : Disjoint u b ∧ v ≤ b
h : (b ⊔ u) \ v = a
pos : (b ⊔ u) \ v ∈ s
pos₁ : (b ⊔ ⊥) \ v ∈ s
pos₂ : (b ⊔ ⊥) \ ⊥ ∈ s
pos₃ : b \ ⊥ ∈ s
pos₄ pos₅ pos₆ pos₇ : b ∈ s
⊢ a ∈ s

Tactic:
rwa [← h, hvu hva, hva, sup_bot_eq, sdiff_bot]

Premises used: sup_bot_eq, sdiff_bot
-- 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 α
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
left : a ∉ s
b : α
hb : b ∈ s
h_1 : ¬(Disjoint u b ∧ v ≤ b)
h : b = a
neg neg₁ neg₂ neg₃ : b ∈ s
⊢ a ∈ s

Tactic:
rwa [← h]
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
u v : Finset α
huv : #u = #v
a : Finset α
pos : ∀ (h : Disjoint u a ∧ v ≤ a), #((a ⊔ u) \ v) = #a
neg : ∀ (h : ¬(Disjoint u a ∧ v ≤ a)), #a = #a
⊢ #(if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a) = #a

Tactic:
split_ifs with h
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
u v : Finset α
huv : #u = #v
a : Finset α
h : Disjoint u a ∧ v ≤ a
pos : #(a ⊔ u) - #v = #a
pos₁ : #(a ∪ u) - #v = #a
pos₂ : #a + #u - #v = #a
pos₃ : #a + #v - #v = #a
pos₄ pos₅ : #a = #a
⊢ #((a ⊔ u) \ v) = #a

Tactic:
rw [card_sdiff_of_subset (h.2.trans le_sup_left), sup_eq_union,
      card_union_of_disjoint h.1.symm, huv, add_tsub_cancel_right]

Premises used: le_sup_left, Finset.card_sdiff_of_subset, Disjoint.symm, And.right, And.left, add_tsub_cancel_right, LE.le.trans, Finset.sup_eq_union, Finset.card_union_of_disjoint
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
u v : Finset α
huv : #u = #v
a : Finset α
h : ¬(Disjoint u a ∧ v ≤ a)
⊢ #a = #a

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
r : ℕ
huv : #u = #v
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
simp_rw : ∀ ⦃x : Finset α⦄, (x ∈ 𝒜 ∧ compress u v x ∈ 𝒜 ∨ x ∉ 𝒜 ∧ ∃ b ∈ 𝒜, compress u v b = x) → #x = r
⊢ Set.Sized r (↑(𝓒 u v 𝒜) : Set (Finset α))

Tactic:
simp_rw [Set.Sized, mem_coe, mem_compression]

Premises used: Set.Sized, UV.mem_compression, Finset.mem_coe
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
r : ℕ
huv : #u = #v
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
s : Finset α
hs : s ∈ 𝒜 ∧ compress u v s ∈ 𝒜
⊢ #s = r

Tactic:
h𝒜 hs.1

Premises used: And.left
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
r : ℕ
huv : #u = #v
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
s : Finset α
hs : s ∈ 𝒜 ∧ compress u v s ∈ 𝒜
⊢ #s = r

Tactic:
exact h𝒜 hs.1

Premises used: And.left
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
r : ℕ
huv : #u = #v
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
t : Finset α
ht : t ∈ 𝒜
huvt : compress u v t ∉ 𝒜
inr : #t = r
inr₁ inr₂ : r = r
⊢ #(compress u v t) = r

Tactic:
rw [card_compress huv, h𝒜 ht]

Premises used: UV.card_compress
-- 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) 𝒜
⊢ v = ∅ → u = ∅

Tactic:
grind
-- 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) 𝒜
set :
  let 𝒜' := 𝓒 u v 𝒜;
  ∂ 𝒜' ⊆ 𝓒 u v (∂ 𝒜)
⊢ ∂ (𝓒 u v 𝒜) ⊆ 𝓒 u v (∂ 𝒜)

Tactic:
set 𝒜' := 𝓒 u v 𝒜

Premises used: UV.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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
rw : s ∈ ∂ 𝒜 ∧ compress u v s ∈ ∂ 𝒜 ∨ s ∉ ∂ 𝒜 ∧ ∃ b ∈ ∂ 𝒜, compress u v b = s
⊢ s ∈ 𝓒 u v (∂ 𝒜)

Tactic:
rw [mem_compression]

Premises used: UV.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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
pos : ∀ (hs : s ∈ ∂ 𝒜), s ∈ ∂ 𝒜 ∧ compress u v s ∈ ∂ 𝒜 ∨ s ∉ ∂ 𝒜 ∧ ∃ b ∈ ∂ 𝒜, compress u v b = s
neg : ∀ (hs : s ∉ ∂ 𝒜), s ∈ ∂ 𝒜 ∧ compress u v s ∈ ∂ 𝒜 ∨ s ∉ ∂ 𝒜 ∧ ∃ b ∈ ∂ 𝒜, compress u v b = s
⊢ s ∈ ∂ 𝒜 ∧ compress u v s ∈ ∂ 𝒜 ∨ s ∉ ∂ 𝒜 ∧ ∃ b ∈ ∂ 𝒜, compress u v b = s

Tactic:
by_cases hs : s ∈ 𝒜.shadow

Premises used: Finset.shadow
-- 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
hs : s ∉ ∂ 𝒜
⊢ u ⊆ s

Tactic:
obtain ⟨hus, hvs, h, _⟩ := H _ hs' hs
-- 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
hs : s ∉ ∂ 𝒜
hus : u ⊆ s
⊢ Disjoint v s

Tactic:
obtain ⟨hus, hvs, h, _⟩ := H _ hs' hs
-- 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
hs : s ∉ ∂ 𝒜
hus : u ⊆ s
hvs : Disjoint v s
⊢ (s ∪ v) \ u ∈ ∂ 𝒜

Tactic:
obtain ⟨hus, hvs, h, _⟩ := H _ hs' hs