awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : PartialOrder M
inst_4 : IsOrderedAddMonoid M
inst_5 : Module R M
inst_6 : PosSMulStrictMono R M
x : M
⊢ Membership.mem (γ := ConvexCone R M) (strictlyPositive R M) x ↔ 0 < x

Tactic:
.rfl

Premises used: Set.Ioi, 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 : AddCommGroup M
inst_3 : PartialOrder M
inst_4 : IsOrderedAddMonoid M
inst_5 : Module R M
inst_6 : PosSMulStrictMono R M
⊢ (↑(strictlyPositive R M) : Set M) = Ioi 0

Tactic:
rfl

Premises used: Set.Ioi, setOf, 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 : AddCommGroup M
inst_3 : PartialOrder M
inst_4 : IsOrderedAddMonoid M
inst_5 : Module R M
inst_6 : PosSMulStrictMono R M
⊢ LE.le (α := ConvexCone R M) (strictlyPositive R M) (positive R M)

Tactic:
fun _ => le_of_lt

Premises used: Set.Ioi, Set.Ici, Set.Mem, setOf, le_of_lt
-- 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 : PartialOrder M
inst_4 : IsOrderedAddMonoid M
inst_5 : Module R M
inst_6 : PosSMulStrictMono R M
⊢ Salient (strictlyPositive R M)

Tactic:
salient_positive.anti strictlyPositive_le_positive

Premises used: ConvexCone.Salient.anti, ConvexCone.strictlyPositive_le_positive, ConvexCone.salient_positive
-- 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 : PartialOrder M
inst_4 : IsOrderedAddMonoid M
inst_5 : Module R M
inst_6 : PosSMulStrictMono R M
⊢ Blunt (strictlyPositive R M)

Tactic:
lt_irrefl 0

Premises used: Set.Ioi, lt_irrefl, Set.Mem, setOf, ConvexCone.Blunt, OfNat.ofNat
-- 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 : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
smul_mem' :
  ∀ ⦃c : 𝕜⦄,
    0 < c →
      ∀ ⦃x : M⦄,
        Membership.mem (γ := Set M) (⋃ (c : 𝕜), ⋃ (_ : 0 < c), c • s) x →
          Membership.mem (γ := Set M) (⋃ (c : 𝕜), ⋃ (_ : 0 < c), c • s) (c • x)
add_mem' :
  ∀ ⦃x : M⦄,
    Membership.mem (γ := Set M) (⋃ (c : 𝕜), ⋃ (_ : 0 < c), c • s) x →
      ∀ ⦃y : M⦄,
        Membership.mem (γ := Set M) (⋃ (c : 𝕜), ⋃ (_ : 0 < c), c • s) y →
          Membership.mem (γ := Set M) (⋃ (c : 𝕜), ⋃ (_ : 0 < c), c • s) (x + y)
⊢ ConvexCone 𝕜 M

Tactic:
apply ConvexCone.mk (⋃ (c : 𝕜) (_ : 0 < c), c • s)

Premises used: ConvexCone.mk, HSMul.hSMul, Set.iUnion
-- 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 : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
smul_mem' :
  ∀ ⦃c : 𝕜⦄,
    0 < c → ∀ ⦃x : M⦄, (∃ (i : 𝕜) (_ : 0 < i), ∃ y ∈ s, i • y = x) → ∃ (i : 𝕜) (_ : 0 < i), ∃ y ∈ s, i • y = c • x
⊢ ∀ ⦃c : 𝕜⦄,
    0 < c →
      ∀ ⦃x : M⦄,
        Membership.mem (γ := Set M) (⋃ (c : 𝕜), ⋃ (_ : 0 < c), c • s) x →
          Membership.mem (γ := Set M) (⋃ (c : 𝕜), ⋃ (_ : 0 < c), c • s) (c • x)

Tactic:
simp only [mem_iUnion, mem_smul_set]

Premises used: Set.mem_iUnion, Set.mem_smul_set
-- 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 : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
add_mem' :
  ∀ ⦃x : M⦄,
    (∃ (i : 𝕜) (_ : 0 < i), ∃ y ∈ s, i • y = x) →
      ∀ ⦃y : M⦄, (∃ (i : 𝕜) (_ : 0 < i), ∃ y_1 ∈ s, i • y_1 = y) → ∃ (i : 𝕜) (_ : 0 < i), ∃ y_1 ∈ s, i • y_1 = x + y
⊢ ∀ ⦃x : M⦄,
    Membership.mem (γ := Set M) (⋃ (c : 𝕜), ⋃ (_ : 0 < c), c • s) x →
      ∀ ⦃y : M⦄,
        Membership.mem (γ := Set M) (⋃ (c : 𝕜), ⋃ (_ : 0 < c), c • s) y →
          Membership.mem (γ := Set M) (⋃ (c : 𝕜), ⋃ (_ : 0 < c), c • s) (x + y)

Tactic:
simp only [mem_iUnion, mem_smul_set]

Premises used: Set.mem_iUnion, Set.mem_smul_set
-- 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 : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
c : 𝕜
c_pos : 0 < c
c' : 𝕜
c'_pos : 0 < c'
x : M
hx : x ∈ s
⊢ ∃ (i : 𝕜) (_ : 0 < i), ∃ y ∈ s, i • y = c • c' • x

Tactic:
⟨c * c', mul_pos c_pos c'_pos, x, hx, (smul_smul _ _ _).symm⟩

Premises used: HMul.hMul, smul_smul, mul_pos, And.intro, Exists.intro, Eq.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 : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
c : 𝕜
c_pos : 0 < c
c' : 𝕜
c'_pos : 0 < c'
x : M
hx : x ∈ s
⊢ ∃ (i : 𝕜) (_ : 0 < i), ∃ y ∈ s, i • y = c • c' • x

Tactic:
exact ⟨c * c', mul_pos c_pos c'_pos, x, hx, (smul_smul _ _ _).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 : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
cx : 𝕜
cx_pos : 0 < cx
x : M
hx : x ∈ s
cy : 𝕜
cy_pos : 0 < cy
y : M
hy : y ∈ s
⊢ 0 < cx + cy

Tactic:
have : 0 < cx + cy := add_pos cx_pos cy_pos
-- 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 : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
cx : 𝕜
cx_pos : 0 < cx
x : M
hx : x ∈ s
cy : 𝕜
cy_pos : 0 < cy
y : M
hy : y ∈ s
this : 0 < cx + cy
⊢ ∃ (i : 𝕜) (_ : 0 < i), ∃ y_1 ∈ s, i • y_1 = cx • x + cy • y

Tactic:
⟨_, this, _, convex_iff_div.1 hs hx hy cx_pos.le cy_pos.le this, ?_⟩

Premises used: LT.lt.le, And.intro, convex_iff_div, Exists.intro, Iff.mp
-- 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 : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
cx : 𝕜
cx_pos : 0 < cx
x : M
hx : x ∈ s
cy : 𝕜
cy_pos : 0 < cy
y : M
hy : y ∈ s
this : 0 < cx + cy
add_mem' : (cx + cy) • ((cx / (cx + cy)) • x + (cy / (cx + cy)) • y) = cx • x + cy • y
⊢ ∃ (i : 𝕜) (_ : 0 < i), ∃ y_1 ∈ s, i • y_1 = cx • x + cy • y

Tactic:
refine ⟨_, this, _, convex_iff_div.1 hs hx hy cx_pos.le cy_pos.le this, ?_⟩
-- 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 : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup M
inst_4 : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
cx : 𝕜
cx_pos : 0 < cx
x : M
hx : x ∈ s
cy : 𝕜
cy_pos : 0 < cy
y : M
hy : y ∈ s
this : 0 < cx + cy
⊢ (cx + cy) • ((cx / (cx + cy)) • x + (cy / (cx + cy)) • y) = cx • x + cy • y

Tactic:
simp only [smul_add, smul_smul, mul_div_assoc', mul_div_cancel_left₀ _ this.ne']

Premises used: smul_smul, mul_div_assoc', mul_div_cancel_left₀, LT.lt.ne', smul_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
hs : Convex 𝕜 s
x : M
⊢ x ∈ toCone s hs ↔ ∃ (c : 𝕜), 0 < c ∧ ∃ y ∈ s, c • y = x

Tactic:
simp only [toCone, ConvexCone.mem_mk, mem_iUnion, mem_smul_set, eq_comm, exists_prop]

Premises used: Set.mem_iUnion, Set.mem_smul_set, exists_prop, eq_comm, ConvexCone.mem_mk, Convex.toCone
-- 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 ∈ toCone s hs ↔ ∃ (c : 𝕜), 0 < c ∧ c • x ∈ s

Tactic:
hs.mem_toCone.trans ⟨?_, ?_⟩

Premises used: Convex.mem_toCone, Iff.intro, Iff.trans
-- 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
refine_1 : (∃ (c : 𝕜), 0 < c ∧ ∃ y ∈ s, c • y = x) → ∃ (c : 𝕜), 0 < c ∧ c • x ∈ s
refine_2 : (∃ (c : 𝕜), 0 < c ∧ c • x ∈ s) → ∃ (c : 𝕜), 0 < c ∧ ∃ y ∈ s, c • y = x
⊢ x ∈ toCone s hs ↔ ∃ (c : 𝕜), 0 < c ∧ c • x ∈ s

Tactic:
refine hs.mem_toCone.trans ⟨?_, ?_⟩

Premises used: Convex.mem_toCone, Iff.intro, Iff.trans
-- 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
c : 𝕜
hc : 0 < c
y : M
hy : y ∈ s
rwa : (c⁻¹ * c) • y ∈ s
rwa₁ : HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) 1 y ∈ s
rwa₂ rwa₃ rwa₄ rwa₅ : y ∈ s
⊢ c⁻¹ • c • y ∈ s

Tactic:
rwa [smul_smul, inv_mul_cancel₀ hc.ne', one_smul]

Premises used: smul_smul, one_smul, LT.lt.ne', inv_mul_cancel₀
-- 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
c : 𝕜
hc : 0 < c
y : M
hy : y ∈ s
⊢ ∃ (c_1 : 𝕜), 0 < c_1 ∧ c_1 • c • y ∈ s

Tactic:
exact ⟨c⁻¹, inv_pos.2 hc, by rwa [smul_smul, inv_mul_cancel₀ hc.ne', one_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
hs : Convex 𝕜 s
x : M
c : 𝕜
hc : 0 < c
hcx : c • x ∈ s
rw : (c⁻¹ * c) • x = x
rw₁ : HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) 1 x = x
rw₂ rw₃ : x = x
⊢ c⁻¹ • c • x = x

Tactic:
rw [smul_smul, inv_mul_cancel₀ hc.ne', one_smul]

Premises used: smul_smul, one_smul, LT.lt.ne', inv_mul_cancel₀
-- 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
c : 𝕜
hc : 0 < c
hcx : c • x ∈ s
⊢ ∃ (c : 𝕜), 0 < c ∧ ∃ y ∈ s, c • y = x

Tactic:
exact ⟨c⁻¹, inv_pos.2 hc, _, hcx, by rw [smul_smul, inv_mul_cancel₀ hc.ne', one_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
hs : Convex 𝕜 s
x : M
hx rwa rwa₁ rwa₂ rwa₃ : x ∈ s
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) 1 x ∈ s

Tactic:
rwa [one_smul]

Premises used: one_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
hs : Convex 𝕜 s
⊢ IsLeast {t : ConvexCone 𝕜 M | s ⊆ (↑t : Set M)} (toCone s hs)

Tactic:
⟨hs.subset_toCone, fun t ht x hx => ?_⟩

Premises used: IsLeast, And.intro, Convex.subset_toCone
-- 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
refine :
  ∀ (t : ConvexCone 𝕜 M) (ht : Membership.mem (γ := Set (ConvexCone 𝕜 M)) {t : ConvexCone 𝕜 M | s ⊆ (↑t : Set M)} t)
    (x : M) (hx : x ∈ toCone s hs), x ∈ t
⊢ IsLeast {t : ConvexCone 𝕜 M | s ⊆ (↑t : Set M)} (toCone s hs)

Tactic:
refine ⟨hs.subset_toCone, fun t ht x hx => ?_⟩
-- 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
t : ConvexCone 𝕜 M
ht : Membership.mem (γ := Set (ConvexCone 𝕜 M)) {t : ConvexCone 𝕜 M | s ⊆ (↑t : Set M)} t
x : M
hx : x ∈ toCone s hs
rcases : ∀ (c : 𝕜) (hc : 0 < c) (y : M) (hy : y ∈ s) (hx : c • y ∈ toCone s hs), c • y ∈ t
⊢ x ∈ t

Tactic:
rcases hs.mem_toCone.1 hx with ⟨c, hc, y, hy, rfl⟩

Premises used: Convex.mem_toCone, Iff.mp, rfl
-- 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
t : ConvexCone 𝕜 M
ht : Membership.mem (γ := Set (ConvexCone 𝕜 M)) {t : ConvexCone 𝕜 M | s ⊆ (↑t : Set M)} t
c : 𝕜
hc : 0 < c
y : M
hy : y ∈ s
hx : c • y ∈ toCone s hs
⊢ c • y ∈ t

Tactic:
t.smul_mem hc (ht hy)

Premises used: ConvexCone.smul_mem
-- 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
t : ConvexCone 𝕜 M
ht : Membership.mem (γ := Set (ConvexCone 𝕜 M)) {t : ConvexCone 𝕜 M | s ⊆ (↑t : Set M)} t
c : 𝕜
hc : 0 < c
y : M
hy : y ∈ s
hx : c • y ∈ toCone s hs
⊢ c • y ∈ t

Tactic:
exact t.smul_mem hc (ht hy)

Premises used: ConvexCone.smul_mem
-- 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
⊢ toCone s hs = sInf {t : ConvexCone 𝕜 M | s ⊆ (↑t : Set M)}

Tactic:
hs.toCone_isLeast.isGLB.sInf_eq.symm

Premises used: IsGLB.sInf_eq, IsLeast.isGLB, Convex.toCone_isLeast, Eq.symm
-- 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
⊢ IsLeast (α := ConvexCone 𝕜 M) {t : ConvexCone 𝕜 M | (convexHull 𝕜 : (a : Set M) → Set M) s ⊆ (↑t : Set M)}
    (Convex.toCone ((convexHull 𝕜 : (a : Set M) → Set M) s) ⋯)

Tactic:
(convex_convexHull 𝕜 s).toCone_isLeast

Premises used: convex_convexHull, Convex.toCone_isLeast
-- 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
h :
  Eq.{u_4 + 1} (α := Set (ConvexCone 𝕜 M)) {t : ConvexCone 𝕜 M | s ⊆ (↑t : Set M)}
    {t : ConvexCone 𝕜 M | (convexHull 𝕜 : (a : Set M) → Set M) s ⊆ (↑t : Set M)}
⊢ IsLeast (α := ConvexCone 𝕜 M) {t : ConvexCone 𝕜 M | s ⊆ (↑t : Set M)}
    (Convex.toCone ((convexHull 𝕜 : (a : Set M) → Set M) s) ⋯)

Tactic:
convert! (convex_convexHull 𝕜 s).toCone_isLeast using 1

Premises used: convex_convexHull, Convex.toCone_isLeast
-- 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
h :
  ∀ (t : ConvexCone 𝕜 M),
    Membership.mem (γ := Set (ConvexCone 𝕜 M)) {t : ConvexCone 𝕜 M | s ⊆ (↑t : Set M)} t ↔
      Membership.mem (γ := Set (ConvexCone 𝕜 M))
        {t : ConvexCone 𝕜 M | (convexHull 𝕜 : (a : Set M) → Set M) s ⊆ (↑t : Set M)} t
⊢ Eq.{u_4 + 1} (α := Set (ConvexCone 𝕜 M)) {t : ConvexCone 𝕜 M | s ⊆ (↑t : Set M)}
    {t : ConvexCone 𝕜 M | (convexHull 𝕜 : (a : Set M) → Set M) s ⊆ (↑t : Set M)}

Tactic:
ext t
-- 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
t : ConvexCone 𝕜 M
⊢ Membership.mem (γ := Set (ConvexCone 𝕜 M)) {t : ConvexCone 𝕜 M | s ⊆ (↑t : Set M)} t ↔
    Membership.mem (γ := Set (ConvexCone 𝕜 M))
      {t : ConvexCone 𝕜 M | (convexHull 𝕜 : (a : Set M) → Set M) s ⊆ (↑t : Set M)} t

Tactic:
⟨fun h => convexHull_min h t.convex, (subset_convexHull 𝕜 s).trans⟩

Premises used: ConvexCone.convex, subset_convexHull, HasSubset.Subset.trans, Iff.intro, convexHull_min
-- 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
t : ConvexCone 𝕜 M
⊢ Membership.mem (γ := Set (ConvexCone 𝕜 M)) {t : ConvexCone 𝕜 M | s ⊆ (↑t : Set M)} t ↔
    Membership.mem (γ := Set (ConvexCone 𝕜 M))
      {t : ConvexCone 𝕜 M | (convexHull 𝕜 : (a : Set M) → Set M) s ⊆ (↑t : Set M)} t

Tactic:
exact ⟨fun h => convexHull_min h t.convex, (subset_convexHull 𝕜 s).trans⟩
-- 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
⊢ Eq (α := ConvexCone 𝕜 M) (Convex.toCone ((convexHull 𝕜 : (a : Set M) → Set M) s) ⋯)
    (sInf {t : ConvexCone 𝕜 M | s ⊆ (↑t : Set M)})

Tactic:
Eq.symm <| IsGLB.sInf_eq <| IsLeast.isGLB <| convexHull_toCone_isLeast s

Premises used: IsGLB.sInf_eq, IsLeast.isGLB, convexHull_toCone_isLeast, Eq.symm
-- Module: Mathlib.Geometry.Convex.Cone.DualFinite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
⊢ Eq (α := PointedCone R N) (dual p (↑∅ : Set M)) ⊤

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.Cone.DualFinite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
C : PointedCone R N
hC : DualFG p C
obtain :
  ∀ (s : Finset M) (hs : dual p (↑s : Set M) = C), ∃ (D : PointedCone R M), Submodule.FG D ∧ dual p (↑D : Set M) = C
⊢ ∃ (D : PointedCone R M), Submodule.FG D ∧ dual p (↑D : Set M) = C

Tactic:
obtain ⟨s, hs⟩ := hC
-- Module: Mathlib.Geometry.Convex.Cone.DualFinite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
C : PointedCone R N
s : Finset M
hs : dual p (↑s : Set M) = C
⊢ dual p (↑(Submodule.span { c : R // 0 ≤ c } (↑s : Set M)) : Set M) = C

Tactic:
simp [hs]
-- Module: Mathlib.Geometry.Convex.Cone.DualFinite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
C : PointedCone R N
s : Finset M
hs : dual p (↑s : Set M) = C
⊢ ∃ (D : PointedCone R M), Submodule.FG D ∧ dual p (↑D : Set M) = C

Tactic:
exact ⟨_, Submodule.fg_span s.finite_toSet, by simp [hs]⟩
-- Module: Mathlib.Geometry.Convex.Cone.DualFinite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Finset M
h : Eq (α := PointedCone R N) (dual p (↑s : Set M)) (dual p (↑(Submodule.span { c : R // 0 ≤ c } (↑s : Set M)) : Set M))
⊢ DualFG p (dual p (↑(Submodule.span { c : R // 0 ≤ c } (↑s : Set M)) : Set M))

Tactic:
use s
-- Module: Mathlib.Geometry.Convex.Cone.DualFinite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Finset M
⊢ Eq (α := PointedCone R N) (dual p (↑s : Set M)) (dual p (↑(Submodule.span { c : R // 0 ≤ c } (↑s : Set M)) : Set M))

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.Cone.DualFinite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
C : PointedCone R N
hC : DualFG p C
obtain : ∀ (s : Finset M), DualFG (M := N →ₗ[R] R) LinearMap.id (dual p (↑s : Set M))
⊢ DualFG (M := N →ₗ[R] R) LinearMap.id C

Tactic:
obtain ⟨s, rfl⟩ := hC

Premises used: rfl
-- Module: Mathlib.Geometry.Convex.Cone.DualFinite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Finset M
h :
  Eq (α := PointedCone R N) (dual LinearMap.id (↑(Finset.image (⇑p : (a : M) → N →ₗ[R] R) s) : Set (N →ₗ[R] R)))
    (dual p (↑s : Set M))
⊢ DualFG (M := N →ₗ[R] R) LinearMap.id (dual p (↑s : Set M))

Tactic:
use Finset.image p s

Premises used: DFunLike.coe, Finset.image
-- Module: Mathlib.Geometry.Convex.Cone.DualFinite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Finset M
⊢ Eq (α := PointedCone R N) (dual LinearMap.id (↑(Finset.image (⇑p : (a : M) → N →ₗ[R] R) s) : Set (N →ₗ[R] R)))
    (dual p (↑s : Set M))

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.Cone.DualFinite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
C : PointedCone R N
hC : DualFG p C
obtain : ∀ (s : Finset M), DualFG (M := N →ₗ[R] R) LinearMap.id (dual p (↑s : Set M))
h :
  ∀ (s : Finset M),
    Eq (α := PointedCone R N) (dual LinearMap.id (↑(Finset.image (⇑p : (a : M) → N →ₗ[R] R) s) : Set (N →ₗ[R] R)))
      (dual p (↑s : Set M))
⊢ DualFG (M := N →ₗ[R] R) LinearMap.id C

Tactic:
classical
  obtain ⟨s, rfl⟩ := hC
  use Finset.image p s
  simp

Premises used: rfl
-- Module: Mathlib.Geometry.Convex.Cone.DualFinite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s w : Finset M
h : Eq (α := PointedCone R N) (dual p (↑s : Set M)) (dual p (↑s : Set M))
⊢ DualFG p (dual p (↑s : Set M))

Tactic:
use s
-- Module: Mathlib.Geometry.Convex.Cone.DualFinite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
hs : s.Finite
h : Eq (α := PointedCone R N) (dual p (↑(hs.toFinset (s := s)) : Set M)) (dual p s)
⊢ DualFG p (dual p s)

Tactic:
use hs.toFinset

Premises used: Set.Finite.toFinset
-- Module: Mathlib.Geometry.Convex.Cone.DualFinite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
hs : s.Finite
h h₁ : Eq (α := PointedCone R N) (dual p s) (dual p s)
⊢ Eq (α := PointedCone R N) (dual p (↑(hs.toFinset (s := s)) : Set M)) (dual p s)

Tactic:
rw [Set.Finite.coe_toFinset]

Premises used: Set.Finite.coe_toFinset
-- Module: Mathlib.Geometry.Convex.Cone.DualFinite
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
C : PointedCone R M
hC : Submodule.FG C
obtain : ∀ (s : Finset M), DualFG p (dual p (↑(Submodule.span { c : R // 0 ≤ c } (↑s : Set M)) : Set M))
⊢ DualFG p (dual p (↑C : Set M))

Tactic:
obtain ⟨s, rfl⟩ := hC

Premises used: rfl