no goals
α✝ : Type ?u.53011
β✝ : Type ?u.53014
γ : Type ?u.53017
δ : Type ?u.53020
a : α✝
s t : Multiset α✝
f✝ g : α✝ → Multiset β✝
α : Type u_1
β : Type u_2
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
⊢ f x ≤ bind S f
classical
  rw [le_iff_count]
  intro a
  rw [count_bind]
  apply le_sum_of_mem
  rw [mem_map]
  exact ⟨x, hx, rfl⟩
α✝ : Type ?u.53011
β✝ : Type ?u.53014
γ : Type ?u.53017
δ : Type ?u.53020
a : α✝
s t : Multiset α✝
f✝ g : α✝ → Multiset β✝
α : Type u_1
β : Type u_2
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
⊢ ∀ (a : β), count a (f x) ≤ count a (bind S f)
α✝ : Type ?u.53011
β✝ : Type ?u.53014
γ : Type ?u.53017
δ : Type ?u.53020
a : α✝
s t : Multiset α✝
f✝ g : α✝ → Multiset β✝
α : Type u_1
β : Type u_2
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
⊢ f x ≤ bind S f
rw [le_iff_count]
α✝ : Type ?u.53011
β✝ : Type ?u.53014
γ : Type ?u.53017
δ : Type ?u.53020
a✝ : α✝
s t : Multiset α✝
f✝ g : α✝ → Multiset β✝
α : Type u_1
β : Type u_2
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
⊢ count a (f x) ≤ count a (bind S f)
α✝ : Type ?u.53011
β✝ : Type ?u.53014
γ : Type ?u.53017
δ : Type ?u.53020
a : α✝
s t : Multiset α✝
f✝ g : α✝ → Multiset β✝
α : Type u_1
β : Type u_2
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
⊢ ∀ (a : β), count a (f x) ≤ count a (bind S f)
intro a
α✝ : Type ?u.53011
β✝ : Type ?u.53014
γ : Type ?u.53017
δ : Type ?u.53020
a✝ : α✝
s t : Multiset α✝
f✝ g : α✝ → Multiset β✝
α : Type u_1
β : Type u_2
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
⊢ count a (f x) ≤ sum (map (fun b => count a (f b)) S)
α✝ : Type ?u.53011
β✝ : Type ?u.53014
γ : Type ?u.53017
δ : Type ?u.53020
a✝ : α✝
s t : Multiset α✝
f✝ g : α✝ → Multiset β✝
α : Type u_1
β : Type u_2
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
⊢ count a (f x) ≤ count a (bind S f)
rw [count_bind]
case h
α✝ : Type ?u.53011
β✝ : Type ?u.53014
γ : Type ?u.53017
δ : Type ?u.53020
a✝ : α✝
s t : Multiset α✝
f✝ g : α✝ → Multiset β✝
α : Type u_1
β : Type u_2
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
⊢ count a (f x) ∈ map (fun b => count a (f b)) S
α✝ : Type ?u.53011
β✝ : Type ?u.53014
γ : Type ?u.53017
δ : Type ?u.53020
a✝ : α✝
s t : Multiset α✝
f✝ g : α✝ → Multiset β✝
α : Type u_1
β : Type u_2
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
⊢ count a (f x) ≤ sum (map (fun b => count a (f b)) S)
apply le_sum_of_mem
case h
α✝ : Type ?u.53011
β✝ : Type ?u.53014
γ : Type ?u.53017
δ : Type ?u.53020
a✝ : α✝
s t : Multiset α✝
f✝ g : α✝ → Multiset β✝
α : Type u_1
β : Type u_2
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
⊢ ∃ a_1, a_1 ∈ S ∧ count a (f a_1) = count a (f x)
case h
α✝ : Type ?u.53011
β✝ : Type ?u.53014
γ : Type ?u.53017
δ : Type ?u.53020
a✝ : α✝
s t : Multiset α✝
f✝ g : α✝ → Multiset β✝
α : Type u_1
β : Type u_2
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
⊢ count a (f x) ∈ map (fun b => count a (f b)) S
rw [mem_map]
no goals
case h
α✝ : Type ?u.53011
β✝ : Type ?u.53014
γ : Type ?u.53017
δ : Type ?u.53020
a✝ : α✝
s t : Multiset α✝
f✝ g : α✝ → Multiset β✝
α : Type u_1
β : Type u_2
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
⊢ ∃ a_1, a_1 ∈ S ∧ count a (f a_1) = count a (f x)
exact ⟨x, hx, rfl⟩