case intro
α : Type u
β : Type ?u.1549
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.1549
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
case intro.intro
α : Type u
β : Type ?u.1549
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.1549
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
case intro.intro
α : Type u
β : Type ?u.1549
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.1549
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.1549
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_le_add_left (mul_le_mul_of_nonneg_right hab <| (le_add_iff_nonneg_right _).1 hcd) _