awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)}
⊢ Eq (α := (a : (↑univ : Type u_2)) → ℝ)
    (sSup
      {f : (a : (↑univ : Type u_2)) → ℝ |
        f ≤ Set.restrict (π := fun (a : E) ↦ ℝ) univ φ ∧
          ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
            f =
              HAdd.hAdd (α := (a : (↑univ : Type u_2)) → ℝ)
                (Set.restrict (π := fun (a : E) ↦ ℝ) univ
                  (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜)))
                (const (↑univ : Type u_2) c)})
    (Set.restrict (π := fun (a : E) ↦ ℝ) univ φ)

Tactic:
have := hφcv.sSup_affine_eq (𝕜 := 𝕜) isClosed_univ (lowerSemicontinuousOn_univ_iff.2 hφc)
-- 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))
e_a :
  Eq.{u_2 + 1} (α := (E → ℝ) → Prop)
    (fun (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)
    fun (x : E → ℝ) ↦
    ∃ a ∈ 𝓕,
      (fun (g : (↑univ : Type u_2) → ℝ) ↦ (g ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)) : E → ℝ)) a = 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))) '' 𝓕))

Tactic:
congr
-- 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))
e_a :
  ∀ (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) ↔
      ∃ a ∈ 𝓕,
        (fun (g : (↑univ : Type u_2) → ℝ) ↦ (g ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)) : E → ℝ)) a =
          f
⊢ Eq.{u_2 + 1} (α := (E → ℝ) → Prop)
    (fun (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)
    fun (x : E → ℝ) ↦
    ∃ a ∈ 𝓕,
      (fun (g : (↑univ : Type u_2) → ℝ) ↦ (g ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)) : E → ℝ)) a = x

Tactic:
ext f
-- 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 → ℝ
⊢ (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:
⟨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, ?_⟩⟩⟩

Premises used: _private.0.ConvexOn.univ_sSup_affine_eq.match_2, Function.comp, Membership.mem, Exists, _private.0.ConvexOn.univ_sSup_affine_eq.match_1, LE.le, And, HAdd.hAdd, And.intro, Iff.intro, Exists.intro, RCLike.re, Function.const, Equiv.symm, Subtype.val, Eq, DFunLike.coe, Equiv.Set.univ
-- 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 → ℝ
h :
  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
e_a :
  ∀ (x : (↑univ : Type u_2)),
    (f ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x)) x =
      HAdd.hAdd (α := { x : E // Membership.mem (γ := Set E) univ x } → ℝ) (β := (↑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) x
⊢ 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)

Tactic:
ext x
-- 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 → ℝ
h :
  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
x : (↑univ : Type u_2)
⊢ (f ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x)) x =
    HAdd.hAdd (α := { x : E // Membership.mem (γ := Set E) univ x } → ℝ) (β := (↑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) x

Tactic:
simpa using congrFun hlc x

Premises used: congrFun, Subtype.val
-- 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 → ℝ
h :
  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
e_a :
  ∀ (x : E),
    (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)) x =
      f x
⊢ (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

Tactic:
ext
-- 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 → ℝ
h :
  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
x : E
⊢ (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)) x =
    f x

Tactic:
simp
-- 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 → ℝ
h_1 :
  ∃ 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

Tactic:
simpa using hb ▸ h ⟨x, trivial⟩
-- 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 → ℝ
h_1 :
  ∃ 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
⊢ 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) ≤
    φ ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x)

Tactic:
subst hlc