case inl
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type ?u.71755
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type ?u.71837
inst✝ : DecidableEq ι
y z : M
hy : SameRay R y z
hx : SameRay R 0 z
⊢ SameRay R (0 + y) z

case inr
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type ?u.71755
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type ?u.71837
inst✝ : DecidableEq ι
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
⊢ SameRay R (x + y) z
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type ?u.71755
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type ?u.71837
inst✝ : DecidableEq ι
x y z : M
hx : SameRay R x z
hy : SameRay R y z
⊢ SameRay R (x + y) z
rcases eq_or_ne x 0 with (rfl | hx₀)
case inr.inl
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type ?u.71755
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type ?u.71837
inst✝ : DecidableEq ι
x z : M
hx : SameRay R x z
hx₀ : x ≠ 0
hy : SameRay R 0 z
⊢ SameRay R (x + 0) z

case inr.inr
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type ?u.71755
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type ?u.71837
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
case inr
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type ?u.71755
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type ?u.71837
inst✝ : DecidableEq ι
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
⊢ SameRay R (x + y) z
rcases eq_or_ne y 0 with (rfl | hy₀)
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.71755
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type ?u.71837
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

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.71755
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type ?u.71837
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
case inr.inr
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type ?u.71755
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type ?u.71837
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
rcases eq_or_ne z 0 with (rfl | hz₀)
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.71755
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type ?u.71837
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
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.71755
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type ?u.71837
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
rcases hx.exists_pos hx₀ hz₀ with ⟨rx, rz₁, hrx, hrz₁, Hx⟩
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.71755
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type ?u.71837
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
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.71755
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type ?u.71837
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
rcases hy.exists_pos hy₀ hz₀ with ⟨ry, rz₂, hry, hrz₂, Hy⟩
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.71755
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type ?u.71837
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₂

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.71755
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type ?u.71837
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
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.71755
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type ?u.71837
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
refine' Or.inr (Or.inr ⟨rx * ry, ry * rz₁ + rx * rz₂, mul_pos hrx hry, _, _⟩)
no goals
case inl
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type ?u.71755
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type ?u.71837
inst✝ : DecidableEq ι
y z : M
hy : SameRay R y z
hx : SameRay R 0 z
⊢ SameRay R (0 + y) z
rwa [zero_add]
no goals
case inr.inl
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type ?u.71755
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type ?u.71837
inst✝ : DecidableEq ι
x z : M
hx : SameRay R x z
hx₀ : x ≠ 0
hy : SameRay R 0 z
⊢ SameRay R (x + 0) z
rwa [add_zero]
no goals
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.71755
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type ?u.71837
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
apply zero_right
no goals
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.71755
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type ?u.71837
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₂
apply_rules [add_pos, mul_pos]
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.71755
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type ?u.71837
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
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.71755
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type ?u.71837
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
simp only [mul_smul, smul_add, add_smul, ← Hx, ← Hy]
no goals
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.71755
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type ?u.71837
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
rw [smul_comm]