-- Mathlib/LinearAlgebra/Ray.lean
/-- A vector is in the same ray as a nonnegative multiple of itself. -/
lemma sameRay_nonneg_smul_right (v : M) (h : 0 ≤ a) : SameRay R v (a • v)

Proof state:
case inl
R : Type u_1
inst✝⁷ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
S : Type u_5
inst✝⁴ : OrderedCommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : SMulPosMono S R
inst✝ : IsScalarTower S R M
a : S
v : M
h✝ : 0 ≤ a
h : (algebraMap S R) a = 0
⊢ SameRay R v (a • v)

Tactic:
rw [← algebraMap_smul R a v, h, zero_smul]

Result:
case inl
R : Type u_1
inst✝⁷ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
S : Type u_5
inst✝⁴ : OrderedCommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : SMulPosMono S R
inst✝ : IsScalarTower S R M
a : S
v : M
h✝ : 0 ≤ a
h : (algebraMap S R) a = 0
⊢ SameRay R v 0

Proof state:
R : Type u_1
inst✝⁷ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
S : Type u_5
inst✝⁴ : OrderedCommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : SMulPosMono S R
inst✝ : IsScalarTower S R M
a : S
v : M
h✝ : 0 ≤ a
h : 0 < (algebraMap S R) a
⊢ 0 < 1

Tactic:
nontriviality R

Result:
R : Type u_1
inst✝⁸ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
S : Type u_5
inst✝⁵ : OrderedCommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : Module S M
inst✝² : SMulPosMono S R
inst✝¹ : IsScalarTower S R M
a : S
v : M
h✝ : 0 ≤ a
h : 0 < (algebraMap S R) a
inst✝ : Nontrivial R
⊢ 0 < 1

Proof state:
case inl
R : Type u_1
inst✝⁷ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
S : Type u_5
inst✝⁴ : OrderedCommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : SMulPosMono S R
inst✝ : IsScalarTower S R M
a : S
v : M
h✝ : 0 ≤ a
h : (algebraMap S R) a = 0
⊢ SameRay R v 0

Tactic:
exact zero_right _

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
S : Type u_5
inst✝⁴ : OrderedCommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : SMulPosMono S R
inst✝ : IsScalarTower S R M
a : S
v : M
h✝ : 0 ≤ a
h : 0 < (algebraMap S R) a
⊢ SameRay R v (a • v)

Tactic:
refine Or.inr <| Or.inr ⟨algebraMap S R a, 1, h, by nontriviality R; exact zero_lt_one, ?_⟩

Result:
case inr
R : Type u_1
inst✝⁷ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
S : Type u_5
inst✝⁴ : OrderedCommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : SMulPosMono S R
inst✝ : IsScalarTower S R M
a : S
v : M
h✝ : 0 ≤ a
h : 0 < (algebraMap S R) a
⊢ (algebraMap S R) a • v = 1 • a • v

Proof state:
R : Type u_1
inst✝⁷ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
S : Type u_5
inst✝⁴ : OrderedCommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : SMulPosMono S R
inst✝ : IsScalarTower S R M
a : S
v : M
h : 0 ≤ a
⊢ SameRay R v (a • v)

Tactic:
obtain h | h := (algebraMap_nonneg R h).eq_or_gt

Result:
case inl
R : Type u_1
inst✝⁷ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
S : Type u_5
inst✝⁴ : OrderedCommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : SMulPosMono S R
inst✝ : IsScalarTower S R M
a : S
v : M
h✝ : 0 ≤ a
h : (algebraMap S R) a = 0
⊢ SameRay R v (a • v)

case inr
R : Type u_1
inst✝⁷ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
S : Type u_5
inst✝⁴ : OrderedCommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : SMulPosMono S R
inst✝ : IsScalarTower S R M
a : S
v : M
h✝ : 0 ≤ a
h : 0 < (algebraMap S R) a
⊢ SameRay R v (a • v)

Proof state:
case inr
R : Type u_1
inst✝⁷ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
S : Type u_5
inst✝⁴ : OrderedCommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : SMulPosMono S R
inst✝ : IsScalarTower S R M
a : S
v : M
h✝ : 0 ≤ a
h : 0 < (algebraMap S R) a
⊢ (algebraMap S R) a • v = 1 • a • v

Tactic:
module

Result:
no goals

Proof state:
R : Type u_1
inst✝⁸ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
S : Type u_5
inst✝⁵ : OrderedCommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : Module S M
inst✝² : SMulPosMono S R
inst✝¹ : IsScalarTower S R M
a : S
v : M
h✝ : 0 ≤ a
h : 0 < (algebraMap S R) a
inst✝ : Nontrivial R
⊢ 0 < 1

Tactic:
exact zero_lt_one

Result:
no goals