how to judge the common upper bound

Stream: maths

[Billlie Franch]

import Mathlib.Tactic
import Mathlib.Analysis.Convex.Function
import Mathlib.Data.Real.EReal
import Mathlib.Topology.Basic
import Mathlib.Topology.Sequences
import Mathlib.Order.Filter.Basic
import Mathlib.Order.LiminfLimsup
import Mathlib.Data.Set.Basic
import Mathlib.Logic.Basic
import Mathlib.Order.Basic
import Mathlib.Topology.Sets.Closeds
import Mathlib.Topology.Bases
import Mathlib.Init.Set
import Mathlib.Data.Set.Basic

open EReal Function Topology Filter Set TopologicalSpace


variable {𝕜 E α β ι : Type _}

variable [OrderedSemiring 𝕜]

variable [AddCommMonoid E]

variable (𝕜) (s : Set E) (f : E → EReal)[SMul 𝕜 E]

variable (x : s)
variable (f1 : E → EReal)
variable (f2 : E → EReal)
example (h1 : f1 x ≤ r)(h2 : f2 x ≤ r) : sSup {f1, f2} x ≤ r := by sorry

Can someone please help me to complete this sorry?

[Adam Topaz]

I came up with this:

example (h1 : f1 x ≤ r)(h2 : f2 x ≤ r) : sSup {f1, f2} x ≤ r := by
  apply sSup_le
  rintro _ ⟨⟨w,hw⟩,rfl⟩
  simp only [mem_singleton_iff, mem_insert_iff] at hw
  rcases hw with rfl|rfl <;> assumption

Is there any particular reason you're using sSup? Using sup or max in this case would probably be easier.