awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ (a ⊔ v) \ u ∈ s
have pos : ((b ⊔ u) \ v ⊔ 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]
-- 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
pos : ((b ⊔ u) \ v ⊔ v) \ u ∈ s
⊢ (a ⊔ v) \ u ∈ s
have pos₁ : (b ⊔ u) \ 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]
-- 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
pos : ((b ⊔ u) \ v ⊔ v) \ u ∈ s
pos₁ : (b ⊔ u) \ u ∈ s
⊢ (a ⊔ v) \ u ∈ s
have pos₂ : b \ 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]
-- 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 α
ha : a ∈ 𝓒 u v s
hva : v ≤ a
hua : Disjoint u a
⊢ (a ⊔ u) \ v ∈ s
have ha₁ : 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
Cleared hypotheses: ha, hva, hua
-- 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 ∧ (a ⊔ u) \ v ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
hva : v ≤ a
hua : Disjoint u a
⊢ (a ⊔ u) \ v ∈ s
have inl : a ∈ s → ∀ (ha : (a ⊔ u) \ v ∈ s), (a ⊔ u) \ v ∈ s
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 ∧ (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
⊢ (a ⊔ u) \ v ∈ s
have 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
Tactic: obtain ⟨_, ha⟩ | ⟨_, b, hb, rfl⟩ := ha
Cleared hypotheses: a, ha, hva, hua
-- 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 α
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)
⊢ u = ⊥
have rwa : ∀ (this : Disjoint u u), u = ⊥
Tactic: rwa [(hua.mono_right hva).sdiff_eq_left, disjoint_self] at this
Cleared hypotheses: this
-- 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 α
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 = ⊥
⊢ u = ⊥
have rwa₁ : ∀ (this : u = ⊥), u = ⊥
Tactic: rwa [(hua.mono_right hva).sdiff_eq_left, disjoint_self] at this
Cleared hypotheses: this
-- 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 α
b : α
hb : b ∈ s
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left : compress u v b ∉ s
⊢ u = ⊥
have suffices : Disjoint u (u \ v)
Tactic: suffices Disjoint u (u \ v) by rwa [(hua.mono_right hva).sdiff_eq_left, disjoint_self] at this
-- 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 α
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)
have refine : u \ v ≤ compress u v b
Tactic: refine hua.mono_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 α
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
have rw : u \ v ≤ (compress u v b ⊔ u) \ v
Tactic: rw [← compress_idem, compress_of_disjoint_of_le hua hva]
-- 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 α
b : α
hb : b ∈ s
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left : compress u v b ∉ s
⊢ (compress u v b ⊔ u) \ v ∈ s
have hu : 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
-- 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 α
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 = ⊥
have rw : Disjoint v v
Tactic: rw [← disjoint_self]
-- 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 α
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 v
have apply : Disjoint v (compress u v b)
Tactic: apply Disjoint.mono_right hva
-- 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 α
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)
have rw : Disjoint v ((compress u v b ⊔ u) \ v)
Tactic: rw [← compress_idem, compress_of_disjoint_of_le hua hva]
-- 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 α
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 = ⊥
⊢ (compress u v b ⊔ u) \ v ∈ s
have hv : 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
-- 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 α
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 = ⊥
⊢ (compress u v b ⊔ u) \ v ∈ s
have inr : (compress ⊥ v b ⊔ ⊥) \ v ∈ s
Tactic: rwa [hu, hv, compress_self, sup_bot_eq, sdiff_bot]
-- 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 α
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
⊢ (compress u v b ⊔ u) \ v ∈ s
have inr₁ : (compress ⊥ ⊥ b ⊔ ⊥) \ ⊥ ∈ s
Tactic: rwa [hu, hv, compress_self, sup_bot_eq, sdiff_bot]
-- 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 α
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
⊢ (compress u v b ⊔ u) \ v ∈ s
have inr₂ : (b ⊔ ⊥) \ ⊥ ∈ s
Tactic: rwa [hu, hv, compress_self, sup_bot_eq, sdiff_bot]
-- 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 α
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
⊢ (compress u v b ⊔ u) \ v ∈ s
have inr₃ : b \ ⊥ ∈ s
Tactic: rwa [hu, hv, compress_self, sup_bot_eq, sdiff_bot]
-- 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 α
ha : a ∈ 𝓒 u v s
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
⊢ a ∈ s
have ha₁ : a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
Tactic: rw [mem_compression] at ha
Cleared hypotheses: ha, hva, hvu
-- 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
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
⊢ a ∈ s
have inl : ∀ (ha : a ∈ s ∧ compress u v a ∈ s), a ∈ s
Tactic: obtain ha | ⟨_, b, hb, h⟩ := 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
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
inl : ∀ (ha : a ∈ s ∧ compress u v a ∈ s), a ∈ s
⊢ a ∈ s
have inr : a ∉ s → ∀ (b : α) (hb : b ∈ s) (h : compress u v b = a), a ∈ s
Tactic: obtain ha | ⟨_, b, hb, h⟩ := 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 α
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
⊢ a ∈ s
have pos : Disjoint u b ∧ v ≤ b → ∀ (h : (b ⊔ u) \ v = a), a ∈ s
Tactic: split_ifs 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 α
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
⊢ a ∈ s
have neg : ¬(Disjoint u b ∧ v ≤ b) → ∀ (h : b = a), a ∈ s
Tactic: split_ifs at h
Cleared hypotheses: h
-- 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 α
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
⊢ a ∈ s
have hva₁ : v = ⊥
Tactic: rw [← h, le_sdiff_right] at hva
Cleared hypotheses: hva, hb, h_1, 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 α
hvu : v = ⊥ → u = ⊥
left : a ∉ s
b : α
hva : v = ⊥
hb : b ∈ s
h_1 : Disjoint u b ∧ v ≤ b
h : (b ⊔ u) \ v = a
⊢ a ∈ s
have pos : (b ⊔ u) \ v ∈ s
Tactic: rwa [← h, hvu hva, hva, sup_bot_eq, sdiff_bot]
-- 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 α
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
⊢ a ∈ s
have pos₁ : (b ⊔ ⊥) \ v ∈ s
Tactic: rwa [← h, hvu hva, hva, sup_bot_eq, sdiff_bot]
-- 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 α
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
⊢ a ∈ s
have pos₂ : (b ⊔ ⊥) \ ⊥ ∈ s
Tactic: rwa [← h, hvu hva, hva, sup_bot_eq, sdiff_bot]
-- 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 α
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
⊢ a ∈ s
have pos₃ : b \ ⊥ ∈ s
Tactic: rwa [← h, hvu hva, hva, sup_bot_eq, sdiff_bot]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
Goal:
α : Type u_1
inst : DecidableEq α
u v : Finset α
huv : #u = #v
a : Finset α
⊢ #(if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a) = #a
have pos : ∀ (h : Disjoint u a ∧ v ≤ a), #((a ⊔ u) \ v) = #a
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ #(if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a) = #a
have neg : ∀ (h : ¬(Disjoint u a ∧ v ≤ a)), #a = #a
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
Goal:
α : Type u_1
inst : DecidableEq α
u v : Finset α
huv : #u = #v
a : Finset α
h : Disjoint u a ∧ v ≤ a
⊢ #((a ⊔ u) \ v) = #a
have pos : #(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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ #((a ⊔ u) \ v) = #a
have pos₁ : #(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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ #((a ⊔ u) \ v) = #a
have pos₂ : #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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ #((a ⊔ u) \ v) = #a
have pos₃ : #a + #v - #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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ #((a ⊔ u) \ v) = #a
have pos₄ : #a = #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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
r : ℕ
huv : #u = #v
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
⊢ Set.Sized r (↑(𝓒 u v 𝒜) : Set (Finset α))
have simp_rw : ∀ ⦃x : Finset α⦄, (x ∈ 𝒜 ∧ compress u v x ∈ 𝒜 ∨ x ∉ 𝒜 ∧ ∃ b ∈ 𝒜, compress u v b = x) → #x = r
Tactic: simp_rw [Set.Sized, mem_coe, mem_compression]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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 ∉ 𝒜
⊢ #(compress u v t) = r
have inr : #t = r
Tactic: rw [card_compress huv, h𝒜 ht]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ #(compress u v t) = r
have inr₁ : r = r
Tactic: rw [card_compress huv, h𝒜 ht]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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 ∈ ∂ 𝒜'
⊢ s ∈ 𝓒 u v (∂ 𝒜)
have rw : s ∈ ∂ 𝒜 ∧ compress u v s ∈ ∂ 𝒜 ∨ s ∉ ∂ 𝒜 ∧ ∃ b ∈ ∂ 𝒜, compress u v b = s
Tactic: rw [mem_compression]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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 ∈ ∂ 𝒜'
⊢ s ∈ ∂ 𝒜 ∧ compress u v s ∈ ∂ 𝒜 ∨ s ∉ ∂ 𝒜 ∧ ∃ b ∈ ∂ 𝒜, compress u v b = s
have pos : ∀ (hs : s ∈ ∂ 𝒜), s ∈ ∂ 𝒜 ∧ compress u v s ∈ ∂ 𝒜 ∨ s ∉ ∂ 𝒜 ∧ ∃ b ∈ ∂ 𝒜, compress u v b = s
Tactic: by_cases hs : s ∈ 𝒜.shadow
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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
⊢ s ∈ ∂ 𝒜 ∧ compress u v s ∈ ∂ 𝒜 ∨ s ∉ ∂ 𝒜 ∧ ∃ b ∈ ∂ 𝒜, compress u v b = s
have neg : ∀ (hs : s ∉ ∂ 𝒜), s ∈ ∂ 𝒜 ∧ compress u v s ∈ ∂ 𝒜 ∨ s ∉ ∂ 𝒜 ∧ ∃ b ∈ ∂ 𝒜, compress u v b = s
Tactic: by_cases hs : s ∈ 𝒜.shadow
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (hypothesis)
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 ∉ ∂ 𝒜
⊢ s ∈ ∂ 𝒜 ∧ compress u v s ∈ ∂ 𝒜 ∨ s ∉ ∂ 𝒜 ∧ ∃ b ∈ ∂ 𝒜, compress u v b = s
have hus : u ⊆ s
Tactic: obtain ⟨hus, hvs, h, _⟩ := H _ hs' hs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (hypothesis)
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
⊢ s ∈ ∂ 𝒜 ∧ compress u v s ∈ ∂ 𝒜 ∨ s ∉ ∂ 𝒜 ∧ ∃ b ∈ ∂ 𝒜, compress u v b = s
have hvs : Disjoint v s
Tactic: obtain ⟨hus, hvs, h, _⟩ := H _ hs' hs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (hypothesis)
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 ∈ ∂ 𝒜 ∧ compress u v s ∈ ∂ 𝒜 ∨ s ∉ ∂ 𝒜 ∧ ∃ b ∈ ∂ 𝒜, compress u v b = s
have h : (s ∪ v) \ u ∈ ∂ 𝒜
Tactic: obtain ⟨hus, hvs, h, _⟩ := H _ hs' hs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (hypothesis)
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
h : (s ∪ v) \ u ∈ ∂ 𝒜
⊢ s ∈ ∂ 𝒜 ∧ compress u v s ∈ ∂ 𝒜 ∨ s ∉ ∂ 𝒜 ∧ ∃ b ∈ ∂ 𝒜, compress u v b = s
have right : (s ∪ v) \ u ∉ ∂ 𝒜'
Tactic: obtain ⟨hus, hvs, h, _⟩ := H _ hs' hs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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 ∈ ∂ 𝒜
⊢ s ∈ ∂ 𝒜 ∧ compress u v s ∈ ∂ 𝒜 ∨ s ∉ ∂ 𝒜 ∧ ∃ b ∈ ∂ 𝒜, compress u v b = s
have pos : compress u v s ∈ ∂ 𝒜
Tactic: refine Or.inl ⟨hs, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Compression.UV (goal)
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 ∈ ∂ 𝒜
⊢ (if Disjoint u s ∧ v ≤ s then (s ⊔ u) \ v else s) ∈ ∂ 𝒜
have pos : ∀ (huvs : Disjoint u s ∧ v ≤ s), (s ⊔ u) \ v ∈ ∂ 𝒜
Tactic: split_ifs with huvs