awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
φ : 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
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set (E → ℝ) :=
  {f : E → ℝ |
    f ≤ φ ∧
      ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
        f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c}
⊢ BddAbove 𝓕

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

Premises used: Iff.mpr, Exists.intro, bddAbove_def
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
φ : 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
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set (E → ℝ) :=
  {f : E → ℝ |
    f ≤ φ ∧
      ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
        f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c}
⊢ IsLUB 𝓕 φ

Tactic:
have hl : IsLUB 𝓕 φ := by
    refine (hφcv.univ_sSup_affine_eq (𝕜 := 𝕜) hφc) ▸ isLUB_csSup ?_ ?_
    · obtain ⟨l, c, hlc⟩ := exists_affine_le_of_lt (𝕜 := 𝕜) (@mem_univ E 0)
        (by grind : φ 0 - 1 < φ (⟨0, @mem_univ E 0⟩ : univ)) isClosed_univ
        (lowerSemicontinuousOn_univ_iff.2 hφc) hφcv
      exact ⟨(re ∘ l) + const E c, fun x => hlc.1 ⟨x, mem_univ x⟩, ⟨l, c, rfl⟩⟩
    · exact (bddAbove_def.2 ⟨φ, fun y hy => hy.1⟩)
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
φ : 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
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set (E → ℝ) :=
  {f : E → ℝ |
    f ≤ φ ∧
      ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
        f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c}
hl : IsLUB 𝓕 φ
f : E → ℝ
hf : f ∈ 𝓕
obtain :
  ∀ (l : E →L[𝕜] 𝕜) (c : ℝ)
    (hlc : f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E 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
φ : 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
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set (E → ℝ) :=
  {f : E → ℝ |
    f ≤ φ ∧
      ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
        f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c}
hl : IsLUB 𝓕 φ
f : E → ℝ
hf : f ∈ 𝓕
l : E →L[𝕜] 𝕜
c : ℝ
hlc : f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c
rw : Continuous (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c)
⊢ Continuous f

Tactic:
rw [hlc]
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
φ : 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
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set (E → ℝ) :=
  {f : E → ℝ |
    f ≤ φ ∧
      ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
        f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c}
hl : IsLUB 𝓕 φ
f : E → ℝ
hf : f ∈ 𝓕
l : E →L[𝕜] 𝕜
c : ℝ
hlc : f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c
⊢ Continuous (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
φ : 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
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set (E → ℝ) :=
  {f : E → ℝ |
    f ≤ φ ∧
      ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
        f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c}
hl : IsLUB 𝓕 φ
f : E → ℝ
hf : f ∈ 𝓕
l : E →L[𝕜] 𝕜
c : ℝ
hlc : f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c
⊢ LowerSemicontinuous f

Tactic:
exact Continuous.lowerSemicontinuous (by rw [hlc]; fun_prop)

Premises used: Continuous.lowerSemicontinuous
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
φ : 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
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set (E → ℝ) :=
  {f : E → ℝ |
    f ≤ φ ∧
      ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
        f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c}
hl : IsLUB 𝓕 φ
⊢ ∀ (f : E → ℝ) (hf : f ∈ 𝓕), LowerSemicontinuous f

Tactic:
have hr (f) (hf : f ∈ 𝓕) : LowerSemicontinuous f := by
    obtain ⟨l, c, hlc⟩ := hf.2
    exact Continuous.lowerSemicontinuous (by rw [hlc]; fun_prop)
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
φ : 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
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set (E → ℝ) :=
  {f : E → ℝ |
    f ≤ φ ∧
      ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
        f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c}
hl : IsLUB 𝓕 φ
hr : ∀ (f : E → ℝ) (hf : f ∈ 𝓕), LowerSemicontinuous f
obtain :
  ∀ (𝓕' : Set (E → ℝ)) (h𝓕' : 𝓕' ⊆ 𝓕 ∧ 𝓕'.Countable ∧ IsLUB 𝓕' φ),
    ∃ (𝓕' : Set (E → ℝ)),
      𝓕'.Countable ∧
        sSup 𝓕' = φ ∧
          ∀ f ∈ 𝓕',
            f ≤ φ ∧
              ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
                f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c
⊢ ∃ (𝓕' : Set (E → ℝ)),
    𝓕'.Countable ∧
      sSup 𝓕' = φ ∧
        ∀ f ∈ 𝓕',
          f ≤ φ ∧
            ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
              f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E 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
φ : 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
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set (E → ℝ) :=
  {f : E → ℝ |
    f ≤ φ ∧
      ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
        f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c}
hl : IsLUB 𝓕 φ
hr : ∀ (f : E → ℝ) (hf : f ∈ 𝓕), LowerSemicontinuous f
𝓕' : Set (E → ℝ)
h𝓕' : 𝓕' ⊆ 𝓕 ∧ 𝓕'.Countable ∧ IsLUB 𝓕' φ
⊢ ∃ (𝓕' : Set (E → ℝ)),
    𝓕'.Countable ∧
      sSup 𝓕' = φ ∧
        ∀ f ∈ 𝓕',
          f ≤ φ ∧
            ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
              f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E 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
φ : 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
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set (E → ℝ) :=
  {f : E → ℝ |
    f ≤ φ ∧
      ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
        f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c}
hl : IsLUB 𝓕 φ
hr : ∀ (f : E → ℝ) (hf : f ∈ 𝓕), LowerSemicontinuous f
𝓕' : Set (E → ℝ)
h𝓕' : 𝓕' ⊆ 𝓕 ∧ 𝓕'.Countable ∧ IsLUB 𝓕' φ
refine : 𝓕'.Nonempty
⊢ ∃ (𝓕' : Set (E → ℝ)),
    𝓕'.Countable ∧
      sSup 𝓕' = φ ∧
        ∀ f ∈ 𝓕',
          f ≤ φ ∧
            ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
              f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E 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
φ : 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
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set (E → ℝ) :=
  {f : E → ℝ |
    f ≤ φ ∧
      ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
        f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c}
hl : IsLUB 𝓕 φ
hr : ∀ (f : E → ℝ) (hf : f ∈ 𝓕), LowerSemicontinuous f
𝓕' : Set (E → ℝ)
h𝓕' : 𝓕' ⊆ 𝓕 ∧ 𝓕'.Countable ∧ IsLUB 𝓕' φ
by_contra! : ∀ (this : 𝓕' = ∅), False
⊢ 𝓕'.Nonempty

Tactic:
by_contra!
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
φ : 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
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set (E → ℝ) :=
  {f : E → ℝ |
    f ≤ φ ∧
      ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
        f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c}
hl : IsLUB 𝓕 φ
hr : ∀ (f : E → ℝ) (hf : f ∈ 𝓕), LowerSemicontinuous f
𝓕' : Set (E → ℝ)
h𝓕' : 𝓕' ⊆ 𝓕 ∧ 𝓕'.Countable ∧ IsLUB 𝓕' φ
this : 𝓕' = ∅
⊢ False

Tactic:
grind [(isLUB_empty_iff.1 (this ▸ h𝓕'.2.2)) (fun x => φ x - 1) 0]

Premises used: HSub.hSub, Iff.mp, isLUB_empty_iff, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
φ : 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
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
obtain :
  ∀ (l : ℕ → E →L[𝕜] 𝕜) (c : ℕ → ℝ)
    (hle :
      ∀ (i : ℕ),
        HAdd.hAdd (α := (a : (↑univ : Type u_2)) → ℝ)
            (Set.restrict (π := fun (a : E) ↦ ℝ) univ
              (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)))
            (const (↑univ : Type u_2) (c i)) ≤
          Set.restrict (π := fun (a : E) ↦ ℝ) univ φ)
    (hsup :
      Eq (α := (a : (↑univ : Type u_2)) → ℝ)
        (⨆ (i : ℕ),
          HAdd.hAdd (α := (a : (↑univ : Type u_2)) → ℝ)
            (Set.restrict (π := fun (a : E) ↦ ℝ) univ
              (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)))
            (const (↑univ : Type u_2) (c i)))
        (Set.restrict (π := fun (a : E) ↦ ℝ) univ φ)),
    ∃ (l : ℕ → E →L[𝕜] 𝕜) (c : ℕ → ℝ),
      (∀ (i : ℕ),
          Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜) + const E (c i) ≤ φ) ∧
        ⨆ (i : ℕ),
            Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜) + const E (c i) =
          φ
⊢ ∃ (l : ℕ → E →L[𝕜] 𝕜) (c : ℕ → ℝ),
    (∀ (i : ℕ),
        Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜) + const E (c i) ≤ φ) ∧
      ⨆ (i : ℕ),
          Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜) + const E (c i) =
        φ

Tactic:
obtain ⟨l, c, hle, hsup⟩ := hφcv.sSup_of_nat_affine_eq (𝕜 := 𝕜) (s := univ) isClosed_univ
    (lowerSemicontinuousOn_univ_iff.2 hφc)

Premises used: isClosed_univ, Iff.mpr, ConvexOn.sSup_of_nat_affine_eq, lowerSemicontinuousOn_univ_iff
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
φ : 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
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
l : ℕ → E →L[𝕜] 𝕜
c : ℕ → ℝ
hle :
  ∀ (i : ℕ),
    HAdd.hAdd (α := (a : (↑univ : Type u_2)) → ℝ)
        (Set.restrict (π := fun (a : E) ↦ ℝ) univ
          (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)))
        (const (↑univ : Type u_2) (c i)) ≤
      Set.restrict (π := fun (a : E) ↦ ℝ) univ φ
hsup :
  Eq (α := (a : (↑univ : Type u_2)) → ℝ)
    (⨆ (i : ℕ),
      HAdd.hAdd (α := (a : (↑univ : Type u_2)) → ℝ)
        (Set.restrict (π := fun (a : E) ↦ ℝ) univ
          (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)))
        (const (↑univ : Type u_2) (c i)))
    (Set.restrict (π := fun (a : E) ↦ ℝ) univ φ)
⊢ ∃ (l : ℕ → E →L[𝕜] 𝕜) (c : ℕ → ℝ),
    (∀ (i : ℕ),
        Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜) + const E (c i) ≤ φ) ∧
      ⨆ (i : ℕ),
          Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜) + const E (c i) =
        φ

Tactic:
⟨l, c, fun i x ↦ hle i ⟨x, trivial⟩, ?_⟩

Premises used: trivial, Subtype.mk, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
φ : 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
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
l : ℕ → E →L[𝕜] 𝕜
c : ℕ → ℝ
hle :
  ∀ (i : ℕ),
    HAdd.hAdd (α := (a : (↑univ : Type u_2)) → ℝ)
        (Set.restrict (π := fun (a : E) ↦ ℝ) univ
          (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)))
        (const (↑univ : Type u_2) (c i)) ≤
      Set.restrict (π := fun (a : E) ↦ ℝ) univ φ
hsup :
  Eq (α := (a : (↑univ : Type u_2)) → ℝ)
    (⨆ (i : ℕ),
      HAdd.hAdd (α := (a : (↑univ : Type u_2)) → ℝ)
        (Set.restrict (π := fun (a : E) ↦ ℝ) univ
          (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)))
        (const (↑univ : Type u_2) (c i)))
    (Set.restrict (π := fun (a : E) ↦ ℝ) univ φ)
refine :
  ⨆ (i : ℕ), Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜) + const E (c i) = φ
⊢ ∃ (l : ℕ → E →L[𝕜] 𝕜) (c : ℕ → ℝ),
    (∀ (i : ℕ),
        Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜) + const E (c i) ≤ φ) ∧
      ⨆ (i : ℕ),
          Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜) + const E (c i) =
        φ

Tactic:
refine ⟨l, c, fun i x ↦ hle i ⟨x, trivial⟩, ?_⟩
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
φ : 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
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
l : ℕ → E →L[𝕜] 𝕜
c : ℕ → ℝ
hle :
  ∀ (i : ℕ),
    HAdd.hAdd (α := (a : (↑univ : Type u_2)) → ℝ)
        (Set.restrict (π := fun (a : E) ↦ ℝ) univ
          (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)))
        (const (↑univ : Type u_2) (c i)) ≤
      Set.restrict (π := fun (a : E) ↦ ℝ) univ φ
hsup :
  Eq (α := (a : (↑univ : Type u_2)) → ℝ)
    (⨆ (i : ℕ),
      HAdd.hAdd (α := (a : (↑univ : Type u_2)) → ℝ)
        (Set.restrict (π := fun (a : E) ↦ ℝ) univ
          (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)))
        (const (↑univ : Type u_2) (c i)))
    (Set.restrict (π := fun (a : E) ↦ ℝ) univ φ)
h :
  ∀ (x : E),
    (⨆ (i : ℕ), Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜) + const E (c i))
        x =
      φ x
⊢ ⨆ (i : ℕ), Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜) + const E (c i) = φ

Tactic:
ext x
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
φ : 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
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
l : ℕ → E →L[𝕜] 𝕜
c : ℕ → ℝ
hle :
  ∀ (i : ℕ),
    HAdd.hAdd (α := (a : (↑univ : Type u_2)) → ℝ)
        (Set.restrict (π := fun (a : E) ↦ ℝ) univ
          (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)))
        (const (↑univ : Type u_2) (c i)) ≤
      Set.restrict (π := fun (a : E) ↦ ℝ) univ φ
hsup :
  Eq (α := (a : (↑univ : Type u_2)) → ℝ)
    (⨆ (i : ℕ),
      HAdd.hAdd (α := (a : (↑univ : Type u_2)) → ℝ)
        (Set.restrict (π := fun (a : E) ↦ ℝ) univ
          (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)))
        (const (↑univ : Type u_2) (c i)))
    (Set.restrict (π := fun (a : E) ↦ ℝ) univ φ)
x : E
⊢ (⨆ (i : ℕ), Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜) + const E (c i))
      x =
    φ x

Tactic:
simpa using congrFun hsup ⟨x, trivial⟩

Premises used: trivial, Subtype.mk, congrFun
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
E : Type u_2
s : Set E
φ : E → ℝ
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
⊢ sSup
      {f : (a : (↑s : Type u_2)) → ℝ |
        f ≤ s.restrict (π := fun (a : E) ↦ ℝ) φ ∧
          ∃ (l : E →L[ℝ] ℝ) (c : ℝ),
            f =
              HAdd.hAdd (α := (a : (↑s : Type u_2)) → ℝ) (β := (↑s : Type u_2) → ℝ)
                (s.restrict (π := fun (a : E) ↦ ℝ) (⇑l : (a : E) → ℝ) : (a : (↑s : Type u_2)) → ℝ)
                (const (↑s : Type u_2) c)} =
    s.restrict (π := fun (a : E) ↦ ℝ) φ

Tactic:
sSup_affine_eq (𝕜 := ℝ) hsc hφc hφcv

Premises used: setOf, ConvexOn.sSup_affine_eq
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
E : Type u_2
s : Set E
φ : E → ℝ
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
inst_6 : 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 =
                HAdd.hAdd (α := (a : (↑s : Type u_2)) → ℝ) (β := (↑s : Type u_2) → ℝ)
                  (s.restrict (π := fun (a : E) ↦ ℝ) (⇑l : (a : E) → ℝ) : (a : (↑s : Type u_2)) → ℝ)
                  (const (↑s : Type u_2) c)

Tactic:
sSup_of_countable_affine_eq (𝕜 := ℝ) hsc hφc hφcv

Premises used: ConvexOn.sSup_of_countable_affine_eq
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
E : Type u_2
s : Set E
φ : E → ℝ
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
inst_6 : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
⊢ ∃ (l : ℕ → E →L[ℝ] ℝ) (c : ℕ → ℝ),
    (∀ (i : ℕ),
        HAdd.hAdd (α := (a : (↑s : Type u_2)) → ℝ) (β := (↑s : Type u_2) → ℝ)
            (s.restrict (π := fun (a : E) ↦ ℝ) (⇑(l i) : (a : E) → ℝ) : (a : (↑s : Type u_2)) → ℝ)
            (const (↑s : Type u_2) (c i)) ≤
          s.restrict (π := fun (a : E) ↦ ℝ) φ) ∧
      ⨆ (i : ℕ),
          HAdd.hAdd (α := (a : (↑s : Type u_2)) → ℝ) (β := (↑s : Type u_2) → ℝ)
            (s.restrict (π := fun (a : E) ↦ ℝ) (⇑(l i) : (a : E) → ℝ) : (a : (↑s : Type u_2)) → ℝ)
            (const (↑s : Type u_2) (c i)) =
        s.restrict (π := fun (a : E) ↦ ℝ) φ

Tactic:
sSup_of_nat_affine_eq (𝕜 := ℝ) hsc hφc hφcv

Premises used: ConvexOn.sSup_of_nat_affine_eq
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
E : Type u_2
φ : E → ℝ
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
⊢ sSup {f : E → ℝ | f ≤ φ ∧ ∃ (l : E →L[ℝ] ℝ) (c : ℝ), f = (⇑l : (a : E) → ℝ) + const E c} = φ

Tactic:
univ_sSup_affine_eq (𝕜 := ℝ) hφc hφcv

Premises used: setOf, ConvexOn.univ_sSup_affine_eq
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
E : Type u_2
φ : E → ℝ
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
inst_6 : HereditarilyLindelofSpace E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
⊢ ∃ (𝓕' : Set (E → ℝ)),
    𝓕'.Countable ∧ sSup 𝓕' = φ ∧ ∀ f ∈ 𝓕', f ≤ φ ∧ ∃ (l : E →L[ℝ] ℝ) (c : ℝ), f = (⇑l : (a : E) → ℝ) + const E c

Tactic:
univ_sSup_of_countable_affine_eq (𝕜 := ℝ) hφc hφcv

Premises used: ConvexOn.univ_sSup_of_countable_affine_eq
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
E : Type u_2
φ : E → ℝ
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
inst_6 : HereditarilyLindelofSpace E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
⊢ ∃ (l : ℕ → E →L[ℝ] ℝ) (c : ℕ → ℝ),
    (∀ (i : ℕ), (⇑(l i) : (a : E) → ℝ) + const E (c i) ≤ φ) ∧ ⨆ (i : ℕ), (⇑(l i) : (a : E) → ℝ) + const E (c i) = φ

Tactic:
univ_sSup_of_nat_affine_eq (𝕜 := ℝ) hφc hφcv

Premises used: ConvexOn.univ_sSup_of_nat_affine_eq
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
s : Set E
x : E
hs : Convex 𝕜 s
hx : x ∈ s
⊢ StarConvex 𝕜 x s

Tactic:
hs hx