-- Mathlib/Combinatorics/SetFamily/Compression/UV.lean
theorem compression_self (u : α) (s : Finset α) : 𝓒 u u s = s

Proof state:
case h.e'_2.h.e'_4
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : DecidableEq α
u : α
s : Finset α
⊢ filter (fun a => a ∉ s) (image (compress u u) s) = ∅

Tactic:
refine eq_empty_of_forall_not_mem fun a ha ↦ ?_

Result:
case h.e'_2.h.e'_4
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : DecidableEq α
u : α
s : Finset α
a : α
ha : a ∈ filter (fun a => a ∉ s) (image (compress u u) s)
⊢ False

Proof state:
case h.e'_2.h.e'_4
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : DecidableEq α
u : α
s : Finset α
a : α
ha : (∃ a_1 ∈ s, a_1 = a) ∧ a ∉ s
⊢ False

Tactic:
obtain ⟨⟨b, hb, rfl⟩, hb'⟩ := ha

Result:
case h.e'_2.h.e'_4.intro.intro.intro
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : DecidableEq α
u : α
s : Finset α
b : α
hb : b ∈ s
hb' : b ∉ s
⊢ False

Proof state:
case h.e'_2.h.e'_3
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : DecidableEq α
u : α
s : Finset α
⊢ filter (fun a => compress u u a ∈ s) s = s

Tactic:
ext a

Result:
case h.e'_2.h.e'_3.h
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : DecidableEq α
u : α
s : Finset α
a : α
⊢ a ∈ filter (fun a => compress u u a ∈ s) s ↔ a ∈ s

Proof state:
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : DecidableEq α
u : α
s : Finset α
⊢ filter (fun a => compress u u a ∈ s) s ∪ filter (fun a => a ∉ s) (image (compress u u) s) = s

Tactic:
convert union_empty s

Result:
case h.e'_2.h.e'_3
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : DecidableEq α
u : α
s : Finset α
⊢ filter (fun a => compress u u a ∈ s) s = s

case h.e'_2.h.e'_4
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : DecidableEq α
u : α
s : Finset α
⊢ filter (fun a => a ∉ s) (image (compress u u) s) = ∅

Proof state:
case h.e'_2.h.e'_4.intro.intro.intro
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : DecidableEq α
u : α
s : Finset α
b : α
hb : b ∈ s
hb' : b ∉ s
⊢ False

Tactic:
exact hb' hb

Result:
no goals

Proof state:
case h.e'_2.h.e'_4
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : DecidableEq α
u : α
s : Finset α
a : α
ha : a ∈ filter (fun a => a ∉ s) (image (compress u u) s)
⊢ False

Tactic:
simp_rw [mem_filter, mem_image, compress_self] at ha

Result:
case h.e'_2.h.e'_4
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : DecidableEq α
u : α
s : Finset α
a : α
ha : (∃ a_1 ∈ s, a_1 = a) ∧ a ∉ s
⊢ False

Proof state:
case h.e'_2.h.e'_3.h
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : DecidableEq α
u : α
s : Finset α
a : α
⊢ a ∈ filter (fun a => compress u u a ∈ s) s ↔ a ∈ s

Tactic:
rw [mem_filter, compress_self, and_self_iff]

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : DecidableEq α
u : α
s : Finset α
⊢ 𝓒 u u s = s

Tactic:
unfold compression

Result:
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : DecidableEq α
u : α
s : Finset α
⊢ filter (fun a => compress u u a ∈ s) s ∪ filter (fun a => a ∉ s) (image (compress u u) s) = s