awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
φ : 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
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set ({ x : E // Membership.mem (γ := Set E) univ x } → ℝ) :=
  {f : { x : E // Membership.mem (γ := Set E) univ x } → ℝ |
    f ≤ φ ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x) ∧
      ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
        f =
          HAdd.hAdd (α := { x : E // Membership.mem (γ := Set E) univ x } → ℝ)
            (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) ∘
              Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x))
            (const (↑univ : Type u_2) c)}
this :
  Eq (α := (a : (↑univ : Type u_2)) → ℝ)
    (sSup
      {f : (a : (↑univ : Type u_2)) → ℝ |
        f ≤ φ ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x) ∧
          ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
            f =
              HAdd.hAdd (α := (a : (↑univ : Type u_2)) → ℝ)
                (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) ∘
                  Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x))
                (const (↑univ : Type u_2) c)})
    (φ ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x))
x : E
⊢ sSup ((fun (g : (↑univ : Type u_2) → ℝ) ↦ g ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2))) '' 𝓕) x =
    (sSup 𝓕 ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2))) x
have h : Eq (α := ℝ)
  ((⨆ (a : (↑𝓕 : Type u_2)), (↑a : (↑univ : Type u_2) → ℝ) ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)))
    x)
  (Function.comp (β := { x : E // Membership.mem (γ := Set E) univ x })
    (⨆ (a : (↑𝓕 : Type u_2)), (↑a : { x : E // x ∈ univ } → ℝ))
    (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)) x)
Tactic: rw [sSup_image', sSup_eq_iSup']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
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
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set ({ x : E // Membership.mem (γ := Set E) univ x } → ℝ) :=
  {f : { x : E // Membership.mem (γ := Set E) univ x } → ℝ |
    f ≤ φ ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x) ∧
      ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
        f =
          HAdd.hAdd (α := { x : E // Membership.mem (γ := Set E) univ x } → ℝ)
            (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) ∘
              Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x))
            (const (↑univ : Type u_2) c)}
this :
  Eq (α := (a : (↑univ : Type u_2)) → ℝ)
    (sSup
      {f : (a : (↑univ : Type u_2)) → ℝ |
        f ≤ φ ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x) ∧
          ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
            f =
              HAdd.hAdd (α := (a : (↑univ : Type u_2)) → ℝ)
                (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) ∘
                  Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x))
                (const (↑univ : Type u_2) c)})
    (φ ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x))
⊢ φ ∘
      Function.comp (β := { x : E // Membership.mem (γ := Set E) univ x })
        (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x))
        (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)) =
    φ
have h : ∀ (x : E),
  (φ ∘
        Function.comp (β := { x : E // Membership.mem (γ := Set E) univ x })
          (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x))
          (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)))
      x =
    φ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
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
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set ({ x : E // Membership.mem (γ := Set E) univ x } → ℝ) :=
  {f : { x : E // Membership.mem (γ := Set E) univ x } → ℝ |
    f ≤ φ ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x) ∧
      ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
        f =
          HAdd.hAdd (α := { x : E // Membership.mem (γ := Set E) univ x } → ℝ)
            (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) ∘
              Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x))
            (const (↑univ : Type u_2) c)}
this :
  Eq (α := (a : (↑univ : Type u_2)) → ℝ)
    (sSup
      {f : (a : (↑univ : Type u_2)) → ℝ |
        f ≤ φ ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x) ∧
          ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
            f =
              HAdd.hAdd (α := (a : (↑univ : Type u_2)) → ℝ)
                (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) ∘
                  Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x))
                (const (↑univ : Type u_2) c)})
    (φ ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x))
⊢ sSup
      {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} =
    φ
have _ : Eq (α := E → ℝ)
  (sSup
    {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})
  (sSup ((fun (g : (↑univ : Type u_2) → ℝ) ↦ g ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2))) '' 𝓕))
Tactic: calc
  _ = sSup ((fun g => g ∘ (Equiv.Set.univ E).symm) '' 𝓕) := by
    congr
    ext f
    refine ⟨fun ⟨hp, l, c, hlc⟩ => ⟨f ∘ Subtype.val, ⟨fun x => hp (Subtype.val x), ⟨l, c, ?_⟩⟩, ?_⟩,
      fun ⟨a, ⟨⟨h, ⟨l, c, hlc⟩⟩, hb⟩⟩ => ⟨fun x => ?_, ⟨l, c, ?_⟩⟩⟩
    · ext x; simpa using congrFun hlc x
    · ext; simp
    · simpa using hb ▸ h ⟨x, trivial⟩
    · subst hlc; simpa using hb.symm
  _ = sSup 𝓕 ∘ (Equiv.Set.univ E).symm := by ext x; rw [sSup_image', sSup_eq_iSup']; simp
  _ = φ ∘ Subtype.val ∘ (Equiv.Set.univ E).symm :=
    congrArg (fun g => g ∘ (Equiv.Set.univ E).symm) this
  _ = φ := by ext; simp
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
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
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set ({ x : E // Membership.mem (γ := Set E) univ x } → ℝ) :=
  {f : { x : E // Membership.mem (γ := Set E) univ x } → ℝ |
    f ≤ φ ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x) ∧
      ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
        f =
          HAdd.hAdd (α := { x : E // Membership.mem (γ := Set E) univ x } → ℝ)
            (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) ∘
              Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x))
            (const (↑univ : Type u_2) c)}
this :
  Eq (α := (a : (↑univ : Type u_2)) → ℝ)
    (sSup
      {f : (a : (↑univ : Type u_2)) → ℝ |
        f ≤ φ ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x) ∧
          ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
            f =
              HAdd.hAdd (α := (a : (↑univ : Type u_2)) → ℝ)
                (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) ∘
                  Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x))
                (const (↑univ : Type u_2) c)})
    (φ ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x))
_ :
  Eq (α := E → ℝ)
    (sSup
      {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})
    (sSup ((fun (g : (↑univ : Type u_2) → ℝ) ↦ g ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2))) '' 𝓕))
⊢ sSup
      {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} =
    φ
have _₁ : Eq (α := E → ℝ)
  (sSup ((fun (g : (↑univ : Type u_2) → ℝ) ↦ g ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2))) '' 𝓕))
  (sSup 𝓕 ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)))
Tactic: calc
  _ = sSup ((fun g => g ∘ (Equiv.Set.univ E).symm) '' 𝓕) := by
    congr
    ext f
    refine ⟨fun ⟨hp, l, c, hlc⟩ => ⟨f ∘ Subtype.val, ⟨fun x => hp (Subtype.val x), ⟨l, c, ?_⟩⟩, ?_⟩,
      fun ⟨a, ⟨⟨h, ⟨l, c, hlc⟩⟩, hb⟩⟩ => ⟨fun x => ?_, ⟨l, c, ?_⟩⟩⟩
    · ext x; simpa using congrFun hlc x
    · ext; simp
    · simpa using hb ▸ h ⟨x, trivial⟩
    · subst hlc; simpa using hb.symm
  _ = sSup 𝓕 ∘ (Equiv.Set.univ E).symm := by ext x; rw [sSup_image', sSup_eq_iSup']; simp
  _ = φ ∘ Subtype.val ∘ (Equiv.Set.univ E).symm :=
    congrArg (fun g => g ∘ (Equiv.Set.univ E).symm) this
  _ = φ := by ext; simp
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
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
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set ({ x : E // Membership.mem (γ := Set E) univ x } → ℝ) :=
  {f : { x : E // Membership.mem (γ := Set E) univ x } → ℝ |
    f ≤ φ ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x) ∧
      ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
        f =
          HAdd.hAdd (α := { x : E // Membership.mem (γ := Set E) univ x } → ℝ)
            (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) ∘
              Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x))
            (const (↑univ : Type u_2) c)}
this :
  Eq (α := (a : (↑univ : Type u_2)) → ℝ)
    (sSup
      {f : (a : (↑univ : Type u_2)) → ℝ |
        f ≤ φ ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x) ∧
          ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
            f =
              HAdd.hAdd (α := (a : (↑univ : Type u_2)) → ℝ)
                (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) ∘
                  Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x))
                (const (↑univ : Type u_2) c)})
    (φ ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x))
_ :
  Eq (α := E → ℝ)
    (sSup
      {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})
    (sSup ((fun (g : (↑univ : Type u_2) → ℝ) ↦ g ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2))) '' 𝓕))
_₁ :
  Eq (α := E → ℝ)
    (sSup ((fun (g : (↑univ : Type u_2) → ℝ) ↦ g ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2))) '' 𝓕))
    (sSup 𝓕 ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)))
⊢ sSup
      {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} =
    φ
have _₂ : φ ∘
    Function.comp (β := { x : E // Membership.mem (γ := Set E) univ x })
      (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x))
      (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)) =
  φ
Tactic: calc
  _ = sSup ((fun g => g ∘ (Equiv.Set.univ E).symm) '' 𝓕) := by
    congr
    ext f
    refine ⟨fun ⟨hp, l, c, hlc⟩ => ⟨f ∘ Subtype.val, ⟨fun x => hp (Subtype.val x), ⟨l, c, ?_⟩⟩, ?_⟩,
      fun ⟨a, ⟨⟨h, ⟨l, c, hlc⟩⟩, hb⟩⟩ => ⟨fun x => ?_, ⟨l, c, ?_⟩⟩⟩
    · ext x; simpa using congrFun hlc x
    · ext; simp
    · simpa using hb ▸ h ⟨x, trivial⟩
    · subst hlc; simpa using hb.symm
  _ = sSup 𝓕 ∘ (Equiv.Set.univ E).symm := by ext x; rw [sSup_image', sSup_eq_iSup']; simp
  _ = φ ∘ Subtype.val ∘ (Equiv.Set.univ E).symm :=
    congrArg (fun g => g ∘ (Equiv.Set.univ E).symm) this
  _ = φ := by ext; simp
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
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 𝓕 φ
have refine_1 : 𝓕.Nonempty
Tactic: refine (hφcv.univ_sSup_affine_eq (𝕜 := 𝕜) hφc) ▸ isLUB_csSup ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
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}
refine_1 : 𝓕.Nonempty
⊢ IsLUB 𝓕 φ
have refine_2 : BddAbove 𝓕
Tactic: refine (hφcv.univ_sSup_affine_eq (𝕜 := 𝕜) hφc) ▸ isLUB_csSup ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
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}
⊢ 𝓕.Nonempty
have refine_1 : ∀ (l : E →L[𝕜] 𝕜) (c : ℝ)
  (hlc :
    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 : (a : E) → 𝕜)))
          (const (↑univ : Type u_2) c) ≤
        Set.restrict (π := fun (a : E) ↦ ℝ) univ φ ∧
      HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) 0 : 𝕜) : ℝ) c = φ 0 - 1),
  𝓕.Nonempty
Tactic: 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
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (hypothesis)
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}
⊢ ∃ (𝓕' : 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
have hl : 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⟩)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
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
have 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
Tactic: obtain ⟨l, c, hlc⟩ := hf.2
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
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 f
have rw : Continuous (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c)
Tactic: rw [hlc]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (hypothesis)
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 𝓕 φ
⊢ ∃ (𝓕' : 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
have hr : ∀ (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)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
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 → ℝ)),
    𝓕'.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
have 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
Tactic: obtain ⟨𝓕', h𝓕'⟩ := exists_countable_lowerSemicontinuous_isLUB hr hl
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
φ : 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
have refine : 𝓕'.Nonempty
Tactic: refine ⟨𝓕', h𝓕'.2.1, h𝓕'.2.2.csSup_eq ?_, fun f hf => h𝓕'.1 hf⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
φ : 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 𝓕' φ
⊢ 𝓕'.Nonempty
have by_contra! : ∀ (this : 𝓕' = ∅), False
Tactic: by_contra!