# Zulip Chat Archive

## Stream: new members

### Topic: if `x|a*b` then `x|a` or `x|b`

#### Lars Ericson (Jan 10 2021 at 23:32):

I'm looking for a lifeline here:

```
import data.nat.basic
import tactic
lemma expand_dvd (a b: ℕ ) : a ∣ b ↔ ∃ c, b = a * c :=
begin
exact iff.rfl,
end
lemma dvd_mul_a_b_then_a_or_b {a b x : ℕ} (h: (x ∣ (a*b))) : x ∣ a ∨ x ∣ b :=
begin
have h1 := exists_eq_mul_right_of_dvd h,
by_cases ha : x ∣ a,
finish,
refine or.inr _,
cases h1 with c hc,
have h2 := (expand_dvd x b).2,
apply h2,
sorry
end
```

The tactic state is

```
1 goal
abx: ℕ
h: x ∣ a * b
ha: ¬x ∣ a
c: ℕ
hc: a * b = x * c
h2: (∃ (c : ℕ), b = x * c) → x ∣ b
⊢ ∃ (c : ℕ), b = x * c
```

It seems like an obvious fact but I'm blanking out and I don't see it already in docs#dvd

#### Kevin Buzzard (Jan 10 2021 at 23:34):

Do you know the maths proof? I'm particularly interested in your answer this time, because in this case you're wasting your time -- what you're trying to prove here is false. You have to know the maths proof.

#### Bryan Gin-ge Chen (Jan 10 2021 at 23:41):

`slim_check`

can find lots of counterexamples:

```
import tactic.slim_check
lemma dvd_mul_a_b_then_a_or_b {a b x : ℕ} (h: (x ∣ (a*b))) : x ∣ a ∨ x ∣ b :=
by slim_check
/-
===================
Found problems!
a := 1198
b := 18
x := 4
(0 shrinks)
-------------------
state:
a b x : ℕ,
h : x ∣ a * b
⊢ x ∣ a ∨ x ∣ b
-/
```

#### Kevin Buzzard (Jan 10 2021 at 23:42):

Oh nice! It's about time I stopped forgetting that `slim_check`

exists.

#### Adam Topaz (Jan 10 2021 at 23:49):

I wonder... Can slim check work in "reverse" trying to find additional hypotheses that will "fix" a statement?

#### Kevin Buzzard (Jan 10 2021 at 23:50):

`h : false`

will fix this one

#### Adam Topaz (Jan 10 2021 at 23:50):

Yeah, it needs to be a bit more clever than that :wink:

#### Kevin Buzzard (Jan 10 2021 at 23:51):

Lars -- if x is 0 or 1 or prime you're OK. But I'm not sure if a computer could spot that!

#### Kevin Buzzard (Jan 10 2021 at 23:53):

The smartest thing to do on this occasion would be to try values of x sequentially, figure out which ones seem to work, and then to query oeis.org to try and find out what's going on. But even here there's a subtlety -- you have to know that it's a condition on x which gives you the interesting theorem, as opposed to a condition on a or b.

#### Kevin Buzzard (Jan 10 2021 at 23:54):

#### Adam Topaz (Jan 10 2021 at 23:54):

Oooh searching oeis is a very interesting idea!

#### Kevin Buzzard (Jan 10 2021 at 23:55):

In the old days you had to search Don Zagier, which was much more inconvenient.

#### Kevin Buzzard (Jan 10 2021 at 23:57):

I remember when people started uploading pari code to OEIS which produced the sequences -- I thought it was a neat idea. Now I'm thinking that if enough people started uploading Lean code to produce the functions, you really could get something neat :-) Can we port the pari code to Lean?

#### Julian Berman (Jan 11 2021 at 00:05):

is there a tactic that knows how to instead look at the type of the goal and suggest hypotheses based on things in mathlib already with that goal type?

#### Adam Topaz (Jan 11 2021 at 00:06):

There's the `#find`

command

#### Lars Ericson (Jan 11 2021 at 00:10):

@Kevin Buzzard you're right, I didn't consider the possibility that `x`

could be a product of a factor in `a`

and a factor in `b`

.

I was actually trying to prove this lemma which is also false by `slim_check`

:

```
import data.nat.basic
import tactic.slim_check
lemma neg_dvd_mul {a b x : ℕ} (ha: ¬(x ∣ a)) (hb: ¬(x ∣ b)) : ¬ (x ∣ (a*b)) :=
by slim_check
```

The counterexample is

```
a := 34
b := 6
x := 12
```

#### Lars Ericson (Jan 11 2021 at 00:10):

Thank you @Bryan Gin-ge Chen for `slim_check`

.

#### Kevin Buzzard (Jan 11 2021 at 00:11):

or x=4, a=b=2.

Last updated: May 15 2021 at 23:13 UTC