awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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) * 0 + f₁ (insert a s) * f₂ (insert a t) ≤
    collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
have pos : f₁ (insert a s) * f₂ (insert a t) ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
Tactic: rw [mul_zero, zero_add]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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) * 0 + f₁ (insert a s) * 0 ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
have neg : 0 ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
Tactic: simp_rw [mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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 ∉ 𝒜
⊢ HAdd.hAdd (α := β) 0 0 * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
have neg : 0 ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
Tactic: simp_rw [add_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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) (∑ s ∈ 𝒜, f s)
have calc_1 : ∑ s ∈ u.powerset, collapse 𝒜 a f s =
  HAdd.hAdd (α := β) (∑ s ∈ u.powerset ∩ 𝒜, f s) (∑ s ∈ image (insert a) u.powerset ∩ 𝒜, 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 := ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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)
⊢ Eq.{u_2 + 1} (α := β) (∑ s ∈ u.powerset, collapse 𝒜 a f s) (∑ s ∈ 𝒜, f s)
have 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)
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 := ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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)
⊢ Eq.{u_2 + 1} (α := β) (∑ s ∈ u.powerset, collapse 𝒜 a f s) (∑ s ∈ 𝒜, f s)
have calc_3 : HAdd.hAdd (α := β) (∑ s ∈ u.powerset ∩ 𝒜, f s) (∑ s ∈ (insert a u).powerset \ u.powerset ∩ 𝒜, 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 := ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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)
have 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))
Tactic: rw [← Finset.sum_ite_mem, ← Finset.sum_ite_mem, sum_image, ← sum_add_distrib]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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))
⊢ ∑ s ∈ u.powerset, collapse 𝒜 a f s =
    HAdd.hAdd (α := β) (∑ s ∈ u.powerset ∩ 𝒜, f s) (∑ s ∈ image (insert a) u.powerset ∩ 𝒜, f s)
have calc_1₁ : Set.InjOn (insert a) (↑u.powerset : Set (Finset α))
Tactic: rw [← Finset.sum_ite_mem, ← Finset.sum_ite_mem, sum_image, ← sum_add_distrib]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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)
have calc_2 : ∀ (s : Finset α), s ∈ image (insert a) u.powerset ↔ s ∈ (insert a u).powerset \ u.powerset
Tactic: congr with s
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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 α
⊢ s ∈ image (insert a) u.powerset ↔ s ∈ (insert a u).powerset \ u.powerset
have calc_2 : (∃ a_1 ⊆ u, insert a a_1 = s) ↔ s.erase a ⊆ u ∧ ¬s ⊆ u
Tactic: simp only [mem_image, mem_powerset, mem_sdiff, subset_insert_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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
have calc_2 : (∃ a_1 ⊆ u, insert a a_1 = s) → s.erase a ⊆ u ∧ ¬s ⊆ u
Tactic: refine ⟨?_, fun h ↦ ⟨_, h.1, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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
⊢ (∃ a_1 ⊆ u, insert a a_1 = s) ↔ s.erase a ⊆ u ∧ ¬s ⊆ u
have calc_2₁ : ∀ (h : s.erase a ⊆ u ∧ ¬s ⊆ u), insert a (s.erase a) = s
Tactic: refine ⟨?_, fun h ↦ ⟨_, h.1, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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
⊢ insert a (s.erase a) = s
have rw : ∀ (hs : s.erase a = s), False
Tactic: rw [insert_erase (erase_ne_self.1 fun hs ↦ ?_)]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (hypothesis)
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
⊢ False
have h₁ : s ⊆ u ∧ ¬s ⊆ u
Tactic: rw [hs] at h
Cleared hypotheses: h, hs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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
have calc_3 : Eq.{u_2 + 1} (α := β) (∑ x ∈ u.powerset ∩ 𝒜 ∪ (insert a u).powerset \ u.powerset ∩ 𝒜, f x) (∑ 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𝒜]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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)
⊢ HAdd.hAdd (α := β) (∑ s ∈ u.powerset ∩ 𝒜, f s) (∑ s ∈ (insert a u).powerset \ u.powerset ∩ 𝒜, f s) = ∑ s ∈ 𝒜, f s
have calc_3₁ : Eq.{u_2 + 1} (α := β) (∑ x ∈ (u.powerset ∪ (insert a u).powerset \ u.powerset) ∩ 𝒜, f x) (∑ 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𝒜]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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)
⊢ HAdd.hAdd (α := β) (∑ s ∈ u.powerset ∩ 𝒜, f s) (∑ s ∈ (insert a u).powerset \ u.powerset ∩ 𝒜, f s) = ∑ s ∈ 𝒜, f s
have calc_3₂ : Eq.{u_2 + 1} (α := β) (∑ x ∈ (insert a u).powerset ∩ 𝒜, f x) (∑ 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𝒜]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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)
⊢ HAdd.hAdd (α := β) (∑ s ∈ u.powerset ∩ 𝒜, f s) (∑ s ∈ (insert a u).powerset \ u.powerset ∩ 𝒜, f s) = ∑ s ∈ 𝒜, f s
have calc_3₃ : Eq.{u_2 + 1} (α := β) (∑ x ∈ 𝒜, f x) (∑ 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𝒜]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (hypothesis)
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 ∅
⊢ HMul.hMul (α := β) (∑ s ∈ 𝒜, f₁ s) (∑ s ∈ ℬ, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) (∑ s ∈ 𝒜 ⊻ ℬ, f₄ s)
have h𝒜₁ : 𝒜 = ∅ ∨ 𝒜 = {∅}
Tactic: simp only [Finset.powerset_empty, Finset.subset_singleton_iff] at h𝒜 hℬ
Cleared hypotheses: h𝒜, hℬ
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (hypothesis)
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𝒜₁ : 𝒜 = ∅ ∨ 𝒜 = {∅}
⊢ HMul.hMul (α := β) (∑ s ∈ 𝒜, f₁ s) (∑ s ∈ ℬ, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) (∑ s ∈ 𝒜 ⊻ ℬ, f₄ s)
have hℬ₁ : ℬ = ∅ ∨ ℬ = {∅}
Tactic: simp only [Finset.powerset_empty, Finset.subset_singleton_iff] at h𝒜 hℬ
Cleared hypotheses: h𝒜, hℬ
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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ℬ : ℬ = ∅ ∨ ℬ = {∅}
⊢ HMul.hMul (α := β) (∑ s ∈ 𝒜, f₁ s) (∑ s ∈ ℬ, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) (∑ s ∈ 𝒜 ⊻ ℬ, f₄ s)
have empty : HMul.hMul (α := β) (∑ s ∈ ∅, f₁ s) (∑ s ∈ ℬ, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ ∅ ⊼ ℬ, f₃ s) (∑ s ∈ ∅ ⊻ ℬ, f₄ s)
Tactic: obtain rfl | rfl := h𝒜
Cleared hypotheses: 𝒜, h𝒜
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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)
⊢ HMul.hMul (α := β) (∑ s ∈ 𝒜, f₁ s) (∑ s ∈ ℬ, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) (∑ s ∈ 𝒜 ⊻ ℬ, f₄ s)
have empty₁ : HMul.hMul (α := β) (∑ s ∈ {∅}, f₁ s) (∑ s ∈ ℬ, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ {∅} ⊼ ℬ, f₃ s) (∑ s ∈ {∅} ⊻ ℬ, f₄ s)
Tactic: obtain rfl | rfl := h𝒜
Cleared hypotheses: 𝒜, h𝒜
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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ℬ : ℬ = ∅ ∨ ℬ = {∅}
⊢ HMul.hMul (α := β) (∑ s ∈ ∅, f₁ s) (∑ s ∈ ℬ, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ ∅ ⊼ ℬ, f₃ s) (∑ s ∈ ∅ ⊻ ℬ, f₄ s)
have empty : HMul.hMul (α := β) (∑ s ∈ ∅, f₁ s) (∑ s ∈ ∅, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ ∅ ⊼ ∅, f₃ s) (∑ s ∈ ∅ ⊻ ∅, f₄ s)
Tactic: obtain rfl | rfl := hℬ
Cleared hypotheses: ℬ, hℬ
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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)
⊢ HMul.hMul (α := β) (∑ s ∈ ∅, f₁ s) (∑ s ∈ ℬ, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ ∅ ⊼ ℬ, f₃ s) (∑ s ∈ ∅ ⊻ ℬ, f₄ s)
have empty₁ : HMul.hMul (α := β) (∑ s ∈ ∅, f₁ s) (∑ s ∈ {∅}, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ ∅ ⊼ {∅}, f₃ s) (∑ s ∈ ∅ ⊻ {∅}, f₄ s)
Tactic: obtain rfl | rfl := hℬ
Cleared hypotheses: ℬ, hℬ
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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ℬ : ℬ = ∅ ∨ ℬ = {∅}
⊢ HMul.hMul (α := β) (∑ s ∈ {∅}, f₁ s) (∑ s ∈ ℬ, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ {∅} ⊼ ℬ, f₃ s) (∑ s ∈ {∅} ⊻ ℬ, f₄ s)
have empty : HMul.hMul (α := β) (∑ s ∈ {∅}, f₁ s) (∑ s ∈ ∅, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ {∅} ⊼ ∅, f₃ s) (∑ s ∈ {∅} ⊻ ∅, f₄ s)
Tactic: obtain rfl | rfl := hℬ
Cleared hypotheses: ℬ, hℬ
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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)
⊢ HMul.hMul (α := β) (∑ s ∈ {∅}, f₁ s) (∑ s ∈ ℬ, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ {∅} ⊼ ℬ, f₃ s) (∑ s ∈ {∅} ⊻ ℬ, f₄ s)
have empty₁ : HMul.hMul (α := β) (∑ s ∈ {∅}, f₁ s) (∑ s ∈ {∅}, f₂ s) ≤
  HMul.hMul (α := β) (∑ s ∈ {∅} ⊼ {∅}, f₃ s) (∑ s ∈ {∅} ⊻ {∅}, f₄ s)
Tactic: obtain rfl | rfl := hℬ
Cleared hypotheses: ℬ, hℬ
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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)
have empty : f₁ ∅ * f₂ ∅ ≤ f₃ ∅ * f₄ ∅
Tactic: simp
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (hypothesis)
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 ∈ 𝒜, f₁ s) (∑ s ∈ ℬ, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) (∑ s ∈ 𝒜 ⊻ ℬ, f₄ s)
have 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)
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
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (hypothesis)
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)
⊢ HMul.hMul (α := β) (∑ s ∈ 𝒜, f₁ s) (∑ s ∈ ℬ, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) (∑ s ∈ 𝒜 ⊻ ℬ, f₄ s)
have this : 𝒜 ⊼ ℬ ⊆ (insert a u).powerset
Tactic: have : 𝒜 ⊼ ℬ ⊆ powerset (insert a u) := by simpa using infs_subset h𝒜 hℬ
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (hypothesis)
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
⊢ HMul.hMul (α := β) (∑ s ∈ 𝒜, f₁ s) (∑ s ∈ ℬ, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) (∑ s ∈ 𝒜 ⊻ ℬ, f₄ s)
have this₁ : 𝒜 ⊻ ℬ ⊆ (insert a u).powerset
Tactic: have : 𝒜 ⊻ ℬ ⊆ powerset (insert a u) := by simpa using sups_subset h𝒜 hℬ