case intro
k : Type u_2
M : Type u_1
N : Type ?u.53981
inst✝⁴ : OrderedRing k
inst✝³ : OrderedAddCommGroup M
inst✝² : Module k M
inst✝¹ : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a : k
c d : M
hcd : c ≤ d
b : k
hab : a ≤ a + b
⊢ a • d + (a + b) • c ≤ a • c + (a + b) • d
k : Type u_2
M : Type u_1
N : Type ?u.53981
inst✝⁴ : OrderedRing k
inst✝³ : OrderedAddCommGroup M
inst✝² : Module k M
inst✝¹ : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : k
c d : M
hab : a ≤ b
hcd : c ≤ d
⊢ a • d + b • c ≤ a • c + b • d
obtain ⟨b, rfl⟩ := exists_add_of_le hab
case intro.intro
k : Type u_2
M : Type u_1
N : Type ?u.53981
inst✝⁴ : OrderedRing k
inst✝³ : OrderedAddCommGroup M
inst✝² : Module k M
inst✝¹ : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a : k
c : M
b : k
hab : a ≤ a + b
d : M
hcd : c ≤ c + d
⊢ a • (c + d) + (a + b) • c ≤ a • c + (a + b) • (c + d)
case intro
k : Type u_2
M : Type u_1
N : Type ?u.53981
inst✝⁴ : OrderedRing k
inst✝³ : OrderedAddCommGroup M
inst✝² : Module k M
inst✝¹ : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a : k
c d : M
hcd : c ≤ d
b : k
hab : a ≤ a + b
⊢ a • d + (a + b) • c ≤ a • c + (a + b) • d
obtain ⟨d, rfl⟩ := exists_add_of_le hcd
case intro.intro
k : Type u_2
M : Type u_1
N : Type ?u.53981
inst✝⁴ : OrderedRing k
inst✝³ : OrderedAddCommGroup M
inst✝² : Module k M
inst✝¹ : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a : k
c : M
b : k
hab : a ≤ a + b
d : M
hcd : c ≤ c + d
⊢ a • c + (a + b) • c + a • d ≤ a • c + (a + b) • c + (a • d + b • d)
case intro.intro
k : Type u_2
M : Type u_1
N : Type ?u.53981
inst✝⁴ : OrderedRing k
inst✝³ : OrderedAddCommGroup M
inst✝² : Module k M
inst✝¹ : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a : k
c : M
b : k
hab : a ≤ a + b
d : M
hcd : c ≤ c + d
⊢ a • (c + d) + (a + b) • c ≤ a • c + (a + b) • (c + d)
rw [smul_add, add_right_comm, smul_add, ← add_assoc, add_smul _ _ d]
case intro.intro
k : Type u_2
M : Type u_1
N : Type ?u.53981
inst✝⁴ : OrderedRing k
inst✝³ : OrderedAddCommGroup M
inst✝² : Module k M
inst✝¹ : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a : k
c : M
b : k
hab : 0 ≤ b
d : M
hcd : 0 ≤ d
⊢ a • c + (a + b) • c + a • d ≤ a • c + (a + b) • c + (a • d + b • d)
case intro.intro
k : Type u_2
M : Type u_1
N : Type ?u.53981
inst✝⁴ : OrderedRing k
inst✝³ : OrderedAddCommGroup M
inst✝² : Module k M
inst✝¹ : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a : k
c : M
b : k
hab : a ≤ a + b
d : M
hcd : c ≤ c + d
⊢ a • c + (a + b) • c + a • d ≤ a • c + (a + b) • c + (a • d + b • d)
rw [le_add_iff_nonneg_right] at hab hcd
no goals
case intro.intro
k : Type u_2
M : Type u_1
N : Type ?u.53981
inst✝⁴ : OrderedRing k
inst✝³ : OrderedAddCommGroup M
inst✝² : Module k M
inst✝¹ : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a : k
c : M
b : k
hab : 0 ≤ b
d : M
hcd : 0 ≤ d
⊢ a • c + (a + b) • c + a • d ≤ a • c + (a + b) • c + (a • d + b • d)
exact add_le_add_left (le_add_of_nonneg_right <| smul_nonneg hab hcd) _