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)}
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
h₁ :
  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)
⊢ (fun (g : (↑univ : Type u_2) → ℝ) ↦ (g ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)) : E → ℝ))
      (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)) =
    f

Tactic:
subst hlc
-- 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
l : E →L[𝕜] 𝕜
c : ℝ
h :
  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)
hb :
  (fun (g : (↑univ : Type u_2) → ℝ) ↦ (g ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)) : E → ℝ))
      (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)) =
    f
⊢ f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c

Tactic:
simpa using hb.symm

Premises used: Eq.symm
-- 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))
h :
  ∀ (x : E),
    sSup ((fun (g : (↑univ : Type u_2) → ℝ) ↦ g ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2))) '' 𝓕) x =
      (sSup 𝓕 ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2))) x
⊢ 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)))

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))
x : E
h :
  Eq (α := ℝ)
    ((⨆ (a : (↑𝓕 : Type u_2)),
        (↑a : (↑univ : Type u_2) → ℝ) ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)))
      x)
    (Function.comp (β := { x : E // Membership.mem (γ := Set E) univ x })
      (⨆ (a : (↑𝓕 : Type u_2)), (↑a : { x : E // x ∈ univ } → ℝ))
      (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)) x)
⊢ sSup ((fun (g : (↑univ : Type u_2) → ℝ) ↦ g ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2))) '' 𝓕) x =
    (sSup 𝓕 ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2))) x

Tactic:
rw [sSup_image', sSup_eq_iSup']

Premises used: sSup_image', sSup_eq_iSup'
-- 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))
x : E
⊢ Eq (α := ℝ)
    ((⨆ (a : (↑𝓕 : Type u_2)),
        (↑a : (↑univ : Type u_2) → ℝ) ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)))
      x)
    (Function.comp (β := { x : E // Membership.mem (γ := Set E) univ x })
      (⨆ (a : (↑𝓕 : Type u_2)), (↑a : { x : E // x ∈ univ } → ℝ))
      (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)) 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))
⊢ Eq (α := E → ℝ) (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)))

Tactic:
congrArg (fun g => g ∘ (Equiv.Set.univ E).symm) this

Premises used: congrArg, setOf, Function.comp, Equiv.symm, 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))
h :
  ∀ (x : E),
    (φ ∘
          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)))
        x =
      φ x
⊢ φ ∘
      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)) =
    φ

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))
x : E
⊢ (φ ∘
        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)))
      x =
    φ 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
inst_9 : HereditarilyLindelofSpace E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set (E → ℝ) :=
  {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}
⊢ IsLUB 𝓕 φ

Tactic:
(hφcv.univ_sSup_affine_eq (𝕜 := 𝕜) hφc) ▸ isLUB_csSup ?_ ?_

Premises used: Eq.rec, ConvexOn.univ_sSup_affine_eq, isLUB_csSup
-- 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
inst_9 : HereditarilyLindelofSpace E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set (E → ℝ) :=
  {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}
refine_1 : 𝓕.Nonempty
refine_2 : BddAbove 𝓕
⊢ IsLUB 𝓕 φ

Tactic:
refine (hφcv.univ_sSup_affine_eq (𝕜 := 𝕜) hφc) ▸ isLUB_csSup ?_ ?_
-- 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
inst_9 : HereditarilyLindelofSpace E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set (E → ℝ) :=
  {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}
⊢ φ 0 - 1 < φ (↑(Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x) 0 ⋯) : E)

Tactic:
grind
-- 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
inst_9 : HereditarilyLindelofSpace E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set (E → ℝ) :=
  {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}
refine_1 :
  ∀ (l : E →L[𝕜] 𝕜) (c : ℝ)
    (hlc :
      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 φ ∧
        HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) 0 : 𝕜) : ℝ) c = φ 0 - 1),
    𝓕.Nonempty
⊢ 𝓕.Nonempty

Tactic:
obtain ⟨l, c, hlc⟩ := exists_affine_le_of_lt (𝕜 := 𝕜) (@mem_univ E 0)
        (by grind : φ 0 - 1 < φ (⟨0, @mem_univ E 0⟩ : univ)) isClosed_univ
        (lowerSemicontinuousOn_univ_iff.2 hφc) hφcv

Premises used: isClosed_univ, Iff.mpr, Set.mem_univ, lowerSemicontinuousOn_univ_iff, OfNat.ofNat, ConvexOn.exists_affine_le_of_lt
-- 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
inst_9 : HereditarilyLindelofSpace E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set (E → ℝ) :=
  {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}
l : E →L[𝕜] 𝕜
c : ℝ
hlc :
  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 φ ∧
    HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) 0 : 𝕜) : ℝ) c = φ 0 - 1
⊢ 𝓕.Nonempty

Tactic:
⟨(re ∘ l) + const E c, fun x => hlc.1 ⟨x, mem_univ x⟩, ⟨l, c, rfl⟩⟩

Premises used: Function.comp, Subtype.mk, Set.Nonempty, And.left, HAdd.hAdd, And.intro, Exists.intro, Set.mem_univ, RCLike.re, Function.const, DFunLike.coe, rfl
-- 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
inst_9 : HereditarilyLindelofSpace E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set (E → ℝ) :=
  {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}
l : E →L[𝕜] 𝕜
c : ℝ
hlc :
  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 φ ∧
    HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) 0 : 𝕜) : ℝ) c = φ 0 - 1
⊢ 𝓕.Nonempty

Tactic:
exact ⟨(re ∘ l) + const E c, fun x => hlc.1 ⟨x, mem_univ x⟩, ⟨l, c, rfl⟩⟩
-- 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
inst_9 : HereditarilyLindelofSpace E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set (E → ℝ) :=
  {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}
⊢ BddAbove 𝓕

Tactic:
(bddAbove_def.2 ⟨φ, fun y hy => hy.1⟩)

Premises used: Iff.mpr, And.left, Exists.intro, bddAbove_def