-- 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 β
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 β)
refine_1₁ 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)
⊢ 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 _)

Premises used: mul_nonneg, le_rfl, Exists, em, Finset.inf_eq_inter, Function.Injective.extend_apply, InfHomClass.map_inf, Function.extend_nonneg, SupHomClass.map_sup, Finset.sup_eq_union, Subtype.val, Eq, DFunLike.coe, rfl