# Zulip Chat Archive

## Stream: new members

### Topic: rational coertion

#### Sayantan Majumdar (May 04 2020 at 22:17):

having some trouble prooving this

```
theorem simple_01 (p : ℚ) : 2 * ↑(p.num * p.num) = 2 * ↑(p.num) * ↑(p.num) := rfl
```

there is some coercion problem

#### Kevin Buzzard (May 04 2020 at 22:23):

#mwe? This doesn't compile for me. Did you try `by norm_cast`

?

#### Sayantan Majumdar (May 04 2020 at 22:24):

no, will now

I was trying to prove

```
example : ¬(∃ p : ℚ, p * p = 2) := sorry
```

#### Sayantan Majumdar (May 04 2020 at 22:26):

it talks about class_instance resolution dept

have to increase class.instance_max_dept

#### Sayantan Majumdar (May 04 2020 at 22:28):

`rat.cast_mul`

#### Sayantan Majumdar (May 04 2020 at 22:37):

thanks, fixed it with `int.cast_mul`

and `nat.cast_mul`

for `rat.num`

and `rat.denom`

respectively

#### Kevin Buzzard (May 04 2020 at 23:05):

All these `cast_mul`

lemmas are known to the `norm_cast`

tactic, which should in theory solve all problems of this nature in one fell swoop. I still don't know what the up-arrows signify in your original question, they are a coercion but you haven't given enough information to enable people to work out where you're coercing.

#### Sayantan Majumdar (May 04 2020 at 23:51):

they are taking them to `\Q`

#### Sayantan Majumdar (May 04 2020 at 23:52):

I was trying to prove these but there is some issue

```
example : ¬(∃ p : ℚ, p * p = 2) :=
begin
assume h,
apply exists.elim h,
assume p,
assume h₀,
have h₁ : (p * p) * (p * p).denom = 2 * (p * p).denom, from (@congr_arg ℚ ℚ (p * p) (2 : ℤ) (λ x : ℚ, x * (p * p).denom) h₀),
rewrite rat.mul_own_denom_eq_num at h₁,
rewrite rat.mul_self_denom at h₁,
rewrite rat.mul_self_num at h₁,
rewrite (int.cast_mul) at h₁,
rewrite (nat.cast_mul) at h₁,
have h₂ : 2 ∣ (↑p.num * ↑p.num), from (dvd.intro (p.denom * p.denom) (eq.symm h₁)),
-- have h₃ : 2 ∣ ↑p.num, from nat.coprime.mul_dvd_of_dvd_of_dvd
-- have h₂ : p.num * p.num = 2 * (p.denom * p.denom),
-- have h₂ : 2 ∣ (↑p.num * ↑p.num), from @dvd.intro _ _ 2 ↑(p.num * p.num) ↑(p.denom * p.denom) (eq.symm h₁),
-- have a₀ : 2 ∣ (p * p).num, from @dvd.intro ℤ _ 2 (p * p).num (p * p).denom (eq.symm h₁),
-- have a₀ : ↑(p * p).denom ∣ ↑(p * p).num, from dvd.intro_left 2 (eq.symm h₁),
-- have a₁, from rat.cop (p * p),
-- have h₃ : 2 ∣ p.num, from dvd.
-- sorry
end
```

`h₂`

sometimes compiles but sometimes it timesout

#### Sayantan Majumdar (May 04 2020 at 23:53):

it did compile a few minutes ago but it has timed out the next few times

#### Sayantan Majumdar (May 04 2020 at 23:55):

the multiplication in `h₁`

is taking everything to `ℚ`

#### Sayantan Majumdar (May 05 2020 at 00:03):

this helped

```
have h₂ : 2 ∣ ((↑p.num * ↑p.num) : ℚ), from (dvd.intro (p.denom * p.denom) (eq.symm h₁)),
```

#### Kevin Buzzard (May 05 2020 at 16:58):

I think that 2 divides any rational number.

Last updated: May 18 2021 at 16:25 UTC