awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
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 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus_1 : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
this_3 : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∉ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this_4 : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∈ u
z : α
hz : z ∈ v
hxy : IsCompressed (u.erase w) (v.erase z) 𝒜
this : insert w ((s ∪ v) \ u) ∈ 𝒜
⊢ Disjoint (u.erase w) ((s ∪ v) \ u.erase w)

Tactic:
disjoint_sdiff

Premises used: Finset.disjoint_sdiff
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
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 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus_1 : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
this_3 : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∉ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this_4 : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∈ u
z : α
hz : z ∈ v
hxy : IsCompressed (u.erase w) (v.erase z) 𝒜
this : insert w ((s ∪ v) \ u) ∈ 𝒜
⊢ Disjoint (u.erase w) ((s ∪ v) \ u.erase w)

Tactic:
exact disjoint_sdiff

Premises used: Finset.disjoint_sdiff
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
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 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus_1 : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
this_3 : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∉ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this_4 : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∈ u
z : α
hz : z ∈ v
hxy : IsCompressed (u.erase w) (v.erase z) 𝒜
this : insert w ((s ∪ v) \ u) ∈ 𝒜
⊢ (insert w ((s ∪ v) \ u) ∪ u.erase w) \ v.erase z ∈ 𝒜

Tactic:
have : (insert w ((s ∪ v) \ u) ∪ erase u w) \ erase v z ∈ 𝒜 := by
      refine sup_sdiff_mem_of_mem_compression (by rwa [hxy.eq]) ((erase_subset _ _).trans ‹_›) ?_
      rw [← sdiff_erase (mem_union_left _ <| hus hwu)]
      exact disjoint_sdiff
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
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 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus_1 : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
this_3 : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∉ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this_4 : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∈ u
z : α
hz : z ∈ v
hxy : IsCompressed (u.erase w) (v.erase z) 𝒜
this_5 : insert w ((s ∪ v) \ u) ∈ 𝒜
this : (insert w ((s ∪ v) \ u) ∪ u.erase w) \ v.erase z ∈ 𝒜
⊢ (insert w ((s ∪ v) \ u) ∪ u.erase w) \ v.erase z ∈ 𝒜

Tactic:
this
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
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 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus_1 : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
this_3 : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∉ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this_4 : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∈ u
z : α
hz : z ∈ v
hxy : IsCompressed (u.erase w) (v.erase z) 𝒜
this_5 : insert w ((s ∪ v) \ u) ∈ 𝒜
this : (insert w ((s ∪ v) \ u) ∪ u.erase w) \ v.erase z ∈ 𝒜
h : insert z s = (insert w ((s ∪ v) \ u) ∪ u.erase w) \ v.erase z
⊢ insert z s ∈ 𝒜

Tactic:
convert! this using 1
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
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 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus_1 : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
this_3 : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∉ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this_4 : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∈ u
z : α
hz : z ∈ v
hxy : IsCompressed (u.erase w) (v.erase z) 𝒜
this_5 : insert w ((s ∪ v) \ u) ∈ 𝒜
this : (insert w ((s ∪ v) \ u) ∪ u.erase w) \ v.erase z ∈ 𝒜
h : insert z s = ((s ∪ v) \ u ∪ insert w (u.erase w)) \ v.erase z
h₁ : insert z s = ((s ∪ v) \ u ∪ u) \ v.erase z
h₂ : insert z s = (s ∪ v) \ v.erase z
h₃ : insert z s = insert z ((s ∪ v) \ v)
h₄ h₅ : insert z s = insert z s
⊢ insert z s = (insert w ((s ∪ v) \ u) ∪ u.erase w) \ v.erase z

Tactic:
rw [insert_union_comm, insert_erase ‹w ∈ u›,
      sdiff_union_of_subset (hus.trans subset_union_left),
      sdiff_erase (mem_union_right _ ‹z ∈ v›), union_sdiff_cancel_right hsv]

Premises used: HasSubset.Subset.trans, Finset.sdiff_erase, Finset.subset_union_left, Finset.sdiff_union_of_subset, Finset.insert_union_comm, Finset.union_sdiff_cancel_right, Finset.mem_union_right, Finset.insert_erase
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
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 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus_1 : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
this_3 : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∉ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∉ u
⊢ w ∈ s ∪ v → w ∈ u

Tactic:
rw [mem_sdiff, ← Classical.not_imp, Classical.not_not] at hwB

Premises used: Classical.not_not, Finset.mem_sdiff, Classical.not_imp
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
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 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus_1 : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
this_3 : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∉ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∉ u
hwB₁ : w ∈ s ∪ v → w ∈ u
⊢ insert w ((s ∪ v) \ u) ∈ 𝒜'

Tactic:
rw [mem_sdiff, ← Classical.not_imp, Classical.not_not] at hwB

Premises used: Classical.not_not, Finset.mem_sdiff, Classical.not_imp
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
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 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus_1 : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
this_3 : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∉ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∉ u
hwB₁ : w ∈ s ∪ v → w ∈ u
hw𝒜'₁ : insert w ((s ∪ v) \ u) ∈ 𝒜'
⊢ v ⊆ insert w ((s ∪ v) \ u)

Tactic:
rw [mem_sdiff, ← Classical.not_imp, Classical.not_not] at hwB

Premises used: Classical.not_not, Finset.mem_sdiff, Classical.not_imp
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
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 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus_1 : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
this_3 : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∉ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∉ u
hwB₁ : w ∈ s ∪ v → w ∈ u
hw𝒜'₁ : insert w ((s ∪ v) \ u) ∈ 𝒜'
this₁ : v ⊆ insert w ((s ∪ v) \ u)
⊢ w ∉ u

Tactic:
rw [mem_sdiff, ← Classical.not_imp, Classical.not_not] at hwB

Premises used: Classical.not_not, Finset.mem_sdiff, Classical.not_imp
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
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 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus_1 : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
this_3 : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∈ s ∪ v → w ∈ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∉ u
neg : insert w s ∈ 𝒜
⊢ False

Tactic:
apply m w (hwu ∘ hwB ∘ mem_union_left _)

Premises used: Function.comp, Finset.mem_union_left
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
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 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus_1 : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
this_3 : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∈ s ∪ v → w ∈ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∉ u
⊢ (insert w ((s ∪ v) \ u) ∪ u) \ v ∈ 𝒜

Tactic:
have : (insert w ((s ∪ v) \ u) ∪ u) \ v ∈ 𝒜 :=
    sup_sdiff_mem_of_mem_compression ‹insert w ((s ∪ v) \ u) ∈ 𝒜'› ‹_›
      (disjoint_insert_right.2 ⟨‹_›, disjoint_sdiff⟩)
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
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 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus_1 : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
this_3 : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∈ s ∪ v → w ∈ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this_4 : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∉ u
this : (insert w ((s ∪ v) \ u) ∪ u) \ v ∈ 𝒜
⊢ (insert w ((s ∪ v) \ u) ∪ u) \ v ∈ 𝒜

Tactic:
this
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
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 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus_1 : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
this_3 : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∈ s ∪ v → w ∈ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this_4 : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∉ u
this : (insert w ((s ∪ v) \ u) ∪ u) \ v ∈ 𝒜
h : insert w s = (insert w ((s ∪ v) \ u) ∪ u) \ v
⊢ insert w s ∈ 𝒜

Tactic:
convert! this using 1
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
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 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left : x ∉ s
right : insert x s ∈ 𝒜'
hus_1 : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this_1 : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this_2 : v \ u = v
this_3 : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∈ s ∪ v → w ∈ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this_4 : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∉ u
this : (insert w ((s ∪ v) \ u) ∪ u) \ v ∈ 𝒜
h : insert w s = insert w ((s ∪ v) \ u ∪ u) \ v
h₁ : insert w s = insert w (s ∪ v) \ v
h₂ : insert w s = insert w ((s ∪ v) \ v)
h₃ h₄ : insert w s = insert w s
⊢ insert w s = (insert w ((s ∪ v) \ u) ∪ u) \ v

Tactic:
rw [insert_union, sdiff_union_of_subset (hus.trans subset_union_left),
    insert_sdiff_of_notMem _ (hwu ∘ hwB ∘ mem_union_right _), union_sdiff_cancel_right hsv]

Premises used: Function.comp, HasSubset.Subset.trans, Finset.insert_sdiff_of_notMem, Finset.insert_union, Finset.subset_union_left, Finset.sdiff_union_of_subset, Finset.union_sdiff_cancel_right, Finset.mem_union_right
-- Module: Mathlib.Combinatorics.SetFamily.Compression.UV
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
⊢ #(∂ (𝓒 u v 𝒜)) ≤ #(∂ 𝒜)

Tactic:
(card_le_card <| shadow_compression_subset_compression_shadow _ _ huv).trans
    (card_compression _ _ _).le

Premises used: UV.shadow_compression_subset_compression_shadow, Finset.card_le_card, Eq.le, LE.le.trans, UV.card_compression
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
β : Type u_2
inst : CommSemiring β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : ExistsAddOfLE β
a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β
ha₀ : 0 ≤ a₀
ha₁ : 0 ≤ a₁
hb₀ : 0 ≤ b₀
hb₁ : 0 ≤ b₁
hc₀ : 0 ≤ c₀
hc₁ : 0 ≤ c₁
hd₀ : 0 ≤ d₀
hd₁ : 0 ≤ d₁
h₀₀ : a₀ * b₀ ≤ c₀ * d₀
h₁₀ : a₁ * b₀ ≤ c₀ * d₁
h₀₁ : a₀ * b₁ ≤ c₀ * d₁
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
⊢ (a₀ + a₁) * (b₀ + b₁) = a₀ * b₀ + (a₀ * b₁ + a₁ * b₀) + a₁ * b₁

Tactic:
ring
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
β : Type u_2
inst : CommSemiring β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : ExistsAddOfLE β
a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β
ha₀ : 0 ≤ a₀
ha₁ : 0 ≤ a₁
hb₀ : 0 ≤ b₀
hb₁ : 0 ≤ b₁
hc₀ : 0 ≤ c₀
hc₁ : 0 ≤ c₁
hd₀ : 0 ≤ d₀
hd₁ : 0 ≤ d₁
h₀₀ : a₀ * b₀ ≤ c₀ * d₀
h₁₀ : a₁ * b₀ ≤ c₀ * d₁
h₀₁ : a₀ * b₁ ≤ c₀ * d₁
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
⊢ a₀ * b₀ + (a₀ * b₁ + a₁ * b₀) + a₁ * b₁ ≤ c₀ * d₀ + (c₀ * d₁ + c₁ * d₀) + c₁ * d₁

Tactic:
add_le_add_three h₀₀ ?_ h₁₁

Premises used: add_le_add_three
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
β : Type u_2
inst : CommSemiring β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : ExistsAddOfLE β
a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β
ha₀ : 0 ≤ a₀
ha₁ : 0 ≤ a₁
hb₀ : 0 ≤ b₀
hb₁ : 0 ≤ b₁
hc₀ : 0 ≤ c₀
hc₁ : 0 ≤ c₁
hd₀ : 0 ≤ d₀
hd₁ : 0 ≤ d₁
h₀₀ : a₀ * b₀ ≤ c₀ * d₀
h₁₀ : a₁ * b₀ ≤ c₀ * d₁
h₀₁ : a₀ * b₁ ≤ c₀ * d₁
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
⊢ c₀ * d₀ + (c₀ * d₁ + c₁ * d₀) + c₁ * d₁ = (c₀ + c₁) * (d₀ + d₁)

Tactic:
ring
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
β : Type u_2
inst : CommSemiring β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : ExistsAddOfLE β
a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β
ha₀ : 0 ≤ a₀
ha₁ : 0 ≤ a₁
hb₀ : 0 ≤ b₀
hb₁ : 0 ≤ b₁
hc₀ : 0 ≤ c₀
hc₁ : 0 ≤ c₁
hd₀ : 0 ≤ d₀
hd₁ : 0 ≤ d₁
h₀₀ : a₀ * b₀ ≤ c₀ * d₀
h₁₀ : a₁ * b₀ ≤ c₀ * d₁
h₀₁ : a₀ * b₁ ≤ c₀ * d₁
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
_ : a₀ * b₁ + a₁ * b₀ ≤ c₀ * d₁ + c₁ * d₀
⊢ (a₀ + a₁) * (b₀ + b₁) ≤ (c₀ + c₁) * (d₀ + d₁)

Tactic:
calc
    _ = a₀ * b₀ + (a₀ * b₁ + a₁ * b₀) + a₁ * b₁ := by ring
    _ ≤ c₀ * d₀ + (c₀ * d₁ + c₁ * d₀) + c₁ * d₁ := add_le_add_three h₀₀ ?_ h₁₁
    _ = (c₀ + c₁) * (d₀ + d₁) := by ring

Premises used: HMul.hMul, add_le_add_three, HAdd.hAdd
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
β : Type u_2
inst : CommSemiring β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : ExistsAddOfLE β
a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β
ha₀ : 0 ≤ a₀
ha₁ : 0 ≤ a₁
hb₀ : 0 ≤ b₀
hb₁ : 0 ≤ b₁
hc₀ : 0 ≤ c₀
hc₁ : 0 ≤ c₁
hd₀ : 0 ≤ d₀
hd₁ : 0 ≤ d₁
h₀₀ : a₀ * b₀ ≤ c₀ * d₀
h₁₀ : a₁ * b₀ ≤ c₀ * d₁
h₀₁ : a₀ * b₁ ≤ c₀ * d₁
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
inl : ∀ (hcd : c₀ * d₁ = 0), a₀ * b₁ + a₁ * b₀ ≤ c₀ * d₁ + c₁ * d₀
inr : ∀ (hcd : 0 < c₀ * d₁), a₀ * b₁ + a₁ * b₀ ≤ c₀ * d₁ + c₁ * d₀
⊢ a₀ * b₁ + a₁ * b₀ ≤ c₀ * d₁ + c₁ * d₀

Tactic:
obtain hcd | hcd := (mul_nonneg hc₀ hd₁).eq_or_lt'

Premises used: mul_nonneg, LE.le.eq_or_lt'
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
β : Type u_2
inst : CommSemiring β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : ExistsAddOfLE β
a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β
ha₀ : 0 ≤ a₀
ha₁ : 0 ≤ a₁
hb₀ : 0 ≤ b₀
hb₁ : 0 ≤ b₁
hc₀ : 0 ≤ c₀
hc₁ : 0 ≤ c₁
hd₀ : 0 ≤ d₀
hd₁ : 0 ≤ d₁
h₀₀ : a₀ * b₀ ≤ c₀ * d₀
h₁₀ : a₁ * b₀ ≤ c₀ * d₁
h₀₁ : a₀ * b₁ ≤ c₀ * d₁
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
hcd : c₀ * d₁ = 0
⊢ a₁ * b₀ ≤ 0

Tactic:
rw [hcd] at h₀₁ h₁₀
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
β : Type u_2
inst : CommSemiring β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : ExistsAddOfLE β
a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β
ha₀ : 0 ≤ a₀
ha₁ : 0 ≤ a₁
hb₀ : 0 ≤ b₀
hb₁ : 0 ≤ b₁
hc₀ : 0 ≤ c₀
hc₁ : 0 ≤ c₁
hd₀ : 0 ≤ d₀
hd₁ : 0 ≤ d₁
h₀₀ : a₀ * b₀ ≤ c₀ * d₀
h₁₀ : a₁ * b₀ ≤ c₀ * d₁
h₀₁ : a₀ * b₁ ≤ c₀ * d₁
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
hcd : c₀ * d₁ = 0
h₁₂ : a₁ * b₀ ≤ 0
⊢ a₀ * b₁ ≤ 0

Tactic:
rw [hcd] at h₀₁ h₁₀
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
β : Type u_2
inst : CommSemiring β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : ExistsAddOfLE β
a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β
ha₀ : 0 ≤ a₀
ha₁ : 0 ≤ a₁
hb₀ : 0 ≤ b₀
hb₁ : 0 ≤ b₁
hc₀ : 0 ≤ c₀
hc₁ : 0 ≤ c₁
hd₀ : 0 ≤ d₀
hd₁ : 0 ≤ d₁
h₀₀ : a₀ * b₀ ≤ c₀ * d₀
h₁₀ : a₁ * b₀ ≤ c₀ * d₁
h₀₁ : a₀ * b₁ ≤ c₀ * d₁
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
hcd : c₀ * d₁ = 0
h₁₂ : a₁ * b₀ ≤ 0
h₂ : a₀ * b₁ ≤ 0
⊢ a₁ * b₁ ≤ c₁ * d₁

Tactic:
rw [hcd] at h₀₁ h₁₀
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
β : Type u_2
inst : CommSemiring β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : ExistsAddOfLE β
a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β
ha₀ : 0 ≤ a₀
ha₁ : 0 ≤ a₁
hb₀ : 0 ≤ b₀
hb₁ : 0 ≤ b₁
hc₀ : 0 ≤ c₀
hc₁ : 0 ≤ c₁
hd₀ : 0 ≤ d₀
hd₁ : 0 ≤ d₁
h₀₀ : a₀ * b₀ ≤ c₀ * d₀
h₁₀ : a₁ * b₀ ≤ c₀ * d₁
h₀₁ : a₀ * b₁ ≤ c₀ * d₁
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
hcd : c₀ * d₁ = 0
h₁₂ : a₁ * b₀ ≤ 0
h₂ : a₀ * b₁ ≤ 0
h₁₃ : a₁ * b₁ ≤ c₁ * d₁
⊢ c₀ * d₁ = 0

Tactic:
rw [hcd] at h₀₁ h₁₀
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
β : Type u_2
inst : CommSemiring β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : ExistsAddOfLE β
a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β
ha₀ : 0 ≤ a₀
ha₁ : 0 ≤ a₁
hb₀ : 0 ≤ b₀
hb₁ : 0 ≤ b₁
hc₀ : 0 ≤ c₀
hc₁ : 0 ≤ c₁
hd₀ : 0 ≤ d₀
hd₁ : 0 ≤ d₁
h₀₀ : a₀ * b₀ ≤ c₀ * d₀
h₁₀ : a₁ * b₀ ≤ 0
h₀₁ : a₀ * b₁ ≤ 0
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
hcd : c₀ * d₁ = 0
inl : 0 ≤ c₀ * d₁ + c₁ * d₀
inl₁ : 0 ≤ a₁ * b₀
inl₂ : 0 ≤ a₀ * b₁
⊢ a₀ * b₁ + a₁ * b₀ ≤ c₀ * d₁ + c₁ * d₀

Tactic:
rw [h₀₁.antisymm, h₁₀.antisymm, add_zero]

Premises used: LE.le.antisymm, add_zero
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
β : Type u_2
inst : CommSemiring β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : ExistsAddOfLE β
a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β
ha₀ : 0 ≤ a₀
ha₁ : 0 ≤ a₁
hb₀ : 0 ≤ b₀
hb₁ : 0 ≤ b₁
hc₀ : 0 ≤ c₀
hc₁ : 0 ≤ c₁
hd₀ : 0 ≤ d₀
hd₁ : 0 ≤ d₁
h₀₀ : a₀ * b₀ ≤ c₀ * d₀
h₁₀ : a₁ * b₀ ≤ 0
h₀₁ : a₀ * b₁ ≤ 0
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
hcd : c₀ * d₁ = 0
⊢ 0 ≤ c₀ * d₁ + c₁ * d₀

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
β : Type u_2
inst : CommSemiring β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : ExistsAddOfLE β
a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β
ha₀ : 0 ≤ a₀
ha₁ : 0 ≤ a₁
hb₀ : 0 ≤ b₀
hb₁ : 0 ≤ b₁
hc₀ : 0 ≤ c₀
hc₁ : 0 ≤ c₁
hd₀ : 0 ≤ d₀
hd₁ : 0 ≤ d₁
h₀₀ : a₀ * b₀ ≤ c₀ * d₀
h₁₀ : a₁ * b₀ ≤ 0
h₀₁ : a₀ * b₁ ≤ 0
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
hcd : c₀ * d₁ = 0
⊢ 0 ≤ a₁ * b₀

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
β : Type u_2
inst : CommSemiring β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : ExistsAddOfLE β
a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β
ha₀ : 0 ≤ a₀
ha₁ : 0 ≤ a₁
hb₀ : 0 ≤ b₀
hb₁ : 0 ≤ b₁
hc₀ : 0 ≤ c₀
hc₁ : 0 ≤ c₁
hd₀ : 0 ≤ d₀
hd₁ : 0 ≤ d₁
h₀₀ : a₀ * b₀ ≤ c₀ * d₀
h₁₀ : a₁ * b₀ ≤ 0
h₀₁ : a₀ * b₁ ≤ 0
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
hcd : c₀ * d₁ = 0
⊢ 0 ≤ a₀ * b₁

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
β : Type u_2
inst : CommSemiring β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : ExistsAddOfLE β
a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β
ha₀ : 0 ≤ a₀
ha₁ : 0 ≤ a₁
hb₀ : 0 ≤ b₀
hb₁ : 0 ≤ b₁
hc₀ : 0 ≤ c₀
hc₁ : 0 ≤ c₁
hd₀ : 0 ≤ d₀
hd₁ : 0 ≤ d₁
h₀₀ : a₀ * b₀ ≤ c₀ * d₀
h₁₀ : a₁ * b₀ ≤ c₀ * d₁
h₀₁ : a₀ * b₁ ≤ c₀ * d₁
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
hcd : 0 < c₀ * d₁
⊢ a₀ * b₁ + a₁ * b₀ ≤ c₀ * d₁ + c₁ * d₀

Tactic:
le_of_mul_le_mul_right ?_ hcd

Premises used: le_of_mul_le_mul_right
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
β : Type u_2
inst : CommSemiring β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : ExistsAddOfLE β
a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β
ha₀ : 0 ≤ a₀
ha₁ : 0 ≤ a₁
hb₀ : 0 ≤ b₀
hb₁ : 0 ≤ b₁
hc₀ : 0 ≤ c₀
hc₁ : 0 ≤ c₁
hd₀ : 0 ≤ d₀
hd₁ : 0 ≤ d₁
h₀₀ : a₀ * b₀ ≤ c₀ * d₀
h₁₀ : a₁ * b₀ ≤ c₀ * d₁
h₀₁ : a₀ * b₁ ≤ c₀ * d₁
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
hcd : 0 < c₀ * d₁
inr : (a₀ * b₁ + a₁ * b₀) * (c₀ * d₁) ≤ (c₀ * d₁ + c₁ * d₀) * (c₀ * d₁)
⊢ a₀ * b₁ + a₁ * b₀ ≤ c₀ * d₁ + c₁ * d₀

Tactic:
refine le_of_mul_le_mul_right ?_ hcd

Premises used: le_of_mul_le_mul_right
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
β : Type u_2
inst : CommSemiring β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : ExistsAddOfLE β
a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β
ha₀ : 0 ≤ a₀
ha₁ : 0 ≤ a₁
hb₀ : 0 ≤ b₀
hb₁ : 0 ≤ b₁
hc₀ : 0 ≤ c₀
hc₁ : 0 ≤ c₁
hd₀ : 0 ≤ d₀
hd₁ : 0 ≤ d₁
h₀₀ : a₀ * b₀ ≤ c₀ * d₀
h₁₀ : a₁ * b₀ ≤ c₀ * d₁
h₀₁ : a₀ * b₁ ≤ c₀ * d₁
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
hcd : 0 < c₀ * d₁
⊢ (a₀ * b₁ + a₁ * b₀) * (c₀ * d₁) = a₀ * b₁ * (c₀ * d₁) + c₀ * d₁ * (a₁ * b₀)

Tactic:
ring
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
β : Type u_2
inst : CommSemiring β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : ExistsAddOfLE β
a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β
ha₀ : 0 ≤ a₀
ha₁ : 0 ≤ a₁
hb₀ : 0 ≤ b₀
hb₁ : 0 ≤ b₁
hc₀ : 0 ≤ c₀
hc₁ : 0 ≤ c₁
hd₀ : 0 ≤ d₀
hd₁ : 0 ≤ d₁
h₀₀ : a₀ * b₀ ≤ c₀ * d₀
h₁₀ : a₁ * b₀ ≤ c₀ * d₁
h₀₁ : a₀ * b₁ ≤ c₀ * d₁
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
hcd : 0 < c₀ * d₁
⊢ a₀ * b₁ * (c₀ * d₁) + c₀ * d₁ * (a₁ * b₀) ≤ a₀ * b₁ * (a₁ * b₀) + c₀ * d₁ * (c₀ * d₁)

Tactic:
mul_add_mul_le_mul_add_mul h₀₁ h₁₀

Premises used: mul_add_mul_le_mul_add_mul
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
β : Type u_2
inst : CommSemiring β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : ExistsAddOfLE β
a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β
ha₀ : 0 ≤ a₀
ha₁ : 0 ≤ a₁
hb₀ : 0 ≤ b₀
hb₁ : 0 ≤ b₁
hc₀ : 0 ≤ c₀
hc₁ : 0 ≤ c₁
hd₀ : 0 ≤ d₀
hd₁ : 0 ≤ d₁
h₀₀ : a₀ * b₀ ≤ c₀ * d₀
h₁₀ : a₁ * b₀ ≤ c₀ * d₁
h₀₁ : a₀ * b₁ ≤ c₀ * d₁
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
hcd : 0 < c₀ * d₁
⊢ a₀ * b₁ * (a₁ * b₀) + c₀ * d₁ * (c₀ * d₁) = a₀ * b₀ * (a₁ * b₁) + c₀ * d₁ * (c₀ * d₁)

Tactic:
ring