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 β
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_1 : 𝒜 ⊼ ℬ ⊆ (insert a u).powerset
this : 𝒜 ⊻ ℬ ⊆ (insert a u).powerset
⊢ HMul.hMul (α := β) (∑ s ∈ 𝒜, f₁ s) (∑ s ∈ ℬ, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) (∑ s ∈ 𝒜 ⊻ ℬ, f₄ s)

Tactic:
simpa only [powerset_sups_powerset_self, powerset_infs_powerset_self, sum_collapse,
      not_false_eq_true, *] using ih

Premises used: sum_collapse, Finset.powerset_sups_powerset_self, Finset.powerset_infs_powerset_self, not_false_eq_true
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
f₁ f₂ f₃ f₄ : Finset α → β
inst_4 : 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
empty :
  ∀ {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)
insert :
  ∀ (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.insert a u → ∀ ⦃t : Finset α⦄, t ⊆ Insert.insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t))
    {𝒜 ℬ : Finset (Finset α)} (h𝒜 : 𝒜 ⊆ (Insert.insert a u).powerset) (hℬ : ℬ ⊆ (Insert.insert a u).powerset),
    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:
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 a u hu ih =>
    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

Premises used: sum_collapse, Finset.powerset_sups_powerset_self, Finset.powerset_infs_powerset_self, Insert.insert, Finset.subset_singleton_iff, Finset.powerset_empty, not_false_eq_true, subset_rfl, rfl
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
f₁ f₂ f₃ f₄ : Finset α → β
inst_4 : ExistsAddOfLE β
inst_5 : Finite α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (s t : Finset α), f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
have :
  ∀ (this : Fintype α),
    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:
have := Fintype.ofFinite α
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
f₁ f₂ f₃ f₄ : Finset α → β
inst_4 : ExistsAddOfLE β
inst_5 : Finite α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (s t : Finset α), f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
this : Fintype α
⊢ HMul.hMul (α := β) (∑ s ∈ 𝒜, f₁ s) (∑ s ∈ ℬ, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) (∑ s ∈ 𝒜 ⊻ ℬ, f₄ s)

Tactic:
univ.four_functions_theorem h₁ h₂ h₃ h₄ ?_ ?_ ?_

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

Tactic:
refine univ.four_functions_theorem h₁ h₂ h₃ h₄ ?_ ?_ ?_

Premises used: Finset.univ, Finset.four_functions_theorem
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
f₁ f₂ f₃ f₄ : Finset α → β
inst_4 : ExistsAddOfLE β
inst_5 : Finite α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (s t : Finset α), f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
this : Fintype α
⊢ ∀ ⦃s : Finset α⦄, s ⊆ univ → ∀ ⦃t : Finset α⦄, t ⊆ univ → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
f₁ f₂ f₃ f₄ : Finset α → β
inst_4 : ExistsAddOfLE β
inst_5 : Finite α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (s t : Finset α), f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
this : Fintype α
⊢ 𝒜 ⊆ powerset univ

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
f₁ f₂ f₃ f₄ : Finset α → β
inst_4 : ExistsAddOfLE β
inst_5 : Finite α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (s t : Finset α), f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
this : Fintype α
⊢ ℬ ⊆ powerset univ

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DistribLattice α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : α → β
inst_5 : DecidableEq α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
s t : Finset α
L : Sublattice α :=
  { carrier := (latticeClosure : (a : Set α) → Set α) ((↑s : Set α) ∪ (↑t : Set α)), supClosed' := ⋯, infClosed' := ⋯ }
⊢ Finite.{u_1 + 1} ↥L

Tactic:
have : Finite L := (s.finite_toSet.union t.finite_toSet).latticeClosure.to_subtype
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DistribLattice α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : α → β
inst_5 : DecidableEq α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
s t : Finset α
L : Sublattice α :=
  { carrier := (latticeClosure : (a : Set α) → Set α) ((↑s : Set α) ∪ (↑t : Set α)), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite.{u_1 + 1} ↥L
s' : Finset ↥L := s.preimage (Subtype.val (p := fun (x : α) ↦ x ∈ L)) ⋯
t' : Finset ↥L := t.preimage (Subtype.val (p := fun (x : α) ↦ x ∈ L)) ⋯
⊢ map { toFun := (⇑L.subtype : (a : ↥L) → α), inj' := ⋯ : ↥L ↪ α } s' = s

Tactic:
simpa [s', map_eq_image, image_preimage, filter_eq_self] using
      fun a ha ↦ subset_latticeClosure <| Set.subset_union_left ha

Premises used: Finset.filter_eq_self, subset_latticeClosure, Set.subset_union_left, Finset.image_preimage, Finset.map_eq_image
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DistribLattice α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : α → β
inst_5 : DecidableEq α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
s t : Finset α
L : Sublattice α :=
  { carrier := (latticeClosure : (a : Set α) → Set α) ((↑s : Set α) ∪ (↑t : Set α)), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite.{u_1 + 1} ↥L
s' : Finset ↥L := s.preimage (Subtype.val (p := fun (x : α) ↦ x ∈ L)) ⋯
t' : Finset ↥L := t.preimage (Subtype.val (p := fun (x : α) ↦ x ∈ L)) ⋯
⊢ map { toFun := (⇑L.subtype : (a : ↥L) → α), inj' := ⋯ : ↥L ↪ α } s' = s

Tactic:
have hs' : s'.map ⟨L.subtype, Subtype.coe_injective⟩ = s := by
    simpa [s', map_eq_image, image_preimage, filter_eq_self] using
      fun a ha ↦ subset_latticeClosure <| Set.subset_union_left ha
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DistribLattice α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : α → β
inst_5 : DecidableEq α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
s t : Finset α
L : Sublattice α :=
  { carrier := (latticeClosure : (a : Set α) → Set α) ((↑s : Set α) ∪ (↑t : Set α)), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite.{u_1 + 1} ↥L
s' : Finset ↥L := s.preimage (Subtype.val (p := fun (x : α) ↦ x ∈ L)) ⋯
t' : Finset ↥L := t.preimage (Subtype.val (p := fun (x : α) ↦ x ∈ L)) ⋯
hs' : map { toFun := (⇑L.subtype : (a : ↥L) → α), inj' := ⋯ : ↥L ↪ α } s' = s
⊢ map { toFun := (⇑L.subtype : (a : ↥L) → α), inj' := ⋯ : ↥L ↪ α } t' = t

Tactic:
simpa [t', map_eq_image, image_preimage, filter_eq_self] using
      fun a ha ↦ subset_latticeClosure <| Set.subset_union_right ha

Premises used: Set.subset_union_right, Finset.filter_eq_self, subset_latticeClosure, Finset.image_preimage, Finset.map_eq_image
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DistribLattice α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : α → β
inst_5 : DecidableEq α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
s t : Finset α
L : Sublattice α :=
  { carrier := (latticeClosure : (a : Set α) → Set α) ((↑s : Set α) ∪ (↑t : Set α)), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite.{u_1 + 1} ↥L
s' : Finset ↥L := s.preimage (Subtype.val (p := fun (x : α) ↦ x ∈ L)) ⋯
t' : Finset ↥L := t.preimage (Subtype.val (p := fun (x : α) ↦ x ∈ L)) ⋯
hs' : map { toFun := (⇑L.subtype : (a : ↥L) → α), inj' := ⋯ : ↥L ↪ α } s' = s
⊢ map { toFun := (⇑L.subtype : (a : ↥L) → α), inj' := ⋯ : ↥L ↪ α } t' = t

Tactic:
have ht' : t'.map ⟨L.subtype, Subtype.coe_injective⟩ = t := by
    simpa [t', map_eq_image, image_preimage, filter_eq_self] using
      fun a ha ↦ subset_latticeClosure <| Set.subset_union_right ha
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DistribLattice α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : α → β
inst_5 : DecidableEq α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
s t : Finset α
L : Sublattice α :=
  { carrier := (latticeClosure : (a : Set α) → Set α) ((↑s : Set α) ∪ (↑t : Set α)), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite.{u_1 + 1} ↥L
s' : Finset ↥L := s.preimage (Subtype.val (p := fun (x : α) ↦ x ∈ L)) ⋯
t' : Finset ↥L := t.preimage (Subtype.val (p := fun (x : α) ↦ x ∈ L)) ⋯
hs' : map { toFun := (⇑L.subtype : (a : ↥L) → α), inj' := ⋯ : ↥L ↪ α } s' = s
ht' : map { toFun := (⇑L.subtype : (a : ↥L) → α), inj' := ⋯ : ↥L ↪ α } t' = t
clear_value :
  ∀ (s' t' : Finset ↥L) (hs' : map { toFun := (⇑L.subtype : (a : ↥L) → α), inj' := ⋯ : ↥L ↪ α } s' = s)
    (ht' : map { toFun := (⇑L.subtype : (a : ↥L) → α), inj' := ⋯ : ↥L ↪ α } t' = t),
    HMul.hMul (α := β) (∑ a ∈ s, f₁ a) (∑ a ∈ t, f₂ a) ≤ HMul.hMul (α := β) (∑ a ∈ s ⊼ t, f₃ a) (∑ a ∈ s ⊻ t, f₄ a)
⊢ HMul.hMul (α := β) (∑ a ∈ s, f₁ a) (∑ a ∈ t, f₂ a) ≤ HMul.hMul (α := β) (∑ a ∈ s ⊼ t, f₃ a) (∑ a ∈ s ⊻ t, f₄ a)

Tactic:
clear_value s' t'
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β : Type u_2
inst : DistribLattice α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : α → β
inst_5 : DecidableEq α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
s t : Finset α
L : Sublattice α :=
  { carrier := (latticeClosure : (a : Set α) → Set α) ((↑s : Set α) ∪ (↑t : Set α)), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite.{u_1 + 1} ↥L
s' t' : Finset ↥L
hs' : map { toFun := (⇑L.subtype : (a : ↥L) → α), inj' := ⋯ : ↥L ↪ α } s' = s
ht' : map { toFun := (⇑L.subtype : (a : ↥L) → α), inj' := ⋯ : ↥L ↪ α } t' = t
obtain :
  ∀ (β_1 : Type u_1) (w : DecidableEq β_1) (w_1 : Fintype β_1) (g : LatticeHom (↥L) (Finset β_1))
    (hg : Injective (α := ↥L) (β := Finset β_1) (⇑g : (a : ↥L) → Finset β_1)),
    HMul.hMul (α := β) (∑ a ∈ s, f₁ a) (∑ a ∈ t, f₂ a) ≤ HMul.hMul (α := β) (∑ a ∈ s ⊼ t, f₃ a) (∑ a ∈ s ⊻ t, f₄ a)
⊢ HMul.hMul (α := β) (∑ a ∈ s, f₁ a) (∑ a ∈ t, f₂ a) ≤ HMul.hMul (α := β) (∑ a ∈ s ⊼ t, f₃ a) (∑ a ∈ s ⊻ t, f₄ a)

Tactic:
obtain ⟨β, _, _, g, hg⟩ := exists_birkhoff_representation L

Premises used: exists_birkhoff_representation, Membership.mem, Subtype
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β_1 : Type u_2
inst : DistribLattice α
inst_1 : CommSemiring β_1
inst_2 : LinearOrder β_1
inst_3 : IsStrictOrderedRing β_1
inst_4 : ExistsAddOfLE β_1
f₁ f₂ f₃ f₄ : α → β_1
inst_5 : DecidableEq α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
s t : Finset α
L : Sublattice α :=
  { carrier := (latticeClosure : (a : Set α) → Set α) ((↑s : Set α) ∪ (↑t : Set α)), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite.{u_1 + 1} ↥L
s' t' : Finset ↥L
hs' : map { toFun := (⇑L.subtype : (a : ↥L) → α), inj' := ⋯ : ↥L ↪ α } s' = s
ht' : map { toFun := (⇑L.subtype : (a : ↥L) → α), inj' := ⋯ : ↥L ↪ α } t' = t
β : Type u_1
w : DecidableEq β
w_1 : Fintype β
g : LatticeHom (↥L) (Finset β)
hg : Injective (α := ↥L) (β := Finset β) (⇑g : (a : ↥L) → Finset β)
refine_2 :
  ∀
    (this :
      HMul.hMul (α := β_1)
          (∑ s ∈ map { toFun := (⇑g : (a : ↥L) → Finset β), inj' := hg : ↥L ↪ Finset β } s',
            extend (α := ↥L) (⇑g : (a : ↥L) → Finset β) (f₁ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) 0 s)
          (∑ s ∈ map { toFun := (⇑g : (a : ↥L) → Finset β), inj' := hg : ↥L ↪ Finset β } t',
            extend (α := ↥L) (⇑g : (a : ↥L) → Finset β) (f₂ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) 0 s) ≤
        HMul.hMul (α := β_1)
          (∑
            s ∈
              map { toFun := (⇑g : (a : ↥L) → Finset β), inj' := hg : ↥L ↪ Finset β } s' ⊼
                map { toFun := (⇑g : (a : ↥L) → Finset β), inj' := hg : ↥L ↪ Finset β } t',
            extend (α := ↥L) (⇑g : (a : ↥L) → Finset β) (f₃ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) 0 s)
          (∑
            s ∈
              map { toFun := (⇑g : (a : ↥L) → Finset β), inj' := hg : ↥L ↪ Finset β } s' ⊻
                map { toFun := (⇑g : (a : ↥L) → Finset β), inj' := hg : ↥L ↪ Finset β } t',
            extend (α := ↥L) (⇑g : (a : ↥L) → Finset β) (f₄ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) 0 s)),
    HMul.hMul (α := β_1) (∑ a ∈ s, f₁ a) (∑ a ∈ t, f₂ a) ≤ HMul.hMul (α := β_1) (∑ a ∈ s ⊼ t, f₃ a) (∑ a ∈ s ⊻ t, f₄ a)
refine_1 :
  ∀ (s t : Finset β),
    extend (α := ↥L) (⇑g : (a : ↥L) → Finset β) (f₁ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) 0 s *
        extend (α := ↥L) (⇑g : (a : ↥L) → Finset β) (f₂ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) 0 t ≤
      extend (α := ↥L) (⇑g : (a : ↥L) → Finset β) (f₃ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) 0 (s ∩ t) *
        extend (α := ↥L) (⇑g : (a : ↥L) → Finset β) (f₄ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) 0 (s ∪ t)
⊢ HMul.hMul (α := β_1) (∑ a ∈ s, f₁ a) (∑ a ∈ t, f₂ a) ≤ HMul.hMul (α := β_1) (∑ a ∈ s ⊼ t, f₃ a) (∑ a ∈ s ⊻ t, f₄ a)

Tactic:
have := four_functions_theorem_aux (extend g (f₁ ∘ (↑)) 0) (extend g (f₂ ∘ (↑)) 0)
    (extend g (f₃ ∘ (↑)) 0) (extend g (f₄ ∘ (↑)) 0) (extend_nonneg (fun _ ↦ h₁ _) le_rfl)
    (extend_nonneg (fun _ ↦ h₂ _) le_rfl) (extend_nonneg (fun _ ↦ h₃ _) le_rfl)
    (extend_nonneg (fun _ ↦ h₄ _) le_rfl) ?_ (s'.map ⟨g, hg⟩) (t'.map ⟨g, hg⟩)
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β_1 : Type u_2
inst : DistribLattice α
inst_1 : CommSemiring β_1
inst_2 : LinearOrder β_1
inst_3 : IsStrictOrderedRing β_1
inst_4 : ExistsAddOfLE β_1
f₁ f₂ f₃ f₄ : α → β_1
inst_5 : DecidableEq α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
s t : Finset α
L : Sublattice α :=
  { carrier := (latticeClosure : (a : Set α) → Set α) ((↑s : Set α) ∪ (↑t : Set α)), supClosed' := ⋯, infClosed' := ⋯ }
this_1 : Finite.{u_1 + 1} ↥L
s' t' : Finset ↥L
hs' : map { toFun := (⇑L.subtype : (a : ↥L) → α), inj' := ⋯ : ↥L ↪ α } s' = s
ht' : map { toFun := (⇑L.subtype : (a : ↥L) → α), inj' := ⋯ : ↥L ↪ α } t' = t
β : Type u_1
w : DecidableEq β
w_1 : Fintype β
g : LatticeHom (↥L) (Finset β)
hg : Injective (α := ↥L) (β := Finset β) (⇑g : (a : ↥L) → Finset β)
this :
  HMul.hMul (α := β_1)
      (∑ s ∈ map { toFun := (⇑g : (a : ↥L) → Finset β), inj' := hg : ↥L ↪ Finset β } s',
        extend (α := ↥L) (⇑g : (a : ↥L) → Finset β) (f₁ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) 0 s)
      (∑ s ∈ map { toFun := (⇑g : (a : ↥L) → Finset β), inj' := hg : ↥L ↪ Finset β } t',
        extend (α := ↥L) (⇑g : (a : ↥L) → Finset β) (f₂ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) 0 s) ≤
    HMul.hMul (α := β_1)
      (∑
        s ∈
          map { toFun := (⇑g : (a : ↥L) → Finset β), inj' := hg : ↥L ↪ Finset β } s' ⊼
            map { toFun := (⇑g : (a : ↥L) → Finset β), inj' := hg : ↥L ↪ Finset β } t',
        extend (α := ↥L) (⇑g : (a : ↥L) → Finset β) (f₃ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) 0 s)
      (∑
        s ∈
          map { toFun := (⇑g : (a : ↥L) → Finset β), inj' := hg : ↥L ↪ Finset β } s' ⊻
            map { toFun := (⇑g : (a : ↥L) → Finset β), inj' := hg : ↥L ↪ Finset β } t',
        extend (α := ↥L) (⇑g : (a : ↥L) → Finset β) (f₄ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) 0 s)
⊢ HMul.hMul (α := β_1) (∑ a ∈ s, f₁ a) (∑ a ∈ t, f₂ a) ≤ HMul.hMul (α := β_1) (∑ a ∈ s ⊼ t, f₃ a) (∑ a ∈ s ⊻ t, f₄ a)

Tactic:
simpa only [← hs', ← ht', ← map_sups, ← map_infs, sum_map, Embedding.coeFn_mk, hg.extend_apply]
      using this

Premises used: Finset.sum_map, Function.Injective.extend_apply, Finset.map_sups, Function.Embedding.coeFn_mk, Finset.map_infs
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β_1 : Type u_2
inst : DistribLattice α
inst_1 : CommSemiring β_1
inst_2 : LinearOrder β_1
inst_3 : IsStrictOrderedRing β_1
inst_4 : ExistsAddOfLE β_1
f₁ f₂ f₃ f₄ : α → β_1
inst_5 : DecidableEq α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
s_1 t_1 : Finset α
L : Sublattice α :=
  { carrier := (latticeClosure : (a : Set α) → Set α) ((↑s_1 : Set α) ∪ (↑t_1 : Set α)), supClosed' := ⋯,
    infClosed' := ⋯ }
this : Finite.{u_1 + 1} ↥L
s' t' : Finset ↥L
hs' : map { toFun := (⇑L.subtype : (a : ↥L) → α), inj' := ⋯ : ↥L ↪ α } s' = s_1
ht' : map { toFun := (⇑L.subtype : (a : ↥L) → α), inj' := ⋯ : ↥L ↪ α } t' = t_1
β : Type u_1
w : DecidableEq β
w_1 : Fintype β
g : LatticeHom (↥L) (Finset β)
hg : Injective (α := ↥L) (β := Finset β) (⇑g : (a : ↥L) → Finset β)
s t : Finset β
refine_1 :
  ∀ (a : ↥L),
    extend (α := ↥L) (β := Finset β) ((⇑g : (a : ↥L) → Finset β) : (a : ↥L) → Finset β)
          (f₁ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) (0 : Finset β → β_1) ((g : (a : ↥L) → Finset β) a : Finset β) *
        extend (α := ↥L) (⇑g : (a : ↥L) → Finset β) (f₂ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) 0 t ≤
      extend (α := ↥L) (β := Finset β) ((⇑g : (a : ↥L) → Finset β) : (a : ↥L) → Finset β)
          (f₃ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) (0 : Finset β → β_1)
          ((g : (a : ↥L) → Finset β) a ∩ t : Finset β) *
        extend (α := ↥L) (β := Finset β) ((⇑g : (a : ↥L) → Finset β) : (a : ↥L) → Finset β)
          (f₄ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) (0 : Finset β → β_1)
          ((g : (a : ↥L) → Finset β) a ∪ t : Finset β)
refine_1₁ :
  ∀ (hs : ¬∃ (a : ↥L), (g : (a : ↥L) → Finset β) a = s),
    extend (α := ↥L) (⇑g : (a : ↥L) → Finset β) (f₁ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) 0 s *
        extend (α := ↥L) (⇑g : (a : ↥L) → Finset β) (f₂ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) 0 t ≤
      extend (α := ↥L) (⇑g : (a : ↥L) → Finset β) (f₃ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) 0 (s ∩ t) *
        extend (α := ↥L) (⇑g : (a : ↥L) → Finset β) (f₄ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) 0 (s ∪ t)
⊢ extend (α := ↥L) (⇑g : (a : ↥L) → Finset β) (f₁ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) 0 s *
      extend (α := ↥L) (⇑g : (a : ↥L) → Finset β) (f₂ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) 0 t ≤
    extend (α := ↥L) (⇑g : (a : ↥L) → Finset β) (f₃ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) 0 (s ∩ t) *
      extend (α := ↥L) (⇑g : (a : ↥L) → Finset β) (f₄ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) 0 (s ∪ t)

Tactic:
obtain ⟨a, rfl⟩ | hs := em (∃ a, g a = s)

Premises used: Exists, em, Eq, DFunLike.coe, rfl