awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Cone.Extension
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
z : E
hz : z ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ (f.supSpanSingleton y (-c) hy).domain) z hz) : E) ∈ s
refine_2 :
  ∀ (x : E) (hx : x ∈ f.domain) (y' : E)
    (hy' :
      Membership.mem (γ := Submodule ℝ E)
        (LinearPMap.domain (S := ℝ) (σ := RingHom.id ℝ) (LinearPMap.mkSpanSingleton y (-c) ⋯)) y')
    (hz : x + y' ∈ (f.supSpanSingleton y (-c) hy).domain)
    (hzs : (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ (f.supSpanSingleton y (-c) hy).domain) (x + y') hz) : E) ∈ s),
    0 ≤
      (↑(f.supSpanSingleton y (-c) hy) : ↥(f.supSpanSingleton y (-c) hy).domain → ℝ)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ (f.supSpanSingleton y (-c) hy).domain) (x + y') hz)
⊢ 0 ≤
    (↑(f.supSpanSingleton y (-c) hy) : ↥(f.supSpanSingleton y (-c) hy).domain → ℝ)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ (f.supSpanSingleton y (-c) hy).domain) z hz)

Tactic:
rcases mem_sup.1 hz with ⟨x, hx, y', hy', rfl⟩

Premises used: Iff.mp, Submodule.mem_sup, rfl
-- Module: Mathlib.Analysis.Convex.Cone.Extension
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
y' : E
hy' :
  Membership.mem (γ := Submodule ℝ E)
    (LinearPMap.domain (S := ℝ) (σ := RingHom.id ℝ) (LinearPMap.mkSpanSingleton y (-c) ⋯)) y'
hz : x + y' ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ (f.supSpanSingleton y (-c) hy).domain) (x + y') hz) : E) ∈ s
refine_2 :
  ∀ (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 : (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ (f.supSpanSingleton y (-c) hy).domain) (x + r • y) hz) : E) ∈ s),
    0 ≤
      (↑(f.supSpanSingleton y (-c) hy) : ↥(f.supSpanSingleton y (-c) hy).domain → ℝ)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ (f.supSpanSingleton y (-c) hy).domain) (x + r • y) hz)
⊢ 0 ≤
    (↑(f.supSpanSingleton y (-c) hy) : ↥(f.supSpanSingleton y (-c) hy).domain → ℝ)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ (f.supSpanSingleton y (-c) hy).domain) (x + y') hz)

Tactic:
rcases mem_span_singleton.1 hy' with ⟨r, rfl⟩

Premises used: Submodule.mem_span_singleton, Iff.mp, rfl
-- Module: Mathlib.Analysis.Convex.Cone.Extension
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
refine_2 :
  HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
    (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
⊢ 0 ≤
    (↑(f.supSpanSingleton y (-c) hy) : ↥(f.supSpanSingleton y (-c) hy).domain → ℝ)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ (f.supSpanSingleton y (-c) hy).domain) (x + r • y) hz)

Tactic:
rw [LinearPMap.supSpanSingleton_apply_mk _ _ _ _ _ hx, smul_neg, ← sub_eq_add_neg, sub_nonneg]

Premises used: sub_eq_add_neg, smul_neg, LinearPMap.supSpanSingleton_apply_mk, sub_nonneg
-- Module: Mathlib.Analysis.Convex.Cone.Extension
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
refine_2 :
  ∀ (hr : r < 0),
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
      (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
refine_2₁ :
  ∀ (hr : r = 0),
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) c ≤
      (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
refine_2₂ :
  ∀ (hr : 0 < r),
    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)

Tactic:
rcases lt_trichotomy r 0 with (hr | hr | hr)

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Analysis.Convex.Cone.Extension
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 : r < 0
rwa : -r • (-(r⁻¹ • x) - y) ∈ s
rwa₁ : -r • -(r⁻¹ • x) - -r • y ∈ s
rwa₂ : -(-r • r⁻¹ • x) - -r • y ∈ s
rwa₃ : - -(r • r⁻¹ • x) - -r • y ∈ s
rwa₄ : r • r⁻¹ • x - -r • y ∈ s
rwa₅ : (r * r⁻¹) • x - -r • y ∈ s
rwa₆ : HSMul.hSMul (α := ℝ) 1 x - -r • y ∈ s
rwa₇ : x - -r • y ∈ s
rwa₈ : x + -(-r • y) ∈ s
rwa₉ : x + - -(r • y) ∈ s
rwa₁₀ rwa₁₁ rwa₁₂ rwa₁₃ : x + r • y ∈ s
⊢ -(r⁻¹ • x) - y ∈ s

Tactic:
rwa [← s.smul_mem_iff (neg_pos.2 hr), smul_sub, smul_neg, neg_smul, neg_neg, smul_smul,
          mul_inv_cancel₀ hr.ne, one_smul, sub_eq_add_neg, neg_smul, neg_neg]

Premises used: Iff.mpr, neg_smul, mul_inv_cancel₀, neg_pos, sub_eq_add_neg, smul_smul, neg_neg, smul_neg, ConvexCone.smul_mem_iff, one_smul, smul_sub, LT.lt.ne
-- Module: Mathlib.Analysis.Convex.Cone.Extension
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 : r < 0
⊢ -(r⁻¹ • x) - y ∈ s

Tactic:
have : -(r⁻¹ • x) - y ∈ s := by
        rwa [← s.smul_mem_iff (neg_pos.2 hr), smul_sub, smul_neg, neg_smul, neg_neg, smul_smul,
          mul_inv_cancel₀ hr.ne, one_smul, sub_eq_add_neg, neg_smul, neg_neg]
-- Module: Mathlib.Analysis.Convex.Cone.Extension
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 : r < 0
this : -(r⁻¹ • x) - y ∈ s
⊢ (↑f : ↥f.domain → ℝ) (r⁻¹ • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx) ≤ c

Tactic:
replace := le_c (r⁻¹ • ⟨x, hx⟩) this
-- Module: Mathlib.Analysis.Convex.Cone.Extension
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 : r = 0
refine_2 :
  ∀
    (hy' :
      Membership.mem (γ := Submodule ℝ E)
        (LinearPMap.domain (S := ℝ) (σ := RingHom.id ℝ) (LinearPMap.mkSpanSingleton y (-c) ⋯))
        (HSMul.hSMul (α := ℝ) 0 y))
    (hz : x + HSMul.hSMul (α := ℝ) 0 y ∈ (f.supSpanSingleton y (-c) hy).domain)
    (hzs : x + HSMul.hSMul (α := ℝ) 0 y ∈ s),
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) 0 : ℝ) 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:
subst r
-- Module: Mathlib.Analysis.Convex.Cone.Extension
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
hy' :
  Membership.mem (γ := Submodule ℝ E)
    (LinearPMap.domain (S := ℝ) (σ := RingHom.id ℝ) (LinearPMap.mkSpanSingleton y (-c) ⋯)) (HSMul.hSMul (α := ℝ) 0 y)
hz : x + HSMul.hSMul (α := ℝ) 0 y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + HSMul.hSMul (α := ℝ) 0 y ∈ s
⊢ x ∈ s

Tactic:
simp only [zero_smul, add_zero] at hzs ⊢

Premises used: zero_smul, add_zero
-- Module: Mathlib.Analysis.Convex.Cone.Extension
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
hy' :
  Membership.mem (γ := Submodule ℝ E)
    (LinearPMap.domain (S := ℝ) (σ := RingHom.id ℝ) (LinearPMap.mkSpanSingleton y (-c) ⋯)) (HSMul.hSMul (α := ℝ) 0 y)
hz : x + HSMul.hSMul (α := ℝ) 0 y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x ∈ s
refine_2 : 0 ≤ (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)
⊢ HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) 0 : ℝ) c ≤
    (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)

Tactic:
rw [RingHom.id_apply, zero_smul]

Premises used: RingHom.id_apply, zero_smul
-- Module: Mathlib.Analysis.Convex.Cone.Extension
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
hy' :
  Membership.mem (γ := Submodule ℝ E)
    (LinearPMap.domain (S := ℝ) (σ := RingHom.id ℝ) (LinearPMap.mkSpanSingleton y (-c) ⋯)) (HSMul.hSMul (α := ℝ) 0 y)
hz : x + HSMul.hSMul (α := ℝ) 0 y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x ∈ s
refine_2 : (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx) : E) ∈ s
⊢ 0 ≤ (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)

Tactic:
apply nonneg
-- Module: Mathlib.Analysis.Convex.Cone.Extension
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
hy' :
  Membership.mem (γ := Submodule ℝ E)
    (LinearPMap.domain (S := ℝ) (σ := RingHom.id ℝ) (LinearPMap.mkSpanSingleton y (-c) ⋯)) (HSMul.hSMul (α := ℝ) 0 y)
hz : x + HSMul.hSMul (α := ℝ) 0 y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x ∈ s
⊢ (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx) : E) ∈ s

Tactic:
hzs

Premises used: Set.Mem
-- Module: Mathlib.Analysis.Convex.Cone.Extension
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
hy' :
  Membership.mem (γ := Submodule ℝ E)
    (LinearPMap.domain (S := ℝ) (σ := RingHom.id ℝ) (LinearPMap.mkSpanSingleton y (-c) ⋯)) (HSMul.hSMul (α := ℝ) 0 y)
hz : x + HSMul.hSMul (α := ℝ) 0 y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x ∈ s
⊢ (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx) : E) ∈ s

Tactic:
exact hzs
-- Module: Mathlib.Analysis.Convex.Cone.Extension
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
rwa : r • (r⁻¹ • x + y) ∈ s
rwa₁ : r • r⁻¹ • x + r • y ∈ s
rwa₂ : (r * r⁻¹) • x + r • y ∈ s
rwa₃ : HSMul.hSMul (α := ℝ) 1 x + r • y ∈ s
rwa₄ rwa₅ rwa₆ rwa₇ : x + r • y ∈ s
⊢ r⁻¹ • x + y ∈ s

Tactic:
rwa [← s.smul_mem_iff hr, smul_add, smul_smul, mul_inv_cancel₀ hr.ne', one_smul]

Premises used: mul_inv_cancel₀, smul_smul, ConvexCone.smul_mem_iff, one_smul, LT.lt.ne', smul_add
-- Module: Mathlib.Analysis.Convex.Cone.Extension
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
⊢ r⁻¹ • x + y ∈ s

Tactic:
have : r⁻¹ • x + y ∈ s := by
        rwa [← s.smul_mem_iff hr, smul_add, smul_smul, mul_inv_cancel₀ hr.ne', one_smul]
-- Module: Mathlib.Analysis.Convex.Cone.Extension
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 : r⁻¹ • x + y ∈ s
⊢ c ≤ (↑f : ↥f.domain → ℝ) (r⁻¹ • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)

Tactic:
replace := c_le (r⁻¹ • ⟨x, hx⟩) this
-- Module: Mathlib.Analysis.Convex.Cone.Extension
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)
refine_2₅ refine_2₆ refine_2₇ 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)
⊢ 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

Premises used: mul_inv_cancel₀, mul_assoc, LT.lt.ne', LinearPMap.map_smul, smul_eq_mul, one_mul, mul_le_mul_iff_right₀
-- Module: Mathlib.Analysis.Convex.Cone.Extension
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
⊢ c.Nonempty

Tactic:
have cne : c.Nonempty := ⟨y, hy⟩
-- Module: Mathlib.Analysis.Convex.Cone.Extension
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
⊢ DirectedOn (fun (x1 x2 : E →ₗ.[ℝ] ℝ) ↦ x1 ≤ x2) c

Tactic:
have hcd : DirectedOn (· ≤ ·) c := c_chain.directedOn
-- Module: Mathlib.Analysis.Convex.Cone.Extension
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

Tactic:
⟨LinearPMap.sSup c hcd, ?_, fun _ ↦ LinearPMap.le_sSup hcd⟩

Premises used: LinearPMap.sSup, And.intro, Exists.intro, LinearPMap.le_sSup
-- Module: Mathlib.Analysis.Convex.Cone.Extension
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
refine : LinearPMap.sSup c hcd ∈ S
⊢ ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub

Tactic:
refine ⟨LinearPMap.sSup c hcd, ?_, fun _ ↦ LinearPMap.le_sSup hcd⟩
-- Module: Mathlib.Analysis.Convex.Cone.Extension
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
⊢ 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)