# Zulip Chat Archive

## Stream: new members

### Topic: Type confusion

#### Gareth Ma (Feb 02 2023 at 14:46):

Hi. I am dealing with rationals numbers and integers at the same time (oh no), and I am getting very lost converting between all the types. This is what I have:

```
lemma nice_lemma {q : ℚ} {n : ℤ} (h : n ≠ 0) : (q * n).denom = 1 ↔ ↑q.denom ∣ n :=
begin
replace hn : (n : ℚ) ≠ 0, by rwa [ne.def, ← int.cast_zero, rat.coe_int_inj],
split; intros h,
{ rw [← rat.num_div_denom q, div_eq_mul_inv, mul_assoc, mul_comm _ ↑n, ← mul_assoc,
← div_eq_mul_inv, ← int.cast_mul, show (q.denom : ℚ) = ↑(q.denom : ℤ), by exact rfl,
rat.denom_div_cast_eq_one_iff] at h,
{ exact int.dvd_of_dvd_mul_right_of_gcd_one h (coprime.symm q.cop), },
{ norm_cast, exact rat.denom_ne_zero q, }, },
{ rw [← rat.num_div_denom q, div_eq_mul_inv, mul_assoc, mul_comm _ ↑n, ← mul_assoc,
← div_eq_mul_inv, ← int.cast_mul, show (q.denom : ℚ) = ↑(q.denom : ℤ), by exact rfl,
rat.denom_div_cast_eq_one_iff],
{ apply dvd_mul_of_dvd_right h, },
{ norm_cast, exact rat.denom_ne_zero q, }, },
end
lemma nice_lemma' {q : ℚ} {n : ℕ} (h : n ≠ 0) : (q * n).denom = 1 ↔ q.denom ∣ n :=
begin
end
```

I have two questions:

- It is clear that the proof of
`nice_lemma`

has a block of literal copy and paste, but I cannot seem to get rid of it. I tried`rw`

before`split`

but it only`rw`

once, and I will have to`rw`

twice to get the effect I want. Using`simp only`

runs into self-modifying (?) issues. Can someone provide a better solution, or even an existing lemma that will do the work? I looked for a while but can't find anything. - How to prove
`nice_lemma'`

from`nice_lemma`

? I want to do something like`lift n to \Z`

, but it failed and I don't know what I am doing.

#### Riccardo Brasca (Feb 02 2023 at 14:52):

You need an intermediate lemma saying that if `(q : ℚ)`

and `(n : ℕ)`

then `(n : ℤ) * q = n * q`

. This shouldn't be hard (maybe it is `rfl`

). Then you have to convert the assumption `n ≠ 0`

to `(n : ℤ) ≠ 0`

, and this is surely in the library.

#### Gareth Ma (Feb 02 2023 at 15:07):

Thank you! After doing all that then golfing and collapsing everything, I got this :)

```
lemma nice_lemma' {q : ℚ} {n : ℕ} (h : n ≠ 0) : (q * n).denom = 1 ↔ q.denom ∣ n :=
by exact iff.trans (nice_lemma (cast_ne_zero.2 h)) int.coe_nat_dvd
```

One line!

#### Patrick Massot (Feb 02 2023 at 15:13):

That line is too long, it should be `(nice_lemma (cast_ne_zero.2 h)).trans int.coe_nat_dvd`

#### Patrick Massot (Feb 02 2023 at 15:13):

(without `by exact`

which is useless)

#### Eric Wieser (Feb 02 2023 at 15:14):

`by exact_mod_cast (@nice_lemma _ n $ by exact_mod_cast h)`

also works

#### Gareth Ma (Feb 02 2023 at 15:15):

Oh wow, let me understand them slowly :) Sooo much to learn

#### Gareth Ma (Feb 02 2023 at 15:35):

What is the `@`

doing? I don't understand the error after removing it.

#### Pedro Sánchez Terraf (Feb 02 2023 at 16:00):

Gareth Ma said:

What is the

`@`

doing? I don't understand the error after removing it.

It makes all arguments explicit (in this case, `q`

and `n`

).

Last updated: Dec 20 2023 at 11:08 UTC