-- 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))
_ :
  Eq (α := E → ℝ)
    (sSup
      {f : E → ℝ |
        f ≤ φ ∧
          ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
            f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c})
    (sSup ((fun (g : (↑univ : Type u_2) → ℝ) ↦ g ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2))) '' 𝓕))
_₁ :
  Eq (α := E → ℝ)
    (sSup ((fun (g : (↑univ : Type u_2) → ℝ) ↦ g ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2))) '' 𝓕))
    (sSup 𝓕 ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)))
_₂ :
  φ ∘
      Function.comp (β := { x : E // Membership.mem (γ := Set E) univ x })
        (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x))
        (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)) =
    φ
⊢ sSup
      {f : E → ℝ |
        f ≤ φ ∧
          ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
            f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c} =
    φ

Tactic:
calc
  _ = sSup ((fun g => g ∘ (Equiv.Set.univ E).symm) '' 𝓕) := by
    congr
    ext f
    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, ?_⟩⟩⟩
    · ext x; simpa using congrFun hlc x
    · ext; simp
    · simpa using hb ▸ h ⟨x, trivial⟩
    · subst hlc; simpa using hb.symm
  _ = sSup 𝓕 ∘ (Equiv.Set.univ E).symm := by ext x; rw [sSup_image', sSup_eq_iSup']; simp
  _ = φ ∘ Subtype.val ∘ (Equiv.Set.univ E).symm :=
    congrArg (fun g => g ∘ (Equiv.Set.univ E).symm) this
  _ = φ := by ext; simp

Premises used: congrArg, Function.comp, Set.image, Equiv.symm, Subtype.val, DFunLike.coe, SupSet.sSup, Equiv.Set.univ