apply mul_le_mul (mul_le_mul h₁ h₂ c0 b0) h₃ e0 <| mul_nonneg b0 <| le_trans c0 h₂
α : Type u_1
a b c d e f : α
inst✝³ : MulZeroClass α
inst✝² : Preorder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
h₁ : a ≤ b
h₂ : c ≤ d
h₃ : e ≤ f
c0 : 0 ≤ c
b0 : 0 ≤ b
e0 : 0 ≤ e
⊢ a * c * e ≤ b * d * f
no goals