-- 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)
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)
⊢ 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),
  let s' : Finset ↥L := s.preimage (Subtype.val (p := fun (x : α) ↦ x ∈ L)) sorry;
  let t' : Finset ↥L := t.preimage (Subtype.val (p := fun (x : α) ↦ x ∈ L)) sorry;
  ∀ (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: 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 _)