awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (hypothesis)
Goal:
s : Set ℝ
f : ℝ → ℝ
x a : ℝ
hx : x ∈ s
hax : a < f x
hsc : IsClosed s
hfc : LowerSemicontinuousOn f s
hf : ConvexOn ℝ s f
l : ℝ →L[ℝ] ℝ
c' : ℝ
hlc'_le :
  s.restrict (π := fun (a : ℝ) ↦ ℝ) (Function.comp (β := ℝ) (⇑re : (a : ℝ) → ℝ) (⇑l : (a : ℝ) → ℝ)) +
      const (↑s : Type) c' ≤
    s.restrict (π := fun (a : ℝ) ↦ ℝ) f
hlc'_eq : HAdd.hAdd (α := ℝ) ((re : (a : ℝ) → ℝ) ((l : (a : ℝ) → ℝ) x : ℝ) : ℝ) c' = a
⊢ ∃ (c : ℝ) (c' : ℝ), (∀ y ∈ s, c * y + c' ≤ f y) ∧ c * x + c' = a
have h1 : ∀ (y : ℝ), HMul.hMul (α := ℝ) ((l : (a : ℝ) → ℝ) 1 : ℝ) y = (l : (a : ℝ) → ℝ) y
Tactic: have h1 y : l 1 * y = l y := by rw [mul_comm, ← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
Goal:
s : Set ℝ
f : ℝ → ℝ
hsc : IsClosed s
hfc : LowerSemicontinuousOn f s
hf : ConvexOn ℝ s f
⊢ ∃ (c : ℝ) (c' : ℝ), ∀ x ∈ s, c * x + c' ≤ f x
have inl : ∀ (hsc : IsClosed (X := ℝ) ∅) (hfc : LowerSemicontinuousOn f ∅) (hf : ConvexOn ℝ ∅ f),
  ∃ (c : ℝ) (c' : ℝ), ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ∅ x → c * x + c' ≤ f x
Tactic: rcases s.eq_empty_or_nonempty with rfl | ⟨x, hxs⟩
Cleared hypotheses: s, hsc, hfc, hf
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
Goal:
s : Set ℝ
f : ℝ → ℝ
hsc : IsClosed s
hfc : LowerSemicontinuousOn f s
hf : ConvexOn ℝ s f
inl :
  ∀ (hsc : IsClosed (X := ℝ) ∅) (hfc : LowerSemicontinuousOn f ∅) (hf : ConvexOn ℝ ∅ f),
    ∃ (c : ℝ) (c' : ℝ), ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ∅ x → c * x + c' ≤ f x
⊢ ∃ (c : ℝ) (c' : ℝ), ∀ x ∈ s, c * x + c' ≤ f x
have inr : ∀ (x : ℝ) (hxs : x ∈ s), ∃ (c : ℝ) (c' : ℝ), ∀ x ∈ s, c * x + c' ≤ f x
Tactic: rcases s.eq_empty_or_nonempty with rfl | ⟨x, hxs⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
Goal:
s : Set ℝ
f : ℝ → ℝ
hsc : IsClosed s
hfc : LowerSemicontinuousOn f s
hf : ConvexOn ℝ s f
x : ℝ
hxs : x ∈ s
⊢ ∃ (c : ℝ) (c' : ℝ), ∀ x ∈ s, c * x + c' ≤ f x
have inr : ∀ (c c' : ℝ) (hlc'_le : ∀ y ∈ s, c * y + c' ≤ f y), ∃ (c : ℝ) (c' : ℝ), ∀ x ∈ s, c * x + c' ≤ f x
Tactic: obtain ⟨c, c', hlc'_le, -⟩ :=
    hf.exists_affine_le_of_lt_real (a := f x - 1) hxs (by simp) hsc hfc
-- 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
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
⊢ sSup
      {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} =
    s.restrict (π := fun (a : E) ↦ ℝ) φ
have h : ∀ (x : (↑s : Type u_2)),
  sSup
      {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}
      x =
    s.restrict (π := fun (a : E) ↦ ℝ) φ x
Tactic: ext x
-- 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
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
x : (↑s : Type u_2)
⊢ ⨆ (f :
      (↑{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} :
        Type u_2)),
      (↑f : (a : (↑s : Type u_2)) → ℝ) x =
    s.restrict (π := fun (a : E) ↦ ℝ) φ x
have h : Set.Nonempty (α := ℝ)
  (range
    fun
      (f :
        (↑{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} :
          Type u_2)) ↦
    (↑f : (a : (↑s : Type u_2)) → ℝ) x)
Tactic: refine csSup_eq_of_forall_le_of_forall_lt_exists_gt ?_ (fun r ⟨f, hf⟩ => ?_) (fun r hr => ?_)
-- 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
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
x : (↑s : Type u_2)
⊢ Set.Nonempty (α := ℝ)
    (range
      fun
        (f :
          (↑{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} :
            Type u_2)) ↦
      (↑f : (a : (↑s : Type u_2)) → ℝ) x)
have h : ∀ (l : E →L[𝕜] 𝕜) (c : ℝ)
  (hlc :
    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 ≤
        s.restrict (π := fun (a : E) ↦ ℝ) φ ∧
      HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) (↑x : E) : 𝕜) : ℝ) c = φ (↑x : E) - 1),
  Set.Nonempty (α := ℝ)
    (range
      fun
        (f :
          (↑{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} :
            Type u_2)) ↦
      (↑f : (a : (↑s : Type u_2)) → ℝ) x)
Tactic: obtain ⟨l, c, hlc⟩ := exists_affine_le_of_lt (𝕜 := 𝕜) x.2 (show φ x - 1 < φ x from by grind)
      hsc hφc hφcv
-- 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
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
x : (↑s : Type u_2)
r : ℝ
hr : r < s.restrict (π := fun (a : E) ↦ ℝ) φ x
⊢ ∃ (a : ℝ),
    Membership.mem (γ := Set ℝ)
        (range
          fun
            (f :
              (↑{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} :
                Type u_2)) ↦
          (↑f : (a : (↑s : Type u_2)) → ℝ) x)
        a ∧
      r < a
have h : ∀ (z : ℝ) (hz : r < z ∧ z < s.restrict (π := fun (a : E) ↦ ℝ) φ x),
  ∃ (a : ℝ),
    Membership.mem (γ := Set ℝ)
        (range
          fun
            (f :
              (↑{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} :
                Type u_2)) ↦
          (↑f : (a : (↑s : Type u_2)) → ℝ) x)
        a ∧
      r < a
Tactic: obtain ⟨z, hz⟩ := exists_between hr
-- 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
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
x : (↑s : Type u_2)
r : ℝ
hr : r < s.restrict (π := fun (a : E) ↦ ℝ) φ x
z : ℝ
hz : r < z ∧ z < s.restrict (π := fun (a : E) ↦ ℝ) φ x
⊢ ∃ (a : ℝ),
    Membership.mem (γ := Set ℝ)
        (range
          fun
            (f :
              (↑{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} :
                Type u_2)) ↦
          (↑f : (a : (↑s : Type u_2)) → ℝ) x)
        a ∧
      r < a
have h : ∀ (l : E →L[𝕜] 𝕜) (c : ℝ)
  (hlc :
    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 ≤
        s.restrict (π := fun (a : E) ↦ ℝ) φ ∧
      HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) (↑x : E) : 𝕜) : ℝ) c = z),
  ∃ (a : ℝ),
    Membership.mem (γ := Set ℝ)
        (range
          fun
            (f :
              (↑{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} :
                Type u_2)) ↦
          (↑f : (a : (↑s : Type u_2)) → ℝ) x)
        a ∧
      r < a
Tactic: obtain ⟨l, c, hlc⟩ := exists_affine_le_of_lt (𝕜 := 𝕜) x.2 hz.2 hsc hφc hφcv
-- 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) → ℝ)),
    𝓕'.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 : ∀ (hs : s.Nonempty),
  ∃ (𝓕' : 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: by_cases! hs : s.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 φ
pos :
  ∀ (hs : s.Nonempty),
    ∃ (𝓕' : 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
⊢ ∃ (𝓕' : 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 neg : ∀ (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
Tactic: by_cases! hs : s.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 φ
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}
⊢ IsLUB 𝓕 (s.restrict (π := fun (a : E) ↦ ℝ) φ)
have refine_1 : 𝓕.Nonempty
Tactic: refine (hφcv.sSup_affine_eq (𝕜 := 𝕜) hsc hφc) ▸ isLUB_csSup ?_ ?_
-- 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}
refine_1 : 𝓕.Nonempty
⊢ IsLUB 𝓕 (s.restrict (π := fun (a : E) ↦ ℝ) φ)
have refine_2 : BddAbove 𝓕
Tactic: refine (hφcv.sSup_affine_eq (𝕜 := 𝕜) hsc hφc) ▸ isLUB_csSup ?_ ?_
-- 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}
⊢ 𝓕.Nonempty
have refine_1 : ∀ (l : E →L[𝕜] 𝕜) (c : ℝ)
  (hlc :
    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 ≤
        s.restrict (π := fun (a : E) ↦ ℝ) φ ∧
      HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) (hs.some (s := s)) : 𝕜) : ℝ) c =
        φ (hs.some (s := s)) - 1),
  𝓕.Nonempty
Tactic: obtain ⟨l, c, hlc⟩ := exists_affine_le_of_lt (𝕜 := 𝕜) hs.some_mem
          (by grind : φ hs.some - 1 < φ (⟨hs.some, hs.some_mem⟩ : s)) hsc hφc hφcv
-- 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 φ
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}
⊢ ∃ (𝓕' : 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 hl : IsLUB 𝓕 (s.restrict (π := fun (a : E) ↦ ℝ) φ)
Tactic: have hl : IsLUB 𝓕 (s.restrict φ) := by
      refine (hφcv.sSup_affine_eq (𝕜 := 𝕜) hsc hφc) ▸ isLUB_csSup ?_ ?_
      · obtain ⟨l, c, hlc⟩ := exists_affine_le_of_lt (𝕜 := 𝕜) hs.some_mem
          (by grind : φ hs.some - 1 < φ (⟨hs.some, hs.some_mem⟩ : s)) hsc hφc hφcv
        exact ⟨s.restrict (re ∘ l) + const s c, hlc.1, l, c, rfl⟩
      · exact (bddAbove_def.2 ⟨φ ∘ Subtype.val, fun y hy => hy.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 φ
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) ↦ ℝ) φ)
f : (a : (↑s : Type u_2)) → ℝ
hf : f ∈ 𝓕
⊢ LowerSemicontinuous f
have obtain : ∀ (l : E →L[𝕜] 𝕜) (c : ℝ)
  (hlc :
    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),
  LowerSemicontinuous f
Tactic: obtain ⟨l, c, hlc⟩ := hf.2
-- 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 φ
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) ↦ ℝ) φ)
⊢ ∃ (𝓕' : 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 hr : ∀ (f : (a : (↑s : Type u_2)) → ℝ) (hf : f ∈ 𝓕), LowerSemicontinuous f
Tactic: have hr (f) (hf : f ∈ 𝓕) : LowerSemicontinuous f := by
      obtain ⟨l, c, hlc⟩ := hf.2
      exact Continuous.lowerSemicontinuous (hlc ▸ by fun_prop)