case zero
ι : Type ?u.127230
α : Type u_1
β : Type ?u.127236
γ : Type ?u.127239
inst✝ : OrderedCommMonoid α
s t : Multiset α
a : α
⊢ prod 0 ≤ prod 0

case cons
ι : Type ?u.127230
α : Type u_1
β : Type ?u.127236
γ : Type ?u.127239
inst✝ : OrderedCommMonoid α
s t : Multiset α
a a✝¹ b✝ : α
as✝ bs✝ : Multiset α
rh : a✝¹ ≤ b✝
a✝ : Rel (fun x x_1 => x ≤ x_1) as✝ bs✝
rt : prod as✝ ≤ prod bs✝
⊢ prod (a✝¹ ::ₘ as✝) ≤ prod (b✝ ::ₘ bs✝)
ι : Type ?u.127230
α : Type u_1
β : Type ?u.127236
γ : Type ?u.127239
inst✝ : OrderedCommMonoid α
s t : Multiset α
a : α
h : Rel (fun x x_1 => x ≤ x_1) s t
⊢ prod s ≤ prod t
induction' h with _ _ _ _ rh _ rt
no goals
case zero
ι : Type ?u.127230
α : Type u_1
β : Type ?u.127236
γ : Type ?u.127239
inst✝ : OrderedCommMonoid α
s t : Multiset α
a : α
⊢ prod 0 ≤ prod 0
rfl
case cons
ι : Type ?u.127230
α : Type u_1
β : Type ?u.127236
γ : Type ?u.127239
inst✝ : OrderedCommMonoid α
s t : Multiset α
a a✝¹ b✝ : α
as✝ bs✝ : Multiset α
rh : a✝¹ ≤ b✝
a✝ : Rel (fun x x_1 => x ≤ x_1) as✝ bs✝
rt : prod as✝ ≤ prod bs✝
⊢ a✝¹ * prod as✝ ≤ b✝ * prod bs✝
case cons
ι : Type ?u.127230
α : Type u_1
β : Type ?u.127236
γ : Type ?u.127239
inst✝ : OrderedCommMonoid α
s t : Multiset α
a a✝¹ b✝ : α
as✝ bs✝ : Multiset α
rh : a✝¹ ≤ b✝
a✝ : Rel (fun x x_1 => x ≤ x_1) as✝ bs✝
rt : prod as✝ ≤ prod bs✝
⊢ prod (a✝¹ ::ₘ as✝) ≤ prod (b✝ ::ₘ bs✝)
rw [prod_cons, prod_cons]
no goals
case cons
ι : Type ?u.127230
α : Type u_1
β : Type ?u.127236
γ : Type ?u.127239
inst✝ : OrderedCommMonoid α
s t : Multiset α
a a✝¹ b✝ : α
as✝ bs✝ : Multiset α
rh : a✝¹ ≤ b✝
a✝ : Rel (fun x x_1 => x ≤ x_1) as✝ bs✝
rt : prod as✝ ≤ prod bs✝
⊢ a✝¹ * prod as✝ ≤ b✝ * prod bs✝
exact mul_le_mul' rh rt