# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: manipulating multiset elements in proof

#### Bassem Safieldeen (Jul 26 2020 at 11:11):

Hi everyone,

I am learning how to do stuff with multisets and I am stuck. I have a multiset `X : multiset ℝ`

and a function `myFunc : multiset ℝ → multiset ℝ`

that doubles elements of a multiset. I am trying to prove that if the multiset has 10 elements and each element of the multiset is 5, then applying `myFunc`

and summing gives us 100.

Here is my code:

```
import algebra.big_operators
import data.real.basic
/-
A function that doubles every element in a given multiset of ℝ.
-/
def myFunc : multiset ℝ → multiset ℝ :=
begin
intro X,
exact multiset.map (λ x:ℝ, 2*x) X,
end
/-
For a multiset of 10 elements, all of which are 5, doubling
each element and summing gives 100.
-/
example (X : multiset ℝ) (hX' : X.card = 10) :
(∀(x:ℝ), x ∈ X → x = 5) → (myFunc X).sum = 100 :=
begin
intro hX'',
unfold myFunc,
-- ⊢ (multiset.map (λ (x : ℝ), 2 * x) X).sum = 100
sorry
end
```

#### Mario Carneiro (Jul 26 2020 at 11:12):

The first step might be to prove `X = list.repeat 5 10`

#### Bassem Safieldeen (Jul 26 2020 at 11:16):

Mario Carneiro said:

The first step might be to prove

`X = list.repeat 5 10`

Will give it a try now.

#### Kenny Lau (Jul 26 2020 at 11:17):

```
import algebra.big_operators
import data.real.basic
/-
A function that doubles every element in a given multiset of ℝ.
-/
def myFunc (X : multiset ℝ) : multiset ℝ :=
X.map $ λ x, 2 * x
theorem multiset.map_repeat {α β : Sort*} (f : α → β) (x : α) (n : ℕ) :
(multiset.repeat x n).map f = multiset.repeat (f x) n :=
nat.rec_on n rfl $ λ n ih, by simp_rw [multiset.repeat_succ, multiset.map_cons, ih]
/-
For a multiset of 10 elements, all of which are 5, doubling
each element and summing gives 100.
-/
example (X : multiset ℝ) (hX1 : X.card = 10) (hX2 : ∀ x ∈ X, (x : ℝ) = 5) : (myFunc X).sum = 100 :=
by { rw [multiset.eq_repeat_of_mem hX2, hX1, myFunc, multiset.map_repeat, multiset.sum_repeat], norm_num }
```

#### Bassem Safieldeen (Jul 26 2020 at 11:20):

This is a good chance to ask about `$`

:)

I see it occasionally but don't know what it means.

#### Mario Carneiro (Jul 26 2020 at 11:21):

```
example (X : multiset ℝ) (hX' : X.card = 10) :
(∀(x:ℝ), x ∈ X → x = 5) → (myFunc X).sum = 100 :=
begin
intro hX'',
have : X = list.repeat (5:ℝ) 10,
{ obtain ⟨l⟩ := X,
change (l : multiset ℝ) = _, congr,
exact list.eq_repeat.2 ⟨hX', hX''⟩ },
subst X,
rw show (100:ℝ) = (10:ℕ) * (2 * 5), by norm_num,
generalize_hyp : 10 = a at *,
simp [myFunc],
end
```

You can do the last bit without the `generalize_hyp`

but `simp`

does a really stupid proof in that case

#### Mario Carneiro (Jul 26 2020 at 11:23):

```
example (X : multiset ℝ) (hX' : X.card = 10) :
(∀(x:ℝ), x ∈ X → x = 5) → (myFunc X).sum = 100 :=
begin
intro hX'',
have := multiset.eq_repeat.2 ⟨hX', hX''⟩,
subst X,
rw show (100:ℝ) = (10:ℕ) * (2 * 5), by norm_num,
generalize_hyp : 10 = a at *,
simp [myFunc, multiset.repeat],
end
```

#### Mario Carneiro (Jul 26 2020 at 11:23):

`f $ x`

means `f x`

but it has lower precedence

#### Kenny Lau (Jul 26 2020 at 12:26):

That means `f $ x y`

= `f (x y)`

(as opposed to `f x y`

= `(f x) y`

)

#### Eric Wieser (Jul 29 2020 at 18:20):

(deleted)

Last updated: May 16 2021 at 05:21 UTC