α : Type u_1
β : Type ?u.42748
γ : Type ?u.42751
δ : Type ?u.42754
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
this : DecidableEq (Associates α)
⊢ Multiset.prod p ≤ Multiset.prod q
α : Type u_1
β : Type ?u.42748
γ : Type ?u.42751
δ : Type ?u.42754
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
⊢ Multiset.prod p ≤ Multiset.prod q
haveI := Classical.decEq (Associates α)
α : Type u_1
β : Type ?u.42748
γ : Type ?u.42751
δ : Type ?u.42754
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
this✝ : DecidableEq (Associates α)
this : DecidableEq α
⊢ Multiset.prod p ≤ Multiset.prod q
α : Type u_1
β : Type ?u.42748
γ : Type ?u.42751
δ : Type ?u.42754
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
this : DecidableEq (Associates α)
⊢ Multiset.prod p ≤ Multiset.prod q
haveI := Classical.decEq α
α : Type u_1
β : Type ?u.42748
γ : Type ?u.42751
δ : Type ?u.42754
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
this✝ : DecidableEq (Associates α)
this : DecidableEq α
⊢ Multiset.prod p ≤ Multiset.prod (p + (q - p))
α : Type u_1
β : Type ?u.42748
γ : Type ?u.42751
δ : Type ?u.42754
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
this✝ : DecidableEq (Associates α)
this : DecidableEq α
⊢ Multiset.prod p ≤ Multiset.prod q
suffices p.prod ≤ (p + (q - p)).prod by rwa [add_tsub_cancel_of_le h] at this
α : Type u_1
β : Type ?u.42748
γ : Type ?u.42751
δ : Type ?u.42754
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
this✝ : DecidableEq (Associates α)
this : DecidableEq α
⊢ Multiset.prod p * 1 ≤ Multiset.prod p * Multiset.prod (q - p)
α : Type u_1
β : Type ?u.42748
γ : Type ?u.42751
δ : Type ?u.42754
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
this✝ : DecidableEq (Associates α)
this : DecidableEq α
⊢ Multiset.prod p ≤ Multiset.prod (p + (q - p))
suffices p.prod * 1 ≤ p.prod * (q - p).prod by simpa
no goals
α : Type u_1
β : Type ?u.42748
γ : Type ?u.42751
δ : Type ?u.42754
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
this✝ : DecidableEq (Associates α)
this : DecidableEq α
⊢ Multiset.prod p * 1 ≤ Multiset.prod p * Multiset.prod (q - p)
exact mul_mono (le_refl p.prod) one_le
no goals
α : Type u_1
β : Type ?u.42748
γ : Type ?u.42751
δ : Type ?u.42754
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
this✝¹ : DecidableEq (Associates α)
this✝ : DecidableEq α
this : Multiset.prod p ≤ Multiset.prod (p + (q - p))
⊢ Multiset.prod p ≤ Multiset.prod q
rwa [add_tsub_cancel_of_le h] at this
no goals
α : Type u_1
β : Type ?u.42748
γ : Type ?u.42751
δ : Type ?u.42754
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
this✝¹ : DecidableEq (Associates α)
this✝ : DecidableEq α
this : Multiset.prod p * 1 ≤ Multiset.prod p * Multiset.prod (q - p)
⊢ Multiset.prod p ≤ Multiset.prod (p + (q - p))
simpa