-- Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean
@[to_additive le_sum_nonempty_of_subadditive_on_pred]
lemma le_prod_nonempty_of_submultiplicative_on_pred (f : α → β) (p : α → Prop)
    (h_mul : ∀ a b, p a → p b → f (a * b) ≤ f a * f b) (hp_mul : ∀ a b, p a → p b → p (a * b))
    (s : Multiset α) (hs_nonempty : s ≠ ∅) (hs : ∀ a, a ∈ s → p a) : f s.prod ≤ (s.map f).prod

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
s : Multiset α
hs_nonempty : s ≠ ∅
hs : ∀ a ∈ s, p a
⊢ f s.prod ≤ (map f s).prod

Tactic:
revert s

Result:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
⊢ ∀ (s : Multiset α), s ≠ ∅ → (∀ a ∈ s, p a) → f s.prod ≤ (map f s).prod

Proof state:
case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
⊢ ∀ (a : α) (s : Multiset α),
    (s ≠ ∅ → (∀ a ∈ s, p a) → f s.prod ≤ (map f s).prod) →
      a ::ₘ s ≠ ∅ → (∀ a_2 ∈ a ::ₘ s, p a_2) → f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod

Tactic:
rintro a s hs - hsa_prop

Result:
case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : s ≠ ∅ → (∀ a ∈ s, p a) → f s.prod ≤ (map f s).prod
hsa_prop : ∀ a_1 ∈ a ::ₘ s, p a_1
⊢ f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod

Proof state:
case neg
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : s ≠ ∅ → (∀ a ∈ s, p a) → f s.prod ≤ (map f s).prod
hsa_prop : ∀ a_1 ∈ a ::ₘ s, p a_1
hs_empty : ¬s = ∅
hsa_restrict : ∀ x ∈ s, p x
⊢ f (a * s.prod) ≤ f a * (map f s).prod

Tactic:
have hp_sup : p s.prod := prod_induction_nonempty p hp_mul hs_empty hsa_restrict

Result:
case neg
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : s ≠ ∅ → (∀ a ∈ s, p a) → f s.prod ≤ (map f s).prod
hsa_prop : ∀ a_1 ∈ a ::ₘ s, p a_1
hs_empty : ¬s = ∅
hsa_restrict : ∀ x ∈ s, p x
hp_sup : p s.prod
⊢ f (a * s.prod) ≤ f a * (map f s).prod

Proof state:
case neg
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : s ≠ ∅ → (∀ a ∈ s, p a) → f s.prod ≤ (map f s).prod
hsa_prop : ∀ a_1 ∈ a ::ₘ s, p a_1
hs_empty : ¬s = ∅
hsa_restrict : ∀ x ∈ s, p x
hp_sup : p s.prod
⊢ f (a * s.prod) ≤ f a * (map f s).prod

Tactic:
have hp_a : p a := hsa_prop a (mem_cons_self a s)

Result:
case neg
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : s ≠ ∅ → (∀ a ∈ s, p a) → f s.prod ≤ (map f s).prod
hsa_prop : ∀ a_1 ∈ a ::ₘ s, p a_1
hs_empty : ¬s = ∅
hsa_restrict : ∀ x ∈ s, p x
hp_sup : p s.prod
hp_a : p a
⊢ f (a * s.prod) ≤ f a * (map f s).prod

Proof state:
case neg
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : s ≠ ∅ → (∀ a ∈ s, p a) → f s.prod ≤ (map f s).prod
hsa_prop : ∀ a_1 ∈ a ::ₘ s, p a_1
hs_empty : ¬s = ∅
hsa_restrict : ∀ x ∈ s, p x
hp_sup : p s.prod
hp_a : p a
⊢ f (a * s.prod) ≤ f a * (map f s).prod

Tactic:
exact (h_mul a _ hp_a hp_sup).trans (mul_le_mul_left' (hs hs_empty hsa_restrict) _)

Result:
no goals

Proof state:
case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : s ≠ ∅ → (∀ a ∈ s, p a) → f s.prod ≤ (map f s).prod
hsa_prop : ∀ a_1 ∈ a ::ₘ s, p a_1
⊢ f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod

Tactic:
rw [prod_cons, map_cons, prod_cons]

Result:
case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : s ≠ ∅ → (∀ a ∈ s, p a) → f s.prod ≤ (map f s).prod
hsa_prop : ∀ a_1 ∈ a ::ₘ s, p a_1
⊢ f (a * s.prod) ≤ f a * (map f s).prod

Proof state:
case pos
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : s ≠ ∅ → (∀ a ∈ s, p a) → f s.prod ≤ (map f s).prod
hsa_prop : ∀ a_1 ∈ a ::ₘ s, p a_1
hs_empty : s = ∅
⊢ f (a * s.prod) ≤ f a * (map f s).prod

Tactic:
simp [hs_empty]

Result:
no goals

Proof state:
case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : s ≠ ∅ → (∀ a ∈ s, p a) → f s.prod ≤ (map f s).prod
hsa_prop : ∀ a_1 ∈ a ::ₘ s, p a_1
⊢ f (a * s.prod) ≤ f a * (map f s).prod

Tactic:
by_cases hs_empty : s = ∅

Result:
case pos
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : s ≠ ∅ → (∀ a ∈ s, p a) → f s.prod ≤ (map f s).prod
hsa_prop : ∀ a_1 ∈ a ::ₘ s, p a_1
hs_empty : s = ∅
⊢ f (a * s.prod) ≤ f a * (map f s).prod

case neg
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : s ≠ ∅ → (∀ a ∈ s, p a) → f s.prod ≤ (map f s).prod
hsa_prop : ∀ a_1 ∈ a ::ₘ s, p a_1
hs_empty : ¬s = ∅
⊢ f (a * s.prod) ≤ f a * (map f s).prod

Proof state:
case neg
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : s ≠ ∅ → (∀ a ∈ s, p a) → f s.prod ≤ (map f s).prod
hsa_prop : ∀ a_1 ∈ a ::ₘ s, p a_1
hs_empty : ¬s = ∅
⊢ f (a * s.prod) ≤ f a * (map f s).prod

Tactic:
have hsa_restrict : ∀ x, x ∈ s → p x := fun x hx => hsa_prop x (mem_cons_of_mem hx)

Result:
case neg
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : s ≠ ∅ → (∀ a ∈ s, p a) → f s.prod ≤ (map f s).prod
hsa_prop : ∀ a_1 ∈ a ::ₘ s, p a_1
hs_empty : ¬s = ∅
hsa_restrict : ∀ x ∈ s, p x
⊢ f (a * s.prod) ≤ f a * (map f s).prod