-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
x : (↑s : Type u_2)
h :
  Set.Nonempty (α := ℝ)
    (range
      fun
        (f :
          (↑{f : (a : (↑s : Type u_2)) → ℝ |
                f ≤ s.restrict (π := fun (a : E) ↦ ℝ) φ ∧
                  ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
                    f =
                      s.restrict (π := fun (a : E) ↦ ℝ)
                          (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜)) +
                        const (↑s : Type u_2) c} :
            Type u_2)) ↦
      (↑f : (a : (↑s : Type u_2)) → ℝ) x)
⊢ ⨆ (f :
      (↑{f : (a : (↑s : Type u_2)) → ℝ |
            f ≤ s.restrict (π := fun (a : E) ↦ ℝ) φ ∧
              ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
                f =
                  s.restrict (π := fun (a : E) ↦ ℝ)
                      (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜)) +
                    const (↑s : Type u_2) c} :
        Type u_2)),
      (↑f : (a : (↑s : Type u_2)) → ℝ) x =
    s.restrict (π := fun (a : E) ↦ ℝ) φ x
have h₁ : ∀ (r : ℝ),
  Membership.mem (γ := Set ℝ)
      (range
        fun
          (f :
            (↑{f : (a : (↑s : Type u_2)) → ℝ |
                  f ≤ s.restrict (π := fun (a : E) ↦ ℝ) φ ∧
                    ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
                      f =
                        s.restrict (π := fun (a : E) ↦ ℝ)
                            (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜)) +
                          const (↑s : Type u_2) c} :
              Type u_2)) ↦
        (↑f : (a : (↑s : Type u_2)) → ℝ) x)
      r →
    ∀
      (f :
        (↑{f : (a : (↑s : Type u_2)) → ℝ |
              f ≤ s.restrict (π := fun (a : E) ↦ ℝ) φ ∧
                ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
                  f =
                    s.restrict (π := fun (a : E) ↦ ℝ)
                        (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜)) +
                      const (↑s : Type u_2) c} :
          Type u_2))
      (hf :
        (fun
                (f :
                  (↑{f : (a : (↑s : Type u_2)) → ℝ |
                        f ≤ s.restrict (π := fun (a : E) ↦ ℝ) φ ∧
                          ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
                            f =
                              s.restrict (π := fun (a : E) ↦ ℝ)
                                  (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ)
                                    (⇑l : (a : E) → 𝕜)) +
                                const (↑s : Type u_2) c} :
                    Type u_2)) ↦
              (↑f : (a : (↑s : Type u_2)) → ℝ) x)
            f =
          r),
      r ≤ s.restrict (π := fun (a : E) ↦ ℝ) φ x
Tactic: refine csSup_eq_of_forall_le_of_forall_lt_exists_gt ?_ (fun r ⟨f, hf⟩ => ?_) (fun r hr => ?_)