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 ∉ 𝒜
⊢ 0 ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
exact mul_nonneg (collapse_nonneg h₃ _) <| collapse_nonneg h₄ _

Premises used: mul_nonneg, collapse_nonneg
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ ∑ s ∈ u.powerset, collapse 𝒜 a f s =
    HAdd.hAdd (α := β) (∑ s ∈ u.powerset ∩ 𝒜, f s) (∑ s ∈ image (insert a) u.powerset ∩ 𝒜, f s)

Tactic:
?_
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ HAdd.hAdd (α := β) (∑ s ∈ u.powerset ∩ 𝒜, f s) (∑ s ∈ image (insert a) u.powerset ∩ 𝒜, f s) =
    HAdd.hAdd (α := β) (∑ s ∈ u.powerset ∩ 𝒜, f s) (∑ s ∈ (insert a u).powerset \ u.powerset ∩ 𝒜, f s)

Tactic:
?_
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ HAdd.hAdd (α := β) (∑ s ∈ u.powerset ∩ 𝒜, f s) (∑ s ∈ (insert a u).powerset \ u.powerset ∩ 𝒜, f s) = ∑ s ∈ 𝒜, f s

Tactic:
?_
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
calc_1 :
  ∑ s ∈ u.powerset, collapse 𝒜 a f s =
    HAdd.hAdd (α := β) (∑ s ∈ u.powerset ∩ 𝒜, f s) (∑ s ∈ image (insert a) u.powerset ∩ 𝒜, f s)
calc_2 :
  HAdd.hAdd (α := β) (∑ s ∈ u.powerset ∩ 𝒜, f s) (∑ s ∈ image (insert a) u.powerset ∩ 𝒜, f s) =
    HAdd.hAdd (α := β) (∑ s ∈ u.powerset ∩ 𝒜, f s) (∑ s ∈ (insert a u).powerset \ u.powerset ∩ 𝒜, f s)
calc_3 :
  HAdd.hAdd (α := β) (∑ s ∈ u.powerset ∩ 𝒜, f s) (∑ s ∈ (insert a u).powerset \ u.powerset ∩ 𝒜, f s) = ∑ s ∈ 𝒜, f s
⊢ Eq.{u_2 + 1} (α := β) (∑ s ∈ u.powerset, collapse 𝒜 a f s) (∑ s ∈ 𝒜, f s)

Tactic:
calc
    _ = ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ u.powerset.image (insert a) ∩ 𝒜, f s := ?_
    _ = ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ ((insert a u).powerset \ u.powerset) ∩ 𝒜, f s := ?_
    _ = ∑ s ∈ 𝒜, f s := ?_

Premises used: Insert.insert, SDiff.sdiff, Finset.powerset, Finset.image
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
calc_1 :
  Eq.{u_2 + 1} (α := β) (∑ s ∈ u.powerset, collapse 𝒜 a f s)
    (∑ x ∈ u.powerset, ((if x ∈ 𝒜 then f x else 0) + if insert a x ∈ 𝒜 then f (insert a x) else 0))
calc_1₁ : Set.InjOn (insert a) (↑u.powerset : Set (Finset α))
⊢ ∑ s ∈ u.powerset, collapse 𝒜 a f s =
    HAdd.hAdd (α := β) (∑ s ∈ u.powerset ∩ 𝒜, f s) (∑ s ∈ image (insert a) u.powerset ∩ 𝒜, f s)

Tactic:
rw [← Finset.sum_ite_mem, ← Finset.sum_ite_mem, sum_image, ← sum_add_distrib]

Premises used: Finset.sum_ite_mem, Finset.sum_add_distrib, Finset.sum_image
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ Eq.{u_2 + 1} (α := β) (∑ s ∈ u.powerset, collapse 𝒜 a f s)
    (∑ x ∈ u.powerset, ((if x ∈ 𝒜 then f x else 0) + if insert a x ∈ 𝒜 then f (insert a x) else 0))

Tactic:
sum_congr rfl fun s hs ↦ collapse_eq (notMem_mono (mem_powerset.1 hs) hu) _ _

Premises used: collapse_eq, Finset.mem_powerset, Iff.mp, Finset.notMem_mono, Finset.sum_congr, rfl
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ Eq.{u_2 + 1} (α := β) (∑ s ∈ u.powerset, collapse 𝒜 a f s)
    (∑ x ∈ u.powerset, ((if x ∈ 𝒜 then f x else 0) + if insert a x ∈ 𝒜 then f (insert a x) else 0))

Tactic:
exact sum_congr rfl fun s hs ↦ collapse_eq (notMem_mono (mem_powerset.1 hs) hu) _ _

Premises used: collapse_eq, Finset.mem_powerset, Iff.mp, Finset.notMem_mono, Finset.sum_congr, rfl
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ Set.InjOn (insert a) (↑u.powerset : Set (Finset α))

Tactic:
(insert_erase_invOn.2.injOn).mono fun s hs ↦ notMem_mono (mem_powerset.1 hs) hu

Premises used: Finset.insert_erase_invOn, Finset.mem_powerset, And.right, Iff.mp, Set.InjOn.mono, Finset.notMem_mono, Set.LeftInvOn.injOn
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ Set.InjOn (insert a) (↑u.powerset : Set (Finset α))

Tactic:
exact (insert_erase_invOn.2.injOn).mono fun s hs ↦ notMem_mono (mem_powerset.1 hs) hu

Premises used: Finset.insert_erase_invOn, Finset.mem_powerset, And.right, Iff.mp, Set.InjOn.mono, Finset.notMem_mono, Set.LeftInvOn.injOn
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
calc_2 : ∀ (s : Finset α), s ∈ image (insert a) u.powerset ↔ s ∈ (insert a u).powerset \ u.powerset
⊢ HAdd.hAdd (α := β) (∑ s ∈ u.powerset ∩ 𝒜, f s) (∑ s ∈ image (insert a) u.powerset ∩ 𝒜, f s) =
    HAdd.hAdd (α := β) (∑ s ∈ u.powerset ∩ 𝒜, f s) (∑ s ∈ (insert a u).powerset \ u.powerset ∩ 𝒜, f s)

Tactic:
congr with s
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
s : Finset α
calc_2 : (∃ a_1 ⊆ u, insert a a_1 = s) ↔ s.erase a ⊆ u ∧ ¬s ⊆ u
⊢ s ∈ image (insert a) u.powerset ↔ s ∈ (insert a u).powerset \ u.powerset

Tactic:
simp only [mem_image, mem_powerset, mem_sdiff, subset_insert_iff]

Premises used: Finset.mem_image, Finset.mem_powerset, Finset.mem_sdiff, Finset.subset_insert_iff
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
s : Finset α
⊢ (∃ a_1 ⊆ u, insert a a_1 = s) ↔ s.erase a ⊆ u ∧ ¬s ⊆ u

Tactic:
⟨?_, fun h ↦ ⟨_, h.1, ?_⟩⟩

Premises used: And.left, And.intro, Iff.intro, Exists.intro, Finset.erase
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
s : Finset α
calc_2 : (∃ a_1 ⊆ u, insert a a_1 = s) → s.erase a ⊆ u ∧ ¬s ⊆ u
calc_2₁ : ∀ (h : s.erase a ⊆ u ∧ ¬s ⊆ u), insert a (s.erase a) = s
⊢ (∃ a_1 ⊆ u, insert a a_1 = s) ↔ s.erase a ⊆ u ∧ ¬s ⊆ u

Tactic:
refine ⟨?_, fun h ↦ ⟨_, h.1, ?_⟩⟩
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
s : Finset α
hs : s ⊆ u
⊢ (insert a s).erase a ⊆ u ∧ ¬insert a s ⊆ u

Tactic:
⟨subset_insert_iff.1 <| insert_subset_insert _ hs, fun h ↦
        hu <| h <| mem_insert_self _ _⟩

Premises used: Finset.insert_subset_insert, Finset.mem_insert_self, And.intro, Iff.mp, Finset.subset_insert_iff
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
s : Finset α
hs : s ⊆ u
⊢ (insert a s).erase a ⊆ u ∧ ¬insert a s ⊆ u

Tactic:
exact ⟨subset_insert_iff.1 <| insert_subset_insert _ hs, fun h ↦
        hu <| h <| mem_insert_self _ _⟩
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
s : Finset α
h : s.erase a ⊆ u ∧ ¬s ⊆ u
rw : ∀ (hs : s.erase a = s), False
⊢ insert a (s.erase a) = s

Tactic:
rw [insert_erase (erase_ne_self.1 fun hs ↦ ?_)]

Premises used: Iff.mp, Finset.insert_erase, Finset.erase_ne_self
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
s : Finset α
h : s.erase a ⊆ u ∧ ¬s ⊆ u
hs : s.erase a = s
⊢ s ⊆ u ∧ ¬s ⊆ u

Tactic:
rw [hs] at h
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
s : Finset α
h : s.erase a ⊆ u ∧ ¬s ⊆ u
hs : s.erase a = s
h₁ : s ⊆ u ∧ ¬s ⊆ u
⊢ s.erase a = s

Tactic:
rw [hs] at h
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
s : Finset α
h : s ⊆ u ∧ ¬s ⊆ u
hs : s.erase a = s
⊢ False

Tactic:
h.2 h.1

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
s : Finset α
h : s ⊆ u ∧ ¬s ⊆ u
hs : s.erase a = s
⊢ False

Tactic:
exact h.2 h.1

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
calc_3 : Eq.{u_2 + 1} (α := β) (∑ x ∈ u.powerset ∩ 𝒜 ∪ (insert a u).powerset \ u.powerset ∩ 𝒜, f x) (∑ s ∈ 𝒜, f s)
calc_3₁ : Eq.{u_2 + 1} (α := β) (∑ x ∈ (u.powerset ∪ (insert a u).powerset \ u.powerset) ∩ 𝒜, f x) (∑ s ∈ 𝒜, f s)
calc_3₂ : Eq.{u_2 + 1} (α := β) (∑ x ∈ (insert a u).powerset ∩ 𝒜, f x) (∑ s ∈ 𝒜, f s)
calc_3₃ calc_3₄ : Eq.{u_2 + 1} (α := β) (∑ x ∈ 𝒜, f x) (∑ s ∈ 𝒜, f s)
⊢ HAdd.hAdd (α := β) (∑ s ∈ u.powerset ∩ 𝒜, f s) (∑ s ∈ (insert a u).powerset \ u.powerset ∩ 𝒜, f s) = ∑ s ∈ 𝒜, f s

Tactic:
rw [← sum_union (disjoint_sdiff_self_right.mono inf_le_left inf_le_left),
      ← union_inter_distrib_right, union_sdiff_of_subset (powerset_mono.2 <| subset_insert _ _),
      inter_eq_right.2 h𝒜]

Premises used: Iff.mpr, Finset.sum_union, Finset.inter_eq_right, Finset.subset_insert, Finset.union_sdiff_of_subset, Disjoint.mono, Finset.powerset_mono, Finset.union_inter_distrib_right
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : Finset α → β
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ ∅ → ∀ ⦃t : Finset α⦄, t ⊆ ∅ → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
h𝒜 : 𝒜 ⊆ powerset ∅
hℬ : ℬ ⊆ powerset ∅
⊢ 𝒜 = ∅ ∨ 𝒜 = {∅}

Tactic:
simp only [Finset.powerset_empty, Finset.subset_singleton_iff] at h𝒜 hℬ

Premises used: Finset.subset_singleton_iff, Finset.powerset_empty
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : Finset α → β
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ ∅ → ∀ ⦃t : Finset α⦄, t ⊆ ∅ → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
h𝒜 : 𝒜 ⊆ powerset ∅
hℬ : ℬ ⊆ powerset ∅
h𝒜₁ : 𝒜 = ∅ ∨ 𝒜 = {∅}
⊢ ℬ = ∅ ∨ ℬ = {∅}

Tactic:
simp only [Finset.powerset_empty, Finset.subset_singleton_iff] at h𝒜 hℬ

Premises used: Finset.subset_singleton_iff, Finset.powerset_empty
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : Finset α → β
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ ∅ → ∀ ⦃t : Finset α⦄, t ⊆ ∅ → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
h𝒜 : 𝒜 = ∅ ∨ 𝒜 = {∅}
hℬ : ℬ = ∅ ∨ ℬ = {∅}
empty : HMul.hMul (α := β) (∑ s ∈ ∅, f₁ s) (∑ s ∈ ℬ, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ ∅ ⊼ ℬ, f₃ s) (∑ s ∈ ∅ ⊻ ℬ, f₄ s)
empty₁ :
  HMul.hMul (α := β) (∑ s ∈ {∅}, f₁ s) (∑ s ∈ ℬ, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ {∅} ⊼ ℬ, f₃ s) (∑ s ∈ {∅} ⊻ ℬ, f₄ s)
⊢ HMul.hMul (α := β) (∑ s ∈ 𝒜, f₁ s) (∑ s ∈ ℬ, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) (∑ s ∈ 𝒜 ⊻ ℬ, f₄ s)

Tactic:
obtain rfl | rfl := h𝒜

Premises used: rfl
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : Finset α → β
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ ∅ → ∀ ⦃t : Finset α⦄, t ⊆ ∅ → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
ℬ : Finset (Finset α)
hℬ : ℬ = ∅ ∨ ℬ = {∅}
empty : HMul.hMul (α := β) (∑ s ∈ ∅, f₁ s) (∑ s ∈ ∅, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ ∅ ⊼ ∅, f₃ s) (∑ s ∈ ∅ ⊻ ∅, f₄ s)
empty₁ :
  HMul.hMul (α := β) (∑ s ∈ ∅, f₁ s) (∑ s ∈ {∅}, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ ∅ ⊼ {∅}, f₃ s) (∑ s ∈ ∅ ⊻ {∅}, f₄ s)
⊢ HMul.hMul (α := β) (∑ s ∈ ∅, f₁ s) (∑ s ∈ ℬ, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ ∅ ⊼ ℬ, f₃ s) (∑ s ∈ ∅ ⊻ ℬ, f₄ s)

Tactic:
obtain rfl | rfl := hℬ

Premises used: rfl
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : Finset α → β
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ ∅ → ∀ ⦃t : Finset α⦄, t ⊆ ∅ → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
ℬ : Finset (Finset α)
hℬ : ℬ = ∅ ∨ ℬ = {∅}
empty :
  HMul.hMul (α := β) (∑ s ∈ {∅}, f₁ s) (∑ s ∈ ∅, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ {∅} ⊼ ∅, f₃ s) (∑ s ∈ {∅} ⊻ ∅, f₄ s)
empty₁ :
  HMul.hMul (α := β) (∑ s ∈ {∅}, f₁ s) (∑ s ∈ {∅}, f₂ s) ≤
    HMul.hMul (α := β) (∑ s ∈ {∅} ⊼ {∅}, f₃ s) (∑ s ∈ {∅} ⊻ {∅}, f₄ s)
⊢ HMul.hMul (α := β) (∑ s ∈ {∅}, f₁ s) (∑ s ∈ ℬ, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ {∅} ⊼ ℬ, f₃ s) (∑ s ∈ {∅} ⊻ ℬ, f₄ s)

Tactic:
obtain rfl | rfl := hℬ

Premises used: rfl
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : Finset α → β
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ ∅ → ∀ ⦃t : Finset α⦄, t ⊆ ∅ → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
⊢ HMul.hMul (α := β) (∑ s ∈ ∅, f₁ s) (∑ s ∈ ∅, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ ∅ ⊼ ∅, f₃ s) (∑ s ∈ ∅ ⊻ ∅, f₄ s)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : Finset α → β
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ ∅ → ∀ ⦃t : Finset α⦄, t ⊆ ∅ → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
⊢ HMul.hMul (α := β) (∑ s ∈ ∅, f₁ s) (∑ s ∈ {∅}, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ ∅ ⊼ {∅}, f₃ s) (∑ s ∈ ∅ ⊻ {∅}, f₄ s)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : Finset α → β
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ ∅ → ∀ ⦃t : Finset α⦄, t ⊆ ∅ → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
⊢ HMul.hMul (α := β) (∑ s ∈ {∅}, f₁ s) (∑ s ∈ ∅, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ {∅} ⊼ ∅, f₃ s) (∑ s ∈ {∅} ⊻ ∅, f₄ s)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : Finset α → β
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ ∅ → ∀ ⦃t : Finset α⦄, t ⊆ ∅ → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
empty : f₁ ∅ * f₂ ∅ ≤ f₃ ∅ * f₄ ∅
⊢ HMul.hMul (α := β) (∑ s ∈ {∅}, f₁ s) (∑ s ∈ {∅}, f₂ s) ≤
    HMul.hMul (α := β) (∑ s ∈ {∅} ⊼ {∅}, f₃ s) (∑ s ∈ {∅} ⊻ {∅}, f₄ s)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : Finset α → β
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ ∅ → ∀ ⦃t : Finset α⦄, t ⊆ ∅ → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
⊢ f₁ ∅ * f₂ ∅ ≤ f₃ ∅ * f₄ ∅

Tactic:
h (subset_refl ∅) subset_rfl

Premises used: Multiset.zero, subset_refl, Finset.empty, Multiset.ofList, List.filter, EmptyCollection.emptyCollection, List.foldr, subset_rfl, Multiset.ndinter, Multiset.ndunion, Multiset.filter
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : Finset α → β
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ ∅ → ∀ ⦃t : Finset α⦄, t ⊆ ∅ → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
⊢ f₁ ∅ * f₂ ∅ ≤ f₃ ∅ * f₄ ∅

Tactic:
exact h (subset_refl ∅) subset_rfl

Premises used: subset_refl, EmptyCollection.emptyCollection, subset_rfl
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : ExistsAddOfLE β
a : α
u : Finset α
hu : a ∉ u
ih :
  ∀ {f₁ f₂ f₃ f₄ : Finset α → β} (h₁ : 0 ≤ f₁) (h₂ : 0 ≤ f₂) (h₃ : 0 ≤ f₃) (h₄ : 0 ≤ f₄)
    (h : ∀ ⦃s : Finset α⦄, s ⊆ u → ∀ ⦃t : Finset α⦄, t ⊆ u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t))
    {𝒜 ℬ : Finset (Finset α)} (h𝒜 : 𝒜 ⊆ u.powerset) (hℬ : ℬ ⊆ u.powerset),
    HMul.hMul (α := β) (∑ s ∈ 𝒜, f₁ s) (∑ s ∈ ℬ, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) (∑ s ∈ 𝒜 ⊻ ℬ, f₄ s)
f₁ f₂ f₃ f₄ : Finset α → β
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 α)
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hℬ : ℬ ⊆ (insert a u).powerset
⊢ HMul.hMul (α := β) (∑ s ∈ u.powerset, collapse 𝒜 a f₁ s) (∑ s ∈ u.powerset, collapse ℬ a f₂ s) ≤
    HMul.hMul (α := β) (∑ s ∈ u.powerset ⊼ u.powerset, collapse (𝒜 ⊼ ℬ) a f₃ s)
      (∑ s ∈ u.powerset ⊻ u.powerset, collapse (𝒜 ⊻ ℬ) a f₄ s)

Tactic:
specialize ih (collapse_nonneg h₁) (collapse_nonneg h₂) (collapse_nonneg h₃)
      (collapse_nonneg h₄) (collapse_modular hu h₁ h₂ h₃ h₄ h 𝒜 ℬ) Subset.rfl Subset.rfl

Premises used: Finset.Subset.rfl, collapse_nonneg, collapse_modular
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : ExistsAddOfLE β
a : α
u : Finset α
hu : a ∉ u
f₁ f₂ f₃ f₄ : Finset α → β
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 α)
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hℬ : ℬ ⊆ (insert a u).powerset
ih :
  HMul.hMul (α := β) (∑ s ∈ u.powerset, collapse 𝒜 a f₁ s) (∑ s ∈ u.powerset, collapse ℬ a f₂ s) ≤
    HMul.hMul (α := β) (∑ s ∈ u.powerset ⊼ u.powerset, collapse (𝒜 ⊼ ℬ) a f₃ s)
      (∑ s ∈ u.powerset ⊻ u.powerset, collapse (𝒜 ⊻ ℬ) a f₄ s)
⊢ 𝒜 ⊼ ℬ ⊆ (insert a u).powerset

Tactic:
simpa using infs_subset h𝒜 hℬ

Premises used: Finset.infs_subset
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : ExistsAddOfLE β
a : α
u : Finset α
hu : a ∉ u
f₁ f₂ f₃ f₄ : Finset α → β
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 α)
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hℬ : ℬ ⊆ (insert a u).powerset
ih :
  HMul.hMul (α := β) (∑ s ∈ u.powerset, collapse 𝒜 a f₁ s) (∑ s ∈ u.powerset, collapse ℬ a f₂ s) ≤
    HMul.hMul (α := β) (∑ s ∈ u.powerset ⊼ u.powerset, collapse (𝒜 ⊼ ℬ) a f₃ s)
      (∑ s ∈ u.powerset ⊻ u.powerset, collapse (𝒜 ⊻ ℬ) a f₄ s)
⊢ 𝒜 ⊼ ℬ ⊆ (insert a u).powerset

Tactic:
have : 𝒜 ⊼ ℬ ⊆ powerset (insert a u) := by simpa using infs_subset h𝒜 hℬ
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : ExistsAddOfLE β
a : α
u : Finset α
hu : a ∉ u
f₁ f₂ f₃ f₄ : Finset α → β
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 α)
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hℬ : ℬ ⊆ (insert a u).powerset
ih :
  HMul.hMul (α := β) (∑ s ∈ u.powerset, collapse 𝒜 a f₁ s) (∑ s ∈ u.powerset, collapse ℬ a f₂ s) ≤
    HMul.hMul (α := β) (∑ s ∈ u.powerset ⊼ u.powerset, collapse (𝒜 ⊼ ℬ) a f₃ s)
      (∑ s ∈ u.powerset ⊻ u.powerset, collapse (𝒜 ⊻ ℬ) a f₄ s)
this : 𝒜 ⊼ ℬ ⊆ (insert a u).powerset
⊢ 𝒜 ⊻ ℬ ⊆ (insert a u).powerset

Tactic:
simpa using sups_subset h𝒜 hℬ

Premises used: Finset.sups_subset
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : ExistsAddOfLE β
a : α
u : Finset α
hu : a ∉ u
f₁ f₂ f₃ f₄ : Finset α → β
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 α)
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hℬ : ℬ ⊆ (insert a u).powerset
ih :
  HMul.hMul (α := β) (∑ s ∈ u.powerset, collapse 𝒜 a f₁ s) (∑ s ∈ u.powerset, collapse ℬ a f₂ s) ≤
    HMul.hMul (α := β) (∑ s ∈ u.powerset ⊼ u.powerset, collapse (𝒜 ⊼ ℬ) a f₃ s)
      (∑ s ∈ u.powerset ⊻ u.powerset, collapse (𝒜 ⊻ ℬ) a f₄ s)
this : 𝒜 ⊼ ℬ ⊆ (insert a u).powerset
⊢ 𝒜 ⊻ ℬ ⊆ (insert a u).powerset

Tactic:
have : 𝒜 ⊻ ℬ ⊆ powerset (insert a u) := by simpa using sups_subset h𝒜 hℬ