awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
f : M →ₗ[R] N
C : ConvexCone R N
x : M
⊢ x ∈ comap f C ↔ Membership.mem (α := N) C ((f : (a : M) → N) x : N)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
M : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommMonoid M
inst_4 : MulAction 𝕜 M
C : ConvexCone 𝕜 M
c : 𝕜
hc : 0 < c
x : M
⊢ c • x ∈ C ↔ x ∈ C

Tactic:
⟨fun h => inv_smul_smul₀ hc.ne' x ▸ C.smul_mem (inv_pos.2 hc) h, C.smul_mem hc⟩

Premises used: Iff.mpr, inv_smul_smul₀, ConvexCone.smul_mem, Eq.rec, inv_pos, LT.lt.ne', Iff.intro
-- 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 : SMul R M
C : ConvexCone R M
⊢ C.Blunt ↔ ¬C.Pointed

Tactic:
.rfl

Premises used: Iff.rfl, ConvexCone.Blunt, 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 : SMul R M
C : ConvexCone R M
⊢ C.Pointed ↔ ¬C.Blunt

Tactic:
simp [Blunt, Pointed]

Premises used: ConvexCone.Blunt, 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 : SMul R M
C₁ C₂ : ConvexCone R M
h : C₁ ≤ C₂
⊢ C₁.Pointed → C₂.Pointed

Tactic:
@h _

Premises used: 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 : SMul R M
C₁ C₂ : ConvexCone R M
h : C₂ ≤ C₁
⊢ C₁.Blunt → C₂.Blunt

Tactic:
(· ∘ @h 0)

Premises used: Function.comp, ConvexCone.Blunt, Not
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
G : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup G
inst_3 : SMul R G
C : ConvexCone R G
⊢ C.Salient ↔ ¬C.Flat

Tactic:
simp [Salient, Flat]

Premises used: ConvexCone.Salient, ConvexCone.Flat
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
G : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup G
inst_3 : SMul R G
C₁ C₂ : ConvexCone R G
h : C₂ ≤ C₁
⊢ C₁.Salient → C₂.Salient

Tactic:
fun hS x hxT hx hnT => hS x (h hxT) hx (h hnT)

Premises used: ConvexCone.Salient, Not
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
G : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup G
inst_3 : SMul R G
C : ConvexCone R G
hC : C.Flat
obtain : ∀ (x : G) (hx : x ∈ C), x ≠ 0 → ∀ (hxneg : -x ∈ C), C.Pointed
⊢ C.Pointed

Tactic:
obtain ⟨x, hx, _, hxneg⟩ := hC
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
G : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup G
inst_3 : SMul R G
C : ConvexCone R G
x : G
hx : x ∈ C
left : x ≠ 0
hxneg : -x ∈ C
rw : x + -x ∈ C
⊢ C.Pointed

Tactic:
rw [Pointed, ← add_neg_cancel x]

Premises used: add_neg_cancel, ConvexCone.Pointed
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
G : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup G
inst_3 : SMul R G
C : ConvexCone R G
x : G
hx : x ∈ C
left : x ≠ 0
hxneg : -x ∈ C
⊢ x + -x ∈ C

Tactic:
add_mem hx hxneg

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
G : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup G
inst_3 : SMul R G
C : ConvexCone R G
x : G
hx : x ∈ C
left : x ≠ 0
hxneg : -x ∈ C
⊢ x + -x ∈ C

Tactic:
exact add_mem hx hxneg

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
G : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup G
inst_3 : SMul R G
C : ConvexCone R G
rw : ¬C.Pointed → ¬C.Flat
⊢ C.Blunt → C.Salient

Tactic:
rw [salient_iff_not_flat, blunt_iff_not_pointed]

Premises used: ConvexCone.salient_iff_not_flat, ConvexCone.blunt_iff_not_pointed
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
G : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup G
inst_3 : SMul R G
C : ConvexCone R G
⊢ ¬C.Pointed → ¬C.Flat

Tactic:
mt Flat.pointed

Premises used: mt, ConvexCone.Flat.pointed
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
G : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup G
inst_3 : SMul R G
C : ConvexCone R G
⊢ ¬C.Pointed → ¬C.Flat

Tactic:
exact mt Flat.pointed

Premises used: mt, ConvexCone.Flat.pointed
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup G
inst_3 : SMul R G
C_1 C₁ C₂ C : ConvexCone R G
h₁ : C.Pointed
x : G
rw : 0 ∈ C
⊢ x - x ∈ C

Tactic:
rw [sub_self x]

Premises used: sub_self
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup G
inst_3 : SMul R G
C_1 C₁ C₂ C : ConvexCone R G
h₁ : C.Pointed
x : G
⊢ 0 ∈ C

Tactic:
h₁

Premises used: Set.Mem, ConvexCone.Pointed
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup G
inst_3 : SMul R G
C_1 C₁ C₂ C : ConvexCone R G
h₁ : C.Pointed
x : G
⊢ 0 ∈ C

Tactic:
exact h₁
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup G
inst_3 : SMul R G
C_1 C₁ C₂ C : ConvexCone R G
h₁ : C.Pointed
x y z : G
xy : y - x ∈ C
zy : z - y ∈ C
⊢ z - x ∈ C

Tactic:
simpa using add_mem zy xy

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup G
inst_3 : SMul R G
C_1 C₁ C₂ C : ConvexCone R G
h₁ : C.Pointed
h₂ : C.Salient
a b : G
ab : a ≤ b
ba : b ≤ a
by_contra : ∀ (h : ¬a = b), False
⊢ a = b

Tactic:
by_contra h
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup G
inst_3 : SMul R G
C_1 C₁ C₂ C : ConvexCone R G
h₁ : C.Pointed
h₂ : C.Salient
a b : G
ab : a ≤ b
ba : b ≤ a
h : ¬a = b
⊢ b - a ≠ 0

Tactic:
have h' : b - a ≠ 0 := fun h'' => h (eq_of_sub_eq_zero h'').symm
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup G
inst_3 : SMul R G
C_1 C₁ C₂ C : ConvexCone R G
h₁ : C.Pointed
h₂ : C.Salient
a b : G
ab : a ≤ b
ba : b ≤ a
h : ¬a = b
h' : b - a ≠ 0
⊢ -(b - a) ∉ C

Tactic:
have H := h₂ (b - a) ab h'
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup G
inst_3 : SMul R G
C_1 C₁ C₂ C : ConvexCone R G
h₁ : C.Pointed
h₂ : C.Salient
a b : G
ab : a ≤ b
ba : b ≤ a
h : ¬a = b
h' : b - a ≠ 0
H : -(b - a) ∉ C
⊢ a - b ∉ C

Tactic:
rw [neg_sub b a] at H

Premises used: neg_sub
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup G
inst_3 : SMul R G
C_1 C₁ C₂ C : ConvexCone R G
h₁ : C.Pointed
h₂ : C.Salient
a b : G
ab : a ≤ b
ba : b ≤ a
h : ¬a = b
h' : b - a ≠ 0
H : a - b ∉ C
⊢ False

Tactic:
H ba
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup G
inst_3 : SMul R G
C_1 C₁ C₂ C : ConvexCone R G
h₁ : C.Pointed
h₂ : C.Salient
a b : G
ab : a ≤ b
ba : b ≤ a
h : ¬a = b
h' : b - a ≠ 0
H : a - b ∉ C
⊢ False

Tactic:
exact H ba
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
G : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup G
inst_3 : SMul R G
C : ConvexCone R G
h₁ : C.Pointed
h₂ : C.Salient
a b : G
hab : a ≤ b
c : G
rwa rwa₁ rwa₂ rwa₃ : b - a ∈ C
⊢ b + c - (a + c) ∈ C

Tactic:
rwa [add_sub_add_right_eq_sub]

Premises used: add_sub_add_right_eq_sub
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : Module R M
C₁ C₂ : ConvexCone R M
x : M
x_1 : R
h : 0 < x_1
⊢ ∀ ⦃x : M⦄, Membership.mem (γ := Set M) 0 x → Membership.mem (γ := Set M) 0 (x_1 • x)

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : Module R M
C₁ C₂ : ConvexCone R M
x x_1 : M
⊢ Membership.mem (γ := Set M) 0 x_1 →
    ∀ ⦃y : M⦄, Membership.mem (γ := Set M) 0 y → Membership.mem (γ := Set M) 0 (x_1 + y)

Tactic:
simp
-- 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
x : M
⊢ Membership.mem (γ := ConvexCone R M) 0 x ↔ x = 0

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.singleton
-- 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
⊢ (↑0 : Set M) = 0

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
rw : Membership.mem (γ := ConvexCone R M) 0 0
rw₁ rw₂ : Eq.{u_4 + 1} (α := M) 0 0
⊢ Pointed.{u_2, u_4} (R := R) (M := M) 0

Tactic:
rw [Pointed, mem_zero]

Premises used: ConvexCone.mem_zero, ConvexCone.Pointed
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : Module R M
C₁_1 C₂_1 : ConvexCone R M
x_1 : M
C₁ C₂ : ConvexCone R M
c : R
hc : 0 < c
x : M
hx : x ∈ (↑C₁ : Set M)
y : M
hy : y ∈ (↑C₂ : Set M)
rw : c • x + c • y ∈ (↑C₁ : Set M) + (↑C₂ : Set M)
⊢ HSMul.hSMul (β := M) c ((fun (x1 x2 : M) ↦ x1 + x2) x y) ∈ (↑C₁ : Set M) + (↑C₂ : Set M)

Tactic:
rw [smul_add]

Premises used: smul_add
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : Module R M
C₁_1 C₂_1 : ConvexCone R M
x_1 : M
C₁ C₂ : ConvexCone R M
c : R
hc : 0 < c
x : M
hx : x ∈ (↑C₁ : Set M)
y : M
hy : y ∈ (↑C₂ : Set M)
w : M
left : c • x ∈ (↑C₁ : Set M)
w₁ : M
left₁ : c • y ∈ (↑C₂ : Set M)
right : (fun (x1 x2 : M) ↦ x1 + x2) (c • x) (c • y) = c • x + c • y
⊢ c • x + c • y ∈ (↑C₁ : Set M) + (↑C₂ : Set M)

Tactic:
use c • x, C₁.smul_mem hc hx, c • y, C₂.smul_mem hc hy

Premises used: ConvexCone.smul_mem
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : Module R M
C₁_1 C₂_1 : ConvexCone R M
x : M
C₁ C₂ : ConvexCone R M
x₁ : M
hx₁ : x₁ ∈ (↑C₁ : Set M)
x₂ : M
hx₂ : x₂ ∈ (↑C₂ : Set M)
y₁ : M
hy₁ : y₁ ∈ (↑C₁ : Set M)
y₂ : M
hy₂ : y₂ ∈ (↑C₂ : Set M)
⊢ HAdd.hAdd (α := M) ((fun (x1 x2 : M) ↦ x1 + x2) x₁ x₂) ((fun (x1 x2 : M) ↦ x1 + x2) y₁ y₂) ∈
    (↑C₁ : Set M) + (↑C₂ : Set M)

Tactic:
⟨x₁ + y₁, add_mem hx₁ hy₁, x₂ + y₂, add_mem hx₂ hy₂, add_add_add_comm ..⟩

Premises used: Set.Mem, setOf, HAdd.hAdd, Set.image2, And.intro, Exists.intro, AddMemClass.add_mem, add_add_add_comm
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : Module R M
C₁_1 C₂_1 : ConvexCone R M
x : M
C₁ C₂ : ConvexCone R M
x₁ : M
hx₁ : x₁ ∈ (↑C₁ : Set M)
x₂ : M
hx₂ : x₂ ∈ (↑C₂ : Set M)
y₁ : M
hy₁ : y₁ ∈ (↑C₁ : Set M)
y₂ : M
hy₂ : y₂ ∈ (↑C₂ : Set M)
⊢ HAdd.hAdd (α := M) ((fun (x1 x2 : M) ↦ x1 + x2) x₁ x₂) ((fun (x1 x2 : M) ↦ x1 + x2) y₁ y₂) ∈
    (↑C₁ : Set M) + (↑C₂ : Set M)

Tactic:
exact ⟨x₁ + y₁, add_mem hx₁ hy₁, x₂ + y₂, add_mem hx₂ hy₂, add_add_add_comm ..⟩
-- 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₂ : ConvexCone R M
⊢ (↑(C₁ + C₂) : Set M) = (↑C₁ : 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₁ C₂ : ConvexCone R M
x : M
⊢ x ∈ C₁ + C₂ ↔ ∃ y ∈ C₁, ∃ z ∈ C₂, y + z = x

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.image2
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : Module R M
C₁ C₂ : ConvexCone R M
x : M
x_1 : ConvexCone R M
h : ∀ (x : M), x ∈ 0 + x_1 ↔ x ∈ x_1
⊢ 0 + x_1 = x_1

Tactic:
ext
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : Module R M
C₁ C₂ : ConvexCone R M
x : M
x_1 : ConvexCone R M
x_2 : M
⊢ x_2 ∈ 0 + x_1 ↔ x_2 ∈ x_1

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : Module R M
C₁ C₂ : ConvexCone R M
x : M
x_1 : ConvexCone R M
h : ∀ (x : M), x ∈ x_1 + 0 ↔ x ∈ x_1
⊢ x_1 + 0 = x_1

Tactic:
ext
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommMonoid M
inst_3 : Module R M
C₁ C₂ : ConvexCone R M
x : M
x_1 : ConvexCone R M
x_2 : M
⊢ x_2 ∈ x_1 + 0 ↔ x_2 ∈ x_1

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup M
inst_3 : Module R M
C : ConvexCone R M
h : univ ⊆ (↑C : Set M) - (↑C : Set M)
⊢ C.IsReproducing

Tactic:
Set.eq_univ_iff_forall.mpr fun _ ↦ h (Set.mem_univ _)

Premises used: Iff.mpr, Set.eq_univ_iff_forall, ConvexCone.IsReproducing, Set.mem_univ
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup M
inst_3 : Module R M
C : ConvexCone R M
hC : C.IsReproducing
⊢ (↑C : Set M) - (↑C : Set M) = univ

Tactic:
hC

Premises used: ConvexCone.IsReproducing
-- 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 : ConvexCone R M
h : LE.le (α := Submodule R M) ⊤ (Submodule.span R (↑C : Set M))
⊢ C.IsGenerating

Tactic:
eq_top_iff.mpr h

Premises used: Iff.mpr, eq_top_iff, ConvexCone.IsGenerating
-- 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 : ConvexCone R M
hC : C.IsGenerating
⊢ Eq (α := Submodule R M) (Submodule.span R (↑C : Set M)) ⊤

Tactic:
hC

Premises used: ConvexCone.IsGenerating
-- 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 : ConvexCone R M
hC : C.IsGenerating
⊢ LE.le (α := Submodule R M) ⊤ (Submodule.span R (↑C : Set M))

Tactic:
hC.span_eq_top.ge

Premises used: Eq.ge, ConvexCone.IsGenerating.span_eq_top
-- 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
⊢ IsGenerating.{u_2, u_4} (R := R) (M := M) ⊤

Tactic:
simp
-- 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
⊢ IsGenerating.{u_2, u_4} (R := R) (M := M) ⊥ ↔ Subsingleton M

Tactic:
simpa only [IsGenerating, coe_bot, Submodule.span_empty, ← Submodule.subsingleton_iff R] using
    subsingleton_iff_bot_eq_top

Premises used: Submodule.subsingleton_iff, ConvexCone.IsGenerating, Submodule.span_empty, subsingleton_iff_bot_eq_top, ConvexCone.coe_bot
-- 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
inst_4 : Subsingleton M
⊢ IsGenerating.{u_2, u_4} (R := R) (M := M) ⊥

Tactic:
isGenerating_bot_iff.mpr inferInstance

Premises used: Iff.mpr, inferInstance, ConvexCone.isGenerating_bot_iff
-- 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₂ : ConvexCone R M
h : C₁ ≤ C₂
hgen : C₁.IsGenerating
rw :
  ∀ (hgen : LE.le (α := Submodule R M) ⊤ (Submodule.span R (↑C₁ : Set M))),
    LE.le (α := Submodule R M) ⊤ (Submodule.span R (↑C₂ : Set M))
⊢ C₂.IsGenerating

Tactic:
rw [IsGenerating, ← top_le_iff] at hgen ⊢

Premises used: ConvexCone.IsGenerating, top_le_iff
-- 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₂ : ConvexCone R M
h : C₁ ≤ C₂
hgen : LE.le (α := Submodule R M) ⊤ (Submodule.span R (↑C₁ : Set M))
⊢ LE.le (α := Submodule R M) ⊤ (Submodule.span R (↑C₂ : Set M))

Tactic:
hgen.trans (Submodule.span_mono h)

Premises used: Submodule.span_mono, LE.le.trans
-- 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₂ : ConvexCone R M
h : C₁ ≤ C₂
hgen : LE.le (α := Submodule R M) ⊤ (Submodule.span R (↑C₁ : Set M))
⊢ LE.le (α := Submodule R M) ⊤ (Submodule.span R (↑C₂ : Set M))

Tactic:
exact hgen.trans (Submodule.span_mono h)

Premises used: Submodule.span_mono, LE.le.trans
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup M
inst_3 : Module R M
C : ConvexCone R M
h : C.IsReproducing
rw : LE.le (α := Submodule R M) ⊤ (Submodule.span R (↑C : Set M))
⊢ Eq (α := Submodule R M) (Submodule.span R (↑C : Set M)) ⊤

Tactic:
rw [eq_top_iff]

Premises used: eq_top_iff
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup M
inst_3 : Module R M
C : ConvexCone R M
h : C.IsReproducing
x : M
rw :
  ∀ (h : ∀ (x : M), x ∈ (↑C : Set M) - (↑C : Set M)) ⦃x : M⦄,
    Membership.mem (γ := Submodule R M) (Submodule.span R (↑C : Set M)) x
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R (↑C : Set M)) x

Tactic:
rw [IsReproducing, Set.eq_univ_iff_forall] at h

Premises used: Set.eq_univ_iff_forall, ConvexCone.IsReproducing
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup M
inst_3 : Module R M
C : ConvexCone R M
h : ∀ (x : M), x ∈ (↑C : Set M) - (↑C : Set M)
x : M
obtain :
  ∀ (y : M) (hy : y ∈ (↑C : Set M)) (z : M) (hz : z ∈ (↑C : Set M)),
    Membership.mem (γ := Submodule R M) (Submodule.span R (↑C : Set M)) (y - z)
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R (↑C : Set M)) x

Tactic:
obtain ⟨y, hy, z, hz, rfl⟩ := Set.mem_sub.mp (h x)

Premises used: Set.mem_sub, Iff.mp, rfl
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup M
inst_3 : Module R M
C : ConvexCone R M
h : ∀ (x : M), x ∈ (↑C : Set M) - (↑C : Set M)
y : M
hy : y ∈ (↑C : Set M)
z : M
hz : z ∈ (↑C : Set M)
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R (↑C : Set M)) (y - z)

Tactic:
sub_mem (Submodule.subset_span hy) (Submodule.subset_span hz)

Premises used: sub_mem, Submodule.subset_span
-- Module: Mathlib.Geometry.Convex.Cone.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup M
inst_3 : Module R M
C : ConvexCone R M
h : ∀ (x : M), x ∈ (↑C : Set M) - (↑C : Set M)
y : M
hy : y ∈ (↑C : Set M)
z : M
hz : z ∈ (↑C : Set M)
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R (↑C : Set M)) (y - z)

Tactic:
exact sub_mem (Submodule.subset_span hy) (Submodule.subset_span hz)

Premises used: sub_mem, Submodule.subset_span
-- 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)) ⊤
rw : ∀ (x : M), x ∈ (↑C : Set M) - (↑C : Set M)
⊢ C.IsReproducing

Tactic:
rw [IsReproducing, Set.eq_univ_iff_forall]

Premises used: Set.eq_univ_iff_forall, ConvexCone.IsReproducing
-- 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
h' : (↑C : Set M) = ∅
⊢ False

Tactic:
simp [h'] at h
-- 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
⊢ (↑C : Set M).Nonempty

Tactic:
have hne : (C : Set M).Nonempty := Set.nonempty_iff_ne_empty.2 fun h' => by simp [h'] at h
-- 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)
y₂ : M
hy₂ : y₂ ∈ (↑C : Set M)
z₂ : M
hz₂ : z₂ ∈ (↑C : Set M)
⊢ HAdd.hAdd (α := M) ((fun (x1 x2 : M) ↦ x1 - x2) y₁ z₁) ((fun (x1 x2 : M) ↦ x1 - x2) y₂ z₂) ∈
    (↑C : Set M) - (↑C : Set M)

Tactic:
⟨y₁ + y₂, C.add_mem hy₁ hy₂, z₁ + z₂, C.add_mem hz₁ hz₂, add_sub_add_comm ..⟩

Premises used: Set.Mem, setOf, HAdd.hAdd, Set.image2, And.intro, Exists.intro, add_sub_add_comm, ConvexCone.add_mem
-- 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)
y₂ : M
hy₂ : y₂ ∈ (↑C : Set M)
z₂ : M
hz₂ : z₂ ∈ (↑C : Set M)
⊢ HAdd.hAdd (α := M) ((fun (x1 x2 : M) ↦ x1 - x2) y₁ z₁) ((fun (x1 x2 : M) ↦ x1 - x2) y₂ z₂) ∈
    (↑C : Set M) - (↑C : Set M)

Tactic:
exact ⟨y₁ + y₂, C.add_mem hy₁ hy₂, z₁ + z₂, C.add_mem hz₁ hz₂, add_sub_add_comm ..⟩