## 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