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 β
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
⊢ HMul.hMul (α := β) (∑ s ∈ 𝒜, f₁ s) (∑ s ∈ ℬ, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) (∑ s ∈ 𝒜 ⊻ ℬ, f₄ s)
have 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)
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
Cleared hypotheses: f₁, f₂, f₃, f₄, u, h₁, h₂, h₃, h₄, h, 𝒜, ℬ, 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 β
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)
⊢ HMul.hMul (α := β) (∑ s ∈ 𝒜, f₁ s) (∑ s ∈ ℬ, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) (∑ s ∈ 𝒜 ⊻ ℬ, f₄ s)
have 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 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)
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
Cleared hypotheses: f₁, f₂, f₃, f₄, u, h₁, h₂, h₃, h₄, h, 𝒜, ℬ, 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 β
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 α)
⊢ HMul.hMul (α := β) (∑ s ∈ 𝒜, f₁ s) (∑ s ∈ ℬ, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) (∑ s ∈ 𝒜 ⊻ ℬ, f₄ s)
have have : ∀ (this : Fintype α),
  HMul.hMul (α := β) (∑ s ∈ 𝒜, f₁ s) (∑ s ∈ ℬ, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) (∑ s ∈ 𝒜 ⊻ ℬ, f₄ s)
Tactic: have := Fintype.ofFinite α
-- 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 β
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)
have refine_1 : ∀ ⦃s : Finset α⦄, s ⊆ univ → ∀ ⦃t : Finset α⦄, t ⊆ univ → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
Tactic: refine univ.four_functions_theorem h₁ h₂ 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 β
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)
⊢ HMul.hMul (α := β) (∑ s ∈ 𝒜, f₁ s) (∑ s ∈ ℬ, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) (∑ s ∈ 𝒜 ⊻ ℬ, f₄ s)
have refine_2 : 𝒜 ⊆ powerset univ
Tactic: refine univ.four_functions_theorem h₁ h₂ 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 β
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
⊢ HMul.hMul (α := β) (∑ s ∈ 𝒜, f₁ s) (∑ s ∈ ℬ, f₂ s) ≤ HMul.hMul (α := β) (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) (∑ s ∈ 𝒜 ⊻ ℬ, f₄ s)
have refine_3 : ℬ ⊆ powerset univ
Tactic: refine univ.four_functions_theorem h₁ h₂ h₃ h₄ ?_ ?_ ?_
-- 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₁ 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' := ⋯ }
⊢ HMul.hMul (α := β) (∑ a ∈ s, f₁ a) (∑ a ∈ t, f₂ a) ≤ HMul.hMul (α := β) (∑ a ∈ s ⊼ t, f₃ a) (∑ a ∈ s ⊻ t, f₄ a)
have this : Finite.{u_1 + 1} ↥L
Tactic: have : Finite L := (s.finite_toSet.union t.finite_toSet).latticeClosure.to_subtype
-- 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₁ 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)) ⋯
⊢ HMul.hMul (α := β) (∑ a ∈ s, f₁ a) (∑ a ∈ t, f₂ a) ≤ HMul.hMul (α := β) (∑ a ∈ s ⊼ t, f₃ a) (∑ a ∈ s ⊻ t, f₄ a)
have hs' : map { toFun := (⇑L.subtype : (a : ↥L) → α), inj' := sorry : ↥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
-- 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₁ 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
⊢ HMul.hMul (α := β) (∑ a ∈ s, f₁ a) (∑ a ∈ t, f₂ a) ≤ HMul.hMul (α := β) (∑ a ∈ s ⊼ t, f₃ a) (∑ a ∈ s ⊻ t, f₄ a)
have ht' : map { toFun := (⇑L.subtype : (a : ↥L) → α), inj' := sorry : ↥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
-- 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 α
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
⊢ HMul.hMul (α := β) (∑ a ∈ s, f₁ a) (∑ a ∈ t, f₂ a) ≤ HMul.hMul (α := β) (∑ a ∈ s ⊼ t, f₃ a) (∑ a ∈ s ⊻ t, f₄ a)
have clear_value : ∀ (s' t' : Finset ↥L) (hs' : map { toFun := (⇑L.subtype : (a : ↥L) → α), inj' := sorry : ↥L ↪ α } s' = s)
  (ht' : map { toFun := (⇑L.subtype : (a : ↥L) → α), inj' := sorry : ↥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)
Tactic: clear_value s' t'
Cleared hypotheses: s', t', hs', ht'
-- 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 α
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
⊢ HMul.hMul (α := β) (∑ a ∈ s, f₁ a) (∑ a ∈ t, f₂ a) ≤ HMul.hMul (α := β) (∑ a ∈ s ⊼ t, f₃ a) (∑ a ∈ s ⊻ t, f₄ a)
have 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)
Tactic: obtain ⟨β, _, _, g, hg⟩ := exists_birkhoff_representation L
-- 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 β)
⊢ HMul.hMul (α := β_1) (∑ a ∈ s, f₁ a) (∑ a ∈ t, f₂ a) ≤ HMul.hMul (α := β_1) (∑ a ∈ s ⊼ t, f₃ a) (∑ a ∈ s ⊻ t, f₄ a)
have 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)
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⟩)
-- 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 β)
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)
⊢ HMul.hMul (α := β_1) (∑ a ∈ s, f₁ a) (∑ a ∈ t, f₂ a) ≤ HMul.hMul (α := β_1) (∑ a ∈ s ⊼ t, f₃ a) (∑ a ∈ s ⊻ t, f₄ a)
have 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)
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⟩)
-- 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: obtain ⟨a, rfl⟩ | hs := em (∃ a, g a = s)
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: obtain ⟨a, rfl⟩ | hs := em (∃ a, g a = s)