awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁
bc : 0 ≤ a₁ * b₁
bc₁ : 0 ≤ c₀ * d₀
⊢ a₀ * b₀ * (a₁ * b₁) + c₀ * d₁ * (c₀ * d₁) ≤ c₀ * d₀ * (c₁ * d₁) + c₀ * d₁ * (c₀ * d₁)

Tactic:
gcongr
-- 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₁
⊢ c₀ * d₀ * (c₁ * d₁) + c₀ * d₁ * (c₀ * d₁) = (c₀ * d₁ + c₁ * d₀) * (c₀ * 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₁
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₁)
calc₂ : a₀ * b₀ * (a₁ * b₁) + c₀ * d₁ * (c₀ * d₁) ≤ c₀ * d₀ * (c₁ * d₁) + c₀ * d₁ * (c₀ * d₁)
calc₃ : c₀ * d₀ * (c₁ * d₁) + c₀ * d₁ * (c₀ * d₁) = (c₀ * d₁ + c₁ * d₀) * (c₀ * d₁)
⊢ (a₀ * b₁ + a₁ * b₀) * (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

Premises used: HMul.hMul, HAdd.hAdd, mul_add_mul_le_mul_add_mul
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s t : Finset α
hs : a ∉ s
⊢ t.erase a = s ↔ t = s ∨ t = insert a s

Tactic:
grind
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
h :
  ∀ (t : Finset α),
    t ∈ {t ∈ 𝒜 | t.erase a = s} ↔
      Membership.mem (γ := Finset (Finset α))
        (if s ∈ 𝒜 then if insert a s ∈ 𝒜 then {s, insert a s} else {s} else if insert a s ∈ 𝒜 then {insert a s} else ∅)
        t
⊢ {t ∈ 𝒜 | t.erase a = s} =
    if s ∈ 𝒜 then if insert a s ∈ 𝒜 then {s, insert a s} else {s} else if insert a s ∈ 𝒜 then {insert a s} else ∅

Tactic:
ext t
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
pos : s ∈ 𝒜 → insert a s ∈ 𝒜 → (t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ Membership.mem (γ := Finset (Finset α)) {s, insert a s} t)
neg : s ∈ 𝒜 → insert a s ∉ 𝒜 → (t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ Membership.mem (γ := Finset (Finset α)) {s} t)
pos₁ : s ∉ 𝒜 → insert a s ∈ 𝒜 → (t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ Membership.mem (γ := Finset (Finset α)) {insert a s} t)
neg₁ : s ∉ 𝒜 → insert a s ∉ 𝒜 → (t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ Membership.mem (γ := Finset (Finset α)) ∅ t)
⊢ t ∈ {t ∈ 𝒜 | t.erase a = s} ↔
    Membership.mem (γ := Finset (Finset α))
      (if s ∈ 𝒜 then if insert a s ∈ 𝒜 then {s, insert a s} else {s} else if insert a s ∈ 𝒜 then {insert a s} else ∅) t

Tactic:
split_ifs
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h : s ∈ 𝒜
h_1 : insert a s ∈ 𝒜
pos : t = s ∨ t = insert a s → t ∈ 𝒜
⊢ t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ Membership.mem (γ := Finset (Finset α)) {s, insert a s} t

Tactic:
simp [erase_eq_iff ha]

Premises used: _private.0.erase_eq_iff
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h : s ∈ 𝒜
h_1 : insert a s ∉ 𝒜
neg : t ∈ 𝒜 ∧ (t = s ∨ t = insert a s) ↔ t = s
⊢ t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ Membership.mem (γ := Finset (Finset α)) {s} t

Tactic:
simp [erase_eq_iff ha]

Premises used: _private.0.erase_eq_iff
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h : s ∉ 𝒜
h_1 : insert a s ∈ 𝒜
pos : t ∈ 𝒜 ∧ (t = s ∨ t = insert a s) ↔ t = insert a s
⊢ t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ Membership.mem (γ := Finset (Finset α)) {insert a s} t

Tactic:
simp [erase_eq_iff ha]

Premises used: _private.0.erase_eq_iff
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h : s ∉ 𝒜
h_1 : insert a s ∉ 𝒜
neg : t ∈ 𝒜 → ¬t = s ∧ ¬t = insert a s
⊢ t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ Membership.mem (γ := Finset (Finset α)) ∅ t

Tactic:
simp [erase_eq_iff ha]

Premises used: _private.0.erase_eq_iff
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h : s ∈ 𝒜
h_1 : insert a s ∈ 𝒜
⊢ t = s ∨ t = insert a s → t ∈ 𝒜

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h : s ∈ 𝒜
h_1 : insert a s ∉ 𝒜
⊢ t ∈ 𝒜 ∧ (t = s ∨ t = insert a s) ↔ t = s

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h : s ∉ 𝒜
h_1 : insert a s ∈ 𝒜
⊢ t ∈ 𝒜 ∧ (t = s ∨ t = insert a s) ↔ t = insert a s

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h : s ∉ 𝒜
h_1 : insert a s ∉ 𝒜
⊢ t ∈ 𝒜 → ¬t = s ∧ ¬t = insert a s

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
f : Finset α → β
rw :
  ∑ t ∈ if s ∈ 𝒜 then if insert a s ∈ 𝒜 then {s, insert a s} else {s} else if insert a s ∈ 𝒜 then {insert a s} else ∅,
      f t =
    (if s ∈ 𝒜 then f s else 0) + if insert a s ∈ 𝒜 then f (insert a s) else 0
⊢ collapse 𝒜 a f s = (if s ∈ 𝒜 then f s else 0) + if insert a s ∈ 𝒜 then f (insert a s) else 0

Tactic:
rw [collapse, filter_collapse_eq ha]

Premises used: _private.0.filter_collapse_eq, _private.0.collapse
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
f : Finset α → β
pos : s ∈ 𝒜 → insert a s ∈ 𝒜 → ∑ x ∈ {s, insert a s}, f x = f s + f (insert a s)
neg : s ∈ 𝒜 → insert a s ∉ 𝒜 → ∑ x ∈ {s}, f x = f s + 0
pos₁ : s ∉ 𝒜 → insert a s ∈ 𝒜 → ∑ x ∈ {insert a s}, f x = 0 + f (insert a s)
neg₁ : s ∉ 𝒜 → insert a s ∉ 𝒜 → ∑ x ∈ ∅, f x = HAdd.hAdd (α := β) 0 0
⊢ ∑ t ∈ if s ∈ 𝒜 then if insert a s ∈ 𝒜 then {s, insert a s} else {s} else if insert a s ∈ 𝒜 then {insert a s} else ∅,
      f t =
    (if s ∈ 𝒜 then f s else 0) + if insert a s ∈ 𝒜 then f (insert a s) else 0

Tactic:
split_ifs
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
f : Finset α → β
h : s ∈ 𝒜
h_1 : insert a s ∈ 𝒜
⊢ ∑ x ∈ {s, insert a s}, f x = f s + f (insert a s)

Tactic:
simp [(ne_of_mem_of_not_mem' (mem_insert_self a s) ha).symm, *]

Premises used: Finset.mem_insert_self, Ne.symm, ne_of_mem_of_not_mem'
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
f : Finset α → β
h : s ∈ 𝒜
h_1 : insert a s ∉ 𝒜
⊢ ∑ x ∈ {s}, f x = f s + 0

Tactic:
simp [(ne_of_mem_of_not_mem' (mem_insert_self a s) ha).symm, *]

Premises used: Finset.mem_insert_self, Ne.symm, ne_of_mem_of_not_mem'
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
f : Finset α → β
h : s ∉ 𝒜
h_1 : insert a s ∈ 𝒜
⊢ ∑ x ∈ {insert a s}, f x = 0 + f (insert a s)

Tactic:
simp [(ne_of_mem_of_not_mem' (mem_insert_self a s) ha).symm, *]

Premises used: Finset.mem_insert_self, Ne.symm, ne_of_mem_of_not_mem'
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
f : Finset α → β
h : s ∉ 𝒜
h_1 : insert a s ∉ 𝒜
⊢ ∑ x ∈ ∅, f x = HAdd.hAdd (α := β) 0 0

Tactic:
simp [(ne_of_mem_of_not_mem' (mem_insert_self a s) ha).symm, *]

Premises used: Finset.mem_insert_self, Ne.symm, ne_of_mem_of_not_mem'
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t u : Finset α
ha : a ∉ s
ht : t ∈ 𝒜
hu : u ∈ 𝒜
hts : t = s
hus : u = insert a s
subst : ∀ (ha : a ∉ t) (hus : u = insert a t), collapse 𝒜 a f t = f t + f u
⊢ collapse 𝒜 a f s = f t + f u

Tactic:
subst hts
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t u : Finset α
ht : t ∈ 𝒜
hu : u ∈ 𝒜
ha : a ∉ t
hus : u = insert a t
subst : ∀ (hu : insert a t ∈ 𝒜), collapse 𝒜 a f t = f t + f (insert a t)
⊢ collapse 𝒜 a f t = f t + f u

Tactic:
subst hus
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
ht : t ∈ 𝒜
ha : a ∉ t
hu : insert a t ∈ 𝒜
simp_rw : ((if t ∈ 𝒜 then f t else 0) + if insert a t ∈ 𝒜 then f (insert a t) else 0) = f t + f (insert a t)
simp_rw₁ : (f t + if insert a t ∈ 𝒜 then f (insert a t) else 0) = f t + f (insert a t)
⊢ collapse 𝒜 a f t = f t + f (insert a t)

Tactic:
simp_rw [collapse_eq ha, if_pos ht, if_pos hu]

Premises used: collapse_eq, if_pos
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = s
ht : t ∈ 𝒜
subst : ∀ (ha : a ∉ t), f t ≤ collapse 𝒜 a f t
⊢ f t ≤ collapse 𝒜 a f s

Tactic:
subst hts
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
hf : 0 ≤ f
ht : t ∈ 𝒜
ha : a ∉ t
rw : f t ≤ f t + if insert a t ∈ 𝒜 then f (insert a t) else 0
⊢ f t ≤ collapse 𝒜 a f t

Tactic:
rw [collapse_eq ha, if_pos ht]

Premises used: collapse_eq, if_pos
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
hf : 0 ≤ f
ht : t ∈ 𝒜
ha : a ∉ t
pos : insert a t ∈ 𝒜 → f t ≤ f t + f (insert a t)
neg : insert a t ∉ 𝒜 → f t ≤ f t + 0
⊢ f t ≤ f t + if insert a t ∈ 𝒜 then f (insert a t) else 0

Tactic:
split_ifs
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
hf : 0 ≤ f
ht : t ∈ 𝒜
ha : a ∉ t
h : insert a t ∈ 𝒜
⊢ f t ≤ f t + f (insert a t)

Tactic:
le_add_of_nonneg_right <| hf _

Premises used: le_add_of_nonneg_right
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
hf : 0 ≤ f
ht : t ∈ 𝒜
ha : a ∉ t
h : insert a t ∈ 𝒜
⊢ f t ≤ f t + f (insert a t)

Tactic:
exact le_add_of_nonneg_right <| hf _

Premises used: le_add_of_nonneg_right
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
hf : 0 ≤ f
ht : t ∈ 𝒜
ha : a ∉ t
h : insert a t ∉ 𝒜
neg neg₁ : f t ≤ f t
⊢ f t ≤ f t + 0

Tactic:
rw [add_zero]

Premises used: 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 β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = insert a s
ht : t ∈ 𝒜
rw : f t ≤ (if s ∈ 𝒜 then f s else 0) + f t
⊢ f t ≤ collapse 𝒜 a f s

Tactic:
rw [collapse_eq ha, ← hts, if_pos ht]

Premises used: collapse_eq, if_pos
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = insert a s
ht : t ∈ 𝒜
pos : s ∈ 𝒜 → f t ≤ f s + f t
neg : s ∉ 𝒜 → f t ≤ 0 + f t
⊢ f t ≤ (if s ∈ 𝒜 then f s else 0) + f t

Tactic:
split_ifs
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = insert a s
ht : t ∈ 𝒜
h : s ∈ 𝒜
⊢ f t ≤ f s + f t

Tactic:
le_add_of_nonneg_left <| hf _

Premises used: le_add_of_nonneg_left
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = insert a s
ht : t ∈ 𝒜
h : s ∈ 𝒜
⊢ f t ≤ f s + f t

Tactic:
exact le_add_of_nonneg_left <| hf _

Premises used: le_add_of_nonneg_left
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = insert a s
ht : t ∈ 𝒜
h : s ∉ 𝒜
neg neg₁ : f t ≤ f t
⊢ f t ≤ 0 + f t

Tactic:
rw [zero_add]

Premises used: 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 β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
hf : 0 ≤ f
⊢ 0 ≤ collapse 𝒜 a f

Tactic:
fun _s ↦ sum_nonneg fun _t _ ↦ hf _

Premises used: Finset.sum_nonneg, _private.0.collapse
-- 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
⊢ s ⊆ insert a u

Tactic:
have := hsu.trans <| subset_insert a _
-- 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 : s ⊆ insert a u
⊢ t ⊆ insert a u

Tactic:
have := htu.trans <| subset_insert a _
-- 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 : t ⊆ insert a u
⊢ insert a s ⊆ insert a u

Tactic:
have := insert_subset_insert a hsu
-- 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 : insert a s ⊆ insert a u
⊢ insert a t ⊆ insert a u

Tactic:
have := insert_subset_insert a htu
-- 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 : insert a t ⊆ insert a u
⊢ a ∉ s

Tactic:
have has := notMem_mono hsu hu
-- 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 : insert a t ⊆ insert a u
has : a ∉ s
⊢ a ∉ t

Tactic:
have hat := notMem_mono htu hu
-- 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 : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
⊢ a ∉ s ∩ t

Tactic:
have : a ∉ s ∩ t := notMem_mono (inter_subset_left.trans hsu) hu
-- 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 : a ∉ s ∩ t
⊢ a ∉ s ∪ t

Tactic:
have := notMem_union.2 ⟨has, hat⟩
-- 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
rw :
  ((if s ∈ 𝒜 then f₁ s else 0) + if insert a s ∈ 𝒜 then f₁ (insert a s) else 0) * collapse ℬ a f₂ t ≤
    collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
⊢ collapse 𝒜 a f₁ s * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
rw [collapse_eq has]

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
pos :
  s ∈ 𝒜 →
    insert a s ∈ 𝒜 →
      (f₁ s + f₁ (insert a s)) * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
neg :
  s ∈ 𝒜 →
    insert a s ∉ 𝒜 → (f₁ s + 0) * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
pos₁ :
  s ∉ 𝒜 →
    insert a s ∈ 𝒜 →
      (0 + f₁ (insert a s)) * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
neg₁ :
  s ∉ 𝒜 →
    insert a s ∉ 𝒜 →
      HAdd.hAdd (α := β) 0 0 * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
⊢ ((if s ∈ 𝒜 then f₁ s else 0) + if insert a s ∈ 𝒜 then f₁ (insert a s) else 0) * collapse ℬ a f₂ t ≤
    collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
split_ifs