awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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 : SMul R M
C C₁_1 C₂_1 : ConvexCone R M
s : Set M
c : R
x : M
C₁ C₂ : ConvexCone R M
h : C₁.carrier = C₂.carrier
⊢ C₁ = C₂
have mk : ∀ (carrier : Set M) (smul_mem' : ∀ ⦃c : R⦄, 0 < c → ∀ ⦃x : M⦄, x ∈ carrier → c • x ∈ carrier)
  (add_mem' : ∀ ⦃x : M⦄, x ∈ carrier → ∀ ⦃y : M⦄, y ∈ carrier → x + y ∈ carrier)
  (h : { carrier := carrier, smul_mem' := smul_mem', add_mem' := add_mem' : ConvexCone R M }.carrier = C₂.carrier),
  { carrier := carrier, smul_mem' := smul_mem', add_mem' := add_mem' : ConvexCone R M } = C₂
Tactic: cases C₁
Cleared hypotheses: C₁, h
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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 : Set M) = (↑⊥ : Set M) ↔ C = ⊥
have norm_cast : C = ⊥ ↔ C = ⊥
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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 : AddCommMonoid N
inst_4 : AddCommMonoid O
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R O
f : M →ₗ[R] N
C : ConvexCone R N
c : R
hc : 0 < c
x : M
hx : Membership.mem (γ := Set M) ((⇑f : (a : M) → N) ⁻¹' (↑C : Set N)) x
⊢ Membership.mem (γ := Set M) ((⇑f : (a : M) → N) ⁻¹' (↑C : Set N)) (c • x)
have rw : HSMul.hSMul (β := N) c ((f : (a : M) → N) x : N) ∈ (↑C : Set N)
Tactic: rw [mem_preimage, f.map_smul c]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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 : AddCommMonoid N
inst_4 : AddCommMonoid O
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R O
f : M →ₗ[R] N
C : ConvexCone R N
x : M
hx : Membership.mem (γ := Set M) ((⇑f : (a : M) → N) ⁻¹' (↑C : Set N)) x
y : M
hy : Membership.mem (γ := Set M) ((⇑f : (a : M) → N) ⁻¹' (↑C : Set N)) y
⊢ Membership.mem (γ := Set M) ((⇑f : (a : M) → N) ⁻¹' (↑C : Set N)) (x + y)
have rw : HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N) ∈ (↑C : Set N)
Tactic: rw [mem_preimage, f.map_add]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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
⊢ C.Pointed
have obtain : ∀ (x : G) (hx : x ∈ C), x ≠ 0 → ∀ (hxneg : -x ∈ C), C.Pointed
Tactic: obtain ⟨x, hx, _, hxneg⟩ := hC
Cleared hypotheses: hC
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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
⊢ C.Pointed
have rw : x + -x ∈ C
Tactic: rw [Pointed, ← add_neg_cancel x]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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.Blunt → C.Salient
have rw : ¬C.Pointed → ¬C.Flat
Tactic: rw [salient_iff_not_flat, blunt_iff_not_pointed]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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
⊢ x - x ∈ C
have rw : 0 ∈ C
Tactic: rw [sub_self x]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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
⊢ a = b
have by_contra : ∀ (h : ¬a = b), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (hypothesis)
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
⊢ False
have h' : b - a ≠ 0
Tactic: have h' : b - a ≠ 0 := fun h'' => h (eq_of_sub_eq_zero h'').symm
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (hypothesis)
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
⊢ False
have H : -(b - a) ∉ C
Tactic: have H := h₂ (b - a) ab h'
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (hypothesis)
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
⊢ False
have H₁ : a - b ∉ C
Tactic: rw [neg_sub b a] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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
⊢ b + c - (a + c) ∈ C
have rwa : b - a ∈ C
Tactic: rwa [add_sub_add_right_eq_sub]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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
⊢ Pointed.{u_2, u_4} (R := R) (M := M) 0
have rw : Membership.mem (γ := ConvexCone R M) 0 0
Tactic: rw [Pointed, mem_zero]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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
⊢ Pointed.{u_2, u_4} (R := R) (M := M) 0
have rw₁ : Eq.{u_4 + 1} (α := M) 0 0
Tactic: rw [Pointed, mem_zero]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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)
⊢ HSMul.hSMul (β := M) c ((fun (x1 x2 : M) ↦ x1 + x2) x y) ∈ (↑C₁ : Set M) + (↑C₂ : Set M)
have rw : c • x + c • y ∈ (↑C₁ : Set M) + (↑C₂ : Set M)
Tactic: rw [smul_add]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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
⊢ c • x + c • y ∈ (↑C₁ : Set M) + (↑C₂ : Set M)
have left : c • x ∈ (↑C₁ : Set M)
Tactic: use c • x, C₁.smul_mem hc hx, c • y, C₂.smul_mem hc hy
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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
⊢ c • x + c • y ∈ (↑C₁ : Set M) + (↑C₂ : Set M)
have left₁ : c • y ∈ (↑C₂ : Set M)
Tactic: use c • x, C₁.smul_mem hc hx, c • y, C₂.smul_mem hc hy
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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)
⊢ c • x + c • y ∈ (↑C₁ : Set M) + (↑C₂ : Set M)
have right : (fun (x1 x2 : M) ↦ x1 + x2) (c • x) (c • y) = c • x + c • y
Tactic: use c • x, C₁.smul_mem hc hx, c • y, C₂.smul_mem hc hy
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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
⊢ 0 + x_1 = x_1
have h : ∀ (x : M), x ∈ 0 + x_1 ↔ x ∈ x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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_1 + 0 = x_1
have h : ∀ (x : M), x ∈ x_1 + 0 ↔ x ∈ x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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
⊢ C₂.IsGenerating
have rw : ∀ (hgen : LE.le (α := Submodule R M) ⊤ (Submodule.span R (↑C₁ : Set M))),
  LE.le (α := Submodule R M) ⊤ (Submodule.span R (↑C₂ : Set M))
Tactic: rw [IsGenerating, ← top_le_iff] at hgen ⊢
Cleared hypotheses: hgen
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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
⊢ Eq (α := Submodule R M) (Submodule.span R (↑C : Set M)) ⊤
have rw : LE.le (α := Submodule R M) ⊤ (Submodule.span R (↑C : Set M))
Tactic: rw [eq_top_iff]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R (↑C : Set M)) x
have 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
Tactic: rw [IsReproducing, Set.eq_univ_iff_forall] at h
Cleared hypotheses: h, x
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R (↑C : Set M)) x
have 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)
Tactic: obtain ⟨y, hy, z, hz, rfl⟩ := Set.mem_sub.mp (h x)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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)) ⊤
⊢ C.IsReproducing
have rw : ∀ (x : M), x ∈ (↑C : Set M) - (↑C : Set M)
Tactic: rw [IsReproducing, Set.eq_univ_iff_forall]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (hypothesis)
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
⊢ x ∈ (↑C : Set M) - (↑C : Set M)
have hne : (↑C : Set M).Nonempty
Tactic: have hne : (C : Set M).Nonempty := Set.nonempty_iff_ne_empty.2 fun h' => by simp [h'] at h
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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
⊢ 0 ∈ (↑C : Set M) - (↑C : Set M)
have obtain : ∀ (c : M) (hc : c ∈ (↑C : Set M)), 0 ∈ (↑C : Set M) - (↑C : Set M)
Tactic: obtain ⟨c, hc⟩ := hne
Cleared hypotheses: hne
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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)
⊢ HSMul.hSMul (β := M) r ((fun (x1 x2 : M) ↦ x1 - x2) y z) ∈ (↑C : Set M) - (↑C : Set M)
have simp : ∃ x ∈ C, ∃ y_1 ∈ C, x - y_1 = r • (y - z)
Tactic: simp only [Set.mem_sub, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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)
⊢ ∃ x ∈ C, ∃ y_1 ∈ C, x - y_1 = r • (y - z)
have inl : ∀ (hr : r < 0), ∃ x ∈ C, ∃ y_1 ∈ C, x - y_1 = r • (y - z)
Tactic: rcases lt_trichotomy r 0 with hr | rfl | hr
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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)
⊢ ∃ x ∈ C, ∃ y_1 ∈ C, x - y_1 = r • (y - z)
have inr : ∃ x ∈ C, ∃ y_1 ∈ C, x - y_1 = HSMul.hSMul.{u_7, u_8, u_8} (α := R) 0 (y - z)
Tactic: rcases lt_trichotomy r 0 with hr | rfl | hr
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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)
⊢ ∃ x ∈ C, ∃ y_1 ∈ C, x - y_1 = r • (y - z)
have inr₁ : ∀ (hr : 0 < r), ∃ x ∈ C, ∃ y_1 ∈ C, x - y_1 = r • (y - z)
Tactic: rcases lt_trichotomy r 0 with hr | rfl | hr
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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)
have inl : -r • z - -r • y = 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, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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
⊢ -r • z - -r • y = r • (y - z)
have inl : -(r • z) - -r • y = r • (y - z)
Tactic: rw [neg_smul, neg_smul, neg_sub_neg, smul_sub]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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)
⊢ -r • z - -r • y = r • (y - z)
have inl₁ : -(r • z) - -(r • y) = r • (y - z)
Tactic: rw [neg_smul, neg_smul, neg_sub_neg, smul_sub]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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)
⊢ -r • z - -r • y = r • (y - z)
have inl₂ : r • y - r • z = r • (y - z)
Tactic: rw [neg_smul, neg_smul, neg_sub_neg, smul_sub]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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)
⊢ -r • z - -r • y = r • (y - z)
have inl₃ : r • y - r • z = r • y - r • z
Tactic: rw [neg_smul, neg_smul, neg_sub_neg, smul_sub]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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)
⊢ ∃ x ∈ C, ∃ y_1 ∈ C, x - y_1 = HSMul.hSMul.{u_7, u_8, u_8} (α := R) 0 (y - z)
have inr : ∃ x ∈ C, ∃ y ∈ C, x - y = 0
Tactic: simp only [zero_smul]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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)
⊢ ∃ x ∈ C, ∃ y ∈ C, x - y = 0
have inr : ∀ (c : M) (hc : c ∈ (↑C : Set M)), ∃ x ∈ C, ∃ y ∈ C, x - y = 0
Tactic: obtain ⟨c, hc⟩ := hne
Cleared hypotheses: hne
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (hypothesis)
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' := ⋯ }
⊢ x ∈ (↑C : Set M) - (↑C : Set M)
have hCS : (↑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⟩
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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
⊢ 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)
have this : ∀ (r₂ : 𝕜) (hr₂ : 0 < r₂) (hy : y ∈ r₂ • s), Membership.mem (γ := Set M) {y : M | ∃ (r : 𝕜), 0 < r ∧ y ∈ r • s} (r₁ • y)
Tactic: ⟨r₂, hr₂, hy⟩
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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)
have refine : r₁ • y ∈ (r₁ * r₂) • s
Tactic: refine ⟨r₁ * r₂, mul_pos hr₁ hr₂, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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
have rw : r₁ • y ∈ r₁ • r₂ • s
Tactic: rw [mul_smul]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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₂)
have refine : y₁ + y₂ ∈ (r₁ + r₂) • s
Tactic: refine ⟨r₁ + r₂, add_pos hr₁ hr₂, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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₁ + r₂) • s
have rw : y₁ + y₂ ∈ r₁ • s + r₂ • s
Tactic: rw [hs.add_smul hr₁.le hr₂.le]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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
⊢ (↑(hull 𝕜 s) : Set M) = {x : M | ∃ (r : 𝕜), 0 < r ∧ x ∈ r • s}
have h : ∀ (x : M), x ∈ (↑(hull 𝕜 s) : Set M) ↔ Membership.mem (γ := Set M) {x : M | ∃ (r : 𝕜), 0 < r ∧ x ∈ r • s} x
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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) C → Disjoint s (↑C : Set M)
have rw : Disjoint (↑(hull 𝕜 s) : Set M) (↑C : Set M) → Disjoint s (↑C : Set M)
Tactic: rw [← disjoint_coe]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Basic (goal)
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 s (↑C : Set M) → Disjoint (hull 𝕜 s) C
have simp_rw : (∀ ⦃a : M⦄, a ∈ s → a ∉ C) → ∀ ⦃a : M⦄, (∃ (r : 𝕜), 0 < r ∧ a ∈ r • s) → a ∉ C
Tactic: simp_rw [← disjoint_coe, disjoint_left, SetLike.mem_coe, mem_hull_of_convex hs]