awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
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}
⊢ (x, (↑a : 𝕜)) ∉ A

Tactic:
simp [A, hax]
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
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}
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
⊢ ∃ (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)

Premises used: LowerSemicontinuousOn.isClosed_re_epigraph, RCLike.geometric_hahn_banach_point_closed
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
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

Tactic:
⟨- c • u, c * re (u x) + a, fun z => ?_, ?_⟩

Premises used: HMul.hMul, HAdd.hAdd, And.intro, Exists.intro, RCLike.re, HSMul.hSMul, DFunLike.coe, Neg.neg
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
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
refine_2 :
  HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ((-c • u : (a : E) → 𝕜) x : 𝕜) : ℝ)
      (HMul.hMul (β := ℝ) c ((re : (a : 𝕜) → ℝ) ((u : (a : E) → 𝕜) x : 𝕜) : ℝ) + a) =
    a
⊢ ∃ (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:
refine ⟨- c • u, c * re (u x) + a, fun z => ?_, ?_⟩
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
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 : 𝕜
rw :
  Eq.{u_1 + 1} (α := 𝕜) ((L : (a : E × 𝕜) → 𝕜) (HSMul.hSMul (β := E × 𝕜) v (0, 1)) : 𝕜)
    ((L : (a : E × 𝕜) → 𝕜) (0, v) : 𝕜)
⊢ HMul.hMul (β := 𝕜) v ((L : (a : E × 𝕜) → 𝕜) (0, 1) : 𝕜) = (L : (a : E × 𝕜) → 𝕜) (0, v)

Tactic:
rw [← smul_eq_mul, ← map_smul]

Premises used: smul_eq_mul, map_smul
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
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 : 𝕜
⊢ Eq.{u_1 + 1} (α := 𝕜) ((L : (a : E × 𝕜) → 𝕜) (HSMul.hSMul (β := E × 𝕜) v (0, 1)) : 𝕜)
    ((L : (a : E × 𝕜) → 𝕜) (0, v) : 𝕜)

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
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)

Tactic:
have hv (v : 𝕜) : v * L (0, 1) = L (0, v) := by rw [← smul_eq_mul, ← map_smul]; simp
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
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
⊢ (w, (↑(φ w) : 𝕜)) ∈ A

Tactic:
simp [A, h]
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
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
⊢ 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))
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
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) : 𝕜)) : 𝕜) : ℝ)
⊢ 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

Premises used: ContinuousLinearMap.coprod_comp_inl_inr
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
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 : 𝕜) → ℝ)
        (((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) : 𝕜)) :
          𝕜) :
      ℝ)
⊢ 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:
simpa [-coprod_comp_inl_inr, ← hv (ofReal a), ← hv (ofReal (φ w)), mul_comm a,
        mul_comm (φ w)] using hw

Premises used: ContinuousLinearMap.coprod_comp_inl_inr, RCLike.ofReal, mul_comm
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
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))

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
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
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))
⊢ 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)
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
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))
hc : 0 < c
⊢ 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:
simpa [smul_re, u, c, mul_add, ← mul_assoc, inv_mul_cancel₀ (ne_of_gt (inv_pos.1 hc))]
      using mul_le_mul_of_nonneg_left (hine z.2).le hc.le

Premises used: RCLike.smul_re, mul_assoc, ne_of_gt, inv_pos, LT.lt.le, Iff.mp, mul_add, mul_le_mul_of_nonneg_left, inv_mul_cancel₀, Subtype.property
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
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) : 𝕜))⁻¹
⊢ HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ((-c • u : (a : E) → 𝕜) x : 𝕜) : ℝ)
      (HMul.hMul (β := ℝ) c ((re : (a : 𝕜) → ℝ) ((u : (a : E) → 𝕜) x : 𝕜) : ℝ) + a) =
    a

Tactic:
simp [u, c, smul_re]

Premises used: RCLike.smul_re
-- Module: Mathlib.Analysis.Convex.Approximation
Goal:
s : Set ℝ
f : ℝ → ℝ
x a : ℝ
hx : x ∈ s
hax : a < f x
hsc : IsClosed s
hfc : LowerSemicontinuousOn f s
hf : ConvexOn ℝ s f
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
⊢ ∃ (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

Premises used: ConvexOn.exists_affine_le_of_lt
-- Module: Mathlib.Analysis.Convex.Approximation
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 : ℝ)
rw₄ rw₅ : Eq (α := ℝ) ((l : (a : ℝ) → ℝ) y : ℝ) ((l : (a : ℝ) → ℝ) y : ℝ)
⊢ HMul.hMul (α := ℝ) ((l : (a : ℝ) → ℝ) 1 : ℝ) y = (l : (a : ℝ) → ℝ) y

Tactic:
rw [mul_comm, ← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one]

Premises used: mul_comm, smul_eq_mul, mul_one, map_smul
-- Module: Mathlib.Analysis.Convex.Approximation
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

Tactic:
have h1 y : l 1 * y = l y := by rw [mul_comm, ← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one]