-- Mathlib/LinearAlgebra/Ray.lean
theorem add_left (hx : SameRay R x z) (hy : SameRay R y z) : SameRay R (x + y) z

Proof state:
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
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

Tactic:
convert congr(ry • $Hx + rx • $Hy) using 1 <;> module

Result:
no goals

Proof state:
R : Type u_1
inst✝² : StrictOrderedCommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hx : SameRay R x z
hy : SameRay R y z
⊢ SameRay R (x + y) z

Tactic:
rcases eq_or_ne x 0 with (rfl | hx₀)

Result:
case inl
R : Type u_1
inst✝² : StrictOrderedCommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
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
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
⊢ SameRay R (x + y) z

Proof state:
case inr.inr
R : Type u_1
inst✝² : StrictOrderedCommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
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

Tactic:
rcases eq_or_ne z 0 with (rfl | hz₀)

Result:
case inr.inr.inl
R : Type u_1
inst✝² : StrictOrderedCommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
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
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

Proof state:
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
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

Tactic:
rcases hy.exists_pos hy₀ hz₀ with ⟨ry, rz₂, hry, hrz₂, Hy⟩

Result:
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
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

Proof state:
case inr.inr.inr
R : Type u_1
inst✝² : StrictOrderedCommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
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

Tactic:
rcases hx.exists_pos hx₀ hz₀ with ⟨rx, rz₁, hrx, hrz₁, Hx⟩

Result:
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
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

Proof state:
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
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

Tactic:
refine Or.inr (Or.inr ⟨rx * ry, ry * rz₁ + rx * rz₂, mul_pos hrx hry, ?_, ?_⟩)

Result:
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
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
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

Proof state:
case inl
R : Type u_1
inst✝² : StrictOrderedCommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
y z : M
hy : SameRay R y z
hx : SameRay R 0 z
⊢ SameRay R (0 + y) z

Tactic:
rwa [zero_add]

Result:
no goals

Proof state:
case inr
R : Type u_1
inst✝² : StrictOrderedCommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
⊢ SameRay R (x + y) z

Tactic:
rcases eq_or_ne y 0 with (rfl | hy₀)

Result:
case inr.inl
R : Type u_1
inst✝² : StrictOrderedCommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
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
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

Proof state:
case inr.inl
R : Type u_1
inst✝² : StrictOrderedCommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x z : M
hx : SameRay R x z
hx₀ : x ≠ 0
hy : SameRay R 0 z
⊢ SameRay R (x + 0) z

Tactic:
rwa [add_zero]

Result:
no goals

Proof state:
case inr.inr.inl
R : Type u_1
inst✝² : StrictOrderedCommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hx : SameRay R x 0
hy : SameRay R y 0
⊢ SameRay R (x + y) 0

Tactic:
apply zero_right

Result:
no goals

Proof state:
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
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₂

Tactic:
positivity

Result:
no goals