case intro
α : Type u
β : Type ?u.10176
inst✝¹ : StrictOrderedSemiring α
a c d : α
inst✝ : ExistsAddOfLE α
hcd : c < d
b : α
hab : a < a + b
⊢ a * d + (a + b) * c < a * c + (a + b) * d
α : Type u
β : Type ?u.10176
inst✝¹ : StrictOrderedSemiring α
a b c d : α
inst✝ : ExistsAddOfLE α
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
α : Type u
β : Type ?u.10176
inst✝¹ : StrictOrderedSemiring α
a c : α
inst✝ : ExistsAddOfLE α
b : α
hab : a < a + b
d : α
hcd : c < c + d
⊢ a * (c + d) + (a + b) * c < a * c + (a + b) * (c + d)
case intro
α : Type u
β : Type ?u.10176
inst✝¹ : StrictOrderedSemiring α
a c d : α
inst✝ : ExistsAddOfLE α
hcd : c < d
b : α
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
α : Type u
β : Type ?u.10176
inst✝¹ : StrictOrderedSemiring α
a c : α
inst✝ : ExistsAddOfLE α
b : α
hab : a < a + b
d : α
hcd : c < c + d
⊢ a * c + (a + b) * c + a * d < a * c + (a + b) * c + (a + b) * d
case intro.intro
α : Type u
β : Type ?u.10176
inst✝¹ : StrictOrderedSemiring α
a c : α
inst✝ : ExistsAddOfLE α
b : α
hab : a < a + b
d : α
hcd : c < c + d
⊢ a * (c + d) + (a + b) * c < a * c + (a + b) * (c + d)
rw [mul_add, add_right_comm, mul_add, ← add_assoc]
no goals
case intro.intro
α : Type u
β : Type ?u.10176
inst✝¹ : StrictOrderedSemiring α
a c : α
inst✝ : ExistsAddOfLE α
b : α
hab : a < a + b
d : α
hcd : c < c + d
⊢ a * c + (a + b) * c + a * d < a * c + (a + b) * c + (a + b) * d
exact add_lt_add_left (mul_lt_mul_of_pos_right hab <| (lt_add_iff_pos_right _).1 hcd) _