case intro
ι : Type ?u.137543
α : Type u_1
β : Type ?u.137549
γ : Type ?u.137552
inst✝ : CanonicallyOrderedMonoid α
a : α
m' : Multiset α
h : a ∈ a ::ₘ m'
⊢ a ≤ prod (a ::ₘ m')
ι : Type ?u.137543
α : Type u_1
β : Type ?u.137549
γ : Type ?u.137552
inst✝ : CanonicallyOrderedMonoid α
m : Multiset α
a : α
h : a ∈ m
⊢ a ≤ prod m
obtain ⟨m', rfl⟩ := exists_cons_of_mem h
case intro
ι : Type ?u.137543
α : Type u_1
β : Type ?u.137549
γ : Type ?u.137552
inst✝ : CanonicallyOrderedMonoid α
a : α
m' : Multiset α
h : a ∈ a ::ₘ m'
⊢ a ≤ a * prod m'
case intro
ι : Type ?u.137543
α : Type u_1
β : Type ?u.137549
γ : Type ?u.137552
inst✝ : CanonicallyOrderedMonoid α
a : α
m' : Multiset α
h : a ∈ a ::ₘ m'
⊢ a ≤ prod (a ::ₘ m')
rw [prod_cons]
no goals
case intro
ι : Type ?u.137543
α : Type u_1
β : Type ?u.137549
γ : Type ?u.137552
inst✝ : CanonicallyOrderedMonoid α
a : α
m' : Multiset α
h : a ∈ a ::ₘ m'
⊢ a ≤ a * prod m'
exact _root_.le_mul_right (le_refl a)