awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 β)
a b : ↥L
refine_1 :
  (f₁ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) a * (f₂ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) b ≤
    (f₃ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) (a ⊓ b) * (f₄ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) (a ⊔ b)
⊢ 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) (β := Finset β) ((⇑g : (a : ↥L) → Finset β) : (a : ↥L) → Finset β)
        (f₂ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) (0 : Finset β → β_1) ((g : (a : ↥L) → Finset β) b : 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 ∩ (g : (a : ↥L) → Finset β) b : 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 ∪ (g : (a : ↥L) → Finset β) b : Finset β)

Tactic:
simp_rw [← sup_eq_union, ← inf_eq_inter, ← map_sup, ← map_inf, hg.extend_apply]

Premises used: Finset.inf_eq_inter, Function.Injective.extend_apply, InfHomClass.map_inf, SupHomClass.map_sup, Finset.sup_eq_union
-- 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 β)
a b : ↥L
⊢ (f₁ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) a * (f₂ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) b ≤
    (f₃ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) (a ⊓ b) * (f₄ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) (a ⊔ b)

Tactic:
h _ _
-- 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 β)
a b : ↥L
⊢ (f₁ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) a * (f₂ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) b ≤
    (f₃ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) (a ⊓ b) * (f₄ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) (a ⊔ b)

Tactic:
exact h _ _
-- 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_1 : Finset α
L : Sublattice α :=
  { carrier := (latticeClosure : (a : Set α) → Set α) ((↑s : 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
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 β)
t : Finset β
a : ↥L
ht : ¬∃ (b : ↥L), (g : (a : ↥L) → Finset β) b = 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 : 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 β)

Tactic:
simpa [extend_apply' _ _ _ ht] using mul_nonneg
        (extend_nonneg (fun a : L ↦ h₃ a) le_rfl _) (extend_nonneg (fun a : L ↦ h₄ a) le_rfl _)

Premises used: mul_nonneg, le_rfl, Function.extend_apply', Function.extend_nonneg, Subtype.val
-- 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 β
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)

Tactic:
simpa [extend_apply' _ _ _ hs] using mul_nonneg
      (extend_nonneg (fun a : L ↦ h₃ a) le_rfl _) (extend_nonneg (fun a : L ↦ h₄ a) le_rfl _)

Premises used: mul_nonneg, le_rfl, Function.extend_apply', Function.extend_nonneg, Subtype.val
-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : DecidableEq α
s t : Finset α
⊢ #s * #t ≤ #(s ⊼ t) * #(s ⊻ t)

Tactic:
simpa using four_functions_theorem (1 : α → ℕ) 1 1 1 zero_le_one zero_le_one zero_le_one
    zero_le_one (fun _ _ ↦ le_rfl) s t

Premises used: le_rfl, zero_le_one, OfNat.ofNat, four_functions_theorem
-- 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 : Fintype α
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)
⊢ HMul.hMul (α := β) (∑ a : α, f₁ a) (∑ a : α, f₂ a) ≤ HMul.hMul (α := β) (∑ a : α, f₃ a) (∑ a : α, f₄ a)

Tactic:
simpa using four_functions_theorem f₁ f₂ f₃ f₄ h₁ h₂ h₃ h₄ h univ univ

Premises used: Finset.univ, four_functions_theorem
-- 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 : Fintype α
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)
⊢ HMul.hMul (α := β) (∑ a : α, f₁ a) (∑ a : α, f₂ a) ≤ HMul.hMul (α := β) (∑ a : α, f₃ a) (∑ a : α, f₄ a)

Tactic:
classical simpa using four_functions_theorem f₁ f₂ f₃ f₄ h₁ h₂ h₃ h₄ h univ univ
-- 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 g μ : α → β
inst_5 : Fintype α
hμ₀ : 0 ≤ μ
hf : 0 ≤ f
hg : 0 ≤ g
hμ : Monotone μ
hfg : Eq.{u_2 + 1} (α := β) (∑ a : α, f a) (∑ a : α, g a)
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
inl :
  ∀ (hf : LE.le (α := α → β) 0 0) (hfg : Eq.{u_2 + 1} (α := β) (∑ a : α, 0 a) (∑ a : α, g a))
    (h : ∀ (a b : α), 0 a * g b ≤ 0 (a ⊓ b) * g (a ⊔ b)), LE.le.{u_2} (α := β) (∑ a : α, μ a * 0 a) (∑ a : α, μ a * g a)
inr : ∀ (hf : 0 < f), LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)
⊢ LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)

Tactic:
obtain rfl | hf := hf.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- 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 β
g μ : α → β
inst_5 : Fintype α
hμ₀ : 0 ≤ μ
hg : 0 ≤ g
hμ : Monotone μ
hf : LE.le (α := α → β) 0 0
hfg : Eq.{u_2 + 1} (α := β) (∑ a : α, 0 a) (∑ a : α, g a)
h : ∀ (a b : α), 0 a * g b ≤ 0 (a ⊓ b) * g (a ⊔ b)
⊢ g = 0

Tactic:
simp only [Pi.zero_apply, sum_const_zero, eq_comm, Fintype.sum_eq_zero_iff_of_nonneg hg] at hfg

Premises used: Pi.zero_apply, eq_comm, Finset.sum_const_zero, Fintype.sum_eq_zero_iff_of_nonneg
-- 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 β
g μ : α → β
inst_5 : Fintype α
hμ₀ : 0 ≤ μ
hg : 0 ≤ g
hμ : Monotone μ
hf : LE.le (α := α → β) 0 0
h : ∀ (a b : α), 0 a * g b ≤ 0 (a ⊓ b) * g (a ⊔ b)
hfg : g = 0
⊢ LE.le.{u_2} (α := β) (∑ a : α, μ a * 0 a) (∑ a : α, μ a * g a)

Tactic:
simp [hfg]
-- 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 g μ : α → β
inst_5 : Fintype α
hμ₀ : 0 ≤ μ
hf_1 : 0 ≤ f
hg : 0 ≤ g
hμ : Monotone μ
hfg : Eq.{u_2 + 1} (α := β) (∑ a : α, f a) (∑ a : α, g a)
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
inr :
  ∀ (hg : LE.le (α := α → β) 0 0) (hfg : Eq.{u_2 + 1} (α := β) (∑ a : α, f a) (∑ a : α, 0 a))
    (h : ∀ (a b : α), f a * 0 b ≤ f (a ⊓ b) * 0 (a ⊔ b)), LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * 0 a)
inr₁ : ∀ (hg : 0 < g), LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)
⊢ LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)

Tactic:
obtain rfl | hg := hg.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- 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 μ : α → β
inst_5 : Fintype α
hμ₀ : 0 ≤ μ
hf_1 : 0 ≤ f
hμ : Monotone μ
hf : 0 < f
hg : LE.le (α := α → β) 0 0
hfg : Eq.{u_2 + 1} (α := β) (∑ a : α, f a) (∑ a : α, 0 a)
h : ∀ (a b : α), f a * 0 b ≤ f (a ⊓ b) * 0 (a ⊔ b)
⊢ f = 0

Tactic:
simp only [Pi.zero_apply, sum_const_zero, Fintype.sum_eq_zero_iff_of_nonneg hf.le] at hfg

Premises used: Pi.zero_apply, LT.lt.le, Finset.sum_const_zero, Fintype.sum_eq_zero_iff_of_nonneg
-- 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 μ : α → β
inst_5 : Fintype α
hμ₀ : 0 ≤ μ
hf_1 : 0 ≤ f
hμ : Monotone μ
hf : 0 < f
hg : LE.le (α := α → β) 0 0
h : ∀ (a b : α), f a * 0 b ≤ f (a ⊓ b) * 0 (a ⊔ b)
hfg : f = 0
⊢ LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * 0 a)

Tactic:
simp [hfg]
-- 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 g μ : α → β
inst_5 : Fintype α
hμ₀ : 0 ≤ μ
hf_1 : 0 ≤ f
hg_1 : 0 ≤ g
hμ : Monotone μ
hfg : Eq.{u_2 + 1} (α := β) (∑ a : α, f a) (∑ a : α, g a)
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
inr :
  ∀
    (this :
      HMul.hMul (α := β) (∑ a : α, g a) (∑ a : α, (μ * f) a) ≤
        HMul.hMul (α := β) (∑ a ∈ univ ⊼ univ, f a) (∑ a ∈ univ ⊻ univ, (μ * g) a)),
    LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)
inr₁ : ∀ (a b : α), g a * (μ * f) b ≤ f (a ⊓ b) * (μ * g) (a ⊔ b)
⊢ LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)

Tactic:
have := four_functions_theorem g (μ * f) f (μ * g) hg.le (mul_nonneg hμ₀ hf.le) hf.le
    (mul_nonneg hμ₀ hg.le) (fun a b ↦ ?_) univ univ
-- 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 g μ : α → β
inst_5 : Fintype α
hμ₀ : 0 ≤ μ
hf_1 : 0 ≤ f
hg_1 : 0 ≤ g
hμ : Monotone μ
hfg : Eq.{u_2 + 1} (α := β) (∑ a : α, f a) (∑ a : α, g a)
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
this :
  HMul.hMul (α := β) (∑ a : α, g a) (∑ a : α, (μ * f) a) ≤
    HMul.hMul (α := β) (∑ a ∈ univ ⊼ univ, f a) (∑ a ∈ univ ⊻ univ, (μ * g) a)
⊢ LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)

Tactic:
simpa [hfg, sum_pos hg] using this

Premises used: Fintype.sum_pos
-- 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 g μ : α → β
inst_5 : Fintype α
hμ₀ : 0 ≤ μ
hf_1 : 0 ≤ f
hg_1 : 0 ≤ g
hμ : Monotone μ
hfg : Eq.{u_2 + 1} (α := β) (∑ a : α, f a) (∑ a : α, g a)
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
a b : α
inr : μ b * (f b * g a) ≤ μ (a ⊔ b) * (f (a ⊓ b) * g (a ⊔ b))
⊢ g a * (μ * f) b ≤ f (a ⊓ b) * (μ * g) (a ⊔ b)

Tactic:
simp_rw [Pi.mul_apply, mul_left_comm _ (μ _), mul_comm (g _)]

Premises used: Pi.mul_apply, mul_left_comm, mul_comm
-- 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 g μ : α → β
inst_5 : Fintype α
hμ₀ : 0 ≤ μ
hf_1 : 0 ≤ f
hg_1 : 0 ≤ g
hμ : Monotone μ
hfg : Eq.{u_2 + 1} (α := β) (∑ a : α, f a) (∑ a : α, g a)
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
a b : α
inr : μ b * (f b * g a) ≤ μ (b ⊔ a) * (f (b ⊓ a) * g (b ⊔ a))
⊢ μ b * (f b * g a) ≤ μ (a ⊔ b) * (f (a ⊓ b) * g (a ⊔ b))

Tactic:
rw [sup_comm, inf_comm]

Premises used: inf_comm, sup_comm
-- 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 g μ : α → β
inst_5 : Fintype α
hμ₀ : 0 ≤ μ
hf_1 : 0 ≤ f
hg_1 : 0 ≤ g
hμ : Monotone μ
hfg : Eq.{u_2 + 1} (α := β) (∑ a : α, f a) (∑ a : α, g a)
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
a b : α
⊢ μ b * (f b * g a) ≤ μ (b ⊔ a) * (f (b ⊓ a) * g (b ⊔ a))

Tactic:
mul_le_mul (hμ le_sup_left) (h _ _) (mul_nonneg (hf.le _) <| hg.le _) <| hμ₀ _

Premises used: mul_nonneg, le_sup_left, LT.lt.le, mul_le_mul
-- 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 g μ : α → β
inst_5 : Fintype α
hμ₀ : 0 ≤ μ
hf_1 : 0 ≤ f
hg_1 : 0 ≤ g
hμ : Monotone μ
hfg : Eq.{u_2 + 1} (α := β) (∑ a : α, f a) (∑ a : α, g a)
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
a b : α
⊢ μ b * (f b * g a) ≤ μ (b ⊔ a) * (f (b ⊓ a) * g (b ⊔ a))

Tactic:
exact mul_le_mul (hμ le_sup_left) (h _ _) (mul_nonneg (hf.le _) <| hg.le _) <| hμ₀ _

Premises used: mul_nonneg, le_sup_left, LT.lt.le, mul_le_mul
-- 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 g μ : α → β
inst_5 : Fintype α
hμ₀ : 0 ≤ μ
hf : 0 ≤ f
hg : 0 ≤ g
hμ : Monotone μ
hfg : Eq.{u_2 + 1} (α := β) (∑ a : α, f a) (∑ a : α, g a)
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
inl :
  ∀ (hf : LE.le (α := α → β) 0 0) (hfg : Eq.{u_2 + 1} (α := β) (∑ a : α, 0 a) (∑ a : α, g a))
    (h : ∀ (a b : α), 0 a * g b ≤ 0 (a ⊓ b) * g (a ⊔ b)), LE.le.{u_2} (α := β) (∑ a : α, μ a * 0 a) (∑ a : α, μ a * g a)
inr inr₁ : ∀ (hf : 0 < f), LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)
inr₂ :
  ∀ (hf : 0 < f) (hg : LE.le (α := α → β) 0 0) (hfg : Eq.{u_2 + 1} (α := β) (∑ a : α, f a) (∑ a : α, 0 a))
    (h : ∀ (a b : α), f a * 0 b ≤ f (a ⊓ b) * 0 (a ⊔ b)), LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * 0 a)
inr₃ inr₄ : ∀ (hf : 0 < f) (hg : 0 < g), LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)
inr₅ :
  ∀ (hf : 0 < f) (hg : 0 < g)
    (this :
      HMul.hMul (α := β) (∑ a : α, g a) (∑ a : α, (μ * f) a) ≤
        HMul.hMul (α := β) (∑ a ∈ univ ⊼ univ, f a) (∑ a ∈ univ ⊻ univ, (μ * g) a)),
    LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)
inr₆ inr₇ : ∀ (hf : 0 < f) (hg : 0 < g) (a b : α), g a * (μ * f) b ≤ f (a ⊓ b) * (μ * g) (a ⊔ b)
⊢ LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)

Tactic:
classical
  obtain rfl | hf := hf.eq_or_lt
  · simp only [Pi.zero_apply, sum_const_zero, eq_comm, Fintype.sum_eq_zero_iff_of_nonneg hg] at hfg
    simp [hfg]
  obtain rfl | hg := hg.eq_or_lt
  · simp only [Pi.zero_apply, sum_const_zero, Fintype.sum_eq_zero_iff_of_nonneg hf.le] at hfg
    simp [hfg]
  have := four_functions_theorem g (μ * f) f (μ * g) hg.le (mul_nonneg hμ₀ hf.le) hf.le
    (mul_nonneg hμ₀ hg.le) (fun a b ↦ ?_) univ univ
  · simpa [hfg, sum_pos hg] using this
  · simp_rw [Pi.mul_apply, mul_left_comm _ (μ _), mul_comm (g _)]
    rw [sup_comm, inf_comm]
    exact mul_le_mul (hμ le_sup_left) (h _ _) (mul_nonneg (hf.le _) <| hg.le _) <| hμ₀ _

Premises used: LE.le.eq_or_lt, Pi.mul_apply, Pi.zero_apply, mul_left_comm, eq_comm, inf_comm, Finset.sum_const_zero, sup_comm, mul_comm, Fintype.sum_eq_zero_iff_of_nonneg, rfl
-- 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 g μ : α → β
inst_5 : Fintype α
hμ₀ : 0 ≤ μ
hf₀ : 0 ≤ f
hg₀ : 0 ≤ g
hf : Monotone f
hg : Monotone g
hμ : ∀ (a b : α), μ a * μ b ≤ μ (a ⊓ b) * μ (a ⊔ b)
⊢ HMul.hMul (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a) ≤
    HMul.hMul (α := β) (∑ a : α, μ a) (∑ a : α, μ a * (f a * g a))

Tactic:
four_functions_theorem_univ (μ * f) (μ * g) μ _ (mul_nonneg hμ₀ hf₀) (mul_nonneg hμ₀ hg₀)
    hμ₀ (mul_nonneg hμ₀ <| mul_nonneg hf₀ hg₀) (fun a b ↦ ?_)

Premises used: mul_nonneg, HMul.hMul, four_functions_theorem_univ
-- 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 g μ : α → β
inst_5 : Fintype α
hμ₀ : 0 ≤ μ
hf₀ : 0 ≤ f
hg₀ : 0 ≤ g
hf : Monotone f
hg : Monotone g
hμ : ∀ (a b : α), μ a * μ b ≤ μ (a ⊓ b) * μ (a ⊔ b)
refine : ∀ (a b : α), (μ * f) a * (μ * g) b ≤ μ (a ⊓ b) * (μ (a ⊔ b) * (f (a ⊔ b) * g (a ⊔ b)))
⊢ HMul.hMul (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a) ≤
    HMul.hMul (α := β) (∑ a : α, μ a) (∑ a : α, μ a * (f a * g a))

Tactic:
refine four_functions_theorem_univ (μ * f) (μ * g) μ _ (mul_nonneg hμ₀ hf₀) (mul_nonneg hμ₀ hg₀)
    hμ₀ (mul_nonneg hμ₀ <| mul_nonneg hf₀ hg₀) (fun a b ↦ ?_)

Premises used: mul_nonneg, HMul.hMul, four_functions_theorem_univ
-- 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 g μ : α → β
inst_5 : Fintype α
hμ₀ : 0 ≤ μ
hf₀ : 0 ≤ f
hg₀ : 0 ≤ g
hf : Monotone f
hg : Monotone g
hμ : ∀ (a b : α), μ a * μ b ≤ μ (a ⊓ b) * μ (a ⊔ b)
a b : α
dsimp : μ a * f a * (μ b * g b) ≤ μ (a ⊓ b) * (μ (a ⊔ b) * (f (a ⊔ b) * g (a ⊔ b)))
⊢ (μ * f) a * (μ * g) b ≤ μ (a ⊓ b) * (μ (a ⊔ b) * (f (a ⊔ b) * g (a ⊔ b)))

Tactic:
dsimp
-- 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 g μ : α → β
inst_5 : Fintype α
hμ₀ : 0 ≤ μ
hf₀ : 0 ≤ f
hg₀ : 0 ≤ g
hf : Monotone f
hg : Monotone g
hμ : ∀ (a b : α), μ a * μ b ≤ μ (a ⊓ b) * μ (a ⊔ b)
a b : α
rw : μ a * μ b * (f a * g b) ≤ μ (a ⊓ b) * μ (a ⊔ b) * (f (a ⊔ b) * g (a ⊔ b))
⊢ μ a * f a * (μ b * g b) ≤ μ (a ⊓ b) * (μ (a ⊔ b) * (f (a ⊔ b) * g (a ⊔ b)))

Tactic:
rw [mul_mul_mul_comm, ← mul_assoc (μ (a ⊓ b))]

Premises used: mul_mul_mul_comm, mul_assoc, Min.min
-- 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 g μ : α → β
inst_5 : Fintype α
hμ₀ : 0 ≤ μ
hf₀ : 0 ≤ f
hg₀ : 0 ≤ g
hf : Monotone f
hg : Monotone g
hμ : ∀ (a b : α), μ a * μ b ≤ μ (a ⊓ b) * μ (a ⊔ b)
a b : α
⊢ μ a * μ b * (f a * g b) ≤ μ (a ⊓ b) * μ (a ⊔ b) * (f (a ⊔ b) * g (a ⊔ b))

Tactic:
mul_le_mul (hμ _ _) (mul_le_mul (hf le_sup_left) (hg le_sup_right) (hg₀ _) <| hf₀ _)
    (mul_nonneg (hf₀ _) <| hg₀ _) <| mul_nonneg (hμ₀ _) <| hμ₀ _

Premises used: mul_nonneg, le_sup_left, le_sup_right, mul_le_mul
-- 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 g μ : α → β
inst_5 : Fintype α
hμ₀ : 0 ≤ μ
hf₀ : 0 ≤ f
hg₀ : 0 ≤ g
hf : Monotone f
hg : Monotone g
hμ : ∀ (a b : α), μ a * μ b ≤ μ (a ⊓ b) * μ (a ⊔ b)
a b : α
⊢ μ a * μ b * (f a * g b) ≤ μ (a ⊓ b) * μ (a ⊔ b) * (f (a ⊔ b) * g (a ⊔ b))

Tactic:
exact mul_le_mul (hμ _ _) (mul_le_mul (hf le_sup_left) (hg le_sup_right) (hg₀ _) <| hf₀ _)
    (mul_nonneg (hf₀ _) <| hg₀ _) <| mul_nonneg (hμ₀ _) <| hμ₀ _

Premises used: mul_nonneg, le_sup_left, le_sup_right, mul_le_mul