awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this_1 : s ⊆ insert a u
this_2 : t ⊆ insert a u
this_3 : insert a s ⊆ insert a u
this_4 : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this_5 : a ∉ s ∩ t
this : a ∉ s ∪ t
h_1 : s ∈ 𝒜
h_2 : insert a s ∈ 𝒜
pos :
  (f₁ s + f₁ (insert a s)) * ((if t ∈ ℬ then f₂ t else 0) + if insert a t ∈ ℬ then f₂ (insert a t) else 0) ≤
    collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
⊢ (f₁ s + f₁ (insert a s)) * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
rw [collapse_eq hat]

Premises used: collapse_eq
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this_1 : s ⊆ insert a u
this_2 : t ⊆ insert a u
this_3 : insert a s ⊆ insert a u
this_4 : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this_5 : a ∉ s ∩ t
this : a ∉ s ∪ t
h_1 : s ∈ 𝒜
h_2 : insert a s ∈ 𝒜
h_3 : t ∈ ℬ
h_4 : insert a t ∈ ℬ
pos :
  (f₁ s + f₁ (insert a s)) * (f₂ t + f₂ (insert a t)) ≤
    (f₃ (s ∩ t) + f₃ (insert a s ∩ insert a t)) * (f₄ (s ∪ t) + f₄ (insert a s ∪ insert a t))
⊢ (f₁ s + f₁ (insert a s)) * (f₂ t + f₂ (insert a t)) ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
rw [collapse_of_mem ‹_› (inter_mem_infs ‹_› ‹_›) (inter_mem_infs ‹_› ‹_›) rfl
        (insert_inter_distrib _ _ _).symm, collapse_of_mem ‹_› (union_mem_sups ‹_› ‹_›)
        (union_mem_sups ‹_› ‹_›) rfl (insert_union_distrib _ _ _).symm]

Premises used: Finset.inter_mem_infs, Finset.union_mem_sups, collapse_of_mem, Finset.insert_union_distrib, Finset.insert_inter_distrib, Eq.symm, rfl
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this_1 : s ⊆ insert a u
this_2 : t ⊆ insert a u
this_3 : insert a s ⊆ insert a u
this_4 : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this_5 : a ∉ s ∩ t
this : a ∉ s ∪ t
h_1 : s ∈ 𝒜
h_2 : insert a s ∈ 𝒜
h_3 : t ∈ ℬ
h_4 : insert a t ∈ ℬ
⊢ (f₁ s + f₁ (insert a s)) * (f₂ t + f₂ (insert a t)) ≤
    (f₃ (s ∩ t) + f₃ (insert a s ∩ insert a t)) * (f₄ (s ∪ t) + f₄ (insert a s ∪ insert a t))

Tactic:
ineq (h₁ _) (h₁ _) (h₂ _) (h₂ _) (h₃ _) (h₃ _) (h₄ _) (h₄ _) (h ‹_› ‹_›) ?_ ?_ ?_

Premises used: _private.0.ineq
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this_1 : s ⊆ insert a u
this_2 : t ⊆ insert a u
this_3 : insert a s ⊆ insert a u
this_4 : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this_5 : a ∉ s ∩ t
this : a ∉ s ∪ t
h_1 : s ∈ 𝒜
h_2 : insert a s ∈ 𝒜
h_3 : t ∈ ℬ
h_4 : insert a t ∈ ℬ
pos : f₁ (insert a s) * f₂ t ≤ f₃ (s ∩ t) * f₄ (insert a s ∪ insert a t)
pos₁ : f₁ s * f₂ (insert a t) ≤ f₃ (s ∩ t) * f₄ (insert a s ∪ insert a t)
pos₂ : f₁ (insert a s) * f₂ (insert a t) ≤ f₃ (insert a s ∩ insert a t) * f₄ (insert a s ∪ insert a t)
⊢ (f₁ s + f₁ (insert a s)) * (f₂ t + f₂ (insert a t)) ≤
    (f₃ (s ∩ t) + f₃ (insert a s ∩ insert a t)) * (f₄ (s ∪ t) + f₄ (insert a s ∪ insert a t))

Tactic:
refine ineq (h₁ _) (h₁ _) (h₂ _) (h₂ _) (h₃ _) (h₃ _) (h₄ _) (h₄ _) (h ‹_› ‹_›) ?_ ?_ ?_

Premises used: _private.0.ineq
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this_1 : s ⊆ insert a u
this_2 : t ⊆ insert a u
this_3 : insert a s ⊆ insert a u
this_4 : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this_5 : a ∉ s ∩ t
this : a ∉ s ∪ t
h_1 : s ∈ 𝒜
h_2 : insert a s ∈ 𝒜
h_3 : t ∈ ℬ
h_4 : insert a t ∈ ℬ
⊢ f₁ (insert a s) * f₂ t ≤ f₃ (s ∩ t) * f₄ (insert a s ∪ insert a t)

Tactic:
simpa [*] using h ‹insert a s ⊆ _› ‹t ⊆ _›
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this_1 : s ⊆ insert a u
this_2 : t ⊆ insert a u
this_3 : insert a s ⊆ insert a u
this_4 : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this_5 : a ∉ s ∩ t
this : a ∉ s ∪ t
h_1 : s ∈ 𝒜
h_2 : insert a s ∈ 𝒜
h_3 : t ∈ ℬ
h_4 : insert a t ∈ ℬ
⊢ f₁ s * f₂ (insert a t) ≤ f₃ (s ∩ t) * f₄ (insert a s ∪ insert a t)

Tactic:
simpa [*] using h ‹s ⊆ _› ‹insert a t ⊆ _›
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this_1 : s ⊆ insert a u
this_2 : t ⊆ insert a u
this_3 : insert a s ⊆ insert a u
this_4 : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this_5 : a ∉ s ∩ t
this : a ∉ s ∪ t
h_1 : s ∈ 𝒜
h_2 : insert a s ∈ 𝒜
h_3 : t ∈ ℬ
h_4 : insert a t ∈ ℬ
⊢ f₁ (insert a s) * f₂ (insert a t) ≤ f₃ (insert a s ∩ insert a t) * f₄ (insert a s ∪ insert a t)

Tactic:
simpa [*] using h ‹insert a s ⊆ _› ‹insert a t ⊆ _›
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this_1 : s ⊆ insert a u
this_2 : t ⊆ insert a u
this_3 : insert a s ⊆ insert a u
this_4 : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this_5 : a ∉ s ∩ t
this : a ∉ s ∪ t
h_1 : s ∈ 𝒜
h_2 : insert a s ∈ 𝒜
h_3 : t ∈ ℬ
h_4 : insert a t ∉ ℬ
neg : f₁ s * f₂ t + f₁ (insert a s) * f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
⊢ (f₁ s + f₁ (insert a s)) * (f₂ t + 0) ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
rw [add_zero, add_mul]

Premises used: add_mul, add_zero
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this_1 : s ⊆ insert a u
this_2 : t ⊆ insert a u
this_3 : insert a s ⊆ insert a u
this_4 : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this_5 : a ∉ s ∩ t
this : a ∉ s ∪ t
h_1 : s ∈ 𝒜
h_2 : insert a s ∈ 𝒜
h_3 : t ∈ ℬ
h_4 : insert a t ∉ ℬ
⊢ f₁ s * f₂ t + f₁ (insert a s) * f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
(add_le_add (h ‹_› ‹_›) <| h ‹_› ‹_›).trans ?_

Premises used: add_le_add, LE.le.trans
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this_1 : s ⊆ insert a u
this_2 : t ⊆ insert a u
this_3 : insert a s ⊆ insert a u
this_4 : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this_5 : a ∉ s ∩ t
this : a ∉ s ∪ t
h_1 : s ∈ 𝒜
h_2 : insert a s ∈ 𝒜
h_3 : t ∈ ℬ
h_4 : insert a t ∉ ℬ
neg :
  f₃ (s ∩ t) * f₄ (s ∪ t) + f₃ (insert a s ∩ t) * f₄ (insert a s ∪ t) ≤
    collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
⊢ f₁ s * f₂ t + f₁ (insert a s) * f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
refine (add_le_add (h ‹_› ‹_›) <| h ‹_› ‹_›).trans ?_

Premises used: add_le_add, LE.le.trans
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this_1 : s ⊆ insert a u
this_2 : t ⊆ insert a u
this_3 : insert a s ⊆ insert a u
this_4 : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this_5 : a ∉ s ∩ t
this : a ∉ s ∪ t
h_1 : s ∈ 𝒜
h_2 : insert a s ∈ 𝒜
h_3 : t ∈ ℬ
h_4 : insert a t ∉ ℬ
neg :
  f₃ (s ∩ t) * (f₄ (s ∪ t) + f₄ (insert a s ∪ t)) ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * (f₄ (s ∪ t) + f₄ (insert a s ∪ t))
⊢ f₃ (s ∩ t) * f₄ (s ∪ t) + f₃ (insert a s ∩ t) * f₄ (insert a s ∪ t) ≤
    collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
rw [collapse_of_mem ‹_› (union_mem_sups ‹_› ‹_›) (union_mem_sups ‹_› ‹_›) rfl
        (insert_union _ _ _), insert_inter_of_notMem ‹_›, ← mul_add]

Premises used: Finset.insert_inter_of_notMem, Finset.insert_union, Finset.union_mem_sups, collapse_of_mem, mul_add, rfl
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this_1 : s ⊆ insert a u
this_2 : t ⊆ insert a u
this_3 : insert a s ⊆ insert a u
this_4 : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this_5 : a ∉ s ∩ t
this : a ∉ s ∪ t
h_1 : s ∈ 𝒜
h_2 : insert a s ∈ 𝒜
h_3 : t ∈ ℬ
h_4 : insert a t ∉ ℬ
neg : 0 ≤ f₄ (s ∪ t) + f₄ (insert a s ∪ t)
neg₁ : f₃ (s ∩ t) ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t)
⊢ f₃ (s ∩ t) * (f₄ (s ∪ t) + f₄ (insert a s ∪ t)) ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * (f₄ (s ∪ t) + f₄ (insert a s ∪ t))

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this_1 : s ⊆ insert a u
this_2 : t ⊆ insert a u
this_3 : insert a s ⊆ insert a u
this_4 : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this_5 : a ∉ s ∩ t
this : a ∉ s ∪ t
h_1 : s ∈ 𝒜
h_2 : insert a s ∈ 𝒜
h_3 : t ∈ ℬ
h_4 : insert a t ∉ ℬ
⊢ 0 ≤ f₄ (s ∪ t) + f₄ (insert a s ∪ t)

Tactic:
add_nonneg (h₄ _) <| h₄ _

Premises used: add_nonneg
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this_1 : s ⊆ insert a u
this_2 : t ⊆ insert a u
this_3 : insert a s ⊆ insert a u
this_4 : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this_5 : a ∉ s ∩ t
this : a ∉ s ∪ t
h_1 : s ∈ 𝒜
h_2 : insert a s ∈ 𝒜
h_3 : t ∈ ℬ
h_4 : insert a t ∉ ℬ
⊢ f₃ (s ∩ t) ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t)

Tactic:
le_collapse_of_mem ‹_› h₃ rfl <| inter_mem_infs ‹_› ‹_›

Premises used: Finset.inter_mem_infs, le_collapse_of_mem, rfl
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this_1 : s ⊆ insert a u
this_2 : t ⊆ insert a u
this_3 : insert a s ⊆ insert a u
this_4 : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this_5 : a ∉ s ∩ t
this : a ∉ s ∪ t
h_1 : s ∈ 𝒜
h_2 : insert a s ∈ 𝒜
h_3 : t ∈ ℬ
h_4 : insert a t ∉ ℬ
⊢ 0 ≤ f₄ (s ∪ t) + f₄ (insert a s ∪ t)

Tactic:
exacts [add_nonneg (h₄ _) <| h₄ _, le_collapse_of_mem ‹_› h₃ rfl <| inter_mem_infs ‹_› ‹_›]

Premises used: Finset.inter_mem_infs, add_nonneg, le_collapse_of_mem, rfl
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this_1 : s ⊆ insert a u
this_2 : t ⊆ insert a u
this_3 : insert a s ⊆ insert a u
this_4 : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this_5 : a ∉ s ∩ t
this : a ∉ s ∪ t
h_1 : s ∈ 𝒜
h_2 : insert a s ∈ 𝒜
h_3 : t ∉ ℬ
h_4 : insert a t ∈ ℬ
pos :
  f₁ s * f₂ (insert a t) + f₁ (insert a s) * f₂ (insert a t) ≤
    collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
⊢ (f₁ s + f₁ (insert a s)) * (0 + f₂ (insert a t)) ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
rw [zero_add, add_mul]

Premises used: add_mul, zero_add
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this_1 : s ⊆ insert a u
this_2 : t ⊆ insert a u
this_3 : insert a s ⊆ insert a u
this_4 : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this_5 : a ∉ s ∩ t
this : a ∉ s ∪ t
h_1 : s ∈ 𝒜
h_2 : insert a s ∈ 𝒜
h_3 : t ∉ ℬ
h_4 : insert a t ∈ ℬ
⊢ f₁ s * f₂ (insert a t) + f₁ (insert a s) * f₂ (insert a t) ≤
    collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
(add_le_add (h ‹_› ‹_›) <| h ‹_› ‹_›).trans ?_

Premises used: add_le_add, LE.le.trans
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this_1 : s ⊆ insert a u
this_2 : t ⊆ insert a u
this_3 : insert a s ⊆ insert a u
this_4 : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this_5 : a ∉ s ∩ t
this : a ∉ s ∪ t
h_1 : s ∈ 𝒜
h_2 : insert a s ∈ 𝒜
h_3 : t ∉ ℬ
h_4 : insert a t ∈ ℬ
pos :
  f₃ (s ∩ insert a t) * f₄ (s ∪ insert a t) + f₃ (insert a s ∩ insert a t) * f₄ (insert a s ∪ insert a t) ≤
    collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
⊢ f₁ s * f₂ (insert a t) + f₁ (insert a s) * f₂ (insert a t) ≤
    collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
refine (add_le_add (h ‹_› ‹_›) <| h ‹_› ‹_›).trans ?_

Premises used: add_le_add, LE.le.trans
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this_1 : s ⊆ insert a u
this_2 : t ⊆ insert a u
this_3 : insert a s ⊆ insert a u
this_4 : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this_5 : a ∉ s ∩ t
this : a ∉ s ∪ t
h_1 : s ∈ 𝒜
h_2 : insert a s ∈ 𝒜
h_3 : t ∉ ℬ
h_4 : insert a t ∈ ℬ
pos :
  (f₃ (s ∩ insert a t) + f₃ (insert a s ∩ insert a t)) * f₄ (insert a s ∪ insert a t) ≤
    (f₃ (s ∩ insert a t) + f₃ (insert a s ∩ insert a t)) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
⊢ f₃ (s ∩ insert a t) * f₄ (s ∪ insert a t) + f₃ (insert a s ∩ insert a t) * f₄ (insert a s ∪ insert a t) ≤
    collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
rw [collapse_of_mem ‹_› (inter_mem_infs ‹_› ‹_›) (inter_mem_infs ‹_› ‹_›)
        (inter_insert_of_notMem ‹_›) (insert_inter_distrib _ _ _).symm, union_insert,
        insert_union_distrib, ← add_mul]

Premises used: add_mul, Finset.inter_mem_infs, Finset.union_insert, collapse_of_mem, Finset.insert_union_distrib, Finset.inter_insert_of_notMem, Finset.insert_inter_distrib, Eq.symm
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this_1 : s ⊆ insert a u
this_2 : t ⊆ insert a u
this_3 : insert a s ⊆ insert a u
this_4 : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this_5 : a ∉ s ∩ t
this : a ∉ s ∪ t
h_1 : s ∈ 𝒜
h_2 : insert a s ∈ 𝒜
h_3 : t ∉ ℬ
h_4 : insert a t ∈ ℬ
pos : 0 ≤ f₃ (s ∩ insert a t) + f₃ (insert a s ∩ insert a t)
pos₁ : f₄ (insert a s ∪ insert a t) ≤ collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
⊢ (f₃ (s ∩ insert a t) + f₃ (insert a s ∩ insert a t)) * f₄ (insert a s ∪ insert a t) ≤
    (f₃ (s ∩ insert a t) + f₃ (insert a s ∩ insert a t)) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this_1 : s ⊆ insert a u
this_2 : t ⊆ insert a u
this_3 : insert a s ⊆ insert a u
this_4 : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this_5 : a ∉ s ∩ t
this : a ∉ s ∪ t
h_1 : s ∈ 𝒜
h_2 : insert a s ∈ 𝒜
h_3 : t ∉ ℬ
h_4 : insert a t ∈ ℬ
⊢ 0 ≤ f₃ (s ∩ insert a t) + f₃ (insert a s ∩ insert a t)

Tactic:
add_nonneg (h₃ _) <| h₃ _

Premises used: add_nonneg
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this_1 : s ⊆ insert a u
this_2 : t ⊆ insert a u
this_3 : insert a s ⊆ insert a u
this_4 : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this_5 : a ∉ s ∩ t
this : a ∉ s ∪ t
h_1 : s ∈ 𝒜
h_2 : insert a s ∈ 𝒜
h_3 : t ∉ ℬ
h_4 : insert a t ∈ ℬ
⊢ f₄ (insert a s ∪ insert a t) ≤ collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
le_collapse_of_insert_mem ‹_› h₄ (insert_union_distrib _ _ _).symm (union_mem_sups ‹_› ‹_›)

Premises used: le_collapse_of_insert_mem, Finset.union_mem_sups, Finset.insert_union_distrib, Eq.symm
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this_1 : s ⊆ insert a u
this_2 : t ⊆ insert a u
this_3 : insert a s ⊆ insert a u
this_4 : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this_5 : a ∉ s ∩ t
this : a ∉ s ∪ t
h_1 : s ∈ 𝒜
h_2 : insert a s ∈ 𝒜
h_3 : t ∉ ℬ
h_4 : insert a t ∈ ℬ
⊢ 0 ≤ f₃ (s ∩ insert a t) + f₃ (insert a s ∩ insert a t)

Tactic:
exacts [add_nonneg (h₃ _) <| h₃ _,
        le_collapse_of_insert_mem ‹_› h₄ (insert_union_distrib _ _ _).symm (union_mem_sups ‹_› ‹_›)]

Premises used: le_collapse_of_insert_mem, add_nonneg, Finset.union_mem_sups, Finset.insert_union_distrib, Eq.symm