Type confusion

Stream: new members

[Gareth Ma]

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:

1. 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.
2. 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]

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]

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]

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

[Patrick Massot]

(without by exact which is useless)

[Eric Wieser]

by exact_mod_cast (@nice_lemma _ n $ by exact_mod_cast h) also works

[Gareth Ma]

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

[Gareth Ma]

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

[Pedro Sánchez Terraf]

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).