awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ 𝓓 a 𝒜 ↔ s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s ∉ 𝒜 ∧ insert a s ∈ 𝒜
have simp_rw : s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ (∃ a_1 ∈ 𝒜, a_1.erase a = s) ∧ s ∉ 𝒜 ↔ s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ insert a s ∈ 𝒜 ∧ s ∉ 𝒜
Tactic: simp_rw [compression, mem_disjUnion, mem_filter, mem_image, and_comm (a := s ∉ 𝒜)]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
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 ∉ 𝒜
have fun : ∀ (hs : s ∉ 𝒜), (∃ a_1 ∈ 𝒜, a_1.erase a = s) → insert a 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⟩⟩)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : s ∈ 𝒜
⊢ s.erase a ∈ 𝓓 a 𝒜
have simp_rw : s.erase a ∈ 𝒜 ∨ s.erase a ∉ 𝒜 ∧ insert a (s.erase a) ∈ 𝒜
Tactic: simp_rw [mem_compression, erase_idem, and_self_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : s ∈ 𝒜
⊢ s.erase a ∈ 𝒜 ∨ s.erase a ∉ 𝒜 ∧ insert a (s.erase a) ∈ 𝒜
have refine : ∀ (h : s.erase a ∉ 𝒜), insert a (s.erase a) ∈ 𝒜
Tactic: refine (em _).imp_right fun h => ⟨h, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ 𝓓 a 𝒜 → s.erase a ∈ 𝓓 a 𝒜
have simp_rw : s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s ∉ 𝒜 ∧ insert a s ∈ 𝒜 →
  s.erase a ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s.erase a ∉ 𝒜 ∧ insert a (s.erase a) ∈ 𝒜
Tactic: simp_rw [mem_compression, erase_idem]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
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) ∈ 𝒜
have refine : ∀ (h : s ∉ 𝒜 ∧ insert a s ∈ 𝒜), s.erase a ∉ 𝒜 ∧ insert a (s.erase a) ∈ 𝒜
Tactic: refine Or.imp (fun h => ⟨h.2, h.2⟩) fun h => ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝓓 a 𝒜
⊢ s ∈ 𝓓 a 𝒜
have pos : ∀ (ha : a ∈ s), s ∈ 𝓓 a 𝒜
Tactic: by_cases ha : a ∈ s
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝓓 a 𝒜
pos : ∀ (ha : a ∈ s), s ∈ 𝓓 a 𝒜
⊢ s ∈ 𝓓 a 𝒜
have neg : ∀ (ha : a ∉ s), s ∈ 𝓓 a 𝒜
Tactic: by_cases ha : a ∈ s
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝓓 a 𝒜
ha : a ∈ s
⊢ s ∈ 𝓓 a 𝒜
have pos : ∀ (h : s ∈ 𝓓 a 𝒜) (ha : a ∈ s), s ∈ 𝓓 a 𝒜
Tactic: rwa [insert_eq_of_mem ha] at h
Cleared hypotheses: h, ha
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝓓 a 𝒜
ha : a ∉ s
⊢ s ∈ 𝓓 a 𝒜
have neg : (insert a s).erase a ∈ 𝓓 a 𝒜
Tactic: rw [← erase_insert ha]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ 𝓓 a (𝓓 a 𝒜) = 𝓓 a 𝒜
have h : ∀ (s : Finset α), s ∈ 𝓓 a (𝓓 a 𝒜) ↔ s ∈ 𝓓 a 𝒜
Tactic: ext s
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ 𝓓 a (𝓓 a 𝒜) ↔ s ∈ 𝓓 a 𝒜
have h : s ∈ 𝓓 a 𝒜 ∧ s.erase a ∈ 𝓓 a 𝒜 ∨ s ∉ 𝓓 a 𝒜 ∧ insert a s ∈ 𝓓 a 𝒜 → s ∈ 𝓓 a 𝒜
Tactic: refine mem_compression.trans ⟨?_, fun h => Or.inl ⟨h, erase_mem_compression_of_mem_compression h⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ #(𝓓 a 𝒜) = #𝒜
have rw : #({s ∈ 𝒜 | s.erase a ∈ 𝒜} ∪ {a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜}) = #𝒜
Tactic: rw [compression, card_disjUnion, filter_image,
    card_image_of_injOn ((erase_injOn' _).mono fun s hs => _), ← card_union_of_disjoint]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
rw : #({s ∈ 𝒜 | s.erase a ∈ 𝒜} ∪ {a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜}) = #𝒜
⊢ #(𝓓 a 𝒜) = #𝒜
have rw₁ : Disjoint ({s ∈ 𝒜 | s.erase a ∈ 𝒜}) ({a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜})
Tactic: rw [compression, card_disjUnion, filter_image,
    card_image_of_injOn ((erase_injOn' _).mono fun s hs => _), ← card_union_of_disjoint]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
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 ∉ 𝒜})
⊢ #(𝓓 a 𝒜) = #𝒜
have rw₂ : ∀ (s : Finset α) (hs : s ∈ (↑({a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜}) : Set (Finset α))),
  Membership.mem (γ := Set (Finset α)) {s : Finset α | a ∈ s} s
Tactic: rw [compression, card_disjUnion, filter_image,
    card_image_of_injOn ((erase_injOn' _).mono fun s hs => _), ← card_union_of_disjoint]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
| #𝒜
have rw : #({s ∈ 𝒜 | s.erase a ∈ 𝒜} ∪ {a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜})
Tactic: rw [← filter_union_filter_not_eq (fun s => (erase s a ∈ 𝒜)) 𝒜]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ #({s ∈ 𝒜 | s.erase a ∈ 𝒜} ∪ {a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜}) = #𝒜
have conv_rhs : #({s ∈ 𝒜 | s.erase a ∈ 𝒜} ∪ {a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜}) = #𝒜
Tactic: conv_rhs => rw [← filter_union_filter_not_eq (fun s => (erase s a ∈ 𝒜)) 𝒜]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
conv_rhs : #({s ∈ 𝒜 | s.erase a ∈ 𝒜} ∪ {a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜}) = #𝒜
⊢ #({s ∈ 𝒜 | s.erase a ∈ 𝒜} ∪ {a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜}) = #𝒜
have conv_rhs₁ : #({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 ∈ 𝒜)) 𝒜]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.Down (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ (↑({a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜}) : Set (Finset α))
⊢ Membership.mem (γ := Set (Finset α)) {s : Finset α | a ∈ s} s
have hs₁ : s ∈ 𝒜 ∧ s.erase a ∉ 𝒜
Tactic: rw [mem_coe, mem_filter] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ ((a ⊔ u) \ v) \ u ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v
have rw : ((b ⊔ u) \ v) \ u ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v
Tactic: rw [hab]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (hypothesis)
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 = b
have h : ((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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ a = b
have rwa : ∀ (h : ((a ⊔ u) \ u) \ v ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v), 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ a = b
have rwa₁ : ∀ (h : a \ v ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v), 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ a = b
have rwa₂ : ∀ (h : a \ v ⊔ v = ((b ⊔ u) \ u) \ v ⊔ v), 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ a = b
have rwa₃ : ∀ (h : a \ v ⊔ v = b \ v ⊔ v), 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ a = b
have rwa₄ : ∀ (h : a = b \ v ⊔ v), 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ a = b
have rwa₅ : ∀ (h : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
u v a : α
hva : Disjoint v a
hua : u ≤ a
⊢ compress u v ((a ⊔ v) \ u) = a
have rw : ((a ⊔ v) \ u ⊔ u) \ v = 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ compress u v ((a ⊔ v) \ u) = a
have rw₁ : (a ⊔ v) \ v = 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ compress u v ((a ⊔ v) \ u) = a
have rw₂ : a = 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
u a : α
⊢ (if Disjoint u a ∧ u ≤ a then (a ⊔ u) \ u else a) = a
have pos : ∀ (h : Disjoint u a ∧ u ≤ a), (a ⊔ u) \ u = a
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ (if Disjoint u a ∧ u ≤ a then (a ⊔ u) \ u else a) = a
have neg : ∀ (h : ¬(Disjoint u a ∧ u ≤ a)), a = a
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
a b : α
⊢ compress (a \ b) (b \ a) b = a
have refine : (b ⊔ a \ b) \ (b \ a) = a
Tactic: refine (compress_of_disjoint_of_le disjoint_sdiff_self_left sdiff_le).trans ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
a b : α
⊢ (b ⊔ a \ b) \ (b \ a) = a
have rw : b \ (b \ a) ≤ a
Tactic: rw [sup_sdiff_self_right, sup_sdiff, disjoint_sdiff_self_right.sdiff_eq_left, sup_eq_right]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
u v a : α
⊢ compress u v (compress u v a) = compress u v a
have 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
Tactic: unfold compress
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
u v 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
have 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
Tactic: split_ifs with h h'
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ (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
have neg : ∀ (h : Disjoint u a ∧ v ≤ a) (h' : ¬(Disjoint u ((a ⊔ u) \ v) ∧ v ≤ (a ⊔ u) \ v)), (a ⊔ u) \ v = (a ⊔ u) \ v
Tactic: split_ifs with h h'
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ (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
have neg₁ : ∀ (h : ¬(Disjoint u a ∧ v ≤ a)), a = a
Tactic: split_ifs with h h'
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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 ⊔ u) \ v = (a ⊔ u) \ v
have pos : ((a ⊔ u) \ ⊥ ⊔ u) \ ⊥ = (a ⊔ u) \ ⊥
Tactic: rw [le_sdiff_right.1 h'.2, sdiff_bot, sdiff_bot, sup_assoc, sup_idem]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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) \ ⊥
⊢ ((a ⊔ u) \ v ⊔ u) \ v = (a ⊔ u) \ v
have pos₁ : (a ⊔ u) \ ⊥ ⊔ u = (a ⊔ u) \ ⊥
Tactic: rw [le_sdiff_right.1 h'.2, sdiff_bot, sdiff_bot, sup_assoc, sup_idem]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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) \ ⊥
⊢ ((a ⊔ u) \ v ⊔ u) \ v = (a ⊔ u) \ v
have pos₂ : a ⊔ u ⊔ u = a ⊔ u
Tactic: rw [le_sdiff_right.1 h'.2, sdiff_bot, sdiff_bot, sup_assoc, sup_idem]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ ((a ⊔ u) \ v ⊔ u) \ v = (a ⊔ u) \ v
have pos₃ : a ⊔ (u ⊔ u) = a ⊔ u
Tactic: rw [le_sdiff_right.1 h'.2, sdiff_bot, sdiff_bot, sup_assoc, sup_idem]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ ((a ⊔ u) \ v ⊔ u) \ v = (a ⊔ u) \ v
have pos₄ : a ⊔ u = a ⊔ u
Tactic: rw [le_sdiff_right.1 h'.2, sdiff_bot, sdiff_bot, sup_assoc, sup_idem]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ a = b
have 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
Tactic: rw [mem_coe, mem_filter] at ha hb
Cleared hypotheses: ha, b, hb, hab
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ a = b
have 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
Tactic: rw [compress] at ha hab
Cleared hypotheses: ha, b, hb, hab
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ a = b
have pos : ∀ (has : Disjoint u a ∧ v ≤ a) (ha : a ∈ s ∧ (a ⊔ u) \ v ∉ s) (hab : (a ⊔ u) \ v = compress u v b), a = b
Tactic: split_ifs at ha hab with has
Cleared hypotheses: ha, hab
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ a = b
have neg : ∀ (has : ¬(Disjoint u a ∧ v ≤ a)) (ha : a ∈ s ∧ a ∉ s) (hab : a = compress u v b), a = b
Tactic: split_ifs at ha hab with has
Cleared hypotheses: ha, hab