case intro
k : Type u_2
M : Type u_1
N : Type ?u.70650
inst✝⁵ : OrderedRing k
inst✝⁴ : OrderedAddCommGroup M
inst✝³ : Module k M
inst✝² : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝¹ : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
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.70650
inst✝⁵ : OrderedRing k
inst✝⁴ : OrderedAddCommGroup M
inst✝³ : Module k M
inst✝² : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝¹ : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
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.le
case intro.intro
k : Type u_2
M : Type u_1
N : Type ?u.70650
inst✝⁵ : OrderedRing k
inst✝⁴ : OrderedAddCommGroup M
inst✝³ : Module k M
inst✝² : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝¹ : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
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.70650
inst✝⁵ : OrderedRing k
inst✝⁴ : OrderedAddCommGroup M
inst✝³ : Module k M
inst✝² : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝¹ : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
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.le
case intro.intro
k : Type u_2
M : Type u_1
N : Type ?u.70650
inst✝⁵ : OrderedRing k
inst✝⁴ : OrderedAddCommGroup M
inst✝³ : Module k M
inst✝² : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝¹ : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
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.70650
inst✝⁵ : OrderedRing k
inst✝⁴ : OrderedAddCommGroup M
inst✝³ : Module k M
inst✝² : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝¹ : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
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.70650
inst✝⁵ : OrderedRing k
inst✝⁴ : OrderedAddCommGroup M
inst✝³ : Module k M
inst✝² : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝¹ : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
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.70650
inst✝⁵ : OrderedRing k
inst✝⁴ : OrderedAddCommGroup M
inst✝³ : Module k M
inst✝² : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝¹ : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
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 [lt_add_iff_pos_right] at hab hcd
no goals
case intro.intro
k : Type u_2
M : Type u_1
N : Type ?u.70650
inst✝⁵ : OrderedRing k
inst✝⁴ : OrderedAddCommGroup M
inst✝³ : Module k M
inst✝² : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝¹ : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
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_lt_add_left (lt_add_of_pos_right _ <| smul_pos hab hcd) _