awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 h₁ :
  Eq (α := PointedCone R N) (dual p (↑(hull R (↑s : Set M)) : Set M))
    (dual p (↑(Submodule.span { c : R // 0 ≤ c } (↑s : Set M)) : Set M))
⊢ Eq (α := PointedCone R N) (dual p (↑s : Set M)) (dual p (↑(Submodule.span { c : R // 0 ≤ c } (↑s : Set M)) : Set M))

Tactic:
rw [← dual_hull]

Premises used: PointedCone.dual_hull
-- 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 D : PointedCone R N
hC : DualFG p C
hD : DualFG p D
obtain : ∀ (S : Finset M), DualFG p (dual p (↑S : Set M) ⊓ D)
⊢ DualFG p (C ⊓ D)

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
D : PointedCone R N
hD : DualFG p D
S : Finset M
obtain : ∀ (T : Finset M), DualFG p (dual p (↑S : Set M) ⊓ dual p (↑T : Set M))
⊢ DualFG p (dual p (↑S : Set M) ⊓ D)

Tactic:
obtain ⟨T, rfl⟩ := hD

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 T : Finset M
h : Eq (α := PointedCone R N) (dual p (↑(S ∪ T) : Set M)) (dual p (↑S : Set M) ⊓ dual p (↑T : Set M))
⊢ DualFG p (dual p (↑S : Set M) ⊓ dual p (↑T : Set M))

Tactic:
use S ∪ T
-- 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 T : Finset M
h : Eq (α := PointedCone R N) (dual p ((↑S : Set M) ∪ (↑T : Set M))) (dual p (↑S : Set M) ⊓ dual p (↑T : Set M))
h₁ h₂ :
  Eq (α := PointedCone R N) (dual p (↑S : Set M) ⊓ dual p (↑T : Set M)) (dual p (↑S : Set M) ⊓ dual p (↑T : Set M))
⊢ Eq (α := PointedCone R N) (dual p (↑(S ∪ T) : Set M)) (dual p (↑S : Set M) ⊓ dual p (↑T : Set M))

Tactic:
rw [Finset.coe_union, dual_union]

Premises used: PointedCone.dual_union, Finset.coe_union
-- 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 D : PointedCone R N
hC : DualFG p C
hD : DualFG p D
obtain obtain₁ : ∀ (S : Finset M), DualFG p (dual p (↑S : Set M) ⊓ D)
obtain₂ : ∀ (S T : Finset M), DualFG p (dual p (↑S : Set M) ⊓ dual p (↑T : Set M))
h h₁ :
  ∀ (S T : Finset M), Eq (α := PointedCone R N) (dual p (↑(S ∪ T) : Set M)) (dual p (↑S : Set M) ⊓ dual p (↑T : Set M))
⊢ DualFG p (C ⊓ D)

Tactic:
classical
  obtain ⟨S, rfl⟩ := hC; obtain ⟨T, rfl⟩ := hD
  use S ∪ T; rw [Finset.coe_union, dual_union]

Premises used: PointedCone.dual_union, rfl, Finset.coe_union
-- 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 :
  ∀ (D : PointedCone R M) (hDualFG : Submodule.FG D) (hC : DualFG p (dual p (↑D : Set M))),
    Eq (α := PointedCone R N) (dual p (↑(dual p.flip (↑(dual p (↑D : Set M)) : Set N)) : Set M)) (dual p (↑D : Set M))
⊢ dual p (↑(dual p.flip (↑C : Set N)) : Set M) = C

Tactic:
obtain ⟨D, hDualFG, rfl⟩ := exists_fg_dual hC

Premises used: PointedCone.DualFG.exists_fg_dual, 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
D : PointedCone R M
hDualFG : Submodule.FG D
hC : DualFG p (dual p (↑D : Set M))
⊢ Eq (α := PointedCone R N) (dual p (↑(dual p.flip (↑(dual p (↑D : Set M)) : Set N)) : Set M)) (dual p (↑D : Set M))

Tactic:
dual_dual_flip_dual (p := p) D

Premises used: setOf, SetLike.coe, PointedCone.dual_dual_flip_dual
-- 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
D : PointedCone R M
hDualFG : Submodule.FG D
hC : DualFG p (dual p (↑D : Set M))
⊢ Eq (α := PointedCone R N) (dual p (↑(dual p.flip (↑(dual p (↑D : Set M)) : Set N)) : Set M)) (dual p (↑D : Set M))

Tactic:
exact dual_dual_flip_dual (p := p) D

Premises used: SetLike.coe, PointedCone.dual_dual_flip_dual
-- 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 : DualFG p.flip C
⊢ dual p.flip (↑(dual p (↑C : Set M)) : Set N) = C

Tactic:
hC.dual_dual_flip

Premises used: PointedCone.DualFG.dual_dual_flip, setOf
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
S : Submodule R E
⊢ (↑(↑S : PointedCone R E) : Set E) = (↑S : Set E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
S : Submodule R E
x : E
⊢ Membership.mem (γ := PointedCone R E) (↑S : PointedCone R E) x ↔ x ∈ S

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
S T : Submodule R E
⊢ Eq (α := PointedCone R E) (↑S : PointedCone R E) (↑T : PointedCone R E) ↔ S = T

Tactic:
restrictScalars_inj ..

Premises used: Submodule.restrictScalars_inj
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
S T : Submodule R E
⊢ LE.le (α := PointedCone R E) (↑S : PointedCone R E) (↑T : PointedCone R E) ↔ S ≤ T

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
S T : Submodule R E
⊢ LT.lt (α := PointedCone R E) (↑S : PointedCone R E) (↑T : PointedCone R E) ↔ S < T

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
S T : Submodule R E
⊢ Eq (α := PointedCone R E) (↑(S ⊓ T) : PointedCone R E) ((↑S : PointedCone R E) ⊓ (↑T : PointedCone R E))

Tactic:
restrictScalars_inf _ _ _

Premises used: Submodule.restrictScalars_inf
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
S T : Submodule R E
⊢ Eq (α := PointedCone R E) (↑(S ⊔ T) : PointedCone R E) ((↑S : PointedCone R E) ⊔ (↑T : PointedCone R E))

Tactic:
restrictScalars_sup _ _ _

Premises used: Set.Mem, setOf, Submodule.restrictScalars_sup
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
s : Set (Submodule R E)
⊢ Eq (α := PointedCone R E) (↑(sInf s) : PointedCone R E) (sInf (ofSubmodule '' s))

Tactic:
ofSubmoduleLatticeHom.map_sInf' s

Premises used: Set.Mem, Submodule.restrictScalars, CompleteLatticeHom.tosInfHom, PointedCone.ofSubmoduleLatticeHom, sInfHom.map_sInf'
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
s : Set (Submodule R E)
rw : Eq (α := PointedCone R E) (↑(sInf s) : PointedCone R E) (⨅ S ∈ s, (↑S : PointedCone R E))
rw₁ : Eq (α := PointedCone R E) (sInf (ofSubmodule '' s)) (⨅ S ∈ s, (↑S : PointedCone R E))
rw₂ :
  Eq.{u_2 + 1} (α := PointedCone R E)
    (⨅ (a : PointedCone R E), ⨅ (_ : Membership.mem (γ := Set (PointedCone R E)) (ofSubmodule '' s) a), a)
    (⨅ S ∈ s, (↑S : PointedCone R E))
rw₃ rw₄ : Eq.{u_2 + 1} (α := PointedCone R E) (⨅ b ∈ s, (↑b : PointedCone R E)) (⨅ S ∈ s, (↑S : PointedCone R E))
⊢ Eq.{u_2 + 1} (α := PointedCone R E) (↑(⨅ S ∈ s, S) : PointedCone R E) (⨅ S ∈ s, (↑S : PointedCone R E))

Tactic:
rw [← sInf_eq_iInf, ofSubmodule_sInf, sInf_eq_iInf, iInf_image]

Premises used: PointedCone.ofSubmodule_sInf, sInf_eq_iInf, iInf_image
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
s : Set (Submodule R E)
⊢ Eq (α := PointedCone R E) (↑(sSup s) : PointedCone R E) (sSup (ofSubmodule '' s))

Tactic:
ofSubmoduleLatticeHom.map_sSup' s

Premises used: Set.Mem, CompleteLatticeHom.map_sSup', Submodule.restrictScalars, setOf, PointedCone.ofSubmoduleLatticeHom
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
s : Set (Submodule R E)
rw : Eq (α := PointedCone R E) (↑(sSup s) : PointedCone R E) (⨆ S ∈ s, (↑S : PointedCone R E))
rw₁ : Eq (α := PointedCone R E) (sSup (ofSubmodule '' s)) (⨆ S ∈ s, (↑S : PointedCone R E))
rw₂ :
  Eq.{u_2 + 1} (α := PointedCone R E)
    (⨆ (a : PointedCone R E), ⨆ (_ : Membership.mem (γ := Set (PointedCone R E)) (ofSubmodule '' s) a), a)
    (⨆ S ∈ s, (↑S : PointedCone R E))
rw₃ rw₄ : Eq.{u_2 + 1} (α := PointedCone R E) (⨆ b ∈ s, (↑b : PointedCone R E)) (⨆ S ∈ s, (↑S : PointedCone R E))
⊢ Eq.{u_2 + 1} (α := PointedCone R E) (↑(⨆ S ∈ s, S) : PointedCone R E) (⨆ S ∈ s, (↑S : PointedCone R E))

Tactic:
rw [← sSup_eq_iSup, ofSubmodule_sSup, sSup_eq_iSup, iSup_image]

Premises used: PointedCone.ofSubmodule_sSup, iSup_image, sSup_eq_iSup
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_5
E : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup E
inst_4 : Module R E
S : Submodule R E
⊢ Eq (α := PointedCone R E) (-(↑S : PointedCone R E)) (↑(-S) : PointedCone R E)

Tactic:
neg_restrictScalars S

Premises used: Submodule.neg_restrictScalars
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
x x_1 : PointedCone R E
⊢ (↑x : ConvexCone R E) = (↑x_1 : ConvexCone R E) → x = x_1

Tactic:
simp [toConvexCone]

Premises used: PointedCone.toConvexCone
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
C : PointedCone R E
⊢ (↑C : ConvexCone R E).Pointed

Tactic:
simp [toConvexCone, ConvexCone.Pointed]

Premises used: ConvexCone.Pointed, PointedCone.toConvexCone
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
C : PointedCone R E
x : E
⊢ x ∈ (↑C : ConvexCone R E) ↔ x ∈ C

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
C₁ C₂ : PointedCone R E
h : ∀ (x : E), x ∈ C₁ ↔ x ∈ C₂
⊢ C₁ = C₂

Tactic:
SetLike.ext h

Premises used: SetLike.ext
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
C : PointedCone R E
⊢ Convex R (↑C : Set E)

Tactic:
C.toConvexCone.convex

Premises used: ConvexCone.convex, PointedCone.toConvexCone
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
x : E
r : R
C : PointedCone R E
hr : 0 ≤ r
hx : x ∈ C
⊢ r • x ∈ C

Tactic:
C.smul_mem ⟨r, hr⟩ hx

Premises used: Set.Mem, Subtype.mk, Submodule.smul_mem
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
C_1 C₁ C₂ : PointedCone R E
x_1 : E
r : R
C : ConvexCone R E
hC : C.Pointed
x_2 : R≥0
x : E
hx : x ∈ (↑C : Set E)
c : R
hc : 0 ≤ c
inl : ∀ (hzero : 0 = c), Subtype.mk (p := fun (c : R) ↦ 0 ≤ c) c hc • x ∈ C
inr : ∀ (hpos : 0 < c), Subtype.mk (p := fun (c : R) ↦ 0 ≤ c) c hc • x ∈ C
⊢ Subtype.mk (p := fun (c : R) ↦ 0 ≤ c) c hc • x ∈ C

Tactic:
rcases eq_or_lt_of_le hc with hzero | hpos

Premises used: eq_or_lt_of_le
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
C_1 C₁ C₂ : PointedCone R E
x_1 : E
r : R
C : ConvexCone R E
hC : 0 ∈ C
x_2 : R≥0
x : E
hx : x ∈ (↑C : Set E)
c : R
hc : 0 ≤ c
hzero : 0 = c
⊢ 0 ∈ C

Tactic:
hC
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
C_1 C₁ C₂ : PointedCone R E
x_1 : E
r : R
C : ConvexCone R E
hC : 0 ∈ C
x_2 : R≥0
x : E
hx : x ∈ (↑C : Set E)
c : R
hc : 0 ≤ c
hzero : 0 = c
h : Subtype.mk (p := fun (c : R) ↦ 0 ≤ c) c hc • x = 0
⊢ Subtype.mk (p := fun (c : R) ↦ 0 ≤ c) c hc • x ∈ C

Tactic:
convert! hC
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
C_1 C₁ C₂ : PointedCone R E
x_1 : E
r : R
C : ConvexCone R E
hC : 0 ∈ C
x_2 : R≥0
x : E
hx : x ∈ (↑C : Set E)
c : R
hc : 0 ≤ c
hzero : 0 = c
⊢ Subtype.mk (p := fun (c : R) ↦ 0 ≤ c) c hc • x = 0

Tactic:
simp [← hzero]
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
C_1 C₁ C₂ : PointedCone R E
x_1 : E
r : R
C : ConvexCone R E
hC : C.Pointed
x_2 : R≥0
x : E
hx : x ∈ (↑C : Set E)
c : R
hc : 0 ≤ c
hpos : 0 < c
inr : 0 < (↑(Subtype.mk (p := fun (c : R) ↦ 0 ≤ c) c hc) : R)
inr₁ : x ∈ C
⊢ Subtype.mk (p := fun (c : R) ↦ 0 ≤ c) c hc • x ∈ C

Tactic:
apply ConvexCone.smul_mem

Premises used: ConvexCone.smul_mem
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
C_1 C₁ C₂ : PointedCone R E
x_1 : E
r : R
C : ConvexCone R E
hC : C.Pointed
x_2 : R≥0
x : E
hx : x ∈ (↑C : Set E)
c : R
hc : 0 ≤ c
hpos : 0 < c
⊢ 0 < c

Tactic:
hpos
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
C_1 C₁ C₂ : PointedCone R E
x_1 : E
r : R
C : ConvexCone R E
hC : C.Pointed
x_2 : R≥0
x : E
hx : x ∈ (↑C : Set E)
c : R
hc : 0 ≤ c
hpos : 0 < c
⊢ 0 < (↑(Subtype.mk (p := fun (c : R) ↦ 0 ≤ c) c hc) : R)

Tactic:
convert! hpos
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
C_1 C₁ C₂ : PointedCone R E
x_1 : E
r : R
C : ConvexCone R E
hC : C.Pointed
x_2 : R≥0
x : E
hx : x ∈ (↑C : Set E)
c : R
hc : 0 ≤ c
hpos : 0 < c
⊢ x ∈ C

Tactic:
hx
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
C_1 C₁ C₂ : PointedCone R E
x_1 : E
r : R
C : ConvexCone R E
hC : C.Pointed
x_2 : R≥0
x : E
hx : x ∈ (↑C : Set E)
c : R
hc : 0 ≤ c
hpos : 0 < c
⊢ x ∈ C

Tactic:
exact hx
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
C : ConvexCone R E
hC : C.Pointed
x : E
⊢ Membership.mem (γ := PointedCone R E) (C.toPointedCone hC) x ↔ x ∈ C

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
C : ConvexCone R E
hC : C.Pointed
⊢ (↑(C.toPointedCone hC) : ConvexCone R E) = C

Tactic:
rfl

Premises used: rfl, PointedCone.toConvexCone
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
⊢ Eq.{u_2 + 1} (α := PointedCone R E) (ConvexCone.toPointedCone ⊤ trivial) ⊤

Tactic:
rfl

Premises used: Set.univ, setOf, ConvexCone.toPointedCone, rfl
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
s : Set E
⊢ s ⊆ (↑(hull R s) : Set E)

Tactic:
subset_span

Premises used: Submodule.subset_span
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
s : Set E
⊢ LE.le (α := PointedCone R E) (hull R s) (↑(span R s) : PointedCone R E)

Tactic:
span_le_restrictScalars R≥0 R s

Premises used: Set.Mem, setOf, Submodule.span_le_restrictScalars, Subtype, LE.le, OfNat.ofNat
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
x : E
s : Set E
rw :
  (∃ (c : Finsupp.{u_2, u_1} E R≥0), (↑c.support : Set E) ⊆ s ∧ (c.sum fun (mi : E) (r : R≥0) ↦ r • mi) = x) ↔
    ∃ (c : E →₀ R),
      (↑c.support : Set E) ⊆ s ∧
        (∀ (y : E), LE.le.{u_1} (α := R) (0 : R) ((c : (a : E) → R) y : R)) ∧ (c.sum fun (m : E) (r : R) ↦ r • m) = x
⊢ Membership.mem (γ := PointedCone R E) (hull R s) x ↔
    ∃ (c : E →₀ R),
      (↑c.support : Set E) ⊆ s ∧
        (∀ (y : E), LE.le.{u_1} (α := R) (0 : R) ((c : (a : E) → R) y : R)) ∧ (c.sum fun (m : E) (r : R) ↦ r • m) = x

Tactic:
rw [mem_span_set]

Premises used: Submodule.mem_span_set
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
x : E
s : Set E
mp :
  (∃ (c : Finsupp.{u_2, u_1} E R≥0), (↑c.support : Set E) ⊆ s ∧ (c.sum fun (mi : E) (r : R≥0) ↦ r • mi) = x) →
    ∃ (c : E →₀ R),
      (↑c.support : Set E) ⊆ s ∧
        (∀ (y : E), LE.le.{u_1} (α := R) (0 : R) ((c : (a : E) → R) y : R)) ∧ (c.sum fun (m : E) (r : R) ↦ r • m) = x
mpr :
  (∃ (c : E →₀ R),
      (↑c.support : Set E) ⊆ s ∧
        (∀ (y : E), LE.le.{u_1} (α := R) (0 : R) ((c : (a : E) → R) y : R)) ∧ (c.sum fun (m : E) (r : R) ↦ r • m) = x) →
    ∃ (c : Finsupp.{u_2, u_1} E R≥0), (↑c.support : Set E) ⊆ s ∧ (c.sum fun (mi : E) (r : R≥0) ↦ r • mi) = x
⊢ (∃ (c : Finsupp.{u_2, u_1} E R≥0), (↑c.support : Set E) ⊆ s ∧ (c.sum fun (mi : E) (r : R≥0) ↦ r • mi) = x) ↔
    ∃ (c : E →₀ R),
      (↑c.support : Set E) ⊆ s ∧
        (∀ (y : E), LE.le.{u_1} (α := R) (0 : R) ((c : (a : E) → R) y : R)) ∧ (c.sum fun (m : E) (r : R) ↦ r • m) = x

Tactic:
constructor
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
s : Set E
c : Finsupp.{u_2, u_1} E R≥0
hc : (↑c.support : Set E) ⊆ s
⊢ ∀ (a : E),
    a ∈ c.support ↔
      Ne.{u_1 + 1} (α := R) (comp (β := R≥0) (Subtype.val (p := fun (c : R) ↦ 0 ≤ c)) (⇑c : (a : E) → R≥0) a) 0

Tactic:
simp [← Subtype.val_inj]

Premises used: Subtype.val_inj
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
s : Set E
c : Finsupp.{u_2, u_1} E R≥0
hc : (↑c.support : Set E) ⊆ s
⊢ ∃ (c_1 : E →₀ R),
    (↑c_1.support : Set E) ⊆ s ∧
      (∀ (y : E), LE.le.{u_1} (α := R) (0 : R) ((c_1 : (a : E) → R) y : R)) ∧
        Eq (α := E) (c_1.sum fun (m : E) (r : R) ↦ r • m) (c.sum fun (mi : E) (r : R≥0) ↦ r • mi)

Tactic:
exact ⟨⟨c.support, Subtype.val ∘ c, by simp [← Subtype.val_inj]⟩, hc, fun y ↦ (c y).2, rfl⟩
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
s : Set E
c : E →₀ R
hc : (↑c.support : Set E) ⊆ s
hc₀ : ∀ (y : E), LE.le.{u_1} (α := R) (0 : R) ((c : (a : E) → R) y : R)
⊢ ∀ (a : E),
    a ∈ c.support ↔
      Ne.{u_1 + 1} (α := R≥0) ((fun (y : E) ↦ (Subtype.mk (p := fun (c : R) ↦ 0 ≤ c) ((c : (a : E) → R) y) ⋯ : R≥0)) a)
        0

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
s : Set E
c : E →₀ R
hc : (↑c.support : Set E) ⊆ s
hc₀ : ∀ (y : E), LE.le.{u_1} (α := R) (0 : R) ((c : (a : E) → R) y : R)
⊢ ∃ (c_1 : Finsupp.{u_2, u_1} E R≥0),
    (↑c_1.support : Set E) ⊆ s ∧
      Eq (α := E) (c_1.sum fun (mi : E) (r : R≥0) ↦ r • mi) (c.sum fun (m : E) (r : R) ↦ r • m)

Tactic:
exact ⟨⟨c.support, fun y ↦ ⟨c y, hc₀ _⟩, by simp⟩, hc, rfl⟩
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
inst_5 : AddCommMonoid F
inst_6 : Module R F
C : PointedCone R E
f : E →ₗ[R] F
⊢ (↑(map f C) : ConvexCone R F) = ConvexCone.map f (↑C : ConvexCone R E)

Tactic:
rfl

Premises used: Set.Mem, ConvexCone.map, setOf, Set.image, rfl, PointedCone.toConvexCone
-- Module: Mathlib.Geometry.Convex.Cone.Pointed
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
inst_5 : AddCommMonoid F
inst_6 : Module R F
C : PointedCone R E
f : E →ₗ[R] F
⊢ (↑(map f C) : Set F) = (⇑f : (a : E) → F) '' (↑C : Set E)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.image, rfl