awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
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 : ℕ), f i = s.restrict (π := fun (a : E) ↦ ℝ) φ
have rw : sSup (range fun (i : ℕ) ↦ f i) = s.restrict (π := fun (a : E) ↦ ℝ) φ
Tactic: rw [← sSup_range, ← hf, h𝓕'.2.1]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
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) ↦ ℝ) φ
⊢ ⨆ (i : ℕ), f i = s.restrict (π := fun (a : E) ↦ ℝ) φ
have rw₁ : sSup 𝓕' = s.restrict (π := fun (a : E) ↦ ℝ) φ
Tactic: rw [← sSup_range, ← hf, h𝓕'.2.1]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
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) ↦ ℝ) φ
⊢ ⨆ (i : ℕ), f i = s.restrict (π := fun (a : E) ↦ ℝ) φ
have rw₂ : s.restrict (π := fun (a : E) ↦ ℝ) φ = s.restrict (π := fun (a : E) ↦ ℝ) φ
Tactic: rw [← sSup_range, ← hf, h𝓕'.2.1]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
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 : ℕ),
      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) ↦ ℝ) φ
have _ : 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: calc
    _ = ⨆ i, f i := by congr with i x; exact congrFun (hlc i).symm x
    _ = _ := by rw [← sSup_range, ← hf, h𝓕'.2.1]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
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 : ℕ),
      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) ↦ ℝ) φ
have _₁ : ⨆ (i : ℕ), f 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
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 : 𝓕' = ∅
⊢ ∃ (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) ↦ ℝ) φ
have 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) ↦ ℝ) φ
Tactic: by_cases! hsφ : s.restrict φ = 0
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
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) ↦ ℝ) φ
⊢ ∃ (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) ↦ ℝ) φ
have 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) ↦ ℝ) φ
Tactic: by_cases! hsφ : s.restrict φ = 0
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (hypothesis)
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
⊢ ∃ (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) ↦ ℝ) φ
have this : ∀ (a : (↑s : Type u_2)), s.restrict (π := fun (a : E) ↦ ℝ) φ a = 0 a
Tactic: have := congrFun hsφ
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
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) ↦ ℝ) φ
have 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) ↦ ℝ) φ
Tactic: refine ⟨fun _ => 0, fun _ => 0, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
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) ↦ ℝ) φ
⊢ ∃ (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) ↦ ℝ) φ
have 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) ↦ ℝ) φ
Tactic: refine ⟨fun _ => 0, fun _ => 0, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
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) ↦ ℝ) φ
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
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
⊢ ∃ (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) ↦ ℝ) φ
have 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) ↦ ℝ) φ
Tactic: obtain ⟨x, hx⟩ := Function.ne_iff.1 hsφ
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (hypothesis)
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 = ∅
have this : sSup 𝓕' x = s.restrict (π := fun (a : E) ↦ ℝ) φ x
Tactic: have := congrFun h𝓕'.2.1 x