awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -(↑x : E) - y ∈ s → (↑f : ↥f.domain → ℝ) x ≤ c
c_le : ∀ (x : ↥f.domain), (↑x : E) + y ∈ s → c ≤ (↑f : ↥f.domain → ℝ) x
x : E
hx : x ∈ f.domain
r : ℝ
hy' :
  Membership.mem (γ := Submodule ℝ E)
    (LinearPMap.domain (S := ℝ) (σ := RingHom.id ℝ) (LinearPMap.mkSpanSingleton y (-c) ⋯)) (r • y)
hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + r • y ∈ s
hr : 0 < r
this : c ≤ (↑f : ↥f.domain → ℝ) (r⁻¹ • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
refine_2 :
  ∀ (this : r * c ≤ r * (↑f : ↥f.domain → ℝ) (r⁻¹ • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)),
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
      (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
refine_2₁ :
  ∀ (this : r * c ≤ r * r⁻¹ • (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)),
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
      (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
refine_2₂ :
  ∀ (this : r * c ≤ r * (r⁻¹ * (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx))),
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
      (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
refine_2₃ :
  ∀ (this : r * c ≤ r * r⁻¹ * (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)),
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
      (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
refine_2₄ :
  ∀ (this : r * c ≤ 1 * (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)),
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
      (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
⊢ HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
    (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
have refine_2₅ : ∀ (this : r * c ≤ (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)),
  HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
    (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
Tactic: rwa [← mul_le_mul_iff_right₀ hr, f.map_smul, smul_eq_mul, ← mul_assoc, mul_inv_cancel₀ hr.ne',
        one_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (hypothesis)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
S : Set (E →ₗ.[ℝ] ℝ) := {p : E →ₗ.[ℝ] ℝ | ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
⊢ ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
have cne : c.Nonempty
Tactic: have cne : c.Nonempty := ⟨y, hy⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (hypothesis)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
S : Set (E →ₗ.[ℝ] ℝ) := {p : E →ₗ.[ℝ] ℝ | ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : c.Nonempty
⊢ ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
have hcd : DirectedOn (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c
Tactic: have hcd : DirectedOn (· ≤ ·) c := c_chain.directedOn
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
S : Set (E →ₗ.[ℝ] ℝ) := {p : E →ₗ.[ℝ] ℝ | ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : c.Nonempty
hcd : DirectedOn (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c
⊢ ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
have refine : LinearPMap.sSup c hcd ∈ S
Tactic: refine ⟨LinearPMap.sSup c hcd, ?_, fun _ ↦ LinearPMap.le_sSup hcd⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (hypothesis)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
S : Set (E →ₗ.[ℝ] ℝ) := {p : E →ₗ.[ℝ] ℝ | ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : c.Nonempty
hcd : DirectedOn (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c
x : E
hx : x ∈ (LinearPMap.sSup c hcd).domain
hxs : (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ (LinearPMap.sSup c hcd).domain) x hx) : E) ∈ s
⊢ 0 ≤
    (↑(LinearPMap.sSup c hcd) : ↥(LinearPMap.sSup c hcd).domain → ℝ)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ (LinearPMap.sSup c hcd).domain) x hx)
have hdir : DirectedOn (fun (x1 x2 : Submodule ℝ E) ↦ x1 ≤ x2) (LinearPMap.domain '' c)
Tactic: have hdir : DirectedOn (· ≤ ·) (LinearPMap.domain '' c) :=
      directedOn_image.2 (hcd.mono LinearPMap.domain_mono.monotone)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
S : Set (E →ₗ.[ℝ] ℝ) := {p : E →ₗ.[ℝ] ℝ | ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : c.Nonempty
hcd : DirectedOn (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c
x : E
hx : x ∈ (LinearPMap.sSup c hcd).domain
hxs : (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ (LinearPMap.sSup c hcd).domain) x hx) : E) ∈ s
hdir : DirectedOn (fun (x1 x2 : Submodule ℝ E) ↦ x1 ≤ x2) (LinearPMap.domain '' c)
⊢ 0 ≤
    (↑(LinearPMap.sSup c hcd) : ↥(LinearPMap.sSup c hcd).domain → ℝ)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ (LinearPMap.sSup c hcd).domain) x hx)
have rcases : ∀ (f : E →ₗ.[ℝ] ℝ) (hfc : f ∈ c) (hfx : x ∈ f.domain),
  0 ≤
    (↑(LinearPMap.sSup c hcd) : ↥(LinearPMap.sSup c hcd).domain → ℝ)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ (LinearPMap.sSup c hcd).domain) x hx)
Tactic: rcases (mem_sSup_of_directed (cne.image _) hdir).1 hx with ⟨_, ⟨f, hfc, rfl⟩, hfx⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (hypothesis)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
S : Set (E →ₗ.[ℝ] ℝ) := {p : E →ₗ.[ℝ] ℝ | ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : c.Nonempty
hcd : DirectedOn (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c
x : E
hx : x ∈ (LinearPMap.sSup c hcd).domain
hxs : (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ (LinearPMap.sSup c hcd).domain) x hx) : E) ∈ s
hdir : DirectedOn (fun (x1 x2 : Submodule ℝ E) ↦ x1 ≤ x2) (LinearPMap.domain '' c)
f : E →ₗ.[ℝ] ℝ
hfc : f ∈ c
hfx : x ∈ f.domain
⊢ 0 ≤
    (↑(LinearPMap.sSup c hcd) : ↥(LinearPMap.sSup c hcd).domain → ℝ)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ (LinearPMap.sSup c hcd).domain) x hx)
have this : f ≤ LinearPMap.sSup c hcd
Tactic: have : f ≤ LinearPMap.sSup c hcd := LinearPMap.le_sSup _ hfc
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
S : Set (E →ₗ.[ℝ] ℝ) := {p : E →ₗ.[ℝ] ℝ | ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
cne : c.Nonempty
hcd : DirectedOn (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c
x : E
hx : x ∈ (LinearPMap.sSup c hcd).domain
hxs : (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ (LinearPMap.sSup c hcd).domain) x hx) : E) ∈ s
hdir : DirectedOn (fun (x1 x2 : Submodule ℝ E) ↦ x1 ≤ x2) (LinearPMap.domain '' c)
f : E →ₗ.[ℝ] ℝ
hfc : f ∈ c
hfx : x ∈ f.domain
this : f ≤ LinearPMap.sSup c hcd
⊢ 0 ≤
    (↑(LinearPMap.sSup c hcd) : ↥(LinearPMap.sSup c hcd).domain → ℝ)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ (LinearPMap.sSup c hcd).domain) x hx)
have h : (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx) =
  (↑(LinearPMap.sSup c hcd) : ↥(LinearPMap.sSup c hcd).domain → ℝ)
    (Subtype.mk (p := fun (x : E) ↦ x ∈ (LinearPMap.sSup c hcd).domain) x hx)
Tactic: convert! ← hcs hfc ⟨x, hfx⟩ hxs using 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (hypothesis)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x
hp_dense : ∀ (y : E), ∃ (x : ↥p.domain), (↑x : E) + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p : E →ₗ.[ℝ] ℝ | ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x}
⊢ ∃ q ≥ p, q.domain = ⊤ ∧ ∀ (x : ↥q.domain), (↑x : E) ∈ s → 0 ≤ (↑q : ↥q.domain → ℝ) x
have hSc : ∀ c ⊆ S, IsChain (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
Tactic: have hSc : ∀ c, c ⊆ S → IsChain (· ≤ ·) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub := by
    intro c hcs c_chain y hy
    clear hp_nonneg hp_dense p
    have cne : c.Nonempty := ⟨y, hy⟩
    have hcd : DirectedOn (· ≤ ·) c := c_chain.directedOn
    refine ⟨LinearPMap.sSup c hcd, ?_, fun _ ↦ LinearPMap.le_sSup hcd⟩
    rintro ⟨x, hx⟩ hxs
    have hdir : DirectedOn (· ≤ ·) (LinearPMap.domain '' c) :=
      directedOn_image.2 (hcd.mono LinearPMap.domain_mono.monotone)
    rcases (mem_sSup_of_directed (cne.image _) hdir).1 hx with ⟨_, ⟨f, hfc, rfl⟩, hfx⟩
    have : f ≤ LinearPMap.sSup c hcd := LinearPMap.le_sSup _ hfc
    convert! ← hcs hfc ⟨x, hfx⟩ hxs using 1
    exact this.2 rfl
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x
hp_dense : ∀ (y : E), ∃ (x : ↥p.domain), (↑x : E) + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p : E →ₗ.[ℝ] ℝ | ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x}
hSc : ∀ c ⊆ S, IsChain (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
⊢ ∃ q ≥ p, q.domain = ⊤ ∧ ∀ (x : ↥q.domain), (↑x : E) ∈ s → 0 ≤ (↑q : ↥q.domain → ℝ) x
have obtain : ∀ (q : E →ₗ.[ℝ] ℝ) (hpq : p ≤ q) (hqs : q ∈ S)
  (hq : ∀ ⦃y : E →ₗ.[ℝ] ℝ⦄, (fun (x : E →ₗ.[ℝ] ℝ) ↦ x ∈ S) y → q ≤ y → y ≤ q),
  ∃ q ≥ p, q.domain = ⊤ ∧ ∀ (x : ↥q.domain), (↑x : E) ∈ s → 0 ≤ (↑q : ↥q.domain → ℝ) x
Tactic: obtain ⟨q, hpq, hqs, hq⟩ := zorn_le_nonempty₀ S hSc p hp_nonneg
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x
hp_dense : ∀ (y : E), ∃ (x : ↥p.domain), (↑x : E) + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p : E →ₗ.[ℝ] ℝ | ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x}
hSc : ∀ c ⊆ S, IsChain (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
q : E →ₗ.[ℝ] ℝ
hpq : p ≤ q
hqs : q ∈ S
hq : ∀ ⦃y : E →ₗ.[ℝ] ℝ⦄, (fun (x : E →ₗ.[ℝ] ℝ) ↦ x ∈ S) y → q ≤ y → y ≤ q
⊢ ∃ q ≥ p, q.domain = ⊤ ∧ ∀ (x : ↥q.domain), (↑x : E) ∈ s → 0 ≤ (↑q : ↥q.domain → ℝ) x
have refine : q.domain = ⊤
Tactic: refine ⟨q, hpq, ?_, hqs⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x
hp_dense : ∀ (y : E), ∃ (x : ↥p.domain), (↑x : E) + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p : E →ₗ.[ℝ] ℝ | ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x}
hSc : ∀ c ⊆ S, IsChain (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
q : E →ₗ.[ℝ] ℝ
hpq : p ≤ q
hqs : q ∈ S
hq : ∀ ⦃y : E →ₗ.[ℝ] ℝ⦄, (fun (x : E →ₗ.[ℝ] ℝ) ↦ x ∈ S) y → q ≤ y → y ≤ q
⊢ q.domain = ⊤
have contrapose! : ∀ (hq : q.domain ≠ ⊤), ∃ y ∈ S, q ≤ y ∧ ¬y ≤ q
Tactic: contrapose! hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (hypothesis)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x
hp_dense : ∀ (y : E), ∃ (x : ↥p.domain), (↑x : E) + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p : E →ₗ.[ℝ] ℝ | ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x}
hSc : ∀ c ⊆ S, IsChain (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
q : E →ₗ.[ℝ] ℝ
hpq : p ≤ q
hqs : q ∈ S
hq : q.domain ≠ ⊤
⊢ ∃ y ∈ S, q ≤ y ∧ ¬y ≤ q
have hqd : ∀ (y : E), ∃ (x : ↥q.domain), (↑x : E) + y ∈ s
Tactic: have hqd : ∀ y, ∃ x : q.domain, (x : E) + y ∈ s := fun y ↦
    let ⟨x, hx⟩ := hp_dense y
    ⟨Submodule.inclusion hpq.left x, hx⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x
hp_dense : ∀ (y : E), ∃ (x : ↥p.domain), (↑x : E) + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p : E →ₗ.[ℝ] ℝ | ∀ (x : ↥p.domain), (↑x : E) ∈ s → 0 ≤ (↑p : ↥p.domain → ℝ) x}
hSc : ∀ c ⊆ S, IsChain (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
q : E →ₗ.[ℝ] ℝ
hpq : p ≤ q
hqs : q ∈ S
hq : q.domain ≠ ⊤
hqd : ∀ (y : E), ∃ (x : ↥q.domain), (↑x : E) + y ∈ s
⊢ ∃ y ∈ S, q ≤ y ∧ ¬y ≤ q
have rcases : ∀ (r : E →ₗ.[ℝ] ℝ) (hqr : q < r) (hr : ∀ (x : ↥r.domain), (↑x : E) ∈ s → 0 ≤ (↑r : ↥r.domain → ℝ) x),
  ∃ y ∈ S, q ≤ y ∧ ¬y ≤ q
Tactic: rcases step s q hqs hqd hq with ⟨r, hqr, hr⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
⊢ ∃ (g : E →ₗ[ℝ] ℝ),
    (∀ (x : ↥f.domain), (g : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x) ∧
      ∀ x ∈ s, LE.le (α := ℝ) (0 : ℝ) ((g : (a : E) → ℝ) x : ℝ)
have rcases : ∀ (g : ↥⊤ →ₗ[ℝ] ℝ)
  (hfg :
    ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ }.domain⦄ (_h : (↑x : E) = (↑y : E)),
      (↑f : ↥f.domain → ℝ) x = (↑{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ } : ↥{ domain := ⊤, toFun := g }.domain → ℝ) y)
  (hgs :
    ∀ (x : ↥{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ }.domain),
      (↑x : E) ∈ s → 0 ≤ (↑{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ } : ↥{ domain := ⊤, toFun := g }.domain → ℝ) x),
  ∃ (g : E →ₗ[ℝ] ℝ),
    (∀ (x : ↥f.domain), (g : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x) ∧
      ∀ x ∈ s, LE.le (α := ℝ) (0 : ℝ) ((g : (a : E) → ℝ) x : ℝ)
Tactic: rcases RieszExtension.exists_top s f nonneg dense
    with ⟨⟨g_dom, g⟩, ⟨-, hfg⟩, rfl : g_dom = ⊤, hgs⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
g : ↥⊤ →ₗ[ℝ] ℝ
hfg :
  ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ }.domain⦄ (_h : (↑x : E) = (↑y : E)),
    (↑f : ↥f.domain → ℝ) x = (↑{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ } : ↥{ domain := ⊤, toFun := g }.domain → ℝ) y
hgs :
  ∀ (x : ↥{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ }.domain),
    (↑x : E) ∈ s → 0 ≤ (↑{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ } : ↥{ domain := ⊤, toFun := g }.domain → ℝ) x
⊢ ∃ (g : E →ₗ[ℝ] ℝ),
    (∀ (x : ↥f.domain), (g : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x) ∧
      ∀ x ∈ s, LE.le (α := ℝ) (0 : ℝ) ((g : (a : E) → ℝ) x : ℝ)
have refine_1 : ∀ (x : ↥f.domain), (g ∘ₗ LinearMap.codRestrict ⊤ LinearMap.id sorry : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x
Tactic: refine ⟨g.comp (LinearMap.id.codRestrict ⊤ fun _ ↦ trivial), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), (↑x : E) ∈ s → 0 ≤ (↑f : ↥f.domain → ℝ) x
dense : ∀ (y : E), ∃ (x : ↥f.domain), (↑x : E) + y ∈ s
g : ↥⊤ →ₗ[ℝ] ℝ
hfg :
  ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ }.domain⦄ (_h : (↑x : E) = (↑y : E)),
    (↑f : ↥f.domain → ℝ) x = (↑{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ } : ↥{ domain := ⊤, toFun := g }.domain → ℝ) y
hgs :
  ∀ (x : ↥{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ }.domain),
    (↑x : E) ∈ s → 0 ≤ (↑{ domain := ⊤, toFun := g : E →ₗ.[ℝ] ℝ } : ↥{ domain := ⊤, toFun := g }.domain → ℝ) x
refine_1 :
  ∀ (x : ↥f.domain), (g ∘ₗ LinearMap.codRestrict ⊤ LinearMap.id ⋯ : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x
⊢ ∃ (g : E →ₗ[ℝ] ℝ),
    (∀ (x : ↥f.domain), (g : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x) ∧
      ∀ x ∈ s, LE.le (α := ℝ) (0 : ℝ) ((g : (a : E) → ℝ) x : ℝ)
have refine_2 : ∀ x ∈ s, LE.le (α := ℝ) (0 : ℝ) ((g ∘ₗ LinearMap.codRestrict ⊤ LinearMap.id sorry : (a : E) → ℝ) x : ℝ)
Tactic: refine ⟨g.comp (LinearMap.id.codRestrict ⊤ fun _ ↦ trivial), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), (↑f : ↥f.domain → ℝ) x ≤ N (↑x : E)
c : ℝ
hc : 0 < c
p : E × ℝ
hp : Membership.mem (γ := Set (E × ℝ)) {p : E × ℝ | N p.1 ≤ p.2} p
⊢ c * N p.1 ≤ c * p.2
have hbc : N p.1 ≤ p.2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (hypothesis)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), (↑f : ↥f.domain → ℝ) x ≤ N (↑x : E)
s : ConvexCone ℝ (E × ℝ) := { carrier := {p : E × ℝ | N p.1 ≤ p.2}, smul_mem' := ⋯, add_mem' := ⋯ }
f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (toPMap LinearMap.id ⊤)
⊢ ∃ (g : E →ₗ[ℝ] ℝ),
    (∀ (x : ↥f.domain), (g : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x) ∧ ∀ (x : E), (g : (a : E) → ℝ) x ≤ N x
have hf'_nonneg : ∀ (x : ↥f'.domain), (↑x : E × ℝ) ∈ s → 0 ≤ (↑f' : ↥f'.domain → ℝ) x
Tactic: have hf'_nonneg : ∀ x : f'.domain, x.1 ∈ s → 0 ≤ f' x := fun x (hx : N x.1.1 ≤ x.1.2) ↦ by
    simpa [f'] using le_trans (hf ⟨x.1.1, x.2.1⟩) hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), (↑f : ↥f.domain → ℝ) x ≤ N (↑x : E)
s : ConvexCone ℝ (E × ℝ) := { carrier := {p : E × ℝ | N p.1 ≤ p.2}, smul_mem' := ⋯, add_mem' := ⋯ }
f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : ↥f'.domain), (↑x : E × ℝ) ∈ s → 0 ≤ (↑f' : ↥f'.domain → ℝ) x
x : E
y : ℝ
⊢ ∃ (x_1 : ↥f'.domain), (↑x_1 : E × ℝ) + (x, y) ∈ s
have refine : (↑(Subtype.mk (p := fun (x : E × ℝ) ↦ x ∈ f'.domain) (0, N x - y) sorry) : E × ℝ) + (x, y) ∈ s
Tactic: refine ⟨⟨(0, N x - y), ⟨f.domain.zero_mem, trivial⟩⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (hypothesis)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), (↑f : ↥f.domain → ℝ) x ≤ N (↑x : E)
s : ConvexCone ℝ (E × ℝ) := { carrier := {p : E × ℝ | N p.1 ≤ p.2}, smul_mem' := ⋯, add_mem' := ⋯ }
f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : ↥f'.domain), (↑x : E × ℝ) ∈ s → 0 ≤ (↑f' : ↥f'.domain → ℝ) x
⊢ ∃ (g : E →ₗ[ℝ] ℝ),
    (∀ (x : ↥f.domain), (g : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x) ∧ ∀ (x : E), (g : (a : E) → ℝ) x ≤ N x
have hf'_dense : ∀ (y : E × ℝ), ∃ (x : ↥f'.domain), (↑x : E × ℝ) + y ∈ s
Tactic: have hf'_dense : ∀ y : E × ℝ, ∃ x : f'.domain, ↑x + y ∈ s := by
    rintro ⟨x, y⟩
    refine ⟨⟨(0, N x - y), ⟨f.domain.zero_mem, trivial⟩⟩, ?_⟩
    simp only [s, ConvexCone.mem_mk, mem_setOf_eq, Prod.fst_add, Prod.snd_add, zero_add,
      sub_add_cancel, le_rfl]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), (↑f : ↥f.domain → ℝ) x ≤ N (↑x : E)
s : ConvexCone ℝ (E × ℝ) := { carrier := {p : E × ℝ | N p.1 ≤ p.2}, smul_mem' := ⋯, add_mem' := ⋯ }
f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : ↥f'.domain), (↑x : E × ℝ) ∈ s → 0 ≤ (↑f' : ↥f'.domain → ℝ) x
hf'_dense : ∀ (y : E × ℝ), ∃ (x : ↥f'.domain), (↑x : E × ℝ) + y ∈ s
⊢ ∃ (g : E →ₗ[ℝ] ℝ),
    (∀ (x : ↥f.domain), (g : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x) ∧ ∀ (x : E), (g : (a : E) → ℝ) x ≤ N x
have obtain : ∀ (g : E × ℝ →ₗ[ℝ] ℝ) (g_eq : ∀ (x : ↥f'.domain), (g : (a : E × ℝ) → ℝ) (↑x : E × ℝ) = (↑f' : ↥f'.domain → ℝ) x)
  (g_nonneg : ∀ x ∈ s, LE.le (α := ℝ) (0 : ℝ) ((g : (a : E × ℝ) → ℝ) x : ℝ)),
  ∃ (g : E →ₗ[ℝ] ℝ),
    (∀ (x : ↥f.domain), (g : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x) ∧ ∀ (x : E), (g : (a : E) → ℝ) x ≤ N x
Tactic: obtain ⟨g, g_eq, g_nonneg⟩ := riesz_extension s f' hf'_nonneg hf'_dense
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (hypothesis)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), (↑f : ↥f.domain → ℝ) x ≤ N (↑x : E)
s : ConvexCone ℝ (E × ℝ) := { carrier := {p : E × ℝ | N p.1 ≤ p.2}, smul_mem' := ⋯, add_mem' := ⋯ }
f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : ↥f'.domain), (↑x : E × ℝ) ∈ s → 0 ≤ (↑f' : ↥f'.domain → ℝ) x
hf'_dense : ∀ (y : E × ℝ), ∃ (x : ↥f'.domain), (↑x : E × ℝ) + y ∈ s
g : E × ℝ →ₗ[ℝ] ℝ
g_eq : ∀ (x : ↥f'.domain), (g : (a : E × ℝ) → ℝ) (↑x : E × ℝ) = (↑f' : ↥f'.domain → ℝ) x
g_nonneg : ∀ x ∈ s, LE.le (α := ℝ) (0 : ℝ) ((g : (a : E × ℝ) → ℝ) x : ℝ)
⊢ ∃ (g : E →ₗ[ℝ] ℝ),
    (∀ (x : ↥f.domain), (g : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x) ∧ ∀ (x : E), (g : (a : E) → ℝ) x ≤ N x
have g_eq₁ : ∀ (x : ↥f.domain) (y : ℝ), (g : (a : E × ℝ) → ℝ) ((↑x : E), y) = y - (↑f : ↥f.domain → ℝ) x
Tactic: replace g_eq : ∀ (x : f.domain) (y : ℝ), g (x, y) = y - f x := fun x y ↦
    (g_eq ⟨(x, y), ⟨x.2, trivial⟩⟩).trans (sub_eq_neg_add _ _).symm
Cleared hypotheses: g_eq
-- Lean 4 proof step from Mathlib.Analysis.Convex.Cone.Extension (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), (↑f : ↥f.domain → ℝ) x ≤ N (↑x : E)
s : ConvexCone ℝ (E × ℝ) := { carrier := {p : E × ℝ | N p.1 ≤ p.2}, smul_mem' := ⋯, add_mem' := ⋯ }
f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (toPMap LinearMap.id ⊤)
hf'_nonneg : ∀ (x : ↥f'.domain), (↑x : E × ℝ) ∈ s → 0 ≤ (↑f' : ↥f'.domain → ℝ) x
hf'_dense : ∀ (y : E × ℝ), ∃ (x : ↥f'.domain), (↑x : E × ℝ) + y ∈ s
g : E × ℝ →ₗ[ℝ] ℝ
g_nonneg : ∀ x ∈ s, LE.le (α := ℝ) (0 : ℝ) ((g : (a : E × ℝ) → ℝ) x : ℝ)
g_eq : ∀ (x : ↥f.domain) (y : ℝ), (g : (a : E × ℝ) → ℝ) ((↑x : E), y) = y - (↑f : ↥f.domain → ℝ) x
⊢ ∃ (g : E →ₗ[ℝ] ℝ),
    (∀ (x : ↥f.domain), (g : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x) ∧ ∀ (x : E), (g : (a : E) → ℝ) x ≤ N x
have refine_1 : ∀ (x : ↥f.domain), (-g ∘ₗ inl ℝ E ℝ : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x
Tactic: refine ⟨-g.comp (inl ℝ E ℝ), fun x ↦ ?_, fun x ↦ ?_⟩