awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Approximation
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
h1 : ∀ (y : ℝ), HMul.hMul (α := ℝ) ((l : (a : ℝ) → ℝ) 1 : ℝ) y = (l : (a : ℝ) → ℝ) y
y : ℝ
hy : y ∈ s
⊢ HMul.hMul (α := ℝ) ((l : (a : ℝ) → ℝ) 1 : ℝ) y + c' ≤ f y

Tactic:
simpa [h1] using hlc'_le ⟨y, hy⟩

Premises used: Subtype.mk
-- Module: Mathlib.Analysis.Convex.Approximation
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
h1 : ∀ (y : ℝ), HMul.hMul (α := ℝ) ((l : (a : ℝ) → ℝ) 1 : ℝ) y = (l : (a : ℝ) → ℝ) y
⊢ HMul.hMul (α := ℝ) ((l : (a : ℝ) → ℝ) 1 : ℝ) x + c' = a

Tactic:
simpa [h1] using hlc'_eq
-- Module: Mathlib.Analysis.Convex.Approximation
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
h1 : ∀ (y : ℝ), HMul.hMul (α := ℝ) ((l : (a : ℝ) → ℝ) 1 : ℝ) y = (l : (a : ℝ) → ℝ) y
⊢ ∃ (c : ℝ) (c' : ℝ), (∀ y ∈ s, c * y + c' ≤ f y) ∧ c * x + c' = a

Tactic:
exact ⟨l 1, c', fun y hy ↦ by simpa [h1] using hlc'_le ⟨y, hy⟩, by simpa [h1] using hlc'_eq⟩
-- Module: Mathlib.Analysis.Convex.Approximation
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
inr : ∀ (x : ℝ) (hxs : x ∈ s), ∃ (c : ℝ) (c' : ℝ), ∀ x ∈ s, c * x + c' ≤ f x
⊢ ∃ (c : ℝ) (c' : ℝ), ∀ x ∈ s, c * x + c' ≤ f x

Tactic:
rcases s.eq_empty_or_nonempty with rfl | ⟨x, hxs⟩

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
f : ℝ → ℝ
hsc : IsClosed (X := ℝ) ∅
hfc : LowerSemicontinuousOn f ∅
hf : ConvexOn ℝ ∅ f
⊢ ∃ (c : ℝ) (c' : ℝ), ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ∅ x → c * x + c' ≤ f x

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
s : Set ℝ
f : ℝ → ℝ
hsc : IsClosed s
hfc : LowerSemicontinuousOn f s
hf : ConvexOn ℝ s f
x : ℝ
hxs : x ∈ s
⊢ f x - 1 < f x

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
s : Set ℝ
f : ℝ → ℝ
hsc : IsClosed s
hfc : LowerSemicontinuousOn f s
hf : ConvexOn ℝ s f
x : ℝ
hxs : x ∈ s
inr : ∀ (c c' : ℝ) (hlc'_le : ∀ y ∈ s, c * y + c' ≤ f y), ∃ (c : ℝ) (c' : ℝ), ∀ x ∈ s, c * x + c' ≤ f x
⊢ ∃ (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

Premises used: ConvexOn.exists_affine_le_of_lt_real
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
s : Set ℝ
f : ℝ → ℝ
hsc : IsClosed s
hfc : LowerSemicontinuousOn f s
hf : ConvexOn ℝ s f
x : ℝ
hxs : x ∈ s
c c' : ℝ
hlc'_le : ∀ y ∈ s, c * y + c' ≤ f y
⊢ ∃ (c : ℝ) (c' : ℝ), ∀ x ∈ s, c * x + c' ≤ f x

Tactic:
⟨c, c', hlc'_le⟩

Premises used: Exists.intro
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
s : Set ℝ
f : ℝ → ℝ
hsc : IsClosed s
hfc : LowerSemicontinuousOn f s
hf : ConvexOn ℝ s f
x : ℝ
hxs : x ∈ s
c c' : ℝ
hlc'_le : ∀ y ∈ s, c * y + c' ≤ f y
⊢ ∃ (c : ℝ) (c' : ℝ), ∀ x ∈ s, c * x + c' ≤ f x

Tactic:
exact ⟨c, c', hlc'_le⟩
-- 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
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}
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
⊢ 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) ↦ ℝ) φ

Tactic:
ext 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
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

Tactic:
csSup_eq_of_forall_le_of_forall_lt_exists_gt ?_ (fun r ⟨f, hf⟩ => ?_) (fun r hr => ?_)

Premises used: iSup, _private.0.ConvexOn.sSup_affine_eq.match_1, LE.le, csSup_eq_of_forall_le_of_forall_lt_exists_gt, 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
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)
⊢ φ (↑x : E) - 1 < φ (↑x : E)

Tactic:
grind
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
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)
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)
⊢ 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

Premises used: ConvexOn.exists_affine_le_of_lt, Subtype.property
-- 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
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)
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:
⟨φ x - 1, hlc.2 ▸ ⟨⟨s.restrict (re ∘ l) + const s c, hlc.1, l, c, rfl⟩, rfl⟩⟩

Premises used: HSub.hSub, Set.Nonempty, Exists.intro, OfNat.ofNat, Subtype.val
-- 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
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)
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:
exact ⟨φ x - 1, hlc.2 ▸ ⟨⟨s.restrict (re ∘ l) + const s c, hlc.1, l, c, rfl⟩, rfl⟩⟩
-- 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
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 : ℝ
h :
  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)
    r
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)
hf :
  (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)
      f =
    r
⊢ r ≤ s.restrict (π := fun (a : E) ↦ ℝ) φ x

Tactic:
hf ▸ f.2.1 x

Premises used: Eq.rec, And.left, Subtype.property
-- 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
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 : ℝ
h :
  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)
    r
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)
hf :
  (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)
      f =
    r
⊢ r ≤ s.restrict (π := fun (a : E) ↦ ℝ) φ x

Tactic:
exact hf ▸ f.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
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
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
⊢ ∃ (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

Premises used: exists_between
-- 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
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
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
⊢ ∃ (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

Premises used: And.right, ConvexOn.exists_affine_le_of_lt, Subtype.property
-- 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
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
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:
⟨z, hlc.2 ▸ ⟨⟨s.restrict (re ∘ l) + const s c, hlc.1, l, c, rfl⟩, rfl⟩, hz.1⟩

Premises used: Function.comp, Eq.rec, Set.Elem, Subtype.mk, And.right, And.left, HAdd.hAdd, And.intro, Exists.intro, RCLike.re, Function.const, Set.restrict, DFunLike.coe, rfl
-- 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
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
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:
exact ⟨z, hlc.2 ▸ ⟨⟨s.restrict (re ∘ l) + const s c, hlc.1, l, c, rfl⟩, rfl⟩, hz.1⟩