-- 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)
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
⊢ ⨆ (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 : ℝ) (hr : r < s.restrict (π := fun (a : E) ↦ ℝ) φ x),
  ∃ (a : ℝ),
    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)
        a ∧
      r < a
Tactic: refine csSup_eq_of_forall_le_of_forall_lt_exists_gt ?_ (fun r ⟨f, hf⟩ => ?_) (fun r hr => ?_)