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 φ
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) → ℝ)),
    𝓕'.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
have pos : ∀ (𝓕' : Set ((↑s : Type u_2) → ℝ)) (h𝓕' : 𝓕' ⊆ 𝓕 ∧ 𝓕'.Countable ∧ IsLUB 𝓕' (s.restrict (π := fun (a : E) ↦ ℝ) φ)),
  ∃ (𝓕' : 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: obtain ⟨𝓕', h𝓕'⟩ := exists_countable_lowerSemicontinuous_isLUB hr hl
-- 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 φ
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) ↦ ℝ) φ)
⊢ ∃ (𝓕' : 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
have pos : 𝓕'.Nonempty
Tactic: refine ⟨𝓕', h𝓕'.2.1, h𝓕'.2.2.csSup_eq ?_, fun f hf => h𝓕'.1 hf⟩
-- 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 φ
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) ↦ ℝ) φ)
⊢ 𝓕'.Nonempty
have pos : ∀ (this : 𝓕' = ∅), False
Tactic: by_contra!
-- 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 φ
hs : s = ∅
⊢ ∃ (𝓕' : 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
have 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
Tactic: use ∅
-- 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 φ
hs : s = ∅
⊢ 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
have h : Eq.{u_2 + 1} (α := (↑s : Type u_2) → ℝ) (sSup ∅) fun (x : (↑s : Type u_2)) ↦ φ (↑x : E)
Tactic: simp [restrict_def]
-- 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 φ
⊢ ∃ (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 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) ↦ ℝ) φ
Tactic: obtain ⟨𝓕', h𝓕'⟩ := hφcv.sSup_of_countable_affine_eq (𝕜 := 𝕜) hsc hφc
-- 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
⊢ ∃ (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 : ∀ (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) ↦ ℝ) φ
Tactic: by_cases! he : 𝓕'.Nonempty
-- 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
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) ↦ ℝ) φ
⊢ ∃ (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 : ∀ (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) ↦ ℝ) φ
Tactic: by_cases! he : 𝓕'.Nonempty
-- 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
⊢ ∃ (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 : ∀ (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) ↦ ℝ) φ
Tactic: obtain ⟨f, hf⟩ := h𝓕'.1.exists_eq_range he
-- 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 : 𝓕'.Nonempty
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) ↦ ℝ) φ
have 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
Tactic: have (i : ℕ) : ∃ (l : E →L[𝕜] 𝕜) (c : ℝ), f i = s.restrict (re ∘ l) + const s c := by simp_all
-- 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
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
⊢ ∃ (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 : ∀ (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: choose l c hlc using this
Cleared hypotheses: this
-- 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)
⊢ ∃ (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 : ℕ),
    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, ?_⟩
-- 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)
have 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
Tactic: congr with i x