awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Approximation
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
inst_9 : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
hs : s.Nonempty
𝓕 : Set ((a : (↑s : Type u_2)) → ℝ) :=
  {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}
hl : IsLUB 𝓕 (s.restrict (π := fun (a : E) ↦ ℝ) φ)
hr : ∀ (f : (a : (↑s : Type u_2)) → ℝ) (hf : f ∈ 𝓕), LowerSemicontinuous f
𝓕' : Set ((↑s : Type u_2) → ℝ)
h𝓕' : 𝓕' ⊆ 𝓕 ∧ 𝓕'.Countable ∧ IsLUB 𝓕' (s.restrict (π := fun (a : E) ↦ ℝ) φ)
this : 𝓕' = ∅
⊢ False

Tactic:
grind [(isLUB_empty_iff.1 (this ▸ h𝓕'.2.2)) (fun x : s => φ x - 1) ⟨hs.some, hs.some_mem⟩]

Premises used: HSub.hSub, Set.Nonempty.some_mem, Subtype.mk, Iff.mp, isLUB_empty_iff, OfNat.ofNat, Subtype.val, Set.Nonempty.some
-- Module: Mathlib.Analysis.Convex.Approximation
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
inst_9 : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
hs : s = ∅
h :
  Set.Countable.{u_2} (α := (↑s : Type u_2) → ℝ) ∅ ∧
    sSup ∅ = s.restrict (π := fun (a : E) ↦ ℝ) φ ∧
      ∀ (f : (↑s : Type u_2) → ℝ),
        Membership.mem (γ := Set ((↑s : Type u_2) → ℝ)) ∅ f →
          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
⊢ ∃ (𝓕' : Set ((↑s : Type u_2) → ℝ)),
    𝓕'.Countable ∧
      sSup 𝓕' = s.restrict (π := fun (a : E) ↦ ℝ) φ ∧
        ∀ f ∈ 𝓕',
          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

Tactic:
use ∅
-- Module: Mathlib.Analysis.Convex.Approximation
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
inst_9 : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
hs : s = ∅
h : Eq.{u_2 + 1} (α := (↑s : Type u_2) → ℝ) (sSup ∅) fun (x : (↑s : Type u_2)) ↦ φ (↑x : E)
⊢ Set.Countable.{u_2} (α := (↑s : Type u_2) → ℝ) ∅ ∧
    sSup ∅ = s.restrict (π := fun (a : E) ↦ ℝ) φ ∧
      ∀ (f : (↑s : Type u_2) → ℝ),
        Membership.mem (γ := Set ((↑s : Type u_2) → ℝ)) ∅ f →
          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

Tactic:
simp [restrict_def]

Premises used: Set.restrict_def
-- Module: Mathlib.Analysis.Convex.Approximation
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
inst_9 : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
hs : s = ∅
⊢ Eq.{u_2 + 1} (α := (↑s : Type u_2) → ℝ) (sSup ∅) fun (x : (↑s : Type u_2)) ↦ φ (↑x : E)

Tactic:
grind
-- Module: Mathlib.Analysis.Convex.Approximation
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
inst_9 : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
obtain :
  ∀ (𝓕' : Set ((↑s : Type u_2) → ℝ))
    (h𝓕' :
      𝓕'.Countable ∧
        sSup 𝓕' = s.restrict (π := fun (a : E) ↦ ℝ) φ ∧
          ∀ f ∈ 𝓕',
            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),
    ∃ (l : ℕ → E →L[𝕜] 𝕜) (c : ℕ → ℝ),
      (∀ (i : ℕ),
          s.restrict (π := fun (a : E) ↦ ℝ)
                (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)) +
              const (↑s : Type u_2) (c i) ≤
            s.restrict (π := fun (a : E) ↦ ℝ) φ) ∧
        ⨆ (i : ℕ),
            s.restrict (π := fun (a : E) ↦ ℝ)
                (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)) +
              const (↑s : Type u_2) (c i) =
          s.restrict (π := fun (a : E) ↦ ℝ) φ
⊢ ∃ (l : ℕ → E →L[𝕜] 𝕜) (c : ℕ → ℝ),
    (∀ (i : ℕ),
        s.restrict (π := fun (a : E) ↦ ℝ)
              (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)) +
            const (↑s : Type u_2) (c i) ≤
          s.restrict (π := fun (a : E) ↦ ℝ) φ) ∧
      ⨆ (i : ℕ),
          s.restrict (π := fun (a : E) ↦ ℝ)
              (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)) +
            const (↑s : Type u_2) (c i) =
        s.restrict (π := fun (a : E) ↦ ℝ) φ

Tactic:
obtain ⟨𝓕', h𝓕'⟩ := hφcv.sSup_of_countable_affine_eq (𝕜 := 𝕜) hsc hφc

Premises used: ConvexOn.sSup_of_countable_affine_eq
-- Module: Mathlib.Analysis.Convex.Approximation
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
inst_9 : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
𝓕' : Set ((↑s : Type u_2) → ℝ)
h𝓕' :
  𝓕'.Countable ∧
    sSup 𝓕' = s.restrict (π := fun (a : E) ↦ ℝ) φ ∧
      ∀ f ∈ 𝓕',
        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
pos :
  ∀ (he : 𝓕'.Nonempty),
    ∃ (l : ℕ → E →L[𝕜] 𝕜) (c : ℕ → ℝ),
      (∀ (i : ℕ),
          s.restrict (π := fun (a : E) ↦ ℝ)
                (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)) +
              const (↑s : Type u_2) (c i) ≤
            s.restrict (π := fun (a : E) ↦ ℝ) φ) ∧
        ⨆ (i : ℕ),
            s.restrict (π := fun (a : E) ↦ ℝ)
                (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)) +
              const (↑s : Type u_2) (c i) =
          s.restrict (π := fun (a : E) ↦ ℝ) φ
neg :
  ∀ (he : 𝓕' = ∅),
    ∃ (l : ℕ → E →L[𝕜] 𝕜) (c : ℕ → ℝ),
      (∀ (i : ℕ),
          s.restrict (π := fun (a : E) ↦ ℝ)
                (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)) +
              const (↑s : Type u_2) (c i) ≤
            s.restrict (π := fun (a : E) ↦ ℝ) φ) ∧
        ⨆ (i : ℕ),
            s.restrict (π := fun (a : E) ↦ ℝ)
                (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)) +
              const (↑s : Type u_2) (c i) =
          s.restrict (π := fun (a : E) ↦ ℝ) φ
⊢ ∃ (l : ℕ → E →L[𝕜] 𝕜) (c : ℕ → ℝ),
    (∀ (i : ℕ),
        s.restrict (π := fun (a : E) ↦ ℝ)
              (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)) +
            const (↑s : Type u_2) (c i) ≤
          s.restrict (π := fun (a : E) ↦ ℝ) φ) ∧
      ⨆ (i : ℕ),
          s.restrict (π := fun (a : E) ↦ ℝ)
              (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)) +
            const (↑s : Type u_2) (c i) =
        s.restrict (π := fun (a : E) ↦ ℝ) φ

Tactic:
by_cases! he : 𝓕'.Nonempty

Premises used: Set.Nonempty
-- Module: Mathlib.Analysis.Convex.Approximation
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
inst_9 : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
𝓕' : Set ((↑s : Type u_2) → ℝ)
h𝓕' :
  𝓕'.Countable ∧
    sSup 𝓕' = s.restrict (π := fun (a : E) ↦ ℝ) φ ∧
      ∀ f ∈ 𝓕',
        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
he : 𝓕'.Nonempty
pos :
  ∀ (f : ℕ → (↑s : Type u_2) → ℝ) (hf : 𝓕' = range f),
    ∃ (l : ℕ → E →L[𝕜] 𝕜) (c : ℕ → ℝ),
      (∀ (i : ℕ),
          s.restrict (π := fun (a : E) ↦ ℝ)
                (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)) +
              const (↑s : Type u_2) (c i) ≤
            s.restrict (π := fun (a : E) ↦ ℝ) φ) ∧
        ⨆ (i : ℕ),
            s.restrict (π := fun (a : E) ↦ ℝ)
                (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)) +
              const (↑s : Type u_2) (c i) =
          s.restrict (π := fun (a : E) ↦ ℝ) φ
⊢ ∃ (l : ℕ → E →L[𝕜] 𝕜) (c : ℕ → ℝ),
    (∀ (i : ℕ),
        s.restrict (π := fun (a : E) ↦ ℝ)
              (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)) +
            const (↑s : Type u_2) (c i) ≤
          s.restrict (π := fun (a : E) ↦ ℝ) φ) ∧
      ⨆ (i : ℕ),
          s.restrict (π := fun (a : E) ↦ ℝ)
              (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)) +
            const (↑s : Type u_2) (c i) =
        s.restrict (π := fun (a : E) ↦ ℝ) φ

Tactic:
obtain ⟨f, hf⟩ := h𝓕'.1.exists_eq_range he

Premises used: And.left, Set.Countable.exists_eq_range
-- Module: Mathlib.Analysis.Convex.Approximation
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
inst_9 : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
𝓕' : Set ((↑s : Type u_2) → ℝ)
h𝓕' :
  𝓕'.Countable ∧
    sSup 𝓕' = s.restrict (π := fun (a : E) ↦ ℝ) φ ∧
      ∀ f ∈ 𝓕',
        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
he : 𝓕'.Nonempty
f : ℕ → (↑s : Type u_2) → ℝ
hf : 𝓕' = range f
i : ℕ
⊢ ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
    f i =
      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

Tactic:
simp_all
-- Module: Mathlib.Analysis.Convex.Approximation
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
inst_9 : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
𝓕' : Set ((↑s : Type u_2) → ℝ)
h𝓕' :
  𝓕'.Countable ∧
    sSup 𝓕' = s.restrict (π := fun (a : E) ↦ ℝ) φ ∧
      ∀ f ∈ 𝓕',
        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
he : 𝓕'.Nonempty
f : ℕ → (↑s : Type u_2) → ℝ
hf : 𝓕' = range f
⊢ ∀ (i : ℕ),
    ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
      f i =
        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

Tactic:
have (i : ℕ) : ∃ (l : E →L[𝕜] 𝕜) (c : ℝ), f i = s.restrict (re ∘ l) + const s c := by simp_all
-- Module: Mathlib.Analysis.Convex.Approximation
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
inst_9 : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
𝓕' : Set ((↑s : Type u_2) → ℝ)
h𝓕' :
  𝓕'.Countable ∧
    sSup 𝓕' = s.restrict (π := fun (a : E) ↦ ℝ) φ ∧
      ∀ f ∈ 𝓕',
        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
he : 𝓕'.Nonempty
f : ℕ → (↑s : Type u_2) → ℝ
hf : 𝓕' = range f
this :
  ∀ (i : ℕ),
    ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
      f i =
        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
pos :
  ∀ (l : (i : ℕ) → E →L[𝕜] 𝕜) (c : (i : ℕ) → ℝ)
    (hlc :
      ∀ (i : ℕ),
        f i =
          s.restrict (π := fun (a : E) ↦ ℝ)
              (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)) +
            const (↑s : Type u_2) (c i)),
    ∃ (l : ℕ → E →L[𝕜] 𝕜) (c : ℕ → ℝ),
      (∀ (i : ℕ),
          s.restrict (π := fun (a : E) ↦ ℝ)
                (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)) +
              const (↑s : Type u_2) (c i) ≤
            s.restrict (π := fun (a : E) ↦ ℝ) φ) ∧
        ⨆ (i : ℕ),
            s.restrict (π := fun (a : E) ↦ ℝ)
                (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)) +
              const (↑s : Type u_2) (c i) =
          s.restrict (π := fun (a : E) ↦ ℝ) φ
⊢ ∃ (l : ℕ → E →L[𝕜] 𝕜) (c : ℕ → ℝ),
    (∀ (i : ℕ),
        s.restrict (π := fun (a : E) ↦ ℝ)
              (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)) +
            const (↑s : Type u_2) (c i) ≤
          s.restrict (π := fun (a : E) ↦ ℝ) φ) ∧
      ⨆ (i : ℕ),
          s.restrict (π := fun (a : E) ↦ ℝ)
              (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)) +
            const (↑s : Type u_2) (c i) =
        s.restrict (π := fun (a : E) ↦ ℝ) φ

Tactic:
choose l c hlc using this
-- Module: Mathlib.Analysis.Convex.Approximation
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
inst_9 : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
𝓕' : Set ((↑s : Type u_2) → ℝ)
h𝓕' :
  𝓕'.Countable ∧
    sSup 𝓕' = s.restrict (π := fun (a : E) ↦ ℝ) φ ∧
      ∀ f ∈ 𝓕',
        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
he : 𝓕'.Nonempty
f : ℕ → (↑s : Type u_2) → ℝ
hf : 𝓕' = range f
l : (i : ℕ) → E →L[𝕜] 𝕜
c : (i : ℕ) → ℝ
hlc :
  ∀ (i : ℕ),
    f i =
      s.restrict (π := fun (a : E) ↦ ℝ)
          (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)) +
        const (↑s : Type u_2) (c i)
⊢ ∃ (l : ℕ → E →L[𝕜] 𝕜) (c : ℕ → ℝ),
    (∀ (i : ℕ),
        s.restrict (π := fun (a : E) ↦ ℝ)
              (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)) +
            const (↑s : Type u_2) (c i) ≤
          s.restrict (π := fun (a : E) ↦ ℝ) φ) ∧
      ⨆ (i : ℕ),
          s.restrict (π := fun (a : E) ↦ ℝ)
              (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)) +
            const (↑s : Type u_2) (c i) =
        s.restrict (π := fun (a : E) ↦ ℝ) φ

Tactic:
⟨l, c, fun i => (hlc i) ▸ (h𝓕'.2.2 (f i) (hf ▸ mem_range_self i)).1, ?_⟩

Premises used: Set.mem_range_self, Eq.rec, And.right, And.left, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Analysis.Convex.Approximation
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
inst_9 : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
𝓕' : Set ((↑s : Type u_2) → ℝ)
h𝓕' :
  𝓕'.Countable ∧
    sSup 𝓕' = s.restrict (π := fun (a : E) ↦ ℝ) φ ∧
      ∀ f ∈ 𝓕',
        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
he : 𝓕'.Nonempty
f : ℕ → (↑s : Type u_2) → ℝ
hf : 𝓕' = range f
l : (i : ℕ) → E →L[𝕜] 𝕜
c : (i : ℕ) → ℝ
hlc :
  ∀ (i : ℕ),
    f i =
      s.restrict (π := fun (a : E) ↦ ℝ)
          (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)) +
        const (↑s : Type u_2) (c i)
pos :
  ⨆ (i : ℕ),
      s.restrict (π := fun (a : E) ↦ ℝ)
          (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)) +
        const (↑s : Type u_2) (c i) =
    s.restrict (π := fun (a : E) ↦ ℝ) φ
⊢ ∃ (l : ℕ → E →L[𝕜] 𝕜) (c : ℕ → ℝ),
    (∀ (i : ℕ),
        s.restrict (π := fun (a : E) ↦ ℝ)
              (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)) +
            const (↑s : Type u_2) (c i) ≤
          s.restrict (π := fun (a : E) ↦ ℝ) φ) ∧
      ⨆ (i : ℕ),
          s.restrict (π := fun (a : E) ↦ ℝ)
              (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)) +
            const (↑s : Type u_2) (c i) =
        s.restrict (π := fun (a : E) ↦ ℝ) φ

Tactic:
refine ⟨l, c, fun i => (hlc i) ▸ (h𝓕'.2.2 (f i) (hf ▸ mem_range_self i)).1, ?_⟩
-- Module: Mathlib.Analysis.Convex.Approximation
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
inst_9 : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
𝓕' : Set ((↑s : Type u_2) → ℝ)
h𝓕' :
  𝓕'.Countable ∧
    sSup 𝓕' = s.restrict (π := fun (a : E) ↦ ℝ) φ ∧
      ∀ f ∈ 𝓕',
        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
he : 𝓕'.Nonempty
f : ℕ → (↑s : Type u_2) → ℝ
hf : 𝓕' = range f
l : (i : ℕ) → E →L[𝕜] 𝕜
c : (i : ℕ) → ℝ
hlc :
  ∀ (i : ℕ),
    f i =
      s.restrict (π := fun (a : E) ↦ ℝ)
          (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)) +
        const (↑s : Type u_2) (c i)
e_s :
  ∀ (i : ℕ) (x : (↑s : Type u_2)),
    HAdd.hAdd (α := (a : (↑s : Type u_2)) → ℝ) (β := (↑s : Type u_2) → ℝ)
        (s.restrict (π := fun (a : E) ↦ ℝ)
          (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)))
        (const (↑s : Type u_2) (c i)) x =
      f i x
⊢ Eq.{u_2 + 1} (α := (↑s : Type u_2) → ℝ)
    (⨆ (i : ℕ),
      s.restrict (π := fun (a : E) ↦ ℝ)
          (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)) +
        const (↑s : Type u_2) (c i))
    (⨆ (i : ℕ), f i)

Tactic:
congr with i x
-- Module: Mathlib.Analysis.Convex.Approximation
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
inst_9 : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
𝓕' : Set ((↑s : Type u_2) → ℝ)
h𝓕' :
  𝓕'.Countable ∧
    sSup 𝓕' = s.restrict (π := fun (a : E) ↦ ℝ) φ ∧
      ∀ f ∈ 𝓕',
        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
he : 𝓕'.Nonempty
f : ℕ → (↑s : Type u_2) → ℝ
hf : 𝓕' = range f
l : (i : ℕ) → E →L[𝕜] 𝕜
c : (i : ℕ) → ℝ
hlc :
  ∀ (i : ℕ),
    f i =
      s.restrict (π := fun (a : E) ↦ ℝ)
          (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)) +
        const (↑s : Type u_2) (c i)
i : ℕ
x : (↑s : Type u_2)
⊢ HAdd.hAdd (α := (a : (↑s : Type u_2)) → ℝ) (β := (↑s : Type u_2) → ℝ)
      (s.restrict (π := fun (a : E) ↦ ℝ)
        (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)))
      (const (↑s : Type u_2) (c i)) x =
    f i x

Tactic:
congrFun (hlc i).symm x

Premises used: congrFun, Eq.symm