awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 𝒜
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 z s = (insert w ((s ∪ v) \ u) ∪ u.erase w) \ v.erase z
have h : insert z s = ((s ∪ v) \ u ∪ insert w (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]
-- 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 𝒜
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
⊢ insert z s = (insert w ((s ∪ v) \ u) ∪ u.erase w) \ v.erase z
have h₁ : insert z s = ((s ∪ v) \ u ∪ u) \ 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]
-- 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 𝒜
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
⊢ insert z s = (insert w ((s ∪ v) \ u) ∪ u.erase w) \ v.erase z
have h₂ : insert z s = (s ∪ v) \ 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]
-- 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 𝒜
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
⊢ insert z s = (insert w ((s ∪ v) \ u) ∪ u.erase w) \ v.erase z
have h₃ : insert z s = insert z ((s ∪ v) \ v)
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]
-- 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 𝒜
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)
⊢ insert z s = (insert w ((s ∪ v) \ u) ∪ u.erase w) \ v.erase z
have h₄ : insert z s = insert z s
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]
-- 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 𝒜
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
⊢ False
have hwB₁ : w ∈ s ∪ v → w ∈ u
Tactic: rw [mem_sdiff, ← Classical.not_imp, Classical.not_not] at hwB
Cleared hypotheses: hwB, hw𝒜', this, hwu
-- 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 𝒜
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
⊢ False
have neg : insert w s ∈ 𝒜
Tactic: apply m w (hwu ∘ hwB ∘ mem_union_left _)
-- 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 𝒜
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 ∈ 𝒜
have this₁ : (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⟩)
-- 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 𝒜
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 ∈ 𝒜
have h : insert w s = (insert w ((s ∪ v) \ u) ∪ u) \ v
Tactic: convert! this using 1
-- 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 𝒜
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 = (insert w ((s ∪ v) \ u) ∪ u) \ v
have h : 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]
-- 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 𝒜
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 = (insert w ((s ∪ v) \ u) ∪ u) \ v
have h₁ : insert w s = insert w (s ∪ v) \ 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]
-- 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 𝒜
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
⊢ insert w s = (insert w ((s ∪ v) \ u) ∪ u) \ v
have h₂ : insert w s = insert w ((s ∪ v) \ 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]
-- 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 𝒜
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)
⊢ insert w s = (insert w ((s ∪ v) \ u) ∪ u) \ v
have h₃ : insert w s = insert w s
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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₁) ≤ (c₀ + c₁) * (d₀ + d₁)
have _ : a₀ * b₁ + a₁ * b₀ ≤ c₀ * d₁ + c₁ * 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
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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₀
have inl : ∀ (hcd : c₀ * d₁ = 0), a₀ * b₁ + a₁ * b₀ ≤ c₀ * d₁ + c₁ * d₀
Tactic: obtain hcd | hcd := (mul_nonneg hc₀ hd₁).eq_or_lt'
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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₀
⊢ a₀ * b₁ + a₁ * b₀ ≤ c₀ * d₁ + c₁ * d₀
have inr : ∀ (hcd : 0 < c₀ * d₁), a₀ * b₁ + a₁ * b₀ ≤ c₀ * d₁ + c₁ * d₀
Tactic: obtain hcd | hcd := (mul_nonneg hc₀ hd₁).eq_or_lt'
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (hypothesis)
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₁ + a₁ * b₀ ≤ c₀ * d₁ + c₁ * d₀
have h₁₂ : a₁ * b₀ ≤ 0
Tactic: rw [hcd] at h₀₁ h₁₀
Cleared hypotheses: h₁₀, h₀₁, h₁₁, hcd
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (hypothesis)
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₁ + a₁ * b₀ ≤ c₀ * d₁ + c₁ * d₀
have h₂ : a₀ * b₁ ≤ 0
Tactic: rw [hcd] at h₀₁ h₁₀
Cleared hypotheses: h₁₀, h₀₁, h₁₁, hcd
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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
⊢ a₀ * b₁ + a₁ * b₀ ≤ c₀ * d₁ + c₁ * d₀
have inl : 0 ≤ c₀ * d₁ + c₁ * d₀
Tactic: rw [h₀₁.antisymm, h₁₀.antisymm, add_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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₀
⊢ a₀ * b₁ + a₁ * b₀ ≤ c₀ * d₁ + c₁ * d₀
have inl₁ : 0 ≤ a₁ * b₀
Tactic: rw [h₀₁.antisymm, h₁₀.antisymm, add_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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₀
⊢ a₀ * b₁ + a₁ * b₀ ≤ c₀ * d₁ + c₁ * d₀
have inl₂ : 0 ≤ a₀ * b₁
Tactic: rw [h₀₁.antisymm, h₁₀.antisymm, add_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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₀
have inr : (a₀ * b₁ + a₁ * b₀) * (c₀ * d₁) ≤ (c₀ * d₁ + c₁ * d₀) * (c₀ * d₁)
Tactic: refine le_of_mul_le_mul_right ?_ hcd
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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₁) ≤ c₀ * d₀ * (c₁ * d₁) + c₀ * d₁ * (c₀ * d₁)
have bc : 0 ≤ a₁ * b₁
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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₁
bc : 0 ≤ a₁ * b₁
⊢ a₀ * b₀ * (a₁ * b₁) + c₀ * d₁ * (c₀ * d₁) ≤ c₀ * d₀ * (c₁ * d₁) + c₀ * d₁ * (c₀ * d₁)
have bc₁ : 0 ≤ c₀ * d₀
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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₁ + c₁ * d₀) * (c₀ * d₁)
have calc : (a₀ * b₁ + a₁ * b₀) * (c₀ * d₁) = a₀ * b₁ * (c₀ * d₁) + c₀ * d₁ * (a₁ * b₀)
Tactic: calc (a₀ * b₁ + a₁ * b₀) * (c₀ * d₁)
      = a₀ * b₁ * (c₀ * d₁) + c₀ * d₁ * (a₁ * b₀) := by ring
    _ ≤ a₀ * b₁ * (a₁ * b₀) + c₀ * d₁ * (c₀ * d₁) := mul_add_mul_le_mul_add_mul h₀₁ h₁₀
    _ = a₀ * b₀ * (a₁ * b₁) + c₀ * d₁ * (c₀ * d₁) := by ring
    _ ≤ c₀ * d₀ * (c₁ * d₁) + c₀ * d₁ * (c₀ * d₁) := by gcongr
    _ = (c₀ * d₁ + c₁ * d₀) * (c₀ * d₁) := by ring
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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₁
calc : (a₀ * b₁ + a₁ * b₀) * (c₀ * d₁) = a₀ * b₁ * (c₀ * d₁) + c₀ * d₁ * (a₁ * b₀)
⊢ (a₀ * b₁ + a₁ * b₀) * (c₀ * d₁) ≤ (c₀ * d₁ + c₁ * d₀) * (c₀ * d₁)
have calc₁ : a₀ * b₁ * (a₁ * b₀) + c₀ * d₁ * (c₀ * d₁) = a₀ * b₀ * (a₁ * b₁) + c₀ * d₁ * (c₀ * d₁)
Tactic: calc (a₀ * b₁ + a₁ * b₀) * (c₀ * d₁)
      = a₀ * b₁ * (c₀ * d₁) + c₀ * d₁ * (a₁ * b₀) := by ring
    _ ≤ a₀ * b₁ * (a₁ * b₀) + c₀ * d₁ * (c₀ * d₁) := mul_add_mul_le_mul_add_mul h₀₁ h₁₀
    _ = a₀ * b₀ * (a₁ * b₁) + c₀ * d₁ * (c₀ * d₁) := by ring
    _ ≤ c₀ * d₀ * (c₁ * d₁) + c₀ * d₁ * (c₀ * d₁) := by gcongr
    _ = (c₀ * d₁ + c₁ * d₀) * (c₀ * d₁) := by ring
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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₁
calc : (a₀ * b₁ + a₁ * b₀) * (c₀ * d₁) = a₀ * b₁ * (c₀ * d₁) + c₀ * d₁ * (a₁ * b₀)
calc₁ : a₀ * b₁ * (a₁ * b₀) + c₀ * d₁ * (c₀ * d₁) = a₀ * b₀ * (a₁ * b₁) + c₀ * d₁ * (c₀ * d₁)
⊢ (a₀ * b₁ + a₁ * b₀) * (c₀ * d₁) ≤ (c₀ * d₁ + c₁ * d₀) * (c₀ * d₁)
have calc₂ : a₀ * b₀ * (a₁ * b₁) + c₀ * d₁ * (c₀ * d₁) ≤ c₀ * d₀ * (c₁ * d₁) + c₀ * d₁ * (c₀ * d₁)
Tactic: calc (a₀ * b₁ + a₁ * b₀) * (c₀ * d₁)
      = a₀ * b₁ * (c₀ * d₁) + c₀ * d₁ * (a₁ * b₀) := by ring
    _ ≤ a₀ * b₁ * (a₁ * b₀) + c₀ * d₁ * (c₀ * d₁) := mul_add_mul_le_mul_add_mul h₀₁ h₁₀
    _ = a₀ * b₀ * (a₁ * b₁) + c₀ * d₁ * (c₀ * d₁) := by ring
    _ ≤ c₀ * d₀ * (c₁ * d₁) + c₀ * d₁ * (c₀ * d₁) := by gcongr
    _ = (c₀ * d₁ + c₁ * d₀) * (c₀ * d₁) := by ring