Mechanics of Proof, Example 3.2.6

Stream: new members

[JK]

I am having trouble with Mechanics of Proof, Example 3.2.6. The recommended solution uses Int.not_dvd_of_exists_lt_and_lt which I think no longer exists. I tried using Int.exists_lt_and_lt_iff_not_dvd instead, but

import Mathlib

example : ¬(5 : ℤ) ∣ 12 := by
  have h : 0 < 5 := by norm_num
  apply Int.exists_lt_and_lt_iff_not_dvd

doesn't change the goal. What am I doing wrong?

[Kenny Lau]

you can't apply an iff lemma, you rw it instead

[JK]

Changing the line to   rw [Int.exists_lt_and_lt_iff_not_dvd] doesn't work either.

[Kenny Lau]

you need to rewrite it backwards, the errors usually guide you

[JK]

<delete>

[Kenny Lau]

@JK

axiom P : Prop
axiom Q : Prop
axiom P_iff_Q : P ↔ Q

example : P := by
  rw [P_iff_Q]
  -- ⊢ Q

example : Q := by
  rw [P_iff_Q]
  /-
Tactic `rewrite` failed: Did not find an occurrence of the pattern
  P
in the target expression
  Q
  -/

example : Q := by
  apply P_iff_Q
  /-
Tactic `apply` failed: could not unify the type of `P_iff_Q`
  P ↔ Q
with the goal
  Q
  -/

[JK]

Thanks. I did find that

  rw [← Int.exists_lt_and_lt_iff_not_dvd]

worked.

[Kenny Lau]

Do you understand the error messages above?

[JK]

I understood the first one, at least