-- 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 α
set set₁ :
  HMul.hMul (α := β) (∑ a ∈ s, f₁ a) (∑ a ∈ t, f₂ a) ≤ HMul.hMul (α := β) (∑ a ∈ s ⊼ t, f₃ a) (∑ a ∈ s ⊻ t, f₄ a)
set₂ set₃ set₄ :
  let L : Sublattice α :=
    { carrier := (latticeClosure : (a : Set α) → Set α) ((↑s : Set α) ∪ (↑t : Set α)), supClosed' := ⋯,
      infClosed' := ⋯ };
  ∀ (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)
set₅ :
  let L : Sublattice α :=
    { carrier := (latticeClosure : (a : Set α) → Set α) ((↑s : Set α) ∪ (↑t : Set α)), supClosed' := ⋯,
      infClosed' := ⋯ };
  ∀ (this : Finite.{u_1 + 1} ↥L),
    let s' : Finset ↥L := s.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)
set₆ :
  let L : Sublattice α :=
    { carrier := (latticeClosure : (a : Set α) → Set α) ((↑s : Set α) ∪ (↑t : Set α)), supClosed' := ⋯,
      infClosed' := ⋯ };
  ∀ (this : Finite.{u_1 + 1} ↥L),
    let s' : Finset ↥L := s.preimage (Subtype.val (p := fun (x : α) ↦ x ∈ L)) ⋯;
    let 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)
set₇ :
  let 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)
set₈ :
  let 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) (β_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)
refine_2 :
  let 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) (β_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))
    (this :
      HMul.hMul (α := β)
          (∑ s ∈ map { toFun := (⇑g : (a : ↥L) → Finset β_1), inj' := hg : ↥L ↪ Finset β_1 } s',
            extend (α := ↥L) (⇑g : (a : ↥L) → Finset β_1) (f₁ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) 0 s)
          (∑ s ∈ map { toFun := (⇑g : (a : ↥L) → Finset β_1), inj' := hg : ↥L ↪ Finset β_1 } t',
            extend (α := ↥L) (⇑g : (a : ↥L) → Finset β_1) (f₂ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) 0 s) ≤
        HMul.hMul (α := β)
          (∑
            s ∈
              map { toFun := (⇑g : (a : ↥L) → Finset β_1), inj' := hg : ↥L ↪ Finset β_1 } s' ⊼
                map { toFun := (⇑g : (a : ↥L) → Finset β_1), inj' := hg : ↥L ↪ Finset β_1 } t',
            extend (α := ↥L) (⇑g : (a : ↥L) → Finset β_1) (f₃ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) 0 s)
          (∑
            s ∈
              map { toFun := (⇑g : (a : ↥L) → Finset β_1), inj' := hg : ↥L ↪ Finset β_1 } s' ⊻
                map { toFun := (⇑g : (a : ↥L) → Finset β_1), inj' := hg : ↥L ↪ Finset β_1 } t',
            extend (α := ↥L) (⇑g : (a : ↥L) → Finset β_1) (f₄ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) 0 s)),
    HMul.hMul (α := β) (∑ a ∈ s, f₁ a) (∑ a ∈ t, f₂ a) ≤ HMul.hMul (α := β) (∑ a ∈ s ⊼ t, f₃ a) (∑ a ∈ s ⊻ t, f₄ a)
refine_1 refine_1₁ refine_1₂ :
  let 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) (β_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)) (s t : Finset β_1),
    extend (α := ↥L) (⇑g : (a : ↥L) → Finset β_1) (f₁ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) 0 s *
        extend (α := ↥L) (⇑g : (a : ↥L) → Finset β_1) (f₂ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) 0 t ≤
      extend (α := ↥L) (⇑g : (a : ↥L) → Finset β_1) (f₃ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) 0 (s ∩ t) *
        extend (α := ↥L) (⇑g : (a : ↥L) → Finset β_1) (f₄ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) 0 (s ∪ t)
⊢ 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 _)

Premises used: Sublattice, Finset.sum_map, Finset.inf_eq_inter, InfHomClass.map_inf, Finset.preimage, Finset.map_sups, Function.Embedding.coeFn_mk, SupHomClass.map_sup, Finset.map_infs, Finset.sup_eq_union, rfl