awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : AddCommGroup M
inst_4 : Nontrivial M
inst_5 : Module R M
C : ConvexCone R M
h : Eq (α := Submodule R M) (Submodule.span R (↑C : Set M)) ⊤
x : M
hne : (↑C : Set M).Nonempty
obtain : ∀ (c : M) (hc : c ∈ (↑C : Set M)), 0 ∈ (↑C : Set M) - (↑C : Set M)
⊢ 0 ∈ (↑C : Set M) - (↑C : Set M)

Tactic:
obtain ⟨c, hc⟩ := hne
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : AddCommGroup M
inst_4 : Nontrivial M
inst_5 : Module R M
C : ConvexCone R M
h : Eq (α := Submodule R M) (Submodule.span R (↑C : Set M)) ⊤
x c : M
hc : c ∈ (↑C : Set M)
⊢ 0 ∈ (↑C : Set M) - (↑C : Set M)

Tactic:
⟨c, hc, c, hc, sub_self c⟩

Premises used: sub_self, Set.Mem, setOf, Set.image2, And.intro, Exists.intro
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : AddCommGroup M
inst_4 : Nontrivial M
inst_5 : Module R M
C : ConvexCone R M
h : Eq (α := Submodule R M) (Submodule.span R (↑C : Set M)) ⊤
x c : M
hc : c ∈ (↑C : Set M)
⊢ 0 ∈ (↑C : Set M) - (↑C : Set M)

Tactic:
exact ⟨c, hc, c, hc, sub_self c⟩
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : AddCommGroup M
inst_4 : Nontrivial M
inst_5 : Module R M
C : ConvexCone R M
h : Eq (α := Submodule R M) (Submodule.span R (↑C : Set M)) ⊤
x : M
hne : (↑C : Set M).Nonempty
r : R
y : M
hy : y ∈ (↑C : Set M)
z : M
hz : z ∈ (↑C : Set M)
simp : ∃ x ∈ C, ∃ y_1 ∈ C, x - y_1 = r • (y - z)
⊢ HSMul.hSMul (β := M) r ((fun (x1 x2 : M) ↦ x1 - x2) y z) ∈ (↑C : Set M) - (↑C : Set M)

Tactic:
simp only [Set.mem_sub, SetLike.mem_coe]

Premises used: Set.mem_sub, SetLike.mem_coe
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : AddCommGroup M
inst_4 : Nontrivial M
inst_5 : Module R M
C : ConvexCone R M
h : Eq (α := Submodule R M) (Submodule.span R (↑C : Set M)) ⊤
x : M
hne : (↑C : Set M).Nonempty
r : R
y : M
hy : y ∈ (↑C : Set M)
z : M
hz : z ∈ (↑C : Set M)
inl : ∀ (hr : r < 0), ∃ x ∈ C, ∃ y_1 ∈ C, x - y_1 = r • (y - z)
inr : ∃ x ∈ C, ∃ y_1 ∈ C, x - y_1 = HSMul.hSMul.{u_7, u_8, u_8} (α := R) 0 (y - z)
inr₁ : ∀ (hr : 0 < r), ∃ x ∈ C, ∃ y_1 ∈ C, x - y_1 = r • (y - z)
⊢ ∃ x ∈ C, ∃ y_1 ∈ C, x - y_1 = r • (y - z)

Tactic:
rcases lt_trichotomy r 0 with hr | rfl | hr

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : AddCommGroup M
inst_4 : Nontrivial M
inst_5 : Module R M
C : ConvexCone R M
h : Eq (α := Submodule R M) (Submodule.span R (↑C : Set M)) ⊤
x : M
hne : (↑C : Set M).Nonempty
r : R
y : M
hy : y ∈ (↑C : Set M)
z : M
hz : z ∈ (↑C : Set M)
hr : r < 0
⊢ ∃ x ∈ C, ∃ y_1 ∈ C, x - y_1 = r • (y - z)

Tactic:
⟨(-r) • z, C.smul_mem (neg_pos.mpr hr) hz,
               (-r) • y, C.smul_mem (neg_pos.mpr hr) hy, ?_⟩

Premises used: Iff.mpr, neg_pos, ConvexCone.smul_mem, And.intro, Exists.intro, HSMul.hSMul, Neg.neg
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : AddCommGroup M
inst_4 : Nontrivial M
inst_5 : Module R M
C : ConvexCone R M
h : Eq (α := Submodule R M) (Submodule.span R (↑C : Set M)) ⊤
x : M
hne : (↑C : Set M).Nonempty
r : R
y : M
hy : y ∈ (↑C : Set M)
z : M
hz : z ∈ (↑C : Set M)
hr : r < 0
inl : -r • z - -r • y = r • (y - z)
⊢ ∃ x ∈ C, ∃ y_1 ∈ C, x - y_1 = r • (y - z)

Tactic:
refine ⟨(-r) • z, C.smul_mem (neg_pos.mpr hr) hz,
               (-r) • y, C.smul_mem (neg_pos.mpr hr) hy, ?_⟩
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : AddCommGroup M
inst_4 : Nontrivial M
inst_5 : Module R M
C : ConvexCone R M
h : Eq (α := Submodule R M) (Submodule.span R (↑C : Set M)) ⊤
x : M
hne : (↑C : Set M).Nonempty
r : R
y : M
hy : y ∈ (↑C : Set M)
z : M
hz : z ∈ (↑C : Set M)
hr : r < 0
inl : -(r • z) - -r • y = r • (y - z)
inl₁ : -(r • z) - -(r • y) = r • (y - z)
inl₂ : r • y - r • z = r • (y - z)
inl₃ inl₄ : r • y - r • z = r • y - r • z
⊢ -r • z - -r • y = r • (y - z)

Tactic:
rw [neg_smul, neg_smul, neg_sub_neg, smul_sub]

Premises used: neg_smul, smul_sub, neg_sub_neg
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : AddCommGroup M
inst_4 : Nontrivial M
inst_5 : Module R M
C : ConvexCone R M
h : Eq (α := Submodule R M) (Submodule.span R (↑C : Set M)) ⊤
x : M
hne : (↑C : Set M).Nonempty
y : M
hy : y ∈ (↑C : Set M)
z : M
hz : z ∈ (↑C : Set M)
inr : ∃ x ∈ C, ∃ y ∈ C, x - y = 0
⊢ ∃ x ∈ C, ∃ y_1 ∈ C, x - y_1 = HSMul.hSMul.{u_7, u_8, u_8} (α := R) 0 (y - z)

Tactic:
simp only [zero_smul]

Premises used: zero_smul
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : AddCommGroup M
inst_4 : Nontrivial M
inst_5 : Module R M
C : ConvexCone R M
h : Eq (α := Submodule R M) (Submodule.span R (↑C : Set M)) ⊤
x : M
hne : (↑C : Set M).Nonempty
y : M
hy : y ∈ (↑C : Set M)
z : M
hz : z ∈ (↑C : Set M)
inr : ∀ (c : M) (hc : c ∈ (↑C : Set M)), ∃ x ∈ C, ∃ y ∈ C, x - y = 0
⊢ ∃ x ∈ C, ∃ y ∈ C, x - y = 0

Tactic:
obtain ⟨c, hc⟩ := hne
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : AddCommGroup M
inst_4 : Nontrivial M
inst_5 : Module R M
C : ConvexCone R M
h : Eq (α := Submodule R M) (Submodule.span R (↑C : Set M)) ⊤
x y : M
hy : y ∈ (↑C : Set M)
z : M
hz : z ∈ (↑C : Set M)
c : M
hc : c ∈ (↑C : Set M)
⊢ ∃ x ∈ C, ∃ y ∈ C, x - y = 0

Tactic:
⟨c, hc, c, hc, sub_self c⟩

Premises used: sub_self, And.intro, Exists.intro
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : AddCommGroup M
inst_4 : Nontrivial M
inst_5 : Module R M
C : ConvexCone R M
h : Eq (α := Submodule R M) (Submodule.span R (↑C : Set M)) ⊤
x y : M
hy : y ∈ (↑C : Set M)
z : M
hz : z ∈ (↑C : Set M)
c : M
hc : c ∈ (↑C : Set M)
⊢ ∃ x ∈ C, ∃ y ∈ C, x - y = 0

Tactic:
exact ⟨c, hc, c, hc, sub_self c⟩
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : AddCommGroup M
inst_4 : Nontrivial M
inst_5 : Module R M
C : ConvexCone R M
h : Eq (α := Submodule R M) (Submodule.span R (↑C : Set M)) ⊤
x : M
hne : (↑C : Set M).Nonempty
r : R
y : M
hy : y ∈ (↑C : Set M)
z : M
hz : z ∈ (↑C : Set M)
hr : 0 < r
⊢ ∃ x ∈ C, ∃ y_1 ∈ C, x - y_1 = r • (y - z)

Tactic:
⟨r • y, C.smul_mem hr hy, r • z, C.smul_mem hr hz, (smul_sub r y z).symm⟩

Premises used: ConvexCone.smul_mem, smul_sub, And.intro, Exists.intro, HSMul.hSMul, Eq.symm
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : AddCommGroup M
inst_4 : Nontrivial M
inst_5 : Module R M
C : ConvexCone R M
h : Eq (α := Submodule R M) (Submodule.span R (↑C : Set M)) ⊤
x : M
hne : (↑C : Set M).Nonempty
r : R
y : M
hy : y ∈ (↑C : Set M)
z : M
hz : z ∈ (↑C : Set M)
hr : 0 < r
⊢ ∃ x ∈ C, ∃ y_1 ∈ C, x - y_1 = r • (y - z)

Tactic:
exact ⟨r • y, C.smul_mem hr hy, r • z, C.smul_mem hr hz, (smul_sub r y z).symm⟩
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : AddCommGroup M
inst_4 : Nontrivial M
inst_5 : Module R M
C : ConvexCone R M
h : Eq (α := Submodule R M) (Submodule.span R (↑C : Set M)) ⊤
x : M
hne : (↑C : Set M).Nonempty
S : Submodule R M := { carrier := (↑C : Set M) - (↑C : Set M), add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ (↑C : Set M) ⊆ (↑S : Set M)

Tactic:
have hCS : (C : Set M) ⊆ S := fun x hx ↦
    let ⟨c, hc⟩ := hne; ⟨x + c, C.add_mem hx hc, c, hc, add_sub_cancel_right x c⟩
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : AddCommGroup M
inst_4 : Nontrivial M
inst_5 : Module R M
C : ConvexCone R M
h : Eq (α := Submodule R M) (Submodule.span R (↑C : Set M)) ⊤
x : M
hne : (↑C : Set M).Nonempty
S : Submodule R M := { carrier := (↑C : Set M) - (↑C : Set M), add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hCS : (↑C : Set M) ⊆ (↑S : Set M)
⊢ x ∈ (↑C : Set M) - (↑C : Set M)

Tactic:
exact (h ▸ Submodule.span_le.mpr hCS) trivial
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : LinearOrder R
inst_2 : AddLeftStrictMono R
inst_3 : AddCommGroup M
inst_4 : Nontrivial M
inst_5 : Module R M
C : ConvexCone R M
⊢ Eq (α := Submodule R M) (Submodule.span R (↑C : Set M)) ⊤ ↔ C.IsReproducing

Tactic:
⟨.of_span_eq_top, IsReproducing.span_eq_top⟩

Premises used: ConvexCone.IsReproducing.span_eq_top, Iff.intro, ConvexCone.IsReproducing.of_span_eq_top
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
x : M
hs : Convex 𝕜 s
hx : Membership.mem (γ := ConvexCone 𝕜 M) (hull 𝕜 s) x
r₁ : 𝕜
hr₁ : 0 < r₁
y : M
this :
  ∀ (r₂ : 𝕜) (hr₂ : 0 < r₂) (hy : y ∈ r₂ • s),
    Membership.mem (γ := Set M) {y : M | ∃ (r : 𝕜), 0 < r ∧ y ∈ r • s} (r₁ • y)
⊢ Membership.mem (γ := Set M) {y : M | ∃ (r : 𝕜), 0 < r ∧ y ∈ r • s} y →
    Membership.mem (γ := Set M) {y : M | ∃ (r : 𝕜), 0 < r ∧ y ∈ r • s} (r₁ • y)

Tactic:
⟨r₂, hr₂, hy⟩
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
x : M
hs : Convex 𝕜 s
hx : Membership.mem (γ := ConvexCone 𝕜 M) (hull 𝕜 s) x
r₁ : 𝕜
hr₁ : 0 < r₁
y : M
r₂ : 𝕜
hr₂ : 0 < r₂
hy : y ∈ r₂ • s
⊢ Membership.mem (γ := Set M) {y : M | ∃ (r : 𝕜), 0 < r ∧ y ∈ r • s} (r₁ • y)

Tactic:
⟨r₁ * r₂, mul_pos hr₁ hr₂, ?_⟩

Premises used: HMul.hMul, Set.Mem, setOf, mul_pos, And.intro, Exists.intro
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
x : M
hs : Convex 𝕜 s
hx : Membership.mem (γ := ConvexCone 𝕜 M) (hull 𝕜 s) x
r₁ : 𝕜
hr₁ : 0 < r₁
y : M
r₂ : 𝕜
hr₂ : 0 < r₂
hy : y ∈ r₂ • s
refine : r₁ • y ∈ (r₁ * r₂) • s
⊢ Membership.mem (γ := Set M) {y : M | ∃ (r : 𝕜), 0 < r ∧ y ∈ r • s} (r₁ • y)

Tactic:
refine ⟨r₁ * r₂, mul_pos hr₁ hr₂, ?_⟩
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
x : M
hs : Convex 𝕜 s
hx : Membership.mem (γ := ConvexCone 𝕜 M) (hull 𝕜 s) x
r₁ : 𝕜
hr₁ : 0 < r₁
y : M
r₂ : 𝕜
hr₂ : 0 < r₂
hy : y ∈ r₂ • s
rw : r₁ • y ∈ r₁ • r₂ • s
⊢ r₁ • y ∈ (r₁ * r₂) • s

Tactic:
rw [mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
x : M
hs : Convex 𝕜 s
hx : Membership.mem (γ := ConvexCone 𝕜 M) (hull 𝕜 s) x
r₁ : 𝕜
hr₁ : 0 < r₁
y : M
r₂ : 𝕜
hr₂ : 0 < r₂
hy : y ∈ r₂ • s
⊢ r₁ • y ∈ r₁ • r₂ • s

Tactic:
smul_mem_smul_set hy

Premises used: Set.Mem, Set.smul_mem_smul_set
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
x : M
hs : Convex 𝕜 s
hx : Membership.mem (γ := ConvexCone 𝕜 M) (hull 𝕜 s) x
r₁ : 𝕜
hr₁ : 0 < r₁
y : M
r₂ : 𝕜
hr₂ : 0 < r₂
hy : y ∈ r₂ • s
⊢ r₁ • y ∈ r₁ • r₂ • s

Tactic:
exact smul_mem_smul_set hy

Premises used: Set.smul_mem_smul_set
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
x : M
hs : Convex 𝕜 s
hx : Membership.mem (γ := ConvexCone 𝕜 M) (hull 𝕜 s) x
y₁ : M
r₁ : 𝕜
hr₁ : 0 < r₁
hy₁ : y₁ ∈ r₁ • s
y₂ : M
r₂ : 𝕜
hr₂ : 0 < r₂
hy₂ : y₂ ∈ r₂ • s
⊢ Membership.mem (γ := Set M) {y : M | ∃ (r : 𝕜), 0 < r ∧ y ∈ r • s} (y₁ + y₂)

Tactic:
⟨r₁ + r₂, add_pos hr₁ hr₂, ?_⟩

Premises used: Set.Mem, add_pos, setOf, HAdd.hAdd, And.intro, Exists.intro
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
x : M
hs : Convex 𝕜 s
hx : Membership.mem (γ := ConvexCone 𝕜 M) (hull 𝕜 s) x
y₁ : M
r₁ : 𝕜
hr₁ : 0 < r₁
hy₁ : y₁ ∈ r₁ • s
y₂ : M
r₂ : 𝕜
hr₂ : 0 < r₂
hy₂ : y₂ ∈ r₂ • s
refine : y₁ + y₂ ∈ (r₁ + r₂) • s
⊢ Membership.mem (γ := Set M) {y : M | ∃ (r : 𝕜), 0 < r ∧ y ∈ r • s} (y₁ + y₂)

Tactic:
refine ⟨r₁ + r₂, add_pos hr₁ hr₂, ?_⟩
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
x : M
hs : Convex 𝕜 s
hx : Membership.mem (γ := ConvexCone 𝕜 M) (hull 𝕜 s) x
y₁ : M
r₁ : 𝕜
hr₁ : 0 < r₁
hy₁ : y₁ ∈ r₁ • s
y₂ : M
r₂ : 𝕜
hr₂ : 0 < r₂
hy₂ : y₂ ∈ r₂ • s
rw : y₁ + y₂ ∈ r₁ • s + r₂ • s
⊢ y₁ + y₂ ∈ (r₁ + r₂) • s

Tactic:
rw [hs.add_smul hr₁.le hr₂.le]

Premises used: LT.lt.le, Convex.add_smul
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
x : M
hs : Convex 𝕜 s
hx : Membership.mem (γ := ConvexCone 𝕜 M) (hull 𝕜 s) x
y₁ : M
r₁ : 𝕜
hr₁ : 0 < r₁
hy₁ : y₁ ∈ r₁ • s
y₂ : M
r₂ : 𝕜
hr₂ : 0 < r₂
hy₂ : y₂ ∈ r₂ • s
⊢ y₁ + y₂ ∈ r₁ • s + r₂ • s

Tactic:
add_mem_add hy₁ hy₂

Premises used: Set.add_mem_add
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
x : M
hs : Convex 𝕜 s
hx : Membership.mem (γ := ConvexCone 𝕜 M) (hull 𝕜 s) x
y₁ : M
r₁ : 𝕜
hr₁ : 0 < r₁
hy₁ : y₁ ∈ r₁ • s
y₂ : M
r₂ : 𝕜
hr₂ : 0 < r₂
hy₂ : y₂ ∈ r₂ • s
⊢ y₁ + y₂ ∈ r₁ • s + r₂ • s

Tactic:
exact add_mem_add hy₁ hy₂

Premises used: Set.add_mem_add
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
x : M
hs : Convex 𝕜 s
hx : Membership.mem (γ := ConvexCone 𝕜 M) (hull 𝕜 s) x
y : M
hy : y ∈ s
⊢ LT.lt.{u_1} (α := 𝕜) 0 1 ∧ y ∈ HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) 1 s

Tactic:
simpa
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
r : 𝕜
hr : 0 < r
y : M
hy : y ∈ s
⊢ Membership.mem (γ := ConvexCone 𝕜 M) (hull 𝕜 s) ((fun (x : M) ↦ r • x) y)

Tactic:
(hull 𝕜 s).smul_mem hr <| subset_hull hy

Premises used: Set.Mem, ConvexCone.hull, ConvexCone.smul_mem, ConvexCone.subset_hull
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
r : 𝕜
hr : 0 < r
y : M
hy : y ∈ s
⊢ Membership.mem (γ := ConvexCone 𝕜 M) (hull 𝕜 s) ((fun (x : M) ↦ r • x) y)

Tactic:
exact (hull 𝕜 s).smul_mem hr <| subset_hull hy

Premises used: ConvexCone.hull, ConvexCone.smul_mem, ConvexCone.subset_hull
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
h : ∀ (x : M), x ∈ (↑(hull 𝕜 s) : Set M) ↔ Membership.mem (γ := Set M) {x : M | ∃ (r : 𝕜), 0 < r ∧ x ∈ r • s} x
⊢ (↑(hull 𝕜 s) : Set M) = {x : M | ∃ (r : 𝕜), 0 < r ∧ x ∈ r • s}

Tactic:
ext
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
x : M
⊢ x ∈ (↑(hull 𝕜 s) : Set M) ↔ Membership.mem (γ := Set M) {x : M | ∃ (r : 𝕜), 0 < r ∧ x ∈ r • s} x

Tactic:
mem_hull_of_convex hs

Premises used: Set.Mem, setOf, ConvexCone.mem_hull_of_convex
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
x : M
⊢ x ∈ (↑(hull 𝕜 s) : Set M) ↔ Membership.mem (γ := Set M) {x : M | ∃ (r : 𝕜), 0 < r ∧ x ∈ r • s} x

Tactic:
exact mem_hull_of_convex hs

Premises used: ConvexCone.mem_hull_of_convex
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
C : ConvexCone 𝕜 M
s : Set M
hs : Convex 𝕜 s
rw : Disjoint (↑(hull 𝕜 s) : Set M) (↑C : Set M) → Disjoint s (↑C : Set M)
⊢ Disjoint (hull 𝕜 s) C → Disjoint s (↑C : Set M)

Tactic:
rw [← disjoint_coe]

Premises used: ConvexCone.disjoint_coe
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
C : ConvexCone 𝕜 M
s : Set M
hs : Convex 𝕜 s
⊢ Disjoint (↑(hull 𝕜 s) : Set M) (↑C : Set M) → Disjoint s (↑C : Set M)

Tactic:
.mono_left subset_hull

Premises used: ConvexCone.subset_hull, Disjoint.mono_left
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
C : ConvexCone 𝕜 M
s : Set M
hs : Convex 𝕜 s
⊢ Disjoint (↑(hull 𝕜 s) : Set M) (↑C : Set M) → Disjoint s (↑C : Set M)

Tactic:
exact .mono_left subset_hull
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
C : ConvexCone 𝕜 M
s : Set M
hs : Convex 𝕜 s
simp_rw : (∀ ⦃a : M⦄, a ∈ s → a ∉ C) → ∀ ⦃a : M⦄, (∃ (r : 𝕜), 0 < r ∧ a ∈ r • s) → a ∉ C
⊢ Disjoint s (↑C : Set M) → Disjoint (hull 𝕜 s) C

Tactic:
simp_rw [← disjoint_coe, disjoint_left, SetLike.mem_coe, mem_hull_of_convex hs]

Premises used: Set.disjoint_left, ConvexCone.disjoint_coe, SetLike.mem_coe, ConvexCone.mem_hull_of_convex
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
C : ConvexCone 𝕜 M
s : Set M
hs : Convex 𝕜 s
hsC : ∀ ⦃a : M⦄, a ∈ s → a ∉ C
r : 𝕜
hr : 0 < r
y : M
hy : y ∈ s
⊢ (fun (x : M) ↦ r • x) y ∉ C

Tactic:
(C.smul_mem_iff hr).not.mpr (hsC hy)

Premises used: Iff.mpr, Set.Mem, Iff.not, ConvexCone.smul_mem_iff
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
C : ConvexCone 𝕜 M
s : Set M
hs : Convex 𝕜 s
hsC : ∀ ⦃a : M⦄, a ∈ s → a ∉ C
r : 𝕜
hr : 0 < r
y : M
hy : y ∈ s
⊢ (fun (x : M) ↦ r • x) y ∉ C

Tactic:
exact (C.smul_mem_iff hr).not.mpr (hsC hy)

Premises used: Iff.mpr, Iff.not, ConvexCone.smul_mem_iff
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
C : ConvexCone 𝕜 M
s : Set M
hs : Convex 𝕜 s
rw : Disjoint (hull 𝕜 s) C ↔ Disjoint (↑C : Set M) s
rw₁ : Disjoint s (↑C : Set M) ↔ Disjoint (↑C : Set M) s
rw₂ rw₃ : Disjoint (↑C : Set M) s ↔ Disjoint (↑C : Set M) s
⊢ Disjoint C (hull 𝕜 s) ↔ Disjoint (↑C : Set M) s

Tactic:
rw [disjoint_comm, disjoint_hull_left_of_convex hs, disjoint_comm]

Premises used: disjoint_comm, ConvexCone.disjoint_hull_left_of_convex
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : Module R M
C : Submodule R M
⊢ (↑C.toConvexCone : Set M) = (↑C : Set M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : Module R M
C : Submodule R M
x : M
⊢ Membership.mem (γ := ConvexCone R M) C.toConvexCone x ↔ x ∈ C

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : Module R M
C₁ C₂ : Submodule R M
⊢ LE.le (α := ConvexCone R M) C₁.toConvexCone C₂.toConvexCone ↔ C₁ ≤ C₂

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : Module R M
⊢ Eq.{u_4 + 1} (α := ConvexCone R M) (toConvexCone ⊥) 0

Tactic:
rfl

Premises used: Submodule.toConvexCone, rfl
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : Module R M
⊢ Eq.{u_4 + 1} (α := ConvexCone R M) (toConvexCone ⊤) ⊤

Tactic:
rfl

Premises used: Submodule.toConvexCone, Set.univ, setOf, ConvexCone.copy, rfl
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : Module R M
C₁ C₂ : Submodule R M
⊢ Eq (α := ConvexCone R M) (C₁ ⊓ C₂).toConvexCone (C₁.toConvexCone ⊓ C₂.toConvexCone)

Tactic:
rfl

Premises used: Submodule.toConvexCone, ConvexCone.copy, rfl
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : Module R M
C : Submodule R M
⊢ ConvexCone.Pointed C.toConvexCone

Tactic:
C.zero_mem

Premises used: Set.Mem, Submodule.zero_mem, ConvexCone.Pointed
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : PartialOrder M
inst_4 : IsOrderedAddMonoid M
inst_5 : Module R M
inst_6 : PosSMulMono R M
x : M
⊢ Membership.mem (γ := ConvexCone R M) (positive R M) x ↔ 0 ≤ x

Tactic:
.rfl

Premises used: Set.Ici, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : PartialOrder M
inst_4 : IsOrderedAddMonoid M
inst_5 : Module R M
inst_6 : PosSMulMono R M
⊢ (↑(positive R M) : Set M) = Ici 0

Tactic:
rfl

Premises used: Set.Ici, setOf, rfl
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
G : Type u_7
inst_2 : AddCommGroup G
inst_3 : PartialOrder G
inst_4 : IsOrderedAddMonoid G
inst_5 : Module R G
inst_6 : PosSMulMono R G
x : G
hx_nonneg : Membership.mem (γ := ConvexCone R G) (positive R G) x
hx_ne_zero : x ≠ 0
hx_nonpos : Membership.mem (γ := ConvexCone R G) (positive R G) (-x)
⊢ LT.lt.{u_7} (α := G) 0 0

Tactic:
simpa using add_pos_of_nonneg_of_pos hx_nonpos <| hx_nonneg.lt_of_ne' hx_ne_zero

Premises used: add_pos_of_nonneg_of_pos, LE.le.lt_of_ne'
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : PartialOrder M
inst_4 : IsOrderedAddMonoid M
inst_5 : Module R M
inst_6 : PosSMulMono R M
⊢ Pointed (positive R M)

Tactic:
le_refl 0

Premises used: le_refl, Set.Ici, Set.Mem, setOf, ConvexCone.Pointed, OfNat.ofNat