# Zulip Chat Archive

## Stream: new members

### Topic: Help with proof

#### Markus Schmaus (Oct 11 2023 at 22:31):

I am working on a proof and my tactics state looks like this:

```
h_prod: List.prod dvds = n / x * (x * List.prod acc)
h_x_mem_div: x ∣ n
⊢ List.prod dvds = n * List.prod acc
```

I think I know what needs to happen. Apply `Nat.mul_assoc`

to the right hand side of `h_prod`

and then `Nat.div_mul_cancel`

with `h_x_mem_div`

gives me the result.

But I can't get lean to do that, I similar looking cases I have used`simp`

or `rw`

, but for some reason I can't get either to work. Can someone give me a hint?

#### Patrick Massot (Oct 11 2023 at 22:42):

Could you please help us helping you by reading #mwe and then editing your post?

#### Markus Schmaus (Oct 11 2023 at 22:50):

I think this should be a mwe

```
import Mathlib
example
(h_prod: List.prod dvds = n / x * (x * List.prod acc))
(h_n_eq_0: ¬n = 0)
(h_x_mem_div: x ∣ n)
: (List.prod dvds = n * List.prod acc) := by
sorry
```

#### Eric Wieser (Oct 11 2023 at 22:57):

Can you include the `rw`

/`simp`

/ whatever invocation that you tried?

#### Eric Wieser (Oct 11 2023 at 22:58):

Your outline works without any difficulty for me, so it seems that the problem is with how you attempted to lean-ify it

#### Markus Schmaus (Oct 11 2023 at 23:14):

This is what I expected to work: `simp [Nat.mul_assoc, Nat.div_mul_cancel] at h_prod`

. I tried all permutations of this I could think off, including throwing in some `Nat.mul_comm`

. So yes, the problem is that I don't know how to lean-ify it.

#### Markus Schmaus (Oct 12 2023 at 06:36):

@Eric Wieser Could you tell me how you solved the outline without any difficulty?

#### Ruben Van de Velde (Oct 12 2023 at 07:16):

I'm not Eric, but this is how I tackled it:

```
example
(h_prod: List.prod dvds = n / x * (x * List.prod acc))
(h_n_eq_0: ¬n = 0)
(h_x_mem_div: x ∣ n) :
List.prod dvds = n * List.prod acc := by
rw [h_prod] -- eliminate `dvds`, this is now just a theorem about natural numbers
rw [← mul_assoc] -- move the parentheses around so we can work on `(n / x * x)`
congr -- optional: remove the parts of the expression that are the same on both sides
-- Goal is `n / x * x = n`: there should be a theorem in the library that states this
-- `apply?` tells us what it's called:
exact Nat.div_mul_cancel h_x_mem_div
```

#### Markus Schmaus (Oct 12 2023 at 07:28):

Thank you, this was the piece I was missing: `←`

Last updated: Dec 20 2023 at 11:08 UTC