awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
𝒜_1 : Finset (Finset α)
empty : p ∅
singleton_empty : p {∅}
image_insert : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, (∀ s ∈ 𝒜, a ∉ s) → p 𝒜 → p (image (insert a) 𝒜)
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p ({s ∈ 𝒜 | a ∉ s}) → p ({s ∈ 𝒜 | a ∈ s}) → p 𝒜
a : α
𝒜 : Finset (Finset α)
h𝒜₀ : p (nonMemberSubfamily a 𝒜)
h𝒜₁ : p (memberSubfamily a 𝒜)
rw : p (image (insert a) (memberSubfamily a 𝒜))
⊢ p ({s ∈ 𝒜 | a ∈ s})

Tactic:
rw [← image_insert_memberSubfamily]

Premises used: Finset.image_insert_memberSubfamily
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
𝒜_1 : Finset (Finset α)
empty : p ∅
singleton_empty : p {∅}
image_insert : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, (∀ s ∈ 𝒜, a ∉ s) → p 𝒜 → p (image (insert a) 𝒜)
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p ({s ∈ 𝒜 | a ∉ s}) → p ({s ∈ 𝒜 | a ∈ s}) → p 𝒜
a : α
𝒜 : Finset (Finset α)
h𝒜₀ : p (nonMemberSubfamily a 𝒜)
h𝒜₁ : p (memberSubfamily a 𝒜)
⊢ ∀ s ∈ memberSubfamily a 𝒜, a ∉ s

Tactic:
simp
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
p : Finset (Finset α) → Prop
𝒜_1 : Finset (Finset α)
empty : p ∅
singleton_empty : p {∅}
image_insert : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, (∀ s ∈ 𝒜, a ∉ s) → p 𝒜 → p (image (insert a) 𝒜)
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p ({s ∈ 𝒜 | a ∉ s}) → p ({s ∈ 𝒜 | a ∈ s}) → p 𝒜
a : α
𝒜 : Finset (Finset α)
h𝒜₀ : p (nonMemberSubfamily a 𝒜)
h𝒜₁ : p (memberSubfamily a 𝒜)
⊢ p (image (insert a) (memberSubfamily a 𝒜))

Tactic:
exact image_insert _ (by simp) h𝒜₁
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
simp_rw : s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ (∃ a_1 ∈ 𝒜, a_1.erase a = s) ∧ s ∉ 𝒜 ↔ s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ insert a s ∈ 𝒜 ∧ s ∉ 𝒜
⊢ s ∈ 𝓓 a 𝒜 ↔ s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s ∉ 𝒜 ∧ insert a s ∈ 𝒜

Tactic:
simp_rw [compression, mem_disjUnion, mem_filter, mem_image, and_comm (a := s ∉ 𝒜)]

Premises used: Finset.mem_image, and_comm, Finset.mem_disjUnion, Finset.mem_filter, Down.compression
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ (∃ a_1 ∈ 𝒜, a_1.erase a = s) ∧ s ∉ 𝒜 ↔ s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ insert a s ∈ 𝒜 ∧ s ∉ 𝒜

Tactic:
or_congr_right
      (and_congr_left fun hs =>
        ⟨?_, fun h => ⟨_, h, erase_insert <| insert_ne_self.1 <| ne_of_mem_of_not_mem h hs⟩⟩)

Premises used: Insert.insert, ne_of_mem_of_not_mem, and_congr_left, Finset.erase_insert, Finset.insert_ne_self, or_congr_right, And.intro, Iff.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
fun : ∀ (hs : s ∉ 𝒜), (∃ a_1 ∈ 𝒜, a_1.erase a = s) → insert a s ∈ 𝒜
⊢ s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ (∃ a_1 ∈ 𝒜, a_1.erase a = s) ∧ s ∉ 𝒜 ↔ s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ insert a s ∈ 𝒜 ∧ s ∉ 𝒜

Tactic:
refine
    or_congr_right
      (and_congr_left fun hs =>
        ⟨?_, fun h => ⟨_, h, erase_insert <| insert_ne_self.1 <| ne_of_mem_of_not_mem h hs⟩⟩)

Premises used: and_congr_left, or_congr_right, Iff.intro
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
t : Finset α
ht : t ∈ 𝒜
hs : t.erase a ∉ 𝒜
rwa rwa₁ rwa₂ rwa₃ : t ∈ 𝒜
⊢ insert a (t.erase a) ∈ 𝒜

Tactic:
rwa [insert_erase (erase_ne_self.1 (ne_of_mem_of_not_mem ht hs).symm)]

Premises used: Ne.symm, ne_of_mem_of_not_mem, Iff.mp, Finset.insert_erase, Finset.erase_ne_self
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : s ∈ 𝒜
simp_rw : s.erase a ∈ 𝒜 ∨ s.erase a ∉ 𝒜 ∧ insert a (s.erase a) ∈ 𝒜
⊢ s.erase a ∈ 𝓓 a 𝒜

Tactic:
simp_rw [mem_compression, erase_idem, and_self_iff]

Premises used: Finset.erase_idem, and_self_iff, Down.mem_compression
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : s ∈ 𝒜
⊢ s.erase a ∈ 𝒜 ∨ s.erase a ∉ 𝒜 ∧ insert a (s.erase a) ∈ 𝒜

Tactic:
(em _).imp_right fun h => ⟨h, ?_⟩

Premises used: em, And.intro, Or.imp_right
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : s ∈ 𝒜
refine : ∀ (h : s.erase a ∉ 𝒜), insert a (s.erase a) ∈ 𝒜
⊢ s.erase a ∈ 𝒜 ∨ s.erase a ∉ 𝒜 ∧ insert a (s.erase a) ∈ 𝒜

Tactic:
refine (em _).imp_right fun h => ⟨h, ?_⟩

Premises used: em, Or.imp_right
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : s ∈ 𝒜
h : s.erase a ∉ 𝒜
rwa rwa₁ rwa₂ rwa₃ : s ∈ 𝒜
⊢ insert a (s.erase a) ∈ 𝒜

Tactic:
rwa [insert_erase (erase_ne_self.1 (ne_of_mem_of_not_mem hs h).symm)]

Premises used: Ne.symm, ne_of_mem_of_not_mem, Iff.mp, Finset.insert_erase, Finset.erase_ne_self
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
simp_rw :
  s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s ∉ 𝒜 ∧ insert a s ∈ 𝒜 →
    s.erase a ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s.erase a ∉ 𝒜 ∧ insert a (s.erase a) ∈ 𝒜
⊢ s ∈ 𝓓 a 𝒜 → s.erase a ∈ 𝓓 a 𝒜

Tactic:
simp_rw [mem_compression, erase_idem]

Premises used: Finset.erase_idem, Down.mem_compression
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s ∉ 𝒜 ∧ insert a s ∈ 𝒜 →
    s.erase a ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s.erase a ∉ 𝒜 ∧ insert a (s.erase a) ∈ 𝒜

Tactic:
Or.imp (fun h => ⟨h.2, h.2⟩) fun h => ?_

Premises used: And.right, And.intro, Or.imp
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
refine : ∀ (h : s ∉ 𝒜 ∧ insert a s ∈ 𝒜), s.erase a ∉ 𝒜 ∧ insert a (s.erase a) ∈ 𝒜
⊢ s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s ∉ 𝒜 ∧ insert a s ∈ 𝒜 →
    s.erase a ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s.erase a ∉ 𝒜 ∧ insert a (s.erase a) ∈ 𝒜

Tactic:
refine Or.imp (fun h => ⟨h.2, h.2⟩) fun h => ?_

Premises used: Or.imp
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h rwa rwa₁ rwa₂ rwa₃ : s ∉ 𝒜 ∧ insert a s ∈ 𝒜
⊢ s.erase a ∉ 𝒜 ∧ insert a (s.erase a) ∈ 𝒜

Tactic:
rwa [erase_eq_of_notMem (insert_ne_self.1 <| ne_of_mem_of_not_mem h.2 h.1)]

Premises used: ne_of_mem_of_not_mem, Finset.insert_ne_self, And.right, And.left, Iff.mp, Finset.erase_eq_of_notMem
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝓓 a 𝒜
pos : ∀ (ha : a ∈ s), s ∈ 𝓓 a 𝒜
neg : ∀ (ha : a ∉ s), s ∈ 𝓓 a 𝒜
⊢ s ∈ 𝓓 a 𝒜

Tactic:
by_cases ha : a ∈ s
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝓓 a 𝒜
ha : a ∈ s
pos pos₁ pos₂ pos₃ : ∀ (h : s ∈ 𝓓 a 𝒜) (ha : a ∈ s), s ∈ 𝓓 a 𝒜
⊢ s ∈ 𝓓 a 𝒜

Tactic:
rwa [insert_eq_of_mem ha] at h

Premises used: Finset.insert_eq_of_mem
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝓓 a 𝒜
ha : a ∉ s
neg : (insert a s).erase a ∈ 𝓓 a 𝒜
⊢ s ∈ 𝓓 a 𝒜

Tactic:
rw [← erase_insert ha]

Premises used: Finset.erase_insert
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝓓 a 𝒜
ha : a ∉ s
⊢ (insert a s).erase a ∈ 𝓓 a 𝒜

Tactic:
erase_mem_compression_of_mem_compression h

Premises used: Down.erase_mem_compression_of_mem_compression
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝓓 a 𝒜
ha : a ∉ s
⊢ (insert a s).erase a ∈ 𝓓 a 𝒜

Tactic:
exact erase_mem_compression_of_mem_compression h

Premises used: Down.erase_mem_compression_of_mem_compression
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
h : ∀ (s : Finset α), s ∈ 𝓓 a (𝓓 a 𝒜) ↔ s ∈ 𝓓 a 𝒜
⊢ 𝓓 a (𝓓 a 𝒜) = 𝓓 a 𝒜

Tactic:
ext s
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ 𝓓 a (𝓓 a 𝒜) ↔ s ∈ 𝓓 a 𝒜

Tactic:
mem_compression.trans ⟨?_, fun h => Or.inl ⟨h, erase_mem_compression_of_mem_compression h⟩⟩

Premises used: And.intro, Iff.intro, Iff.trans, Or.inl, Down.erase_mem_compression_of_mem_compression, Down.mem_compression
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
h : s ∈ 𝓓 a 𝒜 ∧ s.erase a ∈ 𝓓 a 𝒜 ∨ s ∉ 𝓓 a 𝒜 ∧ insert a s ∈ 𝓓 a 𝒜 → s ∈ 𝓓 a 𝒜
⊢ s ∈ 𝓓 a (𝓓 a 𝒜) ↔ s ∈ 𝓓 a 𝒜

Tactic:
refine mem_compression.trans ⟨?_, fun h => Or.inl ⟨h, erase_mem_compression_of_mem_compression h⟩⟩

Premises used: And.intro, Iff.intro, Iff.trans, Or.inl, Down.erase_mem_compression_of_mem_compression, Down.mem_compression
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
h : s ∈ 𝓓 a 𝒜 ∧ s.erase a ∈ 𝓓 a 𝒜
⊢ s ∈ 𝓓 a 𝒜

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
h : s ∈ 𝓓 a 𝒜 ∧ s.erase a ∈ 𝓓 a 𝒜
⊢ s ∈ 𝓓 a 𝒜

Tactic:
exact h.1

Premises used: And.left
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
h : s ∉ 𝓓 a 𝒜 ∧ insert a s ∈ 𝓓 a 𝒜
⊢ s ∈ 𝓓 a 𝒜

Tactic:
cases h.1 (mem_compression_of_insert_mem_compression h.2)

Premises used: Down.mem_compression_of_insert_mem_compression, And.right, And.left
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
rw : #({s ∈ 𝒜 | s.erase a ∈ 𝒜} ∪ {a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜}) = #𝒜
rw₁ : Disjoint ({s ∈ 𝒜 | s.erase a ∈ 𝒜}) ({a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜})
rw₂ :
  ∀ (s : Finset α) (hs : s ∈ (↑({a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜}) : Set (Finset α))),
    Membership.mem (γ := Set (Finset α)) {s : Finset α | a ∈ s} s
⊢ #(𝓓 a 𝒜) = #𝒜

Tactic:
rw [compression, card_disjUnion, filter_image,
    card_image_of_injOn ((erase_injOn' _).mono fun s hs => _), ← card_union_of_disjoint]

Premises used: Finset.erase_injOn', Set.InjOn.mono, Finset.card_image_of_injOn, Down.compression, Finset.filter_image, Finset.card_disjUnion, Finset.card_union_of_disjoint
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
rw : #({s ∈ 𝒜 | s.erase a ∈ 𝒜} ∪ {a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜})
| #𝒜

Tactic:
rw [← filter_union_filter_not_eq (fun s => (erase s a ∈ 𝒜)) 𝒜]

Premises used: Membership.mem, Finset.filter_union_filter_not_eq, Finset.erase
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
conv_rhs : #({s ∈ 𝒜 | s.erase a ∈ 𝒜} ∪ {a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜}) = #𝒜
conv_rhs₁ :
  #({s ∈ 𝒜 | s.erase a ∈ 𝒜} ∪ {a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜}) = #({s ∈ 𝒜 | s.erase a ∈ 𝒜} ∪ {a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜})
⊢ #({s ∈ 𝒜 | s.erase a ∈ 𝒜} ∪ {a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜}) = #𝒜

Tactic:
conv_rhs => rw [← filter_union_filter_not_eq (fun s => (erase s a ∈ 𝒜)) 𝒜]

Premises used: Membership.mem, Finset.filter_union_filter_not_eq, Finset.erase
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ Disjoint ({s ∈ 𝒜 | s.erase a ∈ 𝒜}) ({a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜})

Tactic:
disjoint_filter_filter_not 𝒜 𝒜 (fun s => (erase s a ∈ 𝒜))

Premises used: Membership.mem, Finset.disjoint_filter_filter_not, Finset.erase
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ Disjoint ({s ∈ 𝒜 | s.erase a ∈ 𝒜}) ({a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜})

Tactic:
exact disjoint_filter_filter_not 𝒜 𝒜 (fun s => (erase s a ∈ 𝒜))

Premises used: Membership.mem, Finset.disjoint_filter_filter_not, Finset.erase
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ (↑({a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜}) : Set (Finset α))
⊢ s ∈ 𝒜 ∧ s.erase a ∉ 𝒜

Tactic:
rw [mem_coe, mem_filter] at hs

Premises used: Finset.mem_filter, Finset.mem_coe
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜 ∧ s.erase a ∉ 𝒜
⊢ Membership.mem (γ := Set (Finset α)) {s : Finset α | a ∈ s} s

Tactic:
not_imp_comm.1 erase_eq_of_notMem (ne_of_mem_of_not_mem hs.1 hs.2).symm

Premises used: Set.Mem, not_imp_comm, setOf, Ne.symm, ne_of_mem_of_not_mem, Multiset.Mem, And.right, And.left, Iff.mp, Finset.erase_eq_of_notMem
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜 ∧ s.erase a ∉ 𝒜
⊢ Membership.mem (γ := Set (Finset α)) {s : Finset α | a ∈ s} s

Tactic:
exact not_imp_comm.1 erase_eq_of_notMem (ne_of_mem_of_not_mem hs.1 hs.2).symm

Premises used: not_imp_comm, Ne.symm, ne_of_mem_of_not_mem, And.right, And.left, Iff.mp, Finset.erase_eq_of_notMem
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
u v a : α
ha : Membership.mem (γ := Set α) {x : α | Disjoint u x ∧ v ≤ x} a
b : α
hb : Membership.mem (γ := Set α) {x : α | Disjoint u x ∧ v ≤ x} b
hab : (a ⊔ u) \ v = (b ⊔ u) \ v
rw rw₁ : ((b ⊔ u) \ v) \ u ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v
⊢ ((a ⊔ u) \ v) \ u ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v

Tactic:
rw [hab]
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
u v a : α
ha : Membership.mem (γ := Set α) {x : α | Disjoint u x ∧ v ≤ x} a
b : α
hb : Membership.mem (γ := Set α) {x : α | Disjoint u x ∧ v ≤ x} b
hab : Eq.{u_1 + 1} (α := α) ((fun (x : α) ↦ (x ⊔ u) \ v) a) ((fun (x : α) ↦ (x ⊔ u) \ v) b)
⊢ ((a ⊔ u) \ v) \ u ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v

Tactic:
have h : ((a ⊔ u) \ v) \ u ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v := by
    dsimp at hab
    rw [hab]
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
u v a : α
ha : Membership.mem (γ := Set α) {x : α | Disjoint u x ∧ v ≤ x} a
b : α
hb : Membership.mem (γ := Set α) {x : α | Disjoint u x ∧ v ≤ x} b
hab : Eq.{u_1 + 1} (α := α) ((fun (x : α) ↦ (x ⊔ u) \ v) a) ((fun (x : α) ↦ (x ⊔ u) \ v) b)
h : ((a ⊔ u) \ v) \ u ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v
rwa : ∀ (h : ((a ⊔ u) \ u) \ v ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v), a = b
rwa₁ : ∀ (h : a \ v ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v), a = b
rwa₂ : ∀ (h : a \ v ⊔ v = ((b ⊔ u) \ u) \ v ⊔ v), a = b
rwa₃ : ∀ (h : a \ v ⊔ v = b \ v ⊔ v), a = b
rwa₄ : ∀ (h : a = b \ v ⊔ v), a = b
rwa₅ rwa₆ rwa₇ rwa₈ : ∀ (h : a = b), a = b
⊢ a = b

Tactic:
rwa [sdiff_sdiff_comm, ha.1.symm.sup_sdiff_cancel_right, sdiff_sdiff_comm,
    hb.1.symm.sup_sdiff_cancel_right, sdiff_sup_cancel ha.2, sdiff_sup_cancel hb.2] at h

Premises used: sdiff_sup_cancel, sdiff_sdiff_comm, Disjoint.symm, And.right, And.left, Disjoint.sup_sdiff_cancel_right
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
u v a : α
hua : Disjoint u a
hva : v ≤ a
⊢ compress u v a = (a ⊔ u) \ v

Tactic:
if_pos ⟨hua, hva⟩

Premises used: if_pos, UV.compress
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
u v a : α
hva : Disjoint v a
hua : u ≤ a
rw : ((a ⊔ v) \ u ⊔ u) \ v = a
rw₁ : (a ⊔ v) \ v = a
rw₂ rw₃ : a = a
⊢ compress u v ((a ⊔ v) \ u) = a

Tactic:
rw [compress_of_disjoint_of_le disjoint_sdiff_self_right
      (le_sdiff.2 ⟨(le_sup_right : v ≤ a ⊔ v), hva.mono_right hua⟩),
    sdiff_sup_cancel (le_sup_of_le_left hua), hva.symm.sup_sdiff_cancel_right]

Premises used: sdiff_sup_cancel, Iff.mpr, disjoint_sdiff_self_right, le_sup_of_le_left, le_sup_right, le_sdiff, Disjoint.symm, And.intro, UV.compress_of_disjoint_of_le, Disjoint.mono_right, Disjoint.sup_sdiff_cancel_right
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
u a : α
pos : ∀ (h : Disjoint u a ∧ u ≤ a), (a ⊔ u) \ u = a
neg : ∀ (h : ¬(Disjoint u a ∧ u ≤ a)), a = a
⊢ (if Disjoint u a ∧ u ≤ a then (a ⊔ u) \ u else a) = a

Tactic:
split_ifs with h
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
u a : α
h : Disjoint u a ∧ u ≤ a
⊢ (a ⊔ u) \ u = a

Tactic:
h.1.symm.sup_sdiff_cancel_right

Premises used: Disjoint.symm, And.left, Disjoint.sup_sdiff_cancel_right
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
u a : α
h : Disjoint u a ∧ u ≤ a
⊢ (a ⊔ u) \ u = a

Tactic:
exact h.1.symm.sup_sdiff_cancel_right

Premises used: Disjoint.symm, And.left, Disjoint.sup_sdiff_cancel_right
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
u a : α
h : ¬(Disjoint u a ∧ u ≤ a)
⊢ a = a

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
a b : α
⊢ compress (a \ b) (b \ a) b = a

Tactic:
(compress_of_disjoint_of_le disjoint_sdiff_self_left sdiff_le).trans ?_

Premises used: sdiff_le, UV.compress_of_disjoint_of_le, disjoint_sdiff_self_left, Eq.trans
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
a b : α
refine : (b ⊔ a \ b) \ (b \ a) = a
⊢ compress (a \ b) (b \ a) b = a

Tactic:
refine (compress_of_disjoint_of_le disjoint_sdiff_self_left sdiff_le).trans ?_

Premises used: sdiff_le, UV.compress_of_disjoint_of_le, disjoint_sdiff_self_left, Eq.trans
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
a b : α
rw : b \ (b \ a) ≤ a
⊢ (b ⊔ a \ b) \ (b \ a) = a

Tactic:
rw [sup_sdiff_self_right, sup_sdiff, disjoint_sdiff_self_right.sdiff_eq_left, sup_eq_right]

Premises used: disjoint_sdiff_self_right, Disjoint.sdiff_eq_left, sup_eq_right, sup_sdiff, sup_sdiff_self_right
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
a b : α
⊢ b \ (b \ a) ≤ a

Tactic:
sdiff_sdiff_le

Premises used: sdiff_sdiff_le
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
a b : α
⊢ b \ (b \ a) ≤ a

Tactic:
exact sdiff_sdiff_le

Premises used: sdiff_sdiff_le
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
u v a : α
unfold :
  (if
        Disjoint u (if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a) ∧
          v ≤ if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a then
      ((if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a) ⊔ u) \ v
    else if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a) =
    if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a
⊢ compress u v (compress u v a) = compress u v a

Tactic:
unfold compress

Premises used: UV.compress
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
u v a : α
pos :
  ∀ (h : Disjoint u a ∧ v ≤ a) (h' : Disjoint u ((a ⊔ u) \ v) ∧ v ≤ (a ⊔ u) \ v), ((a ⊔ u) \ v ⊔ u) \ v = (a ⊔ u) \ v
neg : ∀ (h : Disjoint u a ∧ v ≤ a) (h' : ¬(Disjoint u ((a ⊔ u) \ v) ∧ v ≤ (a ⊔ u) \ v)), (a ⊔ u) \ v = (a ⊔ u) \ v
neg₁ : ∀ (h : ¬(Disjoint u a ∧ v ≤ a)), a = a
⊢ (if
        Disjoint u (if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a) ∧
          v ≤ if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a then
      ((if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a) ⊔ u) \ v
    else if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a) =
    if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a

Tactic:
split_ifs with h h'
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
u v a : α
h : Disjoint u a ∧ v ≤ a
h' : Disjoint u ((a ⊔ u) \ v) ∧ v ≤ (a ⊔ u) \ v
pos : ((a ⊔ u) \ ⊥ ⊔ u) \ ⊥ = (a ⊔ u) \ ⊥
pos₁ : (a ⊔ u) \ ⊥ ⊔ u = (a ⊔ u) \ ⊥
pos₂ : a ⊔ u ⊔ u = a ⊔ u
pos₃ : a ⊔ (u ⊔ u) = a ⊔ u
pos₄ pos₅ : a ⊔ u = a ⊔ u
⊢ ((a ⊔ u) \ v ⊔ u) \ v = (a ⊔ u) \ v

Tactic:
rw [le_sdiff_right.1 h'.2, sdiff_bot, sdiff_bot, sup_assoc, sup_idem]

Premises used: le_sdiff_right, sup_idem, sup_assoc, And.right, Iff.mp, sdiff_bot
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
u v a : α
h : Disjoint u a ∧ v ≤ a
h' : ¬(Disjoint u ((a ⊔ u) \ v) ∧ v ≤ (a ⊔ u) \ v)
⊢ (a ⊔ u) \ v = (a ⊔ u) \ v

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
u v a : α
h : ¬(Disjoint u a ∧ v ≤ a)
⊢ a = a

Tactic:
rfl
-- 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 : α
ha : a ∈ (↑({a ∈ s | compress u v a ∉ s}) : Set α)
b : α
hb : b ∈ (↑({a ∈ s | compress u v a ∉ s}) : Set α)
hab : compress u v a = compress u v b
rw :
  ∀ (ha : a ∈ s ∧ compress u v a ∉ s) ⦃b : α⦄ (hb : b ∈ s ∧ compress u v b ∉ s) (hab : compress u v a = compress u v b),
    a = b
⊢ a = b

Tactic:
rw [mem_coe, mem_filter] at ha hb

Premises used: Finset.mem_filter, Finset.mem_coe
-- 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 : α
ha : a ∈ s ∧ compress u v a ∉ s
b : α
hb : b ∈ s ∧ compress u v b ∉ s
hab : compress u v a = compress u v b
rw :
  ∀ (ha : a ∈ s ∧ (if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a) ∉ s) ⦃b : α⦄ (hb : b ∈ s ∧ compress u v b ∉ s)
    (hab : (if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a) = compress u v b), a = b
⊢ a = b

Tactic:
rw [compress] at ha 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 : α
ha : a ∈ s ∧ (if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a) ∉ s
b : α
hb : b ∈ s ∧ compress u v b ∉ s
hab : (if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a) = compress u v b
pos : ∀ (has : Disjoint u a ∧ v ≤ a) (ha : a ∈ s ∧ (a ⊔ u) \ v ∉ s) (hab : (a ⊔ u) \ v = compress u v b), a = b
neg : ∀ (has : ¬(Disjoint u a ∧ v ≤ a)) (ha : a ∈ s ∧ a ∉ s) (hab : a = compress u v b), a = b
⊢ a = b

Tactic:
split_ifs at ha hab with has