case inl
ι : Type ?u.20016
𝕜 : Type ?u.20019
R : Type u_2
M : Type u_1
N : Type ?u.20028
inst✝³ : OrderedSemiring R
inst✝² : OrderedAddCommMonoid M
inst✝¹ : SMulWithZero R M
inst✝ : OrderedSMul R M
s : Set M
a : M
c : R
h₂ : 0 ≤ c
h₁ : a ≤ a
⊢ c • a ≤ c • a

case inr
ι : Type ?u.20016
𝕜 : Type ?u.20019
R : Type u_2
M : Type u_1
N : Type ?u.20028
inst✝³ : OrderedSemiring R
inst✝² : OrderedAddCommMonoid M
inst✝¹ : SMulWithZero R M
inst✝ : OrderedSMul R M
s : Set M
a b : M
c : R
h₁ : a ≤ b
h₂ : 0 ≤ c
hab : a < b
⊢ c • a ≤ c • b
ι : Type ?u.20016
𝕜 : Type ?u.20019
R : Type u_2
M : Type u_1
N : Type ?u.20028
inst✝³ : OrderedSemiring R
inst✝² : OrderedAddCommMonoid M
inst✝¹ : SMulWithZero R M
inst✝ : OrderedSMul R M
s : Set M
a b : M
c : R
h₁ : a ≤ b
h₂ : 0 ≤ c
⊢ c • a ≤ c • b
rcases h₁.eq_or_lt with (rfl | hab)
no goals
case inl
ι : Type ?u.20016
𝕜 : Type ?u.20019
R : Type u_2
M : Type u_1
N : Type ?u.20028
inst✝³ : OrderedSemiring R
inst✝² : OrderedAddCommMonoid M
inst✝¹ : SMulWithZero R M
inst✝ : OrderedSMul R M
s : Set M
a : M
c : R
h₂ : 0 ≤ c
h₁ : a ≤ a
⊢ c • a ≤ c • a
rfl
case inr.inl
ι : Type ?u.20016
𝕜 : Type ?u.20019
R : Type u_2
M : Type u_1
N : Type ?u.20028
inst✝³ : OrderedSemiring R
inst✝² : OrderedAddCommMonoid M
inst✝¹ : SMulWithZero R M
inst✝ : OrderedSMul R M
s : Set M
a b : M
h₁ : a ≤ b
hab : a < b
h₂ : 0 ≤ 0
⊢ 0 • a ≤ 0 • b

case inr.inr
ι : Type ?u.20016
𝕜 : Type ?u.20019
R : Type u_2
M : Type u_1
N : Type ?u.20028
inst✝³ : OrderedSemiring R
inst✝² : OrderedAddCommMonoid M
inst✝¹ : SMulWithZero R M
inst✝ : OrderedSMul R M
s : Set M
a b : M
c : R
h₁ : a ≤ b
h₂ : 0 ≤ c
hab : a < b
hc : 0 < c
⊢ c • a ≤ c • b
case inr
ι : Type ?u.20016
𝕜 : Type ?u.20019
R : Type u_2
M : Type u_1
N : Type ?u.20028
inst✝³ : OrderedSemiring R
inst✝² : OrderedAddCommMonoid M
inst✝¹ : SMulWithZero R M
inst✝ : OrderedSMul R M
s : Set M
a b : M
c : R
h₁ : a ≤ b
h₂ : 0 ≤ c
hab : a < b
⊢ c • a ≤ c • b
rcases h₂.eq_or_lt with (rfl | hc)
no goals
case inr.inl
ι : Type ?u.20016
𝕜 : Type ?u.20019
R : Type u_2
M : Type u_1
N : Type ?u.20028
inst✝³ : OrderedSemiring R
inst✝² : OrderedAddCommMonoid M
inst✝¹ : SMulWithZero R M
inst✝ : OrderedSMul R M
s : Set M
a b : M
h₁ : a ≤ b
hab : a < b
h₂ : 0 ≤ 0
⊢ 0 • a ≤ 0 • b
rw [zero_smul, zero_smul]
no goals
case inr.inr
ι : Type ?u.20016
𝕜 : Type ?u.20019
R : Type u_2
M : Type u_1
N : Type ?u.20028
inst✝³ : OrderedSemiring R
inst✝² : OrderedAddCommMonoid M
inst✝¹ : SMulWithZero R M
inst✝ : OrderedSMul R M
s : Set M
a b : M
c : R
h₁ : a ≤ b
h₂ : 0 ≤ c
hab : a < b
hc : 0 < c
⊢ c • a ≤ c • b
exact (smul_lt_smul_of_pos hab hc).le