-- Mathlib/Combinatorics/SetFamily/FourFunctions.lean
/-- The **Four Functions Theorem** on a powerset algebra. See `four_functions_theorem` for the
finite distributive lattice generalisation. -/
protected lemma Finset.four_functions_theorem (u : Finset α)
    (h₁ : 0 ≤ f₁) (h₂ : 0 ≤ f₂) (h₃ : 0 ≤ f₃) (h₄ : 0 ≤ f₄)
    (h : ∀ ⦃s⦄, s ⊆ u → ∀ ⦃t⦄, t ⊆ u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t))
    {𝒜 ℬ : Finset (Finset α)} (h𝒜 : 𝒜 ⊆ u.powerset) (hℬ : ℬ ⊆ u.powerset) :
    (∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) * ∑ s ∈ 𝒜 ⊻ ℬ, f₄ s

Proof state:
case insert
α : Type u_1
β : Type u_2
inst✝² : DecidableEq α
inst✝¹ : LinearOrderedCommSemiring β
inst✝ : ExistsAddOfLE β
a✝ : α
s✝ : Finset α
hu : a✝ ∉ s✝
ih :
  ∀ {f₁ f₂ f₃ f₄ : Finset α → β},
    0 ≤ f₁ →
      0 ≤ f₂ →
        0 ≤ f₃ →
          0 ≤ f₄ →
            (∀ ⦃s : Finset α⦄, s ⊆ s✝ → ∀ ⦃t : Finset α⦄, t ⊆ s✝ → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)) →
              ∀ {𝒜 ℬ : Finset (Finset α)},
                𝒜 ⊆ s✝.powerset →
                  ℬ ⊆ s✝.powerset → (∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ 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✝ s✝ → ∀ ⦃t : Finset α⦄, t ⊆ insert a✝ s✝ → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
h𝒜 : 𝒜 ⊆ (insert a✝ s✝).powerset
hℬ : ℬ ⊆ (insert a✝ s✝).powerset
⊢ (∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) * ∑ s ∈ 𝒜 ⊻ ℬ, f₄ s

Tactic:
rename_i a u

Result:
case insert
α : Type u_1
β : Type u_2
inst✝² : DecidableEq α
inst✝¹ : LinearOrderedCommSemiring β
inst✝ : ExistsAddOfLE β
a : α
u : Finset α
hu : a ∉ u
ih :
  ∀ {f₁ f₂ f₃ f₄ : Finset α → β},
    0 ≤ f₁ →
      0 ≤ f₂ →
        0 ≤ f₃ →
          0 ≤ f₄ →
            (∀ ⦃s : Finset α⦄, s ⊆ u → ∀ ⦃t : Finset α⦄, t ⊆ u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)) →
              ∀ {𝒜 ℬ : Finset (Finset α)},
                𝒜 ⊆ u.powerset →
                  ℬ ⊆ u.powerset → (∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ 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
⊢ (∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) * ∑ s ∈ 𝒜 ⊻ ℬ, f₄ s

Proof state:
α : Type u_1
β : Type u_2
inst✝² : DecidableEq α
inst✝¹ : LinearOrderedCommSemiring β
f₁ f₂ f₃ f₄ : Finset α → β
inst✝ : ExistsAddOfLE β
u : 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
⊢ (∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) * ∑ s ∈ 𝒜 ⊻ ℬ, f₄ s

Tactic:
induction u using Finset.induction generalizing f₁ f₂ f₃ f₄ 𝒜 ℬ with
| empty =>
  simp only [Finset.powerset_empty, Finset.subset_singleton_iff] at h𝒜 hℬ
  obtain rfl | rfl := h𝒜 <;> obtain rfl | rfl := hℬ <;> simp; exact h (subset_refl ∅) subset_rfl
| insert hu ih =>
  rename_i a u
  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
  have : 𝒜 ⊼ ℬ ⊆ powerset (insert a u) := by simpa using infs_subset h𝒜 hℬ
  have : 𝒜 ⊻ ℬ ⊆ powerset (insert a u) := by simpa using sups_subset h𝒜 hℬ
  simpa only [powerset_sups_powerset_self, powerset_infs_powerset_self, sum_collapse,
    not_false_eq_true, *] using ih

Result:
no goals

Proof state:
case insert
α : Type u_1
β : Type u_2
inst✝² : DecidableEq α
inst✝¹ : LinearOrderedCommSemiring β
inst✝ : ExistsAddOfLE β
a : α
u : Finset α
hu : a ∉ u
ih :
  ∀ {f₁ f₂ f₃ f₄ : Finset α → β},
    0 ≤ f₁ →
      0 ≤ f₂ →
        0 ≤ f₃ →
          0 ≤ f₄ →
            (∀ ⦃s : Finset α⦄, s ⊆ u → ∀ ⦃t : Finset α⦄, t ⊆ u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)) →
              ∀ {𝒜 ℬ : Finset (Finset α)},
                𝒜 ⊆ u.powerset →
                  ℬ ⊆ u.powerset → (∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ 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
⊢ (∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) * ∑ s ∈ 𝒜 ⊻ ℬ, 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

Result:
case insert
α : Type u_1
β : Type u_2
inst✝² : DecidableEq α
inst✝¹ : LinearOrderedCommSemiring β
inst✝ : 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 :
  (∑ s ∈ u.powerset, collapse 𝒜 a f₁ s) * ∑ s ∈ u.powerset, collapse ℬ a f₂ s ≤
    (∑ s ∈ u.powerset ⊼ u.powerset, collapse (𝒜 ⊼ ℬ) a f₃ s) * ∑ s ∈ u.powerset ⊻ u.powerset, collapse (𝒜 ⊻ ℬ) a f₄ s
⊢ (∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) * ∑ s ∈ 𝒜 ⊻ ℬ, f₄ s

Proof state:
case empty.inr.inr
α : Type u_1
β : Type u_2
inst✝² : DecidableEq α
inst✝¹ : LinearOrderedCommSemiring β
inst✝ : 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

Result:
no goals