Help with proof

Stream: new members

[Markus Schmaus]

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?

[Patrick Massot]

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

[Markus Schmaus]

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]

Can you include the rw /simp / whatever invocation that you tried?

[Eric Wieser]

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]

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]

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

[Ruben Van de Velde]

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]

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