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 : AddCommMonoid E
inst_2 : Module ℝ E
hφcv : ConvexOn ℝ s φ
⊢ Convex ℝ (E := E × 𝕜) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
have lem : Eq (α := Set (E × 𝕜)) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
  (preimage (β := E × ℝ) (⇑(LinearMap.prodMap LinearMap.id reLm) : (a : E × 𝕜) → E × ℝ)
    {p : E × ℝ | p.1 ∈ s ∧ φ p.1 ≤ p.2})
Tactic: have lem : { p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ re p.2 } =
    ((LinearMap.id : E →ₗ[ℝ] E).prodMap reLm) ⁻¹' { p : E × ℝ | p.1 ∈ s ∧ φ p.1 ≤ p.2 } := by simp
-- 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
hsc : IsClosed s
hφ_cont : LowerSemicontinuousOn φ s
A : Set (E × EReal) := {p : E × EReal | p.1 ∈ s ∧ (↑(φ p.1) : EReal) ≤ p.2}
⊢ IsClosed (X := E × 𝕜) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
have hC : Eq (α := Set (E × 𝕜)) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
  (Prod.map id (Real.toEReal ∘ (⇑re : (a : 𝕜) → ℝ)) ⁻¹' A)
Tactic: have hC : { p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ re p.2 }
    = (Prod.map id ((Real.toEReal ∘ re) : 𝕜 → EReal)) ⁻¹' A := by simp [A]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
hsc : IsClosed s
hφ_cont : LowerSemicontinuousOn φ s
A : Set (E × EReal) := {p : E × EReal | p.1 ∈ s ∧ (↑(φ p.1) : EReal) ≤ p.2}
hC :
  Eq (α := Set (E × 𝕜)) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
    (Prod.map id (Real.toEReal ∘ (⇑re : (a : 𝕜) → ℝ)) ⁻¹' A)
⊢ IsClosed (X := E × 𝕜) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
have refine_1 : Continuous (X := E × 𝕜) (Prod.map id (Real.toEReal ∘ (⇑re : (a : 𝕜) → ℝ)))
Tactic: refine hC.symm ▸ IsClosed.preimage ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
hsc : IsClosed s
hφ_cont : LowerSemicontinuousOn φ s
A : Set (E × EReal) := {p : E × EReal | p.1 ∈ s ∧ (↑(φ p.1) : EReal) ≤ p.2}
hC :
  Eq (α := Set (E × 𝕜)) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
    (Prod.map id (Real.toEReal ∘ (⇑re : (a : 𝕜) → ℝ)) ⁻¹' A)
refine_1 : Continuous (X := E × 𝕜) (Prod.map id (Real.toEReal ∘ (⇑re : (a : 𝕜) → ℝ)))
⊢ IsClosed (X := E × 𝕜) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
have refine_2 : IsClosed A
Tactic: refine hC.symm ▸ IsClosed.preimage ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
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
x : E
a : ℝ
hx : x ∈ s
hax : a < φ x
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
⊢ ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
    s.restrict (π := fun (a : E) ↦ ℝ)
            (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜)) +
          const (↑s : Type u_2) c ≤
        s.restrict (π := fun (a : E) ↦ ℝ) φ ∧
      HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) x : 𝕜) : ℝ) c = a
have obtain : ∀ (L : StrongDual 𝕜 (E × 𝕜)) (b : ℝ)
  (hLb :
    (re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (x, (↑a : 𝕜)) : 𝕜) < b ∧
      ∀ (b_1 : E × 𝕜),
        Membership.mem (γ := Set (E × 𝕜)) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2} b_1 →
          b < (re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) b_1 : 𝕜)),
  ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
    s.restrict (π := fun (a : E) ↦ ℝ)
            (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜)) +
          const (↑s : Type u_2) c ≤
        s.restrict (π := fun (a : E) ↦ ℝ) φ ∧
      HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) x : 𝕜) : ℝ) c = a
Tactic: obtain ⟨L, ⟨b, hLb⟩⟩ := geometric_hahn_banach_point_closed (𝕜 := 𝕜) hφcv.convex_re_epigraph
    (hφc.isClosed_re_epigraph hsc) (by simp [A, hax] : (x, ofReal a) ∉ A)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
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
x : E
a : ℝ
hx : x ∈ s
hax : a < φ x
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
L : StrongDual 𝕜 (E × 𝕜)
b : ℝ
hLb :
  (re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (x, (↑a : 𝕜)) : 𝕜) < b ∧
    ∀ (b_1 : E × 𝕜),
      Membership.mem (γ := Set (E × 𝕜)) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2} b_1 →
        b < (re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) b_1 : 𝕜)
u : E →L[𝕜] 𝕜 := L ∘SL inl 𝕜 E 𝕜
c : ℝ := ((re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (0, 1) : 𝕜))⁻¹
⊢ ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
    s.restrict (π := fun (a : E) ↦ ℝ)
            (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜)) +
          const (↑s : Type u_2) c ≤
        s.restrict (π := fun (a : E) ↦ ℝ) φ ∧
      HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) x : 𝕜) : ℝ) c = a
have refine_1 : ∀ (z : (↑s : Type u_2)),
  HAdd.hAdd (α := (a : (↑s : Type u_2)) → ℝ) (β := (↑s : Type u_2) → ℝ)
      (s.restrict (π := fun (a : E) ↦ ℝ)
        (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(-c • u) : (a : E) → 𝕜)))
      (const (↑s : Type u_2) (HMul.hMul (β := ℝ) c ((re : (a : 𝕜) → ℝ) ((u : (a : E) → 𝕜) x : 𝕜) : ℝ) + a)) z ≤
    s.restrict (π := fun (a : E) ↦ ℝ) φ z
Tactic: refine ⟨- c • u, c * re (u x) + a, fun z => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
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
x : E
a : ℝ
hx : x ∈ s
hax : a < φ x
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
L : StrongDual 𝕜 (E × 𝕜)
b : ℝ
hLb :
  (re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (x, (↑a : 𝕜)) : 𝕜) < b ∧
    ∀ (b_1 : E × 𝕜),
      Membership.mem (γ := Set (E × 𝕜)) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2} b_1 →
        b < (re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) b_1 : 𝕜)
u : E →L[𝕜] 𝕜 := L ∘SL inl 𝕜 E 𝕜
c : ℝ := ((re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (0, 1) : 𝕜))⁻¹
refine_1 :
  ∀ (z : (↑s : Type u_2)),
    HAdd.hAdd (α := (a : (↑s : Type u_2)) → ℝ) (β := (↑s : Type u_2) → ℝ)
        (s.restrict (π := fun (a : E) ↦ ℝ)
          (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(-c • u) : (a : E) → 𝕜)))
        (const (↑s : Type u_2) (HMul.hMul (β := ℝ) c ((re : (a : 𝕜) → ℝ) ((u : (a : E) → 𝕜) x : 𝕜) : ℝ) + a)) z ≤
      s.restrict (π := fun (a : E) ↦ ℝ) φ z
⊢ ∃ (l : E →L[𝕜] 𝕜) (c : ℝ),
    s.restrict (π := fun (a : E) ↦ ℝ)
            (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑l : (a : E) → 𝕜)) +
          const (↑s : Type u_2) c ≤
        s.restrict (π := fun (a : E) ↦ ℝ) φ ∧
      HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) x : 𝕜) : ℝ) c = a
have refine_2 : HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ((-c • u : (a : E) → 𝕜) x : 𝕜) : ℝ)
    (HMul.hMul (β := ℝ) c ((re : (a : 𝕜) → ℝ) ((u : (a : E) → 𝕜) x : 𝕜) : ℝ) + a) =
  a
Tactic: refine ⟨- c • u, c * re (u x) + a, fun z => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
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
x : E
a : ℝ
hx : x ∈ s
hax : a < φ x
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
L : StrongDual 𝕜 (E × 𝕜)
b : ℝ
hLb :
  (re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (x, (↑a : 𝕜)) : 𝕜) < b ∧
    ∀ (b_1 : E × 𝕜),
      Membership.mem (γ := Set (E × 𝕜)) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2} b_1 →
        b < (re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) b_1 : 𝕜)
u : E →L[𝕜] 𝕜 := L ∘SL inl 𝕜 E 𝕜
c : ℝ := ((re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (0, 1) : 𝕜))⁻¹
z : (↑s : Type u_2)
v : 𝕜
⊢ HMul.hMul (β := 𝕜) v ((L : (a : E × 𝕜) → 𝕜) (0, 1) : 𝕜) = (L : (a : E × 𝕜) → 𝕜) (0, v)
have rw : Eq.{u_1 + 1} (α := 𝕜) ((L : (a : E × 𝕜) → 𝕜) (HSMul.hSMul (β := E × 𝕜) v (0, 1)) : 𝕜) ((L : (a : E × 𝕜) → 𝕜) (0, v) : 𝕜)
Tactic: rw [← smul_eq_mul, ← map_smul]
-- 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
x : E
a : ℝ
hx : x ∈ s
hax : a < φ x
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
L : StrongDual 𝕜 (E × 𝕜)
b : ℝ
hLb :
  (re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (x, (↑a : 𝕜)) : 𝕜) < b ∧
    ∀ (b_1 : E × 𝕜),
      Membership.mem (γ := Set (E × 𝕜)) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2} b_1 →
        b < (re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) b_1 : 𝕜)
u : E →L[𝕜] 𝕜 := L ∘SL inl 𝕜 E 𝕜
c : ℝ := ((re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (0, 1) : 𝕜))⁻¹
z : (↑s : Type u_2)
⊢ HAdd.hAdd (α := (a : (↑s : Type u_2)) → ℝ) (β := (↑s : Type u_2) → ℝ)
      (s.restrict (π := fun (a : E) ↦ ℝ)
        (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(-c • u) : (a : E) → 𝕜)))
      (const (↑s : Type u_2) (HMul.hMul (β := ℝ) c ((re : (a : 𝕜) → ℝ) ((u : (a : E) → 𝕜) x : 𝕜) : ℝ) + a)) z ≤
    s.restrict (π := fun (a : E) ↦ ℝ) φ z
have hv : ∀ (v : 𝕜), HMul.hMul (β := 𝕜) v ((L : (a : E × 𝕜) → 𝕜) (0, 1) : 𝕜) = (L : (a : E × 𝕜) → 𝕜) (0, v)
Tactic: have hv (v : 𝕜) : v * L (0, 1) = L (0, v) := by rw [← smul_eq_mul, ← map_smul]; simp
-- 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
x : E
a : ℝ
hx : x ∈ s
hax : a < φ x
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
L : StrongDual 𝕜 (E × 𝕜)
b : ℝ
hLb :
  (re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (x, (↑a : 𝕜)) : 𝕜) < b ∧
    ∀ (b_1 : E × 𝕜),
      Membership.mem (γ := Set (E × 𝕜)) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2} b_1 →
        b < (re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) b_1 : 𝕜)
u : E →L[𝕜] 𝕜 := L ∘SL inl 𝕜 E 𝕜
c : ℝ := ((re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (0, 1) : 𝕜))⁻¹
z : (↑s : Type u_2)
hv : ∀ (v : 𝕜), HMul.hMul (β := 𝕜) v ((L : (a : E × 𝕜) → 𝕜) (0, 1) : 𝕜) = (L : (a : E × 𝕜) → 𝕜) (0, v)
w : E
h : w ∈ s
⊢ HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (x, 0) : 𝕜) : ℝ)
      (HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (0, 1) : 𝕜) : ℝ) a) <
    HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (w, 0) : 𝕜) : ℝ)
      (HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (0, 1) : 𝕜) : ℝ) (φ w))
have hw : LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (x, (↑a : 𝕜)) : 𝕜) : ℝ)
  ((re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (w, (↑(φ w) : 𝕜)) : 𝕜) : ℝ)
Tactic: have hw := hLb.1.trans (hLb.2 _ (by simp [A, h] : (w, ofReal (φ w)) ∈ A))
-- 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
x : E
a : ℝ
hx : x ∈ s
hax : a < φ x
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
L : StrongDual 𝕜 (E × 𝕜)
b : ℝ
hLb :
  (re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (x, (↑a : 𝕜)) : 𝕜) < b ∧
    ∀ (b_1 : E × 𝕜),
      Membership.mem (γ := Set (E × 𝕜)) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2} b_1 →
        b < (re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) b_1 : 𝕜)
u : E →L[𝕜] 𝕜 := L ∘SL inl 𝕜 E 𝕜
c : ℝ := ((re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (0, 1) : 𝕜))⁻¹
z : (↑s : Type u_2)
hv : ∀ (v : 𝕜), HMul.hMul (β := 𝕜) v ((L : (a : E × 𝕜) → 𝕜) (0, 1) : 𝕜) = (L : (a : E × 𝕜) → 𝕜) (0, v)
w : E
h : w ∈ s
hw :
  LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (x, (↑a : 𝕜)) : 𝕜) : ℝ)
    ((re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (w, (↑(φ w) : 𝕜)) : 𝕜) : ℝ)
⊢ HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (x, 0) : 𝕜) : ℝ)
      (HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (0, 1) : 𝕜) : ℝ) a) <
    HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (w, 0) : 𝕜) : ℝ)
      (HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (0, 1) : 𝕜) : ℝ) (φ w))
have hw₁ : LT.lt (α := ℝ)
  ((re : (a : 𝕜) → ℝ)
      (((coprod (L ∘SL inl 𝕜 E 𝕜) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) L (inr 𝕜 E 𝕜)) : E × 𝕜 →L[𝕜] 𝕜) :
            (a : E × 𝕜) → 𝕜)
          (x, (↑a : 𝕜)) :
        𝕜) :
    ℝ)
  ((re : (a : 𝕜) → ℝ)
      (((coprod (L ∘SL inl 𝕜 E 𝕜) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) L (inr 𝕜 E 𝕜)) : E × 𝕜 →L[𝕜] 𝕜) :
            (a : E × 𝕜) → 𝕜)
          (w, (↑(φ w) : 𝕜)) :
        𝕜) :
    ℝ)
Tactic: rw [← coprod_comp_inl_inr L] at hw
Cleared hypotheses: hw
-- 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
x : E
a : ℝ
hx : x ∈ s
hax : a < φ x
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
L : StrongDual 𝕜 (E × 𝕜)
b : ℝ
hLb :
  (re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (x, (↑a : 𝕜)) : 𝕜) < b ∧
    ∀ (b_1 : E × 𝕜),
      Membership.mem (γ := Set (E × 𝕜)) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2} b_1 →
        b < (re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) b_1 : 𝕜)
u : E →L[𝕜] 𝕜 := L ∘SL inl 𝕜 E 𝕜
c : ℝ := ((re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (0, 1) : 𝕜))⁻¹
z : (↑s : Type u_2)
hv : ∀ (v : 𝕜), HMul.hMul (β := 𝕜) v ((L : (a : E × 𝕜) → 𝕜) (0, 1) : 𝕜) = (L : (a : E × 𝕜) → 𝕜) (0, v)
⊢ HAdd.hAdd (α := (a : (↑s : Type u_2)) → ℝ) (β := (↑s : Type u_2) → ℝ)
      (s.restrict (π := fun (a : E) ↦ ℝ)
        (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(-c • u) : (a : E) → 𝕜)))
      (const (↑s : Type u_2) (HMul.hMul (β := ℝ) c ((re : (a : 𝕜) → ℝ) ((u : (a : E) → 𝕜) x : 𝕜) : ℝ) + a)) z ≤
    s.restrict (π := fun (a : E) ↦ ℝ) φ z
have hine : ∀ {w : E} (h : w ∈ s),
  HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (x, 0) : 𝕜) : ℝ)
      (HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (0, 1) : 𝕜) : ℝ) a) <
    HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (w, 0) : 𝕜) : ℝ)
      (HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (0, 1) : 𝕜) : ℝ) (φ w))
Tactic: have hine {w : E} (h : w ∈ s) : re (L (x, 0)) + re (L (0, 1)) * a
      < re (L (w, 0)) + re (L (0, 1)) * φ w := by
      have hw := hLb.1.trans (hLb.2 _ (by simp [A, h] : (w, ofReal (φ w)) ∈ A))
      rw [← coprod_comp_inl_inr L] at hw
      simpa [-coprod_comp_inl_inr, ← hv (ofReal a), ← hv (ofReal (φ w)), mul_comm a,
        mul_comm (φ w)] using hw
-- 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
x : E
a : ℝ
hx : x ∈ s
hax : a < φ x
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2}
L : StrongDual 𝕜 (E × 𝕜)
b : ℝ
hLb :
  (re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (x, (↑a : 𝕜)) : 𝕜) < b ∧
    ∀ (b_1 : E × 𝕜),
      Membership.mem (γ := Set (E × 𝕜)) {p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ (re : (a : 𝕜) → ℝ) p.2} b_1 →
        b < (re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) b_1 : 𝕜)
u : E →L[𝕜] 𝕜 := L ∘SL inl 𝕜 E 𝕜
c : ℝ := ((re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (0, 1) : 𝕜))⁻¹
z : (↑s : Type u_2)
hv : ∀ (v : 𝕜), HMul.hMul (β := 𝕜) v ((L : (a : E × 𝕜) → 𝕜) (0, 1) : 𝕜) = (L : (a : E × 𝕜) → 𝕜) (0, v)
hine :
  ∀ {w : E} (h : w ∈ s),
    HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (x, 0) : 𝕜) : ℝ)
        (HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (0, 1) : 𝕜) : ℝ) a) <
      HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (w, 0) : 𝕜) : ℝ)
        (HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ((L : (a : E × 𝕜) → 𝕜) (0, 1) : 𝕜) : ℝ) (φ w))
⊢ HAdd.hAdd (α := (a : (↑s : Type u_2)) → ℝ) (β := (↑s : Type u_2) → ℝ)
      (s.restrict (π := fun (a : E) ↦ ℝ)
        (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(-c • u) : (a : E) → 𝕜)))
      (const (↑s : Type u_2) (HMul.hMul (β := ℝ) c ((re : (a : 𝕜) → ℝ) ((u : (a : E) → 𝕜) x : 𝕜) : ℝ) + a)) z ≤
    s.restrict (π := fun (a : E) ↦ ℝ) φ z
have hc : 0 < c
Tactic: have hc : 0 < c := inv_pos.2 (pos_of_right_mul_lt_le (lt_of_add_lt_add_left (hine hx)) hax.le)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
Goal:
s : Set ℝ
f : ℝ → ℝ
x a : ℝ
hx : x ∈ s
hax : a < f x
hsc : IsClosed s
hfc : LowerSemicontinuousOn f s
hf : ConvexOn ℝ s f
⊢ ∃ (c : ℝ) (c' : ℝ), (∀ y ∈ s, c * y + c' ≤ f y) ∧ c * x + c' = a
have obtain : ∀ (l : ℝ →L[ℝ] ℝ) (c' : ℝ)
  (hlc'_le :
    s.restrict (π := fun (a : ℝ) ↦ ℝ) (Function.comp (β := ℝ) (⇑re : (a : ℝ) → ℝ) (⇑l : (a : ℝ) → ℝ)) +
        const (↑s : Type) c' ≤
      s.restrict (π := fun (a : ℝ) ↦ ℝ) f)
  (hlc'_eq : HAdd.hAdd (α := ℝ) ((re : (a : ℝ) → ℝ) ((l : (a : ℝ) → ℝ) x : ℝ) : ℝ) c' = a),
  ∃ (c : ℝ) (c' : ℝ), (∀ y ∈ s, c * y + c' ≤ f y) ∧ c * x + c' = a
Tactic: obtain ⟨l, c', hlc'_le, hlc'_eq⟩ := exists_affine_le_of_lt (𝕜 := ℝ) hx hax hsc hfc hf
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
Goal:
s : Set ℝ
f : ℝ → ℝ
x a : ℝ
hx : x ∈ s
hax : a < f x
hsc : IsClosed s
hfc : LowerSemicontinuousOn f s
hf : ConvexOn ℝ s f
l : ℝ →L[ℝ] ℝ
c' : ℝ
hlc'_le :
  s.restrict (π := fun (a : ℝ) ↦ ℝ) (Function.comp (β := ℝ) (⇑re : (a : ℝ) → ℝ) (⇑l : (a : ℝ) → ℝ)) +
      const (↑s : Type) c' ≤
    s.restrict (π := fun (a : ℝ) ↦ ℝ) f
hlc'_eq : HAdd.hAdd (α := ℝ) ((re : (a : ℝ) → ℝ) ((l : (a : ℝ) → ℝ) x : ℝ) : ℝ) c' = a
y : ℝ
⊢ HMul.hMul (α := ℝ) ((l : (a : ℝ) → ℝ) 1 : ℝ) y = (l : (a : ℝ) → ℝ) y
have rw : HMul.hMul (β := ℝ) y ((l : (a : ℝ) → ℝ) 1 : ℝ) = (l : (a : ℝ) → ℝ) y
Tactic: rw [mul_comm, ← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
Goal:
s : Set ℝ
f : ℝ → ℝ
x a : ℝ
hx : x ∈ s
hax : a < f x
hsc : IsClosed s
hfc : LowerSemicontinuousOn f s
hf : ConvexOn ℝ s f
l : ℝ →L[ℝ] ℝ
c' : ℝ
hlc'_le :
  s.restrict (π := fun (a : ℝ) ↦ ℝ) (Function.comp (β := ℝ) (⇑re : (a : ℝ) → ℝ) (⇑l : (a : ℝ) → ℝ)) +
      const (↑s : Type) c' ≤
    s.restrict (π := fun (a : ℝ) ↦ ℝ) f
hlc'_eq : HAdd.hAdd (α := ℝ) ((re : (a : ℝ) → ℝ) ((l : (a : ℝ) → ℝ) x : ℝ) : ℝ) c' = a
y : ℝ
rw : HMul.hMul (β := ℝ) y ((l : (a : ℝ) → ℝ) 1 : ℝ) = (l : (a : ℝ) → ℝ) y
⊢ HMul.hMul (α := ℝ) ((l : (a : ℝ) → ℝ) 1 : ℝ) y = (l : (a : ℝ) → ℝ) y
have rw₁ : HSMul.hSMul (β := ℝ) y ((l : (a : ℝ) → ℝ) 1 : ℝ) = (l : (a : ℝ) → ℝ) y
Tactic: rw [mul_comm, ← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
Goal:
s : Set ℝ
f : ℝ → ℝ
x a : ℝ
hx : x ∈ s
hax : a < f x
hsc : IsClosed s
hfc : LowerSemicontinuousOn f s
hf : ConvexOn ℝ s f
l : ℝ →L[ℝ] ℝ
c' : ℝ
hlc'_le :
  s.restrict (π := fun (a : ℝ) ↦ ℝ) (Function.comp (β := ℝ) (⇑re : (a : ℝ) → ℝ) (⇑l : (a : ℝ) → ℝ)) +
      const (↑s : Type) c' ≤
    s.restrict (π := fun (a : ℝ) ↦ ℝ) f
hlc'_eq : HAdd.hAdd (α := ℝ) ((re : (a : ℝ) → ℝ) ((l : (a : ℝ) → ℝ) x : ℝ) : ℝ) c' = a
y : ℝ
rw : HMul.hMul (β := ℝ) y ((l : (a : ℝ) → ℝ) 1 : ℝ) = (l : (a : ℝ) → ℝ) y
rw₁ : HSMul.hSMul (β := ℝ) y ((l : (a : ℝ) → ℝ) 1 : ℝ) = (l : (a : ℝ) → ℝ) y
⊢ HMul.hMul (α := ℝ) ((l : (a : ℝ) → ℝ) 1 : ℝ) y = (l : (a : ℝ) → ℝ) y
have rw₂ : Eq (α := ℝ) ((l : (a : ℝ) → ℝ) (HSMul.hSMul (β := ℝ) y 1) : ℝ) ((l : (a : ℝ) → ℝ) y : ℝ)
Tactic: rw [mul_comm, ← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
Goal:
s : Set ℝ
f : ℝ → ℝ
x a : ℝ
hx : x ∈ s
hax : a < f x
hsc : IsClosed s
hfc : LowerSemicontinuousOn f s
hf : ConvexOn ℝ s f
l : ℝ →L[ℝ] ℝ
c' : ℝ
hlc'_le :
  s.restrict (π := fun (a : ℝ) ↦ ℝ) (Function.comp (β := ℝ) (⇑re : (a : ℝ) → ℝ) (⇑l : (a : ℝ) → ℝ)) +
      const (↑s : Type) c' ≤
    s.restrict (π := fun (a : ℝ) ↦ ℝ) f
hlc'_eq : HAdd.hAdd (α := ℝ) ((re : (a : ℝ) → ℝ) ((l : (a : ℝ) → ℝ) x : ℝ) : ℝ) c' = a
y : ℝ
rw : HMul.hMul (β := ℝ) y ((l : (a : ℝ) → ℝ) 1 : ℝ) = (l : (a : ℝ) → ℝ) y
rw₁ : HSMul.hSMul (β := ℝ) y ((l : (a : ℝ) → ℝ) 1 : ℝ) = (l : (a : ℝ) → ℝ) y
rw₂ : Eq (α := ℝ) ((l : (a : ℝ) → ℝ) (HSMul.hSMul (β := ℝ) y 1) : ℝ) ((l : (a : ℝ) → ℝ) y : ℝ)
⊢ HMul.hMul (α := ℝ) ((l : (a : ℝ) → ℝ) 1 : ℝ) y = (l : (a : ℝ) → ℝ) y
have rw₃ : Eq (α := ℝ) ((l : (a : ℝ) → ℝ) (y * 1) : ℝ) ((l : (a : ℝ) → ℝ) y : ℝ)
Tactic: rw [mul_comm, ← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
Goal:
s : Set ℝ
f : ℝ → ℝ
x a : ℝ
hx : x ∈ s
hax : a < f x
hsc : IsClosed s
hfc : LowerSemicontinuousOn f s
hf : ConvexOn ℝ s f
l : ℝ →L[ℝ] ℝ
c' : ℝ
hlc'_le :
  s.restrict (π := fun (a : ℝ) ↦ ℝ) (Function.comp (β := ℝ) (⇑re : (a : ℝ) → ℝ) (⇑l : (a : ℝ) → ℝ)) +
      const (↑s : Type) c' ≤
    s.restrict (π := fun (a : ℝ) ↦ ℝ) f
hlc'_eq : HAdd.hAdd (α := ℝ) ((re : (a : ℝ) → ℝ) ((l : (a : ℝ) → ℝ) x : ℝ) : ℝ) c' = a
y : ℝ
rw : HMul.hMul (β := ℝ) y ((l : (a : ℝ) → ℝ) 1 : ℝ) = (l : (a : ℝ) → ℝ) y
rw₁ : HSMul.hSMul (β := ℝ) y ((l : (a : ℝ) → ℝ) 1 : ℝ) = (l : (a : ℝ) → ℝ) y
rw₂ : Eq (α := ℝ) ((l : (a : ℝ) → ℝ) (HSMul.hSMul (β := ℝ) y 1) : ℝ) ((l : (a : ℝ) → ℝ) y : ℝ)
rw₃ : Eq (α := ℝ) ((l : (a : ℝ) → ℝ) (y * 1) : ℝ) ((l : (a : ℝ) → ℝ) y : ℝ)
⊢ HMul.hMul (α := ℝ) ((l : (a : ℝ) → ℝ) 1 : ℝ) y = (l : (a : ℝ) → ℝ) y
have rw₄ : Eq (α := ℝ) ((l : (a : ℝ) → ℝ) y : ℝ) ((l : (a : ℝ) → ℝ) y : ℝ)
Tactic: rw [mul_comm, ← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one]