-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
φ : 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
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set ({ x : E // Membership.mem (γ := Set E) univ x } → ℝ) :=
  {f : { x : E // Membership.mem (γ := Set E) univ x } → ℝ |
    f ≤ φ ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x) ∧
      ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
        f =
          HAdd.hAdd (α := { x : E // Membership.mem (γ := Set E) univ x } → ℝ)
            (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) ∘
              Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x))
            (const (↑univ : Type u_2) c)}
this :
  Eq (α := (a : (↑univ : Type u_2)) → ℝ)
    (sSup
      {f : (a : (↑univ : Type u_2)) → ℝ |
        f ≤ φ ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x) ∧
          ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
            f =
              HAdd.hAdd (α := (a : (↑univ : Type u_2)) → ℝ)
                (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) ∘
                  Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x))
                (const (↑univ : Type u_2) c)})
    (φ ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x))
f : E → ℝ
e_a :
  (f ≤ φ ∧
      ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
        f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c) →
    ∀ (hp : f ≤ φ) (l : E →L[𝕜] 𝕜) (c : ℝ)
      (hlc : f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c),
      f ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x) =
        HAdd.hAdd (α := { x : E // Membership.mem (γ := Set E) univ x } → ℝ)
          (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) ∘
            Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x))
          (const (↑univ : Type u_2) c)
e_a₁ :
  (f ≤ φ ∧
      ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
        f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c) →
    ∀ (hp : f ≤ φ) (l : E →L[𝕜] 𝕜) (c : ℝ)
      (hlc : f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c),
      (fun (g : (↑univ : Type u_2) → ℝ) ↦ (g ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)) : E → ℝ))
          (f ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x)) =
        f
e_a₂ :
  (∃ a ∈ 𝓕,
      (fun (g : (↑univ : Type u_2) → ℝ) ↦ (g ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)) : E → ℝ)) a =
        f) →
    ∀ (a : (↑univ : Type u_2) → ℝ) (h : a ≤ φ ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x))
      (l : E →L[𝕜] 𝕜) (c : ℝ)
      (hlc :
        a =
          HAdd.hAdd (α := { x : E // Membership.mem (γ := Set E) univ x } → ℝ)
            (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) ∘
              Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x))
            (const (↑univ : Type u_2) c))
      (hb :
        (fun (g : (↑univ : Type u_2) → ℝ) ↦ (g ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)) : E → ℝ)) a =
          f)
      (x : E), f x ≤ φ x
e_a₃ :
  (∃ a ∈ 𝓕,
      (fun (g : (↑univ : Type u_2) → ℝ) ↦ (g ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)) : E → ℝ)) a =
        f) →
    ∀ (a : (↑univ : Type u_2) → ℝ) (h : a ≤ φ ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x))
      (l : E →L[𝕜] 𝕜) (c : ℝ)
      (hlc :
        a =
          HAdd.hAdd (α := { x : E // Membership.mem (γ := Set E) univ x } → ℝ)
            (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) ∘
              Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x))
            (const (↑univ : Type u_2) c))
      (hb :
        (fun (g : (↑univ : Type u_2) → ℝ) ↦ (g ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)) : E → ℝ)) a =
          f),
      f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c
⊢ (f ≤ φ ∧
      ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
        f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c) ↔
    ∃ a ∈ 𝓕,
      (fun (g : (↑univ : Type u_2) → ℝ) ↦ (g ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)) : E → ℝ)) a = f

Tactic:
refine ⟨fun ⟨hp, l, c, hlc⟩ => ⟨f ∘ Subtype.val, ⟨fun x => hp (Subtype.val x), ⟨l, c, ?_⟩⟩, ?_⟩,
      fun ⟨a, ⟨⟨h, ⟨l, c, hlc⟩⟩, hb⟩⟩ => ⟨fun x => ?_, ⟨l, c, ?_⟩⟩⟩