Proving a square isn't 2 mod 3

Stream: new members

[Adrián Doña Mateo]

Is there an easy way to prove this?

import data.nat.modeq

/-- A square is not congruent to 2 module 3 -/
lemma not_square_of_two_mod_three (n : ℕ) (h : n ≡ 2 [MOD 3]) :
    ¬∃ m, m * m = n := sorry

My initial plan was to show that (m : zmod 3) * ↑m = ↑2 and then use fin_cases on ↑m to find a contradiction, but I can't seem to prove this first statement. I would want to use something like a * b = c → ↑a * ↑b = ↑c but I can't find this anywhere.

[Johan Commelin]

import data.nat.modeq
import data.zmod.basic

/-- A square is not congruent to 2 module 3 -/
lemma not_square_of_two_mod_three :
    ¬∃ (m : zmod 3), m * m = 2 := dec_trivial

[Johan Commelin]

Does that help?

[Johan Commelin]

The benefit of using zmod is that it is a finite type, so lean can just prove everything without your help

[Johan Commelin]

@Adrián Doña Mateo :up:

[Reid Barton]

I think the question is how to reduce the original statement to this one

[Adrián Doña Mateo]

Yes, I would like to reduce it to that

[Shing Tak Lam]

import data.nat.modeq
import data.zmod.basic
import data.nat.modeq

/-- A square is not congruent to 2 module 3 -/
lemma not_square_of_two_mod_three :
    ¬∃ (m : zmod 3), m * m = 2 := dec_trivial


/-- A square is not congruent to 2 module 3 -/
lemma not_square_of_two_mod_three' (n : ℕ) (h : n ≡ 2 [MOD 3]) :
    ¬∃ m, m * m = n :=
begin
  rintro ⟨m, rfl⟩,
  apply not_square_of_two_mod_three,
  use m,
  norm_cast,
  rwa ←zmod.eq_iff_modeq_nat at h,
end

[Adrián Doña Mateo]

I see, so norm_cast was the piece I was missing. Thank you! These are very nice solutions.