[GOAL]
R : Type u_1
inst✝⁶ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_4
inst✝¹ : DecidableEq ι
x✝ y✝ z : M
inst✝ : Subsingleton M
x y : M
⊢ SameRay R x y
[PROOFSTEP]
rw [Subsingleton.elim x 0]
[GOAL]
R : Type u_1
inst✝⁶ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_4
inst✝¹ : DecidableEq ι
x✝ y✝ z : M
inst✝ : Subsingleton M
x y : M
⊢ SameRay R 0 y
[PROOFSTEP]
exact zero_left _
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x✝ y z x : M
⊢ SameRay R x x
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u_1
inst✝⁶ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_4
inst✝¹ : DecidableEq ι
x✝ y z x : M
inst✝ : Nontrivial R
⊢ SameRay R x x
[PROOFSTEP]
exact Or.inr (Or.inr <| ⟨1, 1, zero_lt_one, zero_lt_one, rfl⟩)
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy : y = 0 → x = 0 ∨ z = 0
⊢ SameRay R x z
[PROOFSTEP]
rcases eq_or_ne x 0 with (rfl | hx)
[GOAL]
case inl
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
y z : M
hyz : SameRay R y z
hxy : SameRay R 0 y
hy : y = 0 → 0 = 0 ∨ z = 0
⊢ SameRay R 0 z
[PROOFSTEP]
exact zero_left z
[GOAL]
case inr
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
⊢ SameRay R x z
[PROOFSTEP]
rcases eq_or_ne z 0 with (rfl | hz)
[GOAL]
case inr.inl
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y : M
hxy : SameRay R x y
hx : x ≠ 0
hyz : SameRay R y 0
hy : y = 0 → x = 0 ∨ 0 = 0
⊢ SameRay R x 0
[PROOFSTEP]
exact zero_right x
[GOAL]
case inr.inr
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
⊢ SameRay R x z
[PROOFSTEP]
rcases eq_or_ne y 0 with (rfl | hy)
[GOAL]
case inr.inr.inl
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x z : M
hx : x ≠ 0
hz : z ≠ 0
hxy : SameRay R x 0
hyz : SameRay R 0 z
hy : 0 = 0 → x = 0 ∨ z = 0
⊢ SameRay R x z
[PROOFSTEP]
exact (hy rfl).elim (fun h => (hx h).elim) fun h => (hz h).elim
[GOAL]
case inr.inr.inr
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy✝ : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
hy : y ≠ 0
⊢ SameRay R x z
[PROOFSTEP]
rcases hxy.exists_pos hx hy with ⟨r₁, r₂, hr₁, hr₂, h₁⟩
[GOAL]
case inr.inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy✝ : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
hy : y ≠ 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h₁ : r₁ • x = r₂ • y
⊢ SameRay R x z
[PROOFSTEP]
rcases hyz.exists_pos hy hz with ⟨r₃, r₄, hr₃, hr₄, h₂⟩
[GOAL]
case inr.inr.inr.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy✝ : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
hy : y ≠ 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h₁ : r₁ • x = r₂ • y
r₃ r₄ : R
hr₃ : 0 < r₃
hr₄ : 0 < r₄
h₂ : r₃ • y = r₄ • z
⊢ SameRay R x z
[PROOFSTEP]
refine' Or.inr (Or.inr <| ⟨r₃ * r₁, r₂ * r₄, mul_pos hr₃ hr₁, mul_pos hr₂ hr₄, _⟩)
[GOAL]
case inr.inr.inr.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy✝ : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
hy : y ≠ 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h₁ : r₁ • x = r₂ • y
r₃ r₄ : R
hr₃ : 0 < r₃
hr₄ : 0 < r₄
h₂ : r₃ • y = r₄ • z
⊢ (r₃ * r₁) • x = (r₂ * r₄) • z
[PROOFSTEP]
rw [mul_smul, mul_smul, h₁, ← h₂, smul_comm]
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z v : M
r : R
h✝ : 0 ≤ r
h : 0 < r
⊢ 0 < 1
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u_1
inst✝⁶ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_4
inst✝¹ : DecidableEq ι
x y z v : M
r : R
h✝ : 0 ≤ r
h : 0 < r
inst✝ : Nontrivial R
⊢ 0 < 1
[PROOFSTEP]
exact zero_lt_one
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
r : R
h : SameRay R x y
hr : 0 ≤ r
hy : y = 0
⊢ r • y = 0
[PROOFSTEP]
rw [hy, smul_zero]
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
f : M →ₗ[R] N
h : SameRay R x y
hx : x = 0
⊢ ↑f x = 0
[PROOFSTEP]
rw [hx, map_zero]
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
f : M →ₗ[R] N
h : SameRay R x y
hy : y = 0
⊢ ↑f y = 0
[PROOFSTEP]
rw [hy, map_zero]
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
f : M →ₗ[R] N
h✝ : SameRay R x y
x✝ : ∃ r₁ r₂, 0 < r₁ ∧ 0 < r₂ ∧ r₁ • x = r₂ • y
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x = r₂ • y
⊢ r₁ • ↑f x = r₂ • ↑f y
[PROOFSTEP]
rw [← f.map_smul, ← f.map_smul, h]
[GOAL]
R : Type u_1
inst✝⁶ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_4
inst✝¹ : DecidableEq ι
x y z : M
F : Type u_5
inst✝ : LinearMapClass F R M N
f : F
hf : Function.Injective ↑f
⊢ SameRay R (↑f x) (↑f y) ↔ SameRay R x y
[PROOFSTEP]
simp only [SameRay, map_zero, ← hf.eq_iff, map_smul]
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
hx : SameRay R x z
hy : SameRay R y z
⊢ SameRay R (x + y) z
[PROOFSTEP]
rcases eq_or_ne x 0 with (rfl | hx₀)
[GOAL]
case inl
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
y z : M
hy : SameRay R y z
hx : SameRay R 0 z
⊢ SameRay R (0 + y) z
[PROOFSTEP]
rwa [zero_add]
[GOAL]
case inr
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
⊢ SameRay R (x + y) z
[PROOFSTEP]
rcases eq_or_ne y 0 with (rfl | hy₀)
[GOAL]
case inr.inl
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x z : M
hx : SameRay R x z
hx₀ : x ≠ 0
hy : SameRay R 0 z
⊢ SameRay R (x + 0) z
[PROOFSTEP]
rwa [add_zero]
[GOAL]
case inr.inr
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ SameRay R (x + y) z
[PROOFSTEP]
rcases eq_or_ne z 0 with (rfl | hz₀)
[GOAL]
case inr.inr.inl
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y : M
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hx : SameRay R x 0
hy : SameRay R y 0
⊢ SameRay R (x + y) 0
[PROOFSTEP]
apply zero_right
[GOAL]
case inr.inr.inr
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
⊢ SameRay R (x + y) z
[PROOFSTEP]
rcases hx.exists_pos hx₀ hz₀ with ⟨rx, rz₁, hrx, hrz₁, Hx⟩
[GOAL]
case inr.inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
rx rz₁ : R
hrx : 0 < rx
hrz₁ : 0 < rz₁
Hx : rx • x = rz₁ • z
⊢ SameRay R (x + y) z
[PROOFSTEP]
rcases hy.exists_pos hy₀ hz₀ with ⟨ry, rz₂, hry, hrz₂, Hy⟩
[GOAL]
case inr.inr.inr.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
rx rz₁ : R
hrx : 0 < rx
hrz₁ : 0 < rz₁
Hx : rx • x = rz₁ • z
ry rz₂ : R
hry : 0 < ry
hrz₂ : 0 < rz₂
Hy : ry • y = rz₂ • z
⊢ SameRay R (x + y) z
[PROOFSTEP]
refine' Or.inr (Or.inr ⟨rx * ry, ry * rz₁ + rx * rz₂, mul_pos hrx hry, _, _⟩)
[GOAL]
case inr.inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
rx rz₁ : R
hrx : 0 < rx
hrz₁ : 0 < rz₁
Hx : rx • x = rz₁ • z
ry rz₂ : R
hry : 0 < ry
hrz₂ : 0 < rz₂
Hy : ry • y = rz₂ • z
⊢ 0 < ry * rz₁ + rx * rz₂
[PROOFSTEP]
apply_rules [add_pos, mul_pos]
[GOAL]
case inr.inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
rx rz₁ : R
hrx : 0 < rx
hrz₁ : 0 < rz₁
Hx : rx • x = rz₁ • z
ry rz₂ : R
hry : 0 < ry
hrz₂ : 0 < rz₂
Hy : ry • y = rz₂ • z
⊢ (rx * ry) • (x + y) = (ry * rz₁ + rx * rz₂) • z
[PROOFSTEP]
simp only [mul_smul, smul_add, add_smul, ← Hx, ← Hy]
[GOAL]
case inr.inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
rx rz₁ : R
hrx : 0 < rx
hrz₁ : 0 < rz₁
Hx : rx • x = rz₁ • z
ry rz₂ : R
hry : 0 < ry
hrz₂ : 0 < rz₂
Hy : ry • y = rz₂ • z
⊢ rx • ry • x + rx • ry • y = ry • rx • x + rx • ry • y
[PROOFSTEP]
rw [smul_comm]
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
⊢ ∀ {x y z : RayVector R M}, SameRay R ↑x ↑y → SameRay R ↑y ↑z → SameRay R ↑x ↑z
[PROOFSTEP]
intros x y z hxy hyz
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : RayVector R M
hxy : SameRay R ↑x ↑y
hyz : SameRay R ↑y ↑z
⊢ SameRay R ↑x ↑z
[PROOFSTEP]
exact hxy.trans hyz fun hy => (y.2 hy).elim
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
u : Rˣ
hu : 0 < ↑u
v : Ray R M
⊢ u • v = v
[PROOFSTEP]
induction v using Module.Ray.ind
[GOAL]
case h
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
u : Rˣ
hu : 0 < ↑u
v✝ : M
hv✝ : v✝ ≠ 0
⊢ u • rayOfNeZero R v✝ hv✝ = rayOfNeZero R v✝ hv✝
[PROOFSTEP]
rw [smul_rayOfNeZero, ray_eq_iff]
[GOAL]
case h
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
u : Rˣ
hu : 0 < ↑u
v✝ : M
hv✝ : v✝ ≠ 0
⊢ SameRay R (u • v✝) v✝
[PROOFSTEP]
exact SameRay.sameRay_pos_smul_left _ hu
[GOAL]
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M
⊢ SameRay R (-x) (-y) ↔ SameRay R x y
[PROOFSTEP]
simp only [SameRay, neg_eq_zero, smul_neg, neg_inj]
[GOAL]
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M
⊢ SameRay R (-x) y ↔ SameRay R x (-y)
[PROOFSTEP]
rw [← sameRay_neg_iff, neg_neg]
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
h : SameRay R x (r • x)
⊢ x = 0
[PROOFSTEP]
rcases h with (rfl | h₀ | ⟨r₁, r₂, hr₁, hr₂, h⟩)
[GOAL]
case inl
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
y : M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
⊢ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case inr.inl
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
h₀ : r • x = 0
⊢ x = 0
[PROOFSTEP]
simpa [hr.ne] using h₀
[GOAL]
case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x = r₂ • r • x
⊢ x = 0
[PROOFSTEP]
rw [← sub_eq_zero, smul_smul, ← sub_smul, smul_eq_zero] at h 
[GOAL]
case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h✝ : r₁ • x = r₂ • r • x
h : r₁ - r₂ * r = 0 ∨ x = 0
⊢ x = 0
[PROOFSTEP]
refine' h.resolve_left (ne_of_gt <| sub_pos.2 _)
[GOAL]
case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : r < 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h✝ : r₁ • x = r₂ • r • x
h : r₁ - r₂ * r = 0 ∨ x = 0
⊢ r₂ * r < r₁
[PROOFSTEP]
exact (mul_neg_of_pos_of_neg hr₂ hr).trans hr₁
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
h : SameRay R x (-x)
⊢ x = 0
[PROOFSTEP]
nontriviality M
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
h : SameRay R x (-x)
✝ : Nontrivial M
⊢ x = 0
[PROOFSTEP]
haveI : Nontrivial R := Module.nontrivial R M
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
h : SameRay R x (-x)
✝ : Nontrivial M
this : Nontrivial R
⊢ x = 0
[PROOFSTEP]
refine' eq_zero_of_sameRay_neg_smul_right (neg_lt_zero.2 (zero_lt_one' R)) _
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
h : SameRay R x (-x)
✝ : Nontrivial M
this : Nontrivial R
⊢ SameRay R x (-1 • x)
[PROOFSTEP]
rwa [neg_one_smul]
[GOAL]
R✝ : Type u_1
inst✝⁴ : StrictOrderedCommRing R✝
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R✝ M
inst✝ : Module R✝ N
x y : M
R : Type u_4
v : RayVector R M
⊢ - -v = v
[PROOFSTEP]
rw [Subtype.ext_iff, coe_neg, coe_neg, neg_neg]
[GOAL]
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ y : M
x : Ray R M
⊢ - -x = x
[PROOFSTEP]
apply ind R (by simp) x
[GOAL]
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ y : M
x : Ray R M
⊢ ∀ (v : M) (hv : v ≠ 0), - -rayOfNeZero R v hv = rayOfNeZero R v hv
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x✝ y : M
inst✝ : NoZeroSMulDivisors R M
x : Ray R M
⊢ x ≠ -x
[PROOFSTEP]
induction' x using Module.Ray.ind with x hx
[GOAL]
case h
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x✝ y : M
inst✝ : NoZeroSMulDivisors R M
x : M
hx : x ≠ 0
⊢ rayOfNeZero R x hx ≠ -rayOfNeZero R x hx
[PROOFSTEP]
rw [neg_rayOfNeZero, Ne.def, ray_eq_iff]
[GOAL]
case h
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x✝ y : M
inst✝ : NoZeroSMulDivisors R M
x : M
hx : x ≠ 0
⊢ ¬SameRay R x (-x)
[PROOFSTEP]
exact mt eq_zero_of_sameRay_self_neg hx
[GOAL]
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M
u : Rˣ
v : Ray R M
⊢ -u • v = -(u • v)
[PROOFSTEP]
induction v using Module.Ray.ind
[GOAL]
case h
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M
u : Rˣ
v✝ : M
hv✝ : v✝ ≠ 0
⊢ -u • rayOfNeZero R v✝ hv✝ = -(u • rayOfNeZero R v✝ hv✝)
[PROOFSTEP]
simp only [smul_rayOfNeZero, Units.smul_def, Units.val_neg, neg_smul, neg_rayOfNeZero]
[GOAL]
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M
u : Rˣ
hu : ↑u < 0
v : Ray R M
⊢ u • v = -v
[PROOFSTEP]
rw [← neg_inj, neg_neg, ← neg_units_smul, units_smul_of_pos]
[GOAL]
case hu
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M
u : Rˣ
hu : ↑u < 0
v : Ray R M
⊢ 0 < ↑(-u)
[PROOFSTEP]
rwa [Units.val_neg, Right.neg_pos_iff]
[GOAL]
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M
f : M ≃ₗ[R] N
v : Ray R M
⊢ ↑(map f) (-v) = -↑(map f) v
[PROOFSTEP]
induction' v using Module.Ray.ind with g hg
[GOAL]
case h
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M
f : M ≃ₗ[R] N
g : M
hg : g ≠ 0
⊢ ↑(map f) (-rayOfNeZero R g hg) = -↑(map f) (rayOfNeZero R g hg)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝² : LinearOrderedCommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₁ v₂ : M
h : v₁ ∈ MulAction.orbit { x // x ∈ Units.posSubgroup R } v₂
⊢ SameRay R v₁ v₂
[PROOFSTEP]
rcases h with ⟨⟨r, hr : 0 < r.1⟩, rfl : r • v₂ = v₁⟩
[GOAL]
case intro.mk
R : Type u_1
inst✝² : LinearOrderedCommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₂ : M
r : Rˣ
hr : 0 < ↑r
⊢ SameRay R (r • v₂) v₂
[PROOFSTEP]
exact SameRay.sameRay_pos_smul_left _ hr
[GOAL]
R : Type u_1
inst✝² : LinearOrderedCommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
u : Rˣ
v : Module.Ray R M
this : 0 < ↑u * ↑u
⊢ 0 < ↑(u * u)
[PROOFSTEP]
exact this
[GOAL]
R : Type u_1
inst✝² : LinearOrderedCommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
u : Rˣ
v : Module.Ray R M
this : 0 < ↑u * ↑u
⊢ (u * u) • u⁻¹ • v = u • v
[PROOFSTEP]
rw [mul_smul, smul_inv_smul]
[GOAL]
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
v : M
hv : v ≠ 0
r : R
hr : r ≠ 0
⊢ SameRay R v (r • v) ↔ 0 < r
[PROOFSTEP]
simp only [sameRay_smul_right_iff, hv, or_false_iff, hr.symm.le_iff_lt]
[GOAL]
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
v : M
r : R
⊢ SameRay R (-v) (r • v) ↔ r ≤ 0 ∨ v = 0
[PROOFSTEP]
rw [← sameRay_neg_iff, neg_neg, ← neg_smul, sameRay_smul_right_iff, neg_nonneg]
[GOAL]
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
v : M
r : R
hv : v ≠ 0
hr : r ≠ 0
⊢ SameRay R (-v) (r • v) ↔ r < 0
[PROOFSTEP]
simp only [sameRay_neg_smul_right_iff, hv, or_false_iff, hr.le_iff_lt]
[GOAL]
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
u : Rˣ
v : Module.Ray R M
⊢ u • v = v ↔ 0 < ↑u
[PROOFSTEP]
induction' v using Module.Ray.ind with v hv
[GOAL]
case h
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
u : Rˣ
v : M
hv : v ≠ 0
⊢ u • rayOfNeZero R v hv = rayOfNeZero R v hv ↔ 0 < ↑u
[PROOFSTEP]
simp only [smul_rayOfNeZero, ray_eq_iff, Units.smul_def, sameRay_smul_left_iff_of_ne hv u.ne_zero]
[GOAL]
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
u : Rˣ
v : Module.Ray R M
⊢ u • v = -v ↔ ↑u < 0
[PROOFSTEP]
rw [← neg_inj, neg_neg, ← Module.Ray.neg_units_smul, units_smul_eq_self_iff, Units.val_neg, neg_pos]
[GOAL]
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
⊢ SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : x = 0
⊢ SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
[PROOFSTEP]
simpa [hx] using fun h : LinearIndependent R ![0, y] => h.ne_zero 0 rfl
[GOAL]
case neg
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
⊢ SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
[PROOFSTEP]
by_cases hy : y = 0
[GOAL]
case pos
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : y = 0
⊢ SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
[PROOFSTEP]
simpa [hy] using fun h : LinearIndependent R ![x, 0] => h.ne_zero 1 rfl
[GOAL]
case neg
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
⊢ SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
[PROOFSTEP]
simp_rw [Fintype.not_linearIndependent_iff]
[GOAL]
case neg
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
⊢ SameRay R x y ∨ SameRay R x (-y) ↔
    ∃ g, ∑ i : Fin (Nat.succ (Nat.succ 0)), g i • Matrix.vecCons x ![y] i = 0 ∧ ∃ i, g i ≠ 0
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case neg.refine'_1
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
h : SameRay R x y ∨ SameRay R x (-y)
⊢ ∃ g, ∑ i : Fin (Nat.succ (Nat.succ 0)), g i • Matrix.vecCons x ![y] i = 0 ∧ ∃ i, g i ≠ 0
[PROOFSTEP]
rcases h with ((hx0 | hy0 | ⟨r₁, r₂, hr₁, _, h⟩) | (hx0 | hy0 | ⟨r₁, r₂, hr₁, _, h⟩))
[GOAL]
case neg.refine'_1.inl.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hx0 : x = 0
⊢ ∃ g, ∑ i : Fin (Nat.succ (Nat.succ 0)), g i • Matrix.vecCons x ![y] i = 0 ∧ ∃ i, g i ≠ 0
[PROOFSTEP]
exact False.elim (hx hx0)
[GOAL]
case neg.refine'_1.inl.inr.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hy0 : y = 0
⊢ ∃ g, ∑ i : Fin (Nat.succ (Nat.succ 0)), g i • Matrix.vecCons x ![y] i = 0 ∧ ∃ i, g i ≠ 0
[PROOFSTEP]
exact False.elim (hy hy0)
[GOAL]
case neg.refine'_1.inl.inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
r₁ r₂ : R
hr₁ : 0 < r₁
left✝ : 0 < r₂
h : r₁ • x = r₂ • y
⊢ ∃ g, ∑ i : Fin (Nat.succ (Nat.succ 0)), g i • Matrix.vecCons x ![y] i = 0 ∧ ∃ i, g i ≠ 0
[PROOFSTEP]
refine' ⟨![r₁, -r₂], _⟩
[GOAL]
case neg.refine'_1.inl.inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
r₁ r₂ : R
hr₁ : 0 < r₁
left✝ : 0 < r₂
h : r₁ • x = r₂ • y
⊢ ∑ i : Fin (Nat.succ (Nat.succ 0)), Matrix.vecCons r₁ ![-r₂] i • Matrix.vecCons x ![y] i = 0 ∧
    ∃ i, Matrix.vecCons r₁ ![-r₂] i ≠ 0
[PROOFSTEP]
rw [Fin.sum_univ_two, Fin.exists_fin_two]
[GOAL]
case neg.refine'_1.inl.inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
r₁ r₂ : R
hr₁ : 0 < r₁
left✝ : 0 < r₂
h : r₁ • x = r₂ • y
⊢ Matrix.vecCons r₁ ![-r₂] 0 • Matrix.vecCons x ![y] 0 + Matrix.vecCons r₁ ![-r₂] 1 • Matrix.vecCons x ![y] 1 = 0 ∧
    (Matrix.vecCons r₁ ![-r₂] 0 ≠ 0 ∨ Matrix.vecCons r₁ ![-r₂] 1 ≠ 0)
[PROOFSTEP]
simp [h, hr₁.ne.symm]
[GOAL]
case neg.refine'_1.inr.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hx0 : x = 0
⊢ ∃ g, ∑ i : Fin (Nat.succ (Nat.succ 0)), g i • Matrix.vecCons x ![y] i = 0 ∧ ∃ i, g i ≠ 0
[PROOFSTEP]
exact False.elim (hx hx0)
[GOAL]
case neg.refine'_1.inr.inr.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
hy0 : -y = 0
⊢ ∃ g, ∑ i : Fin (Nat.succ (Nat.succ 0)), g i • Matrix.vecCons x ![y] i = 0 ∧ ∃ i, g i ≠ 0
[PROOFSTEP]
exact False.elim (hy (neg_eq_zero.1 hy0))
[GOAL]
case neg.refine'_1.inr.inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
r₁ r₂ : R
hr₁ : 0 < r₁
left✝ : 0 < r₂
h : r₁ • x = r₂ • -y
⊢ ∃ g, ∑ i : Fin (Nat.succ (Nat.succ 0)), g i • Matrix.vecCons x ![y] i = 0 ∧ ∃ i, g i ≠ 0
[PROOFSTEP]
refine' ⟨![r₁, r₂], _⟩
[GOAL]
case neg.refine'_1.inr.inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
r₁ r₂ : R
hr₁ : 0 < r₁
left✝ : 0 < r₂
h : r₁ • x = r₂ • -y
⊢ ∑ i : Fin (Nat.succ (Nat.succ 0)), Matrix.vecCons r₁ ![r₂] i • Matrix.vecCons x ![y] i = 0 ∧
    ∃ i, Matrix.vecCons r₁ ![r₂] i ≠ 0
[PROOFSTEP]
rw [Fin.sum_univ_two, Fin.exists_fin_two]
[GOAL]
case neg.refine'_1.inr.inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
r₁ r₂ : R
hr₁ : 0 < r₁
left✝ : 0 < r₂
h : r₁ • x = r₂ • -y
⊢ Matrix.vecCons r₁ ![r₂] 0 • Matrix.vecCons x ![y] 0 + Matrix.vecCons r₁ ![r₂] 1 • Matrix.vecCons x ![y] 1 = 0 ∧
    (Matrix.vecCons r₁ ![r₂] 0 ≠ 0 ∨ Matrix.vecCons r₁ ![r₂] 1 ≠ 0)
[PROOFSTEP]
simp [h, hr₁.ne.symm]
[GOAL]
case neg.refine'_2
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
h : ∃ g, ∑ i : Fin (Nat.succ (Nat.succ 0)), g i • Matrix.vecCons x ![y] i = 0 ∧ ∃ i, g i ≠ 0
⊢ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
rcases h with ⟨m, hm, hmne⟩
[GOAL]
case neg.refine'_2.intro.intro
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : ∑ i : Fin (Nat.succ (Nat.succ 0)), m i • Matrix.vecCons x ![y] i = 0
hmne : ∃ i, m i ≠ 0
⊢ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
rw [Fin.sum_univ_two, add_eq_zero_iff_eq_neg, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons] at hm 
[GOAL]
case neg.refine'_2.intro.intro
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
⊢ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
rcases lt_trichotomy (m 0) 0 with (hm0 | hm0 | hm0)
[GOAL]
case neg.refine'_2.intro.intro.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 < 0
⊢ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
rcases lt_trichotomy (m 1) 0 with (hm1 | hm1 | hm1)
[GOAL]
case neg.refine'_2.intro.intro.inr.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 = 0
⊢ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
rcases lt_trichotomy (m 1) 0 with (hm1 | hm1 | hm1)
[GOAL]
case neg.refine'_2.intro.intro.inr.inr
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
⊢ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
rcases lt_trichotomy (m 1) 0 with (hm1 | hm1 | hm1)
[GOAL]
case neg.refine'_2.intro.intro.inl.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 < 0
hm1 : m 1 < 0
⊢ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
refine' Or.inr (Or.inr (Or.inr ⟨-m 0, -m 1, Left.neg_pos_iff.2 hm0, Left.neg_pos_iff.2 hm1, _⟩))
[GOAL]
case neg.refine'_2.intro.intro.inl.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 < 0
hm1 : m 1 < 0
⊢ -m 0 • x = -m 1 • -y
[PROOFSTEP]
rw [neg_smul_neg, neg_smul, hm, neg_neg]
[GOAL]
case neg.refine'_2.intro.intro.inl.inr.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 < 0
hm1 : m 1 = 0
⊢ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
exfalso
[GOAL]
case neg.refine'_2.intro.intro.inl.inr.inl.h
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 < 0
hm1 : m 1 = 0
⊢ False
[PROOFSTEP]
simp [hm1, hx, hm0.ne] at hm 
[GOAL]
case neg.refine'_2.intro.intro.inl.inr.inr
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 < 0
hm1 : 0 < m 1
⊢ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
refine' Or.inl (Or.inr (Or.inr ⟨-m 0, m 1, Left.neg_pos_iff.2 hm0, hm1, _⟩))
[GOAL]
case neg.refine'_2.intro.intro.inl.inr.inr
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 < 0
hm1 : 0 < m 1
⊢ -m 0 • x = m 1 • y
[PROOFSTEP]
rw [neg_smul, hm, neg_neg]
[GOAL]
case neg.refine'_2.intro.intro.inr.inl.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 = 0
hm1 : m 1 < 0
⊢ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
exfalso
[GOAL]
case neg.refine'_2.intro.intro.inr.inl.inl.h
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 = 0
hm1 : m 1 < 0
⊢ False
[PROOFSTEP]
simp [hm0, hy, hm1.ne] at hm 
[GOAL]
case neg.refine'_2.intro.intro.inr.inl.inr.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 = 0
hm1 : m 1 = 0
⊢ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
rw [Fin.exists_fin_two] at hmne 
[GOAL]
case neg.refine'_2.intro.intro.inr.inl.inr.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : m 0 ≠ 0 ∨ m 1 ≠ 0
hm0 : m 0 = 0
hm1 : m 1 = 0
⊢ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
exact False.elim (not_and_or.2 hmne ⟨hm0, hm1⟩)
[GOAL]
case neg.refine'_2.intro.intro.inr.inl.inr.inr
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 = 0
hm1 : 0 < m 1
⊢ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
exfalso
[GOAL]
case neg.refine'_2.intro.intro.inr.inl.inr.inr.h
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 = 0
hm1 : 0 < m 1
⊢ False
[PROOFSTEP]
simp [hm0, hy, hm1.ne.symm] at hm 
[GOAL]
case neg.refine'_2.intro.intro.inr.inr.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : m 1 < 0
⊢ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
refine' Or.inl (Or.inr (Or.inr ⟨m 0, -m 1, hm0, Left.neg_pos_iff.2 hm1, _⟩))
[GOAL]
case neg.refine'_2.intro.intro.inr.inr.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : m 1 < 0
⊢ m 0 • x = -m 1 • y
[PROOFSTEP]
rwa [neg_smul]
[GOAL]
case neg.refine'_2.intro.intro.inr.inr.inr.inl
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : m 1 = 0
⊢ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
exfalso
[GOAL]
case neg.refine'_2.intro.intro.inr.inr.inr.inl.h
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : m 1 = 0
⊢ False
[PROOFSTEP]
simp [hm1, hx, hm0.ne.symm] at hm 
[GOAL]
case neg.refine'_2.intro.intro.inr.inr.inr.inr
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : 0 < m 1
⊢ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
refine' Or.inr (Or.inr (Or.inr ⟨m 0, m 1, hm0, hm1, _⟩))
[GOAL]
case neg.refine'_2.intro.intro.inr.inr.inr.inr
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ (Nat.succ 0)) → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : 0 < m 1
⊢ m 0 • x = m 1 • -y
[PROOFSTEP]
rwa [smul_neg]
[GOAL]
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
⊢ SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
[PROOFSTEP]
rw [← sameRay_or_sameRay_neg_iff_not_linearIndependent]
[GOAL]
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
⊢ SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : x = 0
⊢ SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
simp [hx]
[GOAL]
case neg
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
⊢ SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
by_cases hy : y = 0
[GOAL]
case pos
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : y = 0
⊢ SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
simp [hx, hy]
[GOAL]
case neg
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
⊢ SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ SameRay R x y ∨ SameRay R x (-y)
[PROOFSTEP]
simp [hx, hy]
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y v₁ v₂ : M
h✝ : SameRay R x y
hx : x ≠ 0
hy : y ≠ 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x = r₂ • y
⊢ (r₂⁻¹ * r₁) • x = y
[PROOFSTEP]
rw [mul_smul, h, inv_smul_smul₀ hr₂.ne']
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y v₁ v₂ : M
h : SameRay R x y
hx : x ≠ 0
⊢ ∃ r, 0 ≤ r ∧ r • x = y
[PROOFSTEP]
obtain rfl | hy := eq_or_ne y 0
[GOAL]
case inl
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x v₁ v₂ : M
hx : x ≠ 0
h : SameRay R x 0
⊢ ∃ r, 0 ≤ r ∧ r • x = 0
[PROOFSTEP]
exact ⟨0, le_rfl, zero_smul _ _⟩
[GOAL]
case inr
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y v₁ v₂ : M
h : SameRay R x y
hx : x ≠ 0
hy : y ≠ 0
⊢ ∃ r, 0 ≤ r ∧ r • x = y
[PROOFSTEP]
exact (h.exists_pos_left hx hy).imp fun _ => And.imp_left le_of_lt
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y v₁ v₂ : M
h : SameRay R v₁ v₂
⊢ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • (v₁ + v₂) ∧ v₂ = b • (v₁ + v₂)
[PROOFSTEP]
rcases h with (rfl | rfl | ⟨r₁, r₂, h₁, h₂, H⟩)
[GOAL]
case inl
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y v₂ : M
⊢ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ 0 = a • (0 + v₂) ∧ v₂ = b • (0 + v₂)
[PROOFSTEP]
use 0, 1
[GOAL]
case h
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y v₂ : M
⊢ 0 ≤ 0 ∧ 0 ≤ 1 ∧ 0 + 1 = 1 ∧ 0 = 0 • (0 + v₂) ∧ v₂ = 1 • (0 + v₂)
[PROOFSTEP]
simp
[GOAL]
case inr.inl
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y v₁ : M
⊢ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • (v₁ + 0) ∧ 0 = b • (v₁ + 0)
[PROOFSTEP]
use 1, 0
[GOAL]
case h
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y v₁ : M
⊢ 0 ≤ 1 ∧ 0 ≤ 0 ∧ 1 + 0 = 1 ∧ v₁ = 1 • (v₁ + 0) ∧ 0 = 0 • (v₁ + 0)
[PROOFSTEP]
simp
[GOAL]
case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y v₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
⊢ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • (v₁ + v₂) ∧ v₂ = b • (v₁ + v₂)
[PROOFSTEP]
have h₁₂ : 0 < r₁ + r₂ := add_pos h₁ h₂
[GOAL]
case inr.inr.intro.intro.intro.intro
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y v₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
⊢ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • (v₁ + v₂) ∧ v₂ = b • (v₁ + v₂)
[PROOFSTEP]
refine' ⟨r₂ / (r₁ + r₂), r₁ / (r₁ + r₂), div_nonneg h₂.le h₁₂.le, div_nonneg h₁.le h₁₂.le, _, _, _⟩
[GOAL]
case inr.inr.intro.intro.intro.intro.refine'_1
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y v₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
⊢ r₂ / (r₁ + r₂) + r₁ / (r₁ + r₂) = 1
[PROOFSTEP]
rw [← add_div, add_comm, div_self h₁₂.ne']
[GOAL]
case inr.inr.intro.intro.intro.intro.refine'_2
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y v₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
⊢ v₁ = (r₂ / (r₁ + r₂)) • (v₁ + v₂)
[PROOFSTEP]
rw [div_eq_inv_mul, mul_smul, smul_add, ← H, ← add_smul, add_comm r₂, inv_smul_smul₀ h₁₂.ne']
[GOAL]
case inr.inr.intro.intro.intro.intro.refine'_3
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y v₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
⊢ v₂ = (r₁ / (r₁ + r₂)) • (v₁ + v₂)
[PROOFSTEP]
rw [div_eq_inv_mul, mul_smul, smul_add, H, ← add_smul, add_comm r₂, inv_smul_smul₀ h₁₂.ne']
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ r • x = y) ↔ SameRay R x y
[PROOFSTEP]
refine' ⟨fun h => _, fun h => h.exists_pos_left hx hy⟩
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
h : ∃ r, 0 < r ∧ r • x = y
⊢ SameRay R x y
[PROOFSTEP]
rcases h with ⟨r, hr, rfl⟩
[GOAL]
case intro.intro
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
hx : x ≠ 0
r : R
hr : 0 < r
hy : r • x ≠ 0
⊢ SameRay R x (r • x)
[PROOFSTEP]
exact SameRay.sameRay_pos_smul_right x hr
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
⊢ (∃ r, 0 < r ∧ r • x = y) ↔ SameRay R x y ∧ y ≠ 0
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
⊢ (∃ r, 0 < r ∧ r • x = y) → SameRay R x y ∧ y ≠ 0
[PROOFSTEP]
rintro ⟨r, hr, rfl⟩
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
hx : x ≠ 0
r : R
hr : 0 < r
⊢ SameRay R x (r • x) ∧ r • x ≠ 0
[PROOFSTEP]
simp [hx, hr.le, hr.ne']
[GOAL]
case mpr
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
⊢ SameRay R x y ∧ y ≠ 0 → ∃ r, 0 < r ∧ r • x = y
[PROOFSTEP]
rintro ⟨hxy, hy⟩
[GOAL]
case mpr.intro
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hxy : SameRay R x y
hy : y ≠ 0
⊢ ∃ r, 0 < r ∧ r • x = y
[PROOFSTEP]
exact (exists_pos_left_iff_sameRay hx hy).2 hxy
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
⊢ (∃ r, 0 ≤ r ∧ r • x = y) ↔ SameRay R x y
[PROOFSTEP]
refine' ⟨fun h => _, fun h => h.exists_nonneg_left hx⟩
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
h : ∃ r, 0 ≤ r ∧ r • x = y
⊢ SameRay R x y
[PROOFSTEP]
rcases h with ⟨r, hr, rfl⟩
[GOAL]
case intro.intro
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
hx : x ≠ 0
r : R
hr : 0 ≤ r
⊢ SameRay R x (r • x)
[PROOFSTEP]
exact SameRay.sameRay_nonneg_smul_right x hr
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ x = r • y) ↔ SameRay R x y
[PROOFSTEP]
rw [SameRay.sameRay_comm]
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ x = r • y) ↔ SameRay R y x
[PROOFSTEP]
simp_rw [eq_comm (a := x)]
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ r • y = x) ↔ SameRay R y x
[PROOFSTEP]
exact exists_pos_left_iff_sameRay hy hx
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ x = r • y) ↔ SameRay R x y ∧ x ≠ 0
[PROOFSTEP]
rw [SameRay.sameRay_comm]
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ x = r • y) ↔ SameRay R y x ∧ x ≠ 0
[PROOFSTEP]
simp_rw [eq_comm (a := x)]
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ r • y = x) ↔ SameRay R y x ∧ x ≠ 0
[PROOFSTEP]
exact exists_pos_left_iff_sameRay_and_ne_zero hy
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ r, 0 ≤ r ∧ x = r • y) ↔ SameRay R x y
[PROOFSTEP]
rw [SameRay.sameRay_comm]
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ r, 0 ≤ r ∧ x = r • y) ↔ SameRay R y x
[PROOFSTEP]
simp_rw [eq_comm (a := x)]
[GOAL]
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ r, 0 ≤ r ∧ r • y = x) ↔ SameRay R y x
[PROOFSTEP]
exact exists_nonneg_left_iff_sameRay (R := R) hy
