4 | 2 → false

Stream: new members

[Jia Ming]

Hello, may I have some hints as to how to solve these simple questions? I've tried many powerful tactics but all seem to fail :(

example : (4 ∣ 2) → false := sorry
example : (∃ i : ℤ, (1/2 : ℝ) = ↑i) → false := sorry

[Kenny Lau]

the first one decidable, so dec_trivial

[Kenny Lau]

... and the second one can be reduced to the first one :P

[Jia Ming]

Ooo wow thank you!!!

[Jia Ming]

Umm huh, what exactly do u mean by reduced to the first one?

[Kenny Lau]

well you can prove that 2 * i = 1 given the assumption

[Kenny Lau]

which will allow you to deduce 2 \| 1

[Kenny Lau]

so it reduces to the first one

[Jia Ming]

Ooh rightt

[Mario Carneiro]

Hm, this didn't go as smoothly as I would hope

example : (∃ i : ℤ, (1/2 : ℝ) = ↑i) → false :=
begin
  rintro ⟨i, h⟩,
  have : (1/2 : ℚ) = i,
  { rw ← @rat.cast_inj ℝ,
    simpa using h },
  have := congr_arg rat.denom this,
  simp at this,
  cases this
end

[Mario Carneiro]

Kenny's proof goes a little better

example : (∃ i : ℤ, (1/2 : ℝ) = ↑i) → false :=
begin
  rintro ⟨i, h⟩,
  field_simp at h,
  norm_cast at h,
  have : (2:ℤ) ∣ 1 := ⟨i, by simpa [mul_comm] using h⟩,
  exact absurd this dec_trivial
end

[Jia Ming]

Awesome! Thanks

[Shing Tak Lam]

slightly different approach, I showed if there was such an integer, it'd be between 0 and 1.

example : (∃ i : ℤ, (1/2 : ℝ) = ↑i) → false :=
begin
  rintro ⟨x, hx⟩,
  have h1 : (0 : ℝ) < x, linarith,
  have h2 : (x : ℝ) < 1, linarith,
  norm_cast at h1 h2,
  linarith,
end