awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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
⊢ 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 β)
have refine_1 : ∀ (b : ↥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) (β := 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: obtain ⟨b, rfl⟩ | ht := em (∃ b, g b = t)
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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
⊢ 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 β)
have 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)
Tactic: simp_rw [← sup_eq_union, ← inf_eq_inter, ← map_sup, ← map_inf, hg.extend_apply]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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 β
⊢ 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)
have 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 β)
Tactic: classical
  obtain ⟨a, rfl⟩ | hs := em (∃ a, g a = s)
  · obtain ⟨b, rfl⟩ | ht := em (∃ b, g b = t)
    · simp_rw [← sup_eq_union, ← inf_eq_inter, ← map_sup, ← map_inf, hg.extend_apply]
      exact h _ _
    · 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 _)
  · 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 _)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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 β)
⊢ 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)
have 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)
Tactic: classical
  obtain ⟨a, rfl⟩ | hs := em (∃ a, g a = s)
  · obtain ⟨b, rfl⟩ | ht := em (∃ b, g b = t)
    · simp_rw [← sup_eq_union, ← inf_eq_inter, ← map_sup, ← map_inf, hg.extend_apply]
      exact h _ _
    · 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 _)
  · 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 _)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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 α
set set₁ :
  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)
have set₂ : let L : Sublattice α :=
  { carrier := (latticeClosure : (a : Set α) → Set α) ((↑s : Set α) ∪ (↑t : Set α)), supClosed' := sorry, infClosed' := sorry };
∀ (this : Finite.{u_1 + 1} ↥L),
  HMul.hMul (α := β) (∑ a ∈ s, f₁ a) (∑ a ∈ t, f₂ a) ≤ HMul.hMul (α := β) (∑ a ∈ s ⊼ t, f₃ a) (∑ a ∈ s ⊻ t, f₄ a)
Tactic: classical
  set L : Sublattice α := ⟨latticeClosure (s ∪ t), isSublattice_latticeClosure.1,
    isSublattice_latticeClosure.2⟩
  have : Finite L := (s.finite_toSet.union t.finite_toSet).latticeClosure.to_subtype
  set s' : Finset L := s.preimage (↑) Subtype.coe_injective.injOn
  set t' : Finset L := t.preimage (↑) Subtype.coe_injective.injOn
  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
  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
  clear_value s' t'
  obtain ⟨β, _, _, g, hg⟩ := exists_birkhoff_representation L
  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⟩)
  · simpa only [← hs', ← ht', ← map_sups, ← map_infs, sum_map, Embedding.coeFn_mk, hg.extend_apply]
      using this
  rintro s t
  classical
  obtain ⟨a, rfl⟩ | hs := em (∃ a, g a = s)
  · obtain ⟨b, rfl⟩ | ht := em (∃ b, g b = t)
    · simp_rw [← sup_eq_union, ← inf_eq_inter, ← map_sup, ← map_inf, hg.extend_apply]
      exact h _ _
    · 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 _)
  · 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 _)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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)
⊢ LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)
have 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)
Tactic: obtain rfl | hf := hf.eq_or_lt
Cleared hypotheses: f, hf, hfg, h
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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)
⊢ LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)
have inr : ∀ (hf : 0 < f), LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)
Tactic: obtain rfl | hf := hf.eq_or_lt
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (hypothesis)
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)
⊢ LE.le.{u_2} (α := β) (∑ a : α, μ a * 0 a) (∑ a : α, μ a * g a)
have hfg₁ : g = 0
Tactic: simp only [Pi.zero_apply, sum_const_zero, eq_comm, Fintype.sum_eq_zero_iff_of_nonneg hg] at hfg
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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
⊢ LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)
have 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)
Tactic: obtain rfl | hg := hg.eq_or_lt
Cleared hypotheses: g, hg, hfg, h
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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)
⊢ LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)
have inr₁ : ∀ (hg : 0 < g), LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)
Tactic: obtain rfl | hg := hg.eq_or_lt
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (hypothesis)
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)
⊢ LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * 0 a)
have hfg₁ : f = 0
Tactic: simp only [Pi.zero_apply, sum_const_zero, Fintype.sum_eq_zero_iff_of_nonneg hf.le] at hfg
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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
⊢ LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)
have 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)
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
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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)
⊢ LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)
have inr₁ : ∀ (a b : α), g a * (μ * f) b ≤ f (a ⊓ b) * (μ * g) (a ⊔ b)
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
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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 : α
⊢ g a * (μ * f) b ≤ f (a ⊓ b) * (μ * g) (a ⊔ b)
have inr : μ b * (f b * g a) ≤ μ (a ⊔ b) * (f (a ⊓ b) * g (a ⊔ b))
Tactic: simp_rw [Pi.mul_apply, mul_left_comm _ (μ _), mul_comm (g _)]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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) ≤ μ (a ⊔ b) * (f (a ⊓ b) * g (a ⊔ b))
have inr : μ b * (f b * g a) ≤ μ (b ⊔ a) * (f (b ⊓ a) * g (b ⊔ a))
Tactic: rw [sup_comm, inf_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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)
⊢ LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)
have 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)
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μ₀ _
Cleared hypotheses: f, hf, hfg, h
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
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)
⊢ LE.le.{u_2} (α := β) (∑ a : α, μ a * f a) (∑ a : α, μ a * g a)
have inr : ∀ (hf : 0 < f), 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μ₀ _