awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
inst_9 : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
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
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
⊢ ∃ (𝓕' : 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

Premises used: Set.Nonempty
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
inst_9 : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
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) ↦ ℝ) φ)

Tactic:
(hφcv.sSup_affine_eq (𝕜 := 𝕜) hsc hφc) ▸ isLUB_csSup ?_ ?_

Premises used: Eq.rec, isLUB_csSup, ConvexOn.sSup_affine_eq
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
inst_9 : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
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
refine_2 : BddAbove 𝓕
⊢ IsLUB 𝓕 (s.restrict (π := fun (a : E) ↦ ℝ) φ)

Tactic:
refine (hφcv.sSup_affine_eq (𝕜 := 𝕜) hsc hφc) ▸ isLUB_csSup ?_ ?_
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
inst_9 : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
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}
⊢ φ (hs.some (s := s)) - 1 < φ (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ s) (hs.some (s := s)) ⋯) : 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
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 :
  ∀ (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
⊢ 𝓕.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

Premises used: Set.Nonempty.some_mem, ConvexOn.exists_affine_le_of_lt
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
inst_9 : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
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}
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:
⟨s.restrict (re ∘ l) + const s c, hlc.1, l, c, rfl⟩

Premises used: Function.comp, Set.Elem, Set.Nonempty, 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
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}
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:
exact ⟨s.restrict (re ∘ l) + const s c, hlc.1, l, c, 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
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}
⊢ BddAbove 𝓕

Tactic:
(bddAbove_def.2 ⟨φ ∘ Subtype.val, fun y hy => hy.1⟩)

Premises used: Iff.mpr, Function.comp, And.left, Exists.intro, bddAbove_def, 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
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}
⊢ BddAbove 𝓕

Tactic:
exact (bddAbove_def.2 ⟨φ ∘ Subtype.val, fun y hy => hy.1⟩)

Premises used: Iff.mpr, Function.comp, Exists.intro, bddAbove_def, 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
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) ↦ ℝ) φ)

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⟩)
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
inst_9 : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
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 ∈ 𝓕
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
⊢ LowerSemicontinuous f

Tactic:
obtain ⟨l, c, hlc⟩ := hf.2

Premises used: And.right
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
inst_9 : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
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 ∈ 𝓕
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
⊢ Continuous
    (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:
fun_prop
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
inst_9 : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
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 ∈ 𝓕
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:
exact Continuous.lowerSemicontinuous (hlc ▸ by fun_prop)

Premises used: Continuous.lowerSemicontinuous
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
inst_9 : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
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

Tactic:
have hr (f) (hf : f ∈ 𝓕) : LowerSemicontinuous f := by
      obtain ⟨l, c, hlc⟩ := hf.2
      exact Continuous.lowerSemicontinuous (hlc ▸ by fun_prop)
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
inst_9 : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
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
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
⊢ ∃ (𝓕' : 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

Premises used: exists_countable_lowerSemicontinuous_isLUB
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
inst_9 : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
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

Tactic:
⟨𝓕', h𝓕'.2.1, h𝓕'.2.2.csSup_eq ?_, fun f hf => h𝓕'.1 hf⟩

Premises used: And.right, And.left, IsLUB.csSup_eq, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
inst_9 : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
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) ↦ ℝ) φ)
pos : 𝓕'.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:
refine ⟨𝓕', h𝓕'.2.1, h𝓕'.2.2.csSup_eq ?_, fun f hf => h𝓕'.1 hf⟩
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
inst_9 : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
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) ↦ ℝ) φ)
pos : ∀ (this : 𝓕' = ∅), False
⊢ 𝓕'.Nonempty

Tactic:
by_contra!