ι : Type ?u.149080
α : Type u_1
β : Type u_2
γ : Type ?u.149089
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 : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)
ι : Type ?u.149080
α : Type u_1
β : Type u_2
γ : Type ?u.149089
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 : α), a ∈ s → p a
⊢ f (prod s) ≤ prod (map f s)
revert s
case refine'_1
ι : Type ?u.149080
α : Type u_1
β : Type u_2
γ : Type ?u.149089
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)
⊢ 0 ≠ ∅ → (∀ (a : α), a ∈ 0 → p a) → f (prod 0) ≤ prod (map f 0)

case refine'_2
ι : Type ?u.149080
α : Type u_1
β : Type u_2
γ : Type ?u.149089
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 : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)) →
      a ::ₘ s ≠ ∅ → (∀ (a_2 : α), a_2 ∈ a ::ₘ s → p a_2) → f (prod (a ::ₘ s)) ≤ prod (map f (a ::ₘ s))
ι : Type ?u.149080
α : Type u_1
β : Type u_2
γ : Type ?u.149089
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 : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)
refine' Multiset.induction _ _
case refine'_2
ι : Type ?u.149080
α : Type u_1
β : Type u_2
γ : Type ?u.149089
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 : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)
hsa_prop : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
⊢ f (prod (a ::ₘ s)) ≤ prod (map f (a ::ₘ s))
case refine'_2
ι : Type ?u.149080
α : Type u_1
β : Type u_2
γ : Type ?u.149089
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 : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)) →
      a ::ₘ s ≠ ∅ → (∀ (a_2 : α), a_2 ∈ a ::ₘ s → p a_2) → f (prod (a ::ₘ s)) ≤ prod (map f (a ::ₘ s))
rintro a s hs - hsa_prop
case refine'_2
ι : Type ?u.149080
α : Type u_1
β : Type u_2
γ : Type ?u.149089
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 : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)
hsa_prop : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
⊢ f (a * prod s) ≤ f a * prod (map f s)
case refine'_2
ι : Type ?u.149080
α : Type u_1
β : Type u_2
γ : Type ?u.149089
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 : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)
hsa_prop : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
⊢ f (prod (a ::ₘ s)) ≤ prod (map f (a ::ₘ s))
rw [prod_cons, map_cons, prod_cons]
case pos
ι : Type ?u.149080
α : Type u_1
β : Type u_2
γ : Type ?u.149089
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 : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)
hsa_prop : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs_empty : s = ∅
⊢ f (a * prod s) ≤ f a * prod (map f s)

case neg
ι : Type ?u.149080
α : Type u_1
β : Type u_2
γ : Type ?u.149089
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 : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)
hsa_prop : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs_empty : ¬s = ∅
⊢ f (a * prod s) ≤ f a * prod (map f s)
case refine'_2
ι : Type ?u.149080
α : Type u_1
β : Type u_2
γ : Type ?u.149089
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 : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)
hsa_prop : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
⊢ f (a * prod s) ≤ f a * prod (map f s)
by_cases hs_empty : s = ∅
case neg
ι : Type ?u.149080
α : Type u_1
β : Type u_2
γ : Type ?u.149089
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 : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)
hsa_prop : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs_empty : ¬s = ∅
hsa_restrict : ∀ (x : α), x ∈ s → p x
⊢ f (a * prod s) ≤ f a * prod (map f s)
case neg
ι : Type ?u.149080
α : Type u_1
β : Type u_2
γ : Type ?u.149089
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 : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)
hsa_prop : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs_empty : ¬s = ∅
⊢ f (a * prod s) ≤ f a * prod (map f s)
have hsa_restrict : ∀ x, x ∈ s → p x := fun x hx => hsa_prop x (mem_cons_of_mem hx)
case neg
ι : Type ?u.149080
α : Type u_1
β : Type u_2
γ : Type ?u.149089
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 : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)
hsa_prop : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs_empty : ¬s = ∅
hsa_restrict : ∀ (x : α), x ∈ s → p x
hp_sup : p (prod s)
⊢ f (a * prod s) ≤ f a * prod (map f s)
case neg
ι : Type ?u.149080
α : Type u_1
β : Type u_2
γ : Type ?u.149089
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 : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)
hsa_prop : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs_empty : ¬s = ∅
hsa_restrict : ∀ (x : α), x ∈ s → p x
⊢ f (a * prod s) ≤ f a * prod (map f s)
have hp_sup : p s.prod := prod_induction_nonempty p hp_mul hs_empty hsa_restrict
case neg
ι : Type ?u.149080
α : Type u_1
β : Type u_2
γ : Type ?u.149089
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 : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)
hsa_prop : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs_empty : ¬s = ∅
hsa_restrict : ∀ (x : α), x ∈ s → p x
hp_sup : p (prod s)
hp_a : p a
⊢ f (a * prod s) ≤ f a * prod (map f s)
case neg
ι : Type ?u.149080
α : Type u_1
β : Type u_2
γ : Type ?u.149089
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 : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)
hsa_prop : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs_empty : ¬s = ∅
hsa_restrict : ∀ (x : α), x ∈ s → p x
hp_sup : p (prod s)
⊢ f (a * prod s) ≤ f a * prod (map f s)
have hp_a : p a := hsa_prop a (mem_cons_self a s)
no goals
case neg
ι : Type ?u.149080
α : Type u_1
β : Type u_2
γ : Type ?u.149089
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 : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)
hsa_prop : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs_empty : ¬s = ∅
hsa_restrict : ∀ (x : α), x ∈ s → p x
hp_sup : p (prod s)
hp_a : p a
⊢ f (a * prod s) ≤ f a * prod (map f s)
exact (h_mul a _ hp_a hp_sup).trans (mul_le_mul_left' (hs hs_empty hsa_restrict) _)
case refine'_1
ι : Type ?u.149080
α : Type u_1
β : Type u_2
γ : Type ?u.149089
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)
h : 0 ≠ ∅
⊢ (∀ (a : α), a ∈ 0 → p a) → f (prod 0) ≤ prod (map f 0)
case refine'_1
ι : Type ?u.149080
α : Type u_1
β : Type u_2
γ : Type ?u.149089
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)
⊢ 0 ≠ ∅ → (∀ (a : α), a ∈ 0 → p a) → f (prod 0) ≤ prod (map f 0)
intro h
case refine'_1.h
ι : Type ?u.149080
α : Type u_1
β : Type u_2
γ : Type ?u.149089
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)
h : 0 ≠ ∅
⊢ False
case refine'_1
ι : Type ?u.149080
α : Type u_1
β : Type u_2
γ : Type ?u.149089
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)
h : 0 ≠ ∅
⊢ (∀ (a : α), a ∈ 0 → p a) → f (prod 0) ≤ prod (map f 0)
exfalso
no goals
case refine'_1.h
ι : Type ?u.149080
α : Type u_1
β : Type u_2
γ : Type ?u.149089
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)
h : 0 ≠ ∅
⊢ False
exact h rfl
no goals
case pos
ι : Type ?u.149080
α : Type u_1
β : Type u_2
γ : Type ?u.149089
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 : α), a ∈ s → p a) → f (prod s) ≤ prod (map f s)
hsa_prop : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs_empty : s = ∅
⊢ f (a * prod s) ≤ f a * prod (map f s)
simp [hs_empty]