awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
inst_9 : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
𝓕' : Set ((↑s : Type u_2) → ℝ)
h𝓕' :
  𝓕'.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
he : 𝓕' = ∅
hsφ : s.restrict (π := fun (a : E) ↦ ℝ) φ ≠ 0
x : (↑s : Type u_2)
hx : s.restrict (π := fun (a : E) ↦ ℝ) φ x ≠ 0 x
⊢ ∃ (l : ℕ → E →L[𝕜] 𝕜) (c : ℕ → ℝ),
    (∀ (i : ℕ),
        s.restrict (π := fun (a : E) ↦ ℝ)
              (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)) +
            const (↑s : Type u_2) (c i) ≤
          s.restrict (π := fun (a : E) ↦ ℝ) φ) ∧
      ⨆ (i : ℕ),
          s.restrict (π := fun (a : E) ↦ ℝ)
              (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)) +
            const (↑s : Type u_2) (c i) =
        s.restrict (π := fun (a : E) ↦ ℝ) φ
have this : s = ∅
Tactic: have : s = ∅ := by have := congrFun h𝓕'.2.1 x; simp_all
-- 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
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)}
⊢ 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 this : Eq (α := (a : (↑univ : Type u_2)) → ℝ)
  (sSup
    {f : (a : (↑univ : Type u_2)) → ℝ |
      f ≤ Set.restrict (π := fun (a : E) ↦ ℝ) univ φ ∧
        ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
          f =
            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 φ)
Tactic: have := hφcv.sSup_affine_eq (𝕜 := 𝕜) isClosed_univ (lowerSemicontinuousOn_univ_iff.2 hφc)
-- 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))) '' 𝓕))
have e_a : Eq.{u_2 + 1} (α := (E → ℝ) → Prop)
  (fun (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)
  fun (x : E → ℝ) ↦
  ∃ a ∈ 𝓕,
    (fun (g : (↑univ : Type u_2) → ℝ) ↦ (g ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)) : E → ℝ)) a = x
Tactic: congr
-- 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.{u_2 + 1} (α := (E → ℝ) → Prop)
    (fun (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)
    fun (x : E → ℝ) ↦
    ∃ a ∈ 𝓕,
      (fun (g : (↑univ : Type u_2) → ℝ) ↦ (g ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)) : E → ℝ)) a = x
have e_a : ∀ (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) ↔
    ∃ a ∈ 𝓕,
      (fun (g : (↑univ : Type u_2) → ℝ) ↦ (g ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)) : E → ℝ)) a = f
Tactic: ext f
-- 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))
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) ↔
    ∃ a ∈ 𝓕,
      (fun (g : (↑univ : Type u_2) → ℝ) ↦ (g ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)) : E → ℝ)) a = f
have e_a : (f ≤ φ ∧
    ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
      f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c) →
  ∀ (hp : f ≤ φ) (l : E →L[𝕜] 𝕜) (c : ℝ)
    (hlc : f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c),
    f ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x) =
      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)
Tactic: 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, ?_⟩⟩⟩
-- 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))
f : E → ℝ
h :
  f ≤ φ ∧
    ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
      f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c
hp : f ≤ φ
l : E →L[𝕜] 𝕜
c : ℝ
hlc : f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c
⊢ f ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x) =
    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)
have e_a : ∀ (x : (↑univ : Type u_2)),
  (f ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x)) x =
    HAdd.hAdd (α := { x : E // Membership.mem (γ := Set E) univ x } → ℝ) (β := (↑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) x
Tactic: ext x
-- 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))
f : E → ℝ
h :
  f ≤ φ ∧
    ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
      f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c
hp : f ≤ φ
l : E →L[𝕜] 𝕜
c : ℝ
hlc : f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c
⊢ (fun (g : (↑univ : Type u_2) → ℝ) ↦ (g ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)) : E → ℝ))
      (f ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x)) =
    f
have e_a : ∀ (x : E),
  (fun (g : (↑univ : Type u_2) → ℝ) ↦ (g ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)) : E → ℝ))
      (f ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x)) x =
    f x
Tactic: ext
-- 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
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))
f : E → ℝ
h_1 :
  ∃ a ∈ 𝓕,
    (fun (g : (↑univ : Type u_2) → ℝ) ↦ (g ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)) : E → ℝ)) a = f
a : (↑univ : Type u_2) → ℝ
h : a ≤ φ ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x)
l : E →L[𝕜] 𝕜
c : ℝ
hlc :
  a =
    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)
hb : (fun (g : (↑univ : Type u_2) → ℝ) ↦ (g ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)) : E → ℝ)) a = f
⊢ f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c
have h₁ : 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) ≤
  φ ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x)
Tactic: subst hlc
Cleared hypotheses: a, h, hlc, hb
-- 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
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))
f : E → ℝ
h_1 :
  ∃ a ∈ 𝓕,
    (fun (g : (↑univ : Type u_2) → ℝ) ↦ (g ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)) : E → ℝ)) a = f
a : (↑univ : Type u_2) → ℝ
h : a ≤ φ ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x)
l : E →L[𝕜] 𝕜
c : ℝ
hlc :
  a =
    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)
hb : (fun (g : (↑univ : Type u_2) → ℝ) ↦ (g ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)) : E → ℝ)) a = f
h₁ :
  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) ≤
    φ ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) univ x)
⊢ f = Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜) + const E c
have hb₁ : (fun (g : (↑univ : Type u_2) → ℝ) ↦ (g ∘ (⇑(Equiv.Set.univ E).symm : (a : E) → (↑univ : Type u_2)) : E → ℝ))
    (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)) =
  f
Tactic: subst hlc
Cleared hypotheses: a, h, hlc, hb
-- 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 ((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)))
have h : ∀ (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
Tactic: ext x