awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (hypothesis)
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
⊢ a = b
have hb₁ : b ∈ s ∧ (if Disjoint u b ∧ v ≤ b then (b ⊔ u) \ v else b) ∉ s
Tactic: rw [compress] at hb hab
Cleared hypotheses: hb, has, ha, hab
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (hypothesis)
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 = b
have hab₁ : (a ⊔ u) \ v = if Disjoint u b ∧ v ≤ b then (b ⊔ u) \ v else b
Tactic: rw [compress] at hb hab
Cleared hypotheses: hb, has, 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 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
⊢ a = b
have pos : ∀ (hbs : Disjoint u b ∧ v ≤ b) (hb : b ∈ s ∧ (b ⊔ u) \ v ∉ s) (hab : (a ⊔ u) \ v = (b ⊔ u) \ v), a = b
Tactic: split_ifs at hb hab with hbs
Cleared hypotheses: 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 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
⊢ a = b
have neg : ∀ (hbs : ¬(Disjoint u b ∧ v ≤ b)) (hb : b ∈ s ∧ b ∉ s) (hab : (a ⊔ u) \ v = b), a = b
Tactic: split_ifs at hb hab with hbs
Cleared hypotheses: 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 a : α
inst_3 : DecidableEq α
⊢ a ∈ 𝓒 u v s ↔ a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
have 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
Tactic: simp_rw [compression, mem_union, mem_filter, mem_image, and_comm]
-- 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 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
⊢ a ∈ 𝓒 u v s ↔ a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
have 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
Tactic: simp_rw [compression, mem_union, mem_filter, mem_image, and_comm]
-- 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 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
⊢ a ∈ 𝓒 u v s ↔ a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
have 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
Tactic: simp_rw [compression, mem_union, mem_filter, mem_image, and_comm]
-- 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 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
⊢ a ∈ 𝓒 u v s ↔ a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
have 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
Tactic: simp_rw [compression, mem_union, mem_filter, mem_image, and_comm]
-- 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 a : α
inst_3 : DecidableEq α
ha : a ∈ s
⊢ compress u v a ∈ 𝓒 u v s
have 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
Tactic: rw [mem_compression]
-- 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 a : α
inst_3 : DecidableEq α
ha : 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
have 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
Tactic: by_cases h : compress u v a ∈ s
-- 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 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
⊢ 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
have 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
Tactic: by_cases h : compress u v a ∈ s
-- 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 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
have 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
Tactic: rw [compress_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 a : α
inst_3 : DecidableEq α
ha : a ∈ 𝓒 u v s
⊢ compress u v a ∈ 𝓒 u v s
have 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
Tactic: rw [mem_compression] at ha ⊢
Cleared hypotheses: ha
-- 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 a : α
inst_3 : DecidableEq α
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
have 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
Tactic: simp only [compress_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 a : α
inst_3 : DecidableEq α
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 a ∈ s ∨ compress u v a ∉ s ∧ ∃ b ∈ s, compress u v b = compress u v a
have 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
Tactic: obtain ⟨_, ha⟩ | ⟨_, b, hb, rfl⟩ := ha
Cleared hypotheses: ha
-- 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 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
⊢ 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
have 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)
Tactic: obtain ⟨_, ha⟩ | ⟨_, b, hb, rfl⟩ := ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (hypothesis)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableRel (α := α) Disjoint
inst_2 : DecidableLE α
inst_3 : DecidableEq α
u v : α
s : Finset α
⊢ 𝓒 u v (𝓒 u v s) = 𝓒 u v s
have h : {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
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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} = ∅
⊢ 𝓒 u v (𝓒 u v s) = 𝓒 u v s
have 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
Tactic: rw [compression, filter_image, h, image_empty, ← 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 α
inst_3 : DecidableEq α
u v : α
s : Finset α
⊢ #(𝓒 u v s) = #s
have rw : #({a ∈ s | compress u v a ∈ s} ∪ {a ∈ image (compress u v) s | a ∉ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ #(𝓒 u v s) = #s
have rw₁ : #({a ∈ s | compress u v a ∈ s}) + #({a ∈ image (compress u v) s | a ∉ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ #(𝓒 u v s) = #s
have rw₂ : #({a ∈ s | compress u v a ∈ s}) + #(image (compress u v) ({a ∈ s | compress u v a ∉ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ #(𝓒 u v s) = #s
have rw₃ : #({a ∈ s | compress u v a ∈ s}) + #({a ∈ s | compress u v a ∉ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ #(𝓒 u v s) = #s
have rw₄ : #({a ∈ s | compress u v a ∈ s} ∪ {a ∈ s | compress u v a ∉ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ #(𝓒 u v s) = #s
have rw₅ : #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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (hypothesis)
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
⊢ u ≤ a
have h₁ : a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
Tactic: rw [mem_compression] at h
Cleared hypotheses: h, ha
-- 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 a : α
inst_3 : DecidableEq α
h : a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
ha : a ∉ s
⊢ u ≤ a
have inl : ∀ (h : a ∈ s ∧ compress u v a ∈ s), u ≤ a
Tactic: obtain h | ⟨-, b, hb, hba⟩ := 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 α
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
⊢ u ≤ a
have inr : ∀ (b : α) (hb : b ∈ s) (hba : compress u v b = a), u ≤ a
Tactic: obtain h | ⟨-, b, hb, hba⟩ := 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 α
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
⊢ u ≤ a
have pos : ∀ (h : Disjoint u b ∧ v ≤ b) (hba : (b ⊔ u) \ v = a), u ≤ a
Tactic: split_ifs at hba with h
Cleared hypotheses: hba
-- 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 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
⊢ u ≤ a
have neg : ∀ (h : ¬(Disjoint u b ∧ v ≤ b)) (hba : b = a), u ≤ a
Tactic: split_ifs at hba with h
Cleared hypotheses: hba
-- 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 a : α
inst_3 : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
h : Disjoint u b ∧ v ≤ b
hba : (b ⊔ u) \ v = a
⊢ u ≤ a
have pos : u ≤ b ⊔ u ∧ Disjoint u v
Tactic: rw [← hba, le_sdiff]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (hypothesis)
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
⊢ Disjoint v a
have h₁ : a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
Tactic: rw [mem_compression] at h
Cleared hypotheses: h, ha
-- 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 a : α
inst_3 : DecidableEq α
h : a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
ha : a ∉ s
⊢ Disjoint v a
have inl : ∀ (h : a ∈ s ∧ compress u v a ∈ s), Disjoint v a
Tactic: obtain h | ⟨-, b, hb, hba⟩ := 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 α
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
⊢ Disjoint v a
have inr : ∀ (b : α) (hb : b ∈ s) (hba : compress u v b = a), Disjoint v a
Tactic: obtain h | ⟨-, b, hb, hba⟩ := 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 α
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
⊢ Disjoint v a
have pos : Disjoint u b ∧ v ≤ b → ∀ (hba : (b ⊔ u) \ v = a), Disjoint v a
Tactic: split_ifs at hba
Cleared hypotheses: hba
-- 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 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
⊢ Disjoint v a
have neg : ¬(Disjoint u b ∧ v ≤ b) → ∀ (hba : b = a), Disjoint v a
Tactic: split_ifs at hba
Cleared hypotheses: hba
-- 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 a : α
inst_3 : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
h : Disjoint u b ∧ v ≤ b
hba : (b ⊔ u) \ v = a
⊢ Disjoint v a
have pos : Disjoint v ((b ⊔ u) \ v)
Tactic: rw [← hba]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (hypothesis)
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 ⊔ v) \ u ∈ s
have h₁ : a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
Tactic: rw [mem_compression] at h
Cleared hypotheses: h, ha
-- 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 a : α
inst_3 : DecidableEq α
h : a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
ha : a ∉ s
⊢ (a ⊔ v) \ u ∈ s
have inl : ∀ (h : a ∈ s ∧ compress u v a ∈ s), (a ⊔ v) \ u ∈ s
Tactic: obtain h | ⟨-, b, hb, hba⟩ := 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 α
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
⊢ (a ⊔ v) \ u ∈ s
have inr : ∀ (b : α) (hb : b ∈ s) (hba : compress u v b = a), (a ⊔ v) \ u ∈ s
Tactic: obtain h | ⟨-, b, hb, hba⟩ := 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 α
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
⊢ (a ⊔ v) \ u ∈ s
have pos : ∀ (h : Disjoint u b ∧ v ≤ b) (hba : (b ⊔ u) \ v = a), (a ⊔ v) \ u ∈ s
Tactic: split_ifs at hba with h
Cleared hypotheses: hba
-- 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 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
⊢ (a ⊔ v) \ u ∈ s
have neg : ∀ (h : ¬(Disjoint u b ∧ v ≤ b)) (hba : b = a), (a ⊔ v) \ u ∈ s
Tactic: split_ifs at hba with h
Cleared hypotheses: hba