How to use dvd_of_mul_left_dvd and friends?

Stream: new members

[Jordan Scales]

Hey :) I'm toying around with some modular arithmetic, and am struggling to prove a basic premise: 3 ∣ n → ¬ 5 ∣ n → ¬ 15 ∣ n

I'd like to prove this by assuming divisibility by 15, and finding a contradiction with divisibility by 5. However, dvd_of_mul_left_dvd is giving me pause.

example (n : ℕ) : 3 ∣ n -> ¬ 5 ∣ n -> ¬ 15 ∣ n := begin
  intros h₃ h₅ h,
  have q : 15 = 3 * 5, { refl },
  rw q at h,
  have contra := dvd_of_mul_left_dvd h,
end

specifically:

type mismatch at application
  dvd_of_mul_left_dvd h
term
  h
has type
  3 * 5 ∣ n
but is expected to have type
  ?m_3 * ?m_4 ∣ ?m_5

I am unsure why the pattern matching isn't working here. Any pointers?

[Kevin Buzzard]

What do I need to import/open to get this working? Can you post a #mwe?

[Jordan Scales]

my apologies! I have the following imported:

import tactic.suggest
import algebra.divisibility

so the entire (not working :( ) file is as follows:

import tactic.suggest
import algebra.divisibility

example (n : ℕ) : 3 ∣ n -> ¬ 5 ∣ n -> ¬ 15 ∣ n := begin
  intros h₃ h₅ h,
  have q : 15 = 3 * 5, { refl },
  rw q at h,
  have contra := dvd_of_mul_left_dvd h,
end

[Kevin Buzzard]

You don't have enough imports, apparently: you seem to have managed to avoid importing the fact that the naturals are a commutative monoid.

import tactic

example (n : ℕ) : 3 ∣ n -> ¬ 5 ∣ n -> ¬ 15 ∣ n := begin
  intros h₃ h₅ h,
  have q : 15 = 3 * 5, { refl },
  rw q at h,
  have contra := dvd_of_mul_left_dvd h,
 sorry
end

works fine.

[Jordan Scales]

fascinating! works for me as well :) thank you.

[Kevin Buzzard]

These facts used to be in core Lean 3 but in the community fork we ripped them out and moved them to mathlib, so now you have to explicitly import them.

[Kevin Buzzard]

I didn't know this wasn't there by default any more because every Lean file I write starts with import tactic.

[Jordan Scales]

starting every file with import tactic is something I can definitely accept