semigroup.to_has_mul versus nat.has_mul

Stream: new members

[Moritz Firsching]

Consider the following proof attempt to a simple lemma:

import tactic

lemma factorial_divide (n m : ℕ) (hmn: m ≤ n):
((m.factorial * (n-m).factorial)) ∣ (n.factorial) :=
begin
  have chosse_mul:
  (n.choose m)* ((m.factorial * (n-m).factorial)) = (n.factorial) :=
    begin
      simp [nat.choose_eq_factorial_div_factorial hmn],
      -- simp [div_mul_eq_mul_div], why doesn't this work?
      sorry,
    end,
    apply dvd.intro_left ((n.choose m)),
    -- exact choose_mul, why doesn't this work?
  sorry,
end

I'm a bit stumped that e.g. in the after the line apply dvd.intro_left ((n.choose m)), I see the exact same state in the goal and in choose_mul in the lean infoview. When I click on the terms, I can see there is some difference, but how can I actually get control over how the division/multiplication is done when defining choose_mul?

[Kevin Buzzard]

The second question is easy to answer -- you made a typo :-) chosse -> choose

[Moritz Firsching]

cool, that explains solves the second "why doesn't this work?"!

[Kevin Buzzard]

As for the first, #check @div_mul_eq_mul_div shows you that it's a theorem which applies to comm_group_with_zeros, and the naturals are not an example of a comm_group_with_zero.

[Kevin Buzzard]

In fact there will not be a theorem of the form (a / b) * b = a for naturals, because this is not true in general, e.g. (3 / 2) * 2 = 1 * 2 = 2 :-/

[Kevin Buzzard]

to prove a / b * b = a for nats you need the assumption that b divides a, which unfortunately is what you're trying to prove :-/

[Kevin Buzzard]

The result you're trying to prove is already in the library -- it's called nat.factorial_mul_factorial_dvd_factorial, so you can prove it with by library_search. But if you're looking for a proof of your own then maybe this doesn't help.

[Kevin Buzzard]

There is also nat.choose_mul_factorial_mul_factorial

[Moritz Firsching]

Thanks I will just check out how those proofs work! (and meanwhile just use them)