case inl
α : Type u
inst✝ : CanonicallyLinearOrderedMonoid α
a b c : α
hb : a ≤ b
⊢ min a (b * c) = min a (min a b * min a c)

case inr
α : Type u
inst✝ : CanonicallyLinearOrderedMonoid α
a b c : α
hb : b ≤ a
⊢ min a (b * c) = min a (min a b * min a c)
α : Type u
inst✝ : CanonicallyLinearOrderedMonoid α
a b c : α
⊢ min a (b * c) = min a (min a b * min a c)
cases' le_total a b with hb hb
no goals
case inl
α : Type u
inst✝ : CanonicallyLinearOrderedMonoid α
a b c : α
hb : a ≤ b
⊢ min a (b * c) = min a (min a b * min a c)
simp [hb, le_mul_right]
case inr.inl
α : Type u
inst✝ : CanonicallyLinearOrderedMonoid α
a b c : α
hb : b ≤ a
hc : a ≤ c
⊢ min a (b * c) = min a (min a b * min a c)

case inr.inr
α : Type u
inst✝ : CanonicallyLinearOrderedMonoid α
a b c : α
hb : b ≤ a
hc : c ≤ a
⊢ min a (b * c) = min a (min a b * min a c)
case inr
α : Type u
inst✝ : CanonicallyLinearOrderedMonoid α
a b c : α
hb : b ≤ a
⊢ min a (b * c) = min a (min a b * min a c)
cases' le_total a c with hc hc
no goals
case inr.inl
α : Type u
inst✝ : CanonicallyLinearOrderedMonoid α
a b c : α
hb : b ≤ a
hc : a ≤ c
⊢ min a (b * c) = min a (min a b * min a c)
simp [hc, le_mul_left]
no goals
case inr.inr
α : Type u
inst✝ : CanonicallyLinearOrderedMonoid α
a b c : α
hb : b ≤ a
hc : c ≤ a
⊢ min a (b * c) = min a (min a b * min a c)
simp [hb, hc]