## 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 usedsimp or rw, but for some reason I can't get either to work. Can someone give me a hint?

#### 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