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 φ
𝓕' : 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:
exact congrFun (hlc i).symm x

Premises used: congrFun, 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)
rw : sSup (range fun (i : ℕ) ↦ f i) = s.restrict (π := fun (a : E) ↦ ℝ) φ
rw₁ : sSup 𝓕' = s.restrict (π := fun (a : E) ↦ ℝ) φ
rw₂ rw₃ : s.restrict (π := fun (a : E) ↦ ℝ) φ = s.restrict (π := fun (a : E) ↦ ℝ) φ
⊢ ⨆ (i : ℕ), f i = s.restrict (π := fun (a : E) ↦ ℝ) φ

Tactic:
rw [← sSup_range, ← hf, h𝓕'.2.1]

Premises used: And.right, And.left, sSup_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
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)
_ :
  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)
_₁ : ⨆ (i : ℕ), f 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:
calc
    _ = ⨆ i, f i := by congr with i x; exact congrFun (hlc i).symm x
    _ = _ := by rw [← sSup_range, ← hf, h𝓕'.2.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 : 𝓕' = ∅
pos :
  ∀ (hsφ : s.restrict (π := fun (a : E) ↦ ℝ) φ = 0),
    ∃ (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 :
  ∀ (hsφ : s.restrict (π := fun (a : E) ↦ ℝ) φ ≠ 0),
    ∃ (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! hsφ : s.restrict φ = 0

Premises used: Set.restrict
-- 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 : 𝓕' = ∅
hsφ : s.restrict (π := fun (a : E) ↦ ℝ) φ = 0
⊢ ∀ (a : (↑s : Type u_2)), s.restrict (π := fun (a : E) ↦ ℝ) φ a = 0 a

Tactic:
have := congrFun hsφ
-- 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 : 𝓕' = ∅
hsφ : s.restrict (π := fun (a : E) ↦ ℝ) φ = 0
this : ∀ (a : (↑s : Type u_2)), s.restrict (π := fun (a : E) ↦ ℝ) φ a = 0 a
⊢ ∃ (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:
⟨fun _ => 0, fun _ => 0, ?_, ?_⟩

Premises used: And.intro, Exists.intro, OfNat.ofNat
-- 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 : 𝓕' = ∅
hsφ : s.restrict (π := fun (a : E) ↦ ℝ) φ = 0
this : ∀ (a : (↑s : Type u_2)), s.restrict (π := fun (a : E) ↦ ℝ) φ a = 0 a
pos :
  ∀ (i : ℕ),
    HAdd.hAdd (α := (a : (↑s : Type u_2)) → ℝ)
        (s.restrict (π := fun (a : E) ↦ ℝ)
          (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ)
            (⇑((fun (x : ℕ) ↦ (0 : E →L[𝕜] 𝕜)) i) : (a : E) → 𝕜)))
        (const (↑s : Type u_2) ((fun (x : ℕ) ↦ (0 : ℝ)) i)) ≤
      s.restrict (π := fun (a : E) ↦ ℝ) φ
pos₁ :
  ⨆ (i : ℕ),
      HAdd.hAdd (α := (a : (↑s : Type u_2)) → ℝ)
        (s.restrict (π := fun (a : E) ↦ ℝ)
          (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ)
            (⇑((fun (x : ℕ) ↦ (0 : E →L[𝕜] 𝕜)) i) : (a : E) → 𝕜)))
        (const (↑s : Type u_2) ((fun (x : ℕ) ↦ (0 : ℝ)) 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 ⟨fun _ => 0, fun _ => 0, ?_, ?_⟩
-- 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 : 𝓕' = ∅
hsφ : s.restrict (π := fun (a : E) ↦ ℝ) φ = 0
this : ∀ (a : (↑s : Type u_2)), s.restrict (π := fun (a : E) ↦ ℝ) φ a = 0 a
⊢ ∀ (i : ℕ),
    HAdd.hAdd (α := (a : (↑s : Type u_2)) → ℝ)
        (s.restrict (π := fun (a : E) ↦ ℝ)
          (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ)
            (⇑((fun (x : ℕ) ↦ (0 : E →L[𝕜] 𝕜)) i) : (a : E) → 𝕜)))
        (const (↑s : Type u_2) ((fun (x : ℕ) ↦ (0 : ℝ)) i)) ≤
      s.restrict (π := fun (a : E) ↦ ℝ) φ

Tactic:
simp_all [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 φ
𝓕' : 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 : 𝓕' = ∅
hsφ : s.restrict (π := fun (a : E) ↦ ℝ) φ = 0
this : ∀ (a : (↑s : Type u_2)), s.restrict (π := fun (a : E) ↦ ℝ) φ a = 0 a
pos :
  ∀ (x : (↑s : Type u_2)),
    (⨆ (i : ℕ),
          HAdd.hAdd (α := (a : (↑s : Type u_2)) → ℝ)
            (s.restrict (π := fun (a : E) ↦ ℝ)
              (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ)
                (⇑((fun (x : ℕ) ↦ (0 : E →L[𝕜] 𝕜)) i) : (a : E) → 𝕜)))
            (const (↑s : Type u_2) ((fun (x : ℕ) ↦ (0 : ℝ)) i)))
        x =
      s.restrict (π := fun (a : E) ↦ ℝ) φ x
⊢ ⨆ (i : ℕ),
      HAdd.hAdd (α := (a : (↑s : Type u_2)) → ℝ)
        (s.restrict (π := fun (a : E) ↦ ℝ)
          (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ)
            (⇑((fun (x : ℕ) ↦ (0 : E →L[𝕜] 𝕜)) i) : (a : E) → 𝕜)))
        (const (↑s : Type u_2) ((fun (x : ℕ) ↦ (0 : ℝ)) i)) =
    s.restrict (π := fun (a : E) ↦ ℝ) φ

Tactic:
ext
-- 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 : 𝓕' = ∅
hsφ : s.restrict (π := fun (a : E) ↦ ℝ) φ = 0
this : ∀ (a : (↑s : Type u_2)), s.restrict (π := fun (a : E) ↦ ℝ) φ a = 0 a
x : (↑s : Type u_2)
⊢ (⨆ (i : ℕ),
        HAdd.hAdd (α := (a : (↑s : Type u_2)) → ℝ)
          (s.restrict (π := fun (a : E) ↦ ℝ)
            (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ)
              (⇑((fun (x : ℕ) ↦ (0 : E →L[𝕜] 𝕜)) i) : (a : E) → 𝕜)))
          (const (↑s : Type u_2) ((fun (x : ℕ) ↦ (0 : ℝ)) i)))
      x =
    s.restrict (π := fun (a : E) ↦ ℝ) φ x

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 : 𝓕' = ∅
hsφ : s.restrict (π := fun (a : E) ↦ ℝ) φ ≠ 0
neg :
  ∀ (x : (↑s : Type u_2)) (hx : s.restrict (π := fun (a : E) ↦ ℝ) φ x ≠ 0 x),
    ∃ (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 ⟨x, hx⟩ := Function.ne_iff.1 hsφ

Premises used: Function.ne_iff, Iff.mp
-- 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 : 𝓕' = ∅
hsφ : s.restrict (π := fun (a : E) ↦ ℝ) φ ≠ 0
x : (↑s : Type u_2)
hx : s.restrict (π := fun (a : E) ↦ ℝ) φ x ≠ 0 x
⊢ sSup 𝓕' x = s.restrict (π := fun (a : E) ↦ ℝ) φ x

Tactic:
have := congrFun h𝓕'.2.1 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 : 𝓕' = ∅
hsφ : s.restrict (π := fun (a : E) ↦ ℝ) φ ≠ 0
x : (↑s : Type u_2)
hx : s.restrict (π := fun (a : E) ↦ ℝ) φ x ≠ 0 x
this : sSup 𝓕' x = s.restrict (π := fun (a : E) ↦ ℝ) φ x
⊢ s = ∅

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 : 𝓕' = ∅
hsφ : s.restrict (π := fun (a : E) ↦ ℝ) φ ≠ 0
x : (↑s : Type u_2)
hx : s.restrict (π := fun (a : E) ↦ ℝ) φ x ≠ 0 x
⊢ s = ∅

Tactic:
have : s = ∅ := by have := congrFun h𝓕'.2.1 x; 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 : 𝓕' = ∅
hsφ : s.restrict (π := fun (a : E) ↦ ℝ) φ ≠ 0
x : (↑s : Type u_2)
hx : s.restrict (π := fun (a : E) ↦ ℝ) φ x ≠ 0 x
this : s = ∅
⊢ ∃ (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:
grind